Merge PR #10489: Fix output for "Printing Dependent Evars Line"

Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: hendriktews
Reviewed-by: herbelin
Ack-by: mattam82

13 files changed, 347 insertions, 44 deletions

diff --git a/doc/changelog/07-commands-and-options/10489-print_dependent_evars.rst b/doc/changelog/07-commands-and-options/10489-print_dependent_evars.rst
new file mode 100644
index 0000000000..580e808baa
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/10489-print_dependent_evars.rst
@@ -0,0 +1,7 @@
+- Update output generated by :flag:`Printing Dependent Evars Line` flag
+  used by the Prooftree tool in Proof General.
+  (`#10489 <https://github.com/coq/coq/pull/10489>`_,
+  closes `#4504 <https://github.com/coq/coq/issues/4504>`_,
+  `#10399 <https://github.com/coq/coq/issues/10399>`_ and
+  `#10400 <https://github.com/coq/coq/issues/10400>`_,
+  by Jim Fehrle).
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 2885d6dc33..843459b723 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1012,8 +1012,9 @@ Controlling display
 
 .. flag:: Printing Dependent Evars Line
 
-   This option controls the printing of the “(dependent evars: …)” line when
-   ``-emacs`` is passed.
+   This option controls the printing of the “(dependent evars: …)” information
+   after each tactic.  The information is used by the Prooftree tool in Proof
+   General. (https://askra.de/software/prooftree)
 
 
 .. _vernac-controlling-the-reduction-strategies:
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index c946125d3f..5444d88e47 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -661,26 +661,26 @@ let clear_hyps2_in_evi env sigma hyps t concl ids =
 (* 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
-let queue_term evm q is_dependent c =
-  queue_set q is_dependent (evars_of_term evm c)
+let queue_term q is_dependent c =
+  queue_set q is_dependent (evar_nodes_of_term c)
 
 let process_dependent_evar q acc evm is_dependent e =
   let evi = Evd.find evm e in
   (* Queues evars appearing in the types of the goal (conclusion, then
      hypotheses), they are all dependent. *)
-  queue_term evm q true evi.evar_concl;
+  queue_term q true evi.evar_concl;
   List.iter begin fun decl ->
     let open NamedDecl in
-    queue_term evm q true (NamedDecl.get_type decl);
+    queue_term q true (NamedDecl.get_type decl);
     match decl with
     | LocalAssum _ -> ()
-    | LocalDef (_,b,_) -> queue_term evm q true b
+    | LocalDef (_,b,_) -> queue_term q true b
   end (EConstr.named_context_of_val evi.evar_hyps);
   match evi.evar_body with
   | Evar_empty ->
       if is_dependent then Evar.Map.add e None acc else acc
   | Evar_defined b ->
-      let subevars = evars_of_term evm b in
+      let subevars = evar_nodes_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
diff --git a/engine/evd.ml b/engine/evd.ml
index 6a721a1a8a..099c83abf1 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1403,7 +1403,16 @@ end
 
 let evars_of_term evd c =
   let rec evrec acc c =
-    match MiniEConstr.kind evd c with
+    let c = MiniEConstr.whd_evar evd c in
+    match kind c with
+    | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l)
+    | _ -> Constr.fold evrec acc c
+  in
+  evrec Evar.Set.empty c
+
+let evar_nodes_of_term c =
+  let rec evrec acc c =
+    match kind c with
     | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l)
     | _ -> Constr.fold evrec acc c
   in
diff --git a/engine/evd.mli b/engine/evd.mli
index 132f7bc745..5ab53947f7 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -509,6 +509,10 @@ val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t option
 val evars_of_term : evar_map -> econstr -> Evar.Set.t
   (** including evars in instances of evars *)
 
