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

Parent Directory | Revision Log

---

Revision 76 - (view) (download)

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

---

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