Skip to content

Commit 04105f0

Browse files
jfehrlejfehrle
committed
Fix rocq-prover#10420 Add dependent evar mapping info to output
1 parent 0074c72 commit 04105f0

File tree

9 files changed

+326
-36
lines changed

9 files changed

+326
-36
lines changed

‎doc/changelog/07-commands-and-options/10489-print_dependent_evars.rst

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
- Update output generated by :flag:`Printing Dependent Evars Line` flag
2+
used by the Prooftree tool in Proof General.
3+
(`#10489 <https://github.com/coq/coq/pull/10489>`_,
4+
closes `#4504 <https://github.com/coq/coq/issues/4504>`_,
5+
`#10399 <https://github.com/coq/coq/issues/10399>`_ and
6+
`#10400 <https://github.com/coq/coq/issues/10400>`_,
7+
by Jim Fehrle).

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

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1012,8 +1012,9 @@ Controlling display
10121012

10131013
.. flag:: Printing Dependent Evars Line
10141014

1015-
This option controls the printing of the “(dependent evars: …)” line when
1016-
``-emacs`` is passed.
1015+
This option controls the printing of the “(dependent evars: …)” information
1016+
after each tactic. The information is used by the Prooftree tool in Proof
1017+
General. (https://askra.de/software/prooftree)
10171018

10181019

10191020
.. _vernac-controlling-the-reduction-strategies:

‎printing/printer.ml

Lines changed: 42 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -635,27 +635,34 @@ let () =
635635
optwrite = (fun v -> should_print_dependent_evars := v) }
636636

637637
let print_dependent_evars gl sigma seeds =
638-
let constraints = print_evar_constraints gl sigma in
639-
let evars () =
640-
if !should_print_dependent_evars then
641-
let evars = Evarutil.gather_dependent_evars sigma seeds in
642-
let evars =
643-
Evar.Map.fold begin fun e i s ->
644-
let e' = pr_internal_existential_key e in
645-
match i with
646-
| None -> s ++ str" " ++ e' ++ str " open,"
647-
| Some i ->
648-
s ++ str " " ++ e' ++ str " using " ++
649-
Evar.Set.fold begin fun d s ->
650-
pr_internal_existential_key d ++ str " " ++ s
651-
end i (str ",")
652-
end evars (str "")
638+
if !should_print_dependent_evars then
639+
let mt_pp = mt () in
640+
let evars = Evarutil.gather_dependent_evars sigma seeds in
641+
let evars_pp = Evar.Map.fold (fun e i s ->
642+
let e' = pr_internal_existential_key e in
643+
let sep = if s = mt_pp then "" else ", " in
644+
s ++ str sep ++ e' ++
645+
(match i with
646+
| None -> str ":" ++ (Termops.pr_existential_key sigma e)
647+
| Some i ->
648+
let using = Evar.Set.fold (fun d s ->
649+
s ++ str " " ++ (pr_internal_existential_key d))
650+
i mt_pp in
651+
str " using" ++ using))
652+
evars mt_pp
653+
in
654+
let evars_current_pp = match gl with
655+
| None -> mt_pp
656+
| Some gl ->
657+
let evars_current = Evarutil.gather_dependent_evars sigma [ gl ] in
658+
Evar.Map.fold (fun e _ s ->
659+
s ++ str " " ++ (pr_internal_existential_key e))
660+
evars_current mt_pp
653661
in
654662
cut () ++ cut () ++
655-
str "(dependent evars:" ++ evars ++ str ")"
656-
else mt ()
657-
in
658-
constraints ++ evars ()
663+
str "(dependent evars: " ++ evars_pp ++
664+
str "; in current goal:" ++ evars_current_pp ++ str ")"
665+
else mt ()
659666

660667
module GoalMap = Evar.Map
661668

