Another correction to the dependent existential variable printing

for emacs mode.

Hopefully fixes Bug 2678 this time. Much saner and more compact code.

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

3 files changed, 52 insertions, 52 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 7a9b415598..036bed5252 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1772,48 +1772,50 @@ 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
+(* spiwack: a few functions to gather evars on which goals depend. *)
+let queue_set q is_dependent set =
+  Intset.iter (fun a -> Queue.push (is_dependent,a) q) set
+let queue_term q is_dependent c =
+  queue_set q is_dependent (evars_of_term c)
 
-let add_evars_of_evars_in_type acc evm e =
+let process_dependent_evar q acc evm is_dependent 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
+  (* Queues evars appearing in the types of the goal (conclusion, then
+     hypotheses), they are all dependent. *)
+  queue_term q true evi.evar_concl;
+  List.iter begin fun (_,b,t) ->
+    queue_term q true t;
     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 ->
-        (* Adds the evars used to define [b] to the binding map. *)
-        let r = add_evars_of_evars_of_term r evm b in
-        (* Goes recursively in the [evar_info] of each of these evar. *)
-        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
+    | None -> ()
+    | Some b -> queue_term q true b
+  end (Environ.named_context_of_val evi.evar_hyps);
+  match evi.evar_body with
+  | Evar_empty ->
+      if is_dependent then Intmap.add e None acc else acc
+  | Evar_defined b ->
+      let subevars = evars_of_term b in
+      (* evars appearing in the definition of an evar [e] are marked
+         as dependent when [e] is dependent itself: if [e] is a
+         non-dependent goal, then, unless they are reach from another
+         path, these evars are just other non-dependent goals. *)
+      queue_set q is_dependent subevars;
+      if is_dependent then Intmap.add e (Some subevars) acc else acc
+
+let gather_dependent_evars q evm =
+  let acc = ref Intmap.empty in
+  while not (Queue.is_empty q) do
+    let (is_dependent,e) = Queue.pop q in
+    (* checks if [e] has already been added to [!acc] *)
+    begin if not (Intmap.mem e !acc) then
+        acc := process_dependent_evar q !acc evm is_dependent e  
+    end
+  done;
+  !acc
+
+let gather_dependent_evars evm l =
+  let q = Queue.create () in
+  List.iter (fun a -> Queue.add (false,a) q) l;
+  gather_dependent_evars q evm
 
 (* /spiwack *)
 
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 77985c8d73..41e8e0e187 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -120,21 +120,19 @@ val solve_pattern_eqn : env -> constr list -> constr -> constr
 
 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
-
+(** [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
+    of a goal. A dependent evar is an evar appearing in the type
+    (hypotheses and conclusion) of a goal, or in the type or (partial)
+    definition of a dependent evar.  The value return is a map
+    associating to each dependent evar [None] if it has no (partial)
+    definition or [Some s] if [s] is the list of evars appearing in
+    its (partial) definition. *)
+val gather_dependent_evars : 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.
diff --git a/printing/printer.ml b/printing/printer.ml
index 0386fc6522..23e6e277fb 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -334,7 +334,7 @@ let default_pr_subgoal n sigma =
 
 let emacs_print_dependent_evars sigma seeds =
   let evars () =
-    let evars = Evarutil.evars_of_evars_in_types_of_list sigma seeds in
+    let evars = Evarutil.gather_dependent_evars sigma seeds in
     let evars =
       Intmap.fold begin fun e i s ->
 	let e' = str (string_of_existential e) in