diff options
Diffstat (limited to 'src/driver/Driver.ml')
-rw-r--r-- | src/driver/Driver.ml | 12 |
1 files changed, 12 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 |