diff options
author | Malte Voos <git@mal.tc> | 2024-06-17 17:41:38 +0200 |
---|---|---|
committer | Malte Voos <git@mal.tc> | 2024-06-17 17:41:38 +0200 |
commit | 04d62df9fdd42c603fad7bb1b5e3fb49bf8550c1 (patch) | |
tree | 0a11c38a9f7bfad5624f0821b3a7041a9d4ff4d8 /bin | |
parent | edcd6c17b873b11b18016c9fe6efbe47576574ae (diff) | |
download | toytt-04d62df9fdd42c603fad7bb1b5e3fb49bf8550c1.tar.gz toytt-04d62df9fdd42c603fad7bb1b5e3fb49bf8550c1.zip |
implement typechecking
Diffstat (limited to 'bin')
-rw-r--r-- | bin/dune | 3 | ||||
-rw-r--r-- | bin/main.ml | 15 |
2 files changed, 15 insertions, 3 deletions
diff --git a/bin/dune b/bin/dune index 52ff1d3..2e2f594 100644 --- a/bin/dune +++ b/bin/dune @@ -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 () |