Adds a pair of function in Evar_util to gather dependent evars in an

[evar_map].

We also gather some metadata on these evars: if they are still undefined,
and if not, which evars have been used in their (partial) instantiation.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14720 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 56 insertions, 0 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index af9db2cdea..fd07680b54 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1461,6 +1461,47 @@ let evars_of_term c =
   in
   evrec Intset.empty c
 
+(* spiwack: a few functions to gather the existential variables
+   that occur in the types of goals present or past. *)
+let add_evars_of_evars_of_term acc evm c =
+  let evars = evars_of_term c in
+  Intset.fold begin fun e r ->
+    let body = (Evd.find evm e).evar_body in
+    let subevars =
+      match body with
+      | Evar_empty -> None
+      | Evar_defined c' -> Some (evars_of_term c')
+    in
+    Intmap.add e subevars r
+  end evars acc
+
+let evars_of_evars_of_term = add_evars_of_evars_of_term Intmap.empty
+
+let add_evars_of_evars_in_type acc evm e =
+  let evi = Evd.find evm e in
+  let acc_with_concl = add_evars_of_evars_of_term acc evm evi.evar_concl in
+  let hyps = Environ.named_context_of_val evi.evar_hyps in
+  List.fold_left begin fun r (_,b,t) ->
+    let r = add_evars_of_evars_of_term r evm t in
+    match b with
+    | None -> r
+    | Some b -> add_evars_of_evars_of_term r evm b
+  end acc_with_concl hyps
+
+let rec add_evars_of_evars_in_types_of_set acc evm s =
+  Intset.fold begin fun e r ->
+    let r = add_evars_of_evars_in_type r evm e in
+    match (Evd.find evm e).evar_body with
+    | Evar_empty -> r
+    | Evar_defined b -> add_evars_of_evars_in_types_of_set r evm (evars_of_term b)
+  end s acc
+
+let evars_of_evars_in_types_of_list evm l =
+  let set_of_l = List.fold_left (fun x y -> Intset.add y x) Intset.empty l in
+  add_evars_of_evars_in_types_of_set Intmap.empty evm set_of_l
+
+(* /spiwack *)
+
 let evars_of_named_context nc =
   List.fold_right (fun (_, b, t) s ->
     Option.fold_left (fun s t ->
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index c0c4252e68..36e64c9ad2 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -110,10 +110,25 @@ val solve_pattern_eqn : env -> constr list -> constr -> constr
 (** The following functions return the set of evars immediately
     contained in the object, including defined evars *)
 
+
 val evars_of_term : constr -> Intset.t
+
+(** returns the evars contained in the term associated with
+    the evars they contain themselves in their body, if any.
+    If the evar has no body, [None] is associated to it. *)
+val evars_of_evars_of_term : evar_map -> constr -> (Intset.t option) Intmap.t
 val evars_of_named_context : named_context -> Intset.t
 val evars_of_evar_info : evar_info -> Intset.t
 
+(** returns the evars which can be found in the typing context of the argument evars,
+    in the same format as {!evars_of_evars_of_term}.
+    It explores recursively the evars in the body of the argument evars -- but does
+    not return them. *)
+(* spiwack: tongue in cheek: it should have been called
+    [evars_of_evars_in_types_of_list_and_recursively_in_bodies] *)
+val evars_of_evars_in_types_of_list : evar_map -> evar list -> (Intset.t option) Intmap.t
+
+
 (** 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