diff options
Diffstat (limited to 'engine/evd.ml')
| -rw-r--r-- | engine/evd.ml | 59 |
1 files changed, 30 insertions, 29 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index c2f848291b..62d3963954 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -13,11 +13,13 @@ open Names open Nameops open Term open Vars -open Termops open Environ open Globnames open Context.Named.Declaration +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + (** Generic filters *) module Filter : sig @@ -226,7 +228,7 @@ let evar_instance_array test_id info args = if i < len then let c = Array.unsafe_get args i in if test_id d c then instrec filter ctxt (succ i) - else (get_id d, c) :: instrec filter ctxt (succ i) + else (NamedDecl.get_id d, c) :: instrec filter ctxt (succ i) else instance_mismatch () | _ -> instance_mismatch () in @@ -235,7 +237,7 @@ let evar_instance_array test_id info args = let map i d = if (i < len) then let c = Array.unsafe_get args i in - if test_id d c then None else Some (get_id d, c) + if test_id d c then None else Some (NamedDecl.get_id d, c) else instance_mismatch () in List.map_filter_i map (evar_context info) @@ -243,7 +245,7 @@ let evar_instance_array test_id info args = instrec filter (evar_context info) 0 let make_evar_instance_array info args = - evar_instance_array (isVarId % get_id) info args + evar_instance_array (NamedDecl.get_id %> isVarId) info args let instantiate_evar_array info c args = let inst = make_evar_instance_array info args in @@ -284,7 +286,7 @@ let metavars_of c = let rec collrec acc c = match kind_of_term c with | Meta mv -> Int.Set.add mv acc - | _ -> fold_constr collrec acc c + | _ -> Term.fold_constr collrec acc c in collrec Int.Set.empty c @@ -383,8 +385,7 @@ let add_name_newly_undefined naming evk evi (evtoid, idtoev as names) = | Misctypes.IntroAnonymous -> None | Misctypes.IntroIdentifier id -> if Idmap.mem id idtoev then - user_err_loc - (Loc.ghost,"",str "Already an existential evar of name " ++ pr_id id); + user_err (str "Already an existential evar of name " ++ pr_id id); Some id | Misctypes.IntroFresh id -> let id = Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) in @@ -685,7 +686,7 @@ let restrict evk filter ?candidates evd = | _ -> Evar.Set.add evk evd.last_mods in let evar_names = EvNames.reassign_name_defined evk evk' evd.evar_names in let ctxt = Filter.filter_list filter (evar_context evar_info) in - let id_inst = Array.map_of_list (mkVar % get_id) ctxt in + let id_inst = Array.map_of_list (NamedDecl.get_id %> mkVar) ctxt in let body = mkEvar(evk',id_inst) in let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in { evd with undf_evars = EvMap.add evk' evar_info' undf_evars; @@ -735,23 +736,22 @@ let evar_list c = let rec evrec acc c = match kind_of_term c with | Evar (evk, _ as ev) -> ev :: acc - | _ -> fold_constr evrec acc c in + | _ -> Term.fold_constr evrec acc c in evrec [] c let evars_of_term c = let rec evrec acc c = match kind_of_term c with | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l) - | _ -> fold_constr evrec acc c + | _ -> Term.fold_constr evrec acc c in evrec Evar.Set.empty c let evars_of_named_context nc = - List.fold_right (fun decl s -> - Option.fold_left (fun s t -> - Evar.Set.union s (evars_of_term t)) - (Evar.Set.union s (evars_of_term (get_type decl))) (get_value decl)) - nc Evar.Set.empty + Context.Named.fold_outside + (NamedDecl.fold_constr (fun constr s -> Evar.Set.union s (evars_of_term constr))) + nc + ~init:Evar.Set.empty let evars_of_filtered_evar_info evi = Evar.Set.union (evars_of_term evi.evar_concl) @@ -1273,7 +1273,9 @@ let protect f x = try f x with e -> str "EXCEPTION: " ++ str (Printexc.to_string e) -let print_constr a = protect print_constr a +let (f_print_constr, print_constr_hook) = Hook.make () + +let print_constr a = protect (fun c -> Hook.get f_print_constr (Global.env ()) c) a let pr_meta_map mmap = let pr_name = function @@ -1294,13 +1296,13 @@ let pr_meta_map mmap = prlist pr_meta_binding (metamap_to_list mmap) let pr_decl (decl,ok) = - let id = get_id decl in - match get_value decl with - | None -> if ok then pr_id id else (str "{" ++ pr_id id ++ str "}") - | Some c -> str (if ok then "(" else "{") ++ pr_id id ++ str ":=" ++ - print_constr c ++ str (if ok then ")" else "}") + match decl with + | LocalAssum (id,_) -> if ok then pr_id id else (str "{" ++ pr_id id ++ str "}") + | LocalDef (id,c,_) -> str (if ok then "(" else "{") ++ pr_id id ++ str ":=" ++ + print_constr c ++ str (if ok then ")" else "}") let pr_evar_source = function + | Evar_kinds.NamedHole id -> pr_id id | Evar_kinds.QuestionMark _ -> str "underscore" | Evar_kinds.CasesType false -> str "pattern-matching return predicate" | Evar_kinds.CasesType true -> @@ -1409,12 +1411,11 @@ let pr_evar_universe_context ctx = h 0 (Universes.pr_universe_opt_subst (UState.subst ctx)) ++ fnl()) let print_env_short env = - let pr_body n = function - | None -> pr_name n - | Some b -> str "(" ++ pr_name n ++ str " := " ++ print_constr b ++ str ")" in - let pr_named_decl decl = pr_body (Name (get_id decl)) (get_value decl) in - let pr_rel_decl decl = let open Context.Rel.Declaration in - pr_body (get_name decl) (get_value decl) in + let pr_rel_decl = function + | RelDecl.LocalAssum (n,_) -> pr_name n + | RelDecl.LocalDef (n,b,_) -> str "(" ++ pr_name n ++ str " := " ++ print_constr b ++ str ")" + in + let pr_named_decl = NamedDecl.to_rel_decl %> pr_rel_decl in let nc = List.rev (named_context env) in let rc = List.rev (rel_context env) in str "[" ++ pr_sequence pr_named_decl nc ++ str "]" ++ spc () ++ @@ -1433,11 +1434,11 @@ let pr_evar_constraints pbs = Namegen.make_all_name_different env in print_env_short env ++ spc () ++ str "|-" ++ spc () ++ - print_constr_env env t1 ++ spc () ++ + Hook.get f_print_constr env t1 ++ spc () ++ str (match pbty with | Reduction.CONV -> "==" | Reduction.CUMUL -> "<=") ++ - spc () ++ print_constr_env env t2 + spc () ++ Hook.get f_print_constr env t2 in prlist_with_sep fnl pr_evconstr pbs |