#
# Encoding the C type system in Mythryl.
#
# (C) 2001, Lucent Technologies, Bell Laboratories
#
# author: Matthias Blume
# Compiled by:
# src/lib/c-glue-lib/internals/c-internals.libapi Ctypes {
exception OUT_OF_MEMORY;
# Chunks of type T, constness C.
#
# The T type variable will be the chunk's "witness" type.
# The intention is that there be an isomorphism between such
# witness types and corresponding C types.
#
# Witness types are often the same as the (abstract) type of the value
# stored in the chunk. However, this is merely a coincidence. For
# example, a constant chunk holding a pointer to a read-write integer
# would have type Chunk (Ptr (Sint, Rw), Ro) and the value itself has
# type Ptr (Sint, Rw).
# However, in the case of the "light" version of this chunk (see below),
# the chunk type is Chunk' (Ptr (Sint, Rw), Ro) while fetching
# from this chunk gives a value of type Ptr' (Sint, Rw).
# (In other words, we use the "heavy" versions of value types as witness
# types -- even in the "light" case.)
Chunk (T, C);
# An alternative "light-weight" version that does not carry
# run-time type information (RTTI) at the cost of requiring
# explicit passing of RTTI for certain operations:
eqtype Chunk' (T, C);
# Constness property, to be substituted for C
Ro also Rw;
# Pointers come in two varieties in C: Pointers to things we
# know and pointers to "incomplete" types. The "ptr" type constructor
# below encodes both kinds using the following convention:
#
# - In the case of complete target types, O will be
# some Chunk(T, C).
#
# - In the case of incomplete target types, O will
# some fresh (abstract) type. (See iptr.api for what this will
# look like in practice)
Ptr( O ); # pointer to O
Arr( T, N ); # N-sized Rw_Vector with T elements
# Light-weight alternative (no implicit RTTI):
eqtype Ptr'( O );
eqtype Void; # no values, admits equality
# void* is really a base type, but it happens to take the
# form of a light-weight pointer type (with an abstract target).
# This design makes it possible to use those ptr-related
# functions that "make sense" for void*.
Voidptr = Ptr'( Void ); # C's void*
# Function pointers
Fptr( F ); # A function pointer
# Lightweight function pointers:
eqtype Fptr'( F );
# Structures and unions:
Su( A_tag ); # struct/union named A_tag;
# A_tag is drawn from the types
# defined in the Tag module
# Enumerations:
eqtype An_Enum( A_tag );
# Primtypes (signed/unsigned char, int, short, long; float, double)
eqtype Schar also Uchar;
eqtype Sint also Uint;
eqtype Sshort also Ushort;
eqtype Slong also Ulong;
eqtype Slonglong also Ulonglong;
Float also Double;
# Going from abstract to concrete and vice versa.
# (This shouldn't be needed except when calling
# functions through function pointers.)
package convert:
api {
# Mythryl -> C
c_schar: mlrep::signed::Int -> Schar;
c_uchar: mlrep::unsigned::Unt -> Uchar;
c_sint: mlrep::signed::Int -> Sint;
c_uint: mlrep::unsigned::Unt -> Uint;
c_sshort: mlrep::signed::Int -> Sshort;
c_ushort: mlrep::unsigned::Unt -> Ushort;
c_slong: mlrep::signed::Int -> Slong;
c_ulong: mlrep::unsigned::Unt -> Ulong;
c_slonglong: mlrep::long_long_signed::Int -> Slonglong;
c_ulonglong: mlrep::long_long_unsigned::Unt -> Ulonglong;
c_float: mlrep::float::Float -> Float;
c_double: mlrep::float::Float -> Double;
i2c_enum: mlrep::signed::Int -> An_Enum( E );
# C -> Mythryl
ml_schar: Schar -> mlrep::signed::Int;
ml_uchar: Uchar -> mlrep::unsigned::Unt;
ml_sint: Sint -> mlrep::signed::Int;
ml_uint: Uint -> mlrep::unsigned::Unt;
ml_sshort: Sshort -> mlrep::signed::Int;
ml_ushort: Ushort -> mlrep::unsigned::Unt;
ml_slong: Slong -> mlrep::signed::Int;
ml_ulong: Ulong -> mlrep::unsigned::Unt;
ml_slonglong: Slonglong -> mlrep::long_long_signed::Int;
ml_ulonglong: Ulonglong -> mlrep::long_long_unsigned::Unt;
ml_float: Float -> mlrep::float::Float;
ml_double: Double -> mlrep::float::Float;
c2i_enum: An_Enum( E ) -> mlrep::signed::Int;
};
# Type-abbreviations for a bit more convenience.
Schar_Chunk( C ) = Chunk( Schar, C );
Uchar_Chunk( C ) = Chunk( Uchar, C );
Sint_Chunk( C ) = Chunk( Sint, C );
Uint_Chunk( C ) = Chunk( Uint, C );
Sshort_Chunk( C ) = Chunk( Sshort, C );
Ushort_Chunk( C ) = Chunk( Ushort, C );
Slong_Chunk( C ) = Chunk( Slong, C );
Ulong_Chunk( C ) = Chunk( Ulong, C );
Slonglong_Chunk( C ) = Chunk( Slonglong, C );
Ulonglong_Chunk( C ) = Chunk( Ulonglong, C );
Float_Chunk( C ) = Chunk( Float, C );
Double_Chunk( C ) = Chunk( Double, C );
Voidptr_Chunk( C ) = Chunk( Voidptr, C );
Enum_Chunk( E, C ) = Chunk( An_Enum( E ), C );
Fptr_Chunk( F, C ) = Chunk( Fptr( F ), C );
Su_Chunk( S, C ) = Chunk( Su( S ), C );
# Alternate lightweight versions (no implicit RTTI):
Schar_Chunk'( C ) = Chunk'( Schar, C );
Uchar_Chunk'( C ) = Chunk'( Uchar, C );
Sint_Chunk'( C ) = Chunk'( Sint, C );
Uint_Chunk'( C ) = Chunk'( Uint, C );
Sshort_Chunk'( C ) = Chunk'( Sshort, C );
Ushort_Chunk'( C ) = Chunk'( Ushort, C );
Slong_Chunk'( C ) = Chunk'( Slong, C );
Ulong_Chunk'( C ) = Chunk'( Ulong, C );
Slonglong_Chunk'( C ) = Chunk'( Slonglong, C );
Ulonglong_Chunk'( C ) = Chunk'( Ulonglong, C );
Float_Chunk'( C ) = Chunk'( Float, C );
Double_Chunk'( C ) = Chunk'( Double, C );
Voidptr_Chunk'( C ) = Chunk'( Voidptr, C );
Enum_Chunk' (E, C ) = Chunk'( An_Enum( E ), C );
Fptr_Chunk' (F, C ) = Chunk'( Fptr( F ), C);
Su_Chunk' (S, C ) = Chunk'( Su( S ), C );
# Bitfields aren't "ordinary chunks",
# so they have their own type:
eqtype Sbf C # "Sbf" == "signed bitfield"
also Ubf C; # "Ubf" == "unsigned bitfield"
package w:
api {
# Conversion "witness" values
Witness( A_from, A_to );
# A small calculus for generating new witnesses.
# Since the only witness constructors that do anything real are
# rw and ro, all this calculus gives you is a way of changing
# "const" attributes at any level within a bigger type.
#
# (The calculus can express nonsensical witnesses -- which
# fortunately are harmless because they can't be applied to any
# values.)
trivial: Witness( T, T );
pointer: Witness( A_from, A_to ) -> Witness( Ptr( A_from ), Ptr( A_to ) );
chunk: Witness( A_st, A_tt ) -> Witness (Chunk( A_st, C ), Chunk( A_tt, C ));
arr: Witness( A_st, A_tt ) -> Witness (Arr( A_st, N ), Arr( A_tt, N ));
ro: Witness( A_st, A_tt ) -> Witness (Chunk( A_st, C ), Chunk( A_tt, Ro ));
rw: Witness( A_st, A_tt ) -> Witness (Chunk( A_st, A_sc ), Chunk( A_tt, A_tc ));
};
# Chunk conversions that rely on witnesses:
convert: w::Witness (Chunk( A_st, A_sc ), Chunk( A_tt, A_tc )) -> Chunk( A_st, A_sc ) -> Chunk ( A_tt, A_tc );
convert': w::Witness (Chunk( A_st, A_sc ), Chunk( A_tt, A_tc )) -> Chunk'( A_st, A_sc ) -> Chunk'( A_tt, A_tc );
# A family of types and corresponding values representing natural numbers.
# (An encoding in Mythryl without using dependent types.)
package dim:
api {
# Internally, a value of type Dim0 (X, Z) is just a number.
# The trick here is to give each of these numbers a different unique
# type. X will be a decimal encoding of the number's value in
# "type digits". Z keeps track of whether the number is zero or not.
Dim0( X, Z );
# We can always get the internal number back...
to_int: Dim0( X, Z ) -> Int;
# These two types act as "flags". They will be substituted for Z
# and remember whether the value is zero or not.
Zero;
Nonzero;
Dim(X) = Dim0( X, Nonzero );
# These are the "type digits". Type "Dec" acts as a "terminator".
# We chose its name so to remind us that the encoding is decimal.
# If a nonzero value's decimal representation is "<Dn>...<D0>", then
# its type will be "Dim0 ( dg<D0> ... Dg<Dn> Dec, Nonzero) ", which
# is the same as "Dim Dg<D0> ... Dg<Dn> Dec". The type of the zero
# value is "Dim0( Dec, Zero )".
Dec;
Dg0(X) also Dg1(X) also Dg2(X) also Dg3(X) also Dg4(X);
Dg5(X) also Dg6(X) also Dg7(X) also Dg8(X) also Dg9(X);
# Here are the corresponding constructors for Dim0 (X, Z) values.
# The type for dg0 ensures that there will be no "leading zeros" in
# any encoding. This guarantees a 1-1 correspondence of constructable
# values and their types.
# To construct the value corresponding to a nonzero number whose
# decimal representation is "<Dn>...<D0>", one must invoke
# "dg<D0>' (... (dg<Dn>' dec')...)", i.e., the least significant
# digit appears leftmost.
dec' : Dim0( Dec, Zero );
dg0' : Dim(X) -> Dim( Dg0(X) );
dg1' : Dim0( X, Z ) -> Dim( Dg1(X) );
dg2' : Dim0( X, Z ) -> Dim( Dg2(X) );
dg3' : Dim0( X, Z ) -> Dim( Dg3(X) );
dg4' : Dim0( X, Z ) -> Dim( Dg4(X) );
dg5' : Dim0( X, Z ) -> Dim( Dg5(X) );
dg6' : Dim0( X, Z ) -> Dim( Dg6(X) );
dg7' : Dim0( X, Z ) -> Dim( Dg7(X) );
dg8' : Dim0( X, Z ) -> Dim( Dg8(X) );
dg9' : Dim0( X, Z ) -> Dim( Dg9(X) );
# Since having to reverse the sequence of digits seems unnatural,
# here is another set of constructors for dim values. These
# constructors use fate-passing style and themselves
# have more complicated types. But their use is easier:
# To construct the value corresponding to a nonzero number whose
# decimal representation is "<Dn>...<D0>", one must invoke
# "dec dg<Dn> ... dg<D0> dim"; i.e., the least significant
# digit appears rightmost -- just like in the usual decimal
# notation for numbers that we are all familiar with.
#
# Moreover, for any dim(X) value we have the neat property that
# it can be constructed by taking its type (expressed using "dim")
# and interpreting it as an expression. For example, the dim
# value representing 312 is "dec dg3 dg1 dg2 dim" and it can
# be constructed by evaluating "dec dg3 dg1 dg2 dim".
dec: (Dim0( Dec, Zero ) -> Y) -> Y;
dg0: Dim(X) -> (Dim( Dg0(X) ) -> Y) -> Y;
dg1: Dim0( X, Z ) -> (Dim( Dg1(X) ) -> Y) -> Y;
dg2: Dim0( X, Z ) -> (Dim( Dg2(X) ) -> Y) -> Y;
dg3: Dim0( X, Z ) -> (Dim( Dg3(X) ) -> Y) -> Y;
dg4: Dim0( X, Z ) -> (Dim( Dg4(X) ) -> Y) -> Y;
dg5: Dim0( X, Z ) -> (Dim( Dg5(X) ) -> Y) -> Y;
dg6: Dim0( X, Z ) -> (Dim( Dg6(X) ) -> Y) -> Y;
dg7: Dim0( X, Z ) -> (Dim( Dg7(X) ) -> Y) -> Y;
dg8: Dim0( X, Z ) -> (Dim( Dg8(X) ) -> Y) -> Y;
dg9: Dim0( X, Z ) -> (Dim( Dg9(X) ) -> Y) -> Y;
dim: Dim0( X, Z ) -> Dim0( X, Z );
};
# A sub-package for dealing with run-time type info (sizes only):
package s:
api {
# Our size info itself is statically typed!
# The size info for a value stored in chunk( T, C ) has
# the following type:
Size( T );
# Get a number out:
to_word: Size( T ) -> Unt;
# Sizes for simple things:
schar: Size( Schar );
uchar: Size( Uchar );
sint: Size( Sint );
uint: Size( Uint );
sshort: Size( Sshort );
ushort: Size( Ushort );
slong: Size( Slong );
ulong: Size( Ulong );
slonglong: Size( Slonglong );
ulonglong: Size( Ulonglong );
float: Size( Float );
double: Size( Double );
voidptr: Size( Voidptr );
ptr: Size( Ptr( O ) );
fptr: Size( Fptr( F ) );
an_enum: Size( An_Enum( A_tag ) );
};
# Sub-package for dealing with run-time type info:
package t:
api {
# Our RTTI itself is statically typed!
# The RTTI for a value stored in chunk( T, C ) has
# the following type:
Type( T );
# Get the RTTI from an actual chunk:
typeof: Chunk( T, C ) -> Type( T );
# Construct a new RTTI from existing RTTI:
pointer: Type( T ) -> Type( Ptr( Chunk( T, Rw ) ) );
target: Type( Ptr( Chunk( T, C ) ) ) -> Type( T );
arr: (Type( T ), dim::Dim( N )) -> Type( Arr( T, N ) );
element: Type( Arr( T, N ) ) -> Type( T );
ro: Type( Ptr( Chunk( T, C ) ) ) -> Type( Ptr( Chunk( T, Ro ) ) );
# Calculate the size of a chunk given its RTTI:
sizeof: Type( T ) -> s::Size( T );
# Dimension of rw_vector type
dim: Type( Arr( T, N ) ) -> dim::Dim( N );
# RTTI for simple things:
schar: Type( Schar );
uchar: Type( Uchar );
sint: Type( Sint );
uint: Type( Uint );
sshort: Type( Sshort );
ushort: Type( Ushort );
slong: Type( Slong );
ulong: Type( Ulong );
slonglong: Type( Slonglong );
ulonglong: Type( Ulonglong );
float: Type( Float );
double: Type( Double );
voidptr: Type( Voidptr );
an_enum: Type( An_Enum( A_tag ) );
};
# Convert from regular (heavy)
# to alternative (light) versions:
package light:
api {
chunk: Chunk( T, C ) -> Chunk'( T, C );
ptr: Ptr( O ) -> Ptr'( O );
fptr: Fptr( F ) -> Fptr'( F );
};
# And vice versa:
package heavy:
api {
chunk: t::Type( T ) -> Chunk'( T, C ) -> Chunk( T, C );
ptr: t::Type( Ptr( O ) ) -> Ptr'( O ) -> Ptr( O );
fptr: t::Type( Fptr( F ) ) -> Fptr'( F ) -> Fptr( F );
};
# Calculate size of an chunk
sizeof: Chunk( T, C ) -> s::Size( T );
# "fetch" methods for various types;
# fetching does not care about constness
package get:
api {
# Primitive types. The results are concrete here:
schar: Schar_Chunk( C ) -> mlrep::signed::Int;
uchar: Uchar_Chunk( C ) -> mlrep::unsigned::Unt;
sint: Sint_Chunk( C ) -> mlrep::signed::Int;
uint: Uint_Chunk( C ) -> mlrep::unsigned::Unt;
sshort: Sshort_Chunk( C ) -> mlrep::signed::Int;
ushort: Ushort_Chunk( C ) -> mlrep::unsigned::Unt;
slong: Slong_Chunk( C ) -> mlrep::signed::Int;
ulong: Ulong_Chunk( C ) -> mlrep::unsigned::Unt;
slonglong: Slonglong_Chunk( C ) -> mlrep::long_long_signed::Int;
ulonglong: Ulonglong_Chunk( C ) -> mlrep::long_long_unsigned::Unt;
float: Float_Chunk( C ) -> mlrep::float::Float;
double: Double_Chunk( C ) -> mlrep::float::Float;
an_enum: Enum_Chunk( E, C ) -> mlrep::signed::Int;
# Alt
schar' : Schar_Chunk'( C ) -> mlrep::signed::Int;
uchar' : Uchar_Chunk'( C ) -> mlrep::unsigned::Unt;
sint' : Sint_Chunk'( C ) -> mlrep::signed::Int;
uint' : Uint_Chunk'( C ) -> mlrep::unsigned::Unt;
sshort' : Sshort_Chunk'( C ) -> mlrep::signed::Int;
ushort' : Ushort_Chunk'( C ) -> mlrep::unsigned::Unt;
slong' : Slong_Chunk'( C ) -> mlrep::signed::Int;
ulong' : Ulong_Chunk'( C ) -> mlrep::unsigned::Unt;
slonglong' : Slonglong_Chunk'( C ) -> mlrep::long_long_signed::Int;
ulonglong' : Ulonglong_Chunk'( C ) -> mlrep::long_long_unsigned::Unt;
float' : Float_Chunk'( C ) -> mlrep::float::Float;
double' : Double_Chunk'( C ) -> mlrep::float::Float;
an_enum' : Enum_Chunk'( E, C ) -> mlrep::signed::Int;
# Fetching pointers. Results have to be abstract:
ptr: Chunk( Ptr( O ), C ) -> Ptr( O );
fptr: Fptr_Chunk( F, C ) -> Fptr( F );
voidptr: Voidptr_Chunk( C ) -> Voidptr;
# Alt
ptr' : Chunk'( Ptr( O ), C ) -> Ptr'( O );
fptr' : Fptr_Chunk'( F, C ) -> Fptr'( F );
voidptr' : Voidptr_Chunk'( C ) -> Voidptr;
# Bitfields. Concrete again:
sbf: Sbf( C ) -> mlrep::signed::Int;
ubf: Ubf( C ) -> mlrep::unsigned::Unt;
};
# "store" methods. These require rw chunks:
package set:
api {
# Primitive types. Use concrete values:
schar: (Schar_Chunk( Rw ), mlrep::signed::Int) -> Void;
uchar: (Uchar_Chunk( Rw ), mlrep::unsigned::Unt) -> Void;
sint: (Sint_Chunk( Rw ), mlrep::signed::Int) -> Void;
uint: (Uint_Chunk( Rw ), mlrep::unsigned::Unt) -> Void;
sshort: (Sshort_Chunk( Rw ), mlrep::signed::Int) -> Void;
ushort: (Ushort_Chunk( Rw ), mlrep::unsigned::Unt) -> Void;
slong: (Slong_Chunk( Rw ), mlrep::signed::Int) -> Void;
ulong: (Ulong_Chunk( Rw ), mlrep::unsigned::Unt) -> Void;
slonglong: (Slonglong_Chunk( Rw ), mlrep::long_long_signed::Int) -> Void;
ulonglong: (Ulonglong_Chunk( Rw ), mlrep::long_long_unsigned::Unt) -> Void;
float: (Float_Chunk( Rw ), mlrep::float::Float) -> Void;
double: (Double_Chunk( Rw ), mlrep::float::Float) -> Void;
an_enum: (Enum_Chunk( E, Rw ), mlrep::signed::Int) -> Void;
# Alternative lightweight versions (no implicit RTTI):
schar' : (Schar_Chunk'( Rw ), mlrep::signed::Int) -> Void;
uchar' : (Uchar_Chunk'( Rw ), mlrep::unsigned::Unt) -> Void;
sint' : (Sint_Chunk'( Rw ), mlrep::signed::Int) -> Void;
uint' : (Uint_Chunk'( Rw ), mlrep::unsigned::Unt) -> Void;
sshort' : (Sshort_Chunk'( Rw ), mlrep::signed::Int) -> Void;
ushort' : (Ushort_Chunk'( Rw ), mlrep::unsigned::Unt) -> Void;
slong' : (Slong_Chunk'( Rw ), mlrep::signed::Int) -> Void;
ulong' : (Ulong_Chunk'( Rw ), mlrep::unsigned::Unt) -> Void;
slonglong' : (Slonglong_Chunk'( Rw ), mlrep::long_long_signed::Int) -> Void;
ulonglong' : (Ulonglong_Chunk'( Rw ), mlrep::long_long_unsigned::Unt) -> Void;
float' : (Float_Chunk'( Rw ), mlrep::float::Float) -> Void;
double' : (Double_Chunk'( Rw ), mlrep::float::Float) -> Void;
an_enum' : (Enum_Chunk'( E, Rw ), mlrep::signed::Int) -> Void;
# Storing pointers. Abstract:
ptr: (Chunk( Ptr( O ), Rw ), Ptr( O )) -> Void;
fptr: (Fptr_Chunk( F, Rw ), Fptr( F )) -> Void;
voidptr: (Voidptr_Chunk( Rw ), Voidptr) -> Void;
# Alternative lightweight variants:
ptr' : (Chunk'( Ptr( O ), Rw ), Ptr'( O )) -> Void;
fptr' : (Fptr_Chunk'( F, Rw ), Fptr'( F )) -> Void;
voidptr' : (Voidptr_Chunk'( Rw ), Voidptr) -> Void;
# When storing, voidptr is compatible
# with any ptr type -- just as in C.
#
# This should eliminate most need for
# run-time type information in practice:
ptr_voidptr: (Chunk( Ptr( O ), Rw ), Voidptr) -> Void;
# Alt
ptr_voidptr' : (Chunk'( Ptr( O ), Rw ), Voidptr) -> Void;
# Bitfields; concrete
sbf: (Sbf( Rw ), mlrep::signed::Int) -> Void;
ubf: (Ubf( Rw ), mlrep::unsigned::Unt) -> Void;
};
# Copy contents of an arbitrary chunk:
copy: { from: Chunk( T, C ),
to: Chunk( T, Rw ) } -> Void;
# Alt
copy' : s::Size( T ) -> { from: Chunk'( T, C ),
to: Chunk'( T, Rw ) } -> Void;
# Manipulating chunk constness:
# rw -> ro: This direction just accounts for the fact that
# rw is conceptually a subtype of ro
# ro -> rw: This is not safe, but C makes it so easy that we
# might as well directly support it;
# Concretely, we make both operations typeagnostic in the argument
# constness. Moreover, the second (unsafe) direction is also
# typeagnostic in the result. This can be used to effectively
# implement a conversion to "whatever the context wants".
#
# Note: fun ro x = convert (w::ro w::trivial) x
# etc.
ro: Chunk( T, C ) -> Chunk( T, Ro );
rw: Chunk( T, A_sc ) -> Chunk( T, A_tc );
# Alt
ro' : Chunk'( T, C ) -> Chunk'( T, Ro );
rw' : Chunk'( T, A_sc ) -> Chunk'( T, A_tc );
# Operations on (mostly) pointers:
package ptr:
api {
# Going from chunk to pointer and vice versa, like C &val and *ptr:
enref: Chunk( T, C ) -> Ptr( Chunk( T, C ) );
deref: Ptr( Chunk( T, C ) ) -> Chunk( T, C );
# Alternate "lightweight" versions (no implicit run-time type info):
enref' : Chunk'( T, C ) -> Ptr'( Chunk ( T, C ) );
deref' : Ptr'( Chunk ( T, C ) ) -> Chunk'( T, C );
# Comparing pointers
compare: (Ptr( O ), Ptr( O )) -> Order;
# Alt
compare' : (Ptr'( O ), Ptr'( O )) -> Order;
# Going from pointer to void*; this also accounts for a conceptual
# subtyping relation and is safe
inject: Ptr( O ) -> Voidptr;
# Alt
inject' : Ptr'( O ) -> Voidptr;
# The opposite is not safe, but C makes it
# not only easy but also almost necessary.
#
# We use our RTTI interface to specify
# the pointer type (not the element type!)
cast: t::Type( Ptr( O ) ) -> Voidptr -> Ptr( O );
# Alt, needs explicit type constraint on result!
cast' : Voidptr -> Ptr'( O );
# NULL as void*
v_null: Voidptr;
# Projecting v_null to given pointer type:
null: t::Type( Ptr( O ) ) -> Ptr( O );
# The "light" NULL pointer is simply a typeagnostic constant
null' : Ptr'( O );
# fptr version of NULL
fnull: t::Type( Fptr( F ) ) -> Fptr( F );
# Again, "light" version is simply a typeagnostic constant
fnull' : Fptr'( F );
# Checking for NULL pointer
v_is_null: Voidptr -> Bool;
# Combining inject and v_is_null for convenience:
is_null: Ptr( O ) -> Bool;
# Alt
is_null' : Ptr'( O ) -> Bool;
# Checking a function pointer for NULL
is_fnull: Fptr( F ) -> Bool;
# Alt
is_fnull' : Fptr'( F ) -> Bool;
# pointer arithmetic
plus: (Ptr( Chunk( T, C ) ), Int) -> Ptr( Chunk( T, C ) );
diff: (Ptr( Chunk( T, C ) ), Ptr( Chunk( T, C ) )) -> Int;
# Alt; needs explicit size (for element)
plus' : s::Size( T ) -> (Ptr'( Chunk( T, C ) ), Int) -> Ptr'( Chunk( T, C ) );
diff' : s::Size( T ) -> (Ptr'( Chunk( T, C ) ), Ptr'( Chunk( T, C ) )) -> Int;
# Subscript through a pointer. This is unchecked:
sub: (Ptr( Chunk( T, C ) ), Int) -> Chunk( T, C );
# Alt; needs explicit size (for element)
sub' : s::Size( T ) -> (Ptr'( Chunk( T, C ) ), Int) -> Chunk'( T, C );
# Conversions that rely on witnesses
convert: w::Witness (Ptr( Chunk( A_st, A_sc ) ), Ptr( Chunk( A_tt, A_tc ) ))
->
Ptr( Chunk( A_st, A_sc ) )
->
Ptr( Chunk( A_tt, A_tc ) );
convert' : w::Witness (Ptr( Chunk( A_st, A_sc ) ), Ptr( Chunk( A_tt, A_tc ) ))
->
Ptr'( Chunk( A_st, A_sc ) )
->
Ptr'( Chunk( A_tt, A_tc ) );
# Constness manipulation for pointers.
# Note: fun ro x = convert (w::pointer (w::ro w::trivial)) x
# etc.
ro: Ptr ( Chunk( T, C ) ) -> Ptr ( Chunk( T, Ro ) );
rw: Ptr ( Chunk( T, A_sc ) ) -> Ptr ( Chunk( T, A_tc ) );
ro': Ptr'( Chunk( T, C ) ) -> Ptr'( Chunk( T, Ro ) );
rw': Ptr'( Chunk( T, A_sc ) ) -> Ptr'( Chunk( T, A_tc ) );
};
# Operations on (mostly) arrays
package arr:
api {
# Array subscript.
# Since we have RTTI, we can actually make this safe:
# We raise exceptions::INDEX_OUT_OF_BOUNDS for out-of-bounds access;
# for unchecked access, go through arr_decay and ptr_sub
sub: (Chunk( Arr( T, N ), C), Int) -> Chunk( T, C );
# Alt; needs element size and rw_vector dimension
sub' : (s::Size( T ), dim::Dim( N )) ->
(Chunk'( Arr( T, N ), C), Int) -> Chunk'( T, C );
# Let a rw_vector chunk decay, yielding pointer to first element:
decay: Chunk ( Arr( T, N ), C) -> Ptr ( Chunk( T, C ) );
decay': Chunk'( Arr( T, N ), C) -> Ptr'( Chunk( T, C ) );
# Reconstruct an rw_vector chunk from the pointer to its first element
reconstruct : (Ptr ( Chunk( T, C ) ), dim::Dim( N )) -> Chunk ( Arr( T, N ), C);
reconstruct': (Ptr'( Chunk( T, C ) ), dim::Dim( N )) -> Chunk'( Arr( T, N ), C);
# Dimension of rw_vector chunk
dim: Chunk( Arr( T, N ), C) -> dim::Dim( N );
};
# Allocating new chunks
new: t::Type( T ) -> Chunk( T, C );
# Alt
new' : s::Size( T ) -> Chunk'( T, C );
# freeing chunks that were allocated earlier
discard: Chunk( T, C ) -> Void;
# Alt
discard' : Chunk'( T, C ) -> Void;
# Allocating a dynamically-sized rw_vector
allot: t::Type( T ) -> Unt -> Ptr( Chunk( T, C ) );
# Alt
allot' : s::Size( T ) -> Unt -> Ptr'( Chunk( T, C ) );
# Freeing through pointers:
free: Ptr( O ) -> Void;
# Alt
free' : Ptr'( O ) -> Void;
# Perform a function call through a function-pointer:
call: (Fptr( X -> Y ), X) -> Y;
# Alt: Needs explicit type for the function pointer:
call' : t::Type( Fptr( X -> Y ) ) -> (Fptr'( X -> Y ), X) -> Y;
# Completely unsafe stuff, but common in C code:
package u:
api {
fcast: Fptr'(X) -> Fptr'(Y);
p2i: Ptr' ( O ) -> Ulong;
i2p: Ulong -> Ptr'( O );
};
};