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-3/compiler/FLINT/kernel/ltydef.sig
ViewVC logotype

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

Parent Directory Parent Directory | Revision Log Revision Log


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

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