+val evar_nodes_of_term : econstr -> Evar.Set.t
+  (** same as evars_of_term but also including defined evars.
+      For use in printing dependent evars *)
+
 val evars_of_named_context : evar_map -> (econstr, etypes) Context.Named.pt -> Evar.Set.t
 
 val evars_of_filtered_evar_info : evar_map -> evar_info -> Evar.Set.t
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 1f076470c1..d6f5aab1d1 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1247,7 +1247,7 @@ module V82 = struct
 
   let top_evars initial { solution=sigma; } =
     let evars_of_initial (c,_) =
-      Evar.Set.elements (Evd.evars_of_term sigma c)
+      Evar.Set.elements (Evd.evar_nodes_of_term c)
     in
     CList.flatten (CList.map evars_of_initial initial)
 
diff --git a/printing/printer.ml b/printing/printer.ml
index 328082fbc2..10a31ac256 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -635,27 +635,34 @@ let () =
       optwrite = (fun v -> should_print_dependent_evars := v) }
 
 let print_dependent_evars gl sigma seeds =
-  let constraints = print_evar_constraints gl sigma in
-  let evars () =
-    if !should_print_dependent_evars then
-      let evars = Evarutil.gather_dependent_evars sigma seeds in
-      let evars =
-	Evar.Map.fold begin fun e i s ->
-	  let e' = pr_internal_existential_key e in
-	  match i with
-	  | None -> s ++ str" " ++ e' ++ str " open,"
-	  | Some i ->
-	    s ++ str " " ++ e' ++ str " using " ++
-	      Evar.Set.fold begin fun d s ->
-		pr_internal_existential_key d ++ str " " ++ s
-	      end i (str ",")
-	end evars (str "")
+  if !should_print_dependent_evars then
+    let mt_pp = mt () in
+    let evars = Evarutil.gather_dependent_evars sigma seeds in
+    let evars_pp = Evar.Map.fold (fun e i s ->
+        let e' = pr_internal_existential_key e in
+        let sep = if s = mt_pp then "" else ", " in
+        s ++ str sep ++ e' ++
+            (match i with
+            | None -> str ":" ++ (Termops.pr_existential_key sigma e)
+            | Some i ->
+              let using = Evar.Set.fold (fun d s ->
+                  s ++ str " " ++ (pr_internal_existential_key d))
+                i mt_pp in
+              str " using" ++ using))
+      evars mt_pp
+    in
+    let evars_current_pp = match gl with
+        | None -> mt_pp
+        | Some gl ->
+           let evars_current = Evarutil.gather_dependent_evars sigma [ gl ] in
+           Evar.Map.fold (fun e _ s ->
+               s ++ str " " ++ (pr_internal_existential_key e))
+             evars_current mt_pp
     in
     cut () ++ cut () ++
-    str "(dependent evars:" ++ evars ++ str ")"
-    else mt ()
-  in
-  constraints ++ evars ()
+      str "(dependent evars: " ++ evars_pp ++
+      str "; in current goal:" ++ evars_current_pp ++ str ")"
+  else mt ()
 
 module GoalMap = Evar.Map
 
@@ -732,6 +739,10 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map
     else 
       pr_rec 1 (g::l)
   in
+  let pr_evar_info gl sigma seeds =
+    let first_goal = if pr_first then gl else None in
+    print_evar_constraints gl sigma ++ print_dependent_evars first_goal sigma seeds
+  in
   (* Side effect! This has to be made more robust *)
   let () =
     match close_cmd with
@@ -742,23 +753,21 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map
   (* Main function *)
   match goals with
   | [] ->
