From 04d62df9fdd42c603fad7bb1b5e3fb49bf8550c1 Mon Sep 17 00:00:00 2001
From: Malte Voos <git@mal.tc>
Date: Mon, 17 Jun 2024 17:41:38 +0200
Subject: implement typechecking

---
 bin/main.ml | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

(limited to 'bin/main.ml')

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 ()
-- 
cgit 1.4.1