aboutsummaryrefslogtreecommitdiff
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 ();