about summary refs log tree commit diff
path: root/bin/main.ml
diff options
context:
space:
mode:
Diffstat (limited to 'bin/main.ml')
-rw-r--r--bin/main.ml15
1 files changed, 13 insertions, 2 deletions
diff --git a/bin/main.ml b/bin/main.ml
index 6c62764..ec5c4d2 100644
--- a/bin/main.ml
+++ b/bin/main.ml
@@ -1,14 +1,25 @@
 open Toytt
 
+module Term = Asai.Tty.Make(Reporter.Message)
+
 let parse (s : string) : Ast.expr =
   let lexbuf = Lexing.from_string s in
+  let string_source : Asai.Range.string_source = {
+    title = None;
+    content = s;
+  } in
+  let source = `String string_source in
+  ParserEff.Eff.run ~env:source @@ fun () ->
   let ast = Parser.parse Lexer.lex lexbuf in
   ast
 
 let rec repl () =
   let input = read_line () in
   let ast = parse input in
-  Format.printf "%a\n%!" Ast.pp_expr ast;
+  let (tp, tm) = Elab.infer_toplevel ast in
+  let value = Eval.eval ~env:Emp tm in
+  Format.printf "%a : %a\n%!" Syntax.Pretty.pp (Quote.quote ~size:0 value) Syntax.Pretty.pp (Quote.quote ~size:0 tp);
   repl ()
 
-let () = repl ()
+let () =
+  Reporter.run ~emit:Term.display ~fatal:Term.display @@ fun () -> repl ()