Home My Page Projects Code Snippets Project Openings SML/NJ
Summary Activity Forums Tracker Lists Tasks Docs Surveys News SCM Files

SCM Repository

[smlnj] Annotation of /sml/trunk/src/compiler/FLINT/kernel/ltykernel.sml
ViewVC logotype

Annotation of /sml/trunk/src/compiler/FLINT/kernel/ltykernel.sml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 53 - (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 :    
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 : league 53 (* unfortunately, the `temporary hack' is being exported now! *)
389 :     val tc_freevars = tc_vs
390 : monnier 16
391 :     (** converting from the hash-consing reps to the standard reps *)
392 :     fun tk_outX (r as ref(_ : int, t : tkindI, _ : aux_info)) = t
393 :     fun tc_outX (r as ref(_ : int, t : tycI, _ : aux_info)) = t
394 :     fun lt_outX (r as ref(_ : int, t : ltyI, _ : aux_info)) = t
395 :    
396 :    
397 :     (** converting from the standard reps to the hash-consing reps *)
398 :     fun tk_injX t = look(tk_table, wtoi(tk_hash t), t, tkI_eq, tk_mk)
399 :     fun tc_injX t = look(tc_table, wtoi(tc_hash t), t, tcI_eq, tc_mk)
400 :     fun lt_injX t = look(lt_table, wtoi(lt_hash t), t, ltI_eq, lt_mk)
401 :    
402 :    
403 :     (** key-comparison on tkind, tyc, lty *)
404 :     fun tk_cmp (k1, k2) = cmp(tk_table, k1, k2)
405 :     fun tc_cmp (t1, t2) = cmp(tc_table, t1, t2)
406 :     fun lt_cmp (t1, t2) = cmp(lt_table, t1, t2)
407 :    
408 :    
409 :     (** get the hash key of each lty, only used by reps/coerce.sml; a hack *)
410 :     fun lt_key (ref (h : int, _ : ltyI, _ : aux_info)) = h
411 :    
412 :     (***************************************************************************
413 :     * UTILITY FUNCTIONS ON TYC ENVIRONMENT *
414 :     ***************************************************************************)
415 :    
416 :     (** utility functions for manipulating the tycEnv *)
417 :     local val tc_void = tc_injX(TC_PRIM(PT.ptc_void))
418 : monnier 45 fun tc_cons (t, b) = tc_injX(TC_ARROW(FF_FIXED, [t],[b]))
419 : monnier 16 fun tc_interp x =
420 :     (case tc_outX x
421 :     of TC_PROJ(y, i) =>
422 :     (case tc_outX y of TC_SEQ ts => (SOME ts, i)
423 :     | TC_PRIM _ => (NONE, i)
424 :     | _ => bug "unexpected tycEnv1 in tc_interp")
425 :     | _ => bug "unexpected tycEnv2 in tc_interp")
426 :    
427 :     fun tc_encode(NONE, i) = tc_injX(TC_PROJ(tc_void,i))
428 :     | tc_encode(SOME ts, i) =
429 :     tc_injX(TC_PROJ(tc_injX(TC_SEQ(ts)), i))
430 :    
431 :     in
432 :    
433 :     exception tcUnbound
434 :     val initTycEnv : tycEnv = tc_void
435 :    
436 :     fun tcLookup(i, tenv : tycEnv) =
437 :     if i > 1 then
438 :     (case tc_outX tenv of TC_ARROW(_,_,[x]) => tcLookup(i-1, x)
439 :     | _ => bug "unexpected tycEnv in tcLookup")
440 :     else if i = 1 then
441 :     (case tc_outX tenv of TC_ARROW(_,[x],_) => tc_interp x
442 :     | _ => raise tcUnbound)
443 :     else bug "unexpected argument in tcLookup"
444 :    
445 :     fun tcInsert(tenv : tycEnv, et) = tc_cons(tc_encode et, tenv)
446 :    
447 :     fun tcSplit(tenv : tycEnv) =
448 :     (case tc_outX tenv of TC_ARROW(_,[x],[y]) => SOME (tc_interp x, y)
449 :     | _ => NONE)
450 :    
451 :    
452 :     end (* utililty function for tycEnv *)
453 :    
454 :    
455 :     (** checking if a tyc or an lty is in the normal form *)
456 :     fun tcp_norm ((t as ref (i, _, AX_REG(b,_))) : tyc) = b
457 :     | tcp_norm _ = false
458 :    
459 :     fun ltp_norm ((t as ref (i, _, AX_REG(b,_))) : lty) = b
460 :     | ltp_norm _ = false
461 :    
462 :    
463 :     (** utility functions for tc_env and lt_env *)
464 :     local fun tcc_env_int(x, 0, 0, te) = x
465 :     | tcc_env_int(x, i, j, te) = tc_injX(TC_ENV(x, i, j, te))
466 :    
467 :     fun ltc_env_int(x, 0, 0, te) = x
468 :     | ltc_env_int(x, i, j, te) = lt_injX(LT_ENV(x, i, j, te))
469 :    
470 :     fun withEff ([], ol, nl, tenv) = false
471 :     | withEff (a::r, ol, nl, tenv) =
472 : league 53 let val (i, j) = tvDecode a
473 : monnier 16 val neweff =
474 :     if i > ol then (ol <> nl)
475 :     else (* case tcLookup(i, tenv)
476 :     of (NONE, n) => (nl - n) <> i
477 :     | (SOME ts, n) =>
478 :     (let val y = List.nth(ts, j)
479 :     in (case tc_outX y
480 :     of TC_VAR(ni, nj) =>
481 :     ((nj <> j) orelse ((ni+nl-n) <> i))
482 :     | _ => true)
483 :     end) *) true
484 :     in neweff orelse (withEff(r, ol, nl, tenv))
485 :     end
486 :    
487 :     in
488 :    
489 :     fun tcc_env(x, ol, nl, tenv) =
490 :     let val tvs = tc_vs x
491 :     in case tvs
492 :     of NONE => tcc_env_int(x, ol, nl, tenv)
493 :     | SOME [] => x
494 :     | SOME nvs => if withEff(nvs, ol, nl, tenv)
495 :     then tcc_env_int(x, ol, nl, tenv)
496 :     else x
497 :     end
498 :    
499 :     fun ltc_env(x, ol, nl, tenv) =
500 :     let val tvs = lt_vs x
501 :     in case tvs
502 :     of NONE => ltc_env_int(x, ol, nl, tenv)
503 :     | SOME [] => x
504 :     | SOME nvs => if withEff (nvs, ol, nl, tenv)
505 :     then ltc_env_int(x, ol, nl, tenv)
506 :     else x
507 :     end
508 :    
509 :     end (* utility functions for lt_env and tc_env *)
510 :    
511 :    
512 :     (** utility functions for updating tycs and ltys *)
513 :     fun tyc_upd (tgt as ref(i : int, old : tycI, AX_NO), nt) =
514 :     (tgt := (i, TC_IND (nt, old), AX_NO))
515 :     | tyc_upd (tgt as ref(i : int, old : tycI, x as (AX_REG(false, _))), nt) =
516 :     (tgt := (i, TC_IND (nt, old), x))
517 :     | tyc_upd _ = bug "unexpected tyc_upd on already normalized tyc"
518 :    
519 :     fun lty_upd (tgt as ref(i : int, old : ltyI, AX_NO), nt) =
520 :     (tgt := (i, LT_IND (nt, old), AX_NO))
521 :     | lty_upd (tgt as ref(i : int, old : ltyI, x as (AX_REG(false, _))), nt) =
522 :     (tgt := (i, LT_IND (nt, old), x))
523 :     | lty_upd _ = bug "unexpected lty_upd on already normalized lty"
524 :    
525 :     (***************************************************************************
526 :     * UTILITY FUNCTIONS ON REASONING ABOUT REDUCTIONS *
527 :     ***************************************************************************)
528 :    
529 :     (** a list of constructor functions *)
530 :     val tcc_var = tc_injX o TC_VAR
531 :     val tcc_fn = tc_injX o TC_FN
532 :     val tcc_app = tc_injX o TC_APP
533 :     val tcc_seq = tc_injX o TC_SEQ
534 :     val tcc_proj = tc_injX o TC_PROJ
535 :     val tcc_fix = tc_injX o TC_FIX
536 :     val tcc_abs = tc_injX o TC_ABS
537 : monnier 45 val tcc_tup = tc_injX o TC_TUPLE
538 :     val tcc_parw = tc_injX o TC_PARROW
539 : monnier 24 val tcc_box = tc_injX o TC_BOX
540 : monnier 45 val tcc_real = tc_injX (TC_PRIM PT.ptc_real)
541 : monnier 16 val ltc_tyc = lt_injX o LT_TYC
542 :     val ltc_str = lt_injX o LT_STR
543 :     val ltc_pst = lt_injX o LT_PST
544 :     val ltc_fct = lt_injX o LT_FCT
545 :     val ltc_poly = lt_injX o LT_POLY
546 : monnier 45 val tcc_sum = tc_injX o TC_SUM
547 :     val tcc_token = tc_injX o TC_TOKEN
548 : monnier 16
549 :     (** the following function contains the procedure on how to
550 : monnier 45 * flatten the arguments and results of an arbitrary FLINT function
551 : monnier 16 *)
552 :     fun isKnown tc =
553 :     (case tc_outX(tc_whnm tc)
554 :     of (TC_PRIM _ | TC_ARROW _ | TC_BOX _ | TC_ABS _ | TC_PARROW _) => true
555 :     | (TC_CONT _ | TC_FIX _ | TC_SUM _ | TC_TUPLE _) => true
556 :     | TC_APP(tc, _) => isKnown tc
557 :     | TC_PROJ(tc, _) => isKnown tc
558 : monnier 45 | TC_TOKEN(k, x) => token_isKnown(k, x)
559 : monnier 16 | _ => false)
560 :    
561 :     and tc_autoflat tc =
562 :     let val ntc = tc_whnm tc
563 :     in (case tc_outX ntc
564 : monnier 45 of TC_TUPLE (_, [_]) => (* singleton record is not flattened to ensure
565 : monnier 16 isomorphism btw plambdatype and flinttype *)
566 :     (true, [ntc], false)
567 : monnier 45 | TC_TUPLE (_, ts) =>
568 :     if length ts < 10 then (true, ts, true)
569 :     else (true, [ntc], false) (* ZHONG added the magic number 10 *)
570 : monnier 16 | _ => if isKnown ntc then (true, [ntc], false)
571 :     else (false, [ntc], false))
572 :     end
573 :    
574 :     and tc_autotuple [x] = x
575 : monnier 45 | tc_autotuple xs =
576 :     if length xs < 10 then tcc_tup (RF_TMP, xs)
577 :     else bug "fatal error with tc_autotuple"
578 : monnier 16
579 :     and tcs_autoflat (flag, ts) =
580 :     if flag then (flag, ts)
581 :     else (case ts
582 : monnier 45 of [tc] => (let val ntc = tc_whnm tc
583 :     val (nraw, ntcs, _) = tc_autoflat ntc
584 : monnier 16 in (nraw, ntcs)
585 :     end)
586 :     | _ => bug "unexpected cooked multiples in tcs_autoflat")
587 :    
588 :     and lt_autoflat lt =
589 :     (case lt_outX(lt_whnm lt)
590 :     of LT_TYC tc =>
591 :     let val (raw, ts, flag) = tc_autoflat tc
592 :     in (raw, map ltc_tyc ts, flag)
593 :     end
594 :     | _ => (true, [lt], false))
595 :    
596 :     (** a special version of tcc_arw that does automatic flattening *)
597 : monnier 45 and tcc_arw (x as (FF_FIXED, _, _)) = tc_injX (TC_ARROW x)
598 :     | tcc_arw (x as (FF_VAR (true, true), _, _)) = tc_injX (TC_ARROW x)
599 :     | tcc_arw (b as (FF_VAR (b1, b2)), ts1, ts2) =
600 : monnier 16 let val (nb1, nts1) = tcs_autoflat (b1, ts1)
601 :     val (nb2, nts2) = tcs_autoflat (b2, ts2)
602 : monnier 45 in tc_injX (TC_ARROW(FF_VAR(nb1, nb2), nts1, nts2))
603 : monnier 16 end
604 :    
605 :     (** utility function to read the top-level of a tyc *)
606 :     and tc_lzrd t =
607 :     let fun g x =
608 :     (case tc_outX x
609 :     of TC_IND (tc, _) => g tc
610 :     | TC_ENV (tc, i, j, te) =>
611 :     let val ntc = g(h(tc, i, j, te))
612 :     in tyc_upd(x, ntc); ntc
613 :     end
614 :     | _ => x)
615 :    
616 :     and h (x, 0, 0, _) = g x
617 :     | h (x, ol, nl, tenv) =
618 :     let fun prop z = tcc_env(z, ol, nl, tenv)
619 :     in (case tc_outX x
620 :     of TC_VAR (i,j) =>
621 :     if (i <= ol) then
622 :     (let val et = tcLookup(i, tenv)
623 :     in case et
624 :     of (NONE, n) => tcc_var(nl - n, j)
625 :     | (SOME ts, n) =>
626 :     (let val y = List.nth(ts, j)
627 :     handle _ => raise tcUnbound
628 :     in h(y, 0, nl - n, initTycEnv)
629 :     end)
630 :     end)
631 :     else tcc_var(i-ol+nl, j)
632 :     | TC_NVAR _ => x
633 :     | TC_PRIM _ => x
634 :     | TC_FN (ks, tc) =>
635 :     let val tenv' = tcInsert(tenv, (NONE, nl))
636 :     in tcc_fn(ks, tcc_env(tc, ol+1, nl+1, tenv'))
637 :     end
638 :     | TC_APP (tc, tcs) => tcc_app(prop tc, map prop tcs)
639 :     | TC_SEQ tcs => tcc_seq (map prop tcs)
640 :     | TC_PROJ (tc, i) => tcc_proj(prop tc, i)
641 :     | TC_SUM tcs => tcc_sum (map prop tcs)
642 :     | TC_FIX ((n,tc,ts), i) =>
643 :     tcc_fix((n, prop tc, map prop ts), i)
644 :     | TC_ABS tc => tcc_abs (prop tc)
645 :     | TC_BOX tc => tcc_box (prop tc)
646 : monnier 45 | TC_TUPLE (rk, tcs) => tcc_tup (rk, map prop tcs)
647 : monnier 16 | TC_ARROW (r, ts1, ts2) =>
648 :     tcc_arw (r, map prop ts1, map prop ts2)
649 :     | TC_PARROW (t1, t2) => tcc_parw (prop t1, prop t2)
650 : monnier 45 | TC_TOKEN (k, t) => tcc_token(k, prop t)
651 : monnier 16 | TC_CONT _ => bug "unexpected TC_CONT in tc_lzrd"
652 :     | TC_IND (tc, _) => h(tc, ol, nl, tenv)
653 :     | TC_ENV(tc, ol', nl', tenv') =>
654 :     if ol = 0 then h(tc, ol', nl+nl', tenv')
655 :     else h(g x, ol, nl, tenv))
656 :     end (* function h *)
657 :     in if tcp_norm(t) then t else g t
658 :     end (* function tc_lzrd *)
659 :    
660 :     (** utility function to read the top-level of an lty *)
661 :     and lt_lzrd t =
662 :     let fun g x =
663 :     (case lt_outX x
664 :     of LT_IND (lt, _) => g lt
665 :     | LT_ENV(lt, i, j, te) =>
666 :     let val nlt = g(h(lt, i, j, te))
667 :     in lty_upd(x, nlt); nlt
668 :     end
669 :     | _ => x)
670 :    
671 :     and h (x, 0, 0, _) = g x
672 :     | h (x, ol, nl, tenv) =
673 :     let fun prop z = ltc_env(z, ol, nl, tenv)
674 :     in (case lt_outX x
675 :     of LT_TYC tc => ltc_tyc (tcc_env(tc, ol, nl, tenv))
676 :     | LT_STR ts => ltc_str (map prop ts)
677 :     | LT_PST its => ltc_pst (map (fn (i, t) => (i, prop t)) its)
678 :     | LT_FCT (ts1, ts2) => ltc_fct(map prop ts1, map prop ts2)
679 :     | LT_POLY (ks, ts) =>
680 :     let val tenv' = tcInsert(tenv, (NONE, nl))
681 :     in ltc_poly(ks,
682 :     map (fn t => ltc_env(t, ol+1, nl+1, tenv')) ts)
683 :     end
684 :     | LT_CONT _ => bug "unexpected LT_CONT in lt_lzrd"
685 :     | LT_IND (t, _) => h(t, ol, nl, tenv)
686 :     | LT_ENV (lt, ol', nl', tenv') =>
687 :     if ol = 0 then h(lt, ol', nl+nl', tenv')
688 :     else h(g x, ol, nl, tenv))
689 :     end (* function h *)
690 :     in if ltp_norm(t) then t else g t
691 :     end (* function lt_lzrd *)
692 :    
693 :     (** taking out the TC_IND indirection *)
694 :     and stripInd t = (case tc_outX t of TC_IND (x,_) => stripInd x | _ => t)
695 :    
696 :     (** normalizing an arbitrary tyc into a simple weak-head-normal-form *)
697 :     and tc_whnm t = if tcp_norm(t) then t else
698 :     let val nt = tc_lzrd t
699 :     in case (tc_outX nt)
700 :     of TC_APP(tc, tcs) =>
701 :     (let val tc' = tc_whnm tc
702 :     in case (tc_outX tc')
703 :     of TC_FN(ks, b) =>
704 :     let fun base () =
705 :     (b, 1, 0, tcInsert(initTycEnv,(SOME tcs, 0)))
706 :     val sp =
707 :     (case tc_outX b
708 :     of TC_ENV(b', ol', nl', te') =>
709 :     (case tcSplit te'
710 :     of SOME((NONE, n), te) =>
711 :     if (n = nl'-1) andalso (ol' > 0)
712 :     then (b', ol', n,
713 :     tcInsert(te, (SOME tcs, n)))
714 :     else base()
715 :     | _ => base())
716 :     | _ => base())
717 :     val res = tc_whnm(tcc_env sp)
718 :     in tyc_upd(nt, res); res
719 :     end
720 :     | ((TC_SEQ _) | (TC_TUPLE _) | (TC_ARROW _) | (TC_IND _)) =>
721 :     bug "unexpected tycs in tc_whnm-TC_APP"
722 :     | _ => let val xx = tcc_app(tc', tcs)
723 :     in stripInd xx
724 :     end
725 :     end)
726 :     | TC_PROJ(tc, i) =>
727 :     (let val tc' = tc_whnm tc
728 :     in (case (tc_outX tc')
729 :     of (TC_SEQ tcs) =>
730 :     let val res = List.nth(tcs, i)
731 :     handle _ => bug "TC_SEQ in tc_whnm"
732 :     val nres = tc_whnm res
733 :     in tyc_upd(nt, nres); nres
734 :     end
735 :     | ((TC_PRIM _) | (TC_NVAR _) | (TC_FIX _) | (TC_FN _) |
736 :     (TC_SUM _) | (TC_ARROW _) | (TC_ABS _) | (TC_BOX _) |
737 :     (TC_IND _) | (TC_TUPLE _)) =>
738 :     bug "unexpected tycs in tc_whnm-TC_PROJ"
739 :     | _ => let val xx = tcc_proj(tc', i)
740 :     in stripInd xx
741 :     end)
742 :     end)
743 : monnier 45 | TC_TOKEN(k, tc) =>
744 :     (let val tc' = tc_whnm tc
745 :     in if token_whnm k tc'
746 :     then let val xx = tcc_token(k, tc') in stripInd xx end
747 :     else let val res = token_reduce(k, tc')
748 :     val nres = tc_whnm res
749 :     in tyc_upd(nt, nres); nres
750 :     end
751 :     end)
752 : monnier 16 | TC_IND (tc, _) => tc_whnm tc
753 :     | TC_ENV _ => bug "unexpected TC_ENV in tc_whnm"
754 :     | _ => nt
755 :     end (* function tc_whnm *)
756 :    
757 :     (** normalizing an arbitrary lty into the simple weak-head-normal-form *)
758 :     and lt_whnm t = if ltp_norm(t) then t else
759 :     let val nt = lt_lzrd t
760 :     in case (lt_outX nt)
761 :     of LT_TYC tc => ltc_tyc(tc_whnm tc)
762 :     | _ => nt
763 :     end (* function lt_whnm *)
764 :    
765 :     (** normalizing an arbitrary tyc into the standard normal form *)
766 :     fun tc_norm t = if (tcp_norm t) then t else
767 :     let val nt = tc_whnm t
768 :     in if (tcp_norm nt) then nt
769 :     else
770 :     (let val res =
771 :     (case (tc_outX nt)
772 :     of TC_FN (ks, tc) => tcc_fn(ks, tc_norm tc)
773 :     | TC_APP (tc, tcs) =>
774 :     tcc_app(tc_norm tc, map tc_norm tcs)
775 :     | TC_SEQ tcs => tcc_seq(map tc_norm tcs)
776 :     | TC_PROJ (tc, i) => tcc_proj(tc_norm tc, i)
777 :     | TC_SUM tcs => tcc_sum (map tc_norm tcs)
778 :     | TC_FIX ((n,tc,ts), i) =>
779 :     tcc_fix((n, tc_norm tc, map tc_norm ts), i)
780 :     | TC_ABS tc => tcc_abs(tc_norm tc)
781 :     | TC_BOX tc => tcc_box(tc_norm tc)
782 : monnier 45 | TC_TUPLE (rk, tcs) => tcc_tup(rk, map tc_norm tcs)
783 : monnier 16 | TC_ARROW (r, ts1, ts2) =>
784 :     tcc_arw(r, map tc_norm ts1, map tc_norm ts2)
785 :     | TC_PARROW (t1, t2) => tcc_parw(tc_norm t1, tc_norm t2)
786 : monnier 45 | TC_TOKEN (k, t) => tcc_token(k, tc_norm t)
787 : monnier 16 | TC_IND (tc, _) => tc_norm tc
788 :     | TC_ENV _ => bug "unexpected tycs in tc_norm"
789 :     | _ => nt)
790 :     in tyc_upd(nt, res); res
791 :     end)
792 :     end (* function tc_norm *)
793 :    
794 :     (** normalizing an arbitrary lty into the standard normal form *)
795 :     fun lt_norm t = if (ltp_norm t) then t else
796 :     let val nt = lt_lzrd t
797 :     in if (ltp_norm nt) then nt
798 :     else
799 :     (let val res =
800 :     (case lt_outX nt
801 :     of LT_TYC tc => ltc_tyc(tc_norm tc)
802 :     | LT_STR ts => ltc_str(map lt_norm ts)
803 :     | LT_PST its =>
804 :     ltc_pst(map (fn (i, t) => (i, lt_norm t)) its)
805 :     | LT_FCT (ts1, ts2) =>
806 :     ltc_fct(map lt_norm ts1, map lt_norm ts2)
807 :     | LT_POLY (ks, ts) => ltc_poly (ks, map lt_norm ts)
808 :     | LT_IND (lt, _) => lt_norm lt
809 :     | _ => bug "unexpected ltys in lt_norm")
810 :     in lty_upd(nt, res); res
811 :     end)
812 :     end (* function lt_norm *)
813 :    
814 :     (***************************************************************************
815 : monnier 45 * REGISTER A NEW TOKEN TYC --- TC_WRAP *
816 :     ***************************************************************************)
817 :    
818 :     (** we add a new constructor named TC_RBOX through the token facility *)
819 :     local val name = "TC_WRAP"
820 :     val abbrev = "WR"
821 :     val is_known = fn _ => true (* why is this ? *)
822 :     fun tcc_tok k t = tcc_token(k, t)
823 :    
824 :     fun unknown tc =
825 :     (case tc_outX tc
826 :     of (TC_VAR _ | TC_NVAR _) => true
827 :     | (TC_APP(tc, _)) => unknown tc
828 :     | (TC_PROJ(tc, _)) => unknown tc
829 :     | _ => false)
830 :    
831 :     fun flex_tuple ts =
832 :     let fun hhh(x::r, ukn, wfree) =
833 :     let fun iswp tc =
834 :     (case tc_outX tc
835 :     of TC_TOKEN(k', t) => (* WARNING: need check k' *)
836 :     (case tc_outX t
837 :     of TC_PRIM pt => false
838 :     | _ => true)
839 :     | _ => true)
840 :     in hhh(r, (unknown x) orelse ukn, (iswp x) andalso wfree)
841 :     end
842 :     | hhh([], ukn, wfree) = ukn andalso wfree
843 :     in hhh(ts, false, true)
844 :     end
845 :    
846 :     fun is_whnm tc =
847 :     (case tc_outX tc
848 :     of (TC_ARROW(FF_FIXED, [t], _)) => (unknown t)
849 :     | (TC_TUPLE(rf, ts)) => flex_tuple ts
850 :     | (TC_PRIM pt) => PT.unboxed pt
851 :     | _ => false)
852 :    
853 :     (* invariants: tc itself is in whnm but is_whnm tc = false *)
854 :     fun reduce_one (k, tc) =
855 :     (case tc_outX tc
856 :     of TC_TUPLE (rk, ts) =>
857 :     let fun hhh (x::r, nts, ukn) =
858 :     let val nx = tc_whnm x
859 :     val b1 = unknown nx
860 :     val nnx =
861 :     (case tc_outX nx
862 :     of TC_TOKEN(k', t) =>
863 :     if token_eq(k, k') then
864 :     (case tc_outX t
865 :     of TC_PRIM _ => t
866 :     | _ => nx)
867 :     else nx
868 :     | _ => nx)
869 :     in hhh(r, nnx::nts, b1 orelse ukn)
870 :     end
871 :     | hhh ([], nts, ukn) =
872 :     let val nt = tcc_tup(rk, rev nts)
873 :     in if ukn then tcc_token(k, nt) else nt
874 :     end
875 :     in hhh(ts, [], false)
876 :     end
877 :     | TC_ARROW (FF_FIXED, [_,_], [_]) => tc
878 :     | TC_ARROW (FF_FIXED, [t1], ts2 as [_]) =>
879 :     let val nt1 = tc_whnm t1
880 :     fun ggg z =
881 :     let val nz = tc_whnm z
882 :     in (case tc_outX nz
883 :     of TC_PRIM pt =>
884 :     if PT.unboxed pt then tcc_token(k, nz)
885 :     else nz
886 :     | _ => nz)
887 :     end
888 :     val (wp, nts1) =
889 :     (case tc_outX nt1
890 :     of TC_TUPLE(_, [x,y]) => (false, [ggg x, ggg y])
891 :     | TC_TOKEN(k', x) =>
892 :     if token_eq(k, k') then
893 :     (case (tc_outX x)
894 :     of TC_TUPLE(_, [y, z]) =>
895 :     (false, [ggg y, ggg z])
896 :     | _ => (true, [nt1]))
897 :     else (false, [nt1])
898 :     | _ => (unknown nt1, [nt1]))
899 :     val nt = tcc_arw(FF_FIXED, nts1, ts2)
900 :     in if wp then tcc_token(k, nt) else nt
901 :     end
902 :     | TC_ARROW (FF_FIXED, _, _) =>
903 :     bug "unexpected reduce_one on ill-formed FF_FIX arrow types"
904 :     | TC_ARROW (FF_VAR(b1,b2), ts1, ts2) =>
905 :     bug "calling reduce_one on FF_VAR arrow types"
906 :     | TC_PRIM pt =>
907 :     if PT.unboxed pt then
908 :     bug "calling reduce_one on an already-reduced whnm"
909 :     else tc
910 :     | TC_TOKEN(k', t) =>
911 :     if token_eq(k, k') then tc
912 :     else bug "unexpected token in reduce_one"
913 :     | (TC_BOX _ | TC_ABS _ | TC_PARROW _) =>
914 :     bug "unexpected tc_box/abs/parrow in reduce_one"
915 :     | TC_ENV _ => bug "unexpected TC_ENV in reduce_one"
916 :     | TC_IND _ => bug "unexpected TC_IND in reduce_one"
917 :     | _ => tc)
918 :    
919 :     in
920 :    
921 :     val wrap_token =
922 :     register_token {name=name, abbrev=abbrev, reduce_one=reduce_one,
923 :     is_whnm=is_whnm, is_known=is_known}
924 :    
925 :     end (* end of creating the box token for "tcc_rbox" *)
926 :    
927 :     (** testing if a tyc is a unknown constructor *)
928 :     fun tc_unknown tc = not (isKnown tc)
929 :    
930 :     (***************************************************************************
931 : monnier 16 * REBINDING THE INJECTION AND PROJECTION FUNCTIONS *
932 :     ***************************************************************************)
933 :     (** converting from the standard reps to the hash-consing reps *)
934 :     val tk_inj = tk_injX
935 :     val tc_inj = tc_injX
936 :     val lt_inj = lt_injX
937 :    
938 :     (** converting from the hash-consing reps to the standard reps *)
939 :     val tk_out = tk_outX
940 :     val tc_out = tc_outX o tc_whnm
941 :     val lt_out = lt_outX o lt_whnm
942 :    
943 :     (***************************************************************************
944 :     * UTILITY FUNCTIONS ON TESTING EQUIVALENCE *
945 :     ***************************************************************************)
946 :    
947 :     (** testing the equality of values of tkind, tyc, lty *)
948 :     fun eqlist (p, x::xs, y::ys) = (p(x,y)) andalso (eqlist(p, xs, ys))
949 :     | eqlist (p, [], []) = true
950 :     | eqlist _ = false
951 :    
952 :     (** testing the "pointer" equality on normalized tkind, tyc, and lty *)
953 :     fun tk_eq (x: tkind, y) = (x = y)
954 :     fun tc_eq (x: tyc, y) = (x = y)
955 :     fun lt_eq (x: lty, y) = (x = y)
956 :    
957 :     (** testing the equivalence for arbitrary tkinds, tycs and ltys *)
958 :     val tk_eqv = tk_eq (* all tkinds are normalized *)
959 :    
960 :     (** tc_eqv_generator, invariant: t1 and t2 are in the wh-normal form *)
961 :     fun tc_eqv_gen (eqop1, eqop2, eqop3, eqop4) (t1, t2) =
962 :     (case (tc_outX t1, tc_outX t2)
963 :     of (TC_FN(ks1, b1), TC_FN(ks2, b2)) =>
964 :     (eqlist(tk_eqv, ks1, ks2)) andalso (eqop2(b1, b2))
965 :     | (TC_APP(a1, b1), TC_APP(a2, b2)) =>
966 :     (eqop1(a1, a2)) andalso (eqlist(eqop2, b1, b2))
967 :     | (TC_SEQ ts1, TC_SEQ ts2) => eqlist(eqop1, ts1, ts2)
968 :     | (TC_SUM ts1, TC_SUM ts2) => eqlist(eqop1, ts1, ts2)
969 : monnier 45 | (TC_TUPLE (_, ts1), TC_TUPLE (_, ts2)) => eqlist(eqop1, ts1, ts2)
970 : monnier 16 | (TC_ABS a, TC_ABS b) => eqop1(a, b)
971 :     | (TC_ABS a, _) => eqop3(a, t2)
972 :     | (_, TC_ABS b) => eqop3(t1, b)
973 :     | (TC_BOX a, TC_BOX b) => eqop1(a, b)
974 :     | (TC_BOX a, _) => eqop3(a, t2)
975 :     | (_, TC_BOX b) => eqop3(t1, b)
976 : monnier 45 | (TC_TOKEN(k1,t1), TC_TOKEN(k2,t2)) =>
977 :     (token_eq(k1,k2)) andalso (eqop1(t1,t2))
978 : monnier 16 | (TC_PROJ(a1, i1), TC_PROJ(a2, i2)) =>
979 :     (i1 = i2) andalso (eqop1(a1, a2))
980 :     | (TC_ARROW(r1, a1, b1), TC_ARROW(r2, a2, b2)) =>
981 :     (r1 = r2) andalso (eqop4(a1, a2)) andalso (eqop4(b1, b2))
982 :     | (TC_PARROW(a1, b1), TC_PARROW(a2, b2)) =>
983 :     (eqop1(a1, a2)) andalso (eqop1(b1, b2))
984 :     | (TC_FIX((n1,tc1,ts1), i1), TC_FIX((n2,tc2,ts2), i2)) =>
985 :     true (* INCORRECT: this is temporary (ZHONG) *)
986 :     | (TC_CONT ts1, TC_CONT ts2) => eqlist(eqop1, ts1, ts2)
987 :     | _ => false)
988 :    
989 :     fun tc_eqv (x as ref (_, _, AX_REG(true, _)),
990 :     y as ref (_, _, AX_REG(true, _))) = tc_eq(x,y)
991 :     | tc_eqv (x, y) =
992 :     let val t1 = tc_whnm x
993 :     val t2 = tc_whnm y
994 :     in if (tcp_norm t1) andalso (tcp_norm t2) then tc_eq(t1, t2)
995 :     else tc_eqv_gen (tc_eqv, tc_eqv, fn _ => false,
996 :     fn (ts1, ts2) => eqlist(tc_eqv, ts1, ts2)) (t1, t2)
997 :     end (* function tc_eqv *)
998 :    
999 : monnier 45 fun tc_eqv_x (x, y) =
1000 :     let val t1 = tc_whnm x
1001 :     val t2 = tc_whnm y
1002 :     in (if (tcp_norm t1) andalso (tcp_norm t2) then tc_eq(t1, t2)
1003 :     else false) orelse
1004 :     (tc_eqv_gen (tc_eqv_x, tc_eqv_x, fn _ => false,
1005 :     fn (ts1, ts2) => eqlist(tc_eqv_x, ts1, ts2)) (t1, t2))
1006 :     end (* function tc_eqv_x *)
1007 :    
1008 : monnier 16 (** testing the equivalence of two tycs with relaxed constraints *)
1009 :     fun tc_eqv_bx (x : tyc, y) =
1010 :     let val t1 = tc_whnm x
1011 :     val t2 = tc_whnm y
1012 :     in (if (tcp_norm t1) andalso (tcp_norm t2) then tc_eq(t1, t2)
1013 :     else false) orelse
1014 :     (tc_eqv_gen (tc_eqv_bx, tc_eqv_sp, fn _ => false,
1015 :     fn (ts1, ts2) => tc_eqv_bx(tc_autotuple ts1,
1016 :     tc_autotuple ts2)) (t1, t2))
1017 :     end (* function tc_eqv_bx *)
1018 :    
1019 :     and tc_eqv_sp (x : tyc, y) =
1020 :     let val t1 = tc_whnm x
1021 :     val t2 = tc_whnm y
1022 :     in (if (tcp_norm t1) andalso (tcp_norm t2) then tc_eq(t1, t2)
1023 :     else false) orelse
1024 :     (tc_eqv_gen (tc_eqv_sp, tc_eqv_sp, tc_eqv_sp,
1025 :     fn (ts1, ts2) => tc_eqv_sp(tc_autotuple ts1,
1026 :     tc_autotuple ts2)) (t1, t2))
1027 :     end (* function tc_eqv_sp *)
1028 :    
1029 :     (*
1030 :     * all the complexity of lt_eqv comes from the partial-structure (or
1031 :     * partial record) type (the LT_PST type). If we can remove LT_PST
1032 :     * type, then the following can be considerabily simplified. (ZHONG)
1033 :     *)
1034 :    
1035 :     (** lt_eqv_generator, invariant: x and y are in the wh-normal form *)
1036 :     fun lt_eqv_gen (eqop1, eqop2) (x : lty, y) =
1037 :     let fun sp (r, []) = true
1038 :     | sp (r, (i,t)::s) =
1039 :     (if (eqop1(List.nth(r,i),t))
1040 :     then sp(r,s) else false) handle _ => false
1041 :    
1042 :     fun pp ([], _) = true
1043 :     | pp (_, []) = true
1044 :     | pp (a as ((i,t)::l), b as ((j,s)::r)) =
1045 :     if i > j then pp(a,r)
1046 :     else if i < j then pp(l,b)
1047 :     else if (eqop1(t,s)) then pp(l,r) else false
1048 :    
1049 :     (* seq should be called if t1 and t2 are weak-head normal form *)
1050 :     fun seq (t1, t2) =
1051 :     (case (lt_outX t1, lt_outX t2)
1052 :     of (LT_POLY(ks1, b1), LT_POLY(ks2, b2)) =>
1053 :     (eqlist(tk_eqv, ks1, ks2)) andalso (eqlist(eqop1, b1, b2))
1054 :     | (LT_FCT(as1, bs1), LT_FCT(as2, bs2)) =>
1055 :     (eqlist(eqop1, as1, as2)) andalso (eqlist(eqop1, bs1, bs2))
1056 :     | (LT_TYC a, LT_TYC b) => eqop2(a, b)
1057 :     | (LT_STR s1, LT_STR s2) => eqlist(eqop1, s1, s2)
1058 :     | (LT_PST s1, LT_PST s2) => pp(s1, s2)
1059 :     | (LT_PST s1, LT_STR s2) => sp(s2, s1)
1060 :     | (LT_STR s1, LT_PST s2) => sp(s1, s2)
1061 :     | (LT_CONT s1, LT_CONT s2) => eqlist(eqop1, s1, s2)
1062 :     | _ => false)
1063 :     in seq(x, y)
1064 :     end (* function lt_eqv_gen *)
1065 :    
1066 :     fun lt_eqv(x : lty, y) =
1067 :     let val seq = lt_eqv_gen (lt_eqv, tc_eqv)
1068 : monnier 45 in if ((ltp_norm x) andalso (ltp_norm y)) then
1069 :     (lt_eq(x, y)) orelse (seq(x, y))
1070 : monnier 16 else (let val t1 = lt_whnm x
1071 :     val t2 = lt_whnm y
1072 :     in if (ltp_norm t1) andalso (ltp_norm t2) then
1073 : monnier 45 (lt_eq(t1, t2)) orelse (seq(t1, t2))
1074 : monnier 16 else seq(t1, t2)
1075 :     end)
1076 :     end (* function lt_eqv *)
1077 :    
1078 : monnier 45 fun lt_eqv_x(x : lty, y) =
1079 :     let val seq = lt_eqv_gen (lt_eqv_x, tc_eqv_x)
1080 :     in if ((ltp_norm x) andalso (ltp_norm y)) then
1081 :     (lt_eq(x, y)) orelse (seq(x, y))
1082 :     else (let val t1 = lt_whnm x
1083 :     val t2 = lt_whnm y
1084 :     in if (ltp_norm t1) andalso (ltp_norm t2) then
1085 :     (lt_eq(t1, t2)) orelse (seq(t1, t2))
1086 :     else seq(t1, t2)
1087 :     end)
1088 :     end (* function lt_eqv *)
1089 :    
1090 : monnier 16 fun lt_eqv_bx (x : lty, y) =
1091 :     let val seq = lt_eqv_gen (lt_eqv_bx, tc_eqv_bx)
1092 :     in if (ltp_norm x) andalso (ltp_norm y) then
1093 :     (lt_eq(x, y)) orelse (seq(x, y))
1094 :     else (let val t1 = lt_whnm x
1095 :     val t2 = lt_whnm y
1096 :     in if (ltp_norm t1) andalso (ltp_norm t2) then
1097 :     (lt_eq(t1, t2)) orelse (seq(t1, t2))
1098 :     else seq(t1, t2)
1099 :     end)
1100 :     end (* function lt_eqv_bx *)
1101 :    
1102 : monnier 45 (** testing equivalence of fflags and rflags *)
1103 :     val ff_eqv : fflag * fflag -> bool = (op =)
1104 :     val rf_eqv : rflag * rflag -> bool = (op =)
1105 :    
1106 :     (***************************************************************************
1107 :     * UTILITY FUNCTIONS ON FINDING OUT THE DEPTH OF THE FREE TYC VARIABLES *
1108 :     ***************************************************************************)
1109 :     (** finding out the innermost binding depth for a tyc's free variables *)
1110 :     fun tc_depth (x, d) =
1111 :     let val tvs = tc_vs (tc_norm x)
1112 :     (* unfortunately we have to reduce everything to the normal form
1113 :     before we can talk about its list of free type variables.
1114 :     *)
1115 :     in case tvs
1116 :     of NONE => bug "unexpected case in tc_depth"
1117 :     | SOME [] => DI.top
1118 : league 53 | SOME (a::_) => d + 1 - (#1(tvDecode a))
1119 : monnier 45 end
1120 :    
1121 :     fun tcs_depth ([], d) = DI.top
1122 :     | tcs_depth (x::r, d) = Int.max(tc_depth(x, d), tcs_depth(r, d))
1123 :    
1124 : monnier 16 end (* toplevel local *)
1125 :     end (* abstraction LtyKernel *)
1126 :    

root@smlnj-gforge.cs.uchicago.edu
ViewVC Help
Powered by ViewVC 1.0.0