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

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