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

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