about summary refs log tree commit diff
path: root/src/bin
diff options
context:
space:
mode:
authorMalte Voos <git@mal.tc>2024-06-23 23:31:59 +0200
committerMalte Voos <git@mal.tc>2024-06-24 00:16:55 +0200
commit5d227bcd0055d02e1d49a3dcd27e80a756923d5b (patch)
treeda468ad3a8f3caf709b731ca2678c86a5a015990 /src/bin
parent8d40541003736d5319ec981278338e8c8c66daf6 (diff)
downloadtoytt-5d227bcd0055d02e1d49a3dcd27e80a756923d5b.tar.gz
toytt-5d227bcd0055d02e1d49a3dcd27e80a756923d5b.zip
split code into smaller libraries and make a better repl
Diffstat (limited to 'src/bin')
-rw-r--r--src/bin/dune11
-rw-r--r--src/bin/main.ml19
2 files changed, 30 insertions, 0 deletions
diff --git a/src/bin/dune b/src/bin/dune
new file mode 100644
index 0000000..980d799
--- /dev/null
+++ b/src/bin/dune
@@ -0,0 +1,11 @@
+(executable
+ (public_name toytt)
+ (name main)
+ (libraries
+  asai
+  linenoise
+  toytt.elaborator
+  toytt.nbe
+  toytt.parser
+  toytt.reporter
+  ))
diff --git a/src/bin/main.ml b/src/bin/main.ml
new file mode 100644
index 0000000..f762d26
--- /dev/null
+++ b/src/bin/main.ml
@@ -0,0 +1,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 ();