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/branches/primop-branch-2/src/compiler/FLINT/kernel/ltydef.sig
ViewVC logotype

Annotation of /sml/branches/primop-branch-2/src/compiler/FLINT/kernel/ltydef.sig

Parent Directory Parent Directory | Revision Log Revision Log


Revision 45 - (view) (download) (as text)
Original Path: sml/branches/SMLNJ/src/compiler/FLINT/kernel/ltydef.sig

1 : monnier 16 (* Copyright (c) 1998 YALE FLINT PROJECT *)
2 :     (* ltydef.sig *)
3 :    
4 :     (*
5 :     * This interface hides the implementation details of FLINT tkind, tyc, and
6 :     * lty defined inside LtyKernel. For each entity, we provide a series of
7 :     * constructor funtions, deconstructor functions, predicate functions, and
8 :     * functions that test equivalence and do pretty-printing. This interface
9 :     * should only refer to DebIndex, LtyKernel, PrimTyc, and Symbol.
10 :     *)
11 :    
12 :     signature LTYDEF =
13 :     sig
14 :    
15 :     (** basic entities *)
16 :     type index = DebIndex.index
17 :     type depth = DebIndex.depth
18 :     type primtyc = PrimTyc.primtyc
19 :     type tvar = LtyKernel.tvar
20 : monnier 45
21 :     type fflag = LtyKernel.fflag
22 :     type rflag = LtyKernel.rflag
23 :    
24 :     type tkind = LtyKernel.tkind
25 : monnier 16 type tyc = LtyKernel.tyc
26 :     type lty = LtyKernel.lty
27 :    
28 :     (*
29 :     * FLINT tkind is roughly equivalent to the following ML datatype
30 :     *
31 :     * datatype tkind
32 :     * = TK_MONO
33 :     * | TK_BOX
34 :     * | TK_SEQ of tkind list
35 :     * | TK_FUN of tkind * tkind
36 :     *
37 :     * We treat tkind as an abstract type so we can no longer use
38 :     * pattern matching.
39 :     *
40 :     *)
41 :    
42 :     (** tkind constructors *)
43 :     val tkc_mono : tkind
44 :     val tkc_box : tkind
45 :     val tkc_seq : tkind list -> tkind
46 : monnier 45 val tkc_fun : tkind list * tkind -> tkind
47 : monnier 16
48 :     (** tkind deconstructors *)
49 :     val tkd_mono : tkind -> unit
50 :     val tkd_box : tkind -> unit
51 :     val tkd_seq : tkind -> tkind list
52 : monnier 45 val tkd_fun : tkind -> tkind list * tkind
53 : monnier 16
54 :     (** tkind predicates *)
55 :     val tkp_mono : tkind -> bool
56 :     val tkp_box : tkind -> bool
57 :     val tkp_seq : tkind -> bool
58 :     val tkp_fun : tkind -> bool
59 :    
60 :     (** tkind one-arm switch *)
61 :     val tkw_mono : tkind * (unit -> 'a) * (tkind -> 'a) -> 'a
62 :     val tkw_box : tkind * (unit -> 'a) * (tkind -> 'a) -> 'a
63 :     val tkw_seq : tkind * (tkind list -> 'a) * (tkind -> 'a) -> 'a
64 : monnier 45 val tkw_fun : tkind * (tkind list * tkind -> 'a) * (tkind -> 'a) -> 'a
65 : monnier 16
66 :    
67 :     (*
68 : monnier 45 * FLINT fflag and rflag are used to classify different kinds of monomorphic
69 :     * functions and records. As of now, they are roughly equivalent to:
70 :     *
71 :     * datatype fflag
72 :     * = FF_VAR of bool * bool
73 :     * | FF_FIXED
74 :     *
75 :     * datatype rflag = RF_TMP
76 :     *
77 :     * We treat both as abstract types so pattern matching no longer applies.
78 :     * NOTE: FF_VAR flags are used by FLINTs before we perform representation
79 :     * analysis while FF_FIXED is used by FLINTs after we perform representation
80 :     * analysis.
81 :     *)
82 :    
83 :     (** fflag and rflag constructors *)
84 :     val ffc_var : bool * bool -> fflag
85 :     val ffc_fixed : fflag
86 :     val rfc_tmp : rflag
87 :    
88 :     (** fflag and rflag deconstructors *)
89 :     val ffd_var : fflag -> bool * bool
90 :     val ffd_fixed : fflag -> unit
91 :     val rfd_tmp : rflag -> unit
92 :    
93 :     (** fflag and rflag predicates *)
94 :     val ffp_var : fflag -> bool
95 :     val ffp_fixed : fflag -> bool
96 :     val rfp_tmp : rflag -> bool
97 :    
98 :     (** fflag and rflag one-arm switch *)
99 :     val ffw_var : fflag * (bool * bool -> 'a) * (fflag -> 'a) -> 'a
100 :     val ffw_fixed : fflag * (unit -> 'a) * (fflag -> 'a) -> 'a
101 :     val rfw_tmp : rflag * (unit -> 'a) * (rflag -> 'a) -> 'a
102 :    
103 :    
104 :     (*
105 : monnier 16 * FLINT tyc is roughly equivalent to the following ML datatype
106 :     *
107 :     * datatype tyc
108 :     * = TC_VAR of index * int
109 : monnier 45 * | TC_NVAR of tvar * depth * int (* NOT USED *)
110 : monnier 16 * | TC_PRIM of primtyc
111 :     * | TC_FN of tkind list * tyc
112 :     * | TC_APP of tyc * tyc list
113 :     * | TC_SEQ of tyc list
114 :     * | TC_PROJ of tyc * int
115 :     * | TC_SUM of tyc list
116 :     * | TC_FIX of tyc * int
117 : monnier 45 * | TC_WRAP of tyc (* used after rep. analysis only *)
118 :     * | TC_ABS of tyc (* NOT USED *)
119 :     * | TC_BOX of tyc (* NOT USED *)
120 :     * | TC_TUPLE of tyc list (* rflag hidden *)
121 :     * | TC_ARROW of fflag * tyc list * tyc list
122 : monnier 16 *
123 :     * We treat tyc as an abstract type so we can no longer use
124 :     * pattern matching. Type applications (TC_APP) and projections
125 :     * (TC_PROJ) are automatically reduced as needed, that is, the
126 :     * client does not need to worry about whether a tyc is in the
127 :     * normal form or not, all functions defined here automatically
128 :     * take care of this.
129 :     *)
130 :    
131 :     (** tyc constructors *)
132 :     val tcc_var : index * int -> tyc
133 :     val tcc_nvar : tvar * depth * int -> tyc
134 :     val tcc_prim : primtyc -> tyc
135 :     val tcc_fn : tkind list * tyc -> tyc
136 :     val tcc_app : tyc * tyc list -> tyc
137 :     val tcc_seq : tyc list -> tyc
138 :     val tcc_proj : tyc * int -> tyc
139 :     val tcc_sum : tyc list -> tyc
140 :     val tcc_fix : (int * tyc * tyc list) * int -> tyc
141 : monnier 45 val tcc_wrap : tyc -> tyc
142 : monnier 16 val tcc_abs : tyc -> tyc
143 :     val tcc_box : tyc -> tyc
144 :     val tcc_tuple : tyc list -> tyc
145 : monnier 45 val tcc_arrow : fflag * tyc list * tyc list -> tyc
146 : monnier 16
147 :     (** tyc deconstructors *)
148 :     val tcd_var : tyc -> index * int
149 :     val tcd_nvar : tyc -> tvar * depth * int
150 :     val tcd_prim : tyc -> primtyc
151 :     val tcd_fn : tyc -> tkind list * tyc
152 :     val tcd_app : tyc -> tyc * tyc list
153 :     val tcd_seq : tyc -> tyc list
154 :     val tcd_proj : tyc -> tyc * int
155 :     val tcd_sum : tyc -> tyc list
156 :     val tcd_fix : tyc -> (int * tyc * tyc list) * int
157 : monnier 45 val tcd_wrap : tyc -> tyc
158 : monnier 16 val tcd_abs : tyc -> tyc
159 :     val tcd_box : tyc -> tyc
160 :     val tcd_tuple : tyc -> tyc list
161 : monnier 45 val tcd_arrow : tyc -> fflag * tyc list * tyc list
162 : monnier 16
163 :     (** tyc predicates *)
164 :     val tcp_var : tyc -> bool
165 :     val tcp_nvar : tyc -> bool
166 :     val tcp_prim : tyc -> bool
167 :     val tcp_fn : tyc -> bool
168 :     val tcp_app : tyc -> bool
169 :     val tcp_seq : tyc -> bool
170 :     val tcp_proj : tyc -> bool
171 :     val tcp_sum : tyc -> bool
172 :     val tcp_fix : tyc -> bool
173 : monnier 45 val tcp_wrap : tyc -> bool
174 : monnier 16 val tcp_abs : tyc -> bool
175 :     val tcp_box : tyc -> bool
176 :     val tcp_tuple : tyc -> bool
177 :     val tcp_arrow : tyc -> bool
178 :    
179 :     (** tyc one-arm switch *)
180 :     val tcw_var : tyc * (index * int -> 'a) * (tyc -> 'a) -> 'a
181 :     val tcw_nvar : tyc * (tvar * depth * int -> 'a) * (tyc -> 'a) -> 'a
182 :     val tcw_prim : tyc * (primtyc -> 'a) * (tyc -> 'a) -> 'a
183 :     val tcw_fn : tyc * (tkind list * tyc -> 'a) * (tyc -> 'a) -> 'a
184 :     val tcw_app : tyc * (tyc * tyc list -> 'a) * (tyc -> 'a) -> 'a
185 :     val tcw_seq : tyc * (tyc list -> 'a) * (tyc -> 'a) -> 'a
186 :     val tcw_proj : tyc * (tyc * int -> 'a) * (tyc -> 'a) -> 'a
187 :     val tcw_sum : tyc * (tyc list -> 'a) * (tyc -> 'a) -> 'a
188 :     val tcw_fix : tyc * ((int * tyc * tyc list) * int -> 'a) * (tyc -> 'a) -> 'a
189 : monnier 45 val tcw_wrap : tyc * (tyc -> 'a) * (tyc -> 'a) -> 'a
190 : monnier 16 val tcw_abs : tyc * (tyc -> 'a) * (tyc -> 'a) -> 'a
191 :     val tcw_box : tyc * (tyc -> 'a) * (tyc -> 'a) -> 'a
192 :     val tcw_tuple : tyc * (tyc list -> 'a) * (tyc -> 'a) -> 'a
193 : monnier 45 val tcw_arrow : tyc * (fflag * tyc list * tyc list -> 'a)
194 : monnier 16 * (tyc -> 'a) -> 'a
195 :    
196 :    
197 :     (*
198 :     * FLINT lty is roughly equivalent to the following ML datatype
199 :     *
200 :     * datatype lty
201 :     * = LT_TYC of tyc
202 :     * | LT_STR of lty list
203 :     * | LT_FCT of lty list * lty list
204 :     * | LT_POLY of tkind list * lty list
205 : monnier 45 * | LT_PST of (int * lty) list (* SOON BECOME OBSOLETE *)
206 : monnier 16 *
207 :     * We treat lty as an abstract type so we can no longer use pattern
208 :     * matching. The client does not need to worry about whether an lty
209 :     * is in normal form or not.
210 :     *)
211 :    
212 :     (** lty constructors *)
213 :     val ltc_tyc : tyc -> lty
214 :     val ltc_str : lty list -> lty
215 :     val ltc_fct : lty list * lty list -> lty
216 :     val ltc_poly : tkind list * lty list -> lty
217 :     val ltc_pst : (int * lty) list -> lty
218 :    
219 :     (** lty deconstructors *)
220 :     val ltd_tyc : lty -> tyc
221 :     val ltd_str : lty -> lty list
222 :     val ltd_fct : lty -> lty list * lty list
223 :     val ltd_poly : lty -> tkind list * lty list
224 :     val ltd_pst : lty -> (int * lty) list
225 :    
226 :     (** lty predicates *)
227 :     val ltp_tyc : lty -> bool
228 :     val ltp_str : lty -> bool
229 :     val ltp_fct : lty -> bool
230 :     val ltp_poly : lty -> bool
231 :     val ltp_pst : lty -> bool
232 :    
233 :     (** lty one arm switches *)
234 :     val ltw_tyc : lty * (tyc -> 'a) * (lty -> 'a) -> 'a
235 :     val ltw_str : lty * (lty list -> 'a) * (lty -> 'a) -> 'a
236 :     val ltw_fct : lty * (lty list * lty list -> 'a) * (lty -> 'a) -> 'a
237 :     val ltw_poly : lty * (tkind list * lty list -> 'a) * (lty -> 'a) -> 'a
238 :     val ltw_pst : lty * ((int * lty) list -> 'a) * (lty -> 'a) -> 'a
239 :    
240 :    
241 :     (*
242 :     * Because FLINT tyc is embedded inside FLINT lty, we supply the
243 :     * the following utility functions on building ltys that are based
244 :     * on simple mono tycs.
245 :     *)
246 :    
247 :     (** tyc-lty constructors *)
248 :     val ltc_var : index * int -> lty
249 :     val ltc_prim : primtyc -> lty
250 :     val ltc_tuple : lty list -> lty
251 : monnier 45 val ltc_arrow : fflag * lty list * lty list -> lty
252 : monnier 16
253 :     (** tyc-lty deconstructors *)
254 :     val ltd_var : lty -> index * int
255 :     val ltd_prim : lty -> primtyc
256 :     val ltd_tuple : lty -> lty list
257 : monnier 45 val ltd_arrow : lty -> fflag * lty list * lty list
258 : monnier 16
259 :     (** tyc-lty predicates *)
260 :     val ltp_var : lty -> bool
261 :     val ltp_prim : lty -> bool
262 :     val ltp_tuple : lty -> bool
263 :     val ltp_arrow : lty -> bool
264 :    
265 :     (** tyc-lty one-arm switches *)
266 :     val ltw_var : lty * (index * int -> 'a) * (lty -> 'a) -> 'a
267 :     val ltw_prim : lty * (primtyc -> 'a) * (lty -> 'a) -> 'a
268 :     val ltw_tuple : lty * (tyc list -> 'a) * (lty -> 'a) -> 'a
269 : monnier 45 val ltw_arrow : lty * (fflag * tyc list * tyc list -> 'a)
270 : monnier 16 * (lty -> 'a) -> 'a
271 :    
272 :    
273 :     (*
274 :     * The following functions are written for CPS only. If you are writing
275 : monnier 45 * code for FLINT, you should not use any of these functions.
276 : monnier 16 * The continuation referred here is the internal continuation introduced
277 :     * via CPS conversion; it is different from the source-level continuation
278 :     * ('a cont) or control continuation ('a control-cont) where are represented
279 :     * as PT.ptc_cont and PT.ptc_ccont respectively.
280 :     *
281 :     *)
282 :    
283 :     (** cont-tyc-lty constructors *)
284 :     val tcc_cont : tyc list -> tyc
285 :     val ltc_cont : lty list -> lty
286 :    
287 :     (** cont-tyc-lty deconstructors *)
288 :     val tcd_cont : tyc -> tyc list
289 :     val ltd_cont : lty -> lty list
290 :    
291 :     (** cont-tyc-lty predicates *)
292 :     val tcp_cont : tyc -> bool
293 :     val ltp_cont : lty -> bool
294 :    
295 :     (** cont-tyc-lty one-arm switches *)
296 :     val tcw_cont : tyc * (tyc list -> 'a) * (tyc -> 'a) -> 'a
297 :     val ltw_cont : lty * (lty list -> 'a) * (lty -> 'a) -> 'a
298 :    
299 :    
300 :     (*
301 :     * The following functions are written for PLambdaType only. If you
302 :     * are writing code for FLINT only, don't use any of these functions.
303 :     * The idea is that in PLambda, all (value or type) functions have single
304 :     * argument and single return-result. Ideally, we should define
305 :     * another sets of datatypes for tycs and ltys. But we want to avoid
306 :     * the translation from PLambdaType to FLINT types, so we let them
307 :     * share the same representations as much as possible.
308 :     *
309 :     * Ultimately, LtyDef should be separated into two files: one for
310 :     * FLINT, another for PLambda, but we will see if this is necessary.
311 :     *
312 :     *)
313 :    
314 :     (** plambda tyc-lty constructors *)
315 :     val tcc_parrow : tyc * tyc -> tyc
316 :     val ltc_parrow : lty * lty -> lty
317 :     val ltc_ppoly : tkind list * lty -> lty
318 :     val ltc_pfct : lty * lty -> lty
319 :    
320 :     (** plambda tyc-lty deconstructors *)
321 :     val tcd_parrow : tyc -> tyc * tyc
322 :     val ltd_parrow : lty -> lty * lty
323 :     val ltd_ppoly : lty -> tkind list * lty
324 :     val ltd_pfct : lty -> lty * lty
325 :    
326 :     (** plambda tyc-lty predicates *)
327 :     val tcp_parrow : tyc -> bool
328 :     val ltp_parrow : lty -> bool
329 :     val ltp_ppoly : lty -> bool
330 :     val ltp_pfct : lty -> bool
331 :    
332 :     (** plambda tyc-lty one-arm switches *)
333 :     val tcw_parrow : tyc * (tyc * tyc -> 'a) * (tyc -> 'a) -> 'a
334 :     val ltw_parrow : lty * (tyc * tyc -> 'a) * (lty -> 'a) -> 'a
335 :     val ltw_ppoly : lty * (tkind list * lty -> 'a) * (lty -> 'a) -> 'a
336 :     val ltw_pfct : lty * (lty * lty -> 'a) * (lty -> 'a) -> 'a
337 :    
338 :     end (* signature LTYDEF *)

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