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 197 - (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 : league 53 (********************************************************************
53 :     * KIND-CHECKING ROUTINES *
54 :     ********************************************************************)
55 : monnier 16 exception TkTycChk
56 :     exception LtyAppChk
57 :    
58 : league 53 (* tkSubkind returns true if k1 is a subkind of k2, or if they are
59 :     * equivalent kinds. it is NOT commutative. tksSubkind is the same
60 :     * thing, component-wise on lists of kinds.
61 :     *)
62 :     fun tksSubkind (ks1, ks2) =
63 :     ListPair.all tkSubkind (ks1, ks2) (* component-wise *)
64 :     and tkSubkind (k1, k2) =
65 :     tk_eqv (k1, k2) orelse (* reflexive *)
66 :     case (tk_out k1, tk_out k2) of
67 :     (LK.TK_BOX, LK.TK_MONO) => true (* ground kinds (base case) *)
68 :     (* this next case is WRONG, but necessary until the
69 :     * infrastructure is there to give proper boxed kinds to
70 :     * certain tycons (e.g., ref : Omega -> Omega_b)
71 :     *)
72 :     | (LK.TK_MONO, LK.TK_BOX) => true
73 :     | (LK.TK_SEQ ks1, LK.TK_SEQ ks2) =>
74 :     tksSubkind (ks1, ks2)
75 :     | (LK.TK_FUN (ks1, k1'), LK.TK_FUN (ks2, k2')) =>
76 :     tksSubkind (ks1, ks2) andalso (* contravariant *)
77 :     tkSubkind (k1', k2')
78 :     | _ => false
79 :    
80 :     (* is a kind monomorphic? *)
81 :     fun tkIsMono k = tkSubkind (k, tkc_mono)
82 :    
83 :     (* assert that k1 is a subkind of k2 *)
84 :     fun tkAssertSubkind (k1, k2) =
85 :     if tkSubkind (k1, k2) then ()
86 :     else raise TkTycChk
87 :    
88 :     (* assert that a kind is monomorphic *)
89 :     fun tkAssertIsMono k =
90 :     if tkIsMono k then ()
91 :     else raise TkTycChk
92 :    
93 :     (* select the ith element from a kind sequence *)
94 : monnier 16 fun tkSel (tk, i) =
95 :     (case (tk_out tk)
96 :     of (LK.TK_SEQ ks) => (List.nth(ks, i) handle _ => raise TkTycChk)
97 :     | _ => raise TkTycChk)
98 :    
99 : monnier 71 fun tks_eqv (ks1, ks2) = tk_eqv(tkc_seq ks1, tkc_seq ks2)
100 :    
101 :     fun tkApp (tk, tks) =
102 :     (case (tk_out tk)
103 :     of LK.TK_FUN(a, b) => if tks_eqv(a, tks) then b else raise TkTycChk
104 :     | _ => raise TkTycChk)
105 :    
106 : league 53 (* check the application of tycs of kinds `tks' to a type function of
107 :     * kind `tk'.
108 :     *)
109 : monnier 45 fun tkApp (tk, tks) =
110 :     (case (tk_out tk)
111 : league 53 of LK.TK_FUN(a, b) =>
112 :     if tksSubkind(tks, a) then b else raise TkTycChk
113 : monnier 16 | _ => raise TkTycChk)
114 :    
115 : league 53 (* Kind-checking naturally requires traversing type graphs. to avoid
116 :     * re-traversing bits of the dag, we use a dictionary to memoize the
117 :     * kind of each tyc we process.
118 :     *
119 :     * The problem is that a tyc can have different kinds, depending on
120 :     * the valuations of its free variables. So this dictionary maps a
121 :     * tyc to an association list that maps the kinds of the free
122 :     * variables in the tyc (represented as a TK_SEQ) to the tyc's kind.
123 : monnier 16 *)
124 : monnier 197 structure TcDict = BinaryDict
125 :     (struct
126 :     type ord_key = tyc
127 :     val cmpKey = LK.tc_cmp
128 :     end)
129 :    
130 : league 53 structure Memo :> sig
131 :     type dict
132 :     val newDict : unit -> dict
133 :     val recallOrCompute : dict * tkindEnv * tyc * (unit -> tkind) -> tkind
134 :     end =
135 :     struct
136 :     type dict = (tkind * tkind) list TcDict.dict ref
137 :     val newDict : unit -> dict = ref o TcDict.mkDict
138 :    
139 :     fun recallOrCompute (dict, kenv, tyc, doit) =
140 : league 65 (* what are the valuations of tyc's free variables
141 :     * in kenv? *)
142 : league 53 (* (might not be available for some tycs) *)
143 : league 65 case LK.tkLookupFreeVars (kenv, tyc) of
144 :     SOME ks_fvs => let
145 : league 53 (* encode those as a kind sequence *)
146 :     val k_fvs = tkc_seq ks_fvs
147 :     (* query the dictionary *)
148 :     val kci = case TcDict.peek(!dict, tyc) of
149 :     SOME kci => kci
150 :     | NONE => []
151 :     (* look for an equivalent environment *)
152 :     fun sameEnv (k_fvs',_) = tk_eqv(k_fvs, k_fvs')
153 :     in
154 :     case List.find sameEnv kci of
155 :     SOME (_,k) => k (* HIT! *)
156 :     | NONE => let
157 :     (* not in the list. we will compute
158 :     * the answer and cache it
159 :     *)
160 :     val k = doit()
161 :     val kci' = (k_fvs, k) :: kci
162 :     in
163 :     dict := TcDict.insert(!dict, tyc, kci');
164 :     k
165 :     end
166 :     end
167 :     | NONE =>
168 :     (* freevars were not available. we'll have to
169 :     * recompute and cannot cache the result.
170 :     *)
171 :     doit()
172 :    
173 :     end (* Memo *)
174 :    
175 :     (* return the kind of a given tyc in the given kind environment *)
176 :     fun tkTycGen() = let
177 :     val dict = Memo.newDict()
178 :    
179 :     fun tkTyc kenv t = let
180 :     (* default recursive invocation *)
181 :     val g = tkTyc kenv
182 :     (* how to compute the kind of a tyc *)
183 :     fun mk() =
184 :     case tc_out t of
185 :     LK.TC_VAR (i, j) =>
186 :     tkLookup (kenv, i, j)
187 :     | LK.TC_NVAR _ =>
188 :     bug "TC_NVAR not supported yet in tkTyc"
189 :     | LK.TC_PRIM pt =>
190 :     tkc_int (PrimTyc.pt_arity pt)
191 :     | LK.TC_FN(ks, tc) =>
192 :     tkc_fun(ks, tkTyc (tkInsert (kenv,ks)) tc)
193 :     | LK.TC_APP (tc, tcs) =>
194 :     tkApp (g tc, map g tcs)
195 :     | LK.TC_SEQ tcs =>
196 :     tkc_seq (map g tcs)
197 :     | LK.TC_PROJ(tc, i) =>
198 :     tkSel(g tc, i)
199 :     | LK.TC_SUM tcs =>
200 :     (List.app (tkAssertIsMono o g) tcs;
201 :     tkc_mono)
202 :     | LK.TC_FIX ((n, tc, ts), i) =>
203 :     let val k = g tc
204 :     val nk =
205 :     case ts of
206 :     [] => k
207 :     | _ => tkApp(k, map g ts)
208 :     in
209 :     case (tk_out nk) of
210 :     LK.TK_FUN(a, b) =>
211 :     let val arg =
212 :     case a of
213 :     [x] => x
214 :     | _ => tkc_seq a
215 :     in
216 :     if tkSubkind(arg, b) then (* order? *)
217 : monnier 45 (if n = 1 then b else tkSel(arg, i))
218 : league 53 else raise TkTycChk
219 :     end
220 :     | _ => raise TkTycChk
221 :     end
222 :     | LK.TC_ABS tc =>
223 :     (tkAssertIsMono (g tc);
224 :     tkc_mono)
225 :     | LK.TC_BOX tc =>
226 :     (tkAssertIsMono (g tc);
227 :     tkc_mono)
228 :     | LK.TC_TUPLE (_,tcs) =>
229 :     (List.app (tkAssertIsMono o g) tcs;
230 :     tkc_mono)
231 :     | LK.TC_ARROW (_, ts1, ts2) =>
232 :     (List.app (tkAssertIsMono o g) ts1;
233 :     List.app (tkAssertIsMono o g) ts2;
234 :     tkc_mono)
235 : monnier 71 | LK.TC_TOKEN(_, tc) =>
236 :     (tkAssertIsMono (g tc);
237 :     tkc_mono)
238 :     | LK.TC_PARROW _ => bug "unexpected TC_PARROW in tkTyc"
239 :     | LK.TC_ENV _ => bug "unexpected TC_ENV in tkTyc"
240 :     | LK.TC_IND _ => bug "unexpected TC_IND in tkTyc"
241 :     | LK.TC_CONT _ => bug "unexpected TC_CONT in tkTyc"
242 : league 53 in
243 :     Memo.recallOrCompute (dict, kenv, t, mk)
244 :     end
245 :     in
246 :     tkTyc
247 :     end
248 : monnier 16
249 : league 53 (* assert that the kind of `tc' is a subkind of `k' in `kenv' *)
250 :     fun tkChkGen() = let
251 :     val tkTyc = tkTycGen()
252 :     fun tkChk kenv (k, tc) =
253 :     tkAssertSubkind (tkTyc kenv tc, k)
254 :     in
255 :     tkChk
256 :     end
257 :    
258 :     (* lty application with kind-checking (exported) *)
259 :     fun lt_inst_chk_gen() = let
260 :     val tkChk = tkChkGen()
261 :     fun lt_inst_chk (lt : lty, ts : tyc list, kenv : tkindEnv) =
262 :     let val nt = lt_whnm lt
263 :     in (case ((* lt_outX *) lt_out nt, ts)
264 :     of (LK.LT_POLY(ks, b), ts) =>
265 :     let val _ = ListPair.app (tkChk kenv) (ks, ts)
266 :     fun h x = ltc_env(x, 1, 0,
267 :     tcInsert(initTycEnv, (SOME ts, 0)))
268 :     in map h b
269 :     end
270 :     | (_, []) => [nt] (* ? problematic *)
271 :     | _ => raise LtyAppChk)
272 :     end
273 :     in
274 :     lt_inst_chk
275 :     end
276 : monnier 16
277 :     (** a special lty application --- used inside the translate/specialize.sml *)
278 :     fun lt_sp_adj(ks, lt, ts, dist, bnl) =
279 :     let fun h(abslevel, ol, nl, tenv) =
280 :     if abslevel = 0 then ltc_env(lt, ol, nl, tenv)
281 :     else if abslevel > 0 then
282 :     h(abslevel-1, ol+1, nl+1, tcInsert(tenv, (NONE, nl)))
283 :     else bug "unexpected cases in ltAdjSt"
284 :    
285 :     val btenv = tcInsert(initTycEnv, (SOME ts, 0))
286 :     val nt = h(dist, 1, bnl, btenv)
287 : monnier 45 in nt (* was lt_norm nt *)
288 : monnier 16 end
289 :    
290 :     (** a special tyc application --- used inside the translate/specialize.sml *)
291 :     fun tc_sp_adj(ks, tc, ts, dist, bnl) =
292 :     let fun h(abslevel, ol, nl, tenv) =
293 :     if abslevel = 0 then tcc_env(tc, ol, nl, tenv)
294 :     else if abslevel > 0 then
295 :     h(abslevel-1, ol+1, nl+1, tcInsert(tenv, (NONE, nl)))
296 :     else bug "unexpected cases in tcAdjSt"
297 :    
298 :     val btenv = tcInsert(initTycEnv, (SOME ts, 0))
299 :     val nt = h(dist, 1, bnl, btenv)
300 : monnier 45 in nt (* was tc_norm nt *)
301 : monnier 16 end
302 :    
303 :     (** sinking the lty one-level down --- used inside the specialize.sml *)
304 :     fun lt_sp_sink (ks, lt, d, nd) =
305 :     let fun h(abslevel, ol, nl, tenv) =
306 :     if abslevel = 0 then ltc_env(lt, ol, nl, tenv)
307 :     else if abslevel > 0 then
308 :     h(abslevel-1, ol+1, nl+1, tcInsert(tenv, (NONE, nl)))
309 :     else bug "unexpected cases in ltSinkSt"
310 :     val nt = h(nd-d, 0, 1, initTycEnv)
311 : monnier 45 in nt (* was lt_norm nt *)
312 : monnier 16 end
313 :    
314 :     (** sinking the tyc one-level down --- used inside the specialize.sml *)
315 :     fun tc_sp_sink (ks, tc, d, nd) =
316 :     let fun h(abslevel, ol, nl, tenv) =
317 :     if abslevel = 0 then tcc_env(tc, ol, nl, tenv)
318 :     else if abslevel > 0 then
319 :     h(abslevel-1, ol+1, nl+1, tcInsert(tenv, (NONE, nl)))
320 :     else bug "unexpected cases in ltSinkSt"
321 :     val nt = h(nd-d, 0, 1, initTycEnv)
322 : monnier 45 in nt (* was tc_norm nt *)
323 : monnier 16 end
324 :    
325 :     (** utility functions used in CPS *)
326 :     fun lt_iscont lt =
327 :     (case lt_out lt
328 :     of LK.LT_CONT _ => true
329 :     | LK.LT_TYC tc =>
330 :     (case tc_out tc of LK.TC_CONT _ => true | _ => false)
331 :     | _ => false)
332 :    
333 :     fun ltw_iscont (lt, f, g, h) =
334 :     (case lt_out lt
335 :     of LK.LT_CONT t => f t
336 :     | LK.LT_TYC tc =>
337 :     (case tc_out tc of LK.TC_CONT x => g x | _ => h lt)
338 :     | _ => h lt)
339 :    
340 :    
341 :     fun tc_bug tc s = bug (s ^ "\n\n" ^ (tc_print tc) ^ "\n\n")
342 :     fun lt_bug lt s = bug (s ^ "\n\n" ^ (lt_print lt) ^ "\n\n")
343 :    
344 :     (** other misc utility functions *)
345 :     fun tc_select(tc, i) =
346 :     (case tc_out tc
347 : monnier 45 of LK.TC_TUPLE (_,zs) =>
348 : monnier 16 ((List.nth(zs, i)) handle _ => bug "wrong TC_TUPLE in tc_select")
349 :     | _ => tc_bug tc "wrong TCs in tc_select")
350 :    
351 :     fun lt_select(t, i) =
352 :     (case lt_out t
353 :     of LK.LT_STR ts =>
354 :     ((List.nth(ts, i)) handle _ => bug "incorrect LT_STR in lt_select")
355 :     | LK.LT_TYC tc => ltc_tyc(tc_select(tc, i))
356 :     | _ => bug "incorrect lambda types in lt_select")
357 :    
358 :     fun tc_swap t =
359 :     (case (tc_out t)
360 : monnier 45 of LK.TC_ARROW (LK.FF_VAR (r1,r2), [s1], [s2]) =>
361 :     tcc_arrow(LK.FF_VAR (r2,r1), [s2], [s1])
362 :     | LK.TC_ARROW (LK.FF_FIXED, [s1], [s2]) =>
363 :     tcc_arrow(LK.FF_FIXED, [s2], [s1])
364 : monnier 16 | _ => bug "unexpected tycs in tc_swap")
365 :    
366 :     fun lt_swap t =
367 :     (case (lt_out t)
368 :     of (LK.LT_POLY (ks, [x])) => ltc_poly(ks, [lt_swap x])
369 :     | (LK.LT_TYC x) => ltc_tyc(tc_swap x)
370 :     | _ => bug "unexpected type in lt_swap")
371 :    
372 : monnier 45 (** functions that manipulate the FLINT function and record types *)
373 : monnier 184 fun ltc_fkfun ({cconv=FL.CC_FCT, ...}: FL.fkind, atys, rtys) =
374 : monnier 45 ltc_fct (atys, rtys)
375 : monnier 184 | ltc_fkfun ({cconv=FL.CC_FUN fixed, ...}, atys, rtys) =
376 : monnier 45 ltc_arrow(fixed, atys, rtys)
377 :    
378 :     fun ltd_fkfun lty =
379 :     if ltp_fct lty then ltd_fct lty
380 :     else let val (_, atys, rtys) = ltd_arrow lty
381 :     in (atys, rtys)
382 :     end
383 :    
384 :     fun ltc_rkind (FL.RK_TUPLE _, lts) = ltc_tuple lts
385 :     | ltc_rkind (FL.RK_STRUCT, lts) = ltc_str lts
386 :     | ltc_rkind (FL.RK_VECTOR t, _) = ltc_vector (ltc_tyc t)
387 :    
388 :     fun ltd_rkind (lt, i) = lt_select (lt, i)
389 :    
390 :     (****************************************************************************
391 :     * UTILITY FUNCTIONS USED BY POST-REPRESENTATION ANALYSIS *
392 :     ****************************************************************************)
393 :     (** find out what is the appropriate primop given a tyc *)
394 :     fun tc_upd_prim tc =
395 :     let fun h(LK.TC_PRIM pt) =
396 :     if PT.ubxupd pt then PO.UNBOXEDUPDATE
397 :     else if PT.bxupd pt then PO.BOXEDUPDATE
398 :     else PO.UPDATE
399 :     | h(LK.TC_TUPLE _ | LK.TC_ARROW _) = PO.BOXEDUPDATE
400 :     | h(LK.TC_FIX ((1,tc,ts), 0)) =
401 :     let val ntc = case ts of [] => tc
402 :     | _ => tcc_app(tc, ts)
403 :     in (case (tc_out ntc)
404 :     of LK.TC_FN([k],b) => h (tc_out b)
405 :     | _ => PO.UPDATE)
406 :     end
407 :     | h(LK.TC_SUM tcs) =
408 :     let fun g (a::r) = if tc_eqv(a, tcc_unit) then g r else false
409 :     | g [] = true
410 :     in if (g tcs) then PO.UNBOXEDUPDATE else PO.UPDATE
411 :     end
412 :     | h _ = PO.UPDATE
413 :     in h(tc_out tc)
414 :     end
415 :    
416 :     (** tk_lty : tkind -> lty --- finds out the corresponding type for a tkind *)
417 :     fun tk_lty tk =
418 :     (case tk_out tk
419 :     of LK.TK_MONO => ltc_int
420 :     | LK.TK_BOX => ltc_int
421 :     | LK.TK_SEQ ks => ltc_tuple (map tk_lty ks)
422 : monnier 71 | LK.TK_FUN (ks, k) =>
423 :     ltc_arrow(ffc_fixed, [ltc_tuple(map tk_lty ks)], [tk_lty k]))
424 : monnier 45
425 :    
426 : monnier 71 (* tnarrow_gen : unit -> ((tyc -> tyc) * (lty -> lty) * (unit->unit)) *)
427 : monnier 45 fun tnarrow_gen () =
428 :     let fun tcNarrow tcf t =
429 :     (case (tc_out t)
430 :     of LK.TC_PRIM pt =>
431 :     if PT.isvoid pt then tcc_void else t
432 :     | LK.TC_TUPLE (_, tcs) => tcc_tuple (map tcf tcs)
433 :     | LK.TC_ARROW (r, ts1, ts2) =>
434 : monnier 71 tcc_arrow(ffc_fixed, map tcf ts1, map tcf ts2)
435 : monnier 45 | _ => tcc_void)
436 :    
437 :     fun ltNarrow (tcf, ltf) t =
438 :     (case lt_out t
439 :     of LK.LT_TYC tc => ltc_tyc (tcf tc)
440 :     | LK.LT_STR ts => ltc_str (map ltf ts)
441 :     | LK.LT_FCT (ts1, ts2) => ltc_fct(map ltf ts1, map ltf ts2)
442 :     | LK.LT_POLY (ks, xs) =>
443 :     ltc_fct([ltc_str (map tk_lty ks)], map ltf xs)
444 :     | LK.LT_CONT _ => bug "unexpected CNTs in ltNarrow"
445 :     | LK.LT_IND _ => bug "unexpected INDs in ltNarrow"
446 :     | LK.LT_ENV _ => bug "unexpected ENVs in ltNarrow")
447 :    
448 :     val {tc_map, lt_map} = LtyDict.tmemo_gen {tcf=tcNarrow, ltf=ltNarrow}
449 : monnier 71 in (tc_map o tc_norm, lt_map o lt_norm, fn ()=>())
450 : monnier 45 end (* function tnarrow_gen *)
451 :    
452 : monnier 71 (* twrap_gen : bool -> ((tyc -> tyc) * (lty -> lty) *
453 :     * (tyc -> tyc) * (lty -> lty) * (unit -> unit))
454 :     *)
455 :     fun twrap_gen bbb =
456 :     let fun tc_wmap (w, u) t =
457 :     (case (tc_out t)
458 :     of (LK.TC_VAR _ | LK.TC_NVAR _) => t
459 :     | LK.TC_PRIM pt => if PT.unboxed pt then tcc_wrap t else t
460 :     | LK.TC_FN (ks, tc) => tcc_fn(ks, w tc) (* impossible case *)
461 :     | LK.TC_APP (tc, tcs) => tcc_app(w tc, map w tcs)
462 :     | LK.TC_SEQ tcs => tcc_seq(map w tcs)
463 :     | LK.TC_PROJ (tc, i) => tcc_proj(w tc, i)
464 :     | LK.TC_SUM tcs => tcc_sum (map w tcs)
465 :     | LK.TC_FIX ((n,tc,ts), i) =>
466 :     tcc_fix((n, tc_norm (u tc), map w ts), i)
467 :    
468 :     | LK.TC_TUPLE (_, ts) => tcc_wrap(tcc_tuple (map w ts)) (* ? *)
469 :     | LK.TC_ARROW (LK.FF_VAR(b1,b2), ts1, ts2) =>
470 :     let val nts1 = (* too specific ! *)
471 :     (case ts1 of [t11,t12] => [w t11, w t12]
472 :     | _ => [w (LK.tc_autotuple ts1)])
473 :     val nts2 = [w (LK.tc_autotuple ts2)]
474 :     val nt = tcc_arrow(ffc_fixed, nts1, nts2)
475 :     in if b1 then nt else tcc_wrap nt
476 :     end
477 :     | LK.TC_ARROW (LK.FF_FIXED, _, _) =>
478 :     bug "unexpected TC_FIXED_ARROW in tc_umap"
479 :     | LK.TC_TOKEN (k, t) => bug "unexpected token tyc in tc_wmap"
480 :     | LK.TC_BOX _ => bug "unexpected TC_BOX in tc_wmap"
481 :     | LK.TC_ABS _ => bug "unexpected TC_ABS in tc_wmap"
482 :     | _ => bug "unexpected other tycs in tc_wmap")
483 :    
484 :     fun tc_umap (u, w) t =
485 :     (case (tc_out t)
486 :     of (LK.TC_VAR _ | LK.TC_NVAR _ | LK.TC_PRIM _) => t
487 :     | LK.TC_FN (ks, tc) => tcc_fn(ks, u tc) (* impossible case *)
488 :     | LK.TC_APP (tc, tcs) => tcc_app(u tc, map w tcs)
489 :     | LK.TC_SEQ tcs => tcc_seq(map u tcs)
490 :     | LK.TC_PROJ (tc, i) => tcc_proj(u tc, i)
491 :     | LK.TC_SUM tcs => tcc_sum (map u tcs)
492 :     | LK.TC_FIX ((n,tc,ts), i) =>
493 :     tcc_fix((n, tc_norm (u tc), map w ts), i)
494 :    
495 :     | LK.TC_TUPLE (rk, tcs) => tcc_tuple(map u tcs)
496 :     | LK.TC_ARROW (LK.FF_VAR(b1,b2), ts1, ts2) =>
497 :     tcc_arrow(ffc_fixed, map u ts1, map u ts2)
498 :     | LK.TC_ARROW (LK.FF_FIXED, _, _) =>
499 :     bug "unexpected TC_FIXED_ARROW in tc_umap"
500 :     | LK.TC_PARROW _ => bug "unexpected TC_PARROW in tc_umap"
501 :    
502 :     | LK.TC_BOX _ => bug "unexpected TC_BOX in tc_umap"
503 :     | LK.TC_ABS _ => bug "unexpected TC_ABS in tc_umap"
504 :     | LK.TC_TOKEN (k, t) =>
505 :     if LK.token_eq(k, LK.wrap_token) then
506 :     bug "unexpected TC_WRAP in tc_umap"
507 :     else tc_inj (LK.TC_TOKEN (k, u t))
508 :    
509 :     | _ => bug "unexpected other tycs in tc_umap")
510 :    
511 :     fun lt_umap (tcf, ltf) t =
512 :     (case (lt_out t)
513 :     of LK.LT_TYC tc => ltc_tyc (tcf tc)
514 :     | LK.LT_STR ts => ltc_str (map ltf ts)
515 :     | LK.LT_FCT (ts1, ts2) => ltc_fct(map ltf ts1, map ltf ts2)
516 :     | LK.LT_POLY (ks, xs) => ltc_poly(ks, map ltf xs)
517 :     | LK.LT_CONT _ => bug "unexpected CNTs in lt_umap"
518 :     | LK.LT_IND _ => bug "unexpected INDs in lt_umap"
519 :     | LK.LT_ENV _ => bug "unexpected ENVs in lt_umap")
520 :    
521 :     val {tc_wmap=tcWrap, tc_umap=tcMap, lt_umap=ltMap, cleanup} =
522 :     LtyDict.wmemo_gen{tc_wmap=tc_wmap, tc_umap=tc_umap, lt_umap=lt_umap}
523 :    
524 :     fun ltWrap x =
525 :     ltw_tyc (x, (fn tc => ltc_tyc (tcWrap tc)),
526 :     fn _ => bug "unexpected case in ltWrap")
527 :    
528 :     in (tcWrap o tc_norm, ltWrap o lt_norm,
529 :     tcMap o tc_norm, ltMap o lt_norm, cleanup)
530 :     end
531 :    
532 :    
533 : monnier 197 (************************************************************************
534 :     * SUBSTITION OF NAMED VARS IN A TYC/LTY *
535 :     ************************************************************************)
536 :     structure LtDict = BinaryDict
537 :     (struct
538 :     type ord_key = lty
539 :     val cmpKey = LtyKernel.lt_cmp
540 :     end)
541 :    
542 :     fun tc_nvar_elim_gen() = let
543 :     val dict = ref (TcDict.mkDict())
544 :    
545 :     fun tc_nvar_elim s d tyc =
546 :     case LK.tc_nvars tyc of
547 :     [] => tyc (* nothing to elim *)
548 :     | _ =>
549 :     let
550 :     (* encode the tyc and the depth for memoization
551 :     * using tcc_proj *)
552 :     val tycdepth = tcc_proj (tyc, d)
553 :     in
554 :     case TcDict.peek(!dict, tycdepth) of
555 :     SOME t => t (* hit! *)
556 :     | NONE => let (* must recompute *)
557 :     val r = tc_nvar_elim s d (* default recursive invoc. *)
558 :     val rs = map r (* recursive invocation on list *)
559 :     val t =
560 :     case tc_out tyc of
561 :     LK.TC_NVAR tvar =>
562 :     (case s (tvar, d) of
563 :     SOME t => t
564 :     | NONE => tyc)
565 :     | LK.TC_VAR _ => tyc
566 :     | LK.TC_PRIM _ => tyc
567 :     | LK.TC_FN (tks, t) =>
568 :     tcc_fn (tks, tc_nvar_elim s (DI.next d) t)
569 :     | LK.TC_APP (t, ts) =>
570 :     tcc_app (r t, rs ts)
571 :     | LK.TC_SEQ ts =>
572 :     tcc_seq (rs ts)
573 :     | LK.TC_PROJ (t, i) =>
574 :     tcc_proj (r t, i)
575 :     | LK.TC_SUM ts =>
576 :     tcc_sum (rs ts)
577 :     | LK.TC_FIX ((i,t,ts),j) =>
578 :     tcc_fix ((i, r t, rs ts), j)
579 :     | LK.TC_TUPLE (rf,ts) =>
580 :     tcc_tuple (rs ts)
581 :     | LK.TC_ARROW (ff, ts, ts') =>
582 :     tcc_arrow (ff, rs ts, rs ts')
583 :     | LK.TC_PARROW (t, t') =>
584 :     tcc_parrow (r t, r t')
585 :     | LK.TC_BOX t =>
586 :     tcc_box (r t)
587 :     | LK.TC_ABS t =>
588 :     tcc_abs (r t)
589 :     | LK.TC_TOKEN (tok, t) =>
590 :     tc_inj (LK.TC_TOKEN (tok, r t))
591 :     | LK.TC_CONT ts =>
592 :     tcc_cont (rs ts)
593 :     | LK.TC_IND _ =>
594 :     bug "unexpected TC_IND in tc_nvar_elim"
595 :     | LK.TC_ENV _ =>
596 :     bug "unexpected TC_ENV in tc_nvar_elim"
597 :     in
598 :     dict := TcDict.insert(!dict, tycdepth, t);
599 :     t
600 :     end
601 :     end (* tc_nvar_elim *)
602 :     in
603 :     tc_nvar_elim
604 :     end
605 :    
606 :     fun lt_nvar_elim_gen() = let
607 :     val dict = ref (LtDict.mkDict())
608 :     val tc_nvar_elim = tc_nvar_elim_gen()
609 :    
610 :     fun lt_nvar_elim s d lty =
611 :     case LK.lt_nvars lty of
612 :     [] => lty (* nothing to elim *)
613 :     | _ =>
614 :     let
615 :     (* encode the lty and depth info using LT_ENV
616 :     * (only first 2 args are useful) *)
617 :     val ltydepth = lt_inj (LK.LT_ENV (lty, d, 0, LK.initTycEnv))
618 :     in
619 :     case LtDict.peek(!dict, ltydepth) of
620 :     SOME t => t (* hit! *)
621 :     | NONE => let (* must recompute *)
622 :     val r = lt_nvar_elim s d (* default recursive invoc. *)
623 :     val rs = map r (* recursive invocation on list *)
624 :     val t =
625 :     case lt_out lty of
626 :     LK.LT_TYC t =>
627 :     ltc_tyc (tc_nvar_elim s d t)
628 :     | LK.LT_STR ts =>
629 :     ltc_str (rs ts)
630 :     | LK.LT_FCT (ts, ts') =>
631 :     ltc_fct (rs ts, rs ts')
632 :     | LK.LT_POLY (tks, ts) =>
633 :     ltc_poly (tks,
634 :     map (lt_nvar_elim s (DI.next d)) ts)
635 :     | LK.LT_CONT ts =>
636 :     ltc_cont (rs ts)
637 :     | LK.LT_IND _ =>
638 :     bug "unexpected LT_IND in lt_nvar_elim"
639 :     | LK.LT_ENV _ =>
640 :     bug "unexpected LT_ENV in lt_nvar_elim"
641 :     in
642 :     dict := LtDict.insert(!dict, ltydepth, t);
643 :     t
644 :     end
645 :     end (* lt_nvar_elim *)
646 :     in
647 :     lt_nvar_elim
648 :     end (* lt_nvar_elim_gen *)
649 :    
650 :     (************************************************************)
651 :    
652 :     type smap = (tvar * tyc) list
653 :    
654 :     (* is the intersection of two sorted lists non-nil? *)
655 :     fun intersectionNonEmpty(nil,_:tvar list) = false
656 :     | intersectionNonEmpty(_,nil) = false
657 :     | intersectionNonEmpty(s1 as (h1:tvar,_)::t1, s2 as h2::t2) =
658 :     case Int.compare (h1, h2) of
659 :     LESS => intersectionNonEmpty(t1, s2)
660 :     | GREATER => intersectionNonEmpty(s1, t2)
661 :     | EQUAL => true
662 :    
663 :     fun searchSubst (tv:tvar, s) =
664 :     let fun h [] = NONE
665 :     | h ((tv':tvar,tyc)::s) =
666 :     case Int.compare (tv, tv') of
667 :     LESS => NONE
668 :     | GREATER => h s
669 :     | EQUAL => SOME tyc
670 :     in h s
671 :     end
672 :    
673 :     fun tc_nvar_subst_gen() = let
674 :     val dict = ref (TcDict.mkDict())
675 :    
676 :     fun tc_nvar_subst subst = let
677 :     fun loop tyc =
678 :     (* check if substitution overlaps with free vars list *)
679 :     (case intersectionNonEmpty(subst, LK.tc_nvars tyc) of
680 :     false => tyc (* nothing to subst *)
681 :     | true =>
682 :     (* next check the memoization table *)
683 :     (case TcDict.peek(!dict, tyc) of
684 :     SOME t => t (* hit! *)
685 :     | NONE =>
686 :     let (* must recompute *)
687 :     val t =
688 :     case tc_out tyc of
689 :     LK.TC_NVAR tv =>
690 :     (case searchSubst(tv,subst) of
691 :     SOME t => t
692 :     | NONE => tyc
693 :     )
694 :     | LK.TC_VAR _ => tyc
695 :     | LK.TC_PRIM _ => tyc
696 :     | LK.TC_FN (tks, t) =>
697 :     tcc_fn (tks, loop t)
698 :     | LK.TC_APP (t, ts) =>
699 :     tcc_app (loop t, map loop ts)
700 :     | LK.TC_SEQ ts =>
701 :     tcc_seq (map loop ts)
702 :     | LK.TC_PROJ (t, i) =>
703 :     tcc_proj (loop t, i)
704 :     | LK.TC_SUM ts =>
705 :     tcc_sum (map loop ts)
706 :     | LK.TC_FIX ((i,t,ts),j) =>
707 :     tcc_fix ((i, loop t, map loop ts), j)
708 :     | LK.TC_TUPLE (rf,ts) =>
709 :     tcc_tuple (map loop ts)
710 :     | LK.TC_ARROW (ff, ts, ts') =>
711 :     tcc_arrow (ff, map loop ts, map loop ts')
712 :     | LK.TC_PARROW (t, t') =>
713 :     tcc_parrow (loop t, loop t')
714 :     | LK.TC_BOX t =>
715 :     tcc_box (loop t)
716 :     | LK.TC_ABS t =>
717 :     tcc_abs (loop t)
718 :     | LK.TC_TOKEN (tok, t) =>
719 :     tc_inj (LK.TC_TOKEN (tok, loop t))
720 :     | LK.TC_CONT ts =>
721 :     tcc_cont (map loop ts)
722 :     | LK.TC_IND _ =>
723 :     bug "unexpected TC_IND in substTyc"
724 :     | LK.TC_ENV _ =>
725 :     bug "unexpected TC_ENV in substTyc"
726 :     in
727 :     (* update memoization table *)
728 :     dict := TcDict.insert(!dict, tyc, t);
729 :     t
730 :     end
731 :     )) (* end cases *)
732 :     in loop
733 :     end (* tc_nvar_subst *)
734 :     in tc_nvar_subst
735 :     end (* tc_nvar_subst_gen *)
736 :    
737 :     fun lt_nvar_subst_gen() = let
738 :     val dict = ref (LtDict.mkDict())
739 :     val tc_nvar_subst' = tc_nvar_subst_gen()
740 :    
741 :     fun lt_nvar_subst subst = let
742 :     val tc_nvar_subst = tc_nvar_subst' subst
743 :    
744 :     fun loop lty =
745 :     (* check if there are any free type variables first *)
746 :     (case intersectionNonEmpty(subst, LK.lt_nvars lty) of
747 :     false => lty (* nothing to subst *)
748 :     | true =>
749 :     (* next check the memoization table *)
750 :     (case LtDict.peek(!dict, lty) of
751 :     SOME t => t (* hit! *)
752 :     | NONE =>
753 :     let (* must recompute *)
754 :     val t =
755 :     case lt_out lty of
756 :     LK.LT_TYC t =>
757 :     ltc_tyc (tc_nvar_subst t)
758 :     | LK.LT_STR ts =>
759 :     ltc_str (map loop ts)
760 :     | LK.LT_FCT (ts, ts') =>
761 :     ltc_fct (map loop ts, map loop ts')
762 :     | LK.LT_POLY (tks, ts) =>
763 :     ltc_poly (tks, map loop ts)
764 :     | LK.LT_CONT ts =>
765 :     ltc_cont (map loop ts)
766 :     | LK.LT_IND _ =>
767 :     bug "unexpected LT_IND in lt_nvar_elim"
768 :     | LK.LT_ENV _ =>
769 :     bug "unexpected LT_ENV in lt_nvar_elim"
770 :     in
771 :     (* update memoization table *)
772 :     dict := LtDict.insert(!dict, lty, t);
773 :     t
774 :     end
775 :     )) (* end cases *)
776 :     in loop
777 :     end (* lt_nvar_subst *)
778 :     in lt_nvar_subst
779 :     end (* lt_nvar_subst_gen *)
780 :    
781 :     (************************************************************)
782 :    
783 :     (** building up a polymorphic type by abstracting over a
784 :     ** list of named vars
785 :     **)
786 :     type tvoffs = (tvar * int) list
787 :    
788 :     fun intersect(nil, _:tvar list) = nil
789 :     | intersect(_, nil) = nil
790 :     | intersect(s1 as (h1:tvar,n)::t1, s2 as h2::t2) =
791 :     case Int.compare (h1, h2) of
792 :     LESS => intersect(t1, s2)
793 :     | GREATER => intersect(s1, t2)
794 :     | EQUAL => (h1,n) :: intersect(t1, t2)
795 :    
796 :     val s_iter = Stats.makeStat "Cvt Iterations"
797 :     val s_hits = Stats.makeStat "Cvt Hits in dict"
798 :     val s_cuts = Stats.makeStat "Cvt Freevar cutoffs"
799 :    
800 :     val s_tvoffs = Stats.makeStat "Cvt tvoffs length"
801 :     val s_nvars = Stats.makeStat "Cvt free nvars length"
802 :    
803 :     fun tc_nvar_cvt_gen() = let
804 :     val dict = ref (TcDict.mkDict())
805 :    
806 :     fun tc_nvar_cvt (tvoffs:tvoffs) d tyc =
807 :     (Stats.addStat s_iter 1;
808 :     Stats.addStat s_tvoffs (length tvoffs);
809 :     Stats.addStat s_nvars (length (LK.tc_nvars tyc));
810 :     (* check if substitution overlaps with free vars list *)
811 :     case intersect(tvoffs, LK.tc_nvars tyc) of
812 :     [] => (Stats.addStat s_cuts 1;
813 :     tyc (* nothing to cvt *)
814 :     )
815 :     | tvoffs =>
816 :     let
817 :     (* encode the tyc and the depth for memoization
818 :     * using tcc_proj *)
819 :     val tycdepth = tcc_proj (tyc, d)
820 :     in
821 :     case TcDict.peek(!dict, tycdepth) of
822 :     SOME t => (Stats.addStat s_hits 1;
823 :     t (* hit! *)
824 :     )
825 :     | NONE => let (* must recompute *)
826 :     val r = tc_nvar_cvt tvoffs d (* default recursive invoc. *)
827 :     val rs = map r (* recursive invocation on list *)
828 :     val t =
829 :     case tc_out tyc of
830 :     LK.TC_NVAR tvar =>
831 :     (case searchSubst(tvar,tvoffs) of
832 :     SOME i => tcc_var (d, i)
833 :     | NONE => tyc)
834 :     | LK.TC_VAR _ => tyc
835 :     | LK.TC_PRIM _ => tyc
836 :     | LK.TC_FN (tks, t) =>
837 :     tcc_fn (tks, tc_nvar_cvt tvoffs (DI.next d) t)
838 :     | LK.TC_APP (t, ts) =>
839 :     tcc_app (r t, rs ts)
840 :     | LK.TC_SEQ ts =>
841 :     tcc_seq (rs ts)
842 :     | LK.TC_PROJ (t, i) =>
843 :     tcc_proj (r t, i)
844 :     | LK.TC_SUM ts =>
845 :     tcc_sum (rs ts)
846 :     | LK.TC_FIX ((i,t,ts),j) =>
847 :     tcc_fix ((i, r t, rs ts), j)
848 :     | LK.TC_TUPLE (rf,ts) =>
849 :     tcc_tuple (rs ts)
850 :     | LK.TC_ARROW (ff, ts, ts') =>
851 :     tcc_arrow (ff, rs ts, rs ts')
852 :     | LK.TC_PARROW (t, t') =>
853 :     tcc_parrow (r t, r t')
854 :     | LK.TC_BOX t =>
855 :     tcc_box (r t)
856 :     | LK.TC_ABS t =>
857 :     tcc_abs (r t)
858 :     | LK.TC_TOKEN (tok, t) =>
859 :     tc_inj (LK.TC_TOKEN (tok, r t))
860 :     | LK.TC_CONT ts =>
861 :     tcc_cont (rs ts)
862 :     | LK.TC_IND _ =>
863 :     bug "unexpected TC_IND in tc_nvar_cvt"
864 :     | LK.TC_ENV _ =>
865 :     bug "unexpected TC_ENV in tc_nvar_cvt"
866 :     in
867 :     dict := TcDict.insert(!dict, tycdepth, t);
868 :     t
869 :     end
870 :     end (* tc_nvar_cvt *)
871 :     )
872 :     in
873 :     tc_nvar_cvt
874 :     end (* tc_nvar_cvt_gen *)
875 :    
876 :    
877 :     fun lt_nvar_cvt_gen() = let
878 :     val dict = ref (LtDict.mkDict())
879 :     val tc_nvar_cvt = tc_nvar_cvt_gen()
880 :    
881 :     fun lt_nvar_cvt tvoffs d lty =
882 :     (* check if substitution overlaps with free vars list *)
883 :     case intersect(tvoffs, LK.lt_nvars lty) of
884 :     [] => lty (* nothing to cvt *)
885 :     | tvoffs =>
886 :     let
887 :     (* encode the lty and depth info using LT_ENV
888 :     * (only first 2 args are useful) *)
889 :     val ltydepth = lt_inj (LK.LT_ENV (lty, d, 0, LK.initTycEnv))
890 :     in
891 :     case LtDict.peek(!dict, ltydepth) of
892 :     SOME t => t (* hit! *)
893 :     | NONE => let (* must recompute *)
894 :     val r = lt_nvar_cvt tvoffs d (* default recursive invoc. *)
895 :     val rs = map r (* recursive invocation on list *)
896 :     val t =
897 :     case lt_out lty of
898 :     LK.LT_TYC t =>
899 :     ltc_tyc (tc_nvar_cvt tvoffs d t)
900 :     | LK.LT_STR ts =>
901 :     ltc_str (rs ts)
902 :     | LK.LT_FCT (ts, ts') =>
903 :     ltc_fct (rs ts, rs ts')
904 :     | LK.LT_POLY (tks, ts) =>
905 :     ltc_poly (tks,
906 :     map (lt_nvar_cvt tvoffs (DI.next d)) ts)
907 :     | LK.LT_CONT ts =>
908 :     ltc_cont (rs ts)
909 :     | LK.LT_IND _ =>
910 :     bug "unexpected LT_IND in lt_nvar_cvt"
911 :     | LK.LT_ENV _ =>
912 :     bug "unexpected LT_ENV in lt_nvar_cvt"
913 :     in
914 :     dict := LtDict.insert(!dict, ltydepth, t);
915 :     t
916 :     end
917 :     end (* lt_nvar_cvt *)
918 :     in
919 :     lt_nvar_cvt
920 :     end (* lt_nvar_cvt_gen *)
921 :    
922 :    
923 : monnier 16 end (* top-level local *)
924 :     end (* structure LtyExtern *)
925 :    
926 : monnier 95
927 :     (*
928 : monnier 118 * $Log$
929 : monnier 95 *)

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