blob: 57eec823bad4ab5c54e5e06142264755917ef16a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
let process_item (toplvl : TopLevel.t) (item : Ast.item) : TopLevel.t =
let (name, item) = match item with
| Ast.Def { name; args; tp; tm } ->
let (tp, tm) = Elaborator.check_def_toplevel ~toplvl ~args ~tp ~tm in
let item = TopLevel.Def {
tp = NbE.eval_toplevel tp;
tm = lazy (NbE.eval_toplevel tm);
} in
(name, item)
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
|