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
|
(* Printers for the ocaml toplevel. *)
open System
open Pp
open Ast
open Names
open Sign
open Univ
open Proof_trees
open Environ
open Printer
open Refiner
open Tacmach
open Term
open Vernacinterp
open Clenv
open Errors
let _ = Termast.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 = (fun x -> pP(prterm 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 prid id = pP [< 'sTR(string_of_id id) >]
let prconst (sp,j) =
pP [< 'sTR"#"; 'sTR(string_of_path sp);
'sTR"="; prterm j.uj_val >]
let prvar ((id,a)) =
pP [< 'sTR"#" ; 'sTR(string_of_id id) ; 'sTR":" ;
prterm a >]
let genprj f j =
let (c,t) = Termast.with_casts f j in [< c; 'sTR " : "; t >]
let prj j = pP (genprj prjudge j)
let prsp sp = pP[< 'sTR(string_of_path sp) >]
let prqualid qid = pP[< pr_qualid qid >]
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 prctxt ctxt = pP(pr_ctxt ctxt)
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 cnt = ref 0
let constr_display csr =
let rec term_display c = match kind_of_term c with
| IsRel n -> "Rel("^(string_of_int n)^")"
| IsMeta n -> "Meta("^(string_of_int n)^")"
| IsVar id -> "Var("^(string_of_id id)^")"
| IsSort s -> "Sort("^(sort_display s)^")"
| IsXtra s -> "Xtra("^s^")"
| IsCast (c,t) -> "Cast("^(term_display c)^","^(term_display t)^")"
| IsProd (na,t,c) ->
"Prod("^(name_display na)^","^(term_display t)^","^(term_display c)^")\n"
| IsLambda (na,t,c) ->
"Lambda("^(name_display na)^","^(term_display t)^","^(term_display c)^")\n"
| IsLetIn (na,b,t,c) ->
"LetIn("^(name_display na)^","^(term_display b)^","
^(term_display t)^","^(term_display c)^")"
| IsApp (c,l) -> "App("^(term_display c)^","^(array_display l)^")\n"
| IsEvar (e,l) -> "Evar("^(string_of_int e)^","^(array_display l)^")"
| IsConst (c,l) -> "Const("^(string_of_path c)^","^(array_display l)^")"
| IsMutInd ((sp,i),l) ->
"MutInd(("^(string_of_path sp)^","^(string_of_int i)^"),"
^(array_display l)^")"
| IsMutConstruct (((sp,i),j),l) ->
"MutConstruct((("^(string_of_path sp)^","^(string_of_int i)^"),"
^(string_of_int j)^"),"^(array_display l)^")"
| IsMutCase (ci,p,c,bl) ->
"MutCase(<abs>,"^(term_display p)^","^(term_display c)^","
^(array_display bl)^")"
| IsFix ((t,i),(tl,lna,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)^","
^(List.fold_right (fun x i -> (name_display x)^(if not(i="")
then (";"^i) else "")) lna "")^","
^(array_display bl)^")"
| IsCoFix(i,(tl,lna,bl)) ->
"CoFix("^(string_of_int i)^"),"
^(array_display tl)^","
^(List.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>]
let _ =
Vernacentries.add "PrintConstr"
(function
| [VARG_CONSTR c] ->
(fun () ->
let (evmap,sign) = Command.get_current_context () in
constr_display (Astterm.interp_constr evmap sign c))
| _ -> bad_vernac_args "PrintConstr")
|
