ATSLIB/prelude/unsafe
This package contains functions primarily needed for bypassing the type
system of ATS. These functions are often employed to implement templates in
ATS, which can be instantiated and then compiled into C-code. This style of
template implementation offers a safer and more reliable alternative to
macro-based template implementation in C.
Note that the file unsafe.sats is not loaded by default and must be done so
explicitly.
Synopsis
castfn
cast{to:t0p}{from:t0p} (x: INV(from)):<> to
Description
This is the generic function for casting values of nonlinear types.
Synopsis
castfn
castvwtp0
{to:vt0p}{from:vt0p} (x: INV(from)):<> to
Description
This is the generic function for casting values of linear types. Note that
it consumes the value being casted. The resource in the argument of this
function, if any, should be completely transferred into the result of the
cast so as to avoid resource-leaking.
Synopsis
castfn
castvwtp1
{to:vt0p}{from:vt0p} (x: !INV(from)>>from):<> to
Description
This is the generic function for casting values of linear types into values
of nonlinear types. Note that It preserves the value being casted.
Synopsis
castfn cast2ptr {a:type} (x: INV(a)):<> ptr
Description
This function casts a boxed value to a pointer of unindexed type.
Synopsis
castfn cast2Ptr0 {a:type} (x: INV(a)):<> Ptr0
Description
This function casts a boxed value to a pointer of indexed type.
Synopsis
castfn cast2Ptr1 {a:type} (x: INV(a)):<> Ptr1
Description
This function casts a boxed value to a non-null pointer of indexed type.
Synopsis
castfn cast2int {a:t0p} (x: INV(a)):<> int
Description
This function casts a value to a signed integer of unindexed type.
Synopsis
castfn cast2uint {a:t0p} (x: INV(a)):<> uint
Description
This function casts a value to an unsigned integer of unindexed type.
Synopsis
castfn cast2lint {a:t0p} (x: INV(a)):<> lint
Description
This function casts a value to a signed long integer of unindexed type.
Synopsis
castfn cast2ulint {a:t0p} (x: INV(a)):<> ulint
Description
This function casts a value to an unsigned long integer of unindexed type.
Synopsis
castfn cast2llint {a:t0p} (x: INV(a)):<> llint
Description
This function casts a value to a signed long long integer of unindexed type.
Synopsis
castfn cast2ullint {a:t0p} (x: INV(a)):<> ullint
Description
This function casts a value to an unsigned long long integer of unindexed type.
Synopsis
castfn cast2sint {a:t0p} (x: INV(a)):<> sint
Description
This function casts a value to a signed short integer of unindexed type.
Synopsis
castfn cast2usint {a:t0p} (x: INV(a)):<> usint
Description
This function casts a value to an unsigned short integer of unindexed type.
Synopsis
Synopsis for [cast2ssint] is unavailable.
Description
This function casts a value to a signed short short integer of unindexed type.
Synopsis
Synopsis for [cast2ussint] is unavailable.
Description
This function casts a value to an unsigned short short integer of unindexed type.
Synopsis
castfn list_vt2t
{a:t0p}{n:int} (xs: !list_vt(INV(a), n)):<> list(a, n)
Description
This function casts a linear list to a nonlinear list (only for temporary use).
Example
A typical use of this function occurs in a case where certain function
defined only on nonlinear lists needs to be applied to a linear list. For
instane, the following code demonstrates a simple way to copy a linear list
by calling the copy function for nonlinear lists:
staload UN = "prelude/SATS/unsafe.sats"
fun{a:t@ype}
list_vt_copy {n:int}
(xs: !list_vt (a, n)): list_vt (a, n) = list_copy ($UN.list_vt2t (xs))
Synopsis
castfn arrayptr2ref
{a:vt0p}{n:int} (x: !arrayptr (INV(a), n)):<> arrayref(a, n)
Synopsis
castfn strptr2string{l:agz}(x: !strptr(l)):<> String0
Description
This function casts a linear (non-null) string to a nonlinear string (only
for temporary use).
Synopsis
fun{a:vt0p} ptr0_get(p: ptr):<> (a)
Description
This function is like ptr1_get except it does not typecheck whether
its argument is non-null.
Synopsis
fun{a:vt0p} ptr1_get(p: Ptr1):<> (a)
Description
This function reads from a non-null pointer with no requirement for a proof
of at-view associated with the pointer. This is precisely like reading from
a pointer in C.
Synopsis
fun{a:vt0p} ptr0_set(p: ptr, x: INV(a)):<!wrt> void
Description
This function is like ptr1_set except it does not typecheck whether
its first argument is non-null.
Synopsis
fun{a:vt0p} ptr1_set(p: Ptr1, x: INV(a)):<!wrt> void
Description
This function writes through a non-null pointer with no requirement for a proof
of at-view associated with the pointer. This is precisely like writing through
a pointer in C.
Synopsis
fun{a:vt0p} ptr0_exch(p: ptr, x: &INV(a) >> a):<!wrt> void
Description
This function is like ptr1_exch except it does not typecheck whether
its first argument is non-null.
Synopsis
fun{a:vt0p} ptr1_exch(p: Ptr1, x: &INV(a) >> a):<!wrt> void
Description
This function exchanges the content at the location to which its first
argument points with the content in its second argument. Note that there
is no proof available that guarantees the first argument being a valid
pointer.
Synopsis
fun{a:t0p}
ptr0_addby(p: ptr, x: a):<!wrt> void
Description
This function is like ptr1_addby except it does not typecheck whether
its first argument is non-null.
Synopsis
fun{a:t0p}
ptr1_addby(p: Ptr1, x: a):<!wrt> void
Description
This function updates the content of p with the sum of its current content
and x.
Synopsis
fun{a:t0p}
ptr0_subby(p: ptr, x: a):<!wrt> void
Description
This function is like ptr1_subby except it does not typecheck whether
its first argument is non-null.
Synopsis
fun{a:t0p}
ptr1_subby(p: Ptr1, x: a):<!wrt> void
Description
This function updates the content of p with the difference of its current
content from x.
Synopsis
fun{a:t0p}
ptr0_mulby(p: ptr, x: a):<!wrt> void
Description
This function is like ptr1_mulby except it does not typecheck whether
its first argument is non-null.
Synopsis
fun{a:t0p}
ptr1_mulby(p: Ptr1, x: a):<!wrt> void
Description
This function updates the content of p with the product of multiplying its
current content by x.
Synopsis
fun{a:t0p}
ptr0_divby(p: ptr, x: a):<!exnwrt> void
Description
This function is like ptr1_divby except it does not typecheck whether
its first argument is non-null.
Synopsis
fun{a:t0p}
ptr1_divby(p: Ptr1, x: a):<!exnwrt> void
Description
This function updates the content of p with the quotient of dividing its
current content by x.
Synopsis
fun{a:t0p}
ptr0_modby(p: ptr, x: a):<!exnwrt> void
Description
This function is like ptr1_modby except it does not typecheck whether
its first argument is non-null.
Synopsis
fun{a:t0p}
ptr1_modby(p: Ptr1, x: a):<!exnwrt> void
Description
This function updates the content of p with the remainder of dividing its
current content by x.