In emacs mode, prints a list of the dependent existential variables introduced

during the proof together with information whether they were (partially)
instantiated and if it's the case the list of existential variables that were
used to that effect.

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

6 files changed, 55 insertions, 11 deletions

diff --git a/parsing/printer.ml b/parsing/printer.ml
index 8727f10228..1c357076c9 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -29,6 +29,8 @@ open Store.Field
 
 let emacs_str s =
   if !Flags.print_emacs then s else ""
+let delayed_emacs_cmd s =
+  if !Flags.print_emacs then s () else str ""
 
 (**********************************************************************)
 (** Terms                                                             *)
@@ -323,8 +325,28 @@ let default_pr_subgoal n sigma =
   in
   prrec n
 
+let emacs_print_dependent_evars sigma seeds =
+  let evars () =
+    let evars = Evarutil.evars_of_evars_in_types_of_list sigma seeds in
+    let evars =
+      Intmap.fold begin fun e i s ->
+	let e' = str (string_of_existential e) in
+	match i with
+	| None -> s ++ e' ++ str " open,"
+	| Some i ->
+	  s ++ e' ++ str " using " ++
+	    Intset.fold begin fun d s ->
+	      str (string_of_existential d) ++ str " " ++ s
+	    end i (str "")
+      end evars (str "")
+    in
+    str "(dependent evars: " ++ evars ++ str ")" ++ fnl ()
+  in
+  delayed_emacs_cmd evars
+
 (* Print open subgoals. Checks for uninstantiated existential variables *)
-let default_pr_subgoals close_cmd sigma = function
+(* spiwack: [seeds] is for printing dependent evars in emacs mode. *)
+let default_pr_subgoals close_cmd sigma seeds = function
   | [] ->
       begin
 	match close_cmd with
@@ -342,7 +364,10 @@ let default_pr_subgoals close_cmd sigma = function
       end
   | [g] ->
       let pg = default_pr_goal { it = g ; sigma = sigma } in
-      v 0 (str ("1 "^"subgoal") ++ pr_goal_tag g ++ cut () ++ pg)
+      v 0 (
+	emacs_print_dependent_evars sigma seeds ++
+	str ("1 "^"subgoal") ++ pr_goal_tag g ++ cut () ++ pg
+      )
   | g1::rest ->
       let rec pr_rec n = function
         | [] -> (mt ())
@@ -353,16 +378,19 @@ let default_pr_subgoals close_cmd sigma = function
       in
       let pg1 = default_pr_goal { it = g1 ; sigma = sigma } in
       let prest = pr_rec 2 rest in
-      v 0 (int(List.length rest+1) ++ str" subgoals" ++
-             str (emacs_str ", subgoal 1") ++ pr_goal_tag g1 ++ cut ()
-	   ++ pg1 ++ prest ++ fnl ())
+      v 0 (
+	emacs_print_dependent_evars sigma seeds ++
+	int(List.length rest+1) ++ str" subgoals" ++
+          str (emacs_str ", subgoal 1") ++ pr_goal_tag g1 ++ cut ()
+	++ pg1 ++ prest ++ fnl ()
+      )
 
 (**********************************************************************)
 (* Abstraction layer                                                  *)
 
 
 type printer_pr = {
- pr_subgoals            : string option -> evar_map -> goal list -> std_ppcmds;
+ pr_subgoals            : string option -> evar_map -> evar list -> goal list -> std_ppcmds;
  pr_subgoal             : int -> evar_map -> goal list -> std_ppcmds;
  pr_goal                : goal sigma -> std_ppcmds;
 }
@@ -387,11 +415,12 @@ let pr_goal     x = !printer_pr.pr_goal     x
 let pr_open_subgoals () =
   let p = Proof_global.give_me_the_proof () in
   let { Evd.it = goals ; sigma = sigma } = Proof.V82.subgoals p in
+  let seeds = Proof.V82.top_evars p in
   begin match goals with
   | [] -> let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in
             begin match bgoals with
