-
Notifications
You must be signed in to change notification settings - Fork 4
/
syntax.ml
334 lines (277 loc) · 9.3 KB
/
syntax.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
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
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
open Format
open Support.Error
open Support.Pervasive
(* ---------------------------------------------------------------------- *)
(* Datatypes *)
type kind =
KnStar
| KnArr of kind * kind
type ty =
TyTop
| TyVar of int * int
| TyArr of ty * ty
| TyAll of string * ty * ty
| TyAbs of string * kind * ty
| TyApp of ty * ty
type term =
TmVar of info * int * int
| TmAbs of info * string * ty * term
| TmApp of info * term * term
| TmTAbs of info * string * ty * term
| TmTApp of info * term * ty
type binding =
NameBind
| VarBind of ty
| TyVarBind of ty
type context = (string * binding) list
type command =
| Eval of info * term
| Bind of info * string * binding
(* ---------------------------------------------------------------------- *)
(* Context management *)
let emptycontext = []
let ctxlength ctx = List.length ctx
let addbinding ctx x bind = (x,bind)::ctx
let addname ctx x = addbinding ctx x NameBind
let rec isnamebound ctx x =
match ctx with
[] -> false
| (y,_)::rest ->
if y=x then true
else isnamebound rest x
let rec pickfreshname ctx x =
if isnamebound ctx x then pickfreshname ctx (x^"'")
else ((x,NameBind)::ctx), x
let index2name fi ctx x =
try
let (xn,_) = List.nth ctx x in
xn
with Failure _ ->
let msg =
Printf.sprintf "Variable lookup failure: offset: %d, ctx size: %d" in
error fi (msg x (List.length ctx))
let rec name2index fi ctx x =
match ctx with
[] -> error fi ("Identifier " ^ x ^ " is unbound")
| (y,_)::rest ->
if y=x then 0
else 1 + (name2index fi rest x)
(* ---------------------------------------------------------------------- *)
(* Shifting *)
let tymap onvar c tyT =
let rec walk c tyT = match tyT with
TyArr(tyT1,tyT2) -> TyArr(walk c tyT1,walk c tyT2)
| TyTop -> TyTop
| TyVar(x,n) -> onvar c x n
| TyAll(tyX,tyT1,tyT2) -> TyAll(tyX,walk c tyT1,walk (c+1) tyT2)
| TyAbs(tyX,knK1,tyT2) -> TyAbs(tyX,knK1,walk (c+1) tyT2)
| TyApp(tyT1,tyT2) -> TyApp(walk c tyT1,walk c tyT2)
in walk c tyT
let tmmap onvar ontype c t =
let rec walk c t = match t with
TmVar(fi,x,n) -> onvar fi c x n
| TmAbs(fi,x,tyT1,t2) -> TmAbs(fi,x,ontype c tyT1,walk (c+1) t2)
| TmApp(fi,t1,t2) -> TmApp(fi,walk c t1,walk c t2)
| TmTAbs(fi,tyX,tyT1,t2) ->
TmTAbs(fi,tyX,ontype c tyT1,walk (c+1) t2)
| TmTApp(fi,t1,tyT2) -> TmTApp(fi,walk c t1,ontype c tyT2)
in walk c t
let typeShiftAbove d c tyT =
tymap
(fun c x n -> if x>=c then TyVar(x+d,n+d) else TyVar(x,n+d))
c tyT
let termShiftAbove d c t =
tmmap
(fun fi c x n -> if x>=c then TmVar(fi,x+d,n+d)
else TmVar(fi,x,n+d))
(typeShiftAbove d)
c t
let termShift d t = termShiftAbove d 0 t
let typeShift d tyT = typeShiftAbove d 0 tyT
let bindingshift d bind =
match bind with
NameBind -> NameBind
| VarBind(tyT) -> VarBind(typeShift d tyT)
| TyVarBind(tyS) -> TyVarBind(typeShift d tyS)
(* ---------------------------------------------------------------------- *)
(* Substitution *)
let termSubst j s t =
tmmap
(fun fi j x n -> if x=j then termShift j s else TmVar(fi,x,n))
(fun j tyT -> tyT)
j t
let termSubstTop s t =
termShift (-1) (termSubst 0 (termShift 1 s) t)
let typeSubst tyS j tyT =
tymap
(fun j x n -> if x=j then (typeShift j tyS) else (TyVar(x,n)))
j tyT
let typeSubstTop tyS tyT =
typeShift (-1) (typeSubst (typeShift 1 tyS) 0 tyT)
let rec tytermSubst tyS j t =
tmmap (fun fi c x n -> TmVar(fi,x,n))
(fun j tyT -> typeSubst tyS j tyT) j t
let tytermSubstTop tyS t =
termShift (-1) (tytermSubst (typeShift 1 tyS) 0 t)
(* ---------------------------------------------------------------------- *)
(* Context management (continued) *)
let rec getbinding fi ctx i =
try
let (_,bind) = List.nth ctx i in
bindingshift (i+1) bind
with Failure _ ->
let msg =
Printf.sprintf "Variable lookup failure: offset: %d, ctx size: %d" in
error fi (msg i (List.length ctx))
let getTypeFromContext fi ctx i =
match getbinding fi ctx i with
VarBind(tyT) -> tyT
| _ -> error fi
("getTypeFromContext: Wrong kind of binding for variable "
^ (index2name fi ctx i))
let rec maketop k = match k with
KnStar -> TyTop
| KnArr(knK1,knK2) -> TyAbs("_",knK1,maketop knK2)
(* ---------------------------------------------------------------------- *)
(* Extracting file info *)
let tmInfo t = match t with
TmVar(fi,_,_) -> fi
| TmAbs(fi,_,_,_) -> fi
| TmApp(fi, _, _) -> fi
| TmTAbs(fi,_,_,_) -> fi
| TmTApp(fi,_, _) -> fi
(* ---------------------------------------------------------------------- *)
(* Printing *)
(* The printing functions call these utility functions to insert grouping
information and line-breaking hints for the pretty-printing library:
obox Open a "box" whose contents will be indented by two spaces if
the whole box cannot fit on the current line
obox0 Same but indent continuation lines to the same column as the
beginning of the box rather than 2 more columns to the right
cbox Close the current box
break Insert a breakpoint indicating where the line maybe broken if
necessary.
See the documentation for the Format module in the OCaml library for
more details.
*)
let obox0() = open_hvbox 0
let obox() = open_hvbox 2
let cbox() = close_box()
let break() = print_break 0 0
let small t =
match t with
TmVar(_,_,_) -> true
| _ -> false
let rec printkn_kind outer ctx k = match k with
knK -> printkn_arrowkind outer ctx knK
and printkn_arrowkind outer ctx k = match k with
KnArr(knK1,knK2) ->
obox0();
printkn_akind false ctx knK1;
if outer then pr " ";
pr "=>";
if outer then print_space() else break();
printkn_arrowkind outer ctx knK2;
cbox()
| knK -> printkn_akind outer ctx knK
and printkn_akind outer ctx k = match k with
KnStar -> pr "*"
| knK -> pr "("; printkn_kind outer ctx knK; pr ")"
let printkn ctx knK = printkn_kind true ctx knK
let prokn ctx knK =
if knK <> KnStar then (pr "::"; printkn_kind false ctx knK)
let rec printty_Type outer ctx tyT = match tyT with
TyAll(tyX,tyT1,tyT2) ->
let (ctx1,tyX) = (pickfreshname ctx tyX) in
obox(); pr "All "; pr tyX;
proty ctx tyT1;
pr ".";
print_space ();
printty_Type outer ctx1 tyT2;
cbox()
| TyAbs(tyX,knK1,tyT2) ->
let (ctx',x') = (pickfreshname ctx tyX) in
obox(); pr "lambda ";
pr x'; prokn ctx knK1;
pr "."; if outer then print_space() else break();
printty_Type outer ctx' tyT2;
cbox()
| tyT -> printty_ArrowType outer ctx tyT
and printty_ArrowType outer ctx tyT = match tyT with
TyArr(tyT1,tyT2) ->
obox0();
printty_AppType false ctx tyT1;
if outer then pr " ";
pr "->";
if outer then print_space() else break();
printty_ArrowType outer ctx tyT2;
cbox()
| tyT -> printty_AppType outer ctx tyT
and proty ctx tyS =
if tyS <> TyTop then (pr "<:"; printty_Type false ctx tyS)
and printty_AppType outer ctx k = match k with
TyApp(tyT1,tyT2) ->
obox0();
printty_AppType false ctx tyT1;
print_space();
printty_AType false ctx tyT2;
cbox()
| tyT -> printty_AType outer ctx tyT
and printty_AType outer ctx tyT = match tyT with
TyTop -> pr "Top"
| TyVar(x,n) ->
if ctxlength ctx = n then
pr (index2name dummyinfo ctx x)
else
pr ("[bad index: " ^ (string_of_int x) ^ "/" ^ (string_of_int n)
^ " in {"
^ (List.fold_left (fun s (x,_) -> s ^ " " ^ x) "" ctx)
^ " }]")
| tyT -> pr "("; printty_Type outer ctx tyT; pr ")"
let printty ctx tyT = printty_Type true ctx tyT
let rec printtm_Term outer ctx t = match t with
TmAbs(fi,x,tyT1,t2) ->
(let (ctx',x') = (pickfreshname ctx x) in
obox(); pr "lambda ";
pr x'; pr ":"; printty_Type false ctx tyT1; pr ".";
if (small t2) && not outer then break() else print_space();
printtm_Term outer ctx' t2;
cbox())
| TmTAbs(fi,x,tyS,t) ->
(let (ctx1,x) = (pickfreshname ctx x) in
obox(); pr "lambda "; pr x;
proty ctx tyS;
pr ".";
if (small t) && not outer then break() else print_space();
printtm_Term outer ctx1 t;
cbox())
| t -> printtm_AppTerm outer ctx t
and printtm_AppTerm outer ctx t = match t with
TmApp(fi, t1, t2) ->
obox0();
printtm_AppTerm false ctx t1;
print_space();
printtm_ATerm false ctx t2;
cbox()
| TmTApp(fi,t,tyS) ->
obox0();
printtm_AppTerm false ctx t;
print_space();
pr "["; printty_Type false ctx tyS; pr "]";
cbox()
| t -> printtm_ATerm outer ctx t
and printtm_ATerm outer ctx t = match t with
TmVar(fi,x,n) ->
if ctxlength ctx = n then
pr (index2name fi ctx x)
else
pr ("[bad index: " ^ (string_of_int x) ^ "/" ^ (string_of_int n)
^ " in {"
^ (List.fold_left (fun s (x,_) -> s ^ " " ^ x) "" ctx)
^ " }]")
| t -> pr "("; printtm_Term outer ctx t; pr ")"
let printtm ctx t = printtm_Term true ctx t
let prbinding ctx b = match b with
NameBind -> ()
| VarBind(tyT) -> pr ": "; printty ctx tyT
| TyVarBind(tyS) -> pr "<: ";printty_Type false ctx tyS