2 files changed, 35 insertions, 15 deletions
diff --git a/src/bin/dune b/src/bin/dune
index f11979a..87fe556 100644
--- a/src/bin/dune
+++ b/src/bin/dune
@@ -4,8 +4,8 @@
  (libraries
   asai
   linenoise
-  toytt.elaborator
-  toytt.nbe
-  toytt.parser
+  yuujinchou
   toytt.error
-  ))
+  toytt.driver
+  toytt.parser
+  toytt.toplevel))
diff --git a/src/bin/main.ml b/src/bin/main.ml
index e1be039..4cbeef7 100644
--- a/src/bin/main.ml
+++ b/src/bin/main.ml
@@ -1,19 +1,39 @@
 module Term = Asai.Tty.Make(Error.Message)
 
-let ep input =
+let display = Term.display ~show_backtrace:false
+
+let handle_error f =
+  Error.run ~emit:display ~fatal:display f
+
+let handle_fatal f =
+  Error.run ~emit:display ~fatal:(fun msg -> display msg; exit 1) f
+
+let ep ~toplvl input =
   let ast = Parser.parse_expr input in
-  let (tp, tm) = Elaborator.infer_toplevel ast in
-  let value = NbE.eval ~env:Emp tm in
+  let toplvl = Option.value toplvl ~default:Yuujinchou.Trie.empty in
+  let (tp, tm) = Elaborator.infer_toplevel ~toplvl ast in
+  let value = NbE.eval_toplevel 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)
+    (Pretty.pp ~names:Emp) (NbE.quote_toplevel @@ NbE.force_all value)
+    (Pretty.pp ~names:Emp) (NbE.quote_toplevel @@ NbE.force_all tp)
 
-let rec repl () =
+let rec repl ~toplvl () =
   match LNoise.linenoise "toytt> " with
-  | Some input -> 
-    Error.run ~emit:(Term.display ~show_backtrace:false) ~fatal:(Term.display ~show_backtrace:false) (fun () -> ep input);
+  | Some input ->
+    handle_error (fun () -> ep ~toplvl input);
     let _ = LNoise.history_add input in
-    repl ()
-  | None -> repl ()
+    repl ~toplvl ()
+  | None -> repl ~toplvl ()
+
+let input_file = ref None
 
-let () = repl ();
+let () =
+  let anon_fun path = input_file := Some path in
+  let usage_msg = "usage: toytt [input file]" in
+  let () = Arg.parse [] anon_fun usage_msg in
+  match !input_file with
+  | None ->
+    repl ~toplvl:None ()
+  | Some path ->
+    let toplvl = handle_fatal (fun () -> Driver.process_file path) in
+    repl ~toplvl:(Some toplvl) ()