Commit | Line | Data |
---|---|---|
7f918cf1 CE |
1 | val toString = Int.toString |
2 | ||
3 | (* Ported to kit 23/4/97 by Mads. | |
4 | Commented out module phrases and changed a couple of sml/nj things (like makestring) | |
5 | No rewriting to please region inference. | |
6 | Still it uses less that 100Kb when it runs (see region.ps) | |
7 | *) | |
8 | ||
9 | (* This is a quickly written type checker for subtyping, using the | |
10 | MATCH and TYPE algorithms from the Fuh and Mishra paper. | |
11 | ||
12 | The code is ugly at places, and no consideration has been given to | |
13 | effeciency -- please accept my apologies | |
14 | ||
15 | -- Mads*) | |
16 | ||
17 | (* | |
18 | structure List = (* list utilities *) | |
19 | struct | |
20 | *) | |
21 | type 'a set = 'a list; (* sets are represented by lists without repeated | |
22 | elements *) | |
23 | val emptyset = [] | |
24 | ||
25 | fun isin(x,[])=false | |
26 | | isin(x,(y::rest)) = x=y orelse isin(x,rest) | |
27 | ||
28 | fun union([],l) = l | |
29 | | union((x::rest),l) = if isin(x,l) then union(rest,l) | |
30 | else x:: union(rest,l); | |
31 | fun intersect([],l) = [] | |
32 | | intersect((x::rest),l) = if isin(x,l) then x:: intersect(rest,l) | |
33 | else intersect(rest,l); | |
34 | fun setminus([],l) = [] | |
35 | | setminus(x::l,l') = if isin(x,l') then setminus(l,l') | |
36 | else x:: setminus(l,l'); | |
37 | fun foldr f b [] = b | |
38 | | foldr f b (x::rest) = f(x,foldr f b rest); | |
39 | ||
40 | fun foldl f base [] = base | |
41 | | foldl f base (x::xs) = foldl f (f(x, base)) xs | |
42 | ||
43 | (* function for finding transitive closure. | |
44 | Culled from other application. | |
45 | DO NOT READ (CRUDE AND INEFFICIENT) *) | |
46 | ||
47 | fun transClos (eq: 'a * 'a -> bool) | |
48 | (insert_when_eq: bool) | |
49 | (newsets: 'a set list, | |
50 | oldsets: 'a set list): bool * 'a set list = | |
51 | (* The lists in oldsets are pairwise disjoint, but nothing is known about the | |
52 | lists in newsets. The resulting sets are pairwise disjoint, | |
53 | and moreover, the resulting boolean is true if and only if | |
54 | every member (i.e. list) of newsets, is contained in some member (i.e., list) | |
55 | of oldsets *) | |
56 | let | |
57 | val any: bool = true (* could be false, for that matter *) | |
58 | ||
59 | fun isin(x,[]) = false | |
60 | | isin(x,x'::rest) = eq(x,x') orelse isin(x,rest) | |
61 | ||
62 | (* In the following function, L is a list of pairwise disjoint | |
63 | sets. S' is the set currently under construction; | |
64 | it is also disjoint from the sets in L. x | |
65 | will be added to S' if x is not in any set in L. *) | |
66 | ||
67 | fun add(x:'a, | |
68 | (found_fixpt: bool, found_class: bool, L as [], S')): | |
69 | bool * bool * 'a list list * 'a list = | |
70 | if isin(x,S') | |
71 | then if insert_when_eq | |
72 | then | |
73 | (found_fixpt andalso found_class, found_class,[],x::S') | |
74 | else | |
75 | (found_fixpt andalso found_class, found_class,[],S') | |
76 | else | |
77 | (false, any, [], x::S') | |
78 | ||
79 | | add(x,(found_fixpt,found_class,(S::L), S')) = | |
80 | if isin(x,S) | |
81 | then | |
82 | if insert_when_eq | |
83 | then | |
84 | (found_fixpt andalso not found_class,true, L, x::(S @ S')) | |
85 | else | |
86 | (found_fixpt andalso not found_class,true, L, S @ S') | |
87 | else | |
88 | let val (found_fixpt1, found_class1, L1, S1)= | |
89 | add(x,(found_fixpt,found_class,L,S')) | |
90 | in | |
91 | (found_fixpt andalso found_fixpt1, | |
92 | found_class orelse found_class1, | |
93 | S::L1, | |
94 | S1 | |
95 | ) | |
96 | end | |
97 | ||
98 | fun add_S (S,(found_fixpt, oldsets)) : bool * 'a set list = | |
99 | let | |
100 | val (found_fixpt1, _, L1, S1) = | |
101 | foldl add (found_fixpt, false, oldsets, emptyset) S | |
102 | in | |
103 | case S1 of | |
104 | [] => (found_fixpt andalso found_fixpt1, L1) | |
105 | | _ => (found_fixpt andalso found_fixpt1, S1::L1) | |
106 | end | |
107 | ||
108 | in | |
109 | foldl add_S (true, oldsets) newsets | |
110 | end | |
111 | (* | |
112 | end; | |
113 | *) | |
114 | (* | |
115 | structure Variables = (* program variables *) | |
116 | struct | |
117 | *) | |
118 | type var = string | |
119 | (* | |
120 | end; | |
121 | *) | |
122 | (*structure Type = (* Types, substitutions and matching *) | |
123 | struct | |
124 | local | |
125 | (* open List Variables*) | |
126 | in | |
127 | *) datatype ty = INT | REAL | ARROW of ty * ty | PROD of ty * ty | TYVAR of int | |
128 | ||
129 | type subst = ty -> ty | |
130 | ||
131 | fun mk_subst_ty(i: int,ty:ty):subst = | |
132 | let | |
133 | fun S(INT) = INT | |
134 | | S(REAL) = REAL | |
135 | | S(ARROW(ty1,ty2)) = ARROW(S ty1, S ty2) | |
136 | | S(PROD(ty1,ty2)) = PROD(S ty1, S ty2) | |
137 | | S(tv as TYVAR j) = if i=j then ty else tv | |
138 | in | |
139 | S | |
140 | end; | |
141 | ||
142 | val Id = fn x => x; | |
143 | ||
144 | val r = ref 0; (* counter for fresh type variables *) | |
145 | fun fresh() = (r:= !r + 1; ! r); | |
146 | fun fresh_ty() = TYVAR(fresh()); | |
147 | ||
148 | (* free variables *) | |
149 | ||
150 | fun fv_ty (INT,acc) = acc | |
151 | | fv_ty (REAL,acc) = acc | |
152 | | fv_ty(ARROW(t1,t2), acc) = fv_ty(t1,fv_ty(t2,acc)) | |
153 | | fv_ty(PROD(t1,t2), acc) = fv_ty(t1,fv_ty(t2,acc)) | |
154 | | fv_ty((TYVAR i),acc) = if isin(i,acc) then acc else i :: acc; | |
155 | ||
156 | fun tyvars(t:ty) = fv_ty(t,[]) | |
157 | ||
158 | fun fv_tyenv TE = | |
159 | foldr (fn((i,tau),acc)=> fv_ty(tau,acc)) [] TE | |
160 | ||
161 | (* ALLNEW, page 168: create a fresh copy of a type, using type variables | |
162 | at the leaves of the type *) | |
163 | ||
164 | fun allnew(INT) = fresh_ty() | |
165 | | allnew(REAL) = fresh_ty() | |
166 | | allnew(ARROW(t1,t2)) = ARROW(allnew(t1),allnew(t2)) | |
167 | | allnew(PROD(t1,t2)) = PROD(allnew(t1),allnew(t2)) | |
168 | | allnew(TYVAR _) = fresh_ty(); | |
169 | ||
170 | (* PAIR, page 168: create list of atomic types that occur in the same | |
171 | places of t1 and t2 *) | |
172 | ||
173 | fun pair(ARROW(t1,t2),ARROW(t1',t2')) = pair(t1,t1') @ pair (t2,t2') | |
174 | | pair(PROD(t1,t2),PROD(t1',t2')) = pair(t1,t1') @ pair (t2,t2') | |
175 | | pair(t1,t2) = [[t1,t2]] | |
176 | ||
177 | (* dealing with equivalence classes of atomic types -- for algorithm MATCH *) | |
178 | ||
179 | (* M_v, page 168: removing that equivalence class containing v from M *) | |
180 | ||
181 | fun remove([], v) = [] | |
182 | | remove((class::rest), v) = | |
183 | if isin(v,class) then rest else class:: remove(rest,v); | |
184 | ||
185 | (* [a]_M, page 168: the equivalence class containing a *) | |
186 | ||
187 | exception ClassOff | |
188 | ||
189 | fun class_of([],a) = raise ClassOff | |
190 | | class_of((class::rest), a) = | |
191 | if isin(a,class) then class else class_of(rest,a); | |
192 | ||
193 | (* [t]^M, page 168: the set of type variables eqivalent to some type variable | |
194 | occurring in non-atomic type t *) | |
195 | ||
196 | fun equiv_tyvars(t,M): ty list = | |
197 | foldr union [] ((map (fn a=> class_of(M,TYVAR a)) (tyvars(t))): ty list list) ; | |
198 | ||
199 | fun transitive_closure(oldsets,newsets) = | |
200 | #2(transClos(op = : ty*ty-> bool)(false)(newsets,oldsets)) | |
201 | ||
202 | (* Coercion sets *) | |
203 | ||
204 | type coercion = ty * ty | |
205 | ||
206 | type coercion_set = coercion list | |
207 | ||
208 | fun on_C(S,C) = map (fn(t1,t2) => (S t1, S t2)) C | |
209 | ||
210 | fun atomic t = | |
211 | case t of | |
212 | INT => true | |
213 | | REAL => true | |
214 | | TYVAR _ => true | |
215 | | _ => false; | |
216 | ||
217 | (* diagonal is used in match to create initial equivalence relation*) | |
218 | ||
219 | ||
220 | fun diagonal(C: coercion_set) = | |
221 | let | |
222 | fun diag(t,acc) = | |
223 | case t of | |
224 | INT => union([INT],acc) | |
225 | | REAL => union([REAL],acc) | |
226 | | PROD(t1,t2) => diag(t1,diag(t2,acc)) | |
227 | | ARROW(t1,t2) => diag(t1,diag(t2,acc)) | |
228 | | TYVAR _ => union([t],acc) | |
229 | ||
230 | fun diag2((t1,t2),acc) = diag(t1,diag(t2,acc)) | |
231 | ||
232 | val atomics = foldr diag2 [] C | |
233 | in | |
234 | map (fn atomic => [atomic,atomic]) atomics | |
235 | end | |
236 | ||
237 | fun ground_atomic t = | |
238 | case t of | |
239 | INT => true | |
240 | | REAL => true | |
241 | | _ => false; | |
242 | ||
243 | fun contains_no_type_constant [] = true | |
244 | | contains_no_type_constant (t::rest) = | |
245 | not (ground_atomic t) andalso contains_no_type_constant rest; | |
246 | ||
247 | exception MATCH | |
248 | ||
249 | local | |
250 | fun match1([]:coercion_set,S:subst,M) = S | |
251 | | match1((t1,t2)::C, S, M) = | |
252 | if atomic t1 andalso atomic t2 then atomicElimination(t1,t2,C,S,M) | |
253 | else if atomic t1 then expansion(t1,t2,C,S,M) | |
254 | else if atomic t2 then expansion(t2,t1,C,S,M) | |
255 | else decomposition(t1,t2,C,S,M) | |
256 | ||
257 | and atomicElimination(t1,t2,C,S,M) = | |
258 | match1(C,S,transitive_closure(M,[[t1,t2]])) | |
259 | ||
260 | and decomposition(ARROW(t1,t2),ARROW(t1',t2'),C,S,M)= | |
261 | match1((t1',t1)::(t2,t2')::C, S, M) | |
262 | | decomposition(PROD(t1,t2),PROD(t1',t2'),C,S,M)= | |
263 | match1((t1,t1')::(t2,t2')::C, S, M) | |
264 | | decomposition(_) = raise MATCH | |
265 | ||
266 | and expansion(t1:ty,t2:ty,C,S,M) = | |
267 | case intersect(class_of(M,t1), equiv_tyvars(t2,M)) (* occurs check *) | |
268 | of | |
269 | []=> if contains_no_type_constant(class_of(M,t1)) | |
270 | then | |
271 | (* not matching of int or real with arrow or prod *) | |
272 | let | |
273 | fun loop([],C,S,M) = match1(C,S,M) | |
274 | | loop((TYVAR alpha)::tyvars, C, S, M) = | |
275 | let val t' = allnew t2 | |
276 | val delta = mk_subst_ty(alpha,t') | |
277 | in | |
278 | loop(tyvars, on_C(delta,C), delta o S, | |
279 | transitive_closure(M,pair(t2,t'))) | |
280 | end | |
281 | | loop((_::tyvars), C, S, M) = | |
282 | (* skip atomic types, that are not variables *) | |
283 | loop(tyvars, C, S, M) | |
284 | in | |
285 | loop(class_of(M,t1),C,S,M) | |
286 | end | |
287 | ||
288 | else (* matching of int or real with arrow or prod *) | |
289 | raise MATCH | |
290 | ||
291 | | _ => (* occurs check failed *) | |
292 | raise MATCH | |
293 | in | |
294 | ||
295 | fun match(C) = match1(C,Id,diagonal C); | |
296 | ||
297 | end | |
298 | ||
299 | (* Type Environments *) | |
300 | ||
301 | type tyenv = (var * ty)list (* no polymorphism! *) | |
302 | ||
303 | (* looking up variables in the type environement *) | |
304 | ||
305 | exception Lookup; | |
306 | ||
307 | fun lookup(i,[]) = raise Lookup | |
308 | | lookup(i,((j,sigma)::rest)) = if i=j then sigma else lookup(i,rest); | |
309 | ||
310 | fun on_tyenv(S:subst,TE:tyenv) = | |
311 | map (fn(i,tau) => (i, S tau)) TE | |
312 | ||
313 | (* pretty printing -- actually not very pretty, but it will do *) | |
314 | ||
315 | (* precedences: -> : 1 | |
316 | * : 2 *) | |
317 | ||
318 | fun pp_ty' (context:int,INT) = "INT" | |
319 | | pp_ty'(_,REAL) = "REAL" | |
320 | | pp_ty'(context,ARROW(ty1, ty2)) = | |
321 | let val s = pp_ty'(2,ty1) ^ "->" ^ | |
322 | pp_ty'(1, ty2) | |
323 | in | |
324 | if context > 1 then "(" ^ s ^ ")" else s | |
325 | end | |
326 | | pp_ty'(context,PROD(ty1, ty2)) = | |
327 | let val s = pp_ty'(3,ty1) ^ "*" ^ pp_ty'(3,ty2) | |
328 | in | |
329 | if context > 2 then "(" ^ s ^ ")" | |
330 | else s | |
331 | end | |
332 | | pp_ty'(context,(TYVAR i)) = "'a" ^ toString i; | |
333 | ||
334 | fun pp_ty ty = pp_ty'(0,ty) | |
335 | ||
336 | local | |
337 | fun filter [] = [] | |
338 | | filter ((x,sigma)::rest) = | |
339 | if isin(x,["fst","snd","floor"]) | |
340 | (* hack to avoid printing of built-in variables fst, snd and floor *) | |
341 | then filter rest | |
342 | else (x,sigma)::filter rest | |
343 | ||
344 | fun pp_tyenv [] = "" | |
345 | | pp_tyenv ([(x,sigma)]) = | |
346 | x ^ ":" ^ pp_ty sigma ^ " " | |
347 | | pp_tyenv ((x,sigma)::rest) = | |
348 | x ^ ":" ^ pp_ty sigma ^ "," ^ pp_tyenv rest; | |
349 | in | |
350 | val pp_tyenv = pp_tyenv o filter | |
351 | end | |
352 | ||
353 | fun pp_coercion(tau1,tau2) = "\n " ^ pp_ty tau1 ^ " |> " ^ pp_ty tau2 | |
354 | ||
355 | fun pp_coercion_set [] = "" | |
356 | | pp_coercion_set[coercion] = pp_coercion coercion | |
357 | | pp_coercion_set(coercion::rest) = | |
358 | pp_coercion coercion ^ ", " ^ pp_coercion_set rest | |
359 | ||
360 | (* | |
361 | end (* local *) | |
362 | end; | |
363 | *) | |
364 | ||
365 | (*structure Expressions = | |
366 | struct | |
367 | local | |
368 | open List Variables | |
369 | in | |
370 | *) datatype exp = VAR of var | |
371 | | INTCON of int | |
372 | | REALCON of real | |
373 | | LAM of var * exp | |
374 | | APP of exp * exp | |
375 | | LET of var * exp * exp | |
376 | | PLUS of exp | |
377 | | MINUS of exp | |
378 | | PAIR of exp * exp; | |
379 | ||
380 | (* pretty printing *) | |
381 | ||
382 | fun pp_exp(VAR x) = x | |
383 | | pp_exp(LAM(x,e')) = "(fn " ^ x ^ " =>" ^ pp_exp e' ^ ")" | |
384 | | pp_exp(APP(e1,e2)) = "(" ^ pp_exp e1 ^ " @ " ^ pp_exp e2 ^ ")" | |
385 | | pp_exp(LET(x,e1,e2)) = "let " ^ x ^ "=" ^ pp_exp e1 ^ " in " ^ pp_exp e2 ^ "end" | |
386 | | pp_exp(INTCON i) = toString i | |
387 | | pp_exp(REALCON r) = toString(floor r) ^ ".?" | |
388 | | pp_exp(PLUS(e1)) = "(+" ^ pp_exp e1 ^ ")" | |
389 | | pp_exp(MINUS(e1)) = "(-" ^ pp_exp e1 ^ ")" | |
390 | | pp_exp(PAIR(e1,e2)) = "(" ^ pp_exp e1 ^ "," ^ pp_exp e2 ^ ")" | |
391 | (* | |
392 | end (* local *) | |
393 | end; | |
394 | *) | |
395 | ||
396 | ||
397 | (*structure TypeChecker= | |
398 | struct | |
399 | local | |
400 | open List Variables Type Expressions | |
401 | in | |
402 | *) | |
403 | type job = tyenv * exp * ty | |
404 | ||
405 | fun TYPE(TE:tyenv,e:exp) : ty * coercion_set = | |
406 | let val alpha0 = fresh_ty() | |
407 | val C = TY([(TE,e,alpha0)],[]) | |
408 | in (alpha0, C) | |
409 | end | |
410 | ||
411 | and TY([]: job list, C: coercion_set)= C | |
412 | | TY((job as (TE,e,tau)) :: rest, C: coercion_set)= | |
413 | case e of | |
414 | VAR x => TY(rest, (lookup(x,TE),tau)::C) | |
415 | | LAM(x,e') => | |
416 | let val (new_ty1,new_ty2) = (fresh_ty(),fresh_ty()); | |
417 | val TE' = (x,(new_ty1))::TE | |
418 | in | |
419 | TY((TE',e',new_ty2)::rest, (ARROW(new_ty1,new_ty2), tau):: C) | |
420 | end | |
421 | | APP(e1,e2) => | |
422 | let val (new_ty1,new_ty2) = (fresh_ty(),fresh_ty()); | |
423 | in | |
424 | TY((TE,e1,ARROW(new_ty1,new_ty2))::(TE,e2,new_ty1)::rest, | |
425 | (new_ty2,tau)::C) | |
426 | end | |
427 | | LET(x,e1,e2) => | |
428 | let val (new_ty1,new_ty2) = (fresh_ty(),fresh_ty()); | |
429 | in | |
430 | TY((TE,e1,new_ty1)::((x,new_ty1)::TE,e2,new_ty2)::rest, | |
431 | (new_ty2,tau)::C) | |
432 | end | |
433 | | INTCON i => TY(rest, (INT, tau):: C) | |
434 | | REALCON i => TY(rest, (REAL, tau):: C) | |
435 | ||
436 | | PLUS e1 => TY((TE,e1, PROD(INT,INT))::rest, (PROD(INT,INT),tau):: C) | |
437 | | MINUS e1 => TY((TE,e1, PROD(INT,INT))::rest, (PROD(INT,INT),tau):: C) | |
438 | | PAIR(e1,e2) => | |
439 | let val (new_ty1,new_ty2) = (fresh_ty(),fresh_ty()); | |
440 | in | |
441 | TY((TE,e1,new_ty1)::(TE,e2,new_ty2)::rest, | |
442 | (PROD(new_ty1,new_ty2),tau)::C) | |
443 | end | |
444 | ||
445 | type judgement = coercion_set * tyenv * exp * ty | |
446 | ||
447 | fun pp_judgement(C,TE,e,tau) = | |
448 | "\nCoersion set: " ^ pp_coercion_set C ^ | |
449 | "\nType environment: " ^ pp_tyenv TE ^ | |
450 | "\nExpression: " ^ pp_exp e ^ | |
451 | "\nType: " ^ pp_ty tau; | |
452 | ||
453 | (* | |
454 | end (* local *) | |
455 | end; | |
456 | *) | |
457 | ||
458 | ||
459 | (*structure Run = | |
460 | struct | |
461 | local | |
462 | open List Variables Type Expressions TypeChecker | |
463 | in | |
464 | *) val e0 = (* let val Id = fn x => x in (Id 3, Id 4.0) end *) | |
465 | let | |
466 | val Id = LAM("x",VAR "x") | |
467 | val pair = PAIR(APP(VAR "Id", INTCON 3), APP(VAR "Id", REALCON 4.0)) | |
468 | in | |
469 | LET("Id",Id, pair) | |
470 | end; | |
471 | ||
472 | val e1 = (* let val makepair = fn x => (x,x) in makepair 3.14 *) | |
473 | let | |
474 | val makepair = LAM("x",PAIR(VAR "x", VAR "x")) | |
475 | in | |
476 | LET("makepair", makepair, APP(VAR "makepair", REALCON 3.14)) | |
477 | end | |
478 | ||
479 | val e2 = (* let fun mappair = fn f => fn x => (f (fst x), f (snd x)) | |
480 | in mappair floor (3.14,2.18) end *) | |
481 | ||
482 | let | |
483 | val mappair = LAM("f",LAM("x", | |
484 | PAIR(APP(VAR "f",APP(VAR "fst", VAR "x")), | |
485 | APP(VAR "f",APP(VAR "snd", VAR "x"))))) | |
486 | in | |
487 | LET("mappair",mappair, APP(APP(VAR "mappair", VAR "floor"), | |
488 | PAIR(REALCON 3.14, REALCON 2.18))) | |
489 | end; | |
490 | ||
491 | val e3 = (* fn x => x *) | |
492 | LAM("x",VAR "x") | |
493 | val e4 = (* fn f => fn x => f x *) | |
494 | LAM("f",LAM("x",APP(VAR "f", VAR "x"))); | |
495 | val e5 = (* fn f => fn x => f(f x) *) | |
496 | LAM("f",LAM("x",APP(VAR "f", APP(VAR "f", VAR "x")))); | |
497 | ||
498 | ||
499 | fun run(e: exp, outfilename: string) = | |
500 | let | |
501 | val _ = r:= 5; (* reset counter for type variables *) | |
502 | val _ = print("\nprocessing " ^ outfilename ^ "...") | |
503 | val TE0 = | |
504 | [("fst", (ARROW(PROD(TYVAR 0,TYVAR 1),TYVAR 0))), (* the type of fst *) | |
505 | ("snd", (ARROW(PROD(TYVAR 0,TYVAR 1),TYVAR 1))), (* the type of snd *) | |
506 | ("floor", (ARROW(REAL,INT)))] (* the type of floor *) | |
507 | val _ = print("running TYPE...") | |
508 | val (ty,C) = TYPE(TE0,e) ; | |
509 | val os = TextIO.openOut outfilename; | |
510 | val _ = TextIO.output(os, "\nResult of TYPE:\n\n\n " ^ pp_judgement(C,TE0,e,ty)); | |
511 | val _ = print("running MATCH...") | |
512 | val S = match C | |
513 | val judgem' as (C',TE',e',ty') = (on_C(S,C),on_tyenv(S,TE0),e,S ty) | |
514 | val _ = TextIO.output(os, "\n\n\nResult of MATCH:\n\n\n " ^ pp_judgement judgem'); | |
515 | in | |
516 | TextIO.closeOut os | |
517 | end; | |
518 | ||
519 | val _ = run(e0,"outFuhMishra0"); | |
520 | val _ = run(e1,"outFuhMishra1"); | |
521 | val _ = run(e2,"outFuhMishra2"); | |
522 | val _ = run(e3,"outFuhMishra3"); | |
523 | val _ = run(e4,"outFuhMishra4"); | |
524 | val _ = run(e5,"outFuhMishra5"); | |
525 | ||
526 | (* | |
527 | end (* local *) | |
528 | end (*struct*); | |
529 | *) | |
530 | ||
531 | val _ = print "\n" |