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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 46 - (view) (download)

1 : monnier 16 (* Copyright (c) 1997 YALE FLINT PROJECT *)
2 :     (* ltydef.sml *)
3 :    
4 :     structure LtyDef : LTYDEF =
5 :     struct
6 :    
7 :     local structure PT = PrimTyc
8 :     structure DI = DebIndex
9 :     structure LK = LtyKernel
10 :    
11 :     fun bug msg = ErrorMsg.impossible("LtyDef: "^msg)
12 :     val say = Control.Print.say
13 :    
14 :     (** common utility functions *)
15 :     val tk_inj = LK.tk_inj
16 :     val tk_out = LK.tk_out
17 :     val tk_eqv = LK.tk_eqv
18 :    
19 :     val tc_inj = LK.tc_inj
20 :     val tc_out = LK.tc_out
21 :     val tc_eqv = LK.tc_eqv
22 :    
23 :     val lt_inj = LK.lt_inj
24 :     val lt_out = LK.lt_out
25 :     val lt_eqv = LK.lt_eqv
26 :    
27 :     in
28 :    
29 :     (** basic entities *)
30 :     type index = DI.index
31 :     type depth = DI.depth
32 :     type primtyc = PT.primtyc
33 :     type tvar = LK.tvar
34 : monnier 45
35 :     type fflag = LK.fflag
36 :     type rflag = LK.rflag
37 :    
38 :     type tkind = LK.tkind
39 : monnier 16 type tyc = LK.tyc
40 :     type lty = LK.lty
41 :    
42 :     (*
43 :     * FLINT tkind is roughly equivalent to the following ML datatype
44 :     *
45 :     * datatype tkind
46 :     * = TK_MONO
47 :     * | TK_BOX
48 :     * | TK_SEQ of tkind list
49 : monnier 45 * | TK_FUN of tkind list * tkind
50 : monnier 16 *
51 :     * We treat tkind as an abstract type so we can no longer use
52 :     * pattern matching.
53 :     *)
54 :    
55 :     (** tkind constructors *)
56 :     val tkc_mono : tkind = tk_inj (LK.TK_MONO)
57 :     val tkc_box : tkind = tk_inj (LK.TK_BOX)
58 :     val tkc_seq : tkind list -> tkind = tk_inj o LK.TK_SEQ
59 : monnier 45 val tkc_fun : tkind list * tkind -> tkind = tk_inj o LK.TK_FUN
60 : monnier 16
61 :     (** tkind deconstructors *)
62 :     val tkd_mono : tkind -> unit = fn _ => ()
63 :     val tkd_box : tkind -> unit = fn _ => ()
64 :     val tkd_seq : tkind -> tkind list = fn tk =>
65 :     (case tk_out tk of LK.TK_SEQ x => x
66 :     | _ => bug "unexpected tkind in tkd_seq")
67 : monnier 45 val tkd_fun : tkind -> tkind list * tkind = fn tk =>
68 : monnier 16 (case tk_out tk of LK.TK_FUN x => x
69 :     | _ => bug "unexpected tkind in tkd_fun")
70 :    
71 :     (** tkind predicates *)
72 :     val tkp_mono : tkind -> bool = fn tk => tk_eqv(tk, tkc_mono)
73 :     val tkp_box : tkind -> bool = fn tk => tk_eqv(tk, tkc_box)
74 :     val tkp_seq : tkind -> bool = fn tk =>
75 :     (case tk_out tk of LK.TK_SEQ _ => true | _ => false)
76 :     val tkp_fun : tkind -> bool = fn tk =>
77 :     (case tk_out tk of LK.TK_FUN _ => true | _ => false)
78 :    
79 :     (** tkind one-arm switches *)
80 :     fun tkw_mono (tk, f, g) = if tk_eqv(tk, tkc_mono) then f () else g tk
81 :     fun tkw_box (tk, f, g) = if tk_eqv(tk, tkc_box) then f () else g tk
82 :     fun tkw_seq (tk, f, g) =
83 :     (case tk_out tk of LK.TK_SEQ x => f x | _ => g tk)
84 :     fun tkw_fun (tk, f, g) =
85 :     (case tk_out tk of LK.TK_FUN x => f x | _ => g tk)
86 :    
87 :    
88 :     (*
89 : monnier 45 * FLINT fflag and rflag are used to classify different kinds of monomorphic
90 :     * functions and records. As of now, they are roughly equivalent to:
91 :     *
92 :     * datatype fflag
93 :     * = FF_VAR of bool * bool
94 :     * | FF_FIXED
95 :     *
96 :     * datatype rflag = RF_TMP
97 :     *
98 :     * We treat both as abstract types so pattern matching no longer applies.
99 :     * NOTE: FF_VAR flags are used by FLINTs before we perform representation
100 :     * analysis while FF_FIXED is used by FLINTs after we perform representation
101 :     * analysis.
102 :     *)
103 :    
104 :     (** fflag and rflag constructors *)
105 :     val ffc_var : bool * bool -> fflag = fn x => LK.FF_VAR x
106 :     val ffc_fixed : fflag = LK.FF_FIXED
107 :     val rfc_tmp : rflag = LK.RF_TMP
108 :    
109 :     (** fflag and rflag deconstructors *)
110 :     val ffd_var : fflag -> bool * bool = fn x =>
111 :     (case x of LK.FF_VAR x => x | _ => bug "unexpected fflag in ffd_var")
112 :     val ffd_fixed : fflag -> unit = fn x =>
113 :     (case x of LK.FF_FIXED => () | _ => bug "unexpected fflag in ffd_fixed")
114 :     val rfd_tmp : rflag -> unit = fn (LK.RF_TMP) => ()
115 :    
116 :     (** fflag and rflag predicates *)
117 :     val ffp_var : fflag -> bool = fn x =>
118 :     (case x of LK.FF_VAR _ => true | _ => false)
119 :     val ffp_fixed : fflag -> bool = fn x =>
120 :     (case x of LK.FF_FIXED => true | _ => false)
121 :     val rfp_tmp : rflag -> bool = fn (LK.RF_TMP) => true
122 :    
123 :     (** fflag and rflag one-arm switch *)
124 :     fun ffw_var (ff, f, g) =
125 :     (case ff of LK.FF_VAR x => f x | _ => g ff)
126 :     fun ffw_fixed (ff, f, g) =
127 :     (case ff of LK.FF_FIXED => f () | _ => g ff)
128 :     fun rfw_tmp (rf, f, g) = f()
129 :    
130 :    
131 :     (*
132 : monnier 16 * FLINT tyc is roughly equivalent to the following ML datatype
133 :     *
134 :     * datatype tyc
135 :     * = TC_VAR of index * int
136 : monnier 45 * | TC_NVAR of tvar * depth * int (* NOT USED *)
137 : monnier 16 * | TC_PRIM of primtyc
138 :     * | TC_FN of tkind list * tyc
139 :     * | TC_APP of tyc * tyc list
140 :     * | TC_SEQ of tyc list
141 :     * | TC_PROJ of tyc * int
142 :     * | TC_SUM of tyc list
143 :     * | TC_FIX of tyc * int
144 : monnier 45 * | TC_WRAP of tyc (* used after rep. analysis only *)
145 :     * | TC_ABS of tyc (* NOT USED *)
146 :     * | TC_BOX of tyc (* NOT USED *)
147 :     * | TC_TUPLE of tyc list (* rflag hidden *)
148 :     * | TC_ARROW of fflag * tyc list * tyc list
149 : monnier 16 *
150 :     * We treat tyc as an abstract type so we can no longer use
151 :     * pattern matching. Type applications (TC_APP) and projections
152 :     * (TC_PROJ) are automatically reduced as needed, that is, the
153 :     * client does not need to worry about whether a tyc is in the
154 :     * normal form or not, all functions defined here automatically
155 :     * take care of this.
156 :     *)
157 :    
158 :     (** tyc constructors *)
159 :     val tcc_var : index * int -> tyc = tc_inj o LK.TC_VAR
160 :     val tcc_nvar : tvar * depth * int -> tyc = tc_inj o LK.TC_NVAR
161 :     val tcc_prim : primtyc -> tyc = tc_inj o LK.TC_PRIM
162 :     val tcc_fn : tkind list * tyc -> tyc = tc_inj o LK.TC_FN
163 :     val tcc_app : tyc * tyc list -> tyc = tc_inj o LK.TC_APP
164 :     val tcc_seq : tyc list -> tyc = tc_inj o LK.TC_SEQ
165 :     val tcc_proj : tyc * int -> tyc = tc_inj o LK.TC_PROJ
166 :     val tcc_sum : tyc list -> tyc = tc_inj o LK.TC_SUM
167 :     val tcc_fix : (int * tyc * tyc list) * int -> tyc = tc_inj o LK.TC_FIX
168 : monnier 45 val tcc_wrap : tyc -> tyc = fn tc => tc_inj (LK.TC_TOKEN(LK.wrap_token, tc))
169 : monnier 16 val tcc_abs : tyc -> tyc = tc_inj o LK.TC_ABS
170 : monnier 45 val tcc_box : tyc -> tyc = tc_inj o LK.TC_BOX
171 :     val tcc_tuple : tyc list -> tyc = fn ts => tc_inj (LK.TC_TUPLE (rfc_tmp, ts))
172 :     val tcc_arrow : fflag * tyc list * tyc list -> tyc = LK.tcc_arw
173 : monnier 16
174 :     (** tyc deconstructors *)
175 :     val tcd_var : tyc -> index * int = fn tc =>
176 :     (case tc_out tc of LK.TC_VAR x => x
177 :     | _ => bug "unexpected tyc in tcd_var")
178 :     val tcd_nvar : tyc -> tvar * depth * int = fn tc =>
179 :     (case tc_out tc of LK.TC_NVAR x => x
180 :     | _ => bug "unexpected tyc in tcd_nvar")
181 :     val tcd_prim : tyc -> primtyc = fn tc =>
182 :     (case tc_out tc of LK.TC_PRIM x => x
183 :     | _ => bug "unexpected tyc in tcd_prim")
184 :     val tcd_fn : tyc -> tkind list * tyc = fn tc =>
185 :     (case tc_out tc of LK.TC_FN x => x
186 :     | _ => bug "unexpected tyc in tcd_fn")
187 :     val tcd_app : tyc -> tyc * tyc list = fn tc =>
188 :     (case tc_out tc of LK.TC_APP x => x
189 :     | _ => bug "unexpected tyc in tcd_app")
190 :     val tcd_seq : tyc -> tyc list = fn tc =>
191 :     (case tc_out tc of LK.TC_SEQ x => x
192 :     | _ => bug "unexpected tyc in tcd_seq")
193 :     val tcd_proj : tyc -> tyc * int = fn tc =>
194 :     (case tc_out tc of LK.TC_PROJ x => x
195 :     | _ => bug "unexpected tyc in tcd_proj")
196 :     val tcd_sum : tyc -> tyc list = fn tc =>
197 :     (case tc_out tc of LK.TC_SUM x => x
198 :     | _ => bug "unexpected tyc in tcd_sum")
199 :     val tcd_fix : tyc -> (int * tyc * tyc list) * int = fn tc =>
200 :     (case tc_out tc of LK.TC_FIX x => x
201 :     | _ => bug "unexpected tyc in tcd_fix")
202 : monnier 45 val tcd_wrap : tyc -> tyc = fn tc =>
203 :     (case tc_out tc
204 :     of LK.TC_TOKEN(tk, x) =>
205 :     if LK.token_eq(tk, LK.wrap_token) then x
206 :     else bug "unexpected token tyc in tcd_wrap"
207 :     | _ => bug "unexpected regular tyc in tcd_wrap")
208 : monnier 16 val tcd_abs : tyc -> tyc = fn tc =>
209 :     (case tc_out tc of LK.TC_ABS x => x
210 :     | _ => bug "unexpected tyc in tcd_abs")
211 : monnier 24 val tcd_box : tyc -> tyc = fn tc =>
212 : monnier 16 (case tc_out tc of LK.TC_BOX x => x
213 :     | _ => bug "unexpected tyc in tcd_box")
214 :     val tcd_tuple : tyc -> tyc list = fn tc =>
215 : monnier 45 (case tc_out tc of LK.TC_TUPLE (_,x) => x
216 : monnier 16 | _ => bug "unexpected tyc in tcd_tuple")
217 : monnier 45 val tcd_arrow : tyc -> fflag * tyc list * tyc list = fn tc =>
218 : monnier 16 (case tc_out tc of LK.TC_ARROW x => x
219 :     | _ => bug "unexpected tyc in tcd_arrow")
220 :    
221 :     (** tyc predicates *)
222 :     val tcp_var : tyc -> bool = fn tc =>
223 :     (case tc_out tc of LK.TC_VAR _ => true | _ => false)
224 :     val tcp_nvar : tyc -> bool = fn tc =>
225 :     (case tc_out tc of LK.TC_NVAR _ => true | _ => false)
226 :     val tcp_prim : tyc -> bool = fn tc =>
227 :     (case tc_out tc of LK.TC_PRIM _ => true | _ => false)
228 :     val tcp_fn : tyc -> bool = fn tc =>
229 :     (case tc_out tc of LK.TC_FN _ => true | _ => false)
230 :     val tcp_app : tyc -> bool = fn tc =>
231 :     (case tc_out tc of LK.TC_APP _ => true | _ => false)
232 :     val tcp_seq : tyc -> bool = fn tc =>
233 :     (case tc_out tc of LK.TC_SEQ _ => true | _ => false)
234 :     val tcp_proj : tyc -> bool = fn tc =>
235 :     (case tc_out tc of LK.TC_PROJ _ => true | _ => false)
236 :     val tcp_sum : tyc -> bool = fn tc =>
237 :     (case tc_out tc of LK.TC_SUM _ => true | _ => false)
238 :     val tcp_fix : tyc -> bool = fn tc =>
239 :     (case tc_out tc of LK.TC_FIX _ => true | _ => false)
240 : monnier 45 val tcp_wrap : tyc -> bool = fn tc =>
241 :     (case tc_out tc of LK.TC_TOKEN (tk, _) => LK.token_eq(tk, LK.wrap_token)
242 :     | _ => false)
243 : monnier 16 val tcp_abs : tyc -> bool = fn tc =>
244 :     (case tc_out tc of LK.TC_ABS _ => true | _ => false)
245 : monnier 24 val tcp_box : tyc -> bool = fn tc =>
246 : monnier 16 (case tc_out tc of LK.TC_BOX _ => true | _ => false)
247 :     val tcp_tuple : tyc -> bool = fn tc =>
248 :     (case tc_out tc of LK.TC_TUPLE _ => true | _ => false)
249 :     val tcp_arrow : tyc -> bool = fn tc =>
250 :     (case tc_out tc of LK.TC_ARROW _ => true | _ => false)
251 :    
252 :     (** tyc one-arm switches *)
253 :     fun tcw_var (tc, f, g) =
254 :     (case tc_out tc of LK.TC_VAR x => f x | _ => g tc)
255 :     fun tcw_nvar (tc, f, g) =
256 :     (case tc_out tc of LK.TC_NVAR x => f x | _ => g tc)
257 :     fun tcw_prim (tc, f, g) =
258 :     (case tc_out tc of LK.TC_PRIM x => f x | _ => g tc)
259 :     fun tcw_fn (tc, f, g) =
260 :     (case tc_out tc of LK.TC_FN x => f x | _ => g tc)
261 :     fun tcw_app (tc, f, g) =
262 :     (case tc_out tc of LK.TC_APP x => f x | _ => g tc)
263 :     fun tcw_seq (tc, f, g) =
264 :     (case tc_out tc of LK.TC_SEQ x => f x | _ => g tc)
265 :     fun tcw_proj (tc, f, g) =
266 :     (case tc_out tc of LK.TC_PROJ x => f x | _ => g tc)
267 :     fun tcw_sum (tc, f, g) =
268 :     (case tc_out tc of LK.TC_SUM x => f x | _ => g tc)
269 :     fun tcw_fix (tc, f, g) =
270 :     (case tc_out tc of LK.TC_FIX x => f x | _ => g tc)
271 : monnier 45 fun tcw_wrap (tc, f, g) =
272 :     (case tc_out tc
273 :     of LK.TC_TOKEN(rk, x) =>
274 :     if LK.token_eq(rk, LK.wrap_token) then f x else g tc
275 :     | _ => g tc)
276 : monnier 16 fun tcw_abs (tc, f, g) =
277 :     (case tc_out tc of LK.TC_ABS x => f x | _ => g tc)
278 : monnier 24 fun tcw_box (tc, f, g) =
279 : monnier 16 (case tc_out tc of LK.TC_BOX x => f x | _ => g tc)
280 :     fun tcw_tuple (tc, f, g) =
281 : monnier 45 (case tc_out tc of LK.TC_TUPLE (_,x) => f x | _ => g tc)
282 : monnier 16 fun tcw_arrow (tc, f, g) =
283 :     (case tc_out tc of LK.TC_ARROW x => f x | _ => g tc)
284 :    
285 :    
286 :     (*
287 :     * FLINT lty is roughly equivalent to the following ML datatype
288 :     *
289 :     * datatype lty
290 :     * = LT_TYC of tyc
291 :     * | LT_STR of lty list
292 :     * | LT_FCT of lty list * lty list
293 :     * | LT_POLY of tkind list * lty list
294 :     * | LT_PST of (int * lty) list (* soon obsolete *)
295 :     *
296 :     * We treat lty as an abstract type so we can no longer use pattern
297 :     * matching. The client does not need to worry about whether an lty
298 :     * is in normal form or not.
299 :     *)
300 :    
301 :     (** lty constructors *)
302 :     val ltc_tyc : tyc -> lty = lt_inj o LK.LT_TYC
303 :     val ltc_str : lty list -> lty = lt_inj o LK.LT_STR
304 :     val ltc_fct : lty list * lty list -> lty = lt_inj o LK.LT_FCT
305 :     val ltc_poly : tkind list * lty list -> lty = lt_inj o LK.LT_POLY
306 :     val ltc_pst : (int * lty) list -> lty = lt_inj o LK.LT_PST
307 :    
308 :     (** lty deconstructors *)
309 :     val ltd_tyc : lty -> tyc = fn lt =>
310 :     (case lt_out lt of LK.LT_TYC x => x
311 :     | _ => bug "unexpected lty in ltd_tyc")
312 :     val ltd_str : lty -> lty list = fn lt =>
313 :     (case lt_out lt of LK.LT_STR x => x
314 :     | _ => bug "unexpected lty in ltd_str")
315 :     val ltd_fct : lty -> lty list * lty list = fn lt =>
316 :     (case lt_out lt of LK.LT_FCT x => x
317 :     | _ => bug "unexpected lty in ltd_fct")
318 :     val ltd_poly : lty -> tkind list * lty list = fn lt =>
319 :     (case lt_out lt of LK.LT_POLY x => x
320 :     | _ => bug "unexpected lty in ltd_poly")
321 :     val ltd_pst : lty -> (int * lty) list = fn lt =>
322 :     (case lt_out lt of LK.LT_PST x => x
323 :     | _ => bug "unexpected lty in ltd_pst")
324 :    
325 :     (** lty predicates *)
326 :     val ltp_tyc : lty -> bool = fn lt =>
327 :     (case lt_out lt of LK.LT_TYC _ => true | _ => false)
328 :     val ltp_str : lty -> bool = fn lt =>
329 :     (case lt_out lt of LK.LT_STR _ => true | _ => false)
330 :     val ltp_fct : lty -> bool = fn lt =>
331 :     (case lt_out lt of LK.LT_FCT _ => true | _ => false)
332 :     val ltp_poly : lty -> bool = fn lt =>
333 :     (case lt_out lt of LK.LT_POLY _ => true | _ => false)
334 :     val ltp_pst : lty -> bool = fn lt =>
335 :     (case lt_out lt of LK.LT_PST _ => true | _ => false)
336 :    
337 :     (** lty one-arm switches *)
338 :     fun ltw_tyc (lt, f, g) =
339 :     (case lt_out lt of LK.LT_TYC x => f x | _ => g lt)
340 :     fun ltw_str (lt, f, g) =
341 :     (case lt_out lt of LK.LT_STR x => f x | _ => g lt)
342 :     fun ltw_fct (lt, f, g) =
343 :     (case lt_out lt of LK.LT_FCT x => f x | _ => g lt)
344 :     fun ltw_poly (lt, f, g) =
345 :     (case lt_out lt of LK.LT_POLY x => f x | _ => g lt)
346 :     fun ltw_pst (lt, f, g) =
347 :     (case lt_out lt of LK.LT_PST x => f x | _ => g lt)
348 :    
349 :    
350 :     (*
351 :     * Because FLINT tyc is embedded inside FLINT lty, we supply the
352 :     * the following utility functions on building ltys that are based
353 :     * on simple mono tycs.
354 :     *)
355 :    
356 :     (** tyc-lty constructors *)
357 :     val ltc_var : index * int -> lty = ltc_tyc o tcc_var
358 :     val ltc_prim : primtyc -> lty = ltc_tyc o tcc_prim
359 :     val ltc_tuple : lty list -> lty = ltc_tyc o (tcc_tuple o (map ltd_tyc))
360 : monnier 45 val ltc_arrow : fflag * lty list * lty list -> lty = fn (r, t1, t2) =>
361 : monnier 16 let val ts1 = map ltd_tyc t1
362 :     val ts2 = map ltd_tyc t2
363 :     in ltc_tyc (tcc_arrow(r, ts1, ts2))
364 :     end
365 :    
366 :     (** tyc-lty deconstructors *)
367 :     val ltd_var : lty -> index * int = tcd_var o ltd_tyc
368 :     val ltd_prim : lty -> primtyc = tcd_prim o ltd_tyc
369 :     val ltd_tuple : lty -> lty list = (map ltc_tyc) o (tcd_tuple o ltd_tyc)
370 : monnier 45 val ltd_arrow : lty -> fflag * lty list * lty list = fn t =>
371 : monnier 16 let val (r, ts1, ts2) = tcd_arrow (ltd_tyc t)
372 :     in (r, map ltc_tyc ts1, map ltc_tyc ts2)
373 :     end
374 :    
375 :     (** tyc-lty predicates *)
376 :     val ltp_var : lty -> bool = fn t =>
377 :     (case lt_out t of LK.LT_TYC x => tcp_var x | _ => false)
378 :     val ltp_prim : lty -> bool = fn t =>
379 :     (case lt_out t of LK.LT_TYC x => tcp_prim x | _ => false)
380 :     val ltp_tuple : lty -> bool = fn t =>
381 :     (case lt_out t of LK.LT_TYC x => tcp_tuple x | _ => false)
382 :     val ltp_arrow : lty -> bool = fn t =>
383 :     (case lt_out t of LK.LT_TYC x => tcp_arrow x | _ => false)
384 :    
385 :     (** tyc-lty one-arm switches *)
386 :     fun ltw_var (lt, f, g) =
387 :     (case lt_out lt
388 :     of LK.LT_TYC tc =>
389 :     (case tc_out tc of LK.TC_VAR x => f x | _ => g lt)
390 :     | _ => g lt)
391 :    
392 :     fun ltw_prim (lt, f, g) =
393 :     (case lt_out lt
394 :     of LK.LT_TYC tc =>
395 :     (case tc_out tc of LK.TC_PRIM x => f x | _ => g lt)
396 :     | _ => g lt)
397 :    
398 :     fun ltw_tuple (lt, f, g) =
399 :     (case lt_out lt
400 :     of LK.LT_TYC tc =>
401 : monnier 45 (case tc_out tc of LK.TC_TUPLE (_, x) => f x | _ => g lt)
402 : monnier 16 | _ => g lt)
403 :    
404 :     fun ltw_arrow (lt, f, g) =
405 :     (case lt_out lt
406 :     of LK.LT_TYC tc =>
407 :     (case tc_out tc of LK.TC_ARROW x => f x | _ => g lt)
408 :     | _ => g lt)
409 :    
410 :    
411 :     (*
412 :     * The following functions are written for CPS only. If you are writing
413 :     * writing code for FLINT, you should not use any of these functions.
414 :     * The continuation referred here is the internal continuation introduced
415 :     * via CPS conversion; it is different from the source-level continuation
416 :     * ('a cont) or control continuation ('a control-cont) where are represented
417 :     * as PT.ptc_cont and PT.ptc_ccont respectively.
418 :     *
419 :     *)
420 :    
421 :     (** cont-tyc-lty constructors *)
422 :     val tcc_cont : tyc list -> tyc = tc_inj o LK.TC_CONT
423 :     val ltc_cont : lty list -> lty = lt_inj o LK.LT_CONT
424 :    
425 :     (** cont-tyc-lty deconstructors *)
426 :     val tcd_cont : tyc -> tyc list = fn tc =>
427 :     (case tc_out tc of LK.TC_CONT x => x
428 :     | _ => bug "unexpected tyc in tcd_cont")
429 :     val ltd_cont : lty -> lty list = fn lt =>
430 :     (case lt_out lt of LK.LT_CONT x => x
431 :     | _ => bug "unexpected lty in ltd_cont")
432 :    
433 :     (** cont-tyc-lty predicates *)
434 :     val tcp_cont : tyc -> bool = fn tc =>
435 :     (case tc_out tc of LK.TC_CONT _ => true | _ => false)
436 :     val ltp_cont : lty -> bool = fn lt =>
437 :     (case lt_out lt of LK.LT_CONT _ => true | _ => false)
438 :    
439 :     (** cont-tyc-lty one-arm switches *)
440 :     fun tcw_cont (tc, f, g) =
441 :     (case tc_out tc of LK.TC_CONT x => f x | _ => g tc)
442 :     fun ltw_cont (lt, f, g) =
443 :     (case lt_out lt of LK.LT_CONT x => f x | _ => g lt)
444 :    
445 :    
446 :    
447 :     (*
448 :     * The following functions are written for PLambdaType only. If you
449 :     * are writing code for FLINT only, don't use any of these functions.
450 :     * The idea is that in PLambda, all (value or type) functions have single
451 :     * argument and single return-result. Ideally, we should define
452 :     * another sets of datatypes for tycs and ltys. But we want to avoid
453 :     * the translation from PLambdaType to FLINT types, so we let them
454 :     * share the same representations as much as possible.
455 :     *
456 :     * Ultimately, LtyDef should be separated into two files: one for
457 :     * FLINT, another for PLambda, but we will see if this is necessary.
458 :     *
459 :     *)
460 :    
461 :     (*
462 :     * The implementation here is TEMPORARY; Stefan needs to take a look at
463 :     * this. Note parrow could share the representation with arrow if there
464 :     * is one-to-one mapping between parrow and arrow.
465 :     *)
466 :    
467 :     (** plambda tyc-lty constructors *)
468 :     val tcc_parrow : tyc * tyc -> tyc =
469 : monnier 45 fn (x, y) => tcc_arrow(ffc_var (false, false), [x], [y])
470 : monnier 16 val ltc_parrow : lty * lty -> lty =
471 :     fn (x, y) => ltc_tyc (tcc_parrow (ltd_tyc x, ltd_tyc y))
472 :     val ltc_ppoly : tkind list * lty -> lty = fn (ks, t) => ltc_poly(ks, [t])
473 :     val ltc_pfct : lty * lty -> lty = fn (x, y) => ltc_fct ([x], [y])
474 :    
475 :     (** plambda tyc-lty deconstructors *)
476 :     val tcd_parrow : tyc -> tyc * tyc = fn tc =>
477 : monnier 45 (case tc_out tc
478 :     of LK.TC_ARROW (_, xs, ys) => (LK.tc_autotuple xs, LK.tc_autotuple ys)
479 :     | _ => bug "unexpected tyc in tcd_parrow")
480 : monnier 16 val ltd_parrow : lty -> lty * lty = fn t =>
481 :     let val (t1, t2) = tcd_parrow (ltd_tyc t)
482 :     in (ltc_tyc t1, ltc_tyc t2)
483 :     end
484 :     val ltd_ppoly : lty -> tkind list * lty = fn t =>
485 :     let val (ks, ts) = ltd_poly t
486 :     in case ts of [x] => (ks, x)
487 :     | _ => bug "unexpected case in ltd_ppoly"
488 :     end
489 :     val ltd_pfct : lty -> lty * lty = fn t =>
490 :     let val (ts1, ts2) = ltd_fct t
491 :     in case (ts1, ts2) of ([x], [y]) => (x, y)
492 :     | _ => bug "unexpected case in ltd_pfct"
493 :     end
494 :    
495 :     (** plambda tyc-lty predicates *)
496 :     val tcp_parrow : tyc -> bool = fn tc =>
497 :     (case tc_out tc of LK.TC_ARROW (_, [x], [y]) => true | _ => false)
498 :     val ltp_parrow : lty -> bool = fn t =>
499 :     (case lt_out t of LK.LT_TYC x => tcp_parrow x | _ => false)
500 :     val ltp_ppoly : lty -> bool = fn t =>
501 :     (case lt_out t of LK.LT_POLY (_, [x]) => true | _ => false)
502 :     val ltp_pfct : lty -> bool = fn t =>
503 :     (case lt_out t of LK.LT_FCT ([x], [y]) => true | _ => false)
504 :    
505 :     (** plambda tyc-lty one-arm switches *)
506 :     fun tcw_parrow (tc, f, g) =
507 :     (case tc_out tc of LK.TC_ARROW (_,[x],[y]) => f (x,y) | _ => g tc)
508 :     fun ltw_parrow (lt, f, g) =
509 :     (case lt_out lt
510 :     of LK.LT_TYC tc =>
511 :     (case tc_out tc of LK.TC_ARROW (_,[x],[y]) => f(x,y) | _ => g lt)
512 :     | _ => g lt)
513 :     fun ltw_ppoly (lt, f, g) =
514 :     (case lt_out lt of LK.LT_POLY(ks,[x]) => f(ks,x) | _ => g lt)
515 :     fun ltw_pfct (lt, f, g) =
516 :     (case lt_out lt of LK.LT_FCT([x],[y]) => f(x,y) | _ => g lt)
517 :    
518 :     end (* top-level local *)
519 :     end (* structure LtyDef *)
520 :    

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