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

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