added current goal info to dependent evars line

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).

doc/sphinx/proof-engine/vernacular-commands.rst

@@ -1031,8 +1031,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:

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

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

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 undefined 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

engine/proofview.ml

@@ -1245,7 +1245,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)
 

printing/printer.ml

@@ -635,27 +635,33 @@ 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 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
+        s ++ e' ++
+            (match i with
+            | None -> (str " : ") ++ (Termops.pr_existential_key sigma e) ++ (str " open")
+            | Some i ->
+              let using = Evar.Set.fold (fun d s ->
+                  s ++ str " " ++ (pr_internal_existential_key d))
+                i (str "") in
+              str " using" ++ using)
+          ++ str ", ")
+      evars (str "")
+    in
+    let evars_current_pp = match gl with
+        | None -> str "no current goal"
+        | Some gl ->
+           let evars_current = Evarutil.gather_dependent_evars sigma [ gl ] in
+           Evar.Map.fold (fun e _ s ->
+               s ++ (pr_internal_existential_key e) ++ (str " "))
+             evars_current (str "current goal: ")
     in
     cut () ++ cut () ++
-    str "(dependent evars:" ++ evars ++ str ")"
-    else mt ()
-  in
-  constraints ++ evars ()
+    str "(dependent evars: " ++ evars_pp ++ str "; " ++
+    evars_current_pp ++ str ")"
+  else mt ()
 
 module GoalMap = Evar.Map
 
@@ -732,6 +738,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,31 +752,29 @@ 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"")
         ++ pr_goal_name sigma g1 ++ cut () ++ goals
         ++ (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 =

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 =

test-suite/output-coqtop/DependentEvars.out

@@ -0,0 +1,94 @@
+
+Coq < 
+Coq < Coq < 1 subgoal
+
+  ============================
+  forall P Q R : Prop, (Q -> R) -> (P -> Q) -> (P -> Q) -> P -> R
+
+(dependent evars: ;
+mapping: ?X1 : ?Goal)
+
+strange_imp_trans < 
+strange_imp_trans < No more subgoals.(dependent evars: ;mapping: )
+
+strange_imp_trans < strange_imp_trans is defined
+
+Coq < Coq < 1 subgoal
+
+  ============================
+  forall P Q : Prop, (P -> Q) /\ P -> Q
+
+(dependent evars: ;
+mapping: ?X2 : ?Goal)
+
+modpon < 
+modpon < No more subgoals.(dependent evars: ;mapping: )
+
+modpon < modpon is defined
+
+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: ;
+mapping: ?X3 : ?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 open, ?X5 open;
+mapping: ?X4 : ?P, ?X5 : ?Q, ?X6 : ?Goal, ?X7 : ?Goal0, ?X8 : ?Goal1, ?X9 : ?Goal2)
+
+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 open, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11 open;
+mapping: ?X4 : ?P, ?X7 : ?Goal, ?X8 : ?Goal0, ?X9 : ?Goal1, ?X11 : ?Goal2)
+
+p14 < 
+Coq < 
+Coq < 

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.

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 ->