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.sig
ViewVC logotype

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 251 - (view) (download) (as text)

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 197 * | TC_NVAR of tvar
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 : monnier 197 val tcc_nvar : tvar -> tyc
134 : monnier 16 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 : monnier 197 val tcd_nvar : tyc -> tvar
150 : monnier 16 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 : monnier 197 val tcw_nvar : tyc * (tvar -> 'a) * (tyc -> 'a) -> 'a
182 : monnier 16 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 :     *
206 :     * We treat lty as an abstract type so we can no longer use pattern
207 :     * matching. The client does not need to worry about whether an lty
208 :     * is in normal form or not.
209 :     *)
210 :    
211 :     (** lty constructors *)
212 :     val ltc_tyc : tyc -> lty
213 :     val ltc_str : lty list -> lty
214 :     val ltc_fct : lty list * lty list -> lty
215 :     val ltc_poly : tkind list * lty list -> lty
216 :    
217 :     (** lty deconstructors *)
218 :     val ltd_tyc : lty -> tyc
219 :     val ltd_str : lty -> lty list
220 :     val ltd_fct : lty -> lty list * lty list
221 :     val ltd_poly : lty -> tkind list * lty list
222 :    
223 :     (** lty predicates *)
224 :     val ltp_tyc : lty -> bool
225 :     val ltp_str : lty -> bool
226 :     val ltp_fct : lty -> bool
227 :     val ltp_poly : lty -> bool
228 :    
229 :     (** lty one arm switches *)
230 :     val ltw_tyc : lty * (tyc -> 'a) * (lty -> 'a) -> 'a
231 :     val ltw_str : lty * (lty list -> 'a) * (lty -> 'a) -> 'a
232 :     val ltw_fct : lty * (lty list * lty list -> 'a) * (lty -> 'a) -> 'a
233 :     val ltw_poly : lty * (tkind list * lty list -> 'a) * (lty -> 'a) -> 'a
234 :    
235 :    
236 :     (*
237 :     * Because FLINT tyc is embedded inside FLINT lty, we supply the
238 :     * the following utility functions on building ltys that are based
239 :     * on simple mono tycs.
240 :     *)
241 :    
242 :     (** tyc-lty constructors *)
243 :     val ltc_var : index * int -> lty
244 :     val ltc_prim : primtyc -> lty
245 :     val ltc_tuple : lty list -> lty
246 : monnier 45 val ltc_arrow : fflag * lty list * lty list -> lty
247 : monnier 16
248 :     (** tyc-lty deconstructors *)
249 :     val ltd_var : lty -> index * int
250 :     val ltd_prim : lty -> primtyc
251 :     val ltd_tuple : lty -> lty list
252 : monnier 45 val ltd_arrow : lty -> fflag * lty list * lty list
253 : monnier 16
254 :     (** tyc-lty predicates *)
255 :     val ltp_var : lty -> bool
256 :     val ltp_prim : lty -> bool
257 :     val ltp_tuple : lty -> bool
258 :     val ltp_arrow : lty -> bool
259 :    
260 :     (** tyc-lty one-arm switches *)
261 :     val ltw_var : lty * (index * int -> 'a) * (lty -> 'a) -> 'a
262 :     val ltw_prim : lty * (primtyc -> 'a) * (lty -> 'a) -> 'a
263 :     val ltw_tuple : lty * (tyc list -> 'a) * (lty -> 'a) -> 'a
264 : monnier 45 val ltw_arrow : lty * (fflag * tyc list * tyc list -> 'a)
265 : monnier 16 * (lty -> 'a) -> 'a
266 :    
267 :    
268 :     (*
269 :     * The following functions are written for CPS only. If you are writing
270 : monnier 45 * code for FLINT, you should not use any of these functions.
271 : monnier 16 * The continuation referred here is the internal continuation introduced
272 :     * via CPS conversion; it is different from the source-level continuation
273 :     * ('a cont) or control continuation ('a control-cont) where are represented
274 :     * as PT.ptc_cont and PT.ptc_ccont respectively.
275 :     *
276 :     *)
277 :    
278 :     (** cont-tyc-lty constructors *)
279 :     val tcc_cont : tyc list -> tyc
280 :     val ltc_cont : lty list -> lty
281 :    
282 :     (** cont-tyc-lty deconstructors *)
283 :     val tcd_cont : tyc -> tyc list
284 :     val ltd_cont : lty -> lty list
285 :    
286 :     (** cont-tyc-lty predicates *)
287 :     val tcp_cont : tyc -> bool
288 :     val ltp_cont : lty -> bool
289 :    
290 :     (** cont-tyc-lty one-arm switches *)
291 :     val tcw_cont : tyc * (tyc list -> 'a) * (tyc -> 'a) -> 'a
292 :     val ltw_cont : lty * (lty list -> 'a) * (lty -> 'a) -> 'a
293 :    
294 :    
295 :     (*
296 :     * The following functions are written for PLambdaType only. If you
297 :     * are writing code for FLINT only, don't use any of these functions.
298 :     * The idea is that in PLambda, all (value or type) functions have single
299 :     * argument and single return-result. Ideally, we should define
300 :     * another sets of datatypes for tycs and ltys. But we want to avoid
301 :     * the translation from PLambdaType to FLINT types, so we let them
302 :     * share the same representations as much as possible.
303 :     *
304 :     * Ultimately, LtyDef should be separated into two files: one for
305 :     * FLINT, another for PLambda, but we will see if this is necessary.
306 :     *
307 :     *)
308 :    
309 :     (** plambda tyc-lty constructors *)
310 :     val tcc_parrow : tyc * tyc -> tyc
311 :     val ltc_parrow : lty * lty -> lty
312 :     val ltc_ppoly : tkind list * lty -> lty
313 :     val ltc_pfct : lty * lty -> lty
314 :    
315 :     (** plambda tyc-lty deconstructors *)
316 :     val tcd_parrow : tyc -> tyc * tyc
317 :     val ltd_parrow : lty -> lty * lty
318 :     val ltd_ppoly : lty -> tkind list * lty
319 :     val ltd_pfct : lty -> lty * lty
320 :    
321 :     (** plambda tyc-lty predicates *)
322 :     val tcp_parrow : tyc -> bool
323 :     val ltp_parrow : lty -> bool
324 :     val ltp_ppoly : lty -> bool
325 :     val ltp_pfct : lty -> bool
326 :    
327 :     (** plambda tyc-lty one-arm switches *)
328 :     val tcw_parrow : tyc * (tyc * tyc -> 'a) * (tyc -> 'a) -> 'a
329 :     val ltw_parrow : lty * (tyc * tyc -> 'a) * (lty -> 'a) -> 'a
330 :     val ltw_ppoly : lty * (tkind list * lty -> 'a) * (lty -> 'a) -> 'a
331 :     val ltw_pfct : lty * (lty * lty -> 'a) * (lty -> 'a) -> 'a
332 :    
333 :     end (* signature LTYDEF *)

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