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

Parent Directory | Revision Log

---

Revision 65 - (view) (download)

1 :	monnier	16	(* Copyright (c) 1997 YALE FLINT PROJECT *)
2 :			(* ltyextern.sml *)
3 :
4 :			structure LtyExtern : LTYEXTERN =
5 :			struct
6 :
7 :			local structure PT = PrimTyc
8 :			structure DI = DebIndex
9 :			structure LK = LtyKernel
10 :	monnier	45	structure PO = PrimOp (* really should not refer to this *)
11 :			structure FL = FLINT
12 :	monnier	16
13 :			fun bug msg = ErrorMsg.impossible("LtyExtern: "^msg)
14 :			val say = Control.Print.say
15 :
16 :			(** common utility functions *)
17 :			val tk_inj = LK.tk_inj
18 :			val tk_out = LK.tk_out
19 :
20 :			val tc_inj = LK.tc_inj
21 :			val tc_out = LK.tc_out
22 :
23 :			val lt_inj = LK.lt_inj
24 :			val lt_out = LK.lt_out
25 :
26 :			val tcc_env = LK.tcc_env
27 :			val ltc_env = LK.ltc_env
28 :			val tc_whnm = LK.tc_whnm
29 :			val lt_whnm = LK.lt_whnm
30 :			val tc_norm = LK.tc_norm
31 :			val lt_norm = LK.lt_norm
32 :
33 :			in
34 :
35 :			open LtyBasic
36 :
37 :			(** instantiating a polymorphic type or an higher-order constructor *)
38 :			fun lt_inst (lt : lty, ts : tyc list) =
39 :			let val nt = lt_whnm lt
40 :			in (case ((* lt_outX *) lt_out nt, ts)
41 :			of (LK.LT_POLY(ks, b), ts) =>
42 :	monnier	45	let val nenv = LK.tcInsert(LK.initTycEnv, (SOME ts, 0))
43 :			in map (fn x => ltc_env(x, 1, 0, nenv)) b
44 :	monnier	16	end
45 :			| (_, []) => [nt] (* this requires further clarifications !!! *)
46 :			| _ => bug "incorrect lty instantiation in lt_inst")
47 :	monnier	45	end
48 :	monnier	16
49 :	monnier	45	fun lt_pinst (lt : lty, ts : tyc list) =
50 :			(case lt_inst (lt, ts) of [y] => y | _ => bug "unexpected lt_pinst")
51 :
52 :	monnier	16	val lt_inst_st = (map lt_norm) o lt_inst (* strict instantiation *)
53 :	monnier	45	val lt_pinst_st = lt_norm o lt_pinst (* strict instantiation *)
54 :	monnier	16
55 :	league	53	(********************************************************************
56 :			* KIND-CHECKING ROUTINES *
57 :			********************************************************************)
58 :	monnier	16	exception TkTycChk
59 :			exception LtyAppChk
60 :
61 :	league	53	(* tkSubkind returns true if k1 is a subkind of k2, or if they are
62 :			* equivalent kinds. it is NOT commutative. tksSubkind is the same
63 :			* thing, component-wise on lists of kinds.
64 :			*)
65 :			fun tksSubkind (ks1, ks2) =
66 :			ListPair.all tkSubkind (ks1, ks2) (* component-wise *)
67 :			and tkSubkind (k1, k2) =
68 :			tk_eqv (k1, k2) orelse (* reflexive *)
69 :			case (tk_out k1, tk_out k2) of
70 :			(LK.TK_BOX, LK.TK_MONO) => true (* ground kinds (base case) *)
71 :			(* this next case is WRONG, but necessary until the
72 :			* infrastructure is there to give proper boxed kinds to
73 :			* certain tycons (e.g., ref : Omega -> Omega_b)
74 :			*)
75 :			| (LK.TK_MONO, LK.TK_BOX) => true
76 :			| (LK.TK_SEQ ks1, LK.TK_SEQ ks2) =>
77 :			tksSubkind (ks1, ks2)
78 :			| (LK.TK_FUN (ks1, k1'), LK.TK_FUN (ks2, k2')) =>
79 :			tksSubkind (ks1, ks2) andalso (* contravariant *)
80 :			tkSubkind (k1', k2')
81 :			| _ => false
82 :
83 :			(* is a kind monomorphic? *)
84 :			fun tkIsMono k = tkSubkind (k, tkc_mono)
85 :
86 :			(* assert that k1 is a subkind of k2 *)
87 :			fun tkAssertSubkind (k1, k2) =
88 :			if tkSubkind (k1, k2) then ()
89 :			else raise TkTycChk
90 :
91 :			(* assert that a kind is monomorphic *)
92 :			fun tkAssertIsMono k =
93 :			if tkIsMono k then ()
94 :			else raise TkTycChk
95 :
96 :			(* select the ith element from a kind sequence *)
97 :	monnier	16	fun tkSel (tk, i) =
98 :			(case (tk_out tk)
99 :			of (LK.TK_SEQ ks) => (List.nth(ks, i) handle _ => raise TkTycChk)
100 :			| _ => raise TkTycChk)
101 :
102 :	league	53	(* check the application of tycs of kinds `tks' to a type function of
103 :			* kind `tk'.
104 :			*)
105 :	monnier	45	fun tkApp (tk, tks) =
106 :			(case (tk_out tk)
107 :	league	53	of LK.TK_FUN(a, b) =>
108 :			if tksSubkind(tks, a) then b else raise TkTycChk
109 :	monnier	16	| _ => raise TkTycChk)
110 :
111 :	league	53	(* Kind-checking naturally requires traversing type graphs. to avoid
112 :			* re-traversing bits of the dag, we use a dictionary to memoize the
113 :			* kind of each tyc we process.
114 :			*
115 :			* The problem is that a tyc can have different kinds, depending on
116 :			* the valuations of its free variables. So this dictionary maps a
117 :			* tyc to an association list that maps the kinds of the free
118 :			* variables in the tyc (represented as a TK_SEQ) to the tyc's kind.
119 :	monnier	16	*)
120 :	league	53	structure Memo :> sig
121 :			type dict
122 :			val newDict : unit -> dict
123 :			val recallOrCompute : dict * tkindEnv * tyc * (unit -> tkind) -> tkind
124 :			end =
125 :			struct
126 :			structure TcDict = BinaryDict
127 :			(struct
128 :			type ord_key = tyc
129 :			val cmpKey = LK.tc_cmp
130 :			end)
131 :
132 :			type dict = (tkind * tkind) list TcDict.dict ref
133 :			val newDict : unit -> dict = ref o TcDict.mkDict
134 :
135 :			fun recallOrCompute (dict, kenv, tyc, doit) =
136 :	league	65	(* what are the valuations of tyc's free variables
137 :			* in kenv? *)
138 :	league	53	(* (might not be available for some tycs) *)
139 :	league	65	case LK.tkLookupFreeVars (kenv, tyc) of
140 :			SOME ks_fvs => let
141 :	league	53	(* encode those as a kind sequence *)
142 :			val k_fvs = tkc_seq ks_fvs
143 :			(* query the dictionary *)
144 :			val kci = case TcDict.peek(!dict, tyc) of
145 :			SOME kci => kci
146 :			| NONE => []
147 :			(* look for an equivalent environment *)
148 :			fun sameEnv (k_fvs',_) = tk_eqv(k_fvs, k_fvs')
149 :			in
150 :			case List.find sameEnv kci of
151 :			SOME (_,k) => k (* HIT! *)
152 :			| NONE => let
153 :			(* not in the list. we will compute
154 :			* the answer and cache it
155 :			*)
156 :			val k = doit()
157 :			val kci' = (k_fvs, k) :: kci
158 :			in
159 :			dict := TcDict.insert(!dict, tyc, kci');
160 :			k
161 :			end
162 :			end
163 :			| NONE =>
164 :			(* freevars were not available. we'll have to
165 :			* recompute and cannot cache the result.
166 :			*)
167 :			doit()
168 :
169 :			end (* Memo *)
170 :
171 :			(* return the kind of a given tyc in the given kind environment *)
172 :			fun tkTycGen() = let
173 :			val dict = Memo.newDict()
174 :
175 :			fun tkTyc kenv t = let
176 :			(* default recursive invocation *)
177 :			val g = tkTyc kenv
178 :			(* how to compute the kind of a tyc *)
179 :			fun mk() =
180 :			case tc_out t of
181 :			LK.TC_VAR (i, j) =>
182 :			tkLookup (kenv, i, j)
183 :			| LK.TC_NVAR _ =>
184 :			bug "TC_NVAR not supported yet in tkTyc"
185 :			| LK.TC_PRIM pt =>
186 :			tkc_int (PrimTyc.pt_arity pt)
187 :			| LK.TC_FN(ks, tc) =>
188 :			tkc_fun(ks, tkTyc (tkInsert (kenv,ks)) tc)
189 :			| LK.TC_APP (tc, tcs) =>
190 :			tkApp (g tc, map g tcs)
191 :			| LK.TC_SEQ tcs =>
192 :			tkc_seq (map g tcs)
193 :			| LK.TC_PROJ(tc, i) =>
194 :			tkSel(g tc, i)
195 :			| LK.TC_SUM tcs =>
196 :			(List.app (tkAssertIsMono o g) tcs;
197 :			tkc_mono)
198 :			| LK.TC_FIX ((n, tc, ts), i) =>
199 :			let val k = g tc
200 :			val nk =
201 :			case ts of
202 :			[] => k
203 :			| _ => tkApp(k, map g ts)
204 :			in
205 :			case (tk_out nk) of
206 :			LK.TK_FUN(a, b) =>
207 :			let val arg =
208 :			case a of
209 :			[x] => x
210 :			| _ => tkc_seq a
211 :			in
212 :			if tkSubkind(arg, b) then (* order? *)
213 :	monnier	45	(if n = 1 then b else tkSel(arg, i))
214 :	league	53	else raise TkTycChk
215 :			end
216 :			| _ => raise TkTycChk
217 :			end
218 :			| LK.TC_ABS tc =>
219 :			(tkAssertIsMono (g tc);
220 :			tkc_mono)
221 :			| LK.TC_BOX tc =>
222 :			(tkAssertIsMono (g tc);
223 :			tkc_mono)
224 :			| LK.TC_TUPLE (_,tcs) =>
225 :			(List.app (tkAssertIsMono o g) tcs;
226 :			tkc_mono)
227 :			| LK.TC_ARROW (_, ts1, ts2) =>
228 :			(List.app (tkAssertIsMono o g) ts1;
229 :			List.app (tkAssertIsMono o g) ts2;
230 :			tkc_mono)
231 :			| _ => bug "unexpected TC_ENV or TC_CONT in tkTyc"
232 :			in
233 :			Memo.recallOrCompute (dict, kenv, t, mk)
234 :			end
235 :			in
236 :			tkTyc
237 :			end
238 :	monnier	16
239 :	league	53	(* assert that the kind of `tc' is a subkind of `k' in `kenv' *)
240 :			fun tkChkGen() = let
241 :			val tkTyc = tkTycGen()
242 :			fun tkChk kenv (k, tc) =
243 :			tkAssertSubkind (tkTyc kenv tc, k)
244 :			in
245 :			tkChk
246 :			end
247 :
248 :			(* lty application with kind-checking (exported) *)
249 :			fun lt_inst_chk_gen() = let
250 :			val tkChk = tkChkGen()
251 :			fun lt_inst_chk (lt : lty, ts : tyc list, kenv : tkindEnv) =
252 :			let val nt = lt_whnm lt
253 :			in (case ((* lt_outX *) lt_out nt, ts)
254 :			of (LK.LT_POLY(ks, b), ts) =>
255 :			let val _ = ListPair.app (tkChk kenv) (ks, ts)
256 :			fun h x = ltc_env(x, 1, 0,
257 :			tcInsert(initTycEnv, (SOME ts, 0)))
258 :			in map h b
259 :			end
260 :			| (_, []) => [nt] (* ? problematic *)
261 :			| _ => raise LtyAppChk)
262 :			end
263 :			in
264 :			lt_inst_chk
265 :			end
266 :	monnier	16
267 :			(** a special lty application --- used inside the translate/specialize.sml *)
268 :			fun lt_sp_adj(ks, lt, ts, dist, bnl) =
269 :			let fun h(abslevel, ol, nl, tenv) =
270 :			if abslevel = 0 then ltc_env(lt, ol, nl, tenv)
271 :			else if abslevel > 0 then
272 :			h(abslevel-1, ol+1, nl+1, tcInsert(tenv, (NONE, nl)))
273 :			else bug "unexpected cases in ltAdjSt"
274 :
275 :			val btenv = tcInsert(initTycEnv, (SOME ts, 0))
276 :			val nt = h(dist, 1, bnl, btenv)
277 :	monnier	45	in nt (* was lt_norm nt *)
278 :	monnier	16	end
279 :
280 :			(** a special tyc application --- used inside the translate/specialize.sml *)
281 :			fun tc_sp_adj(ks, tc, ts, dist, bnl) =
282 :			let fun h(abslevel, ol, nl, tenv) =
283 :			if abslevel = 0 then tcc_env(tc, ol, nl, tenv)
284 :			else if abslevel > 0 then
285 :			h(abslevel-1, ol+1, nl+1, tcInsert(tenv, (NONE, nl)))
286 :			else bug "unexpected cases in tcAdjSt"
287 :
288 :			val btenv = tcInsert(initTycEnv, (SOME ts, 0))
289 :			val nt = h(dist, 1, bnl, btenv)
290 :	monnier	45	in nt (* was tc_norm nt *)
291 :	monnier	16	end
292 :
293 :			(** sinking the lty one-level down --- used inside the specialize.sml *)
294 :			fun lt_sp_sink (ks, lt, d, nd) =
295 :			let fun h(abslevel, ol, nl, tenv) =
296 :			if abslevel = 0 then ltc_env(lt, ol, nl, tenv)
297 :			else if abslevel > 0 then
298 :			h(abslevel-1, ol+1, nl+1, tcInsert(tenv, (NONE, nl)))
299 :			else bug "unexpected cases in ltSinkSt"
300 :			val nt = h(nd-d, 0, 1, initTycEnv)
301 :	monnier	45	in nt (* was lt_norm nt *)
302 :	monnier	16	end
303 :
304 :			(** sinking the tyc one-level down --- used inside the specialize.sml *)
305 :			fun tc_sp_sink (ks, tc, d, nd) =
306 :			let fun h(abslevel, ol, nl, tenv) =
307 :			if abslevel = 0 then tcc_env(tc, ol, nl, tenv)
308 :			else if abslevel > 0 then
309 :			h(abslevel-1, ol+1, nl+1, tcInsert(tenv, (NONE, nl)))
310 :			else bug "unexpected cases in ltSinkSt"
311 :			val nt = h(nd-d, 0, 1, initTycEnv)
312 :	monnier	45	in nt (* was tc_norm nt *)
313 :	monnier	16	end
314 :
315 :			(** utility functions used in CPS *)
316 :			fun lt_iscont lt =
317 :			(case lt_out lt
318 :			of LK.LT_CONT _ => true
319 :			| LK.LT_TYC tc =>
320 :			(case tc_out tc of LK.TC_CONT _ => true | _ => false)
321 :			| _ => false)
322 :
323 :			fun ltw_iscont (lt, f, g, h) =
324 :			(case lt_out lt
325 :			of LK.LT_CONT t => f t
326 :			| LK.LT_TYC tc =>
327 :			(case tc_out tc of LK.TC_CONT x => g x | _ => h lt)
328 :			| _ => h lt)
329 :
330 :
331 :			fun tc_bug tc s = bug (s ^ "\n\n" ^ (tc_print tc) ^ "\n\n")
332 :			fun lt_bug lt s = bug (s ^ "\n\n" ^ (lt_print lt) ^ "\n\n")
333 :
334 :			(** other misc utility functions *)
335 :			fun tc_select(tc, i) =
336 :			(case tc_out tc
337 :	monnier	45	of LK.TC_TUPLE (_,zs) =>
338 :	monnier	16	((List.nth(zs, i)) handle _ => bug "wrong TC_TUPLE in tc_select")
339 :			| _ => tc_bug tc "wrong TCs in tc_select")
340 :
341 :			fun lt_select(t, i) =
342 :			(case lt_out t
343 :			of LK.LT_STR ts =>
344 :			((List.nth(ts, i)) handle _ => bug "incorrect LT_STR in lt_select")
345 :			| LK.LT_PST ts =>
346 :			let fun h [] = bug "incorrect LT_PST in lt_select"
347 :			| h ((j,a)::r) = if i=j then a else h r
348 :			in h ts
349 :			end
350 :			| LK.LT_TYC tc => ltc_tyc(tc_select(tc, i))
351 :			| _ => bug "incorrect lambda types in lt_select")
352 :
353 :			fun tc_swap t =
354 :			(case (tc_out t)
355 :	monnier	45	of LK.TC_ARROW (LK.FF_VAR (r1,r2), [s1], [s2]) =>
356 :			tcc_arrow(LK.FF_VAR (r2,r1), [s2], [s1])
357 :			| LK.TC_ARROW (LK.FF_FIXED, [s1], [s2]) =>
358 :			tcc_arrow(LK.FF_FIXED, [s2], [s1])
359 :	monnier	16	| _ => bug "unexpected tycs in tc_swap")
360 :
361 :			fun lt_swap t =
362 :			(case (lt_out t)
363 :			of (LK.LT_POLY (ks, [x])) => ltc_poly(ks, [lt_swap x])
364 :			| (LK.LT_TYC x) => ltc_tyc(tc_swap x)
365 :			| _ => bug "unexpected type in lt_swap")
366 :
367 :	monnier	45	(** functions that manipulate the FLINT function and record types *)
368 :			fun ltc_fkfun (FL.FK_FCT, atys, rtys) =
369 :			ltc_fct (atys, rtys)
370 :			| ltc_fkfun (FL.FK_FUN {fixed, ...}, atys, rtys) =
371 :			ltc_arrow(fixed, atys, rtys)
372 :
373 :			fun ltd_fkfun lty =
374 :			if ltp_fct lty then ltd_fct lty
375 :			else let val (_, atys, rtys) = ltd_arrow lty
376 :			in (atys, rtys)
377 :			end
378 :
379 :			fun ltc_rkind (FL.RK_TUPLE _, lts) = ltc_tuple lts
380 :			| ltc_rkind (FL.RK_STRUCT, lts) = ltc_str lts
381 :			| ltc_rkind (FL.RK_VECTOR t, _) = ltc_vector (ltc_tyc t)
382 :
383 :			fun ltd_rkind (lt, i) = lt_select (lt, i)
384 :
385 :			(****************************************************************************
386 :			* THE FOLLOWING UTILITY FUNCTIONS WILL SOON BE OBSOLETE *
387 :			****************************************************************************)
388 :
389 :	monnier	16	(** a version of ltc_arrow with singleton argument and return result *)
390 :			val ltc_arw = ltc_parrow
391 :
392 :			(** not knowing what FUNCTION this is, to build a fct or an arw *)
393 :			fun ltc_fun (x, y) =
394 :			(case (lt_out x, lt_out y)
395 :			of (LK.LT_TYC _, LK.LT_TYC _) => ltc_parrow(x, y)
396 :			| _ => ltc_pfct(x, y))
397 :
398 :			(* lt_arrow used by chkflint.sml, checklty.sml, chkplexp.sml, convert.sml
399 :			* and wrapping.sml only
400 :			*)
401 :			fun lt_arrow t =
402 :			(case (lt_out t)
403 :			of (LK.LT_FCT([t1], [t2])) => (t1, t2)
404 :			| (LK.LT_FCT(_, _)) => bug "unexpected case in lt_arrow"
405 :			| (LK.LT_CONT [t]) => (t, ltc_void)
406 :			| _ => (ltd_parrow t) handle _ =>
407 :			bug ("unexpected lt_arrow --- more info: \n\n"
408 :			^ (lt_print t) ^ "\n\n"))
409 :
410 :			(* lt_arrowN used by flintnm.sml and ltysingle.sml only, should go away soon *)
411 :			fun lt_arrowN t =
412 :			(case (lt_out t)
413 :			of (LK.LT_FCT(ts1, ts2)) => (ts1, ts2)
414 :			| (LK.LT_CONT ts) => (ts, [])
415 :			| _ => (let val (_, s1, s2) = ltd_arrow t
416 :			in (s1, s2)
417 :			end))
418 :
419 :	monnier	45
420 :
421 :			(****************************************************************************
422 :			* UTILITY FUNCTIONS USED BY POST-REPRESENTATION ANALYSIS *
423 :			****************************************************************************)
424 :			(** find out what is the appropriate primop given a tyc *)
425 :			fun tc_upd_prim tc =
426 :			let fun h(LK.TC_PRIM pt) =
427 :			if PT.ubxupd pt then PO.UNBOXEDUPDATE
428 :			else if PT.bxupd pt then PO.BOXEDUPDATE
429 :			else PO.UPDATE
430 :			| h(LK.TC_TUPLE _ | LK.TC_ARROW _) = PO.BOXEDUPDATE
431 :			| h(LK.TC_FIX ((1,tc,ts), 0)) =
432 :			let val ntc = case ts of [] => tc
433 :			| _ => tcc_app(tc, ts)
434 :			in (case (tc_out ntc)
435 :			of LK.TC_FN([k],b) => h (tc_out b)
436 :			| _ => PO.UPDATE)
437 :			end
438 :			| h(LK.TC_SUM tcs) =
439 :			let fun g (a::r) = if tc_eqv(a, tcc_unit) then g r else false
440 :			| g [] = true
441 :			in if (g tcs) then PO.UNBOXEDUPDATE else PO.UPDATE
442 :			end
443 :			| h _ = PO.UPDATE
444 :			in h(tc_out tc)
445 :			end
446 :
447 :			(** tk_lty : tkind -> lty --- finds out the corresponding type for a tkind *)
448 :			fun tk_lty tk =
449 :			(case tk_out tk
450 :			of LK.TK_MONO => ltc_int
451 :			| LK.TK_BOX => ltc_int
452 :			| LK.TK_SEQ ks => ltc_tuple (map tk_lty ks)
453 :			| LK.TK_FUN (ks, k) => ltc_parrow(ltc_tuple(map tk_lty ks), tk_lty k))
454 :
455 :
456 :			(* val tnarrow_gen : unit -> ((tyc -> tyc) * (lty -> lty) * (unit->unit)) *)
457 :			fun tnarrow_gen () =
458 :			let fun tcNarrow tcf t =
459 :			(case (tc_out t)
460 :			of LK.TC_PRIM pt =>
461 :			if PT.isvoid pt then tcc_void else t
462 :			| LK.TC_TUPLE (_, tcs) => tcc_tuple (map tcf tcs)
463 :			| LK.TC_ARROW (r, ts1, ts2) =>
464 :			tcc_arrow(r, map tcf ts1, map tcf ts2)
465 :			| _ => tcc_void)
466 :
467 :			fun ltNarrow (tcf, ltf) t =
468 :			(case lt_out t
469 :			of LK.LT_TYC tc => ltc_tyc (tcf tc)
470 :			| LK.LT_STR ts => ltc_str (map ltf ts)
471 :			| LK.LT_PST its => ltc_pst (map (fn (i, t) => (i, ltf t)) its)
472 :			| LK.LT_FCT (ts1, ts2) => ltc_fct(map ltf ts1, map ltf ts2)
473 :			| LK.LT_POLY (ks, xs) =>
474 :			ltc_fct([ltc_str (map tk_lty ks)], map ltf xs)
475 :			| LK.LT_CONT _ => bug "unexpected CNTs in ltNarrow"
476 :			| LK.LT_IND _ => bug "unexpected INDs in ltNarrow"
477 :			| LK.LT_ENV _ => bug "unexpected ENVs in ltNarrow")
478 :
479 :			val {tc_map, lt_map} = LtyDict.tmemo_gen {tcf=tcNarrow, ltf=ltNarrow}
480 :			in (tc_map, lt_map, fn ()=>())
481 :			end (* function tnarrow_gen *)
482 :
483 :	monnier	16	end (* top-level local *)
484 :			end (* structure LtyExtern *)
485 :

---

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