-	    | [] -> pr_subgoals None sigma goals
-	    | _ -> pr_subgoals None bsigma bgoals ++ fnl () ++ fnl () ++
+	    | [] -> pr_subgoals None sigma seeds goals
+	    | _ -> pr_subgoals None bsigma seeds bgoals ++ fnl () ++ fnl () ++
 		      str"This subproof is complete, but there are still unfocused goals:"
 		(* spiwack: to stay compatible with the proof general and coqide,
 		    I use print the message after the goal. It would be better to have
@@ -401,7 +430,7 @@ let pr_open_subgoals () =
 		    instead. But it doesn't quite work.
 		*)
 	    end
-  | _ -> pr_subgoals None sigma goals
+  | _ -> pr_subgoals None sigma seeds goals
   end
 
 let pr_nth_open_subgoal n =
diff --git a/parsing/printer.mli b/parsing/printer.mli
index ff6d818072..2d437c2013 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -104,7 +104,7 @@ val pr_transparent_state   : transparent_state -> std_ppcmds
 (** Proofs *)
 
 val pr_goal                : goal sigma -> std_ppcmds
-val pr_subgoals            : string option -> evar_map -> goal list -> std_ppcmds
+val pr_subgoals            : string option -> evar_map -> evar list -> goal list -> std_ppcmds
 val pr_subgoal             : int -> evar_map -> goal list -> std_ppcmds
 val pr_concl               : int -> evar_map -> goal -> std_ppcmds
 
@@ -141,7 +141,7 @@ val pr_assumptionset :
 val pr_goal_by_id : string -> std_ppcmds
 
 type printer_pr = {
- pr_subgoals            : string option -> evar_map -> goal list -> std_ppcmds;
+ pr_subgoals            : string option -> evar_map -> evar list -> goal list -> std_ppcmds;
  pr_subgoal             : int -> evar_map -> goal list -> std_ppcmds;
  pr_goal                : goal sigma -> std_ppcmds;
 };;
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 8283657983..2aa31cd253 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -435,6 +435,9 @@ module V82 = struct
     in
     { Evd.it=List.hd gls ; sigma=sigma }
 
+  let top_evars p =
+    Proofview.V82.top_evars p.state.proofview
+
   let instantiate_evar n com pr =
     let starting_point = save_state pr in
     let sp = pr.state.proofview in
diff --git a/proofs/proof.mli b/proofs/proof.mli
index b4c84cbf60..d80ac79af2 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -171,6 +171,9 @@ module V82 : sig
   val depth : proof -> int 
 
   val top_goal : proof -> Goal.goal Evd.sigma
+  
+  (* returns the existential variable used to start the proof *)
+  val top_evars : proof -> Evd.evar list
 
   (* Implements the Existential command *)
   val instantiate_evar : int -> Topconstr.constr_expr -> proof -> unit
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index b76c802dfd..0d50d521f3 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -484,6 +484,12 @@ module V82 = struct
     let goals = List.map (fun (t,_) -> Goal.V82.build (fst (Term.destEvar t))) initial in
     { Evd.it = goals ; sigma=solution }
 
+  let top_evars { initial=initial } =
+    let evars_of_initial (c,_) =
+      Util.Intset.elements (Evarutil.evars_of_term c)
+    in
+    List.flatten (List.map evars_of_initial initial)
+
   let instantiate_evar n com pv =
     let (evk,_) = 
       let evl = Evarutil.non_instantiated pv.solution in
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 25a58a482a..24da9d77b3 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -200,6 +200,9 @@ module V82 : sig
   val goals : proofview -> Goal.goal list Evd.sigma
 
   val top_goals : proofview -> Goal.goal list Evd.sigma
+  
+  (* returns the existential variable used to start the proof *)
+  val top_evars : proofview -> Evd.evar list
     
   (* Implements the Existential command *)
   val instantiate_evar : int -> Topconstr.constr_expr -> proofview -> proofview