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.


  • cast
  • castvwtp0
  • castvwtp1
  • cast2ptr
  • cast2Ptr0
  • cast2Ptr1
  • cast2int
  • cast2uint
  • cast2lint
  • cast2ulint
  • cast2llint
  • cast2ullint
  • cast2sint
  • cast2usint
  • cast2ssint
  • cast2ussint
  • list_vt2t
  • arrayptr2ref
  • strptr2string
  • ptr0_get
  • ptr1_get
  • ptr0_set
  • ptr1_set
  • ptr0_exch
  • ptr1_exch
  • ptr0_addby
  • ptr1_addby
  • ptr0_subby
  • ptr1_subby
  • ptr0_mulby
  • ptr1_mulby
  • ptr0_divby
  • ptr1_divby
  • ptr0_modby
  • ptr1_modby

  • cast

    Synopsis

    castfn
    cast{to:t0p}{from:t0p} (x: INV(from)):<> to

    Description

    This is the generic function for casting values of nonlinear types.

    castvwtp0

    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.

    castvwtp1

    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.

    cast2ptr

    Synopsis

    castfn cast2ptr {a:type} (x: INV(a)):<> ptr

    Description

    This function casts a boxed value to a pointer of unindexed type.

    cast2Ptr0

    Synopsis

    castfn cast2Ptr0 {a:type} (x: INV(a)):<> Ptr0

    Description

    This function casts a boxed value to a pointer of indexed type.

    cast2Ptr1

    Synopsis

    castfn cast2Ptr1 {a:type} (x: INV(a)):<> Ptr1

    Description

    This function casts a boxed value to a non-null pointer of indexed type.

    cast2int

    Synopsis

    castfn cast2int {a:t0p} (x: INV(a)):<> int

    Description

    This function casts a value to a signed integer of unindexed type.

    cast2uint

    Synopsis

    castfn cast2uint {a:t0p} (x: INV(a)):<> uint

    Description

    This function casts a value to an unsigned integer of unindexed type.

    cast2lint

    Synopsis

    castfn cast2lint {a:t0p} (x: INV(a)):<> lint

    Description

    This function casts a value to a signed long integer of unindexed type.

    cast2ulint

    Synopsis

    castfn cast2ulint {a:t0p} (x: INV(a)):<> ulint

    Description

    This function casts a value to an unsigned long integer of unindexed type.

    cast2llint

    Synopsis

    castfn cast2llint {a:t0p} (x: INV(a)):<> llint

    Description

    This function casts a value to a signed long long integer of unindexed type.

    cast2ullint

    Synopsis

    castfn cast2ullint {a:t0p} (x: INV(a)):<> ullint

    Description

    This function casts a value to an unsigned long long integer of unindexed type.

    cast2sint

    Synopsis

    castfn cast2sint {a:t0p} (x: INV(a)):<> sint

    Description

    This function casts a value to a signed short integer of unindexed type.

    cast2usint

    Synopsis

    castfn cast2usint {a:t0p} (x: INV(a)):<> usint

    Description

    This function casts a value to an unsigned short integer of unindexed type.

    cast2ssint

    Synopsis

    Synopsis for [cast2ssint] is unavailable.

    Description

    This function casts a value to a signed short short integer of unindexed type.

    cast2ussint

    Synopsis

    Synopsis for [cast2ussint] is unavailable.

    Description

    This function casts a value to an unsigned short short integer of unindexed type.

    list_vt2t

    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))
    // end of [list_vt_copy]
    

    arrayptr2ref

    Synopsis

    castfn arrayptr2ref
      {a:vt0p}{n:int} (x: !arrayptr (INV(a), n)):<> arrayref (a, n)

    strptr2string

    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).

    ptr0_get

    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.

    ptr1_get

    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.

    ptr0_set

    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.

    ptr1_set

    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.

    ptr0_exch

    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.

    ptr1_exch

    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.

    ptr0_addby

    Synopsis

    fun{a:t0p} ptr0_addby (p: ptr, x: a):<!wrt> void // !p += x

    Description

    This function is like ptr1_addby except it does not typecheck whether its first argument is non-null.

    ptr1_addby

    Synopsis

    fun{a:t0p} ptr1_addby (p: Ptr1, x: a):<!wrt> void // !p += x

    Description

    This function updates the content of p with the sum of its current content and x.

    ptr0_subby

    Synopsis

    fun{a:t0p} ptr0_subby (p: ptr, x: a):<!wrt> void // !p -= x

    Description

    This function is like ptr1_subby except it does not typecheck whether its first argument is non-null.

    ptr1_subby

    Synopsis

    fun{a:t0p} ptr1_subby (p: Ptr1, x: a):<!wrt> void // !p -= x

    Description

    This function updates the content of p with the difference of its current content from x.

    ptr0_mulby

    Synopsis

    fun{a:t0p} ptr0_mulby (p: ptr, x: a):<!wrt> void // !p *= x

    Description

    This function is like ptr1_mulby except it does not typecheck whether its first argument is non-null.

    ptr1_mulby

    Synopsis

    fun{a:t0p} ptr1_mulby (p: Ptr1, x: a):<!wrt> void // !p *= x

    Description

    This function updates the content of p with the product of multiplying its current content by x.

    ptr0_divby

    Synopsis

    fun{a:t0p} ptr0_divby (p: ptr, x: a):<!exnwrt> void // !p /= x

    Description

    This function is like ptr1_divby except it does not typecheck whether its first argument is non-null.

    ptr1_divby

    Synopsis

    fun{a:t0p} ptr1_divby (p: Ptr1, x: a):<!exnwrt> void // !p /= x

    Description

    This function updates the content of p with the quotient of dividing its current content by x.

    ptr0_modby

    Synopsis

    fun{a:t0p} ptr0_modby (p: ptr, x: a):<!exnwrt> void // !p %= x

    Description

    This function is like ptr1_modby except it does not typecheck whether its first argument is non-null.

    ptr1_modby

    Synopsis

    fun{a:t0p} ptr1_modby (p: Ptr1, x: a):<!exnwrt> void // !p %= x

    Description

    This function updates the content of p with the remainder of dividing its current content by x.
    This page is created with ATS by Hongwei Xi and also maintained by Hongwei Xi. SourceForge.net Logo