blob: 8e43bf6ed069bd8676fea799c09bf56b3d119ff8 (
plain)
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
|
open Format
open Term
open Names
open Cbytecodes
open Cemitcodes
open Vm
let ppripos (ri,pos) =
(match ri with
| Reloc_annot a ->
let sp,i = a.ci.ci_ind in
print_string
("annot : MutInd("^(MutInd.to_string sp)^","^(string_of_int i)^")\n")
| Reloc_const _ ->
print_string "structured constant\n"
| Reloc_getglobal kn ->
print_string ("getglob "^(Constant.to_string kn)^"\n"));
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
| Prop(Pos) -> print_string "Set"
| Prop(Null) -> 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
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
| Atype u -> print_string "Type(...)"
| 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
| Vsort s -> ppsort s
| 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
| 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 ppvalues v =
open_hovbox 0;ppwhd (whd_val v);close_box();
print_flush()
|
