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
|
open Format
open Term
open Names
open Vmemitcodes
open Vmvalues
let ppripos (ri,pos) =
(match ri with
| Reloc_annot a ->
print_string "switch\n"
| Reloc_const _ ->
print_string "structured constant\n"
| Reloc_getglobal kn ->
print_string ("getglob "^(Constant.to_string kn)^"\n")
| Reloc_caml_prim op ->
print_string ("caml primitive "^ CPrimitives.to_string @@ Vmbytecodes.caml_prim_to_prim op)
);
print_flush ()
let print_vfix () = print_string "vfix"
let print_vfix_app () = print_string "vfix_app"
let print_vswith () = print_string "switch"
let ppsort = function
| SProp -> print_string "SProp"
| Set -> print_string "Set"
| Prop -> print_string "Prop"
| Type u -> print_string "Type"
let print_idkey idk =
match idk with
| ConstKey sp ->
print_string "Cons(";
print_string (Constant.to_string sp);
print_string ")"
| VarKey id -> print_string (Id.to_string id)
| RelKey i -> print_string "~";print_int i
| EvarKey evk ->
print_string "Evar(";
print_int (Evar.repr evk);
print_string ")"
let rec ppzipper z =
match z with
| Zapp args ->
let n = nargs args in
open_hbox ();
for i = 0 to n-2 do
ppvalues (arg args i);print_string ";";print_space()
done;
if n-1 >= 0 then ppvalues (arg args (n-1));
close_box()
| Zfix _ -> print_string "Zfix"
| Zswitch _ -> print_string "Zswitch"
| Zproj _ -> print_string "Zproj"
and ppstack s =
open_hovbox 0;
print_string "[";
List.iter (fun z -> ppzipper z;print_string " | ") s;
print_string "]";
close_box()
and ppatom a =
match a with
| Aid idk -> print_idkey idk
| Asort u -> print_string "Sort(...)"
| Aind(sp,i) -> print_string "Ind(";
print_string (MutInd.to_string sp);
print_string ","; print_int i;
print_string ")"
and ppwhd whd =
match whd with
| Vprod _ -> print_string "product"
| Vfun _ -> print_string "function"
| Vfix _ -> print_vfix()
| Vcofix _ -> print_string "cofix"
| Vconstr_const i -> print_string "C(";print_int i;print_string")"
| Vconstr_block b -> ppvblock b
| Vint64 i -> printf "int64(%LiL)" i
| Vfloat64 f -> printf "float64(%.17g)" f
| Varray t -> ppvarray t
| Vatom_stk(a,s) ->
open_hbox();ppatom a;close_box();
print_string"@";ppstack s
| Vuniv_level lvl -> Feedback.msg_notice (Univ.Level.pr lvl)
and ppvblock b =
open_hbox();
print_string "Cb(";print_int (btag b);
let n = bsize b in
for i = 0 to n -1 do
print_string ",";ppvalues (bfield b i)
done;
print_string")";
close_box()
and ppvarray t =
let length = Parray.length_int t in
open_hbox();
print_string "[|";
for i = 0 to length - 2 do
ppvalues (Parray.get t (Uint63.of_int i));
print_string "; "
done;
ppvalues (Parray.get t (Uint63.of_int (length - 1)));
print_string " | ";
ppvalues (Parray.default t);
print_string " |]";
close_box()
and ppvalues v =
open_hovbox 0;ppwhd (whd_val v);close_box();
print_flush()
|
