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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Pp
open Util
open Sign
open Evd
open Tacexpr
open Proof_type
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_rule = function
| Prim r -> hov 0 (pr_prim_rule r)
| Nested(cmpd,_) ->
begin
match cmpd with
| Tactic (texp,_) -> hov 0 (pr_tactic texp)
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 ->str "PC: ch_evars" ++ mt ()
(* PC: this might be redundant *)
| r ->
pr_rule r ++ if uses_default_tac r then str "..." else str"."
let pr_rule_dot_fnl = function
| Nested (Tactic (TacAtom (_,(TacMutualFix (true,_,_,_)
| TacMutualCofix (true,_,_))),_),_) ->
(* Very big hack to not display hidden tactics in "Theorem with" *)
(* (would not scale!) *)
mt ()
| Prim Change_evars -> mt ()
| r -> pr_rule_dot r ++ fnl ()
exception Different
let rec print_proof sigma osign pf =
(* spiwack: [osign] is currently ignored, not sure if this function is even used. *)
let hyps = Environ.named_context_of_val (Goal.V82.hyps sigma pf.goal) in
match pf.ref with
| None ->
hov 0 (pr_goal {sigma = sigma; it=pf.goal })
| Some(r,spfl) ->
hov 0
(hov 0 (pr_goal {sigma = sigma; it=pf.goal }) ++
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 sigma gl =
str"change " ++
pr_lconstr_env (Goal.V82.env sigma gl) (Goal.V82.concl sigma gl) ++ str"."
let print_decl_script tac_printer ?(nochange=true) sigma pf =
let rec print_prf pf =
match pf.ref with
| None ->
(if nochange then
(str"<Your Proof Text here>")
else
pr_change sigma pf.goal)
++ fnl ()
| Some (Daimon,[]) -> str "(* Some proof has been skipped here *)"
| Some (Prim Change_evars,[subpf]) -> print_prf subpf
| _ -> anomaly "Not Applicable" in
print_prf pf
let print_script ?(nochange=true) sigma pf =
let rec print_prf pf =
match pf.ref with
| None ->
(if nochange then
(str"<Your Tactic Text here>")
else
pr_change sigma pf.goal)
++ fnl ()
| Some(Decl_proof opened,script) ->
assert (List.length script = 1);
begin
if nochange then (mt ()) else (pr_change sigma pf.goal ++ fnl ())
end ++
begin
hov 0 (str "proof." ++ fnl () ++
print_decl_script print_prf
~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 sigma pf.goal ++ fnl ())) ++
prlist_with_sep pr_fnl print_prf spfl )
| Some(rule,spfl) ->
((if nochange then (mt ()) else (pr_change sigma pf.goal ++ fnl ())) ++
pr_rule_dot_fnl rule ++
prlist_with_sep pr_fnl print_prf spfl ) in
print_prf pf
(* printed by Show Script command *)
let print_treescript ?(nochange=true) sigma pf =
let rec print_prf pf =
match pf.ref with
| None ->
if nochange then
str"<Your Proof Text here>"
else pr_change sigma pf.goal
| Some(Decl_proof opened,script) ->
assert (List.length script = 1);
begin
if nochange then mt () else pr_change sigma pf.goal ++ fnl ()
end ++
hov 0
begin str "proof." ++ fnl () ++
print_decl_script print_prf ~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 sigma pf.goal ++ fnl ()) ++
prlist_with_sep pr_fnl (print_script ~nochange sigma) spfl
| Some(r,spfl) ->
let indent = if List.length spfl >= 2 then 1 else 0 in
(if nochange then mt () else pr_change sigma pf.goal ++ fnl ()) ++
hv indent (pr_rule_dot_fnl r ++ prlist_with_sep fnl print_prf spfl)
in hov 0 (print_prf pf)
let rec print_info_script sigma osign pf =
let sign = Goal.V82.hyps sigma 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)
|
