aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--pretyping/evarutil.ml31
-rw-r--r--pretyping/evarutil.mli12
-rw-r--r--pretyping/evd.ml46
-rw-r--r--pretyping/evd.mli17
-rw-r--r--proofs/goal.ml2
-rw-r--r--proofs/proofview.ml2
-rw-r--r--tactics/class_tactics.ml2
-rw-r--r--tactics/equality.ml2
-rw-r--r--tactics/evar_tactics.ml8
-rw-r--r--tactics/extratactics.ml42
-rw-r--r--toplevel/obligations.ml10
11 files changed, 71 insertions, 63 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 7b1fee543..64bdb90a2 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -128,6 +128,11 @@ let nf_evar_map_undefined evm =
(* Auxiliary functions for the conversion algorithms modulo evars
*)
+(* A probably faster though more approximative variant of
+ [has_undefined (nf_evar c)]: instances are not substituted and
+ maybe an evar occurs in an instance and it would disappear by
+ instantiation *)
+
let has_undefined_evars evd t =
let rec has_ev t =
match kind_of_term t with
@@ -536,17 +541,6 @@ let clear_hyps2_in_evi evdref hyps t concl ids =
| (nhyps,[t;nconcl]) -> (nhyps,t,nconcl)
| _ -> assert false
-(** The following functions return the set of evars immediately
- contained in the object, including defined evars *)
-
-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
- in
- evrec Evar.Set.empty c
-
(* spiwack: a few functions to gather evars on which goals depend. *)
let queue_set q is_dependent set =
Evar.Set.iter (fun a -> Queue.push (is_dependent,a) q) set
@@ -594,21 +588,6 @@ let gather_dependent_evars evm l =
(* /spiwack *)
-let evars_of_named_context nc =
- List.fold_right (fun (_, b, t) s ->
- Option.fold_left (fun s t ->
- Evar.Set.union s (evars_of_term t))
- (Evar.Set.union s (evars_of_term t)) b)
- nc Evar.Set.empty
-
-let evars_of_evar_info evi =
- Evar.Set.union (evars_of_term evi.evar_concl)
- (Evar.Set.union
- (match evi.evar_body with
- | Evar_empty -> Evar.Set.empty
- | Evar_defined b -> evars_of_term b)
- (evars_of_named_context (named_context_of_val evi.evar_hyps)))
-
(** The following functions return the set of undefined evars
contained in the object, the defined evars being traversed.
This is roughly a combination of the previous functions and
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index b90a78434..8a07cce5d 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -82,8 +82,9 @@ val head_evar : constr -> existential_key (** may raise NoHeadEvar *)
(* Expand head evar if any *)
val whd_head_evar : evar_map -> constr -> constr
-(* [has_undefined_evars evd c] checks if [c] has undefined evars. *)
+(* An over-approximation of [has_undefined (nf_evars evd c)] *)
val has_undefined_evars : evar_map -> constr -> bool
+
val is_ground_term : evar_map -> constr -> bool
val is_ground_env : evar_map -> env -> bool
(** [check_evars env initial_sigma extended_sigma c] fails if some
@@ -101,15 +102,6 @@ val define_evar_as_sort : env -> evar_map -> existential -> evar_map * sorts
val evar_absorb_arguments : env -> evar_map -> existential -> constr list ->
evar_map * existential
-(** The following functions return the set of evars immediately
- contained in the object, including defined evars *)
-
-
-val evars_of_term : constr -> Evar.Set.t
-
-val evars_of_named_context : named_context -> Evar.Set.t
-val evars_of_evar_info : evar_info -> Evar.Set.t
-
(** [gather_dependent_evars evm seeds] classifies the evars in [evm]
as dependent_evars and goals (these may overlap). A goal is an
evar in [seeds] or an evar appearing in the (partial) definition
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 63e25a541..fd104d847 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -901,12 +901,10 @@ let loc_of_conv_pb evd (pbty,env,t1,t2) =
| Evar (evk2,_) -> fst (evar_source evk2 evd)
| _ -> Loc.ghost
-let evar_list evd c =
- let rec evrec acc c =
- match kind_of_term c with
- | Evar (evk, _ as ev) when mem evd evk -> ev :: acc
- | _ -> fold_constr evrec acc c in
- evrec [] c
+(** The following functions return the set of evars immediately
+ contained in the object *)
+
+(* including defined evars, excluding instances *)
let collect_evars c =
let rec collrec acc c =
@@ -916,6 +914,40 @@ let collect_evars c =
in
collrec Evar.Set.empty c
+(* including defined evars and instances of evars *)
+
+(* excluding defined evars *)
+
+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
+ 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
+ in
+ evrec Evar.Set.empty c
+
+let evars_of_named_context nc =
+ List.fold_right (fun (_, b, t) s ->
+ Option.fold_left (fun s t ->
+ Evar.Set.union s (evars_of_term t))
+ (Evar.Set.union s (evars_of_term t)) b)
+ nc Evar.Set.empty
+
+let evars_of_filtered_evar_info evi =
+ Evar.Set.union (evars_of_term evi.evar_concl)
+ (Evar.Set.union
+ (match evi.evar_body with
+ | Evar_empty -> Evar.Set.empty
+ | Evar_defined b -> evars_of_term b)
+ (evars_of_named_context (evar_filtered_context evi)))
+
(**********************************************************)
(* Side effects *)
@@ -1669,7 +1701,7 @@ let compute_evar_dependency_graph (sigma : evar_map) =
in
match evar_body evi with
| Evar_empty -> assert false
- | Evar_defined c -> Evar.Set.fold fold_ev (collect_evars c) acc
+ | Evar_defined c -> Evar.Set.fold fold_ev (evars_of_term c) acc
in
EvMap.fold fold sigma.defn_evars EvMap.empty
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index db4515ae8..22768fb69 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -82,6 +82,7 @@ type evar_body =
| Evar_empty
| Evar_defined of constr
+
module Store : Store.S
(** Datatype used to store additional information in evar maps. *)
@@ -374,8 +375,20 @@ val extract_changed_conv_pbs : evar_map ->
val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list
val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t
-val evar_list : evar_map -> constr -> existential list
-val collect_evars : constr -> Evar.Set.t
+(** The following functions return the set of evars immediately
+ contained in the object; need the term to be evar-normal otherwise
+ defined evars are returned too. *)
+
+val evar_list : constr -> existential list
+ (** excluding evars in instances of evars and collected with
+ redundancies from right to left (used by tactic "instantiate") *)
+
+val evars_of_term : constr -> Evar.Set.t
+ (** including evars in instances of evars *)
+
+val evars_of_named_context : named_context -> Evar.Set.t
+
+val evars_of_filtered_evar_info : evar_info -> Evar.Set.t
(** Metas *)
val meta_list : evar_map -> (metavariable * clbinding) list
diff --git a/proofs/goal.ml b/proofs/goal.ml
index b0fccc42f..ce7f5959a 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -101,7 +101,7 @@ let equal evars1 gl1 evars2 gl2 =
[evi]. Note: since we want to use it on goals, the body is actually
supposed to be empty. *)
let contained_in_info sigma e evi =
- Evar.Set.mem e (Evarutil.(evars_of_evar_info (nf_evar_info sigma evi)))
+ Evar.Set.mem e (Evd.evars_of_filtered_evar_info (Evarutil.nf_evar_info sigma evi))
(* [depends_on sigma src tgt] checks whether the goal [src] appears as an
existential variable in the definition of the goal [tgt] in [sigma]. *)
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 931d4a2b3..2e65aa8d7 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -816,7 +816,7 @@ module V82 = struct
let top_evars initial =
let evars_of_initial (c,_) =
- Evar.Set.elements (Evarutil.evars_of_term c)
+ Evar.Set.elements (Evd.evars_of_term c)
in
List.flatten (List.map evars_of_initial initial)
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 35889462b..d9f90b02e 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -157,7 +157,7 @@ and e_my_find_search db_list local_db hdc complete sigma concl =
try
let cl = Typeclasses.class_info (fst hdc) in
if cl.cl_strict then
- Evarutil.evars_of_term concl
+ Evd.evars_of_term concl
else Evar.Set.empty
with _ -> Evar.Set.empty
in
diff --git a/tactics/equality.ml b/tactics/equality.ml
index c524e67ce..79e852815 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -127,7 +127,7 @@ let freeze_initial_evars sigma flags clause =
(* We take evars of the type: this may include old evars! For excluding *)
(* all old evars, including the ones occurring in the rewriting lemma, *)
(* we would have to take the clenv_value *)
- let newevars = Evd.collect_evars (clenv_type clause) in
+ let newevars = Evd.evars_of_term (clenv_type clause) in
let evars =
fold_undefined (fun evk _ evars ->
if Evar.Set.mem evk newevars then evars
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 7c4c9c965..b569ef97f 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -35,20 +35,20 @@ let instantiate_tac n c ido =
let sigma = gl.sigma in
let evl =
match ido with
- ConclLocation () -> evar_list sigma (pf_concl gl)
+ ConclLocation () -> evar_list (pf_concl gl)
| HypLocation (id,hloc) ->
let decl = Environ.lookup_named_val id (Goal.V82.hyps sigma (sig_it gl)) in
match hloc with
InHyp ->
(match decl with
- (_,None,typ) -> evar_list sigma typ
+ (_,None,typ) -> evar_list typ
| _ -> error
"Please be more specific: in type or value?")
| InHypTypeOnly ->
- let (_, _, typ) = decl in evar_list sigma typ
+ let (_, _, typ) = decl in evar_list typ
| InHypValueOnly ->
(match decl with
- (_,Some body,_) -> evar_list sigma body
+ (_,Some body,_) -> evar_list body
| _ -> error "Not a defined hypothesis.") in
if List.length evl < n then
error "Not enough uninstantiated existential variables.";
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index ffd164d16..34f5b52eb 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -665,7 +665,7 @@ END
let hget_evar n gl =
let sigma = project gl in
- let evl = evar_list sigma (pf_concl gl) in
+ let evl = evar_list (pf_concl gl) in
if List.length evl < n then
error "Not enough uninstantiated existential variables.";
if n <= 0 then error "Incorrect existential variable index.";
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 1c556d9b6..2ac4339c1 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -153,19 +153,11 @@ let rec chop_product n t =
| Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None
| _ -> None
-let evars_of_evar_info evi =
- Evar.Set.union (Evarutil.evars_of_term evi.evar_concl)
- (Evar.Set.union
- (match evi.evar_body with
- | Evar_empty -> Evar.Set.empty
- | Evar_defined b -> Evarutil.evars_of_term b)
- (Evarutil.evars_of_named_context (evar_filtered_context evi)))
-
let evar_dependencies evm oev =
let one_step deps =
Evar.Set.fold (fun ev s ->
let evi = Evd.find evm ev in
- let deps' = evars_of_evar_info evi in
+ let deps' = evars_of_filtered_evar_info evi in
if Evar.Set.mem oev deps' then
invalid_arg ("Ill-formed evar map: cycle detected for evar " ^ string_of_existential oev)
else Evar.Set.union deps' s)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 06:51:30 +0000