-      begin
-	let exl = Evd.undefined_map sigma in
-	if Evar.Map.is_empty exl then
-	  (str"No more subgoals." ++ print_dependent_evars None sigma seeds)
-	else
-          let pei = pr_evars_int sigma ~shelf ~given_up:[] 1 exl in
-	  v 0 ((str "No more subgoals,"
-                ++ str " but there are non-instantiated existential variables:"
-	        ++ cut () ++ (hov 0 pei)
-                ++ print_dependent_evars None sigma seeds
-                ++ cut () ++ str "You can use Grab Existential Variables."))
-      end
+    let exl = Evd.undefined_map sigma in
+    if Evar.Map.is_empty exl then
+      v 0 (str "No more subgoals." ++ pr_evar_info None sigma seeds)
+    else
+      let pei = pr_evars_int sigma ~shelf ~given_up:[] 1 exl in
+      v 0 ((str "No more subgoals,"
+          ++ str " but there are non-instantiated existential variables:"
+          ++ cut () ++ (hov 0 pei)
+          ++ pr_evar_info None sigma seeds
+          ++ cut () ++ str "You can use Grab Existential Variables."))
   | g1::rest ->
       let goals = print_multiple_goals g1 rest in
       let ngoals = List.length rest+1 in
       v 0 (
-	int ngoals ++ focused_if_needed ++ str(String.plural ngoals "subgoal")
+        int ngoals ++ focused_if_needed ++ str(String.plural ngoals "subgoal")
         ++ print_extra
         ++ str (if (should_gname()) then ", subgoal 1" else "")
         ++ (if should_tag() then pr_goal_tag g1 else str"")
@@ -766,7 +775,7 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map
         ++ (if unfocused=[] then str ""
            else (cut() ++ cut() ++ str "*** Unfocused goals:" ++ cut()
                  ++ pr_rec (List.length rest + 2) unfocused))
-	++ print_dependent_evars (Some g1) sigma seeds
+        ++ pr_evar_info (Some g1) sigma seeds
       )
 
 let pr_open_subgoals_diff ?(quiet=false) ?(diffs=false) ?oproof proof =
diff --git a/printing/printer.mli b/printing/printer.mli
index d62d3789d3..87b09ff755 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -186,6 +186,7 @@ val pr_ne_evar_set         : Pp.t -> Pp.t -> evar_map ->
   Evar.Set.t -> Pp.t
 
 val print_and_diff : Proof.t option -> Proof.t option -> unit
+val print_dependent_evars : Evar.t option -> evar_map -> Evar.t list -> Pp.t
 
 (** Declarations for the "Print Assumption" command *)
 type axiom =
