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 16 - (view) (download)

1 : monnier 16 (* COPYRIGHT (c) 1997 YALE FLINT PROJECT *)
2 :     (* ltykernel.sml *)
3 :    
4 :     structure LtyKernel :> LTYKERNEL =
5 :     struct
6 :    
7 :     (***************************************************************************
8 :     * UTILITY FUNCTIONS FOR HASHCONSING BASICS *
9 :     ***************************************************************************)
10 :    
11 :     (** hashconsing implementation basics *)
12 :     local open SortedList
13 :     val MVAL = 10000
14 :     val BVAL = MVAL * 2 (* all index i start from 0 *)
15 :     in
16 :    
17 :     type enc_tvar = int
18 :     fun tvToInt (d, i) = d * MVAL + i
19 :     fun tvFromInt x = ((x div MVAL), (x mod MVAL))
20 :    
21 :     fun exitLevel xs =
22 :     let fun h ([], x) = rev x
23 :     | h (a::r, x) = if a < BVAL then h(r, x) else h(r, (a-MVAL)::x)
24 :     in h(xs, [])
25 :     end
26 :    
27 :     datatype aux_info = AX_REG of bool * enc_tvar list
28 :     | AX_NO
29 :    
30 :     val mergeTvs = merge
31 :     val fmergeTvs = foldmerge
32 :    
33 :     type 'a hash_cell = (int * 'a * aux_info) ref
34 :    
35 :     end (* local of hashconsing implementation basics *)
36 :    
37 :    
38 :     (***************************************************************************
39 :     * DATATYPE DEFINITIONS *
40 :     ***************************************************************************)
41 :    
42 :     (** definition of kinds for all the lambda tycs *)
43 :     datatype tkindI
44 :     = TK_MONO (* ground mono tycon *)
45 :     | TK_BOX (* boxed/tagged tycon *)
46 :     | TK_SEQ of tkind list (* sequence of tycons *)
47 :     | TK_FUN of tkind list * tkind (* tycon function *)
48 :    
49 :     withtype tkind = tkindI hash_cell (* hash-consing-impl of tkind *)
50 :    
51 :     (* definitoins of named tyc variables *)
52 :     type tvar = LambdaVar.lvar (* temporary definitions *)
53 :     val mkTvar = LambdaVar.mkLvar
54 :    
55 :     (** definitions of lambda type constructors *)
56 :     datatype tycI
57 :     = TC_VAR of DebIndex.index * int (* tyc variables *)
58 :     | TC_NVAR of tvar * DebIndex.depth * int (* named tyc variables *)
59 :     | TC_PRIM of PrimTyc.primtyc (* primitive tyc *)
60 :    
61 :     | TC_FN of tkind list * tyc (* tyc abstraction *)
62 :     | TC_APP of tyc * tyc list (* tyc application *)
63 :     | TC_SEQ of tyc list (* tyc sequence *)
64 :     | TC_PROJ of tyc * int (* tyc projection *)
65 :    
66 :     | TC_SUM of tyc list (* sum tyc *)
67 :     | TC_FIX of (int * tyc * tyc list) * int (* recursive tyc *)
68 :    
69 :     | TC_TUPLE of rflag * tyc list (* std record tyc *)
70 :     | TC_ARROW of fflag * tyc list * tyc list (* std function tyc *)
71 :     | TC_PARROW of tyc * tyc (* special fun tyc, not used *)
72 :    
73 :     | TC_BOX of tyc (* boxed tyc *)
74 :     | TC_ABS of tyc (* abstract tyc, not used *)
75 :     | TC_CONT of tyc list (* intern continuation tycon *)
76 :     | TC_IND of tyc * tycI (* indirect tyc thunk *)
77 :     | TC_ENV of tyc * int * int * tycEnv (* tyc closure *)
78 :    
79 :     withtype tyc = tycI hash_cell (* hash-consed tyc cell *)
80 :     and tycEnv = tyc (*
81 :     * This really is (tyc list option * int) list,
82 :     * it is encoded using SEQ[(PROJ(SEQ tcs),i)]
83 :     * and SEQ[(PROJ(VOID, i))]. (ZHONG)
84 :     *)
85 :    
86 :     and fflag = bool * bool (* is the calling convention fixed ? *)
87 :     and rflag = unit (* record kind, not used as of now *)
88 :    
89 :     val default_rflag = () (* a rflag template *)
90 :     val default_fflag = (true,true)
91 :    
92 :     (** definitions of lambda types *)
93 :     datatype ltyI
94 :     = LT_TYC of tyc (* monomorphic type *)
95 :     | LT_STR of lty list (* structure record type *)
96 :     | LT_FCT of lty list * lty list (* functor arrow type *)
97 :     | LT_POLY of tkind list * lty list (* polymorphic type *)
98 :    
99 :     | LT_PST of (int * lty) list (* partial-structure type *)
100 :     | LT_CONT of lty list (* internal cont type *)
101 :     | LT_IND of lty * ltyI (* a lty thunk and its sig *)
102 :     | LT_ENV of lty * int * int * tycEnv (* lty closure *)
103 :    
104 :     withtype lty = ltyI hash_cell (* hash-consed lty cell *)
105 :    
106 :     (***************************************************************************
107 :     * HASHCONSING IMPLEMENTATIONS *
108 :     ***************************************************************************)
109 :    
110 :     (** Hash-consing implementations of tyc, tkind, lty *)
111 :    
112 :     local structure Weak = SMLofNJ.Weak
113 :     structure PT = PrimTyc
114 :     structure DI = DebIndex
115 :    
116 :     fun bug msg = ErrorMsg.impossible("LtyKernel: "^msg)
117 :    
118 :     val itow = Word.fromInt
119 :     val wtoi = Word.toIntX
120 :     val andb = Word.andb
121 :    
122 :     val N = 2048 (* 1024 *)
123 :     val NN = itow (N*N)
124 :     val P = 0w509 (* was 0w1019, a prime < 1024 so that N*N*P < maxint *)
125 :    
126 :     val tk_table : tkind Weak.weak list Array.array = Array.array(N,nil)
127 :     val tc_table : tyc Weak.weak list Array.array = Array.array(N,nil)
128 :     val lt_table : lty Weak.weak list Array.array = Array.array(N,nil)
129 :    
130 :     fun vector2list v = Vector.foldr (op ::) [] v
131 :    
132 :     fun revcat(a::rest,b) = revcat(rest,a::b)
133 :     | revcat(nil,b) = b
134 :    
135 :     fun combine [x] = itow x
136 :     | combine (a::rest) =
137 :     andb(itow a +(combine rest)*P, NN - 0w1)
138 :     | combine _ = bug "unexpected case in combine"
139 :    
140 :     (*
141 :     * Because of the "cmp" function below, it's necessary to keep
142 :     * each bucket-list in a consistent order, and not reverse
143 :     * or move-to-front or whatever.
144 :     *)
145 :     fun look(table, h, t, eq, mk) =
146 :     let val i = wtoi(andb(itow h, itow(N-1)))
147 :    
148 :     fun g(l, z as (w::rest)) =
149 :     (case Weak.strong w
150 :     of SOME (r as ref(h',t',_)) =>
151 :     if (h=h') andalso (eq {new=t, old=t'})
152 :     then (Array.update(table, i, revcat(l,z)); r)
153 :     else g(w::l, rest)
154 :     | NONE => g(l, rest))
155 :     | g(l, []) =
156 :     let val r = mk(h, t)
157 :     in Array.update(table, i, (Weak.weak r) :: rev l); r
158 :     end
159 :    
160 :     in g([], Array.sub(table, i))
161 :     end
162 :    
163 :     fun cmp(table, a as ref(ai,_,_), b as ref (bi,_,_)) =
164 :     if ai < bi then LESS
165 :     else if ai > bi then GREATER
166 :     else if a = b then EQUAL
167 :     else let val index = wtoi (andb(itow ai,itow(N-1)))
168 :     fun g [] = bug "unexpected case in cmp"
169 :     | g (w::rest) =
170 :     (case Weak.strong w
171 :     of SOME r =>
172 :     if a=r then LESS
173 :     else if b=r then GREATER
174 :     else g rest
175 :     | NONE => g rest)
176 :     in g(Array.sub(table,index))
177 :     end
178 :    
179 :    
180 :     fun getnum (ref(i,_,_)) = i
181 :     fun tagnums nil = nil
182 :     | tagnums ((i,t)::rest) = i::getnum t::tagnums rest
183 :    
184 :     fun tk_hash tk =
185 :     let fun g (TK_MONO) = 0w1
186 :     | g (TK_BOX) = 0w2
187 :     | g (TK_SEQ ks) = combine (3::map getnum ks)
188 :     | g (TK_FUN(ks, k)) = combine (4::getnum k::(map getnum ks))
189 :     in g tk
190 :     end
191 :    
192 :     fun tc_hash tc =
193 :     let fun g (TC_VAR(d, i)) = combine [1, (DI.di_key d)*10, i]
194 :     | g (TC_NVAR(v, d, i)) = combine[15, v, (DI.dp_key d)*13, i]
195 :     | g (TC_PRIM pt) = combine [2, PT.pt_toint pt]
196 :     | g (TC_FN(ks, t)) = combine (3::(getnum t)::(map getnum ks))
197 :     | g (TC_APP(t, ts)) = combine (4::(getnum t)::(map getnum ts))
198 :     | g (TC_SEQ ts) = combine (5::(map getnum ts))
199 :     | g (TC_PROJ(t, i)) = combine [6, (getnum t), i]
200 :     | g (TC_SUM ts) = combine (7::(map getnum ts))
201 :     | g (TC_FIX((n, t, ts), i)) =
202 :     combine (8::n::i::(getnum t)::(map getnum ts))
203 :     | g (TC_ABS t) = combine [9, getnum t]
204 :     | g (TC_BOX t) = combine [10, getnum t]
205 :     | g (TC_TUPLE (_, ts)) = combine (11::(map getnum ts))
206 :     | g (TC_ARROW(rw, ts1, ts2)) =
207 :     let fun h(true, true) = 10
208 :     | h(true, _) = 20
209 :     | h(_, true) = 30
210 :     | h _ = 40
211 :     in combine (12::(h rw)::(map getnum (ts1@ts2)))
212 :     end
213 :     | g (TC_PARROW (t1,t2)) = combine [13, getnum t1, getnum t2]
214 :     | g (TC_CONT ts) = combine (14::(map getnum ts))
215 :     | g (TC_ENV(t,i,j,env)) =
216 :     combine[15, getnum t, i, j, getnum env]
217 :     | g (TC_IND _) = bug "unexpected TC_IND in tc_hash"
218 :    
219 :     in g tc
220 :     end
221 :    
222 :     fun lt_hash lt =
223 :     let fun g (LT_TYC t) = combine [1, getnum t]
224 :     | g (LT_STR ts) = combine (2::(map getnum ts))
225 :     | g (LT_PST ts) = combine (3::(tagnums ts))
226 :     | g (LT_FCT(ts1, ts2)) =
227 :     combine (4::(map getnum (ts1@ts2)))
228 :     | g (LT_POLY(ks, ts)) =
229 :     combine (5::((map getnum ts)@(map getnum ks)))
230 :     | g (LT_CONT ts) = combine (6::(map getnum ts))
231 :     | g (LT_ENV(t,i,j,env)) =
232 :     combine [7, getnum t, i, j, getnum env]
233 :     | g (LT_IND _) = bug "unexpected LT_IND in tc_hash"
234 :     in g lt
235 :     end
236 :    
237 :     fun tkI_eq {new: tkindI, old} = (new = old)
238 :    
239 :     (* the 1st is one being mapped; the 2nd is in the hash table *)
240 :     fun tcI_eq {new : tycI, old=TC_IND(_,s)} = tcI_eq {new=new, old=s}
241 :     | tcI_eq {new, old} = (new=old)
242 :    
243 :     fun ltI_eq {new : ltyI, old=LT_IND(_,s)} = ltI_eq {new=new, old=s}
244 :     | ltI_eq {new, old} = (new=old)
245 :    
246 :     val baseAux = AX_REG (true, [])
247 :    
248 :     fun getAux (ref(i : int, _, x)) = x
249 :    
250 :     fun mergeAux(AX_NO, _) = AX_NO
251 :     | mergeAux(_, AX_NO) = AX_NO
252 :     | mergeAux(AX_REG(b1,vs1), AX_REG(b2,vs2)) =
253 :     AX_REG(b2 andalso b1, mergeTvs(vs1, vs2))
254 :    
255 :     fun fsmerge [] = baseAux
256 :     | fsmerge [x] = getAux x
257 :     | fsmerge xs =
258 :     let fun loop([], z) = z
259 :     | loop(_, AX_NO) = AX_NO
260 :     | loop(a::r, z) = loop(r, mergeAux(getAux a, z))
261 :     in loop(xs, baseAux)
262 :     end
263 :    
264 :     fun exitAux(AX_REG(b, vs)) = AX_REG(b, exitLevel vs)
265 :     | exitAux x = x
266 :    
267 :     fun tc_aux tc =
268 :     let fun g (TC_VAR(d, i)) = AX_REG(true, [tvToInt(d, i)])
269 :     | g (TC_NVAR(v, d, i)) = baseAux (*** THIS IS WRONG ! ***)
270 :     | g (TC_PRIM pt) = baseAux
271 :     | g (TC_APP(ref(_, TC_FN _, AX_NO), _)) = AX_NO
272 :     | g (TC_PROJ(ref(_, TC_SEQ _, AX_NO), _)) = AX_NO
273 :     | g (TC_APP(ref(_, TC_FN _, AX_REG(_,vs)), ts)) =
274 :     mergeAux(AX_REG(false, vs), fsmerge ts) (* ? *)
275 :     | g (TC_PROJ(ref(_, TC_SEQ _, AX_REG(_,vs)), _)) =
276 :     AX_REG(false, vs) (* ? *)
277 :     | g (TC_FN(ks, t)) = exitAux(getAux t)
278 :     | g (TC_APP(t, ts)) = fsmerge (t::ts)
279 :     | g (TC_SEQ ts) = fsmerge ts
280 :     | g (TC_PROJ(t, _)) = getAux t
281 :     | g (TC_SUM ts) = fsmerge ts
282 :     | g (TC_FIX((_,t,ts), _)) =
283 :     let val ax = getAux t
284 :     in case ax
285 :     of AX_REG(_,[]) => mergeAux(ax, fsmerge ts)
286 :     | _ => bug "unexpected TC_FIX freevars in tc_aux"
287 :     end
288 :     | g (TC_ABS t) = getAux t
289 :     | g (TC_BOX t) = getAux t
290 :     | g (TC_TUPLE (_, ts)) = fsmerge ts
291 :     | g (TC_ARROW(_, ts1, ts2)) = fsmerge (ts1@ts2)
292 :     | g (TC_PARROW(t1, t2)) = fsmerge [t1, t2]
293 :     | g (TC_CONT ts) = fsmerge ts
294 :     | g (TC_IND _) = bug "unexpected TC_IND in tc_aux"
295 :     | g (TC_ENV _) = AX_NO
296 :     in g tc
297 :     end
298 :    
299 :     fun lt_aux lt =
300 :     let fun g (LT_TYC t) = getAux t
301 :     | g (LT_STR ts) = fsmerge ts
302 :     | g (LT_PST ts) = fsmerge (map #2 ts)
303 :     | g (LT_FCT(ts1, ts2)) = fsmerge (ts1@ts2)
304 :     | g (LT_POLY(ks, ts)) = exitAux(fsmerge ts)
305 :     | g (LT_CONT ts) = fsmerge ts
306 :     | g (LT_IND _) = bug "unexpected LT_IND in lt_aux"
307 :     | g (LT_ENV _) = AX_NO
308 :     in g lt
309 :     end
310 :    
311 :     fun tk_mk (i : int, k: tkindI) = ref (i, k, AX_NO)
312 :     fun tc_mk (i : int, tc : tycI) = ref (i, tc, tc_aux tc)
313 :     fun lt_mk (i : int, lt : ltyI) = ref (i, lt, lt_aux lt)
314 :    
315 :     in
316 :    
317 :     (** a temporary hack on getting the list of free tyvars *)
318 :     fun tc_vs (r as ref(_ : int, _ : tycI, AX_NO)) = NONE
319 :     | tc_vs (r as ref(_ : int, _ : tycI, AX_REG (_,x))) = SOME x
320 :    
321 :     fun lt_vs (r as ref(_ : int, _ : ltyI, AX_NO)) = NONE
322 :     | lt_vs (r as ref(_ : int, _ : ltyI, AX_REG (_,x))) = SOME x
323 :    
324 :    
325 :     (** converting from the hash-consing reps to the standard reps *)
326 :     fun tk_outX (r as ref(_ : int, t : tkindI, _ : aux_info)) = t
327 :     fun tc_outX (r as ref(_ : int, t : tycI, _ : aux_info)) = t
328 :     fun lt_outX (r as ref(_ : int, t : ltyI, _ : aux_info)) = t
329 :    
330 :    
331 :     (** converting from the standard reps to the hash-consing reps *)
332 :     fun tk_injX t = look(tk_table, wtoi(tk_hash t), t, tkI_eq, tk_mk)
333 :     fun tc_injX t = look(tc_table, wtoi(tc_hash t), t, tcI_eq, tc_mk)
334 :     fun lt_injX t = look(lt_table, wtoi(lt_hash t), t, ltI_eq, lt_mk)
335 :    
336 :    
337 :     (** key-comparison on tkind, tyc, lty *)
338 :     fun tk_cmp (k1, k2) = cmp(tk_table, k1, k2)
339 :     fun tc_cmp (t1, t2) = cmp(tc_table, t1, t2)
340 :     fun lt_cmp (t1, t2) = cmp(lt_table, t1, t2)
341 :    
342 :    
343 :     (** get the hash key of each lty, only used by reps/coerce.sml; a hack *)
344 :     fun lt_key (ref (h : int, _ : ltyI, _ : aux_info)) = h
345 :    
346 :     (***************************************************************************
347 :     * UTILITY FUNCTIONS ON TYC ENVIRONMENT *
348 :     ***************************************************************************)
349 :    
350 :     (** utility functions for manipulating the tycEnv *)
351 :     local val tc_void = tc_injX(TC_PRIM(PT.ptc_void))
352 :     val rawtt = (true, true)
353 :     fun tc_cons (t, b) = tc_injX(TC_ARROW(rawtt, [t],[b]))
354 :     fun tc_interp x =
355 :     (case tc_outX x
356 :     of TC_PROJ(y, i) =>
357 :     (case tc_outX y of TC_SEQ ts => (SOME ts, i)
358 :     | TC_PRIM _ => (NONE, i)
359 :     | _ => bug "unexpected tycEnv1 in tc_interp")
360 :     | _ => bug "unexpected tycEnv2 in tc_interp")
361 :    
362 :     fun tc_encode(NONE, i) = tc_injX(TC_PROJ(tc_void,i))
363 :     | tc_encode(SOME ts, i) =
364 :     tc_injX(TC_PROJ(tc_injX(TC_SEQ(ts)), i))
365 :    
366 :     in
367 :    
368 :     exception tcUnbound
369 :     val initTycEnv : tycEnv = tc_void
370 :    
371 :     fun tcLookup(i, tenv : tycEnv) =
372 :     if i > 1 then
373 :     (case tc_outX tenv of TC_ARROW(_,_,[x]) => tcLookup(i-1, x)
374 :     | _ => bug "unexpected tycEnv in tcLookup")
375 :     else if i = 1 then
376 :     (case tc_outX tenv of TC_ARROW(_,[x],_) => tc_interp x
377 :     | _ => raise tcUnbound)
378 :     else bug "unexpected argument in tcLookup"
379 :    
380 :     fun tcInsert(tenv : tycEnv, et) = tc_cons(tc_encode et, tenv)
381 :    
382 :     fun tcSplit(tenv : tycEnv) =
383 :     (case tc_outX tenv of TC_ARROW(_,[x],[y]) => SOME (tc_interp x, y)
384 :     | _ => NONE)
385 :    
386 :    
387 :     end (* utililty function for tycEnv *)
388 :    
389 :    
390 :     (** checking if a tyc or an lty is in the normal form *)
391 :     fun tcp_norm ((t as ref (i, _, AX_REG(b,_))) : tyc) = b
392 :     | tcp_norm _ = false
393 :    
394 :     fun ltp_norm ((t as ref (i, _, AX_REG(b,_))) : lty) = b
395 :     | ltp_norm _ = false
396 :    
397 :    
398 :     (** utility functions for tc_env and lt_env *)
399 :     local fun tcc_env_int(x, 0, 0, te) = x
400 :     | tcc_env_int(x, i, j, te) = tc_injX(TC_ENV(x, i, j, te))
401 :    
402 :     fun ltc_env_int(x, 0, 0, te) = x
403 :     | ltc_env_int(x, i, j, te) = lt_injX(LT_ENV(x, i, j, te))
404 :    
405 :     fun withEff ([], ol, nl, tenv) = false
406 :     | withEff (a::r, ol, nl, tenv) =
407 :     let val (i, j) = tvFromInt a
408 :     val neweff =
409 :     if i > ol then (ol <> nl)
410 :     else (* case tcLookup(i, tenv)
411 :     of (NONE, n) => (nl - n) <> i
412 :     | (SOME ts, n) =>
413 :     (let val y = List.nth(ts, j)
414 :     in (case tc_outX y
415 :     of TC_VAR(ni, nj) =>
416 :     ((nj <> j) orelse ((ni+nl-n) <> i))
417 :     | _ => true)
418 :     end) *) true
419 :     in neweff orelse (withEff(r, ol, nl, tenv))
420 :     end
421 :    
422 :     in
423 :    
424 :     fun tcc_env(x, ol, nl, tenv) =
425 :     let val tvs = tc_vs x
426 :     in case tvs
427 :     of NONE => tcc_env_int(x, ol, nl, tenv)
428 :     | SOME [] => x
429 :     | SOME nvs => if withEff(nvs, ol, nl, tenv)
430 :     then tcc_env_int(x, ol, nl, tenv)
431 :     else x
432 :     end
433 :    
434 :     fun ltc_env(x, ol, nl, tenv) =
435 :     let val tvs = lt_vs x
436 :     in case tvs
437 :     of NONE => ltc_env_int(x, ol, nl, tenv)
438 :     | SOME [] => x
439 :     | SOME nvs => if withEff (nvs, ol, nl, tenv)
440 :     then ltc_env_int(x, ol, nl, tenv)
441 :     else x
442 :     end
443 :    
444 :     end (* utility functions for lt_env and tc_env *)
445 :    
446 :    
447 :     (** utility functions for updating tycs and ltys *)
448 :     fun tyc_upd (tgt as ref(i : int, old : tycI, AX_NO), nt) =
449 :     (tgt := (i, TC_IND (nt, old), AX_NO))
450 :     | tyc_upd (tgt as ref(i : int, old : tycI, x as (AX_REG(false, _))), nt) =
451 :     (tgt := (i, TC_IND (nt, old), x))
452 :     | tyc_upd _ = bug "unexpected tyc_upd on already normalized tyc"
453 :    
454 :     fun lty_upd (tgt as ref(i : int, old : ltyI, AX_NO), nt) =
455 :     (tgt := (i, LT_IND (nt, old), AX_NO))
456 :     | lty_upd (tgt as ref(i : int, old : ltyI, x as (AX_REG(false, _))), nt) =
457 :     (tgt := (i, LT_IND (nt, old), x))
458 :     | lty_upd _ = bug "unexpected lty_upd on already normalized lty"
459 :    
460 :     (***************************************************************************
461 :     * UTILITY FUNCTIONS ON REASONING ABOUT REDUCTIONS *
462 :     ***************************************************************************)
463 :    
464 :     (** a list of constructor functions *)
465 :     val tcc_var = tc_injX o TC_VAR
466 :     val tcc_fn = tc_injX o TC_FN
467 :     val tcc_app = tc_injX o TC_APP
468 :     val tcc_seq = tc_injX o TC_SEQ
469 :     val tcc_proj = tc_injX o TC_PROJ
470 :     val tcc_fix = tc_injX o TC_FIX
471 :     val tcc_abs = tc_injX o TC_ABS
472 :     val tcc_tup = tc_injX o TC_TUPLE
473 :     val tcc_parw = tc_injX o TC_PARROW
474 :     val ltc_tyc = lt_injX o LT_TYC
475 :     val ltc_str = lt_injX o LT_STR
476 :     val ltc_pst = lt_injX o LT_PST
477 :     val ltc_fct = lt_injX o LT_FCT
478 :     val ltc_poly = lt_injX o LT_POLY
479 :     val tcc_sum = tc_injX o TC_SUM
480 :    
481 :     (** the following function contains the procedure on how to
482 :     flatten the arguments and results of an arbitrary FLINT function
483 :     *)
484 :     fun isKnown tc =
485 :     (case tc_outX(tc_whnm tc)
486 :     of (TC_PRIM _ | TC_ARROW _ | TC_BOX _ | TC_ABS _ | TC_PARROW _) => true
487 :     | (TC_CONT _ | TC_FIX _ | TC_SUM _ | TC_TUPLE _) => true
488 :     | TC_APP(tc, _) => isKnown tc
489 :     | TC_PROJ(tc, _) => isKnown tc
490 :     | _ => false)
491 :    
492 :     and tc_autoflat tc =
493 :     let val ntc = tc_whnm tc
494 :     in (case tc_outX ntc
495 :     of TC_TUPLE (_, [_]) => (* singleton record is not flattened to ensure
496 :     isomorphism btw plambdatype and flinttype *)
497 :     (true, [ntc], false)
498 :     | TC_TUPLE (_, ts) =>
499 :     if length ts < 10 then (true, ts, true)
500 :     else (true, [ntc], false) (* ZHONG added the magic number 10 *)
501 :     | _ => if isKnown ntc then (true, [ntc], false)
502 :     else (false, [ntc], false))
503 :     end
504 :    
505 :     and tc_autotuple [x] = x
506 :     | tc_autotuple xs =
507 :     if length xs < 10 then tcc_tup (default_rflag, xs)
508 :     else bug "fatal error with tc_autotuple"
509 :    
510 :     and tcs_autoflat (flag, ts) =
511 :     if flag then (flag, ts)
512 :     else (case ts
513 :     of [tc] => (let val (nraw, ntcs, _) = tc_autoflat tc
514 :     in (nraw, ntcs)
515 :     end)
516 :     | _ => bug "unexpected cooked multiples in tcs_autoflat")
517 :    
518 :     and lt_autoflat lt =
519 :     (case lt_outX(lt_whnm lt)
520 :     of LT_TYC tc =>
521 :     let val (raw, ts, flag) = tc_autoflat tc
522 :     in (raw, map ltc_tyc ts, flag)
523 :     end
524 :     | _ => (true, [lt], false))
525 :    
526 :     (** a special version of tcc_arw that does automatic flattening *)
527 :     and tcc_arw (x as ((true, true), ts1, ts2)) = tc_injX (TC_ARROW x)
528 :     | tcc_arw (b as (b1, b2), ts1, ts2) =
529 :     let val (nb1, nts1) = tcs_autoflat (b1, ts1)
530 :     val (nb2, nts2) = tcs_autoflat (b2, ts2)
531 :     in tc_injX (TC_ARROW((nb1, nb2), nts1, nts2))
532 :     end
533 :    
534 :     (** tcc_wrap applies to tyc of all kinds *)
535 :     and tcc_wrap t =
536 :     let val nt = tc_whnm t
537 :     in (case tc_outX nt (* follow the kind relationship *)
538 :     of TC_SEQ ts => tcc_seq (map tcc_wrap ts)
539 :     | TC_FN(ks, tc) => tcc_fn(ks, tcc_wrap tc)
540 :     | TC_APP(t, ts) => tcc_app(tcc_wrap t, map tcc_wrap ts)
541 :     | (TC_PROJ _ | TC_VAR _ | TC_NVAR _) => nt
542 :     | TC_PRIM pt => if PT.pt_arity pt > 0 then nt else tcc_box nt
543 :     | _ => tcc_box nt)
544 :     end (* function tc_wrap *)
545 :    
546 :     (** tcc_box only applies to tyc of kind tkc_mono *)
547 :     and tcc_box t =
548 :     let val nt = tcc_uncv t (* must produce a whnm *)
549 :     in (case tc_outX nt
550 :     of (TC_VAR _ | TC_NVAR _ | TC_APP _ | TC_PROJ _) => nt
551 :     | (TC_FIX _ | TC_SUM _) => nt (* simplification here *)
552 :     | TC_PRIM pt => if PT.unboxed pt then tc_injX(TC_BOX nt) else nt
553 :     | (TC_TUPLE _ | TC_ARROW _) => tc_injX(TC_BOX nt)
554 :     | TC_BOX _ => bug "unexpected TC_BOX in tcc_box"
555 :     | (TC_SEQ _ | TC_FN _) => bug "unexpected tyc (SEQ/FN) in tcc_box"
556 :     | _ => bug "unsupported tycs in tcc_box")
557 :     end
558 :    
559 :     (** tcc_uncv is to recursively box a tyc of kind tkc_mono *)
560 :     and tcc_uncv t =
561 :     let val nt = tc_whnm t
562 :     in (case tc_outX nt
563 :     of (TC_VAR _ | TC_NVAR _ | TC_APP _ | TC_PROJ _) => nt
564 :     | (TC_FIX _ | TC_SUM _ | TC_PRIM _) => nt (* simplified here *)
565 :     | (TC_SEQ _ | TC_FN _) => bug "unexpected tyc (SEQ/FN) in tcc_box"
566 :     | TC_BOX x => x
567 :     | TC_TUPLE (rk, ts) => tcc_tup(rk, map tcc_uncv ts)
568 :     (*
569 :     | TC_ARROW ((b1,b2), ts1, ts2) =>
570 :     let val nts1 = map tcc_uncv ts1
571 :     val nts2 = map tcc_uncv ts2
572 :     val nts1 =
573 :     case (b1, ts1)
574 :     of (_, [t11, t12]) => [tcc_box t11, tcc_box t12]
575 :     | (true, _) => tcc_box(tc_autotuple ts1)
576 :     | _ => bug "not implemented"
577 :    
578 :     *)
579 :     | TC_ARROW ((true,b2), [t11,t12], ts2) =>
580 :     let val nt11 = tcc_box t11
581 :     val nt12 = tcc_box t12
582 :     val t2 = tcc_box(tc_autotuple ts2)
583 :     (* after boxing, all calling conventions are fixed ! *)
584 :     in tcc_arw((true,true),[nt11,nt12],[t2])
585 :     end
586 :     | TC_ARROW ((b1,b2), ts1, ts2) =>
587 :     let val t1 = tcc_box(tc_autotuple ts1)
588 :     val t2 = tcc_box(tc_autotuple ts2)
589 :     (* after boxing, all calling conventions are fixed ! *)
590 :     in tcc_arw((true,true),[t1],[t2])
591 :     end
592 :     | _ => bug "unsupported tycs in tcc_box")
593 :     end
594 :    
595 :     (** utility function to read the top-level of a tyc *)
596 :     and tc_lzrd t =
597 :     let fun g x =
598 :     (case tc_outX x
599 :     of TC_IND (tc, _) => g tc
600 :     | TC_ENV (tc, i, j, te) =>
601 :     let val ntc = g(h(tc, i, j, te))
602 :     in tyc_upd(x, ntc); ntc
603 :     end
604 :     | _ => x)
605 :    
606 :     and h (x, 0, 0, _) = g x
607 :     | h (x, ol, nl, tenv) =
608 :     let fun prop z = tcc_env(z, ol, nl, tenv)
609 :     in (case tc_outX x
610 :     of TC_VAR (i,j) =>
611 :     if (i <= ol) then
612 :     (let val et = tcLookup(i, tenv)
613 :     in case et
614 :     of (NONE, n) => tcc_var(nl - n, j)
615 :     | (SOME ts, n) =>
616 :     (let val y = List.nth(ts, j)
617 :     handle _ => raise tcUnbound
618 :     in h(y, 0, nl - n, initTycEnv)
619 :     end)
620 :     end)
621 :     else tcc_var(i-ol+nl, j)
622 :     | TC_NVAR _ => x
623 :     | TC_PRIM _ => x
624 :     | TC_FN (ks, tc) =>
625 :     let val tenv' = tcInsert(tenv, (NONE, nl))
626 :     in tcc_fn(ks, tcc_env(tc, ol+1, nl+1, tenv'))
627 :     end
628 :     | TC_APP (tc, tcs) => tcc_app(prop tc, map prop tcs)
629 :     | TC_SEQ tcs => tcc_seq (map prop tcs)
630 :     | TC_PROJ (tc, i) => tcc_proj(prop tc, i)
631 :     | TC_SUM tcs => tcc_sum (map prop tcs)
632 :     | TC_FIX ((n,tc,ts), i) =>
633 :     tcc_fix((n, prop tc, map prop ts), i)
634 :     | TC_ABS tc => tcc_abs (prop tc)
635 :     | TC_BOX tc => tcc_box (prop tc)
636 :     | TC_TUPLE (rk, tcs) => tcc_tup (rk, map prop tcs)
637 :     | TC_ARROW (r, ts1, ts2) =>
638 :     tcc_arw (r, map prop ts1, map prop ts2)
639 :     | TC_PARROW (t1, t2) => tcc_parw (prop t1, prop t2)
640 :     | TC_CONT _ => bug "unexpected TC_CONT in tc_lzrd"
641 :     | TC_IND (tc, _) => h(tc, ol, nl, tenv)
642 :     | TC_ENV(tc, ol', nl', tenv') =>
643 :     if ol = 0 then h(tc, ol', nl+nl', tenv')
644 :     else h(g x, ol, nl, tenv))
645 :     end (* function h *)
646 :     in if tcp_norm(t) then t else g t
647 :     end (* function tc_lzrd *)
648 :    
649 :     (** utility function to read the top-level of an lty *)
650 :     and lt_lzrd t =
651 :     let fun g x =
652 :     (case lt_outX x
653 :     of LT_IND (lt, _) => g lt
654 :     | LT_ENV(lt, i, j, te) =>
655 :     let val nlt = g(h(lt, i, j, te))
656 :     in lty_upd(x, nlt); nlt
657 :     end
658 :     | _ => x)
659 :    
660 :     and h (x, 0, 0, _) = g x
661 :     | h (x, ol, nl, tenv) =
662 :     let fun prop z = ltc_env(z, ol, nl, tenv)
663 :     in (case lt_outX x
664 :     of LT_TYC tc => ltc_tyc (tcc_env(tc, ol, nl, tenv))
665 :     | LT_STR ts => ltc_str (map prop ts)
666 :     | LT_PST its => ltc_pst (map (fn (i, t) => (i, prop t)) its)
667 :     | LT_FCT (ts1, ts2) => ltc_fct(map prop ts1, map prop ts2)
668 :     | LT_POLY (ks, ts) =>
669 :     let val tenv' = tcInsert(tenv, (NONE, nl))
670 :     in ltc_poly(ks,
671 :     map (fn t => ltc_env(t, ol+1, nl+1, tenv')) ts)
672 :     end
673 :     | LT_CONT _ => bug "unexpected LT_CONT in lt_lzrd"
674 :     | LT_IND (t, _) => h(t, ol, nl, tenv)
675 :     | LT_ENV (lt, ol', nl', tenv') =>
676 :     if ol = 0 then h(lt, ol', nl+nl', tenv')
677 :     else h(g x, ol, nl, tenv))
678 :     end (* function h *)
679 :     in if ltp_norm(t) then t else g t
680 :     end (* function lt_lzrd *)
681 :    
682 :     (** taking out the TC_IND indirection *)
683 :     and stripInd t = (case tc_outX t of TC_IND (x,_) => stripInd x | _ => t)
684 :    
685 :     (** normalizing an arbitrary tyc into a simple weak-head-normal-form *)
686 :     and tc_whnm t = if tcp_norm(t) then t else
687 :     let val nt = tc_lzrd t
688 :     in case (tc_outX nt)
689 :     of TC_APP(tc, tcs) =>
690 :     (let val tc' = tc_whnm tc
691 :     in case (tc_outX tc')
692 :     of TC_FN(ks, b) =>
693 :     let fun base () =
694 :     (b, 1, 0, tcInsert(initTycEnv,(SOME tcs, 0)))
695 :     val sp =
696 :     (case tc_outX b
697 :     of TC_ENV(b', ol', nl', te') =>
698 :     (case tcSplit te'
699 :     of SOME((NONE, n), te) =>
700 :     if (n = nl'-1) andalso (ol' > 0)
701 :     then (b', ol', n,
702 :     tcInsert(te, (SOME tcs, n)))
703 :     else base()
704 :     | _ => base())
705 :     | _ => base())
706 :     val res = tc_whnm(tcc_env sp)
707 :     in tyc_upd(nt, res); res
708 :     end
709 :     | ((TC_SEQ _) | (TC_TUPLE _) | (TC_ARROW _) | (TC_IND _)) =>
710 :     bug "unexpected tycs in tc_whnm-TC_APP"
711 :     | _ => let val xx = tcc_app(tc', tcs)
712 :     in stripInd xx
713 :     end
714 :     (*
715 :     let fun h x =
716 :     let val nx = tc_whnm x
717 :     in (case tc_outX nx
718 :     of TC_BOX z => h z
719 :     | TC_ABS z => h z
720 :     | _ => nx)
721 :     end
722 :     in tcc_app(tc', map h tcs)
723 :     end
724 :     *)
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 :     | TC_IND (tc, _) => tc_whnm tc
744 :     | TC_ENV _ => bug "unexpected TC_ENV in tc_whnm"
745 :     | _ => nt
746 :     end (* function tc_whnm *)
747 :    
748 :     (** normalizing an arbitrary lty into the simple weak-head-normal-form *)
749 :     and lt_whnm t = if ltp_norm(t) then t else
750 :     let val nt = lt_lzrd t
751 :     in case (lt_outX nt)
752 :     of LT_TYC tc => ltc_tyc(tc_whnm tc)
753 :     | _ => nt
754 :     end (* function lt_whnm *)
755 :    
756 :     (** normalizing an arbitrary tyc into the standard normal form *)
757 :     fun tc_norm t = if (tcp_norm t) then t else
758 :     let val nt = tc_whnm t
759 :     in if (tcp_norm nt) then nt
760 :     else
761 :     (let val res =
762 :     (case (tc_outX nt)
763 :     of TC_FN (ks, tc) => tcc_fn(ks, tc_norm tc)
764 :     | TC_APP (tc, tcs) =>
765 :     tcc_app(tc_norm tc, map tc_norm tcs)
766 :     | TC_SEQ tcs => tcc_seq(map tc_norm tcs)
767 :     | TC_PROJ (tc, i) => tcc_proj(tc_norm tc, i)
768 :     | TC_SUM tcs => tcc_sum (map tc_norm tcs)
769 :     | TC_FIX ((n,tc,ts), i) =>
770 :     tcc_fix((n, tc_norm tc, map tc_norm ts), i)
771 :     | TC_ABS tc => tcc_abs(tc_norm tc)
772 :     | TC_BOX tc => tcc_box(tc_norm tc)
773 :     | TC_TUPLE (rk, tcs) => tcc_tup(rk, map tc_norm tcs)
774 :     | TC_ARROW (r, ts1, ts2) =>
775 :     tcc_arw(r, map tc_norm ts1, map tc_norm ts2)
776 :     | TC_PARROW (t1, t2) => tcc_parw(tc_norm t1, tc_norm t2)
777 :     | TC_IND (tc, _) => tc_norm tc
778 :     | TC_ENV _ => bug "unexpected tycs in tc_norm"
779 :     | _ => nt)
780 :     in tyc_upd(nt, res); res
781 :     end)
782 :     end (* function tc_norm *)
783 :    
784 :     (** normalizing an arbitrary lty into the standard normal form *)
785 :     fun lt_norm t = if (ltp_norm t) then t else
786 :     let val nt = lt_lzrd t
787 :     in if (ltp_norm nt) then nt
788 :     else
789 :     (let val res =
790 :     (case lt_outX nt
791 :     of LT_TYC tc => ltc_tyc(tc_norm tc)
792 :     | LT_STR ts => ltc_str(map lt_norm ts)
793 :     | LT_PST its =>
794 :     ltc_pst(map (fn (i, t) => (i, lt_norm t)) its)
795 :     | LT_FCT (ts1, ts2) =>
796 :     ltc_fct(map lt_norm ts1, map lt_norm ts2)
797 :     | LT_POLY (ks, ts) => ltc_poly (ks, map lt_norm ts)
798 :     | LT_IND (lt, _) => lt_norm lt
799 :     | _ => bug "unexpected ltys in lt_norm")
800 :     in lty_upd(nt, res); res
801 :     end)
802 :     end (* function lt_norm *)
803 :    
804 :     (***************************************************************************
805 :     * REBINDING THE INJECTION AND PROJECTION FUNCTIONS *
806 :     ***************************************************************************)
807 :     (** converting from the standard reps to the hash-consing reps *)
808 :     val tk_inj = tk_injX
809 :     val tc_inj = tc_injX
810 :     val lt_inj = lt_injX
811 :    
812 :     (** converting from the hash-consing reps to the standard reps *)
813 :     val tk_out = tk_outX
814 :     val tc_out = tc_outX o tc_whnm
815 :     val lt_out = lt_outX o lt_whnm
816 :    
817 :     (***************************************************************************
818 :     * UTILITY FUNCTIONS ON TESTING EQUIVALENCE *
819 :     ***************************************************************************)
820 :    
821 :     (** testing the equality of values of tkind, tyc, lty *)
822 :     fun eqlist (p, x::xs, y::ys) = (p(x,y)) andalso (eqlist(p, xs, ys))
823 :     | eqlist (p, [], []) = true
824 :     | eqlist _ = false
825 :    
826 :     (** testing the "pointer" equality on normalized tkind, tyc, and lty *)
827 :     fun tk_eq (x: tkind, y) = (x = y)
828 :     fun tc_eq (x: tyc, y) = (x = y)
829 :     fun lt_eq (x: lty, y) = (x = y)
830 :    
831 :     (** testing the equivalence for arbitrary tkinds, tycs and ltys *)
832 :     val tk_eqv = tk_eq (* all tkinds are normalized *)
833 :    
834 :     (** tc_eqv_generator, invariant: t1 and t2 are in the wh-normal form *)
835 :     fun tc_eqv_gen (eqop1, eqop2, eqop3, eqop4) (t1, t2) =
836 :     (case (tc_outX t1, tc_outX t2)
837 :     of (TC_FN(ks1, b1), TC_FN(ks2, b2)) =>
838 :     (eqlist(tk_eqv, ks1, ks2)) andalso (eqop2(b1, b2))
839 :     | (TC_APP(a1, b1), TC_APP(a2, b2)) =>
840 :     (eqop1(a1, a2)) andalso (eqlist(eqop2, b1, b2))
841 :     | (TC_SEQ ts1, TC_SEQ ts2) => eqlist(eqop1, ts1, ts2)
842 :     | (TC_SUM ts1, TC_SUM ts2) => eqlist(eqop1, ts1, ts2)
843 :     | (TC_TUPLE (_, ts1), TC_TUPLE (_, ts2)) => eqlist(eqop1, ts1, ts2)
844 :     | (TC_ABS a, TC_ABS b) => eqop1(a, b)
845 :     | (TC_ABS a, _) => eqop3(a, t2)
846 :     | (_, TC_ABS b) => eqop3(t1, b)
847 :     | (TC_BOX a, TC_BOX b) => eqop1(a, b)
848 :     | (TC_BOX a, _) => eqop3(a, t2)
849 :     | (_, TC_BOX b) => eqop3(t1, b)
850 :     | (TC_PROJ(a1, i1), TC_PROJ(a2, i2)) =>
851 :     (i1 = i2) andalso (eqop1(a1, a2))
852 :     | (TC_ARROW(r1, a1, b1), TC_ARROW(r2, a2, b2)) =>
853 :     (r1 = r2) andalso (eqop4(a1, a2)) andalso (eqop4(b1, b2))
854 :     | (TC_PARROW(a1, b1), TC_PARROW(a2, b2)) =>
855 :     (eqop1(a1, a2)) andalso (eqop1(b1, b2))
856 :     | (TC_FIX((n1,tc1,ts1), i1), TC_FIX((n2,tc2,ts2), i2)) =>
857 :     true (* INCORRECT: this is temporary (ZHONG) *)
858 :     | (TC_CONT ts1, TC_CONT ts2) => eqlist(eqop1, ts1, ts2)
859 :     | _ => false)
860 :    
861 :     fun tc_eqv (x as ref (_, _, AX_REG(true, _)),
862 :     y as ref (_, _, AX_REG(true, _))) = tc_eq(x,y)
863 :     | tc_eqv (x, y) =
864 :     let val t1 = tc_whnm x
865 :     val t2 = tc_whnm y
866 :     in if (tcp_norm t1) andalso (tcp_norm t2) then tc_eq(t1, t2)
867 :     else tc_eqv_gen (tc_eqv, tc_eqv, fn _ => false,
868 :     fn (ts1, ts2) => eqlist(tc_eqv, ts1, ts2)) (t1, t2)
869 :     end (* function tc_eqv *)
870 :    
871 :     (** testing the equivalence of two tycs with relaxed constraints *)
872 :     fun tc_eqv_bx (x : tyc, y) =
873 :     let val t1 = tc_whnm x
874 :     val t2 = tc_whnm y
875 :     in (if (tcp_norm t1) andalso (tcp_norm t2) then tc_eq(t1, t2)
876 :     else false) orelse
877 :     (tc_eqv_gen (tc_eqv_bx, tc_eqv_sp, fn _ => false,
878 :     fn (ts1, ts2) => tc_eqv_bx(tc_autotuple ts1,
879 :     tc_autotuple ts2)) (t1, t2))
880 :     end (* function tc_eqv_bx *)
881 :    
882 :     and tc_eqv_sp (x : tyc, y) =
883 :     let val t1 = tc_whnm x
884 :     val t2 = tc_whnm y
885 :     in (if (tcp_norm t1) andalso (tcp_norm t2) then tc_eq(t1, t2)
886 :     else false) orelse
887 :     (tc_eqv_gen (tc_eqv_sp, tc_eqv_sp, tc_eqv_sp,
888 :     fn (ts1, ts2) => tc_eqv_sp(tc_autotuple ts1,
889 :     tc_autotuple ts2)) (t1, t2))
890 :     end (* function tc_eqv_sp *)
891 :    
892 :     (*
893 :     * all the complexity of lt_eqv comes from the partial-structure (or
894 :     * partial record) type (the LT_PST type). If we can remove LT_PST
895 :     * type, then the following can be considerabily simplified. (ZHONG)
896 :     *)
897 :    
898 :     (** lt_eqv_generator, invariant: x and y are in the wh-normal form *)
899 :     fun lt_eqv_gen (eqop1, eqop2) (x : lty, y) =
900 :     let fun sp (r, []) = true
901 :     | sp (r, (i,t)::s) =
902 :     (if (eqop1(List.nth(r,i),t))
903 :     then sp(r,s) else false) handle _ => false
904 :    
905 :     fun pp ([], _) = true
906 :     | pp (_, []) = true
907 :     | pp (a as ((i,t)::l), b as ((j,s)::r)) =
908 :     if i > j then pp(a,r)
909 :     else if i < j then pp(l,b)
910 :     else if (eqop1(t,s)) then pp(l,r) else false
911 :    
912 :     (* seq should be called if t1 and t2 are weak-head normal form *)
913 :     fun seq (t1, t2) =
914 :     (case (lt_outX t1, lt_outX t2)
915 :     of (LT_POLY(ks1, b1), LT_POLY(ks2, b2)) =>
916 :     (eqlist(tk_eqv, ks1, ks2)) andalso (eqlist(eqop1, b1, b2))
917 :     | (LT_FCT(as1, bs1), LT_FCT(as2, bs2)) =>
918 :     (eqlist(eqop1, as1, as2)) andalso (eqlist(eqop1, bs1, bs2))
919 :     | (LT_TYC a, LT_TYC b) => eqop2(a, b)
920 :     | (LT_STR s1, LT_STR s2) => eqlist(eqop1, s1, s2)
921 :     | (LT_PST s1, LT_PST s2) => pp(s1, s2)
922 :     | (LT_PST s1, LT_STR s2) => sp(s2, s1)
923 :     | (LT_STR s1, LT_PST s2) => sp(s1, s2)
924 :     | (LT_CONT s1, LT_CONT s2) => eqlist(eqop1, s1, s2)
925 :     | _ => false)
926 :     in seq(x, y)
927 :     end (* function lt_eqv_gen *)
928 :    
929 :     fun lt_eqv(x : lty, y) =
930 :     let val seq = lt_eqv_gen (lt_eqv, tc_eqv)
931 :     in if (ltp_norm x) andalso (ltp_norm y) then
932 :     (lt_eq(x, y)) orelse (seq(x, y))
933 :     else (let val t1 = lt_whnm x
934 :     val t2 = lt_whnm y
935 :     in if (ltp_norm t1) andalso (ltp_norm t2) then
936 :     (lt_eq(t1, t2)) orelse (seq(t1, t2))
937 :     else seq(t1, t2)
938 :     end)
939 :     end (* function lt_eqv *)
940 :    
941 :     fun lt_eqv_bx (x : lty, y) =
942 :     let val seq = lt_eqv_gen (lt_eqv_bx, tc_eqv_bx)
943 :     in if (ltp_norm x) andalso (ltp_norm y) then
944 :     (lt_eq(x, y)) orelse (seq(x, y))
945 :     else (let val t1 = lt_whnm x
946 :     val t2 = lt_whnm y
947 :     in if (ltp_norm t1) andalso (ltp_norm t2) then
948 :     (lt_eq(t1, t2)) orelse (seq(t1, t2))
949 :     else seq(t1, t2)
950 :     end)
951 :     end (* function lt_eqv_bx *)
952 :    
953 :     (***************************************************************************
954 :     * UTILITY FUNCTIONS ON FINDING OUT THE DEPTH OF THE FREE TYC VARIABLES *
955 :     ***************************************************************************)
956 :     (** finding out the innermost binding depth for a tyc's free variables *)
957 :     fun tc_depth (x, d) =
958 :     let val tvs = tc_vs (tc_norm x)
959 :     (* unfortunately we have to reduce everything to the normal form
960 :     before we can talk about its list of free type variables.
961 :     *)
962 :     in case tvs
963 :     of NONE => bug "unexpected case in tc_depth"
964 :     | SOME [] => DI.top
965 :     | SOME (a::_) => d + 1 - (#1(tvFromInt a))
966 :     end
967 :    
968 :     fun tcs_depth ([], d) = DI.top
969 :     | tcs_depth (x::r, d) = Int.max(tc_depth(x, d), tcs_depth(r, d))
970 :    
971 :     end (* toplevel local *)
972 :     end (* abstraction LtyKernel *)
973 :    

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