1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* $Id: tactic_printer.ml 9593 2007-02-05 13:58:52Z corbinea $ *)
open Pp
open Util
open Sign
open Evd
open Tacexpr
open Proof_type
open Proof_trees
open Decl_expr
open Logic
open Printer
let pr_tactic = function
| TacArg (Tacexp t) ->
(*top tactic from tacinterp*)
Pptactic.pr_glob_tactic (Global.env()) t
| t ->
Pptactic.pr_tactic (Global.env()) t
let pr_proof_instr instr =
Ppdecl_proof.pr_proof_instr (Global.env()) instr
let pr_rule = function
| Prim r -> hov 0 (pr_prim_rule r)
| Nested(cmpd,_) ->
begin
match cmpd with
Tactic (texp,_) -> hov 0 (pr_tactic texp)
| Proof_instr (_,instr) -> hov 0 (pr_proof_instr instr)
end
| Daimon -> str "<Daimon>"
| Decl_proof _ -> str "proof"
let uses_default_tac = function
| Nested(Tactic(_,dflt),_) -> dflt
| _ -> false
(* Does not print change of evars *)
let pr_rule_dot = function
| Prim Change_evars -> mt ()
| r ->
pr_rule r ++ if uses_default_tac r then str "..." else str"."
exception Different
(* We remove from the var context of env what is already in osign *)
let thin_sign osign sign =
Sign.fold_named_context
(fun (id,c,ty as d) sign ->
try
if Sign.lookup_named id osign = (id,c,ty) then sign
else raise Different
with Not_found | Different -> Environ.push_named_context_val d sign)
sign ~init:Environ.empty_named_context_val
let rec print_proof sigma osign pf =
let hyps = Environ.named_context_of_val pf.goal.evar_hyps in
let hyps' = thin_sign osign hyps in
match pf.ref with
| None ->
hov 0 (pr_goal {pf.goal with evar_hyps=hyps'})
| Some(r,spfl) ->
hov 0
(hov 0 (pr_goal {pf.goal with evar_hyps=hyps'}) ++
spc () ++ str" BY " ++
hov 0 (pr_rule r) ++ fnl () ++
str" " ++
hov 0 (prlist_with_sep pr_fnl (print_proof sigma hyps) spfl))
let pr_change gl =
str"change " ++
pr_lconstr_env (Global.env_of_context gl.evar_hyps) gl.evar_concl ++ str"."
let rec print_decl_script tac_printer nochange sigma pf =
match pf.ref with
| None ->
(if nochange then
(str"<Your Proof Text here>")
else
pr_change pf.goal)
++ fnl ()
| Some (Daimon,[]) -> mt ()
| Some (Prim Change_evars,[next]) ->
(* ignore evar changes *)
print_decl_script tac_printer nochange sigma next
| Some (Nested(Proof_instr (opened,instr),_) as rule,subprfs) ->
begin
match instr.instr,subprfs with
Pescape,[{ref=Some(_,subsubprfs)}] ->
hov 7
(pr_rule_dot rule ++ fnl () ++
prlist_with_sep pr_fnl tac_printer subsubprfs) ++ fnl () ++
if opened then mt () else str "return."
| Pclaim _,[body;cont] ->
hov 2
(pr_rule_dot rule ++ fnl () ++
print_decl_script tac_printer nochange sigma body) ++
fnl () ++
if opened then mt () else str "end claim." ++ fnl () ++
print_decl_script tac_printer nochange sigma cont
| Pfocus _,[body;cont] ->
hov 2
(pr_rule_dot rule ++ fnl () ++
print_decl_script tac_printer nochange sigma body) ++
fnl () ++
if opened then mt () else str "end focus." ++ fnl () ++
print_decl_script tac_printer nochange sigma cont
| (Psuppose _ |Pcase (_,_,_)),[body;cont] ->
hov 2
(pr_rule_dot rule ++ fnl () ++
print_decl_script tac_printer nochange sigma body) ++
fnl () ++
print_decl_script tac_printer nochange sigma cont
| _,[next] ->
pr_rule_dot rule ++ fnl () ++
print_decl_script tac_printer nochange sigma next
| _,[] ->
pr_rule_dot rule
| _,_ -> anomaly "unknown branching instruction"
end
| _ -> anomaly "Not Applicable"
let rec print_script nochange sigma pf =
match pf.ref with
| None ->
(if nochange then
(str"<Your Tactic Text here>")
else
pr_change pf.goal)
++ fnl ()
| Some(Decl_proof opened,script) ->
assert (List.length script = 1);
begin
if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())
end ++
begin
hov 0 (str "proof." ++ fnl () ++
print_decl_script (print_script nochange sigma)
nochange sigma (List.hd script))
end ++ fnl () ++
begin
if opened then mt () else (str "end proof." ++ fnl ())
end
| Some(Daimon,spfl) ->
((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++
prlist_with_sep pr_fnl
(print_script nochange sigma) spfl )
| Some(rule,spfl) ->
((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++
pr_rule_dot rule ++ fnl () ++
prlist_with_sep pr_fnl
(print_script nochange sigma) spfl )
(* printed by Show Script command *)
let print_treescript nochange sigma pf =
let rec aux top pf =
match pf.ref with
| None ->
if nochange then
if pf.goal.evar_extra=None then
(str"<Your Tactic Text here>")
else (str"<Your Proof Text here>")
else
(pr_change pf.goal)
| Some(Decl_proof opened,script) ->
assert (List.length script = 1);
begin
if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())
end ++
hov 0
begin str "proof." ++ fnl () ++
print_decl_script (aux false)
nochange sigma (List.hd script)
end ++ fnl () ++
begin
if opened then mt () else (str "end proof." ++ fnl ())
end
| Some(Daimon,spfl) ->
((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++
prlist_with_sep pr_fnl
(print_script nochange sigma) spfl )
| Some(r,spfl) ->
(if nochange then mt () else (pr_change pf.goal ++ fnl ())) ++
pr_rule_dot r ++
begin
if List.length spfl > 1 then
fnl () ++
str " " ++ hov 0 (aux false (List.hd spfl)) ++ fnl () ++
hov 0 (prlist_with_sep fnl (aux false) (List.tl spfl))
else
match spfl with
| [] -> mt ()
| [spf] -> fnl () ++
(if top then mt () else str " ") ++ aux top spf
| _ -> fnl () ++ str " " ++
hov 0 (prlist_with_sep fnl (aux false) spfl)
end
in hov 0 (aux true pf)
let rec print_info_script sigma osign pf =
let {evar_hyps=sign; evar_concl=cl} = pf.goal in
match pf.ref with
| None -> (mt ())
| Some(r,spfl) ->
(pr_rule r ++
match spfl with
| [pf1] ->
if pf1.ref = None then
(str "." ++ fnl ())
else
(str";" ++ brk(1,3) ++
print_info_script sigma
(Environ.named_context_of_val sign) pf1)
| _ -> (str"." ++ fnl () ++
prlist_with_sep pr_fnl
(print_info_script sigma
(Environ.named_context_of_val sign)) spfl))
let format_print_info_script sigma osign pf =
hov 0 (print_info_script sigma osign pf)
let print_subscript sigma sign pf =
if is_tactic_proof pf then
format_print_info_script sigma sign (subproof_of_proof pf)
else
format_print_info_script sigma sign pf
let _ = Refiner.set_info_printer print_subscript
|