diff --git a/test-suite/output-coqtop/DependentEvars.out b/test-suite/output-coqtop/DependentEvars.out
new file mode 100644
index 0000000000..9ca3fa3357
--- /dev/null
+++ b/test-suite/output-coqtop/DependentEvars.out
@@ -0,0 +1,91 @@
+
+Coq < 
+Coq < Coq < 1 subgoal
+  
+  ============================
+  forall P Q R : Prop, (Q -> R) -> (P -> Q) -> (P -> Q) -> P -> R
+
+(dependent evars: ; in current goal:)
+
+strange_imp_trans < 
+strange_imp_trans < No more subgoals.
+
+(dependent evars: ; in current goal:)
+
+strange_imp_trans < 
+Coq < Coq < 1 subgoal
+  
+  ============================
+  forall P Q : Prop, (P -> Q) /\ P -> Q
+
+(dependent evars: ; in current goal:)
+
+modpon < 
+modpon < No more subgoals.
+
+(dependent evars: ; in current goal:)
+
+modpon < 
+Coq < Coq < 
+Coq < P1 is declared
+P2 is declared
+P3 is declared
+P4 is declared
+
+Coq < p12 is declared
+
+Coq < p123 is declared
+
+Coq < p34 is declared
+
+Coq < Coq < 1 subgoal
+  
+  P1, P2, P3, P4 : Prop
+  p12 : P1 -> P2
+  p123 : (P1 -> P2) -> P3
+  p34 : P3 -> P4
+  ============================
+  P4
+
+(dependent evars: ; in current goal:)
+
+p14 < 
+p14 < 4 focused subgoals
+(shelved: 2)
+  
+  P1, P2, P3, P4 : Prop
+  p12 : P1 -> P2
+  p123 : (P1 -> P2) -> P3
+  p34 : P3 -> P4
+  ============================
+  ?Q -> P4
+
+subgoal 2 is:
+ ?P -> ?Q
+subgoal 3 is:
+ ?P -> ?Q
+subgoal 4 is:
+ ?P
+
+(dependent evars: ?X4:?P, ?X5:?Q; in current goal: ?X5)
+
+p14 < 3 focused subgoals
+(shelved: 2)
+  
+  P1, P2, P3, P4 : Prop
+  p12 : P1 -> P2
+  p123 : (P1 -> P2) -> P3
+  p34 : P3 -> P4
+  ============================
+  ?P -> (?Goal2 -> P4) /\ ?Goal2
+
+subgoal 2 is:
+ ?P -> (?Goal2 -> P4) /\ ?Goal2
+subgoal 3 is:
+ ?P
+
+(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?Goal2; in current goal: ?X4 ?X5 ?X10 ?X11)
+
+p14 < 
+Coq < 
+Coq < 
diff --git a/test-suite/output-coqtop/DependentEvars.v b/test-suite/output-coqtop/DependentEvars.v
new file mode 100644
index 0000000000..5a59054073
--- /dev/null
+++ b/test-suite/output-coqtop/DependentEvars.v
@@ -0,0 +1,24 @@
+Set Printing Dependent Evars Line.
+Lemma strange_imp_trans :
+  forall P Q R : Prop, (Q -> R) -> (P -> Q) -> (P -> Q) -> P -> R.
+Proof.
+  auto.
+Qed.
+
+Lemma modpon : forall P Q : Prop, (P -> Q) /\ P -> Q.
+Proof.
+  tauto.
+Qed.
+
+Section eex.
+  Variables P1 P2 P3 P4 : Prop.
+  Hypothesis p12 : P1 -> P2.
+  Hypothesis p123 : (P1 -> P2) -> P3.
+  Hypothesis p34 : P3 -> P4.
+
+  Lemma p14 : P4.
+  Proof.
+    eapply strange_imp_trans.
+          apply modpon.
+  Abort.
+End eex.
diff --git a/test-suite/output-coqtop/DependentEvars2.out b/test-suite/output-coqtop/DependentEvars2.out
new file mode 100644
index 0000000000..29ebba7c86
--- /dev/null
+++ b/test-suite/output-coqtop/DependentEvars2.out
@@ -0,0 +1,120 @@
+
+Coq < 
+Coq < Coq < 1 subgoal
+  
+  ============================
+  forall P Q R : Prop, (Q -> R) -> (P -> Q) -> (P -> Q) -> P -> R
+
+(dependent evars: ; in current goal:)
+
+strange_imp_trans < 
+strange_imp_trans < No more subgoals.
+
+(dependent evars: ; in current goal:)
+
+strange_imp_trans < 
+Coq < Coq < 1 subgoal
+  
+  ============================
+  forall P Q : Prop, (P -> Q) /\ P -> Q
+
+(dependent evars: ; in current goal:)
+
+modpon < 
+modpon < No more subgoals.
+
+(dependent evars: ; in current goal:)
+
+modpon < 
+Coq < Coq < 
+Coq < P1 is declared
+P2 is declared
+P3 is declared
+P4 is declared
+
+Coq < p12 is declared
+
+Coq < p123 is declared
+
+Coq < p34 is declared
+
+Coq < Coq < 1 subgoal
+  
+  P1, P2, P3, P4 : Prop
+  p12 : P1 -> P2
+  p123 : (P1 -> P2) -> P3
+  p34 : P3 -> P4
+  ============================
+  P4
+
+(dependent evars: ; in current goal:)
+
+p14 < 
+p14 < Second proof:
+
+p14 < 4 focused subgoals
+(shelved: 2)
+  
+  P1, P2, P3, P4 : Prop
+  p12 : P1 -> P2
+  p123 : (P1 -> P2) -> P3
+  p34 : P3 -> P4
+  ============================
+  ?Q -> P4
+
+subgoal 2 is:
+ ?P -> ?Q
+subgoal 3 is:
+ ?P -> ?Q
+subgoal 4 is:
+ ?P
+
+(dependent evars: ?X4:?P, ?X5:?Q; in current goal: ?X5)
+
+p14 < 1 focused subgoal
+(shelved: 2)
+  
+  P1, P2, P3, P4 : Prop
+  p12 : P1 -> P2
+  p123 : (P1 -> P2) -> P3
+  p34 : P3 -> P4
+  ============================
+  ?Q -> P4
+
+(dependent evars: ?X4:?P, ?X5:?Q; in current goal: ?X5)
+
+p14 < This subproof is complete, but there are some unfocused goals.
+Try unfocusing with "}".
+
+3 subgoals
+(shelved: 2)
+
+subgoal 1 is:
+ ?P -> (?Goal2 -> P4) /\ ?Goal2
+subgoal 2 is:
+ ?P -> (?Goal2 -> P4) /\ ?Goal2
+subgoal 3 is:
+ ?P
+
+(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?Goal2; in current goal:)
+
+p14 < 3 focused subgoals
+(shelved: 2)
+  
+  P1, P2, P3, P4 : Prop
+  p12 : P1 -> P2
+  p123 : (P1 -> P2) -> P3
+  p34 : P3 -> P4
+  ============================
+  ?P -> (?Goal2 -> P4) /\ ?Goal2
+
+subgoal 2 is:
+ ?P -> (?Goal2 -> P4) /\ ?Goal2
+subgoal 3 is:
+ ?P
+
+(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?Goal2; in current goal: ?X4 ?X5 ?X10 ?X11)
+
+p14 < 
+Coq < 
+Coq < 
diff --git a/test-suite/output-coqtop/DependentEvars2.v b/test-suite/output-coqtop/DependentEvars2.v
new file mode 100644
index 0000000000..d0f3a4012e
--- /dev/null
+++ b/test-suite/output-coqtop/DependentEvars2.v
@@ -0,0 +1,27 @@
+Set Printing Dependent Evars Line.
+Lemma strange_imp_trans :
+  forall P Q R : Prop, (Q -> R) -> (P -> Q) -> (P -> Q) -> P -> R.
+Proof.
+  auto.
+Qed.
+
+Lemma modpon : forall P Q : Prop, (P -> Q) /\ P -> Q.
+Proof.
+  tauto.
+Qed.
+
+Section eex.
+  Variables P1 P2 P3 P4 : Prop.
+  Hypothesis p12 : P1 -> P2.
+  Hypothesis p123 : (P1 -> P2) -> P3.
+  Hypothesis p34 : P3 -> P4.
+
+  Lemma p14 : P4.
+  Proof.
+    idtac "Second proof:".
+    eapply strange_imp_trans.
+          {
+            apply modpon.
+          }
+  Abort.
+End eex.
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 07466d641e..1f319d2bfd 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -405,7 +405,17 @@ let rec vernac_loop ~state =
 
     | Some (VernacShowGoal {gid; sid}) ->
       let proof = Stm.get_proof ~doc:state.doc (Stateid.of_int sid) in
-      Feedback.msg_notice (Printer.pr_goal_emacs ~proof gid sid);
+      let goal = Printer.pr_goal_emacs ~proof gid sid in
+      let evars =
+        match proof with
+        | None -> mt()
+        | Some p ->
+          let gl = (Evar.unsafe_of_int gid) in
+          let { Proof.sigma } = Proof.data p in
+          try Printer.print_dependent_evars (Some gl) sigma [ gl ]
+          with Not_found -> mt()
+      in
+      Feedback.msg_notice (v 0 (goal ++ evars));
       vernac_loop ~state
 
     | None ->