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 102 - (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 : league 53 structure Memo :> sig
125 :     type dict
126 :     val newDict : unit -> dict
127 :     val recallOrCompute : dict * tkindEnv * tyc * (unit -> tkind) -> tkind
128 :     end =
129 :     struct
130 :     structure TcDict = BinaryDict
131 :     (struct
132 :     type ord_key = tyc
133 :     val cmpKey = LK.tc_cmp
134 :     end)
135 :    
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 :     fun ltc_fkfun (FL.FK_FCT, atys, rtys) =
374 :     ltc_fct (atys, rtys)
375 :     | ltc_fkfun (FL.FK_FUN {fixed, ...}, atys, rtys) =
376 :     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 16 end (* top-level local *)
534 :     end (* structure LtyExtern *)
535 :    
536 : monnier 95
537 :     (*
538 :     * $Log: ltyextern.sml,v $
539 :     * Revision 1.1.1.1 1998/04/08 18:39:40 george
540 :     * Version 110.5
541 :     *
542 :     *)

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