- let rec aux env term =
- match term with
- | AttributedTerm (_, term) -> aux env term
- | Appl terms -> Appl (List.map (aux env) terms)
- | Binder (binder, var, body) ->
- Binder (binder, aux_capture_var env var, aux env body)
- | Case (term, indty, outty_opt, patterns) ->
- Case (aux env term, indty, aux_opt env outty_opt,
- List.map (aux_branch env) patterns)
- | LetIn (var, t1, t2) ->
- LetIn (aux_capture_var env var, aux env t1, aux env t2)
- | LetRec (kind, definitions, body) ->
- LetRec (kind, List.map (aux_definition env) definitions, aux env body)
- | Uri (name, None) -> Uri (name, None)
- | Uri (name, Some substs) -> Uri (name, Some (aux_substs env substs))
- | Ident (name, Some substs) -> Ident (name, Some (aux_substs env substs))
- | Meta (index, substs) -> Meta (index, aux_meta_substs env substs)
-
- | Implicit
- | Ident _
- | Num _
- | Sort _
- | Symbol _
- | UserInput -> term
-
- | Magic magic -> aux_magic env magic
- | Variable var -> aux_variable env var
-
- | _ -> assert false
- and aux_opt env = function
- | Some term -> Some (aux env term)
- | None -> None
- and aux_capture_var env (name, ty_opt) = (aux env name, aux_opt env ty_opt)
- and aux_branch env (pattern, term) =
- (aux_pattern env pattern, aux env term)
- and aux_pattern env (head, vars) =
- (head, List.map (aux_capture_var env) vars)
- and aux_definition env (var, term, i) =
- (aux_capture_var env var, aux env term, i)
- and aux_substs env substs =
- List.map (fun (name, term) -> (name, aux env term)) substs
- and aux_meta_substs env meta_substs = List.map (aux_opt env) meta_substs
- and aux_variable env = function
- | NumVar name -> Num (lookup_num ~env name, 0)
- | IdentVar name -> Ident (lookup_string ~env name, None)
- | TermVar name -> lookup_term ~env name
- | FreshVar name -> Ident (lookup_fresh_name name, None)
- | Ascription (term, name) -> assert false
- and aux_magic env = function
- | Default (some_pattern, none_pattern) ->
- (match meta_names_of some_pattern with
- | [] -> assert false (* some pattern must contain at least 1 name *)
- | (name :: _) as names ->
- (match lookup_value ~env name with
- | OptValue (Some _) ->
- (* assumption: if "name" above is bound to Some _, then all
- * names returned by "meta_names_of" are bound to Some _ as well
- *)
- aux (unopt_names names env) some_pattern
- | OptValue None -> aux env none_pattern
- | _ -> assert false))
- | Fold (`Left, base_pattern, names, rec_pattern) ->
- let acc_name = List.hd names in (* names can't be empty, cfr. parser *)
- let meta_names =
- List.filter ((<>) acc_name) (meta_names_of rec_pattern)
- in
- (match meta_names with
- | [] -> assert false (* as above *)
- | (name :: _) as names ->
- let rec instantiate_fold_left acc env' =
- prerr_endline "instantiate_fold_left";
- match lookup_value ~env:env' name with
- | ListValue (_ :: _) ->
- instantiate_fold_left
- (let acc_binding = acc_name, (TermType, TermValue acc) in
- aux (acc_binding :: head_names names env') rec_pattern)
- (tail_names names env')
- | ListValue [] -> acc
- | _ -> assert false
- in
- instantiate_fold_left (aux env base_pattern) env)
- | Fold (`Right, base_pattern, names, rec_pattern) ->
- let acc_name = List.hd names in (* names can't be empty, cfr. parser *)
- let meta_names =
- List.filter ((<>) acc_name) (meta_names_of rec_pattern)
- in
- (match meta_names with
- | [] -> assert false (* as above *)
- | (name :: _) as names ->
- let rec instantiate_fold_right env' =
- prerr_endline "instantiate_fold_right";
- match lookup_value ~env:env' name with
- | ListValue (_ :: _) ->
- let acc = instantiate_fold_right (tail_names names env') in
- let acc_binding = acc_name, (TermType, TermValue acc) in
- aux (acc_binding :: head_names names env') rec_pattern
- | ListValue [] -> aux env base_pattern
- | _ -> assert false
- in
- instantiate_fold_right env)
- | _ -> assert false