module Term = Asai.Tty.Make(Error.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 -> 
    Error.run ~emit:(Term.display ~show_backtrace:false) ~fatal:(Term.display ~show_backtrace:false) (fun () -> ep input);
    let _ = LNoise.history_add input in
    repl ()
  | None -> repl ()

let () = repl ();