implement top-level definitions

3 files changed, 25 insertions, 0 deletions

diff --git a/src/driver/Driver.ml b/src/driver/Driver.ml
new file mode 100644
index 0000000..a2c4364
--- /dev/null
+++ b/src/driver/Driver.ml
@@ -0,0 +1,12 @@
+let process_item (toplvl : TopLevel.t) (item : Ast.item) : TopLevel.t =
+  let (name, item) = match item with
+    | Ast.Def { name; tp; tm } ->
+      let tp = Elaborator.check_tp_toplevel ~toplvl tp in
+      let tm = Elaborator.check_toplevel ~toplvl ~tm ~tp in
+      (name, TopLevel.Def { tp; tm = lazy (NbE.eval_toplevel tm) })
+  in
+  Yuujinchou.Trie.update_singleton name.value (fun _ -> Some (item, ())) toplvl
+
+let process_file (path : string) : TopLevel.t =
+  let file = Parser.parse_file path in
+  List.fold_left process_item Yuujinchou.Trie.empty file
diff --git a/src/driver/dune b/src/driver/dune
new file mode 100644
index 0000000..db5f824
--- /dev/null
+++ b/src/driver/dune
@@ -0,0 +1,12 @@
+(library
+ (name Driver)
+ (public_name toytt.driver)
+ (libraries
+  algaeff
+  bwd
+  toytt.ast
+  toytt.elaborator
+  toytt.error
+  toytt.nbe
+  toytt.parser
+  toytt.toplevel))
diff --git a/src/driver/test.toytt b/src/driver/test.toytt
new file mode 100644
index 0000000..273b42b
--- /dev/null
+++ b/src/driver/test.toytt
@@ -0,0 +1 @@
+def t : bool := true