Commit | Line | Data |
---|---|---|
7f918cf1 CE |
1 | (* c.sig |
2 | * 2005 Matthew Fluet (mfluet@acm.org) | |
3 | * Adapted for MLton. | |
4 | *) | |
5 | ||
6 | (* | |
7 | * Encoding the C type system in SML. | |
8 | * | |
9 | * (C) 2001, Lucent Technologies, Bell Laboratories | |
10 | * | |
11 | * author: Matthias Blume | |
12 | *) | |
13 | signature C = sig | |
14 | ||
15 | exception OutOfMemory | |
16 | ||
17 | (* objects of type 't, constness 'c; | |
18 | * The 't type variable will be instantiated with the object's "witness" | |
19 | * type. The intention is that there be an isomorphism between such | |
20 | * witness types and corresponding C types. | |
21 | * | |
22 | * Witness types are often the same as the (abstract) type of the value | |
23 | * stored in the object. However, this is merely a coincidence. For | |
24 | * example, a constant object holding a pointer to a read-write integer | |
25 | * would have type | |
26 | * ((sint, rw) ptr, ro) obj | |
27 | * and the value itself has type | |
28 | * (sint, rw) ptr. | |
29 | * | |
30 | * However, in the case of the "light" version of this object (see below), | |
31 | * the object type is | |
32 | * ((sint, rw) ptr, ro) obj' | |
33 | * while fetching from this object gives a value of type | |
34 | * (sint, rw) ptr'. | |
35 | * | |
36 | * (In other words, we use the "heavy" versions of value types as witness | |
37 | * types -- even in the "light" case.) *) | |
38 | type ('t, 'c) obj | |
39 | ||
40 | (* an alternative "light-weight" version that does not carry RTTI at | |
41 | * the cost of requiring explicit passing of RTTI for certain operations *) | |
42 | eqtype ('t, 'c) obj' | |
43 | ||
44 | (* constness property, to be substituted for 'c *) | |
45 | type ro and rw | |
46 | ||
47 | (* Pointers come in two varieties in C: Pointers to things we | |
48 | * know and pointers to "incomplete" types. The "ptr" type constructor | |
49 | * below encodes both kinds using the following convention: | |
50 | * - in the case of complete target types, 'o will be instantiated | |
51 | * to some ('t, 'c) obj | |
52 | * - in the case of incomplete target types, 'o will be instantiated | |
53 | * to some fresh (abstract) type (see iptr.sig for what this will | |
54 | * look like in practice) | |
55 | *) | |
56 | (* pointer to 'o *) | |
57 | type 'o ptr | |
58 | (* light-weight alternative *) | |
59 | eqtype 'o ptr' | |
60 | ||
61 | (* 'n-sized array with 't elements *) | |
62 | type ('t, 'n) arr | |
63 | ||
64 | (* no values, admits equality *) | |
65 | eqtype void | |
66 | ||
67 | (* void* is really a base type, but it happens to take the | |
68 | * form of a light-weight pointer type (with an abstract target). | |
69 | * This design makes it possible to use those ptr-related | |
70 | * functions that "make sense" for void*. *) | |
71 | (* C's void* *) | |
72 | type voidptr = void ptr' | |
73 | ||
74 | (* function pointers *) | |
75 | (* a function pointer *) | |
76 | type 'f fptr | |
77 | (* light-weight alternative *) | |
78 | eqtype 'f fptr' | |
79 | ||
80 | (* structures and unions *) | |
81 | (* struct/union named 'tag; | |
82 | * 'tag is drawn from the types defined in the Tag module | |
83 | *) | |
84 | type 'tag su | |
85 | ||
86 | (* enumerations *) | |
87 | eqtype 'tag enum | |
88 | ||
89 | (* primtypes (signed/unsigned char, short, int, long, long long; float, double) *) | |
90 | eqtype schar and uchar | |
91 | eqtype sshort and ushort | |
92 | eqtype sint and uint | |
93 | eqtype slong and ulong | |
94 | eqtype slonglong and ulonglong | |
95 | type float and double | |
96 | ||
97 | (* going from abstract to concrete and vice versa; | |
98 | * (this shouldn't be needed except when calling functions through | |
99 | * function pointers) *) | |
100 | structure Cvt : sig | |
101 | (* ML -> C *) | |
102 | val c_schar : MLRep.Char.Signed.int -> schar | |
103 | val c_uchar : MLRep.Char.Unsigned.word -> uchar | |
104 | val c_sshort : MLRep.Short.Signed.int -> sshort | |
105 | val c_ushort : MLRep.Short.Unsigned.word -> ushort | |
106 | val c_sint : MLRep.Int.Signed.int -> sint | |
107 | val c_uint : MLRep.Int.Unsigned.word -> uint | |
108 | val c_slong : MLRep.Long.Signed.int -> slong | |
109 | val c_ulong : MLRep.Long.Unsigned.word -> ulong | |
110 | val c_slonglong : MLRep.LongLong.Signed.int -> slonglong | |
111 | val c_ulonglong : MLRep.LongLong.Unsigned.word -> ulonglong | |
112 | val c_float : MLRep.Float.real -> float | |
113 | val c_double : MLRep.Double.real -> double | |
114 | val i2c_enum : MLRep.Int.Signed.int -> 'e enum | |
115 | ||
116 | (* C -> ML *) | |
117 | val ml_schar : schar -> MLRep.Char.Signed.int | |
118 | val ml_uchar : uchar -> MLRep.Char.Unsigned.word | |
119 | val ml_sshort : sshort -> MLRep.Short.Signed.int | |
120 | val ml_ushort : ushort -> MLRep.Short.Unsigned.word | |
121 | val ml_sint : sint -> MLRep.Int.Signed.int | |
122 | val ml_uint : uint -> MLRep.Int.Unsigned.word | |
123 | val ml_slong : slong -> MLRep.Long.Signed.int | |
124 | val ml_ulong : ulong -> MLRep.Long.Unsigned.word | |
125 | val ml_slonglong : slonglong -> MLRep.LongLong.Signed.int | |
126 | val ml_ulonglong : ulonglong -> MLRep.LongLong.Unsigned.word | |
127 | val ml_float : float -> MLRep.Float.real | |
128 | val ml_double : double -> MLRep.Double.real | |
129 | val c2i_enum : 'e enum -> MLRep.Int.Signed.int | |
130 | end | |
131 | ||
132 | (* type-abbreviations for a bit more convenience. *) | |
133 | type 'c schar_obj = ( schar, 'c) obj | |
134 | type 'c uchar_obj = ( uchar, 'c) obj | |
135 | type 'c sshort_obj = ( sshort, 'c) obj | |
136 | type 'c ushort_obj = ( ushort, 'c) obj | |
137 | type 'c sint_obj = ( sint, 'c) obj | |
138 | type 'c uint_obj = ( uint, 'c) obj | |
139 | type 'c slong_obj = ( slong, 'c) obj | |
140 | type 'c ulong_obj = ( ulong, 'c) obj | |
141 | type 'c slonglong_obj = (slonglong, 'c) obj | |
142 | type 'c ulonglong_obj = (ulonglong, 'c) obj | |
143 | type 'c float_obj = ( float, 'c) obj | |
144 | type 'c double_obj = ( double, 'c) obj | |
145 | type 'c voidptr_obj = ( voidptr, 'c) obj | |
146 | type ('e, 'c) enum_obj = ( 'e enum, 'c) obj | |
147 | type ('f, 'c) fptr_obj = ( 'f fptr, 'c) obj | |
148 | type ('s, 'c) su_obj = ( 's su, 'c) obj | |
149 | ||
150 | (* light-weight alternatives *) | |
151 | type 'c schar_obj' = ( schar, 'c) obj' | |
152 | type 'c uchar_obj' = ( uchar, 'c) obj' | |
153 | type 'c sshort_obj' = ( sshort, 'c) obj' | |
154 | type 'c ushort_obj' = ( ushort, 'c) obj' | |
155 | type 'c sint_obj' = ( sint, 'c) obj' | |
156 | type 'c uint_obj' = ( uint, 'c) obj' | |
157 | type 'c slong_obj' = ( slong, 'c) obj' | |
158 | type 'c ulong_obj' = ( ulong, 'c) obj' | |
159 | type 'c slonglong_obj' = (slonglong, 'c) obj' | |
160 | type 'c ulonglong_obj' = (ulonglong, 'c) obj' | |
161 | type 'c float_obj' = ( float, 'c) obj' | |
162 | type 'c double_obj' = ( double, 'c) obj' | |
163 | type 'c voidptr_obj' = ( voidptr, 'c) obj' | |
164 | type ('e, 'c) enum_obj' = ( 'e enum, 'c) obj' | |
165 | type ('f, 'c) fptr_obj' = ( 'f fptr, 'c) obj' | |
166 | type ('s, 'c) su_obj' = ( 's su, 'c) obj' | |
167 | ||
168 | (* bitfields aren't "ordinary objects", so they have their own type *) | |
169 | eqtype 'c sbf and 'c ubf | |
170 | ||
171 | structure W : sig | |
172 | (* conversion "witness" values *) | |
173 | type ('from, 'to) witness | |
174 | ||
175 | (* A small calculus for generating new witnesses. | |
176 | * Since the only witness constructors that do anything real are | |
177 | * rw and ro, all this calculus gives you is a way of changing | |
178 | * "const" attributes at any level within a bigger type. | |
179 | * | |
180 | * (The calculus can express nonsensical witnesses -- which | |
181 | * fortunately are harmless because they can't be applied to any | |
182 | * values.) *) | |
183 | val trivial : ('t, 't) witness | |
184 | ||
185 | val pointer : ('from, 'to) witness -> | |
186 | ('from ptr, 'to ptr) witness | |
187 | val object : ('from, 'to) witness -> | |
188 | (('from, 'c) obj, ('to, 'c) obj) witness | |
189 | val arr : ('from, 'to) witness -> | |
190 | (('from, 'n) arr, ('to, 'n) arr) witness | |
191 | ||
192 | val ro : ('from, 'to) witness -> | |
193 | (('from, 'fc) obj, ('to, ro) obj) witness | |
194 | val rw : ('from, 'to) witness -> | |
195 | (('from, 'fc) obj, ('to, 'tc) obj) witness | |
196 | end | |
197 | ||
198 | (* Object conversions that rely on witnesses: *) | |
199 | val convert : (('st, 'sc) obj, ('tt, 'tc) obj) W.witness -> | |
200 | ('st, 'sc) obj -> ('tt, 'tc) obj | |
201 | val convert' : (('st, 'sc) obj, ('tt, 'tc) obj) W.witness -> | |
202 | ('st, 'sc) obj' -> ('tt, 'tc) obj' | |
203 | ||
204 | (* | |
205 | * A family of types and corresponding values representing natural numbers. | |
206 | * (An encoding in SML without using dependent types.) | |
207 | *) | |
208 | structure Dim : sig | |
209 | ||
210 | (* Internally, a value of type ('a, 'z) dim0 is just a number. | |
211 | * The trick here is to give each of these numbers a different unique | |
212 | * type. 'a will be a decimal encoding of the number's value in | |
213 | * "type digits". 'z keeps track of whether the number is zero or not. | |
214 | *) | |
215 | type ('a, 'z) dim0 | |
216 | ||
217 | (* We can always get the internal number back... *) | |
218 | val toInt : ('a, 'z) dim0 -> int | |
219 | ||
220 | (* These two types act as "flags". They will be substituted for 'z | |
221 | * and remember whether the value is zero or not. *) | |
222 | type zero | |
223 | type nonzero | |
224 | ||
225 | type 'a dim = ('a, nonzero) dim0 | |
226 | ||
227 | (* These are the "type digits". Type "dec" acts as a "terminator". | |
228 | * We chose its name so to remind us that the encoding is decimal. | |
229 | * If a nonzero value's decimal representation is "<Dn>...<D0>", then | |
230 | * its type will be "(dec dg<Dn> ... dg<D0>, nonzero) dim0", which | |
231 | * is the same as "dec dg<Dn> ... dg<D0> dim". The type of the zero | |
232 | * value is "(dec, zero) dim0". *) | |
233 | type dec | |
234 | type 'a dg0 and 'a dg1 and 'a dg2 and 'a dg3 and 'a dg4 | |
235 | type 'a dg5 and 'a dg6 and 'a dg7 and 'a dg8 and 'a dg9 | |
236 | ||
237 | (* Here are the corresponding constructors for ('a, 'z) dim0 values. | |
238 | * The type for dg0 ensures that there will be no "leading zeros" in | |
239 | * any encoding. This guarantees a 1-1 correspondence of constructable | |
240 | * values and their types. | |
241 | * To construct the value corresponding to a nonzero number whose | |
242 | * decimal representation is "<Dn>...<D0>", one must invoke | |
243 | * "dg<D0>' (... (dg<Dn>' dec')...)", i.e., the least significant | |
244 | * digit appears leftmost. *) | |
245 | val dec' : (dec, zero) dim0 | |
246 | val dg0' : 'a dim -> 'a dg0 dim | |
247 | val dg1' : ('a, 'z) dim0 -> 'a dg1 dim | |
248 | val dg2' : ('a, 'z) dim0 -> 'a dg2 dim | |
249 | val dg3' : ('a, 'z) dim0 -> 'a dg3 dim | |
250 | val dg4' : ('a, 'z) dim0 -> 'a dg4 dim | |
251 | val dg5' : ('a, 'z) dim0 -> 'a dg5 dim | |
252 | val dg6' : ('a, 'z) dim0 -> 'a dg6 dim | |
253 | val dg7' : ('a, 'z) dim0 -> 'a dg7 dim | |
254 | val dg8' : ('a, 'z) dim0 -> 'a dg8 dim | |
255 | val dg9' : ('a, 'z) dim0 -> 'a dg9 dim | |
256 | ||
257 | (* Since having to reverse the sequence of digits seems unnatural, | |
258 | * here is another set of constructors for dim values. These | |
259 | * constructors use continuation-passing style and themselves | |
260 | * have more complicated types. But their use is easier: | |
261 | * To construct the value corresponding to a nonzero number whose | |
262 | * decimal representation is "<Dn>...<D0>", one must invoke | |
263 | * "dec dg<Dn> ... dg<D0> dim"; i.e., the least significant | |
264 | * digit appears rightmost -- just like in the usual decimal | |
265 | * notation for numbers that we are all familiar with. | |
266 | * [Moreover, for any 'a dim value we have the neat property that | |
267 | * it can be constructed by taking its type (expressed using "dim") | |
268 | * and interpreting it as an expression. For example, the dim | |
269 | * value representing 312 is "dec dg3 dg1 dg2 dim" and it can | |
270 | * be constructed by evaluating "dec dg3 dg1 dg2 dim".] *) | |
271 | val dec : ((dec, zero) dim0 -> 'b) -> 'b | |
272 | ||
273 | val dg0 : 'a dim -> ('a dg0 dim -> 'b) -> 'b | |
274 | val dg1 : ('a, 'z) dim0 -> ('a dg1 dim -> 'b) -> 'b | |
275 | val dg2 : ('a, 'z) dim0 -> ('a dg2 dim -> 'b) -> 'b | |
276 | val dg3 : ('a, 'z) dim0 -> ('a dg3 dim -> 'b) -> 'b | |
277 | val dg4 : ('a, 'z) dim0 -> ('a dg4 dim -> 'b) -> 'b | |
278 | val dg5 : ('a, 'z) dim0 -> ('a dg5 dim -> 'b) -> 'b | |
279 | val dg6 : ('a, 'z) dim0 -> ('a dg6 dim -> 'b) -> 'b | |
280 | val dg7 : ('a, 'z) dim0 -> ('a dg7 dim -> 'b) -> 'b | |
281 | val dg8 : ('a, 'z) dim0 -> ('a dg8 dim -> 'b) -> 'b | |
282 | val dg9 : ('a, 'z) dim0 -> ('a dg9 dim -> 'b) -> 'b | |
283 | ||
284 | val dim : ('a, 'z) dim0 -> ('a, 'z) dim0 | |
285 | end | |
286 | ||
287 | (* sub-structure for dealing with run-time type info (sizes only) *) | |
288 | structure S : sig | |
289 | ||
290 | (* Our size info itself is statically typed! | |
291 | * The size info for a value stored in ('t, 'c) obj has | |
292 | * the following type: *) | |
293 | type 't size | |
294 | ||
295 | (* get a number out *) | |
296 | val toWord : 't size -> word | |
297 | ||
298 | (* sizes for simple things *) | |
299 | val schar : schar size | |
300 | val uchar : uchar size | |
301 | val sshort : sshort size | |
302 | val ushort : ushort size | |
303 | val sint : sint size | |
304 | val uint : uint size | |
305 | val slong : slong size | |
306 | val ulong : ulong size | |
307 | val slonglong : slonglong size | |
308 | val ulonglong : ulonglong size | |
309 | val float : float size | |
310 | val double : double size | |
311 | ||
312 | val voidptr : voidptr size | |
313 | val ptr : 'o ptr size | |
314 | val fptr : 'f fptr size | |
315 | val enum : 'tag enum size | |
316 | end | |
317 | ||
318 | (* sub-structure for dealing with run-time type info *) | |
319 | structure T : sig | |
320 | ||
321 | (* Our RTTI itself is statically typed! | |
322 | * The RTTI for a value stored in ('t, 'c) obj has | |
323 | * the following type: *) | |
324 | type 't typ | |
325 | ||
326 | (* get the RTTI from an actual object *) | |
327 | val typeof : ('t, 'c) obj -> 't typ | |
328 | ||
329 | (* constructing new RTTI from existing RTTI *) | |
330 | val pointer : 't typ -> ('t, rw) obj ptr typ | |
331 | val target : ('t, 'c) obj ptr typ -> 't typ | |
332 | val arr : 't typ * 'n Dim.dim -> ('t, 'n) arr typ | |
333 | val elem : ('t, 'n) arr typ -> 't typ | |
334 | val ro : ('t, 'c) obj ptr typ -> ('t, ro) obj ptr typ | |
335 | ||
336 | (* calculating the size of an object given its RTTI *) | |
337 | val sizeof : 't typ -> 't S.size | |
338 | ||
339 | (* dimension of array type *) | |
340 | val dim : ('t, 'n) arr typ -> 'n Dim.dim | |
341 | ||
342 | (* RTTI for simple things *) | |
343 | val schar : schar typ | |
344 | val uchar : uchar typ | |
345 | val sshort : sshort typ | |
346 | val ushort : ushort typ | |
347 | val sint : sint typ | |
348 | val uint : uint typ | |
349 | val slong : slong typ | |
350 | val ulong : ulong typ | |
351 | val slonglong : slonglong typ | |
352 | val ulonglong : ulonglong typ | |
353 | val float : float typ | |
354 | val double : double typ | |
355 | ||
356 | val voidptr : voidptr typ | |
357 | ||
358 | val enum : 'tag enum typ | |
359 | end | |
360 | ||
361 | (* convert from regular (heavy) to alternative (light) versions *) | |
362 | structure Light : sig | |
363 | val obj : ('t, 'c) obj -> ('t, 'c) obj' | |
364 | val ptr : 'o ptr -> 'o ptr' | |
365 | val fptr : 'f fptr -> 'f fptr' | |
366 | end | |
367 | ||
368 | (* and vice versa *) | |
369 | structure Heavy : sig | |
370 | val obj : 't T.typ -> ('t, 'c) obj' -> ('t, 'c) obj | |
371 | val ptr : 'o ptr T.typ -> 'o ptr' -> 'o ptr | |
372 | val fptr : 'f fptr T.typ -> 'f fptr' -> 'f fptr | |
373 | end | |
374 | ||
375 | (* calculate size of an object *) | |
376 | val sizeof : ('t, 'c) obj -> 't S.size | |
377 | ||
378 | (* "fetch" methods for various types; | |
379 | * fetching does not care about constness *) | |
380 | structure Get : sig | |
381 | (* primitive types; the results are concrete here *) | |
382 | val schar : 'c schar_obj -> MLRep.Char.Signed.int | |
383 | val uchar : 'c uchar_obj -> MLRep.Char.Unsigned.word | |
384 | val sshort : 'c sshort_obj -> MLRep.Short.Signed.int | |
385 | val ushort : 'c ushort_obj -> MLRep.Short.Unsigned.word | |
386 | val sint : 'c sint_obj -> MLRep.Int.Signed.int | |
387 | val uint : 'c uint_obj -> MLRep.Int.Unsigned.word | |
388 | val slong : 'c slong_obj -> MLRep.Long.Signed.int | |
389 | val ulong : 'c ulong_obj -> MLRep.Long.Unsigned.word | |
390 | val slonglong : 'c slonglong_obj -> MLRep.LongLong.Signed.int | |
391 | val ulonglong : 'c ulonglong_obj -> MLRep.LongLong.Unsigned.word | |
392 | val float : 'c float_obj -> MLRep.Float.real | |
393 | val double : 'c double_obj -> MLRep.Double.real | |
394 | val enum : ('e, 'c) enum_obj -> MLRep.Int.Signed.int | |
395 | ||
396 | (* alt *) | |
397 | val schar' : 'c schar_obj' -> MLRep.Char.Signed.int | |
398 | val uchar' : 'c uchar_obj' -> MLRep.Char.Unsigned.word | |
399 | val sshort' : 'c sshort_obj' -> MLRep.Short.Signed.int | |
400 | val ushort' : 'c ushort_obj' -> MLRep.Short.Unsigned.word | |
401 | val sint' : 'c sint_obj' -> MLRep.Int.Signed.int | |
402 | val uint' : 'c uint_obj' -> MLRep.Int.Unsigned.word | |
403 | val slong' : 'c slong_obj' -> MLRep.Long.Signed.int | |
404 | val ulong' : 'c ulong_obj' -> MLRep.Long.Unsigned.word | |
405 | val slonglong' : 'c slonglong_obj' -> MLRep.LongLong.Signed.int | |
406 | val ulonglong' : 'c ulonglong_obj' -> MLRep.LongLong.Unsigned.word | |
407 | val float' : 'c float_obj' -> MLRep.Float.real | |
408 | val double' : 'c double_obj' -> MLRep.Double.real | |
409 | val enum' : ('e, 'c) enum_obj' -> MLRep.Int.Signed.int | |
410 | ||
411 | (* fetching pointers; results have to be abstract *) | |
412 | val ptr : ('o ptr, 'c) obj -> 'o ptr | |
413 | val fptr : ('f, 'c) fptr_obj -> 'f fptr | |
414 | val voidptr : 'c voidptr_obj -> voidptr | |
415 | ||
416 | (* alt *) | |
417 | val ptr' : ('o ptr, 'c) obj' -> 'o ptr' | |
418 | val fptr' : ('f, 'c) fptr_obj' -> 'f fptr' | |
419 | val voidptr' : 'c voidptr_obj' -> voidptr | |
420 | ||
421 | (* bitfields; concrete again *) | |
422 | val sbf : 'c sbf -> MLRep.Int.Signed.int | |
423 | val ubf : 'c ubf -> MLRep.Int.Unsigned.word | |
424 | end | |
425 | ||
426 | (* "store" methods; these require rw objects *) | |
427 | structure Set : sig | |
428 | (* primitive types; use concrete values *) | |
429 | val schar : rw schar_obj * MLRep.Char.Signed.int -> unit | |
430 | val uchar : rw uchar_obj * MLRep.Char.Unsigned.word -> unit | |
431 | val sshort : rw sshort_obj * MLRep.Short.Signed.int -> unit | |
432 | val ushort : rw ushort_obj * MLRep.Short.Unsigned.word -> unit | |
433 | val sint : rw sint_obj * MLRep.Int.Signed.int -> unit | |
434 | val uint : rw uint_obj * MLRep.Int.Unsigned.word -> unit | |
435 | val slong : rw slong_obj * MLRep.Long.Signed.int -> unit | |
436 | val ulong : rw ulong_obj * MLRep.Long.Unsigned.word -> unit | |
437 | val slonglong : rw slonglong_obj * MLRep.LongLong.Signed.int -> unit | |
438 | val ulonglong : rw ulonglong_obj * MLRep.LongLong.Unsigned.word -> unit | |
439 | val float : rw float_obj * MLRep.Float.real -> unit | |
440 | val double : rw double_obj * MLRep.Double.real -> unit | |
441 | val enum : ('e, rw) enum_obj * MLRep.Int.Signed.int -> unit | |
442 | ||
443 | (* alt *) | |
444 | val schar' : rw schar_obj' * MLRep.Char.Signed.int -> unit | |
445 | val uchar' : rw uchar_obj' * MLRep.Char.Unsigned.word -> unit | |
446 | val sshort' : rw sshort_obj' * MLRep.Short.Signed.int -> unit | |
447 | val ushort' : rw ushort_obj' * MLRep.Short.Unsigned.word -> unit | |
448 | val sint' : rw sint_obj' * MLRep.Int.Signed.int -> unit | |
449 | val uint' : rw uint_obj' * MLRep.Int.Unsigned.word -> unit | |
450 | val slong' : rw slong_obj' * MLRep.Long.Signed.int -> unit | |
451 | val ulong' : rw ulong_obj' * MLRep.Long.Unsigned.word -> unit | |
452 | val slonglong' : rw slonglong_obj' * MLRep.LongLong.Signed.int -> unit | |
453 | val ulonglong' : rw ulonglong_obj' * MLRep.LongLong.Unsigned.word -> unit | |
454 | val float' : rw float_obj' * MLRep.Float.real -> unit | |
455 | val double' : rw double_obj' * MLRep.Double.real -> unit | |
456 | val enum' : ('e, rw) enum_obj' * MLRep.Int.Signed.int -> unit | |
457 | ||
458 | (* storing pointers; abstract *) | |
459 | val ptr : ('o ptr, rw) obj * 'o ptr -> unit | |
460 | val fptr : ('f, rw) fptr_obj * 'f fptr -> unit | |
461 | val voidptr : rw voidptr_obj * voidptr -> unit | |
462 | ||
463 | (* alt *) | |
464 | val ptr' : ('o ptr, rw) obj' * 'o ptr' -> unit | |
465 | val fptr' : ('f, rw) fptr_obj' * 'f fptr' -> unit | |
466 | val voidptr' : rw voidptr_obj' * voidptr -> unit | |
467 | ||
468 | (* When storing, voidptr is compatible with any ptr type | |
469 | * (just like in C). This should eliminate most need for RTTI in | |
470 | * practice. *) | |
471 | val ptr_voidptr : ('o ptr, rw) obj * voidptr -> unit | |
472 | ||
473 | (* alt *) | |
474 | val ptr_voidptr' : ('o ptr, rw) obj' * voidptr -> unit | |
475 | ||
476 | (* bitfields; concrete *) | |
477 | val sbf : rw sbf * MLRep.Int.Signed.int -> unit | |
478 | val ubf : rw ubf * MLRep.Int.Unsigned.word -> unit | |
479 | end | |
480 | ||
481 | (* copying the contents of arbitrary objects *) | |
482 | val copy : { from: ('t, 'c) obj, to: ('t, rw) obj } -> unit | |
483 | ||
484 | (* alt *) | |
485 | val copy' : 't S.size -> { from: ('t, 'c) obj', to: ('t, rw) obj' } -> unit | |
486 | ||
487 | (* manipulating object constness | |
488 | * rw -> ro: this direction just accounts for the fact that | |
489 | * rw is conceptually a subtype of ro | |
490 | * ro -> rw: this is not safe, but C makes it so easy that we | |
491 | * might as well directly support it; | |
492 | * Concretely, we make both operations polymorphic in the argument | |
493 | * constness. Moreover, the second (unsafe) direction is also | |
494 | * polymorphic in the result. This can be used to effectively | |
495 | * implement a conversion to "whatever the context wants". | |
496 | * | |
497 | * Note: fun ro x = convert (W.ro W.trivial) x | |
498 | * etc. | |
499 | *) | |
500 | val ro : ('t, 'c) obj -> ('t, ro) obj | |
501 | val rw : ('t, 'sc) obj -> ('t, 'tc) obj | |
502 | ||
503 | (* alt *) | |
504 | val ro' : ('t, 'c) obj' -> ('t, ro) obj' | |
505 | val rw' : ('t, 'sc) obj' -> ('t, 'tc) obj' | |
506 | ||
507 | (* operations on (mostly) pointers *) | |
508 | structure Ptr : sig | |
509 | ||
510 | (* going from object to pointer and vice versa *) | |
511 | val |&| : ('t, 'c) obj -> ('t, 'c) obj ptr | |
512 | val |*| : ('t, 'c) obj ptr -> ('t, 'c) obj | |
513 | ||
514 | (* alt *) | |
515 | val |&! : ('t, 'c) obj' -> ('t, 'c) obj ptr' | |
516 | val |*! : ('t, 'c) obj ptr' -> ('t, 'c) obj' | |
517 | ||
518 | (* comparing pointers *) | |
519 | val compare : 'o ptr * 'o ptr -> order | |
520 | ||
521 | (* alt *) | |
522 | val compare' : 'o ptr' * 'o ptr' -> order | |
523 | ||
524 | (* going from pointer to void*; this also accounts for a conceptual | |
525 | * subtyping relation and is safe *) | |
526 | val inject : 'o ptr -> voidptr | |
527 | ||
528 | (* alt *) | |
529 | val inject' : 'o ptr' -> voidptr | |
530 | ||
531 | (* the opposite is not safe, but C makes it not only easy but also | |
532 | * almost necessary; we use our RTTI interface to specify the pointer | |
533 | * type (not the element type!) *) | |
534 | val cast : 'o ptr T.typ -> voidptr -> 'o ptr | |
535 | ||
536 | (* alt, needs explicit type constraint on result! *) | |
537 | val cast' : voidptr -> 'o ptr' | |
538 | ||
539 | (* NULL as void* *) | |
540 | val vnull : voidptr | |
541 | ||
542 | (* projecting vnull to given pointer type *) | |
543 | val null : 'o ptr T.typ -> 'o ptr | |
544 | ||
545 | (* the "light" NULL pointer is simply a polymorphic constant *) | |
546 | val null' : 'o ptr' | |
547 | ||
548 | (* fptr version of NULL *) | |
549 | val fnull : 'f fptr T.typ -> 'f fptr | |
550 | ||
551 | (* again, "light" version is simply a polymorphic constant *) | |
552 | val fnull' : 'f fptr' | |
553 | ||
554 | (* checking for NULL pointer *) | |
555 | val isVNull : voidptr -> bool | |
556 | ||
557 | (* combining inject and isVNull for convenience *) | |
558 | val isNull : 'o ptr -> bool | |
559 | ||
560 | (* alt *) | |
561 | val isNull' : 'o ptr' -> bool | |
562 | ||
563 | (* checking a function pointer for NULL *) | |
564 | val isFNull : 'f fptr -> bool | |
565 | ||
566 | (* alt *) | |
567 | val isFNull' : 'f fptr' -> bool | |
568 | ||
569 | (* pointer arithmetic *) | |
570 | val |+| : ('t, 'c) obj ptr * int -> ('t, 'c) obj ptr | |
571 | val |-| : ('t, 'c) obj ptr * ('t, 'c) obj ptr -> int | |
572 | ||
573 | (* alt; needs explicit size (for element) *) | |
574 | val |+! : 't S.size -> ('t, 'c) obj ptr' * int -> ('t, 'c) obj ptr' | |
575 | val |-! : 't S.size -> ('t, 'c) obj ptr' * ('t, 'c) obj ptr' -> int | |
576 | ||
577 | (* subscript through a pointer; this is unchecked *) | |
578 | val sub : ('t, 'c) obj ptr * int -> ('t, 'c) obj | |
579 | ||
580 | (* alt; needs explicit size (for element) *) | |
581 | val sub' : 't S.size -> ('t, 'c) obj ptr' * int -> ('t, 'c) obj' | |
582 | ||
583 | (* conversions that rely on witnesses *) | |
584 | val convert : (('st, 'sc) obj ptr, ('tt, 'tc) obj ptr) W.witness -> | |
585 | ('st, 'sc) obj ptr -> ('tt, 'tc) obj ptr | |
586 | val convert' : (('st, 'sc) obj ptr, ('tt, 'tc) obj ptr) W.witness -> | |
587 | ('st, 'sc) obj ptr' -> ('tt, 'tc) obj ptr' | |
588 | ||
589 | (* constness manipulation for pointers | |
590 | * Note: fun ro x = convert (W.pointer (W.ro W.trivial)) x | |
591 | * etc. *) | |
592 | val ro : ('t, 'c) obj ptr -> ('t, ro) obj ptr | |
593 | val rw : ('t, 'sc) obj ptr -> ('t, 'tc) obj ptr | |
594 | val ro' : ('t, 'c) obj ptr' -> ('t, ro) obj ptr' | |
595 | val rw' : ('t, 'sc) obj ptr' -> ('t, 'tc) obj ptr' | |
596 | end | |
597 | ||
598 | (* operations on (mostly) arrays *) | |
599 | structure Arr : sig | |
600 | ||
601 | (* array subscript; | |
602 | * since we have RTTI, we can actually make this safe: we raise | |
603 | * General.Subscript for out-of-bounds access; | |
604 | * for unchecked access, go through arr_decay and ptr_sub | |
605 | *) | |
606 | val sub : (('t, 'n) arr, 'c) obj * int -> ('t, 'c) obj | |
607 | ||
608 | (* alt; needs element size and array dimension *) | |
609 | val sub' : 't S.size * 'n Dim.dim -> | |
610 | (('t, 'n) arr, 'c) obj' * int -> ('t, 'c) obj' | |
611 | ||
612 | (* let an array object decay, yielding pointer to first element *) | |
613 | val decay : (('t, 'n) arr, 'c) obj -> ('t, 'c) obj ptr | |
614 | ||
615 | (* alt *) | |
616 | val decay' : (('t, 'n) arr, 'c) obj' -> ('t, 'c) obj ptr' | |
617 | ||
618 | (* reconstruct an array object from the pointer to its first element *) | |
619 | val reconstruct : | |
620 | ('t, 'c) obj ptr * 'n Dim.dim -> (('t, 'n) arr, 'c) obj | |
621 | ||
622 | (* alt *) | |
623 | val reconstruct': | |
624 | ('t, 'c) obj ptr' * 'n Dim.dim -> (('t, 'n) arr, 'c) obj' | |
625 | ||
626 | (* dimension of array object *) | |
627 | val dim : (('t, 'n) arr, 'c) obj -> 'n Dim.dim | |
628 | end | |
629 | ||
630 | (* allocating new objects *) | |
631 | val new : 't T.typ -> ('t, 'c) obj | |
632 | ||
633 | (* alt *) | |
634 | val new' : 't S.size -> ('t, 'c) obj' | |
635 | ||
636 | (* freeing objects that were allocated earlier *) | |
637 | val discard : ('t, 'c) obj -> unit | |
638 | ||
639 | (* alt *) | |
640 | val discard' : ('t, 'c) obj' -> unit | |
641 | ||
642 | (* allocating a dynamically-sized array *) | |
643 | val alloc : 't T.typ -> word -> ('t, 'c) obj ptr | |
644 | ||
645 | (* alt *) | |
646 | val alloc' : 't S.size -> word -> ('t, 'c) obj ptr' | |
647 | ||
648 | (* freeing through pointers *) | |
649 | val free : 'o ptr -> unit | |
650 | ||
651 | (* alt *) | |
652 | val free' : 'o ptr' -> unit | |
653 | ||
654 | (* perform function call through function-pointer *) | |
655 | val call : ('a -> 'b) fptr * 'a -> 'b | |
656 | ||
657 | (* alt; needs explicit type for the function pointer *) | |
658 | val call' : ('a -> 'b) fptr T.typ -> ('a -> 'b) fptr' * 'a -> 'b | |
659 | ||
660 | (* completely unsafe stuff that every C programmer just *loves* to do *) | |
661 | structure U : sig | |
662 | val fcast : 'a fptr' -> 'b fptr' | |
663 | val p2i : 'o ptr' -> ulong | |
664 | val i2p : ulong -> 'o ptr' | |
665 | end | |
666 | end |