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 24 - (view) (download)
Original Path: sml/branches/SMLNJ/src/compiler/FLINT/kernel/ltykernel.sml

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

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