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/ltyextern.sml
ViewVC logotype

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

Parent Directory Parent Directory | Revision Log 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