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
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
|
(************************************************************************)
(* 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 *)
(************************************************************************)
(* Printers for the ocaml toplevel. *)
open System
open Pp
open Ast
open Names
open Libnames
open Nameops
open Sign
open Univ
open Proof_trees
open Environ
open Printer
open Refiner
open Tacmach
open Term
open Termops
open Clenv
open Cerrors
open Constrextern
open Constrintern
let _ = Constrextern.print_evar_arguments := true
let pP s = pp (hov 0 s)
let prast c = pp(print_ast c)
let prastpat c = pp(print_astpat c)
let prastpatl c = pp(print_astlpat c)
let ppterm x = pp(prterm x)
let ppsterm x = ppterm (Declarations.force x)
let ppterm_univ x = Constrextern.with_universes ppterm x
let pprawterm = (fun x -> pp(pr_rawterm x))
let pppattern = (fun x -> pp(pr_pattern x))
let pptype = (fun x -> pp(prtype x))
let safe_prglobal = function
| ConstRef kn -> pp (str "CONSTREF(" ++ pr_kn kn ++ str ")")
| IndRef (kn,i) -> pp (str "INDREF(" ++ pr_kn kn ++ str "," ++
int i ++ str ")")
| ConstructRef ((kn,i),j) -> pp (str "INDREF(" ++ pr_kn kn ++ str "," ++
int i ++ str "," ++ int j ++ str ")")
| VarRef id -> pp (str "VARREF(" ++ pr_id id ++ str ")")
let prglobal x = try pp(pr_global x) with _ -> safe_prglobal x
let prid id = pp (pr_id id)
let prlab l = pp (pr_lab l)
let prmsid msid = pp (str (debug_string_of_msid msid))
let prmbid mbid = pp (str (debug_string_of_mbid mbid))
let prdir dir = pp (pr_dirpath dir)
let prmp mp = pp(str (string_of_mp mp))
let prkn kn = pp(pr_kn kn)
let prsp sp = pp(pr_sp sp)
let prqualid qid = pp(pr_qualid qid)
let prconst (sp,j) =
pp (str"#" ++ pr_kn sp ++ str"=" ++ prterm j.uj_val)
let prvar ((id,a)) =
pp (str"#" ++ pr_id id ++ str":" ++ prterm a)
let genprj f j = let (c,t) = f j in (c ++ str " : " ++ t)
let prj j = pp (genprj prjudge j)
let prgoal g = pp(prgl g)
let prsigmagoal g = pp(prgl (sig_it g))
let prgls gls = pp(pr_gls gls)
let prglls glls = pp(pr_glls glls)
let pproof p = pp(print_proof Evd.empty empty_named_context p)
let prevd evd = pp(pr_decls evd)
let prevc evc = pp(pr_evc evc)
let prwc wc = pp(pr_evc wc)
let prclenv clenv = pp(pr_clenv clenv)
let print_uni u = (pp (pr_uni u))
let pp_universes u = pp (str"[" ++ pr_universes u ++ str"]")
let ppenv e = pp
(str "[" ++ pr_named_context_of e ++ str "]" ++ spc() ++
str "[" ++ pr_rel_context e (rel_context e) ++ str "]")
let pptac = (fun x -> pp(Pptactic.pr_glob_tactic x))
let pr_obj obj = Format.print_string (Libobject.object_tag obj)
let cnt = ref 0
let constr_display csr =
let rec term_display c = match kind_of_term c with
| Rel n -> "Rel("^(string_of_int n)^")"
| Meta n -> "Meta("^(string_of_int n)^")"
| Var id -> "Var("^(string_of_id id)^")"
| Sort s -> "Sort("^(sort_display s)^")"
| Cast (c,t) -> "Cast("^(term_display c)^","^(term_display t)^")"
| Prod (na,t,c) ->
"Prod("^(name_display na)^","^(term_display t)^","^(term_display c)^")\n"
| Lambda (na,t,c) ->
"Lambda("^(name_display na)^","^(term_display t)^","^(term_display c)^")\n"
| LetIn (na,b,t,c) ->
"LetIn("^(name_display na)^","^(term_display b)^","
^(term_display t)^","^(term_display c)^")"
| App (c,l) -> "App("^(term_display c)^","^(array_display l)^")\n"
| Evar (e,l) -> "Evar("^(string_of_int e)^","^(array_display l)^")"
| Const c -> "Const("^(string_of_kn c)^")"
| Ind (sp,i) ->
"MutInd("^(string_of_kn sp)^","^(string_of_int i)^")"
| Construct ((sp,i),j) ->
"MutConstruct(("^(string_of_kn sp)^","^(string_of_int i)^"),"
^(string_of_int j)^")"
| Case (ci,p,c,bl) ->
"MutCase(<abs>,"^(term_display p)^","^(term_display c)^","
^(array_display bl)^")"
| Fix ((t,i),(lna,tl,bl)) ->
"Fix(([|"^(Array.fold_right (fun x i -> (string_of_int x)^(if not(i="")
then (";"^i) else "")) t "")^"|],"^(string_of_int i)^"),"
^(array_display tl)^","
^(Array.fold_right (fun x i -> (name_display x)^(if not(i="")
then (";"^i) else "")) lna "")^","
^(array_display bl)^")"
| CoFix(i,(lna,tl,bl)) ->
"CoFix("^(string_of_int i)^"),"
^(array_display tl)^","
^(Array.fold_right (fun x i -> (name_display x)^(if not(i="")
then (";"^i) else "")) lna "")^","
^(array_display bl)^")"
and array_display v =
"[|"^
(Array.fold_right
(fun x i -> (term_display x)^(if not(i="") then (";"^i) else ""))
v "")^"|]"
and sort_display = function
| Prop(Pos) -> "Prop(Pos)"
| Prop(Null) -> "Prop(Null)"
| Type u ->
incr cnt; pp (str "with " ++ int !cnt ++ pr_uni u ++ fnl ());
"Type("^(string_of_int !cnt)^")"
and name_display = function
| Name id -> "Name("^(string_of_id id)^")"
| Anonymous -> "Anonymous"
in
msg (str (term_display csr) ++fnl ())
open Format;;
let print_pure_constr csr =
let rec term_display c = match kind_of_term c with
| Rel n -> print_string "#"; print_int n
| Meta n -> print_string "Meta("; print_int n; print_string ")"
| Var id -> print_string (string_of_id id)
| Sort s -> sort_display s
| Cast (c,t) -> open_hovbox 1;
print_string "("; (term_display c); print_cut();
print_string "::"; (term_display t); print_string ")"; close_box()
| Prod (Name(id),t,c) ->
open_hovbox 1;
print_string"("; print_string (string_of_id id);
print_string ":"; box_display t;
print_string ")"; print_cut();
box_display c; close_box()
| Prod (Anonymous,t,c) ->
print_string"("; box_display t; print_cut(); print_string "->";
box_display c; print_string ")";
| Lambda (na,t,c) ->
print_string "["; name_display na;
print_string ":"; box_display t; print_string "]";
print_cut(); box_display c;
| LetIn (na,b,t,c) ->
print_string "["; name_display na; print_string "=";
box_display b; print_cut();
print_string ":"; box_display t; print_string "]";
print_cut(); box_display c;
| App (c,l) ->
print_string "(";
box_display c;
Array.iter (fun x -> print_space (); box_display x) l;
print_string ")"
| Evar (e,l) -> print_string "Evar#"; print_int e; print_string "{";
Array.iter (fun x -> print_space (); box_display x) l;
print_string"}"
| Const c -> print_string "Cons(";
sp_display c;
print_string ")"
| Ind (sp,i) ->
print_string "Ind(";
sp_display sp;
print_string ","; print_int i;
print_string ")"
| Construct ((sp,i),j) ->
print_string "Constr(";
sp_display sp;
print_string ",";
print_int i; print_string ","; print_int j; print_string ")"
| Case (ci,p,c,bl) ->
open_vbox 0;
print_string "<"; box_display p; print_string ">";
print_cut(); print_string "Case";
print_space(); box_display c; print_space (); print_string "of";
open_vbox 0;
Array.iter (fun x -> print_cut(); box_display x) bl;
close_box();
print_cut();
print_string "end";
close_box()
| Fix ((t,i),(lna,tl,bl)) ->
print_string "Fix("; print_int i; print_string ")";
print_cut();
open_vbox 0;
let rec print_fix () =
for k = 0 to Array.length tl - 1 do
open_vbox 0;
name_display lna.(k); print_string "/";
print_int t.(k); print_cut(); print_string ":";
box_display tl.(k) ; print_cut(); print_string ":=";
box_display bl.(k); close_box ();
print_cut()
done
in print_string"{"; print_fix(); print_string"}"
| CoFix(i,(lna,tl,bl)) ->
print_string "CoFix("; print_int i; print_string ")";
print_cut();
open_vbox 0;
let rec print_fix () =
for k = 0 to Array.length tl - 1 do
open_vbox 1;
name_display lna.(k); print_cut(); print_string ":";
box_display tl.(k) ; print_cut(); print_string ":=";
box_display bl.(k); close_box ();
print_cut();
done
in print_string"{"; print_fix (); print_string"}"
and box_display c = open_hovbox 1; term_display c; close_box()
and sort_display = function
| Prop(Pos) -> print_string "Set"
| Prop(Null) -> print_string "Prop"
| Type u -> open_hbox();
print_string "Type("; pp (pr_uni u); print_string ")"; close_box()
and name_display = function
| Name id -> print_string (string_of_id id)
| Anonymous -> print_string "_"
(* Remove the top names for library and Scratch to avoid long names *)
and sp_display sp =
(* let dir,l = decode_kn sp in
let ls =
match List.rev (List.map string_of_id (repr_dirpath dir)) with
("Top"::l)-> l
| ("Coq"::_::l) -> l
| l -> l
in List.iter (fun x -> print_string x; print_string ".") ls;*)
print_string (string_of_kn sp)
in
box_display csr; print_flush()
(*
let _ =
Vernacentries.add "PrintConstr"
(function
| [VARG_CONSTR c] ->
(fun () ->
let (evmap,sign) = Command.get_current_context () in
constr_display (Constrintern.interp_constr evmap sign c))
| _ -> bad_vernac_args "PrintConstr")
let _ =
Vernacentries.add "PrintPureConstr"
(function
| [VARG_CONSTR c] ->
(fun () ->
let (evmap,sign) = Command.get_current_context () in
print_pure_constr (Constrintern.interp_constr evmap sign c))
| _ -> bad_vernac_args "PrintPureConstr")
*)
let ppfconstr c = ppterm (Closure.term_of_fconstr c)
|