@@ -732,6 +739,10 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map
732739
else
733740
pr_rec 1 (g::l)
734741
in
742+
let pr_evar_info gl sigma seeds =
743+
let first_goal = if pr_first then gl else None in
744+
print_evar_constraints gl sigma ++ print_dependent_evars first_goal sigma seeds
745+
in
735746
(* Side effect! This has to be made more robust *)
736747
let () =
737748
match close_cmd with
@@ -742,31 +753,29 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map
742753
(* Main function *)
743754
match goals with
744755
| [] ->
745-
begin
746-
let exl = Evd.undefined_map sigma in
747-
if Evar.Map.is_empty exl then
748-
(str"No more subgoals." ++ print_dependent_evars None sigma seeds)
749-
else
750-
let pei = pr_evars_int sigma ~shelf ~given_up:[] 1 exl in
751-
v 0 ((str "No more subgoals,"
752-
++ str " but there are non-instantiated existential variables:"
753-
++ cut () ++ (hov 0 pei)
754-
++ print_dependent_evars None sigma seeds
755-
++ cut () ++ str "You can use Grab Existential Variables."))
756-
end
756+
let exl = Evd.undefined_map sigma in
757+
if Evar.Map.is_empty exl then
758+
v 0 (str "No more subgoals." ++ pr_evar_info None sigma seeds)
759+
else
760+
let pei = pr_evars_int sigma ~shelf ~given_up:[] 1 exl in
761+
v 0 ((str "No more subgoals,"
762+
++ str " but there are non-instantiated existential variables:"
763+
++ cut () ++ (hov 0 pei)
764+
++ pr_evar_info None sigma seeds
765+
++ cut () ++ str "You can use Grab Existential Variables."))
757766
| g1::rest ->
758767
let goals = print_multiple_goals g1 rest in
759768
let ngoals = List.length rest+1 in
760769
v 0 (
761-
int ngoals ++ focused_if_needed ++ str(String.plural ngoals "subgoal")
770+
int ngoals ++ focused_if_needed ++ str(String.plural ngoals "subgoal")
762771
++ print_extra
763772
++ str (if (should_gname()) then ", subgoal 1" else "")
764773
++ (if should_tag() then pr_goal_tag g1 else str"")
765774
++ pr_goal_name sigma g1 ++ cut () ++ goals
766775
++ (if unfocused=[] then str ""
767776
else (cut() ++ cut() ++ str "*** Unfocused goals:" ++ cut()
768777
++ pr_rec (List.length rest + 2) unfocused))
769-
++ print_dependent_evars (Some g1) sigma seeds
778+
++ pr_evar_info (Some g1) sigma seeds
770779
)
771780

772781
let pr_open_subgoals_diff ?(quiet=false) ?(diffs=false) ?oproof proof =

‎printing/printer.mli

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -186,6 +186,7 @@ val pr_ne_evar_set : Pp.t -> Pp.t -> evar_map ->
186186
Evar.Set.t -> Pp.t
187187

188188
val print_and_diff : Proof.t option -> Proof.t option -> unit
189+
val print_dependent_evars : Evar.t option -> evar_map -> Evar.t list -> Pp.t
189190

190191
(** Declarations for the "Print Assumption" command *)
191192
type axiom =

‎test-suite/output-coqtop/DependentEvars.out

Lines changed: 91 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,91 @@
1+
2+
Coq <
3+
Coq < Coq < 1 subgoal
4+
5+
============================
6+
forall P Q R : Prop, (Q -> R) -> (P -> Q) -> (P -> Q) -> P -> R
7+
8+
(dependent evars: ; in current goal:)
9+
10+
strange_imp_trans <
11+
strange_imp_trans < No more subgoals.
12+
13+
(dependent evars: ; in current goal:)
14+
15+
strange_imp_trans <
16+
Coq < Coq < 1 subgoal
17+
18+
============================
19+
forall P Q : Prop, (P -> Q) /\ P -> Q
20+
21+
(dependent evars: ; in current goal:)
22+
23+
modpon <
24+
modpon < No more subgoals.
25+
26+
(dependent evars: ; in current goal:)
27+
28+
modpon <
29+
Coq < Coq <
30+
Coq < P1 is declared
31+
P2 is declared
32+
P3 is declared
33+
P4 is declared
34+
35+
Coq < p12 is declared
36+
37+
Coq < p123 is declared
38+
39+
Coq < p34 is declared
40+
41+
Coq < Coq < 1 subgoal
42+
43+
P1, P2, P3, P4 : Prop
44+
p12 : P1 -> P2
45+
p123 : (P1 -> P2) -> P3
46+
p34 : P3 -> P4
47+
============================
48+
P4
49+
50+
(dependent evars: ; in current goal:)
51+
52+
p14 <
53+
p14 < 4 focused subgoals
54+
(shelved: 2)
55+
56+
P1, P2, P3, P4 : Prop
57+
p12 : P1 -> P2
58+
p123 : (P1 -> P2) -> P3
59+
p34 : P3 -> P4
60+
============================
61+
?Q -> P4
62+
63+
subgoal 2 is:
64+
?P -> ?Q
65+
subgoal 3 is:
66+
?P -> ?Q
67+
subgoal 4 is:
68+
?P
69+
70+
(dependent evars: ?X4:?P, ?X5:?Q; in current goal: ?X5)
71+
72+
p14 < 3 focused subgoals
73+
(shelved: 2)
74+
75+
P1, P2, P3, P4 : Prop
76+
p12 : P1 -> P2
77+
p123 : (P1 -> P2) -> P3
78+
p34 : P3 -> P4
79+
============================
80+
?P -> (?Goal2 -> P4) /\ ?Goal2
81+
82+
subgoal 2 is:
83+
?P -> (?Goal2 -> P4) /\ ?Goal2
84+
subgoal 3 is:
85+
?P
86+
87+
(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?Goal2; in current goal: ?X4 ?X5 ?X10 ?X11)
88+
89+
p14 <
90+
Coq <
91+
Coq <

