SCM Repository
Annotation of /sml/trunk/src/compiler/FLINT/kernel/ltykernel.sml
Parent Directory
|
Revision Log
Revision 76 - (view) (download)
1 : | monnier | 16 | (* COPYRIGHT (c) 1997 YALE FLINT PROJECT *) |
2 : | (* ltykernel.sml *) | ||
3 : | |||
4 : | structure LtyKernel :> LTYKERNEL = | ||
5 : | struct | ||
6 : | |||
7 : | monnier | 45 | fun bug s = ErrorMsg.impossible ("LtyKernel:" ^ s) |
8 : | |||
9 : | monnier | 16 | (*************************************************************************** |
10 : | * UTILITY FUNCTIONS FOR HASHCONSING BASICS * | ||
11 : | ***************************************************************************) | ||
12 : | |||
13 : | (** hashconsing implementation basics *) | ||
14 : | local open SortedList | ||
15 : | val MVAL = 10000 | ||
16 : | val BVAL = MVAL * 2 (* all index i start from 0 *) | ||
17 : | in | ||
18 : | |||
19 : | type enc_tvar = int | ||
20 : | league | 53 | fun tvEncode (d, i) = d * MVAL + i |
21 : | fun tvDecode x = ((x div MVAL), (x mod MVAL)) | ||
22 : | monnier | 71 | |
23 : | monnier | 16 | fun exitLevel xs = |
24 : | let fun h ([], x) = rev x | ||
25 : | | h (a::r, x) = if a < BVAL then h(r, x) else h(r, (a-MVAL)::x) | ||
26 : | in h(xs, []) | ||
27 : | end | ||
28 : | |||
29 : | datatype aux_info = AX_REG of bool * enc_tvar list | ||
30 : | | AX_NO | ||
31 : | |||
32 : | val mergeTvs = merge | ||
33 : | val fmergeTvs = foldmerge | ||
34 : | |||
35 : | type 'a hash_cell = (int * 'a * aux_info) ref | ||
36 : | |||
37 : | end (* local of hashconsing implementation basics *) | ||
38 : | |||
39 : | (*************************************************************************** | ||
40 : | * DATATYPE DEFINITIONS * | ||
41 : | ***************************************************************************) | ||
42 : | |||
43 : | (** definition of kinds for all the lambda tycs *) | ||
44 : | datatype tkindI | ||
45 : | = TK_MONO (* ground mono tycon *) | ||
46 : | | TK_BOX (* boxed/tagged tycon *) | ||
47 : | | TK_SEQ of tkind list (* sequence of tycons *) | ||
48 : | monnier | 45 | | TK_FUN of tkind list * tkind (* tycon function *) |
49 : | monnier | 16 | |
50 : | withtype tkind = tkindI hash_cell (* hash-consing-impl of tkind *) | ||
51 : | |||
52 : | (* definitoins of named tyc variables *) | ||
53 : | type tvar = LambdaVar.lvar (* temporary definitions *) | ||
54 : | val mkTvar = LambdaVar.mkLvar | ||
55 : | |||
56 : | monnier | 45 | (* an special extensible token key *) |
57 : | type token = int | ||
58 : | |||
59 : | datatype fflag (* calling conventions *) | ||
60 : | = FF_VAR of bool * bool (* is it fixed ? *) | ||
61 : | | FF_FIXED (* used after rep. analysis *) | ||
62 : | |||
63 : | datatype rflag = RF_TMP (* tuple kind: a template *) | ||
64 : | |||
65 : | (** definitions of lambda type constructors *) | ||
66 : | monnier | 16 | datatype tycI |
67 : | = TC_VAR of DebIndex.index * int (* tyc variables *) | ||
68 : | | TC_NVAR of tvar * DebIndex.depth * int (* named tyc variables *) | ||
69 : | | TC_PRIM of PrimTyc.primtyc (* primitive tyc *) | ||
70 : | |||
71 : | | TC_FN of tkind list * tyc (* tyc abstraction *) | ||
72 : | | TC_APP of tyc * tyc list (* tyc application *) | ||
73 : | | TC_SEQ of tyc list (* tyc sequence *) | ||
74 : | | TC_PROJ of tyc * int (* tyc projection *) | ||
75 : | |||
76 : | | TC_SUM of tyc list (* sum tyc *) | ||
77 : | | TC_FIX of (int * tyc * tyc list) * int (* recursive tyc *) | ||
78 : | |||
79 : | monnier | 45 | | TC_TUPLE of rflag * tyc list (* std record tyc *) |
80 : | | TC_ARROW of fflag * tyc list * tyc list (* std function tyc *) | ||
81 : | monnier | 16 | | TC_PARROW of tyc * tyc (* special fun tyc, not used *) |
82 : | |||
83 : | | TC_BOX of tyc (* boxed tyc *) | ||
84 : | | TC_ABS of tyc (* abstract tyc, not used *) | ||
85 : | monnier | 45 | | TC_TOKEN of token * tyc (* extensible token tyc *) |
86 : | monnier | 16 | | TC_CONT of tyc list (* intern continuation tycon *) |
87 : | | TC_IND of tyc * tycI (* indirect tyc thunk *) | ||
88 : | | TC_ENV of tyc * int * int * tycEnv (* tyc closure *) | ||
89 : | |||
90 : | monnier | 45 | withtype tyc = tycI hash_cell (* hash-consed tyc cell *) |
91 : | and tycEnv = tyc (* | ||
92 : | * This really is (tyc list option * int) list, | ||
93 : | * it is encoded using SEQ[(PROJ(SEQ tcs),i)] | ||
94 : | * and SEQ[(PROJ(VOID, i))]. (ZHONG) | ||
95 : | *) | ||
96 : | |||
97 : | (** definitions of lambda types *) | ||
98 : | datatype ltyI | ||
99 : | monnier | 16 | = LT_TYC of tyc (* monomorphic type *) |
100 : | | LT_STR of lty list (* structure record type *) | ||
101 : | | LT_FCT of lty list * lty list (* functor arrow type *) | ||
102 : | | LT_POLY of tkind list * lty list (* polymorphic type *) | ||
103 : | |||
104 : | | LT_PST of (int * lty) list (* partial-structure type *) | ||
105 : | | LT_CONT of lty list (* internal cont type *) | ||
106 : | | LT_IND of lty * ltyI (* a lty thunk and its sig *) | ||
107 : | | LT_ENV of lty * int * int * tycEnv (* lty closure *) | ||
108 : | |||
109 : | monnier | 45 | withtype lty = ltyI hash_cell (* hash-consed lty cell *) |
110 : | monnier | 16 | |
111 : | monnier | 45 | (*************************************************************************** |
112 : | * TOKEN TYC UTILITY FUNCTIONS * | ||
113 : | ***************************************************************************) | ||
114 : | monnier | 24 | |
115 : | monnier | 45 | type token_info |
116 : | = {name : string, | ||
117 : | abbrev : string, | ||
118 : | reduce_one: token * tyc -> tyc, | ||
119 : | is_whnm : tyc -> bool, | ||
120 : | is_known : token * tyc -> bool} | ||
121 : | monnier | 24 | |
122 : | monnier | 45 | local val token_key = ref 0 |
123 : | val token_table_size = 10 | ||
124 : | val default_token_info = | ||
125 : | {name="TC_GARBAGE", | ||
126 : | abbrev="GB", | ||
127 : | reduce_one=(fn _ => bug "token not implemented"), | ||
128 : | is_whnm=(fn _ => bug "token not implemented"), | ||
129 : | is_known=(fn _ => bug "token not implemented")} | ||
130 : | val token_array : token_info Array.array = | ||
131 : | Array.array(token_table_size,default_token_info) | ||
132 : | val token_validity_table = Array.array(token_table_size,false) | ||
133 : | fun get_next_token () = | ||
134 : | let val n = !token_key | ||
135 : | in if n > token_table_size then bug "running out of tokens" | ||
136 : | else (token_key := n+1; n) | ||
137 : | end | ||
138 : | fun store_token_info (x, k) = Array.update(token_array, k, x) | ||
139 : | fun get_is_whnm k = #is_whnm (Array.sub(token_array, k)) | ||
140 : | fun get_reduce_one (z as (k, t)) = | ||
141 : | (#reduce_one (Array.sub(token_array, k))) z | ||
142 : | fun get_name k = #name (Array.sub(token_array, k)) | ||
143 : | fun get_abbrev k = #abbrev (Array.sub(token_array, k)) | ||
144 : | fun get_is_known (z as (k, t)) = | ||
145 : | (#is_known (Array.sub(token_array, k))) z | ||
146 : | fun is_valid k = Array.sub(token_validity_table, k) | ||
147 : | fun set_valid k = Array.update(token_validity_table, k, true) | ||
148 : | in | ||
149 : | monnier | 24 | |
150 : | monnier | 45 | val register_token: token_info -> token = |
151 : | (fn x => let val k = get_next_token () | ||
152 : | in store_token_info(x, k); set_valid k; k | ||
153 : | end) | ||
154 : | monnier | 24 | |
155 : | monnier | 45 | val token_name : token -> string = get_name |
156 : | val token_abbrev : token -> string = get_abbrev | ||
157 : | val token_whnm : token -> tyc -> bool = get_is_whnm | ||
158 : | val token_reduce : token * tyc -> tyc = get_reduce_one | ||
159 : | val token_isKnown : token * tyc -> bool = get_is_known | ||
160 : | val token_isvalid : token -> bool = is_valid | ||
161 : | val token_eq : token * token -> bool = fn (x,y) => (x=y) | ||
162 : | val token_int : token -> int = fn x => x | ||
163 : | val token_key : int -> token = fn x => x | ||
164 : | |||
165 : | end (* end of all token-related hacks *) | ||
166 : | |||
167 : | monnier | 16 | (*************************************************************************** |
168 : | * HASHCONSING IMPLEMENTATIONS * | ||
169 : | ***************************************************************************) | ||
170 : | |||
171 : | (** Hash-consing implementations of tyc, tkind, lty *) | ||
172 : | |||
173 : | local structure Weak = SMLofNJ.Weak | ||
174 : | structure PT = PrimTyc | ||
175 : | structure DI = DebIndex | ||
176 : | |||
177 : | fun bug msg = ErrorMsg.impossible("LtyKernel: "^msg) | ||
178 : | |||
179 : | val itow = Word.fromInt | ||
180 : | val wtoi = Word.toIntX | ||
181 : | val andb = Word.andb | ||
182 : | |||
183 : | val N = 2048 (* 1024 *) | ||
184 : | val NN = itow (N*N) | ||
185 : | val P = 0w509 (* was 0w1019, a prime < 1024 so that N*N*P < maxint *) | ||
186 : | |||
187 : | val tk_table : tkind Weak.weak list Array.array = Array.array(N,nil) | ||
188 : | val tc_table : tyc Weak.weak list Array.array = Array.array(N,nil) | ||
189 : | val lt_table : lty Weak.weak list Array.array = Array.array(N,nil) | ||
190 : | |||
191 : | fun vector2list v = Vector.foldr (op ::) [] v | ||
192 : | |||
193 : | fun revcat(a::rest,b) = revcat(rest,a::b) | ||
194 : | | revcat(nil,b) = b | ||
195 : | |||
196 : | fun combine [x] = itow x | ||
197 : | | combine (a::rest) = | ||
198 : | andb(itow a +(combine rest)*P, NN - 0w1) | ||
199 : | | combine _ = bug "unexpected case in combine" | ||
200 : | |||
201 : | (* | ||
202 : | * Because of the "cmp" function below, it's necessary to keep | ||
203 : | * each bucket-list in a consistent order, and not reverse | ||
204 : | * or move-to-front or whatever. | ||
205 : | *) | ||
206 : | fun look(table, h, t, eq, mk) = | ||
207 : | let val i = wtoi(andb(itow h, itow(N-1))) | ||
208 : | |||
209 : | fun g(l, z as (w::rest)) = | ||
210 : | (case Weak.strong w | ||
211 : | of SOME (r as ref(h',t',_)) => | ||
212 : | if (h=h') andalso (eq {new=t, old=t'}) | ||
213 : | then (Array.update(table, i, revcat(l,z)); r) | ||
214 : | else g(w::l, rest) | ||
215 : | | NONE => g(l, rest)) | ||
216 : | | g(l, []) = | ||
217 : | let val r = mk(h, t) | ||
218 : | in Array.update(table, i, (Weak.weak r) :: rev l); r | ||
219 : | end | ||
220 : | |||
221 : | in g([], Array.sub(table, i)) | ||
222 : | end | ||
223 : | |||
224 : | fun cmp(table, a as ref(ai,_,_), b as ref (bi,_,_)) = | ||
225 : | if ai < bi then LESS | ||
226 : | else if ai > bi then GREATER | ||
227 : | else if a = b then EQUAL | ||
228 : | else let val index = wtoi (andb(itow ai,itow(N-1))) | ||
229 : | fun g [] = bug "unexpected case in cmp" | ||
230 : | | g (w::rest) = | ||
231 : | (case Weak.strong w | ||
232 : | of SOME r => | ||
233 : | if a=r then LESS | ||
234 : | else if b=r then GREATER | ||
235 : | else g rest | ||
236 : | | NONE => g rest) | ||
237 : | in g(Array.sub(table,index)) | ||
238 : | end | ||
239 : | |||
240 : | |||
241 : | fun getnum (ref(i,_,_)) = i | ||
242 : | fun tagnums nil = nil | ||
243 : | | tagnums ((i,t)::rest) = i::getnum t::tagnums rest | ||
244 : | |||
245 : | fun tk_hash tk = | ||
246 : | let fun g (TK_MONO) = 0w1 | ||
247 : | | g (TK_BOX) = 0w2 | ||
248 : | | g (TK_SEQ ks) = combine (3::map getnum ks) | ||
249 : | monnier | 45 | | g (TK_FUN(ks, k)) = combine (4::getnum k::(map getnum ks)) |
250 : | monnier | 16 | in g tk |
251 : | end | ||
252 : | |||
253 : | fun tc_hash tc = | ||
254 : | let fun g (TC_VAR(d, i)) = combine [1, (DI.di_key d)*10, i] | ||
255 : | | g (TC_NVAR(v, d, i)) = combine[15, v, (DI.dp_key d)*13, i] | ||
256 : | | g (TC_PRIM pt) = combine [2, PT.pt_toint pt] | ||
257 : | | g (TC_FN(ks, t)) = combine (3::(getnum t)::(map getnum ks)) | ||
258 : | | g (TC_APP(t, ts)) = combine (4::(getnum t)::(map getnum ts)) | ||
259 : | | g (TC_SEQ ts) = combine (5::(map getnum ts)) | ||
260 : | | g (TC_PROJ(t, i)) = combine [6, (getnum t), i] | ||
261 : | | g (TC_SUM ts) = combine (7::(map getnum ts)) | ||
262 : | | g (TC_FIX((n, t, ts), i)) = | ||
263 : | combine (8::n::i::(getnum t)::(map getnum ts)) | ||
264 : | | g (TC_ABS t) = combine [9, getnum t] | ||
265 : | | g (TC_BOX t) = combine [10, getnum t] | ||
266 : | monnier | 45 | | g (TC_TUPLE (_, ts)) = combine (11::(map getnum ts)) |
267 : | monnier | 16 | | g (TC_ARROW(rw, ts1, ts2)) = |
268 : | monnier | 45 | let fun h (FF_FIXED) = 10 |
269 : | | h (FF_VAR(true,b2)) = if b2 then 20 else 30 | ||
270 : | | h (FF_VAR(false,b2)) = if b2 then 40 else 50 | ||
271 : | monnier | 16 | in combine (12::(h rw)::(map getnum (ts1@ts2))) |
272 : | end | ||
273 : | | g (TC_PARROW (t1,t2)) = combine [13, getnum t1, getnum t2] | ||
274 : | monnier | 45 | | g (TC_TOKEN (i, tc)) = combine [14, i, getnum tc] |
275 : | | g (TC_CONT ts) = combine (15::(map getnum ts)) | ||
276 : | monnier | 16 | | g (TC_ENV(t,i,j,env)) = |
277 : | monnier | 45 | combine[16, getnum t, i, j, getnum env] |
278 : | monnier | 16 | | g (TC_IND _) = bug "unexpected TC_IND in tc_hash" |
279 : | |||
280 : | in g tc | ||
281 : | end | ||
282 : | |||
283 : | fun lt_hash lt = | ||
284 : | let fun g (LT_TYC t) = combine [1, getnum t] | ||
285 : | | g (LT_STR ts) = combine (2::(map getnum ts)) | ||
286 : | | g (LT_PST ts) = combine (3::(tagnums ts)) | ||
287 : | | g (LT_FCT(ts1, ts2)) = | ||
288 : | combine (4::(map getnum (ts1@ts2))) | ||
289 : | | g (LT_POLY(ks, ts)) = | ||
290 : | combine (5::((map getnum ts)@(map getnum ks))) | ||
291 : | | g (LT_CONT ts) = combine (6::(map getnum ts)) | ||
292 : | | g (LT_ENV(t,i,j,env)) = | ||
293 : | combine [7, getnum t, i, j, getnum env] | ||
294 : | | g (LT_IND _) = bug "unexpected LT_IND in tc_hash" | ||
295 : | in g lt | ||
296 : | end | ||
297 : | |||
298 : | fun tkI_eq {new: tkindI, old} = (new = old) | ||
299 : | |||
300 : | (* the 1st is one being mapped; the 2nd is in the hash table *) | ||
301 : | fun tcI_eq {new : tycI, old=TC_IND(_,s)} = tcI_eq {new=new, old=s} | ||
302 : | | tcI_eq {new, old} = (new=old) | ||
303 : | |||
304 : | fun ltI_eq {new : ltyI, old=LT_IND(_,s)} = ltI_eq {new=new, old=s} | ||
305 : | | ltI_eq {new, old} = (new=old) | ||
306 : | |||
307 : | val baseAux = AX_REG (true, []) | ||
308 : | |||
309 : | fun getAux (ref(i : int, _, x)) = x | ||
310 : | |||
311 : | fun mergeAux(AX_NO, _) = AX_NO | ||
312 : | | mergeAux(_, AX_NO) = AX_NO | ||
313 : | | mergeAux(AX_REG(b1,vs1), AX_REG(b2,vs2)) = | ||
314 : | AX_REG(b2 andalso b1, mergeTvs(vs1, vs2)) | ||
315 : | |||
316 : | fun fsmerge [] = baseAux | ||
317 : | | fsmerge [x] = getAux x | ||
318 : | | fsmerge xs = | ||
319 : | let fun loop([], z) = z | ||
320 : | | loop(_, AX_NO) = AX_NO | ||
321 : | | loop(a::r, z) = loop(r, mergeAux(getAux a, z)) | ||
322 : | in loop(xs, baseAux) | ||
323 : | end | ||
324 : | |||
325 : | fun exitAux(AX_REG(b, vs)) = AX_REG(b, exitLevel vs) | ||
326 : | | exitAux x = x | ||
327 : | |||
328 : | fun tc_aux tc = | ||
329 : | league | 53 | let fun g (TC_VAR(d, i)) = AX_REG(true, [tvEncode(d, i)]) |
330 : | monnier | 45 | | g (TC_NVAR(v, d, i)) = baseAux (*** THIS IS WRONG ! ***) |
331 : | monnier | 16 | | g (TC_PRIM pt) = baseAux |
332 : | | g (TC_APP(ref(_, TC_FN _, AX_NO), _)) = AX_NO | ||
333 : | | g (TC_PROJ(ref(_, TC_SEQ _, AX_NO), _)) = AX_NO | ||
334 : | | g (TC_APP(ref(_, TC_FN _, AX_REG(_,vs)), ts)) = | ||
335 : | mergeAux(AX_REG(false, vs), fsmerge ts) (* ? *) | ||
336 : | | g (TC_PROJ(ref(_, TC_SEQ _, AX_REG(_,vs)), _)) = | ||
337 : | AX_REG(false, vs) (* ? *) | ||
338 : | | g (TC_FN(ks, t)) = exitAux(getAux t) | ||
339 : | | g (TC_APP(t, ts)) = fsmerge (t::ts) | ||
340 : | | g (TC_SEQ ts) = fsmerge ts | ||
341 : | | g (TC_PROJ(t, _)) = getAux t | ||
342 : | | g (TC_SUM ts) = fsmerge ts | ||
343 : | | g (TC_FIX((_,t,ts), _)) = | ||
344 : | let val ax = getAux t | ||
345 : | in case ax | ||
346 : | of AX_REG(_,[]) => mergeAux(ax, fsmerge ts) | ||
347 : | | _ => bug "unexpected TC_FIX freevars in tc_aux" | ||
348 : | end | ||
349 : | | g (TC_ABS t) = getAux t | ||
350 : | | g (TC_BOX t) = getAux t | ||
351 : | monnier | 45 | | g (TC_TUPLE (_, ts)) = fsmerge ts |
352 : | monnier | 16 | | g (TC_ARROW(_, ts1, ts2)) = fsmerge (ts1@ts2) |
353 : | | g (TC_PARROW(t1, t2)) = fsmerge [t1, t2] | ||
354 : | monnier | 45 | | g (TC_TOKEN (k, (ref(_, t, AX_NO)))) = AX_NO |
355 : | | g (TC_TOKEN (k, (x as ref(_, t, AX_REG(b,vs))))) = | ||
356 : | AX_REG((token_whnm k x) andalso b, vs) | ||
357 : | monnier | 16 | | g (TC_CONT ts) = fsmerge ts |
358 : | | g (TC_IND _) = bug "unexpected TC_IND in tc_aux" | ||
359 : | | g (TC_ENV _) = AX_NO | ||
360 : | in g tc | ||
361 : | end | ||
362 : | |||
363 : | fun lt_aux lt = | ||
364 : | let fun g (LT_TYC t) = getAux t | ||
365 : | | g (LT_STR ts) = fsmerge ts | ||
366 : | | g (LT_PST ts) = fsmerge (map #2 ts) | ||
367 : | | g (LT_FCT(ts1, ts2)) = fsmerge (ts1@ts2) | ||
368 : | | g (LT_POLY(ks, ts)) = exitAux(fsmerge ts) | ||
369 : | | g (LT_CONT ts) = fsmerge ts | ||
370 : | | g (LT_IND _) = bug "unexpected LT_IND in lt_aux" | ||
371 : | | g (LT_ENV _) = AX_NO | ||
372 : | in g lt | ||
373 : | end | ||
374 : | |||
375 : | fun tk_mk (i : int, k: tkindI) = ref (i, k, AX_NO) | ||
376 : | fun tc_mk (i : int, tc : tycI) = ref (i, tc, tc_aux tc) | ||
377 : | fun lt_mk (i : int, lt : ltyI) = ref (i, lt, lt_aux lt) | ||
378 : | |||
379 : | in | ||
380 : | |||
381 : | (** a temporary hack on getting the list of free tyvars *) | ||
382 : | fun tc_vs (r as ref(_ : int, _ : tycI, AX_NO)) = NONE | ||
383 : | | tc_vs (r as ref(_ : int, _ : tycI, AX_REG (_,x))) = SOME x | ||
384 : | |||
385 : | fun lt_vs (r as ref(_ : int, _ : ltyI, AX_NO)) = NONE | ||
386 : | | lt_vs (r as ref(_ : int, _ : ltyI, AX_REG (_,x))) = SOME x | ||
387 : | |||
388 : | monnier | 71 | |
389 : | monnier | 16 | (** converting from the hash-consing reps to the standard reps *) |
390 : | fun tk_outX (r as ref(_ : int, t : tkindI, _ : aux_info)) = t | ||
391 : | fun tc_outX (r as ref(_ : int, t : tycI, _ : aux_info)) = t | ||
392 : | fun lt_outX (r as ref(_ : int, t : ltyI, _ : aux_info)) = t | ||
393 : | |||
394 : | |||
395 : | (** converting from the standard reps to the hash-consing reps *) | ||
396 : | fun tk_injX t = look(tk_table, wtoi(tk_hash t), t, tkI_eq, tk_mk) | ||
397 : | fun tc_injX t = look(tc_table, wtoi(tc_hash t), t, tcI_eq, tc_mk) | ||
398 : | fun lt_injX t = look(lt_table, wtoi(lt_hash t), t, ltI_eq, lt_mk) | ||
399 : | |||
400 : | monnier | 71 | |
401 : | monnier | 16 | (** key-comparison on tkind, tyc, lty *) |
402 : | fun tk_cmp (k1, k2) = cmp(tk_table, k1, k2) | ||
403 : | fun tc_cmp (t1, t2) = cmp(tc_table, t1, t2) | ||
404 : | fun lt_cmp (t1, t2) = cmp(lt_table, t1, t2) | ||
405 : | |||
406 : | |||
407 : | (** get the hash key of each lty, only used by reps/coerce.sml; a hack *) | ||
408 : | fun lt_key (ref (h : int, _ : ltyI, _ : aux_info)) = h | ||
409 : | |||
410 : | (*************************************************************************** | ||
411 : | league | 65 | * UTILITY FUNCTIONS ON TKIND ENVIRONMENT * |
412 : | ***************************************************************************) | ||
413 : | (** tkind environment: maps each tyvar, i.e., its debindex, to its kind *) | ||
414 : | type tkindEnv = tkind list list | ||
415 : | |||
416 : | (** utility functions for manipulating the tkindEnv *) | ||
417 : | exception tkUnbound | ||
418 : | val initTkEnv : tkindEnv = [] | ||
419 : | |||
420 : | fun tkLookup (kenv, i, j) = | ||
421 : | let val ks = List.nth(kenv, i-1) handle _ => raise tkUnbound | ||
422 : | in List.nth(ks, j) handle _ => raise tkUnbound | ||
423 : | end | ||
424 : | |||
425 : | fun tkInsert (kenv, ks) = ks::kenv | ||
426 : | |||
427 : | (* strip any unused type variables out of a kenv, given a list of | ||
428 : | * [encoded] free type variables. the result is a "parallel list" of | ||
429 : | * the kinds of those free type variables in the environment. | ||
430 : | * This is meant to use the same representation of a kind environment | ||
431 : | * as in ltybasic. | ||
432 : | * --CALeague | ||
433 : | *) | ||
434 : | fun tkLookupFreeVars (kenv, tyc) = | ||
435 : | let | ||
436 : | fun g (kenv, d, []) = [] | ||
437 : | | g (kenv, d, ftv::ftvs) = | ||
438 : | let val (d', i') = tvDecode ftv | ||
439 : | val kenv' = List.drop (kenv, d'-d) | ||
440 : | handle _ => raise tkUnbound | ||
441 : | val k = List.nth (hd kenv', i') | ||
442 : | handle _ => raise tkUnbound | ||
443 : | val rest = g (kenv', d', ftvs) | ||
444 : | in | ||
445 : | k :: rest | ||
446 : | end | ||
447 : | |||
448 : | fun h ftvs = g (kenv, 1, ftvs) | ||
449 : | in | ||
450 : | Option.map h (tc_vs tyc) | ||
451 : | end | ||
452 : | |||
453 : | (*************************************************************************** | ||
454 : | monnier | 16 | * UTILITY FUNCTIONS ON TYC ENVIRONMENT * |
455 : | ***************************************************************************) | ||
456 : | |||
457 : | (** utility functions for manipulating the tycEnv *) | ||
458 : | local val tc_void = tc_injX(TC_PRIM(PT.ptc_void)) | ||
459 : | monnier | 45 | fun tc_cons (t, b) = tc_injX(TC_ARROW(FF_FIXED, [t],[b])) |
460 : | monnier | 16 | fun tc_interp x = |
461 : | (case tc_outX x | ||
462 : | of TC_PROJ(y, i) => | ||
463 : | (case tc_outX y of TC_SEQ ts => (SOME ts, i) | ||
464 : | | TC_PRIM _ => (NONE, i) | ||
465 : | | _ => bug "unexpected tycEnv1 in tc_interp") | ||
466 : | | _ => bug "unexpected tycEnv2 in tc_interp") | ||
467 : | |||
468 : | fun tc_encode(NONE, i) = tc_injX(TC_PROJ(tc_void,i)) | ||
469 : | | tc_encode(SOME ts, i) = | ||
470 : | tc_injX(TC_PROJ(tc_injX(TC_SEQ(ts)), i)) | ||
471 : | |||
472 : | in | ||
473 : | |||
474 : | exception tcUnbound | ||
475 : | val initTycEnv : tycEnv = tc_void | ||
476 : | |||
477 : | fun tcLookup(i, tenv : tycEnv) = | ||
478 : | if i > 1 then | ||
479 : | (case tc_outX tenv of TC_ARROW(_,_,[x]) => tcLookup(i-1, x) | ||
480 : | | _ => bug "unexpected tycEnv in tcLookup") | ||
481 : | else if i = 1 then | ||
482 : | (case tc_outX tenv of TC_ARROW(_,[x],_) => tc_interp x | ||
483 : | | _ => raise tcUnbound) | ||
484 : | else bug "unexpected argument in tcLookup" | ||
485 : | |||
486 : | fun tcInsert(tenv : tycEnv, et) = tc_cons(tc_encode et, tenv) | ||
487 : | |||
488 : | fun tcSplit(tenv : tycEnv) = | ||
489 : | (case tc_outX tenv of TC_ARROW(_,[x],[y]) => SOME (tc_interp x, y) | ||
490 : | | _ => NONE) | ||
491 : | |||
492 : | |||
493 : | end (* utililty function for tycEnv *) | ||
494 : | |||
495 : | |||
496 : | (** checking if a tyc or an lty is in the normal form *) | ||
497 : | fun tcp_norm ((t as ref (i, _, AX_REG(b,_))) : tyc) = b | ||
498 : | | tcp_norm _ = false | ||
499 : | |||
500 : | fun ltp_norm ((t as ref (i, _, AX_REG(b,_))) : lty) = b | ||
501 : | | ltp_norm _ = false | ||
502 : | |||
503 : | |||
504 : | (** utility functions for tc_env and lt_env *) | ||
505 : | local fun tcc_env_int(x, 0, 0, te) = x | ||
506 : | | tcc_env_int(x, i, j, te) = tc_injX(TC_ENV(x, i, j, te)) | ||
507 : | |||
508 : | fun ltc_env_int(x, 0, 0, te) = x | ||
509 : | | ltc_env_int(x, i, j, te) = lt_injX(LT_ENV(x, i, j, te)) | ||
510 : | |||
511 : | fun withEff ([], ol, nl, tenv) = false | ||
512 : | | withEff (a::r, ol, nl, tenv) = | ||
513 : | league | 53 | let val (i, j) = tvDecode a |
514 : | monnier | 16 | val neweff = |
515 : | if i > ol then (ol <> nl) | ||
516 : | else (* case tcLookup(i, tenv) | ||
517 : | of (NONE, n) => (nl - n) <> i | ||
518 : | | (SOME ts, n) => | ||
519 : | (let val y = List.nth(ts, j) | ||
520 : | in (case tc_outX y | ||
521 : | of TC_VAR(ni, nj) => | ||
522 : | ((nj <> j) orelse ((ni+nl-n) <> i)) | ||
523 : | | _ => true) | ||
524 : | end) *) true | ||
525 : | in neweff orelse (withEff(r, ol, nl, tenv)) | ||
526 : | end | ||
527 : | |||
528 : | in | ||
529 : | |||
530 : | fun tcc_env(x, ol, nl, tenv) = | ||
531 : | let val tvs = tc_vs x | ||
532 : | in case tvs | ||
533 : | of NONE => tcc_env_int(x, ol, nl, tenv) | ||
534 : | | SOME [] => x | ||
535 : | | SOME nvs => if withEff(nvs, ol, nl, tenv) | ||
536 : | then tcc_env_int(x, ol, nl, tenv) | ||
537 : | else x | ||
538 : | end | ||
539 : | |||
540 : | fun ltc_env(x, ol, nl, tenv) = | ||
541 : | let val tvs = lt_vs x | ||
542 : | in case tvs | ||
543 : | of NONE => ltc_env_int(x, ol, nl, tenv) | ||
544 : | | SOME [] => x | ||
545 : | | SOME nvs => if withEff (nvs, ol, nl, tenv) | ||
546 : | then ltc_env_int(x, ol, nl, tenv) | ||
547 : | else x | ||
548 : | end | ||
549 : | |||
550 : | end (* utility functions for lt_env and tc_env *) | ||
551 : | |||
552 : | |||
553 : | (** utility functions for updating tycs and ltys *) | ||
554 : | fun tyc_upd (tgt as ref(i : int, old : tycI, AX_NO), nt) = | ||
555 : | (tgt := (i, TC_IND (nt, old), AX_NO)) | ||
556 : | | tyc_upd (tgt as ref(i : int, old : tycI, x as (AX_REG(false, _))), nt) = | ||
557 : | (tgt := (i, TC_IND (nt, old), x)) | ||
558 : | | tyc_upd _ = bug "unexpected tyc_upd on already normalized tyc" | ||
559 : | |||
560 : | fun lty_upd (tgt as ref(i : int, old : ltyI, AX_NO), nt) = | ||
561 : | (tgt := (i, LT_IND (nt, old), AX_NO)) | ||
562 : | | lty_upd (tgt as ref(i : int, old : ltyI, x as (AX_REG(false, _))), nt) = | ||
563 : | (tgt := (i, LT_IND (nt, old), x)) | ||
564 : | | lty_upd _ = bug "unexpected lty_upd on already normalized lty" | ||
565 : | |||
566 : | (*************************************************************************** | ||
567 : | * UTILITY FUNCTIONS ON REASONING ABOUT REDUCTIONS * | ||
568 : | ***************************************************************************) | ||
569 : | |||
570 : | (** a list of constructor functions *) | ||
571 : | val tcc_var = tc_injX o TC_VAR | ||
572 : | val tcc_fn = tc_injX o TC_FN | ||
573 : | val tcc_app = tc_injX o TC_APP | ||
574 : | val tcc_seq = tc_injX o TC_SEQ | ||
575 : | val tcc_proj = tc_injX o TC_PROJ | ||
576 : | val tcc_fix = tc_injX o TC_FIX | ||
577 : | val tcc_abs = tc_injX o TC_ABS | ||
578 : | monnier | 45 | val tcc_tup = tc_injX o TC_TUPLE |
579 : | val tcc_parw = tc_injX o TC_PARROW | ||
580 : | monnier | 24 | val tcc_box = tc_injX o TC_BOX |
581 : | monnier | 45 | val tcc_real = tc_injX (TC_PRIM PT.ptc_real) |
582 : | monnier | 16 | val ltc_tyc = lt_injX o LT_TYC |
583 : | val ltc_str = lt_injX o LT_STR | ||
584 : | val ltc_pst = lt_injX o LT_PST | ||
585 : | val ltc_fct = lt_injX o LT_FCT | ||
586 : | val ltc_poly = lt_injX o LT_POLY | ||
587 : | monnier | 45 | val tcc_sum = tc_injX o TC_SUM |
588 : | val tcc_token = tc_injX o TC_TOKEN | ||
589 : | monnier | 16 | |
590 : | (** the following function contains the procedure on how to | ||
591 : | monnier | 45 | * flatten the arguments and results of an arbitrary FLINT function |
592 : | monnier | 16 | *) |
593 : | league | 76 | val maxFlat = 5 (* most number of args to flatten *) |
594 : | |||
595 : | monnier | 16 | fun isKnown tc = |
596 : | (case tc_outX(tc_whnm tc) | ||
597 : | of (TC_PRIM _ | TC_ARROW _ | TC_BOX _ | TC_ABS _ | TC_PARROW _) => true | ||
598 : | | (TC_CONT _ | TC_FIX _ | TC_SUM _ | TC_TUPLE _) => true | ||
599 : | | TC_APP(tc, _) => isKnown tc | ||
600 : | | TC_PROJ(tc, _) => isKnown tc | ||
601 : | monnier | 45 | | TC_TOKEN(k, x) => token_isKnown(k, x) |
602 : | monnier | 16 | | _ => false) |
603 : | |||
604 : | and tc_autoflat tc = | ||
605 : | let val ntc = tc_whnm tc | ||
606 : | in (case tc_outX ntc | ||
607 : | monnier | 45 | of TC_TUPLE (_, [_]) => (* singleton record is not flattened to ensure |
608 : | monnier | 16 | isomorphism btw plambdatype and flinttype *) |
609 : | (true, [ntc], false) | ||
610 : | monnier | 71 | | TC_TUPLE (_, []) => (* unit is not flattened to avoid coercions *) |
611 : | (true, [ntc], false) | ||
612 : | monnier | 45 | | TC_TUPLE (_, ts) => |
613 : | league | 76 | if length ts < maxFlat then (true, ts, true) |
614 : | monnier | 45 | else (true, [ntc], false) (* ZHONG added the magic number 10 *) |
615 : | monnier | 16 | | _ => if isKnown ntc then (true, [ntc], false) |
616 : | else (false, [ntc], false)) | ||
617 : | end | ||
618 : | |||
619 : | and tc_autotuple [x] = x | ||
620 : | monnier | 45 | | tc_autotuple xs = |
621 : | league | 76 | if length xs < maxFlat then tcc_tup (RF_TMP, xs) |
622 : | monnier | 45 | else bug "fatal error with tc_autotuple" |
623 : | monnier | 16 | |
624 : | and tcs_autoflat (flag, ts) = | ||
625 : | if flag then (flag, ts) | ||
626 : | else (case ts | ||
627 : | monnier | 45 | of [tc] => (let val ntc = tc_whnm tc |
628 : | val (nraw, ntcs, _) = tc_autoflat ntc | ||
629 : | monnier | 16 | in (nraw, ntcs) |
630 : | end) | ||
631 : | | _ => bug "unexpected cooked multiples in tcs_autoflat") | ||
632 : | |||
633 : | and lt_autoflat lt = | ||
634 : | (case lt_outX(lt_whnm lt) | ||
635 : | of LT_TYC tc => | ||
636 : | let val (raw, ts, flag) = tc_autoflat tc | ||
637 : | in (raw, map ltc_tyc ts, flag) | ||
638 : | end | ||
639 : | | _ => (true, [lt], false)) | ||
640 : | |||
641 : | (** a special version of tcc_arw that does automatic flattening *) | ||
642 : | monnier | 45 | and tcc_arw (x as (FF_FIXED, _, _)) = tc_injX (TC_ARROW x) |
643 : | | tcc_arw (x as (FF_VAR (true, true), _, _)) = tc_injX (TC_ARROW x) | ||
644 : | | tcc_arw (b as (FF_VAR (b1, b2)), ts1, ts2) = | ||
645 : | monnier | 16 | let val (nb1, nts1) = tcs_autoflat (b1, ts1) |
646 : | val (nb2, nts2) = tcs_autoflat (b2, ts2) | ||
647 : | monnier | 45 | in tc_injX (TC_ARROW(FF_VAR(nb1, nb2), nts1, nts2)) |
648 : | monnier | 16 | end |
649 : | |||
650 : | (** utility function to read the top-level of a tyc *) | ||
651 : | and tc_lzrd t = | ||
652 : | let fun g x = | ||
653 : | (case tc_outX x | ||
654 : | of TC_IND (tc, _) => g tc | ||
655 : | | TC_ENV (tc, i, j, te) => | ||
656 : | let val ntc = g(h(tc, i, j, te)) | ||
657 : | in tyc_upd(x, ntc); ntc | ||
658 : | end | ||
659 : | | _ => x) | ||
660 : | |||
661 : | and h (x, 0, 0, _) = g x | ||
662 : | | h (x, ol, nl, tenv) = | ||
663 : | let fun prop z = tcc_env(z, ol, nl, tenv) | ||
664 : | in (case tc_outX x | ||
665 : | of TC_VAR (i,j) => | ||
666 : | if (i <= ol) then | ||
667 : | (let val et = tcLookup(i, tenv) | ||
668 : | in case et | ||
669 : | of (NONE, n) => tcc_var(nl - n, j) | ||
670 : | | (SOME ts, n) => | ||
671 : | (let val y = List.nth(ts, j) | ||
672 : | handle _ => raise tcUnbound | ||
673 : | in h(y, 0, nl - n, initTycEnv) | ||
674 : | end) | ||
675 : | end) | ||
676 : | else tcc_var(i-ol+nl, j) | ||
677 : | | TC_NVAR _ => x | ||
678 : | | TC_PRIM _ => x | ||
679 : | | TC_FN (ks, tc) => | ||
680 : | let val tenv' = tcInsert(tenv, (NONE, nl)) | ||
681 : | in tcc_fn(ks, tcc_env(tc, ol+1, nl+1, tenv')) | ||
682 : | end | ||
683 : | | TC_APP (tc, tcs) => tcc_app(prop tc, map prop tcs) | ||
684 : | | TC_SEQ tcs => tcc_seq (map prop tcs) | ||
685 : | | TC_PROJ (tc, i) => tcc_proj(prop tc, i) | ||
686 : | | TC_SUM tcs => tcc_sum (map prop tcs) | ||
687 : | | TC_FIX ((n,tc,ts), i) => | ||
688 : | tcc_fix((n, prop tc, map prop ts), i) | ||
689 : | | TC_ABS tc => tcc_abs (prop tc) | ||
690 : | | TC_BOX tc => tcc_box (prop tc) | ||
691 : | monnier | 45 | | TC_TUPLE (rk, tcs) => tcc_tup (rk, map prop tcs) |
692 : | monnier | 16 | | TC_ARROW (r, ts1, ts2) => |
693 : | tcc_arw (r, map prop ts1, map prop ts2) | ||
694 : | | TC_PARROW (t1, t2) => tcc_parw (prop t1, prop t2) | ||
695 : | monnier | 45 | | TC_TOKEN (k, t) => tcc_token(k, prop t) |
696 : | monnier | 16 | | TC_CONT _ => bug "unexpected TC_CONT in tc_lzrd" |
697 : | | TC_IND (tc, _) => h(tc, ol, nl, tenv) | ||
698 : | | TC_ENV(tc, ol', nl', tenv') => | ||
699 : | if ol = 0 then h(tc, ol', nl+nl', tenv') | ||
700 : | else h(g x, ol, nl, tenv)) | ||
701 : | end (* function h *) | ||
702 : | in if tcp_norm(t) then t else g t | ||
703 : | end (* function tc_lzrd *) | ||
704 : | |||
705 : | (** utility function to read the top-level of an lty *) | ||
706 : | and lt_lzrd t = | ||
707 : | let fun g x = | ||
708 : | (case lt_outX x | ||
709 : | of LT_IND (lt, _) => g lt | ||
710 : | | LT_ENV(lt, i, j, te) => | ||
711 : | let val nlt = g(h(lt, i, j, te)) | ||
712 : | in lty_upd(x, nlt); nlt | ||
713 : | end | ||
714 : | | _ => x) | ||
715 : | |||
716 : | and h (x, 0, 0, _) = g x | ||
717 : | | h (x, ol, nl, tenv) = | ||
718 : | let fun prop z = ltc_env(z, ol, nl, tenv) | ||
719 : | in (case lt_outX x | ||
720 : | of LT_TYC tc => ltc_tyc (tcc_env(tc, ol, nl, tenv)) | ||
721 : | | LT_STR ts => ltc_str (map prop ts) | ||
722 : | | LT_PST its => ltc_pst (map (fn (i, t) => (i, prop t)) its) | ||
723 : | | LT_FCT (ts1, ts2) => ltc_fct(map prop ts1, map prop ts2) | ||
724 : | | LT_POLY (ks, ts) => | ||
725 : | let val tenv' = tcInsert(tenv, (NONE, nl)) | ||
726 : | in ltc_poly(ks, | ||
727 : | map (fn t => ltc_env(t, ol+1, nl+1, tenv')) ts) | ||
728 : | end | ||
729 : | | LT_CONT _ => bug "unexpected LT_CONT in lt_lzrd" | ||
730 : | | LT_IND (t, _) => h(t, ol, nl, tenv) | ||
731 : | | LT_ENV (lt, ol', nl', tenv') => | ||
732 : | if ol = 0 then h(lt, ol', nl+nl', tenv') | ||
733 : | else h(g x, ol, nl, tenv)) | ||
734 : | end (* function h *) | ||
735 : | in if ltp_norm(t) then t else g t | ||
736 : | end (* function lt_lzrd *) | ||
737 : | |||
738 : | (** taking out the TC_IND indirection *) | ||
739 : | and stripInd t = (case tc_outX t of TC_IND (x,_) => stripInd x | _ => t) | ||
740 : | |||
741 : | (** normalizing an arbitrary tyc into a simple weak-head-normal-form *) | ||
742 : | and tc_whnm t = if tcp_norm(t) then t else | ||
743 : | let val nt = tc_lzrd t | ||
744 : | in case (tc_outX nt) | ||
745 : | of TC_APP(tc, tcs) => | ||
746 : | (let val tc' = tc_whnm tc | ||
747 : | in case (tc_outX tc') | ||
748 : | of TC_FN(ks, b) => | ||
749 : | let fun base () = | ||
750 : | (b, 1, 0, tcInsert(initTycEnv,(SOME tcs, 0))) | ||
751 : | val sp = | ||
752 : | (case tc_outX b | ||
753 : | of TC_ENV(b', ol', nl', te') => | ||
754 : | (case tcSplit te' | ||
755 : | of SOME((NONE, n), te) => | ||
756 : | if (n = nl'-1) andalso (ol' > 0) | ||
757 : | then (b', ol', n, | ||
758 : | tcInsert(te, (SOME tcs, n))) | ||
759 : | else base() | ||
760 : | | _ => base()) | ||
761 : | | _ => base()) | ||
762 : | val res = tc_whnm(tcc_env sp) | ||
763 : | in tyc_upd(nt, res); res | ||
764 : | end | ||
765 : | | ((TC_SEQ _) | (TC_TUPLE _) | (TC_ARROW _) | (TC_IND _)) => | ||
766 : | bug "unexpected tycs in tc_whnm-TC_APP" | ||
767 : | | _ => let val xx = tcc_app(tc', tcs) | ||
768 : | in stripInd xx | ||
769 : | end | ||
770 : | end) | ||
771 : | | TC_PROJ(tc, i) => | ||
772 : | (let val tc' = tc_whnm tc | ||
773 : | in (case (tc_outX tc') | ||
774 : | of (TC_SEQ tcs) => | ||
775 : | let val res = List.nth(tcs, i) | ||
776 : | handle _ => bug "TC_SEQ in tc_whnm" | ||
777 : | val nres = tc_whnm res | ||
778 : | in tyc_upd(nt, nres); nres | ||
779 : | end | ||
780 : | | ((TC_PRIM _) | (TC_NVAR _) | (TC_FIX _) | (TC_FN _) | | ||
781 : | (TC_SUM _) | (TC_ARROW _) | (TC_ABS _) | (TC_BOX _) | | ||
782 : | (TC_IND _) | (TC_TUPLE _)) => | ||
783 : | bug "unexpected tycs in tc_whnm-TC_PROJ" | ||
784 : | | _ => let val xx = tcc_proj(tc', i) | ||
785 : | in stripInd xx | ||
786 : | end) | ||
787 : | end) | ||
788 : | monnier | 45 | | TC_TOKEN(k, tc) => |
789 : | (let val tc' = tc_whnm tc | ||
790 : | in if token_whnm k tc' | ||
791 : | then let val xx = tcc_token(k, tc') in stripInd xx end | ||
792 : | else let val res = token_reduce(k, tc') | ||
793 : | val nres = tc_whnm res | ||
794 : | in tyc_upd(nt, nres); nres | ||
795 : | end | ||
796 : | end) | ||
797 : | monnier | 16 | | TC_IND (tc, _) => tc_whnm tc |
798 : | | TC_ENV _ => bug "unexpected TC_ENV in tc_whnm" | ||
799 : | | _ => nt | ||
800 : | end (* function tc_whnm *) | ||
801 : | |||
802 : | (** normalizing an arbitrary lty into the simple weak-head-normal-form *) | ||
803 : | and lt_whnm t = if ltp_norm(t) then t else | ||
804 : | let val nt = lt_lzrd t | ||
805 : | in case (lt_outX nt) | ||
806 : | of LT_TYC tc => ltc_tyc(tc_whnm tc) | ||
807 : | | _ => nt | ||
808 : | end (* function lt_whnm *) | ||
809 : | |||
810 : | (** normalizing an arbitrary tyc into the standard normal form *) | ||
811 : | fun tc_norm t = if (tcp_norm t) then t else | ||
812 : | let val nt = tc_whnm t | ||
813 : | in if (tcp_norm nt) then nt | ||
814 : | else | ||
815 : | (let val res = | ||
816 : | (case (tc_outX nt) | ||
817 : | of TC_FN (ks, tc) => tcc_fn(ks, tc_norm tc) | ||
818 : | | TC_APP (tc, tcs) => | ||
819 : | tcc_app(tc_norm tc, map tc_norm tcs) | ||
820 : | | TC_SEQ tcs => tcc_seq(map tc_norm tcs) | ||
821 : | | TC_PROJ (tc, i) => tcc_proj(tc_norm tc, i) | ||
822 : | | TC_SUM tcs => tcc_sum (map tc_norm tcs) | ||
823 : | | TC_FIX ((n,tc,ts), i) => | ||
824 : | tcc_fix((n, tc_norm tc, map tc_norm ts), i) | ||
825 : | | TC_ABS tc => tcc_abs(tc_norm tc) | ||
826 : | | TC_BOX tc => tcc_box(tc_norm tc) | ||
827 : | monnier | 45 | | TC_TUPLE (rk, tcs) => tcc_tup(rk, map tc_norm tcs) |
828 : | monnier | 16 | | TC_ARROW (r, ts1, ts2) => |
829 : | tcc_arw(r, map tc_norm ts1, map tc_norm ts2) | ||
830 : | | TC_PARROW (t1, t2) => tcc_parw(tc_norm t1, tc_norm t2) | ||
831 : | monnier | 45 | | TC_TOKEN (k, t) => tcc_token(k, tc_norm t) |
832 : | monnier | 16 | | TC_IND (tc, _) => tc_norm tc |
833 : | | TC_ENV _ => bug "unexpected tycs in tc_norm" | ||
834 : | | _ => nt) | ||
835 : | in tyc_upd(nt, res); res | ||
836 : | end) | ||
837 : | end (* function tc_norm *) | ||
838 : | |||
839 : | (** normalizing an arbitrary lty into the standard normal form *) | ||
840 : | fun lt_norm t = if (ltp_norm t) then t else | ||
841 : | let val nt = lt_lzrd t | ||
842 : | in if (ltp_norm nt) then nt | ||
843 : | else | ||
844 : | (let val res = | ||
845 : | (case lt_outX nt | ||
846 : | of LT_TYC tc => ltc_tyc(tc_norm tc) | ||
847 : | | LT_STR ts => ltc_str(map lt_norm ts) | ||
848 : | | LT_PST its => | ||
849 : | ltc_pst(map (fn (i, t) => (i, lt_norm t)) its) | ||
850 : | | LT_FCT (ts1, ts2) => | ||
851 : | ltc_fct(map lt_norm ts1, map lt_norm ts2) | ||
852 : | | LT_POLY (ks, ts) => ltc_poly (ks, map lt_norm ts) | ||
853 : | | LT_IND (lt, _) => lt_norm lt | ||
854 : | | _ => bug "unexpected ltys in lt_norm") | ||
855 : | in lty_upd(nt, res); res | ||
856 : | end) | ||
857 : | end (* function lt_norm *) | ||
858 : | |||
859 : | (*************************************************************************** | ||
860 : | monnier | 45 | * REGISTER A NEW TOKEN TYC --- TC_WRAP * |
861 : | ***************************************************************************) | ||
862 : | |||
863 : | (** we add a new constructor named TC_RBOX through the token facility *) | ||
864 : | local val name = "TC_WRAP" | ||
865 : | val abbrev = "WR" | ||
866 : | val is_known = fn _ => true (* why is this ? *) | ||
867 : | fun tcc_tok k t = tcc_token(k, t) | ||
868 : | |||
869 : | fun unknown tc = | ||
870 : | (case tc_outX tc | ||
871 : | of (TC_VAR _ | TC_NVAR _) => true | ||
872 : | | (TC_APP(tc, _)) => unknown tc | ||
873 : | | (TC_PROJ(tc, _)) => unknown tc | ||
874 : | | _ => false) | ||
875 : | |||
876 : | fun flex_tuple ts = | ||
877 : | let fun hhh(x::r, ukn, wfree) = | ||
878 : | let fun iswp tc = | ||
879 : | (case tc_outX tc | ||
880 : | of TC_TOKEN(k', t) => (* WARNING: need check k' *) | ||
881 : | (case tc_outX t | ||
882 : | of TC_PRIM pt => false | ||
883 : | | _ => true) | ||
884 : | | _ => true) | ||
885 : | in hhh(r, (unknown x) orelse ukn, (iswp x) andalso wfree) | ||
886 : | end | ||
887 : | | hhh([], ukn, wfree) = ukn andalso wfree | ||
888 : | in hhh(ts, false, true) | ||
889 : | end | ||
890 : | |||
891 : | fun is_whnm tc = | ||
892 : | (case tc_outX tc | ||
893 : | of (TC_ARROW(FF_FIXED, [t], _)) => (unknown t) | ||
894 : | | (TC_TUPLE(rf, ts)) => flex_tuple ts | ||
895 : | | (TC_PRIM pt) => PT.unboxed pt | ||
896 : | | _ => false) | ||
897 : | |||
898 : | (* invariants: tc itself is in whnm but is_whnm tc = false *) | ||
899 : | fun reduce_one (k, tc) = | ||
900 : | (case tc_outX tc | ||
901 : | of TC_TUPLE (rk, ts) => | ||
902 : | let fun hhh (x::r, nts, ukn) = | ||
903 : | let val nx = tc_whnm x | ||
904 : | val b1 = unknown nx | ||
905 : | val nnx = | ||
906 : | (case tc_outX nx | ||
907 : | of TC_TOKEN(k', t) => | ||
908 : | if token_eq(k, k') then | ||
909 : | (case tc_outX t | ||
910 : | of TC_PRIM _ => t | ||
911 : | | _ => nx) | ||
912 : | else nx | ||
913 : | | _ => nx) | ||
914 : | in hhh(r, nnx::nts, b1 orelse ukn) | ||
915 : | end | ||
916 : | | hhh ([], nts, ukn) = | ||
917 : | let val nt = tcc_tup(rk, rev nts) | ||
918 : | in if ukn then tcc_token(k, nt) else nt | ||
919 : | end | ||
920 : | in hhh(ts, [], false) | ||
921 : | end | ||
922 : | | TC_ARROW (FF_FIXED, [_,_], [_]) => tc | ||
923 : | | TC_ARROW (FF_FIXED, [t1], ts2 as [_]) => | ||
924 : | let val nt1 = tc_whnm t1 | ||
925 : | fun ggg z = | ||
926 : | let val nz = tc_whnm z | ||
927 : | in (case tc_outX nz | ||
928 : | of TC_PRIM pt => | ||
929 : | if PT.unboxed pt then tcc_token(k, nz) | ||
930 : | else nz | ||
931 : | | _ => nz) | ||
932 : | end | ||
933 : | val (wp, nts1) = | ||
934 : | (case tc_outX nt1 | ||
935 : | of TC_TUPLE(_, [x,y]) => (false, [ggg x, ggg y]) | ||
936 : | | TC_TOKEN(k', x) => | ||
937 : | if token_eq(k, k') then | ||
938 : | (case (tc_outX x) | ||
939 : | of TC_TUPLE(_, [y, z]) => | ||
940 : | (false, [ggg y, ggg z]) | ||
941 : | monnier | 71 | | _ => (false, [nt1])) |
942 : | monnier | 45 | else (false, [nt1]) |
943 : | | _ => (unknown nt1, [nt1])) | ||
944 : | val nt = tcc_arw(FF_FIXED, nts1, ts2) | ||
945 : | in if wp then tcc_token(k, nt) else nt | ||
946 : | end | ||
947 : | | TC_ARROW (FF_FIXED, _, _) => | ||
948 : | bug "unexpected reduce_one on ill-formed FF_FIX arrow types" | ||
949 : | | TC_ARROW (FF_VAR(b1,b2), ts1, ts2) => | ||
950 : | bug "calling reduce_one on FF_VAR arrow types" | ||
951 : | | TC_PRIM pt => | ||
952 : | if PT.unboxed pt then | ||
953 : | bug "calling reduce_one on an already-reduced whnm" | ||
954 : | else tc | ||
955 : | | TC_TOKEN(k', t) => | ||
956 : | if token_eq(k, k') then tc | ||
957 : | else bug "unexpected token in reduce_one" | ||
958 : | | (TC_BOX _ | TC_ABS _ | TC_PARROW _) => | ||
959 : | bug "unexpected tc_box/abs/parrow in reduce_one" | ||
960 : | | TC_ENV _ => bug "unexpected TC_ENV in reduce_one" | ||
961 : | | TC_IND _ => bug "unexpected TC_IND in reduce_one" | ||
962 : | | _ => tc) | ||
963 : | |||
964 : | in | ||
965 : | |||
966 : | val wrap_token = | ||
967 : | register_token {name=name, abbrev=abbrev, reduce_one=reduce_one, | ||
968 : | is_whnm=is_whnm, is_known=is_known} | ||
969 : | |||
970 : | end (* end of creating the box token for "tcc_rbox" *) | ||
971 : | |||
972 : | (** testing if a tyc is a unknown constructor *) | ||
973 : | fun tc_unknown tc = not (isKnown tc) | ||
974 : | |||
975 : | (*************************************************************************** | ||
976 : | monnier | 16 | * REBINDING THE INJECTION AND PROJECTION FUNCTIONS * |
977 : | ***************************************************************************) | ||
978 : | (** converting from the standard reps to the hash-consing reps *) | ||
979 : | val tk_inj = tk_injX | ||
980 : | val tc_inj = tc_injX | ||
981 : | val lt_inj = lt_injX | ||
982 : | |||
983 : | (** converting from the hash-consing reps to the standard reps *) | ||
984 : | val tk_out = tk_outX | ||
985 : | val tc_out = tc_outX o tc_whnm | ||
986 : | val lt_out = lt_outX o lt_whnm | ||
987 : | |||
988 : | (*************************************************************************** | ||
989 : | * UTILITY FUNCTIONS ON TESTING EQUIVALENCE * | ||
990 : | ***************************************************************************) | ||
991 : | |||
992 : | (** testing the equality of values of tkind, tyc, lty *) | ||
993 : | league | 60 | fun eqlist p (x::xs, y::ys) = (p(x,y)) andalso (eqlist p (xs, ys)) |
994 : | | eqlist p ([], []) = true | ||
995 : | | eqlist _ _ = false | ||
996 : | monnier | 71 | |
997 : | monnier | 16 | (** testing the "pointer" equality on normalized tkind, tyc, and lty *) |
998 : | fun tk_eq (x: tkind, y) = (x = y) | ||
999 : | fun tc_eq (x: tyc, y) = (x = y) | ||
1000 : | fun lt_eq (x: lty, y) = (x = y) | ||
1001 : | |||
1002 : | (** testing the equivalence for arbitrary tkinds, tycs and ltys *) | ||
1003 : | val tk_eqv = tk_eq (* all tkinds are normalized *) | ||
1004 : | |||
1005 : | league | 60 | local (* tyc equivalence utilities *) |
1006 : | (* The efficiency of checking FIX equivalence could probably be | ||
1007 : | * improved somewhat, but it doesn't seem so bad for my purposes right | ||
1008 : | * now. Anyway, somebody might eventually want to do some profiling | ||
1009 : | * and improve this. --league, 24 March 1998 | ||
1010 : | *) | ||
1011 : | |||
1012 : | (* Profiling code, temporary?? *) | ||
1013 : | structure Click = | ||
1014 : | struct | ||
1015 : | local | ||
1016 : | val s_unroll = Stats.makeStat "FIX unrolls" | ||
1017 : | in | ||
1018 : | fun unroll() = Stats.addStat s_unroll 1 | ||
1019 : | end | ||
1020 : | end (* Click *) | ||
1021 : | monnier | 16 | |
1022 : | league | 60 | (** unrolling a fix, tyc -> tyc *) |
1023 : | fun tc_unroll_fix tyc = | ||
1024 : | case tc_outX tyc of | ||
1025 : | (TC_FIX((n,tc,ts),i)) => let | ||
1026 : | fun genfix i = tcc_fix ((n,tc,ts),i) | ||
1027 : | val fixes = List.tabulate(n, genfix) | ||
1028 : | val mu = tc | ||
1029 : | val mu = if null ts then mu | ||
1030 : | else tcc_app (mu,ts) | ||
1031 : | val mu = tcc_app (mu, fixes) | ||
1032 : | val mu = if n=1 then mu | ||
1033 : | else tcc_proj (mu, i) | ||
1034 : | in | ||
1035 : | Click.unroll(); | ||
1036 : | mu | ||
1037 : | end | ||
1038 : | | _ => bug "unexpected non-FIX in tc_unroll_fix" | ||
1039 : | monnier | 16 | |
1040 : | league | 60 | (* In order to check equality of two FIXes, we need to be able to |
1041 : | * unroll them once, and check equality on the unrolled version, with | ||
1042 : | * an inductive assumption that they ARE equal. The following code | ||
1043 : | * supports making and checking these inductive assumptions. | ||
1044 : | * Furthermore, we need to avoid unrolling any FIX more than once. | ||
1045 : | *) | ||
1046 : | structure TcDict = BinaryDict | ||
1047 : | (struct | ||
1048 : | type ord_key = tyc | ||
1049 : | val cmpKey = tc_cmp | ||
1050 : | end) | ||
1051 : | (* for each tyc in this dictionary, we store a dictionary containing | ||
1052 : | * tycs that are assumed equivalent to it. | ||
1053 : | *) | ||
1054 : | type eqclass = unit TcDict.dict | ||
1055 : | type hyp = eqclass TcDict.dict | ||
1056 : | |||
1057 : | (* the null hypothesis, no assumptions about equality *) | ||
1058 : | val empty_eqclass : eqclass = TcDict.mkDict() | ||
1059 : | val null_hyp : hyp = TcDict.mkDict() | ||
1060 : | |||
1061 : | (* add assumption t1=t2 to current hypothesis. returns composite | ||
1062 : | * hypothesis. | ||
1063 : | *) | ||
1064 : | fun assume_eq' (hyp, t1, t1eqOpt, t2) = let | ||
1065 : | val t1eq = case t1eqOpt of SOME e => e | NONE => empty_eqclass | ||
1066 : | val t1eq' = TcDict.insert (t1eq, t2, ()) | ||
1067 : | val hyp' = TcDict.insert (hyp, t1, t1eq') | ||
1068 : | in | ||
1069 : | hyp' | ||
1070 : | end | ||
1071 : | |||
1072 : | fun assume_eq (hyp, t1, t1eqOpt, t2, t2eqOpt) = | ||
1073 : | assume_eq' (assume_eq' (hyp, t1, t1eqOpt, t2), | ||
1074 : | t2, t2eqOpt, t1) | ||
1075 : | |||
1076 : | (* check whether t1=t2 according to the hypothesis *) | ||
1077 : | val eq_by_hyp : eqclass option * tyc -> bool | ||
1078 : | = fn (NONE, t2) => false | ||
1079 : | | (SOME eqclass, t2) => | ||
1080 : | isSome (TcDict.peek (eqclass, t2)) | ||
1081 : | |||
1082 : | (* have we made any assumptions about `t' already? *) | ||
1083 : | val visited : eqclass option -> bool | ||
1084 : | = isSome | ||
1085 : | |||
1086 : | monnier | 71 | (* testing if two recursive datatypes are equivalent *) |
1087 : | fun eq_fix (eqop1, hyp) (t1, t2) = | ||
1088 : | (case (tc_outX t1, tc_outX t2) | ||
1089 : | of (TC_FIX((n1,tc1,ts1),i1), TC_FIX((n2,tc2,ts2),i2)) => | ||
1090 : | league | 60 | if not (!Control.CG.checkDatatypes) then true |
1091 : | else let | ||
1092 : | val t1eqOpt = TcDict.peek (hyp, t1) | ||
1093 : | in | ||
1094 : | (* first check the induction hypothesis. we only ever | ||
1095 : | * make hypotheses about FIX nodes, so this test is okay | ||
1096 : | * here. if assume_eq appears in other cases, this | ||
1097 : | * test should be lifted outside the switch. | ||
1098 : | *) | ||
1099 : | if eq_by_hyp (t1eqOpt, t2) then true | ||
1100 : | (* next try structural eq on the components. i'm not sure why | ||
1101 : | * this part is necessary, but it does seem to be... --league, | ||
1102 : | * 23 March 1998 | ||
1103 : | *) | ||
1104 : | else | ||
1105 : | (n1 = n2 andalso i1 = i2 andalso | ||
1106 : | eqop1 hyp (tc1, tc2) andalso | ||
1107 : | monnier | 71 | eqlist (eqop1 hyp) (ts1, ts2)) orelse |
1108 : | league | 60 | (* not equal by inspection; we have to unroll it. |
1109 : | * we prevent unrolling the same FIX twice by asking | ||
1110 : | * the `visited' function. | ||
1111 : | *) | ||
1112 : | if visited t1eqOpt then false | ||
1113 : | else let | ||
1114 : | val t2eqOpt = TcDict.peek (hyp, t2) | ||
1115 : | in | ||
1116 : | if visited t2eqOpt then false | ||
1117 : | else eqop1 (assume_eq (hyp, t1, t1eqOpt, | ||
1118 : | t2, t2eqOpt)) | ||
1119 : | (tc_unroll_fix t1, tc_unroll_fix t2) | ||
1120 : | end | ||
1121 : | end | ||
1122 : | monnier | 71 | | _ => bug "unexpected types in eq_fix") |
1123 : | |||
1124 : | |||
1125 : | (* tc_eqv_generator, invariant: t1 and t2 are in the wh-normal form | ||
1126 : | * eqop1 is the default equality to be used for tycs | ||
1127 : | * eqop2 is used for body of FN, arguments in APP, | ||
1128 : | * eqop3 is used for ABS and BOX. | ||
1129 : | * eqop4 is used for arrow arguments and results | ||
1130 : | * Each of these first takes the set of hypotheses. | ||
1131 : | *) | ||
1132 : | fun tc_eqv_gen (eqop1, eqop2, hyp) (t1, t2) = | ||
1133 : | case (tc_outX t1, tc_outX t2) of | ||
1134 : | (TC_FIX _, TC_FIX _) => eqop2 (eqop1, hyp) (t1, t2) | ||
1135 : | league | 60 | | (TC_FN(ks1, b1), TC_FN(ks2, b2)) => |
1136 : | monnier | 71 | eqlist tk_eqv (ks1, ks2) andalso eqop1 hyp (b1, b2) |
1137 : | league | 60 | | (TC_APP(a1, b1), TC_APP(a2, b2)) => |
1138 : | monnier | 71 | eqop1 hyp (a1, a2) andalso eqlist (eqop1 hyp) (b1, b2) |
1139 : | league | 60 | | (TC_SEQ ts1, TC_SEQ ts2) => |
1140 : | eqlist (eqop1 hyp) (ts1, ts2) | ||
1141 : | | (TC_SUM ts1, TC_SUM ts2) => | ||
1142 : | eqlist (eqop1 hyp) (ts1, ts2) | ||
1143 : | | (TC_TUPLE (_, ts1), TC_TUPLE (_, ts2)) => | ||
1144 : | eqlist (eqop1 hyp) (ts1, ts2) | ||
1145 : | | (TC_ABS a, TC_ABS b) => | ||
1146 : | eqop1 hyp (a, b) | ||
1147 : | | (TC_BOX a, TC_BOX b) => | ||
1148 : | eqop1 hyp (a, b) | ||
1149 : | | (TC_TOKEN(k1,t1), TC_TOKEN(k2,t2)) => | ||
1150 : | token_eq(k1,k2) andalso eqop1 hyp (t1,t2) | ||
1151 : | | (TC_PROJ(a1, i1), TC_PROJ(a2, i2)) => | ||
1152 : | i1 = i2 andalso eqop1 hyp (a1, a2) | ||
1153 : | | (TC_ARROW(r1, a1, b1), TC_ARROW(r2, a2, b2)) => | ||
1154 : | monnier | 71 | r1 = r2 andalso eqlist (eqop1 hyp) (a1, a2) |
1155 : | andalso eqlist (eqop1 hyp) (b1, b2) | ||
1156 : | league | 60 | | (TC_PARROW(a1, b1), TC_PARROW(a2, b2)) => |
1157 : | eqop1 hyp (a1, a2) andalso eqop1 hyp (b1, b2) | ||
1158 : | | (TC_CONT ts1, TC_CONT ts2) => | ||
1159 : | eqlist (eqop1 hyp) (ts1, ts2) | ||
1160 : | | _ => false | ||
1161 : | |||
1162 : | (** general equality for tycs *) | ||
1163 : | fun tc_eqv' hyp (x as ref (_, _, AX_REG(true, _)), | ||
1164 : | y as ref (_, _, AX_REG(true, _))) = tc_eq(x,y) | ||
1165 : | | tc_eqv' hyp (x, y) = let | ||
1166 : | val t1 = tc_whnm x | ||
1167 : | val t2 = tc_whnm y | ||
1168 : | in | ||
1169 : | if tcp_norm t1 andalso tcp_norm t2 then tc_eq (t1, t2) | ||
1170 : | else | ||
1171 : | monnier | 71 | tc_eqv_gen (tc_eqv', fn _ => tc_eq, hyp) (t1, t2) |
1172 : | league | 60 | end (* tc_eqv' *) |
1173 : | |||
1174 : | (* slightly relaxed constraints (???) *) | ||
1175 : | fun tc_eqv_x' hyp (x, y) = | ||
1176 : | monnier | 45 | let val t1 = tc_whnm x |
1177 : | val t2 = tc_whnm y | ||
1178 : | in (if (tcp_norm t1) andalso (tcp_norm t2) then tc_eq(t1, t2) | ||
1179 : | else false) orelse | ||
1180 : | monnier | 71 | (tc_eqv_gen (tc_eqv_x', eq_fix, hyp) (t1, t2)) |
1181 : | monnier | 45 | end (* function tc_eqv_x *) |
1182 : | |||
1183 : | league | 60 | in (* tyc equivalence utilities *) |
1184 : | |||
1185 : | val tc_eqv = tc_eqv' null_hyp | ||
1186 : | val tc_eqv_x = tc_eqv_x' null_hyp | ||
1187 : | monnier | 16 | |
1188 : | league | 60 | end (* tyc equivalence utilities *) |
1189 : | |||
1190 : | monnier | 71 | (* |
1191 : | * all the complexity of lt_eqv comes from the partial-structure (or | ||
1192 : | * partial record) type (the LT_PST type). If we can remove LT_PST | ||
1193 : | * type, then the following can be considerabily simplified. (ZHONG) | ||
1194 : | *) | ||
1195 : | |||
1196 : | monnier | 16 | (** lt_eqv_generator, invariant: x and y are in the wh-normal form *) |
1197 : | fun lt_eqv_gen (eqop1, eqop2) (x : lty, y) = | ||
1198 : | let fun sp (r, []) = true | ||
1199 : | | sp (r, (i,t)::s) = | ||
1200 : | (if (eqop1(List.nth(r,i),t)) | ||
1201 : | then sp(r,s) else false) handle _ => false | ||
1202 : | |||
1203 : | fun pp ([], _) = true | ||
1204 : | | pp (_, []) = true | ||
1205 : | | pp (a as ((i,t)::l), b as ((j,s)::r)) = | ||
1206 : | if i > j then pp(a,r) | ||
1207 : | else if i < j then pp(l,b) | ||
1208 : | else if (eqop1(t,s)) then pp(l,r) else false | ||
1209 : | |||
1210 : | (* seq should be called if t1 and t2 are weak-head normal form *) | ||
1211 : | fun seq (t1, t2) = | ||
1212 : | (case (lt_outX t1, lt_outX t2) | ||
1213 : | of (LT_POLY(ks1, b1), LT_POLY(ks2, b2)) => | ||
1214 : | league | 60 | (eqlist tk_eqv (ks1, ks2)) andalso (eqlist eqop1 (b1, b2)) |
1215 : | monnier | 16 | | (LT_FCT(as1, bs1), LT_FCT(as2, bs2)) => |
1216 : | league | 60 | (eqlist eqop1 (as1, as2)) andalso (eqlist eqop1 (bs1, bs2)) |
1217 : | monnier | 16 | | (LT_TYC a, LT_TYC b) => eqop2(a, b) |
1218 : | league | 60 | | (LT_STR s1, LT_STR s2) => eqlist eqop1 (s1, s2) |
1219 : | monnier | 16 | | (LT_PST s1, LT_PST s2) => pp(s1, s2) |
1220 : | | (LT_PST s1, LT_STR s2) => sp(s2, s1) | ||
1221 : | | (LT_STR s1, LT_PST s2) => sp(s1, s2) | ||
1222 : | league | 60 | | (LT_CONT s1, LT_CONT s2) => eqlist eqop1 (s1, s2) |
1223 : | monnier | 16 | | _ => false) |
1224 : | in seq(x, y) | ||
1225 : | end (* function lt_eqv_gen *) | ||
1226 : | |||
1227 : | fun lt_eqv(x : lty, y) = | ||
1228 : | let val seq = lt_eqv_gen (lt_eqv, tc_eqv) | ||
1229 : | monnier | 45 | in if ((ltp_norm x) andalso (ltp_norm y)) then |
1230 : | (lt_eq(x, y)) orelse (seq(x, y)) | ||
1231 : | monnier | 16 | else (let val t1 = lt_whnm x |
1232 : | val t2 = lt_whnm y | ||
1233 : | in if (ltp_norm t1) andalso (ltp_norm t2) then | ||
1234 : | monnier | 45 | (lt_eq(t1, t2)) orelse (seq(t1, t2)) |
1235 : | monnier | 16 | else seq(t1, t2) |
1236 : | end) | ||
1237 : | end (* function lt_eqv *) | ||
1238 : | |||
1239 : | monnier | 45 | fun lt_eqv_x(x : lty, y) = |
1240 : | let val seq = lt_eqv_gen (lt_eqv_x, tc_eqv_x) | ||
1241 : | in if ((ltp_norm x) andalso (ltp_norm y)) then | ||
1242 : | (lt_eq(x, y)) orelse (seq(x, y)) | ||
1243 : | else (let val t1 = lt_whnm x | ||
1244 : | val t2 = lt_whnm y | ||
1245 : | in if (ltp_norm t1) andalso (ltp_norm t2) then | ||
1246 : | (lt_eq(t1, t2)) orelse (seq(t1, t2)) | ||
1247 : | else seq(t1, t2) | ||
1248 : | end) | ||
1249 : | end (* function lt_eqv *) | ||
1250 : | |||
1251 : | (** testing equivalence of fflags and rflags *) | ||
1252 : | val ff_eqv : fflag * fflag -> bool = (op =) | ||
1253 : | val rf_eqv : rflag * rflag -> bool = (op =) | ||
1254 : | |||
1255 : | (*************************************************************************** | ||
1256 : | * UTILITY FUNCTIONS ON FINDING OUT THE DEPTH OF THE FREE TYC VARIABLES * | ||
1257 : | ***************************************************************************) | ||
1258 : | (** finding out the innermost binding depth for a tyc's free variables *) | ||
1259 : | fun tc_depth (x, d) = | ||
1260 : | let val tvs = tc_vs (tc_norm x) | ||
1261 : | (* unfortunately we have to reduce everything to the normal form | ||
1262 : | before we can talk about its list of free type variables. | ||
1263 : | *) | ||
1264 : | in case tvs | ||
1265 : | of NONE => bug "unexpected case in tc_depth" | ||
1266 : | | SOME [] => DI.top | ||
1267 : | league | 53 | | SOME (a::_) => d + 1 - (#1(tvDecode a)) |
1268 : | monnier | 45 | end |
1269 : | |||
1270 : | fun tcs_depth ([], d) = DI.top | ||
1271 : | | tcs_depth (x::r, d) = Int.max(tc_depth(x, d), tcs_depth(r, d)) | ||
1272 : | |||
1273 : | monnier | 16 | end (* toplevel local *) |
1274 : | end (* abstraction LtyKernel *) | ||
1275 : |
root@smlnj-gforge.cs.uchicago.edu | ViewVC Help |
Powered by ViewVC 1.0.0 |