bin/main.ml


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
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
  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, Emp) Syntax.Pretty.pp (Quote.quote ~size:0 tp, Emp);
  repl ()

let () =
  Reporter.run ~emit:Term.display ~fatal:Term.display @@ fun () -> repl ()