2 files changed, 30 insertions, 0 deletions
diff --git a/src/bin/dune b/src/bin/dune
new file mode 100644
index 0000000..980d799
--- /dev/null
+++ b/src/bin/dune
@@ -0,0 +1,11 @@
+(executable
+ (public_name toytt)
+ (name main)
+ (libraries
+  asai
+  linenoise
+  toytt.elaborator
+  toytt.nbe
+  toytt.parser
+  toytt.reporter
+  ))
diff --git a/src/bin/main.ml b/src/bin/main.ml
new file mode 100644
index 0000000..f762d26
--- /dev/null
+++ b/src/bin/main.ml
@@ -0,0 +1,19 @@
+module Term = Asai.Tty.Make(Reporter.Message)
+
+let ep input =
+  let ast = Parser.parse_expr input in
+  let (tp, tm) = Elaborator.infer_toplevel ast in
+  let value = NbE.eval ~env:Emp tm in
+  Format.printf "%a : %a\n%!"
+    (Pretty.pp ~names:Emp) (NbE.quote ~size:0 value)
+    (Pretty.pp ~names:Emp) (NbE.quote ~size:0 tp)
+
+let rec repl () =
+  match LNoise.linenoise "toytt> " with
+  | Some input -> 
+    Reporter.run ~emit:Term.display ~fatal:Term.display (fun () -> ep input);
+    let _ = LNoise.history_add input in
+    repl ()
+  | None -> repl ()
+
+let () = repl ();