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
|
(************************************************************************)
(* 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:$ *)
open Util
open Pp
open Decl_expr
open Names
open Nameops
let pr_constr = Printer.pr_constr_env
let pr_tac = Pptactic.pr_glob_tactic
let pr_pat mpat = Ppconstr.pr_cases_pattern_expr mpat.pat_expr
let pr_label = function
Anonymous -> mt ()
| Name id -> pr_id id ++ spc () ++ str ":" ++ spc ()
let pr_justification env = function
Automated [] -> mt ()
| Automated (_::_ as l) ->
spc () ++ str "by" ++ spc () ++
prlist_with_sep (fun () -> str ",") (pr_constr env) l
| By_tactic tac ->
spc () ++ str "by" ++ spc () ++ str "tactic" ++ pr_tac env tac
let pr_statement pr_it env st =
pr_label st.st_label ++ pr_it env st.st_it
let pr_or_thesis pr_this env = function
Thesis Plain -> str "thesis"
| Thesis (For id) ->
str "thesis" ++ spc() ++ str "for" ++ spc () ++ pr_id id
| Thesis (Sub n) -> str "thesis[" ++ int n ++ str "]"
| This c -> pr_this env c
let pr_cut pr_it env c =
hov 1 (pr_statement pr_it env c.cut_stat) ++
pr_justification env c.cut_by
let type_or_thesis = function
Thesis _ -> Term.mkProp
| This c -> c
let _I x = x
let rec print_hyps pconstr gtyp env _and _be hyps =
let _andp = if _and then str "and" ++spc () else mt () in
match hyps with
(Hvar _ ::_) as rest ->
spc () ++ _andp ++ str "we have" ++
print_vars pconstr gtyp env false _be rest
| Hprop st :: rest ->
begin
let nenv =
match st.st_label with
Anonymous -> env
| Name id -> Environ.push_named (id,None,gtyp st.st_it) env in
spc() ++ _andp ++ pr_statement pconstr env st ++
print_hyps pconstr gtyp nenv true _be rest
end
| [] -> mt ()
and print_vars pconstr gtyp env _and _be vars =
match vars with
Hvar st :: rest ->
begin
let nenv =
match st.st_label with
Anonymous -> anomaly "anonymous variable"
| Name id -> Environ.push_named (id,None,st.st_it) env in
let _andp = if _and then pr_coma () else mt () in
spc() ++ _andp ++
pr_statement pr_constr env st ++
print_vars pconstr gtyp nenv true _be rest
end
| (Hprop _ :: _) as rest ->
let _st = if _be then
str "be such that"
else
str "such that" in
spc() ++ _st ++ print_hyps pconstr gtyp env false _be rest
| [] -> mt ()
let pr_elim_type = function
ET_Case_analysis -> str "cases"
| ET_Induction -> str "induction"
let pr_casee env =function
Real c -> str "on" ++ spc () ++ pr_constr env c
| Virtual cut -> str "of" ++ spc () ++ pr_cut pr_constr env cut
let pr_side = function
Lhs -> str "=~"
| Rhs -> str "~="
let rec pr_bare_proof_instr _then _thus env = function
| Pescape -> str "escape"
| Pthen i -> pr_bare_proof_instr true _thus env i
| Pthus i -> pr_bare_proof_instr _then true env i
| Phence i -> pr_bare_proof_instr true true env i
| Pcut c ->
begin
match _then,_thus with
false,false -> str "have" ++ spc () ++
pr_cut (pr_or_thesis pr_constr) env c
| false,true -> str "thus" ++ spc () ++
pr_cut (pr_or_thesis pr_constr) env c
| true,false -> str "then" ++ spc () ++
pr_cut (pr_or_thesis pr_constr) env c
| true,true -> str "hence" ++ spc () ++
pr_cut (pr_or_thesis pr_constr) env c
end
| Prew (sid,c) ->
(if _thus then str "thus" else str " ") ++ spc () ++
pr_side sid ++ spc () ++ pr_cut pr_constr env c
| Passume hyps ->
str "assume" ++ print_hyps pr_constr _I env false false hyps
| Plet hyps ->
str "let" ++ print_vars pr_constr _I env false true hyps
| Pclaim st ->
str "claim" ++ spc () ++ pr_statement pr_constr env st
| Pfocus st ->
str "focus on" ++ spc () ++ pr_statement pr_constr env st
| Pconsider (id,hyps) ->
str "consider" ++ print_vars pr_constr _I env false false hyps
++ spc () ++ str "from " ++ pr_constr env id
| Pgiven hyps ->
str "given" ++ print_vars pr_constr _I env false false hyps
| Ptake witl ->
str "take" ++ spc () ++
prlist_with_sep pr_coma (pr_constr env) witl
| Pdefine (id,args,body) ->
str "define" ++ spc () ++ pr_id id ++ spc () ++
prlist_with_sep spc
(fun st -> str "(" ++
pr_statement pr_constr env st ++ str ")") args ++ spc () ++
str "as" ++ (pr_constr env body)
| Pcast (id,typ) ->
str "reconsider" ++ spc () ++
pr_or_thesis (fun _ -> pr_id) env id ++ spc () ++
str "as" ++ (pr_constr env typ)
| Psuppose hyps ->
str "suppose" ++
print_hyps pr_constr _I env false false hyps
| Pcase (params,pat,hyps) ->
str "suppose it is" ++ spc () ++ pr_pat pat ++
(if params = [] then mt () else
(spc () ++ str "with" ++ spc () ++
prlist_with_sep spc
(fun st -> str "(" ++
pr_statement pr_constr env st ++ str ")") params ++ spc ()))
++
(if hyps = [] then mt () else
(spc () ++ str "and" ++
print_hyps (pr_or_thesis pr_constr) type_or_thesis
env false false hyps))
| Pper (et,c) ->
str "per" ++ spc () ++ pr_elim_type et ++ spc () ++
pr_casee env c
| Pend (B_elim et) -> str "end" ++ spc () ++ pr_elim_type et
| _ -> anomaly "unprintable instruction"
let pr_emph = function
0 -> str " "
| 1 -> str "* "
| 2 -> str "** "
| 3 -> str "*** "
| _ -> anomaly "unknown emphasis"
let pr_proof_instr env instr =
pr_emph instr.emph ++ spc () ++
pr_bare_proof_instr false false env instr.instr
|
