diff options
author | Malte Voos <git@mal.tc> | 2024-07-08 22:01:42 +0200 |
---|---|---|
committer | Malte Voos <git@mal.tc> | 2024-07-08 22:01:42 +0200 |
commit | 97f84ccace4e634b4e02178a702818e69292dc9f (patch) | |
tree | 9cef95c62e3fa078db256c7fe657732fecef40a8 /src/driver/Driver.ml | |
parent | 57de10d8728f51942f676b68f1f3ea29d9b78e6e (diff) | |
download | toytt-97f84ccace4e634b4e02178a702818e69292dc9f.tar.gz toytt-97f84ccace4e634b4e02178a702818e69292dc9f.zip |
implement top-level definitions
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 |