src/bin/main.ml


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19

module Term = Asai.Tty.Make(Reporter.Message)

let ep input =
  let ast = Parser.parse_expr input in
  let (tp, tm) = Elaborator.infer_toplevel ast in
  let value = NbE.eval ~env:Emp tm in
  Format.printf "%a : %a\n%!"
    (Pretty.pp ~names:Emp) (NbE.quote ~size:0 value)
    (Pretty.pp ~names:Emp) (NbE.quote ~size:0 tp)

let rec repl () =
  match LNoise.linenoise "toytt> " with
  | Some input -> 
    Reporter.run ~emit:Term.display ~fatal:Term.display (fun () -> ep input);
    let _ = LNoise.history_add input in
    repl ()
  | None -> repl ()

let () = repl ();