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