diff options
| -rw-r--r-- | pretyping/coercion.ml | 2 | ||||
| -rw-r--r-- | pretyping/evarutil.ml | 5 | ||||
| -rw-r--r-- | pretyping/evarutil.mli | 2 | ||||
| -rw-r--r-- | proofs/goal.ml | 9 | ||||
| -rw-r--r-- | toplevel/autoinstance.ml | 33 | ||||
| -rw-r--r-- | toplevel/command.ml | 8 | ||||
| -rw-r--r-- | toplevel/obligations.ml | 5 | ||||
| -rw-r--r-- | toplevel/record.ml | 10 |
8 files changed, 36 insertions, 38 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index fb5569e2e..93cfdd9be 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -308,8 +308,6 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) [| u; p; cx; evar |]))) | None -> raise NoSubtacCoercion - (*evdref := Evd.add_conv_pb (Reduction.CONV, x, y) !evdref; - None*) in coerce_unify env x y let coerce_itf loc env evd v t c1 = diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 1972aee28..b1dec0fd0 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -315,6 +315,11 @@ let push_rel_context_to_named_context env typ = let default_source = (Loc.ghost,Evar_kinds.InternalHole) +let new_pure_evar_full evd evi = + let evk = new_untyped_evar () in + let evd = Evd.add evd evk evi in + (evd, evk) + let new_pure_evar evd sign ?(src=default_source) ?filter ?candidates typ = let newevk = new_untyped_evar() in let evd = evar_declare sign newevk typ ~src ?filter ?candidates evd in diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 7d917f15b..0d482e9b0 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -36,6 +36,8 @@ val new_pure_evar : evar_map -> named_context_val -> ?src:Loc.t * Evar_kinds.t -> ?filter:bool list -> ?candidates:constr list -> types -> evar_map * evar +val new_pure_evar_full : evar_map -> evar_info -> evar_map * evar + (** the same with side-effects *) val e_new_evar : evar_map ref -> env -> ?src:Loc.t * Evar_kinds.t -> ?filter:bool list -> diff --git a/proofs/goal.ml b/proofs/goal.ml index c6e2c2ed9..50541151a 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -496,7 +496,6 @@ module V82 = struct (* Old style mk_goal primitive *) let mk_goal evars hyps concl extra = - let evk = Evarutil.new_untyped_evar () in let evi = { Evd.evar_hyps = hyps; Evd.evar_concl = concl; Evd.evar_filter = List.map (fun _ -> true) @@ -507,7 +506,7 @@ module V82 = struct Evd.evar_extra = extra } in let evi = Typeclasses.mark_unresolvable evi in - let evars = Evd.add evars evk evi in + let (evars, evk) = Evarutil.new_pure_evar_full evars evi in let ids = List.map Util.pi1 (Environ.named_context_of_val hyps) in let inst = Array.of_list (List.map mkVar ids) in let ev = Term.mkEvar (evk,inst) in @@ -525,8 +524,7 @@ module V82 = struct marked unresolvable for typeclasses, as non-empty Store.t-s happen to have functional content. *) let evi = Evd.make_evar Environ.empty_named_context_val Term.mkProp in - let evk = Evarutil.new_untyped_evar () in - let sigma = Evd.add Evd.empty evk evi in + let (sigma, evk) = Evarutil.new_pure_evar_full Evd.empty evi in { Evd.it = build evk ; Evd.sigma = sigma; eff = Declareops.no_seff } (* Makes a goal out of an evar *) @@ -568,8 +566,7 @@ module V82 = struct let new_evi = { evi with Evd.evar_hyps = new_hyps; Evd.evar_filter = new_filter } in let new_evi = Typeclasses.mark_unresolvable new_evi in - let evk = Evarutil.new_untyped_evar () in - let new_sigma = Evd.add Evd.empty evk new_evi in + let (new_sigma, evk) = Evarutil.new_pure_evar_full Evd.empty new_evi in { Evd.it = build evk ; sigma = new_sigma; eff = Declareops.no_seff } (* Used by the compatibility layer and typeclasses *) diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml index b13d2ea29..10b3febb3 100644 --- a/toplevel/autoinstance.ml +++ b/toplevel/autoinstance.ml @@ -47,14 +47,14 @@ let rec subst_evar evar def n c = | _ -> map_constr_with_binders (fun n->n+1) (subst_evar evar def) n c let subst_evar_in_evm evar def evm = - Evd.fold - (fun ev evi acc -> - let evar_body = match evi.evar_body with - | Evd.Evar_empty -> Evd.Evar_empty - | Evd.Evar_defined c -> Evd.Evar_defined (subst_evar evar def 0 c) in - let evar_concl = subst_evar evar def 0 evi.evar_concl in - Evd.add acc ev {evi with evar_body=evar_body; evar_concl=evar_concl} - ) evm empty + let map ev evi = + let evar_body = match evi.evar_body with + | Evd.Evar_empty -> Evd.Evar_empty + | Evd.Evar_defined c -> Evd.Evar_defined (subst_evar evar def 0 c) in + let evar_concl = subst_evar evar def 0 evi.evar_concl in + {evi with evar_body=evar_body; evar_concl=evar_concl} + in + Evd.raw_map map evm (* Tries to define ev by c in evd. Fails if ev := c1 and c1 /= c ev : * T1, c : T2 and T1 /= T2. Defines recursively all evars instantiated @@ -80,21 +80,16 @@ let rec safe_define evm ev c = define_subst (Evd.define ev c evm) (Termops.filtering [] Reduction.CUMUL t u) let add_gen_ctx (cl,gen,evm) ctx : signature * constr list = - let rec really_new_evar () = - let ev = Evarutil.new_untyped_evar() in - if Evd.is_evar evm ev then really_new_evar() else ev in - let add_gen_evar (cl,gen,evm) ev ty : signature = - let evm = Evd.add evm ev (Evd.make_evar Environ.empty_named_context_val ty) in - (cl,ev::gen,evm) in + let env = Environ.empty_named_context_val in + let fold_new_evar evm _ = Evarutil.new_pure_evar evm env mkProp in let rec mksubst b = function | [] -> [] | a::tl -> b::(mksubst (a::b) tl) in - let evl = List.map (fun _ -> really_new_evar()) ctx in + let (evm, evl) = List.fold_map fold_new_evar evm ctx in let evcl = List.map (fun i -> mkEvar (i,[||])) evl in - let substl = List.rev (mksubst [] (evcl)) in - let ctx = List.map2 (fun s t -> substnl s 0 t) substl ctx in - let sign = List.fold_left2 add_gen_evar (cl,gen,evm) (List.rev evl) ctx in - sign,evcl +(* let substl = List.rev (mksubst [] (evcl)) in *) +(* let ctx = List.map2 (fun s t -> substnl s 0 t) substl ctx in *) + (cl, evl @ gen, evm), evcl (* TODO : for full proof-irrelevance in the search, provide a real compare function for constr instead of Pervasive's one! *) diff --git a/toplevel/command.ml b/toplevel/command.ml index 9f24fc158..118a13ead 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -889,11 +889,6 @@ let out_def = function | Some def -> def | None -> error "Program Fixpoint needs defined bodies." -let collect_evars_of_term evd c ty = - let evars = Int.Set.union (evars_of_term c) (evars_of_term ty) in - Int.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev)) - evars Evd.empty - let do_program_recursive local fixkind fixl ntns = let isfix = fixkind != Obligations.IsCoFixpoint in let (env, rec_sign, evd), fix, info = @@ -911,9 +906,8 @@ let do_program_recursive local fixkind fixl ntns = and typ = nf_evar evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign) in - let evm = collect_evars_of_term evd def typ in let evars, _, def, typ = - Obligations.eterm_obligations env id evm + Obligations.eterm_obligations env id evd (List.length rec_sign) def typ in (id, def, typ, imps, evars) in diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 3d85d3faf..0f49662c8 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -202,12 +202,17 @@ let sort_dependencies evl = open Environ +let collect_evars_of_term c ty = + Int.Set.union (Evarutil.evars_of_term c) (Evarutil.evars_of_term ty) + let eterm_obligations env name evm fs ?status t ty = (* 'Serialize' the evars *) + let evars = collect_evars_of_term t ty in let nc = Environ.named_context env in let nc_len = Context.named_context_length nc in let evm = Evarutil.nf_evar_map_undefined evm in let evl = Evarutil.non_instantiated evm in + let evl = ExistentialMap.filter (fun ev _ -> Int.Set.mem ev evars) evl in let evl = ExistentialMap.bindings evl in let evl = List.map (fun (id, ev) -> (id, ev, evar_dependencies evm id)) evl in let sevl = sort_dependencies evl in diff --git a/toplevel/record.ml b/toplevel/record.ml index 5c59987aa..e0dc6c3a3 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -221,11 +221,13 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls let structure_signature ctx = let rec deps_to_evar evm l = match l with [] -> Evd.empty - | [(_,_,typ)] -> Evd.add evm (Evarutil.new_untyped_evar()) - (Evd.make_evar Environ.empty_named_context_val typ) + | [(_,_,typ)] -> + let env = Environ.empty_named_context_val in + let (evm, _) = Evarutil.new_pure_evar evm env typ in + evm | (_,_,typ)::tl -> - let ev = Evarutil.new_untyped_evar() in - let evm = Evd.add evm ev (Evd.make_evar Environ.empty_named_context_val typ) in + let env = Environ.empty_named_context_val in + let (evm, ev) = Evarutil.new_pure_evar evm env typ in let new_tl = Util.List.map_i (fun pos (n,c,t) -> n,c, Termops.replace_term (mkRel pos) (mkEvar(ev,[||])) t) 1 tl in |