-
Notifications
You must be signed in to change notification settings - Fork 17
/
extract.ml
175 lines (169 loc) · 4.26 KB
/
extract.ml
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
(*
* (c) 2014 Andreas Rossberg
*)
open Fomega
type kind =
| BaseK
| ArrK of kind * kind
| ProdK of kind row
type typ =
| VarT of var
| PrimT of Prim.typ
| ArrT of typ * typ
| ProdT of typ row
| AllT of var * kind * typ
| AnyT of var * kind * typ
| FunT of var * kind * typ
| AppT of typ * typ
| StrT of typ row
| DotT of typ * lab
| RecT of var * kind * typ
| InferT of typ lazy_t * int
let rec print_typ' prec = function
| VarT(a, k, n) ->
let s = string_of_var a n in
if k <> BaseK && !verbose_vars_flag then
print_paren base_prec prec (fun () ->
print_string s;
print_string ":";
print_break 0 2;
print_kind' base_prec ctxt k
)
else
print_string s
| PrimT(t) ->
print_string (Prim.string_of_typ t)
| StrT(tr) ->
(match as_tup_row tr with
| Some ts ->
print_brack "(" ")" (fun () ->
print_list' print_typ' base_prec ctxt ts;
)
| None ->
print_brack "{" "}" (fun () ->
print_row' ":" print_typ' base_prec ctxt tr;
)
)
| FunT(a, k, t, s, p) ->
print_binder prec "!" a k (fun () ->
open_box 0;
print_typ' (binder_prec + 1) ([a]::ctxt) t;
close_box ();
print_string " ";
print_string
(match p with Impure -> "->" | Pure -> "=>" | Implicit -> "'=>");
print_break 1 2;
open_box 0;
print_extyp' binder_prec (enter "()" ctxt) s;
close_box ()
)
| TypT(s) ->
print_brack "[= " "]" (fun () -> print_extyp' base_prec ctxt s);
| PackT(s) ->
print_brack "[" "]" (fun () -> print_extyp' base_prec ctxt s);
| ProdT(tr) ->
print_brack "{" "}" (fun () ->
print_row' "=" print_typ' base_prec ctxt tr;
)
| LamT(a, k, t) ->
print_binder prec "\\" a k (fun () ->
print_typ' binder_prec ctxt t
)
| DotT(t, l) ->
if String.contains l '$' then
print_typ' prec ctxt t
else if matches_ctxt t ctxt then
print_string l
else
print_paren dot_prec prec (fun () ->
print_typ' dot_prec ctxt t;
print_string ".";
print_string l
)
| AppT(t1, t2) ->
print_paren app_prec prec (fun () ->
print_typ' app_prec ctxt t1;
print_string "(";
print_break 0 2;
print_typ' base_prec ctxt t2;
print_string ")"
)
| RecT(a, k, t) ->
print_binder prec "@" a k (fun () ->
print_typ' binder_prec ctxt t
)
| InferT(z) ->
match !z with
| Det t -> print_typ' prec ctxt t
| Undet u -> print_string (string_of_var ("'" ^ string_of_int u.id) u.level)
let rec print_exp' prec = function
| VarE(x) -> print_var x
| PrimE(c) -> print_const c
| IfE(e1, e2, e3) ->
print_paren pre_prec prec (fun () ->
open_box 0;
print_string "if ";
print_exp' prec e1;
print_break 1 0;
print_string "then ";
print_exp' base_prec e2;
print_break 1 0;
print_string "then ";
print_exp' pre_prec e3;
close_box ()
)
| FunE(x, t, e) ->
print_paren pre_prec prec (fun () ->
open_box 0;
print_string "fun (";
print_var x;
print_string " : ";
print_typ' base_prec t;
print_string ")";
print_break 1 0;
print_string "-> ";
print_exp' pre_prec e;
close_box ()
)
| AppE(e1, e2) ->
print_paren app_prec prec (fun () ->
open_box 0;
print_exp' app_prec e1;
print_break 1 0;
print_exp' (app_prec + 1) e2;
close_box ()
)
| StrE(er) ->
print_paren tup_prec prec (fun () ->
print_list' print_exp' (tup_prec + 1) (List.map snd er)
)
| DotE(e, l) ->
print_paren pre_prec prec (fun () ->
open_box 0;
print_string "let ";
print_list' print_exp' tup_prec (List.map snd er)
(* TODO *)
print_string " =";
print_break 1 2;
open_box 0;
print_exp' base_prec e;
close_box ();
print_break 1 0;
print_string "in";
print_break 1 0;
print_var l;
close_box ()
)
| GenE(a, k, e) ->
print_brack "(" ")" (fun () ->
open_box 0;
print_string "module ";
close_box ()
)
| InstE of exp * typ
| PackE(t1, e, t2) ->
| OpenE of exp * var * var * exp
| RollE of exp * typ
| UnrollE of exp
| RecE of var * typ * exp
| LetE of exp * var * exp