diff options
Diffstat (limited to 'bin')
| -rw-r--r-- | bin/dune | 3 | ||||
| -rw-r--r-- | bin/main.ml | 15 |
2 files changed, 15 insertions, 3 deletions
@@ -1,4 +1,5 @@ (executable (public_name toytt) (name main) - (libraries toytt)) + (libraries toytt) + (modes byte exe)) 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 () |