‎test-suite/output-coqtop/DependentEvars.v

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
Set Printing Dependent Evars Line.
2+
Lemma strange_imp_trans :
3+
forall P Q R : Prop, (Q -> R) -> (P -> Q) -> (P -> Q) -> P -> R.
4+
Proof.
5+
auto.
6+
Qed.
7+
8+
Lemma modpon : forall P Q : Prop, (P -> Q) /\ P -> Q.
9+
Proof.
10+
tauto.
11+
Qed.
12+
13+
Section eex.
14+
Variables P1 P2 P3 P4 : Prop.
15+
Hypothesis p12 : P1 -> P2.
16+
Hypothesis p123 : (P1 -> P2) -> P3.
17+
Hypothesis p34 : P3 -> P4.
18+
19+
Lemma p14 : P4.
20+
Proof.
21+
eapply strange_imp_trans.
22+
apply modpon.
23+
Abort.
24+
End eex.

‎test-suite/output-coqtop/DependentEvars2.out

Lines changed: 120 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,120 @@
1+
2+
Coq <
3+
Coq < Coq < 1 subgoal
4+
5+
============================
6+
forall P Q R : Prop, (Q -> R) -> (P -> Q) -> (P -> Q) -> P -> R
7+
8+
(dependent evars: ; in current goal:)
9+
10+
strange_imp_trans <
11+
strange_imp_trans < No more subgoals.
12+
13+
(dependent evars: ; in current goal:)
14+
15+
strange_imp_trans <
16+
Coq < Coq < 1 subgoal
17+
18+
============================
19+
forall P Q : Prop, (P -> Q) /\ P -> Q
20+
21+
(dependent evars: ; in current goal:)
22+
23+
modpon <
24+
modpon < No more subgoals.
25+
26+
(dependent evars: ; in current goal:)
27+
28+
modpon <
29+
Coq < Coq <
30+
Coq < P1 is declared
31+
P2 is declared
32+
P3 is declared
33+
P4 is declared
34+
35+
Coq < p12 is declared
36+
37+
Coq < p123 is declared
38+
39+
Coq < p34 is declared
40+
41+
Coq < Coq < 1 subgoal
42+
43+
P1, P2, P3, P4 : Prop
44+
p12 : P1 -> P2
45+
p123 : (P1 -> P2) -> P3
46+
p34 : P3 -> P4
47+
============================
48+
P4
49+
50+
(dependent evars: ; in current goal:)
51+
52+
p14 <
53+
p14 < Second proof:
54+
55+
p14 < 4 focused subgoals
56+
(shelved: 2)
57+
58+
P1, P2, P3, P4 : Prop
59+
p12 : P1 -> P2
60+
p123 : (P1 -> P2) -> P3
61+
p34 : P3 -> P4
62+
============================
63+
?Q -> P4
64+
65+
subgoal 2 is:
66+
?P -> ?Q
67+
subgoal 3 is:
68+
?P -> ?Q
69+
subgoal 4 is:
70+
?P
71+
72+
(dependent evars: ?X4:?P, ?X5:?Q; in current goal: ?X5)
73+
74+
p14 < 1 focused subgoal
75+
(shelved: 2)
76+
77+
P1, P2, P3, P4 : Prop
78+
p12 : P1 -> P2
79+
p123 : (P1 -> P2) -> P3
80+
p34 : P3 -> P4
81+
============================
82+
?Q -> P4
83+
84+
(dependent evars: ?X4:?P, ?X5:?Q; in current goal: ?X5)
85+
86+
p14 < This subproof is complete, but there are some unfocused goals.
87+
Try unfocusing with "}".
88+
89+
3 subgoals
90+
(shelved: 2)
91+
92+
subgoal 1 is:
93+
?P -> (?Goal2 -> P4) /\ ?Goal2
94+
subgoal 2 is:
95+
?P -> (?Goal2 -> P4) /\ ?Goal2
96+
subgoal 3 is:
97+
?P
98+
99+
(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?Goal2; in current goal:)
100+
101+
p14 < 3 focused subgoals
102+
(shelved: 2)
103+
104+
P1, P2, P3, P4 : Prop
105+
p12 : P1 -> P2
106+
p123 : (P1 -> P2) -> P3
107+
p34 : P3 -> P4
108+
============================
109+
?P -> (?Goal2 -> P4) /\ ?Goal2
110+
111+
subgoal 2 is:
112+
?P -> (?Goal2 -> P4) /\ ?Goal2
113+
subgoal 3 is:
114+
?P
115+
116+
(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?Goal2; in current goal: ?X4 ?X5 ?X10 ?X11)
117+
118+
p14 <
119+
Coq <
120+
Coq <

0 commit comments

Comments
 (0)