1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* $Id: tactic_printer.ml 11313 2008-08-07 11:15:03Z barras $ *)
22
let pr_tactic = function
23
| TacArg (Tacexp t) ->
24
(*top tactic from tacinterp*)
25
Pptactic.pr_glob_tactic (Global.env()) t
27
Pptactic.pr_tactic (Global.env()) t
29
let pr_proof_instr instr =
30
Ppdecl_proof.pr_proof_instr (Global.env()) instr
32
let pr_rule = function
33
| Prim r -> hov 0 (pr_prim_rule r)
37
| Tactic (texp,_) -> hov 0 (pr_tactic texp)
38
| Proof_instr (_,instr) -> hov 0 (pr_proof_instr instr)
40
| Daimon -> str "<Daimon>"
41
| Decl_proof _ -> str "proof"
43
let uses_default_tac = function
44
| Nested(Tactic(_,dflt),_) -> dflt
47
(* Does not print change of evars *)
48
let pr_rule_dot = function
49
| Prim Change_evars ->str "PC: ch_evars" ++ mt ()
50
(* PC: this might be redundant *)
52
pr_rule r ++ if uses_default_tac r then str "..." else str"."
54
let pr_rule_dot_fnl = function
55
| Nested (Tactic (TacAtom (_,(TacMutualFix (true,_,_,_)
56
| TacMutualCofix (true,_,_))),_),_) ->
57
(* Very big hack to not display hidden tactics in "Theorem with" *)
58
(* (would not scale!) *)
60
| Prim Change_evars -> mt ()
61
| r -> pr_rule_dot r ++ fnl ()
65
(* We remove from the var context of env what is already in osign *)
66
let thin_sign osign sign =
67
Sign.fold_named_context
68
(fun (id,c,ty as d) sign ->
70
if Sign.lookup_named id osign = (id,c,ty) then sign
72
with Not_found | Different -> Environ.push_named_context_val d sign)
73
sign ~init:Environ.empty_named_context_val
75
let rec print_proof sigma osign pf =
76
let hyps = Environ.named_context_of_val pf.goal.evar_hyps in
77
let hyps' = thin_sign osign hyps in
80
hov 0 (pr_goal {pf.goal with evar_hyps=hyps'})
83
(hov 0 (pr_goal {pf.goal with evar_hyps=hyps'}) ++
84
spc () ++ str" BY " ++
85
hov 0 (pr_rule r) ++ fnl () ++
87
hov 0 (prlist_with_sep pr_fnl (print_proof sigma hyps) spfl))
91
pr_lconstr_env (Global.env_of_context gl.evar_hyps) gl.evar_concl ++ str"."
93
let print_decl_script tac_printer ?(nochange=true) sigma pf =
94
let rec print_prf pf =
98
(str"<Your Proof Text here>")
102
| Some (Daimon,[]) -> str "(* Some proof has been skipped here *)"
103
| Some (Prim Change_evars,[subpf]) -> print_prf subpf
104
| Some (Nested(Proof_instr (opened,instr),_) as rule,subprfs) ->
106
match instr.instr,subprfs with
107
Pescape,[{ref=Some(_,subsubprfs)}] ->
109
(pr_rule_dot_fnl rule ++
110
prlist_with_sep pr_fnl tac_printer subsubprfs) ++ fnl () ++
111
if opened then mt () else str "return."
112
| Pclaim _,[body;cont] ->
113
hov 2 (pr_rule_dot_fnl rule ++ print_prf body) ++ fnl () ++
114
(if opened then mt () else str "end claim." ++ fnl ()) ++
116
| Pfocus _,[body;cont] ->
117
hov 2 (pr_rule_dot_fnl rule ++ print_prf body) ++
119
(if opened then mt () else str "end focus." ++ fnl ()) ++
121
| (Psuppose _ |Pcase (_,_,_)),[body;cont] ->
122
hov 2 (pr_rule_dot_fnl rule ++ print_prf body) ++ fnl () ++
125
pr_rule_dot_fnl rule ++ print_prf next
128
| _,_ -> anomaly "unknown branching instruction"
130
| _ -> anomaly "Not Applicable" in
133
let print_script ?(nochange=true) sigma pf =
134
let rec print_prf pf =
138
(str"<Your Tactic Text here>")
142
| Some(Decl_proof opened,script) ->
143
assert (List.length script = 1);
145
if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())
148
hov 0 (str "proof." ++ fnl () ++
149
print_decl_script print_prf
150
~nochange sigma (List.hd script))
153
if opened then mt () else (str "end proof." ++ fnl ())
155
| Some(Daimon,spfl) ->
156
((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++
157
prlist_with_sep pr_fnl print_prf spfl )
159
((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++
160
pr_rule_dot_fnl rule ++
161
prlist_with_sep pr_fnl print_prf spfl ) in
164
(* printed by Show Script command *)
166
let print_treescript ?(nochange=true) sigma pf =
167
let rec print_prf pf =
171
if pf.goal.evar_extra=None then str"<Your Tactic Text here>"
172
else str"<Your Proof Text here>"
173
else pr_change pf.goal
174
| Some(Decl_proof opened,script) ->
175
assert (List.length script = 1);
177
if nochange then mt () else pr_change pf.goal ++ fnl ()
180
begin str "proof." ++ fnl () ++
181
print_decl_script print_prf ~nochange sigma (List.hd script)
184
if opened then mt () else (str "end proof." ++ fnl ())
186
| Some(Daimon,spfl) ->
187
(if nochange then mt () else pr_change pf.goal ++ fnl ()) ++
188
prlist_with_sep pr_fnl (print_script ~nochange sigma) spfl
190
let indent = if List.length spfl >= 2 then 1 else 0 in
191
(if nochange then mt () else pr_change pf.goal ++ fnl ()) ++
192
hv indent (pr_rule_dot_fnl r ++ prlist_with_sep fnl print_prf spfl)
193
in hov 0 (print_prf pf)
195
let rec print_info_script sigma osign pf =
196
let {evar_hyps=sign; evar_concl=cl} = pf.goal in
203
if pf1.ref = None then
206
(str";" ++ brk(1,3) ++
207
print_info_script sigma
208
(Environ.named_context_of_val sign) pf1)
209
| _ -> (str"." ++ fnl () ++
210
prlist_with_sep pr_fnl
211
(print_info_script sigma
212
(Environ.named_context_of_val sign)) spfl))
214
let format_print_info_script sigma osign pf =
215
hov 0 (print_info_script sigma osign pf)
217
let print_subscript sigma sign pf =
218
if is_tactic_proof pf then
219
format_print_info_script sigma sign (subproof_of_proof pf)
221
format_print_info_script sigma sign pf
223
let _ = Refiner.set_info_printer print_subscript