ats-reference.txt

ATS Reference
=============
Chris Double <chris.double@double.co.nz>
27 June 2012

Overloaded Functions
--------------------

The ATS prelude provides some functions that are overloaded with
implementations for different types. These can be used instead of the explicit
typed functions in many cases to make code easier to understand and more
generic.

print
~~~~~

Definition
^^^^^^^^^^
----
fun print (p):<!ref> void
----

Description
^^^^^^^^^^
Prints some representation of 'p' to standard output.

prerr
~~~~~

Definition
^^^^^^^^^^
----
fun prerr (p):<!ref> void
----

Description
^^^^^^^^^^^
Prints some representation of 'p' to standard error.

Math operators
~~~~~~~~~~~~~~

Definition
^^^^^^^^^^
----
fun - (a, b):<> c
fun + (a, b):<> c
----

Description
^^^^^^^^^^^
Standard mathematical operators overloaded for different types (pointers,
numbers, etc).

Comparison operators
~~~~~~~~~~~~~~~~~~~~

Definition
^^^^^^^^^^
----
fun < (a, b):<> bool
fun <= (a, b):<> bool
fun > (a, b):<> bool
fun >= (a, b):<> bool
fun = (a, b):<> bool
fun <> (a, b):<> bool
fun != (a, b):<> bool
----

Description
^^^^^^^^^^^
Standard comparison operators overloaded for different types (pointers,
numbers, etc).

Pointer operators
~~~~~~~~~~~~~~~~~

Definition
^^^^^^^^^^
----
fun ~ {l:addr} (p: ptr l):<> bool (l > null)
----

Description
^^^^^^^^^^^
Overloaded for the pointer types to return 'true' if the pointer is not null.

succ
~~~~

Definition
^^^^^^^^^^
----
fun succ (a):<> b
----

Description
^^^^^^^^^^^
Returns the successor of a given value. For numbers and pointers this is the
value + 1.

pred
~~~~

Definition
^^^^^^^^^^
----
fun predc (a):<> b
----

Description
^^^^^^^^^^^
Returns the predecessor of a given value. For numbers and pointers this is the
value - 1.

padd
~~~~

Definition
^^^^^^^^^^
----
fun padd {l:addr} {i:int} (p, i) :<> p
----

Description
^^^^^^^^^^^
Adds 'i' to pointer 'p'.

psub
~~~~

Definition
^^^^^^^^^^
----
fun psub {l:addr} {i:int} (p, i) :<> p
----

Description
^^^^^^^^^^^
Subtracts 'i' from pointer 'p'.

compare
~~~~~~~

Definition
^^^^^^^^^^
----
fun compare (a, b):<> Sgn 
----

Description
^^^^^^^^^^^
Returns a negative number if 'a' is less than 'b', a positive number if 'a' is
greater than 'b' and zero if 'a' equals 'b'.

tostring
~~~~~~~~

Definition
^^^^^^^^^^
----
fun tostring (x):<> strptr1
----

Description
^^^^^^^^^^^
Returns a string representation of value 'x'.

Linear Lists
------------

list_vt is a polymorphic linear datatype for dealing with linked lists. 
list_vt.sats contains the definition for datatypes and funtions that operate on
linear lists. Use of these routines does not require the garbage collector.

The list_vt datatype has two constructors. list_vt_nil and list_vt_cons.
The former represents an empty list and the latter a pair of a viewtype and an
existing list.

Constructors
~~~~~~~~~~~~

----
dataviewtype list_vt (a:viewt@ype+, int) =
  | {n:int | n >= 0}
    list_vt_cons (a, n+1) of (a, list_vte (a, n))
  | list_vt_nil (a, 0)
----

The list_vt type is indexed by the type of the item contained in the list and
an integer representing the length of the list. A slightly simpler typedef is
provided that represents a list of any length:

----
viewtypedef List_vt (a:viewt@ype) = [n:int | n >=0] list_vt (a, n)
----

list_vt_length_is_nonnegative
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Definition
^^^^^^^^^^
----
prfun list_vt_length_is_nonnegative
  {a:vt0p} {n:int} (xs: !list_vt (a, n)): [n>=0] void
----

Description
^^^^^^^^^^^
Proof function that asserts that the linear list has a non-negative length.


list_vt_sing
~~~~~~~~~~~~

Definition
^^^^^^^^^^
----
macdef list_vt_sing (x) =
  list_vt_cons (,(x), list_vt_nil ())
----

Description
^^^^^^^^^^^
Creates a 'list_vt' containing single element

Example
^^^^^^^
----
implement main() = {
  val a = list_vt_sing (42)
  val+ ~list_vt_cons (b, ~list_vt_nil ()) = a
  val () = print_int (b)
}
----

list_vt_pair
~~~~~~~~~~~~

Definition
^^^^^^^^^^
----
macdef list_vt_pair (x1, x2) =
  list_vt_cons (,(x1), list_vt_cons (,(x2), list_vt_nil))
----

Description
^^^^^^^^^^^
Creates a 'list_vt' containing two elements

Example
^^^^^^^
----
implement main() = {
  val a = list_vt_pair ("a", "b")
  val+ ~list_vt_cons (b, c) = a
  val+ ~list_vt_cons (d, ~list_vt_nil ()) = c
  val () = print_string (b)
  val () = print_newline ()
  val () = print_string (d)
}
----

list_vt_is_nil
~~~~~~~~~~~~~~

Definition
^^^^^^^^^^
----
fun{} list_vt_is_nil
  {a:vt0p} {n:int} (xs: !list_vt (a, n)):<> bool (n==0)
----

Description
^^^^^^^^^^^
Returns 'true' if the given list is empty.

Example
^^^^^^^
----
staload _ = "prelude/DATS/list_vt.dats"

implement main() = {
  val a = list_vt_sing (42)
  val+ ~list_vt_cons (b, c) = a
  val () = assertloc (list_vt_is_nil (c))
  val+ ~list_vt_nil () = c
  val () = print_int (b)
}
----

list_vt_is_cons
~~~~~~~~~~~~~~~

Definition
^^^^^^^^^^
----
fun{} list_vt_is_cons
  {a:vt0p} {n:int} (xs: !list_vt (a, n)):<> bool (n > 0)
----

Description
^^^^^^^^^^^
Returns 'true' if the given list is not empty.

Example
^^^^^^^
----
staload _ = "prelude/DATS/list_vt.dats"

implement main() = {
  val a = list_vt_sing (42)
  val () = assertloc (list_vt_is_cons (a))
  val+ ~list_vt_cons (b, c) = a
  val+ ~list_vt_nil () = c
  val () = print_int (b)
}
----

list_vt_make_array
~~~~~~~~~~~~~~~~~~

Definition
^^^^^^^^^^
----
fun{a:vt0p}
list_vt_make_array {n:int}
  (A: &(@[a][n]) >> @[a?!][n], n: size_t n):<> list_vt (a, n)
----

Description
^^^^^^^^^^^
Given a reference to an array, return a linear list of the items in that
array. 

Example
^^^^^^^
----
staload _ = "prelude/DATS/list_vt.dats"

implement main() = {
  var !arr = @[string] ("a", "b")
  val a = list_vt_make_array (!arr, 2)
  val+ ~list_vt_cons (b, c) = a
  val+ ~list_vt_cons (d, ~list_vt_nil ()) = c
  val () = print_string (b)
  val () = print_newline ()
  val () = print_string (d)
}
----

list_vt_of_arraysize
~~~~~~~~~~~~~~~~~~~~

Definition
^^^^^^^^^^
----
fun{a:vt0p}
list_vt_of_arraysize
  {n:int} (arrsz: arraysize (a, n)):<> list_vt (a, n)
----

Description
^^^^^^^^^^^
Given an arraysize, destructively convert it into a linear list.

Example
^^^^^^^
----
staload _ = "prelude/DATS/list_vt.dats"

implement main() = {
  val a = list_vt_of_arraysize<int> $arrsz(41, 42)
  val+ ~list_vt_cons (b, c) = a
  val+ ~list_vt_cons (d, ~list_vt_nil ()) = c
  val () = print_int (b)
  val () = print_newline ()
  val () = print_int (d)
}
----

list_vt_copy
~~~~~~~~~~~~

Definition
^^^^^^^^^^
----
fun{a:t0p}
list_vt_copy {n:int} (xs: !list_vt (a, n)):<> list_vt (a, n)
----

Description
^^^^^^^^^^^
Copy an existing linear list. Note that the items held in the list must be
non-linear. The implementation of this template function requires
'prelude/DATS/list.dats' to be loaded.

Example
^^^^^^^
----
staload _ = "prelude/DATS/list_vt.dats"
staload _ = "prelude/DATS/list.dats"

implement main() = {
  val a = list_vt_sing 42
  val b = list_vt_copy (a)
  val+ ~list_vt_cons (c, ~list_vt_nil ()) = a
  val+ ~list_vt_cons (d, ~list_vt_nil ()) = b
  val () = print_int (c)
  val () = print_newline ()
  val () = print_int (d)
}
----

list_vt_free
~~~~~~~~~~~~

Definition
^^^^^^^^^^
----
fun{a:t0p}
list_vt_free (xs: List_vt a):<> void
----

Description
^^^^^^^^^^^
Frees the linear list, destroying it. The items in the list must be
non-linear. See 'list_vt_free_fun' for freeing a linear list containing linear
resources.

Example
^^^^^^^
----
staload _ = "prelude/DATS/list_vt.dats"

implement main() = {
  val a = list_vt_of_arraysize<int> $arrsz(41, 42)
  val () = list_vt_free (a)
}
----

list_vt_free_fun
~~~~~~~~~~~~~~~~

Definition
^^^^^^^^^^
----
fun{a:vt0p}
list_vt_free_fun (
  xs: List_vt a, f: (&a >> a?) -<fun> void
) :<> void 
----

Description
^^^^^^^^^^^
Frees the linear list, taking a function that will free the items held by the
list.

Example
^^^^^^^
----
staload _ = "prelude/DATS/list_vt.dats"

dataviewtype foo = foo

fn foo_free (f: &foo >> foo?):<> void =
  case+ f of
  | ~foo () => ()

implement main() = {
  val a = list_vt_cons (foo, list_vt_nil ())
  val () = list_vt_free_fun (a, foo_free)
}
----

list_vt_length
~~~~~~~~~~~~~~

Definition
^^^^^^^^^^
----
fun{a:vt0p}
list_vt_length {n:int} (xs: !list_vt (a, n)):<> int n
----

Description
^^^^^^^^^^^
Returns the length of the linear list.

Example
^^^^^^^
----
staload _ = "prelude/DATS/list_vt.dats"

implement main() = {
  val a = list_vt_of_arraysize<int> $arrsz(41, 42)
  val len = list_vt_length (a)
  val () = printf("Length: %d\n", @(len))
  val () = list_vt_free (a)
}
----

list_vt_make_elt
~~~~~~~~~~~~~~~~

Definition
^^^^^^^^^^
----
fun{a:t0p}
list_vt_make_elt {n:nat} (x: a, n: int n):<> list_vt (a, n)
----

Description
^^^^^^^^^^^
Return a linear list composed of length 'n' containing 'n' copies of 'x'. The
element type must be non-linear.

Example
^^^^^^^
----
staload _ ="prelude/DATS/list_vt.dats"

implement main() = {
  val a = list_vt_make_elt (42, 5)
  val () = printf("List is length: %d\n", @(list_vt_length (a)))
  val () = list_vt_free (a)
}
----

list_vt_append
~~~~~~~~~~~~~~

Definition
^^^^^^^^^^
----
fun{a:vt0p}
list_vt_append {m,n:int}
  (xs: list_vt (a, m), ys: list_vt (a, n)):<> list_vt (a, m+n)
----

Description
^^^^^^^^^^^
Returns a linear list containing the elements from 'xs' followed by the
elements in 'ys'. Both 'xs' and 'ys' are destroyed.

Example
^^^^^^^
----
staload _ = "prelude/DATS/list_vt.dats"

implement main() = {
  val a = list_vt_of_arraysize<int> $arrsz(41, 42)
  val b = list_vt_of_arraysize<int> $arrsz(43, 44)
  val c = list_vt_append (a, b)
  val () = printf("Length of c = %d\n", @(list_vt_length (c)))
  val () = list_vt_free (c)
}
----

list_vt_split_at
~~~~~~~~~~~~~~~~

Definition
^^^^^^^^^^
----
fun{a:vt0p}
list_vt_split_at {n:int} {i:nat | i <= n}
  (xs: &list_vt (a, n) >> list_vt (a, n-i), i: int i):<> list_vt (a, i)
----

Description
^^^^^^^^^^^
Given a reference to a linear list, and in index into that list 'i', return a
list containing the first 'i' items and modifies the original list to have the
remaining items.

Example
^^^^^^^
----
staload _ = "prelude/DATS/list_vt.dats"

implement main() = {
  var a = list_vt_of_arraysize<int> $arrsz(41, 42, 43, 44)
  val b = list_vt_split_at (a, 3)

  fun loop {n:nat} (lst: !list_vt (int, n)): void =
    case+ lst of
    | list_vt_nil () => (fold@ lst; print_newline ())
    | list_vt_cons (i, !rest) => (print_int (i);
                                  loop (!rest);
				  fold@ lst)

  val () = (print_string ("a:"); print_newline (); loop (a))
  val () = (print_string ("b:"); print_newline (); loop (b))

  val () = list_vt_free (a)
  val () = list_vt_free (b)
}
----

list_vt_reverse
~~~~~~~~~~~~~~~

Definition
^^^^^^^^^^
----
fun{a:vt0p}
list_vt_reverse {n:int} (xs: list_vt (a, n)):<> list_vt (a, n)
----

Description
^^^^^^^^^^^
Given a linear list, reverses the order of elements and returns the resulting
list. The original list is destroyed.

Example
^^^^^^^
----
staload _ = "prelude/DATS/list_vt.dats"

implement main() = {
  var a = list_vt_of_arraysize<int> $arrsz(41, 42, 43, 44)
  val b = list_vt_reverse (a)

  val () = loop (b) where {
             fun loop {n:nat} (lst: !list_vt (int, n)): void =
               case+ lst of
               | list_vt_nil () => (fold@ lst; print_newline ())
               | list_vt_cons (i, !rest) => (print_int (i);
	                                     loop (!rest);
					     fold@ lst)
	   }

  val () = list_vt_free (b)
}
----

list_vt_reverse_append
~~~~~~~~~~~~~~~~~~~~~~

Definition
^^^^^^^^^^
----
fun{a:vt0p}
list_vt_reverse_append {m,n:int}
  (xs: list_vt (a, m), ys: list_vt (a, n)):<> list_vt (a, m+n)
----

Description
^^^^^^^^^^^
Reverses the list 'xs' then appends 'ys' to the resulting list and returns it.

Example
^^^^^^^
----
staload _ = "prelude/DATS/list_vt.dats"

implement main() = {
  var a = list_vt_of_arraysize<int> $arrsz(41, 42, 43, 44)
  var b = list_vt_of_arraysize<int> $arrsz(45, 46, 47, 48)

  val c = list_vt_reverse_append (a, b)

  val () = loop (c) where {
             fun loop {n:nat} (lst: !list_vt (int, n)): void =
               case+ lst of
               | list_vt_nil () => (fold@ lst; print_newline ())
               | list_vt_cons (i, !rest) => (printf("%d ", @(i));
	                                     loop (!rest);
					     fold@ lst)
	   }

  val () = list_vt_free (c)
}
----

list_vt_concat
~~~~~~~~~~~~~~

Definition
^^^^^^^^^^
----
fun{a:vt0p}
list_vt_concat (xss: List_vt (List_vt (a))):<> List_vt (a)
----

Description
^^^^^^^^^^^
Concatenates a list of lists into a single list.

Example
^^^^^^^
----
staload _ = "prelude/DATS/list_vt.dats"

implement main() = {
  var a = list_vt_of_arraysize<int> $arrsz(1, 2, 3, 4)
  var b = list_vt_of_arraysize<int> $arrsz(5, 6, 7, 8)
  var c = list_vt_of_arraysize<int> $arrsz(9, 10)
  var d = list_vt_cons (a, list_vt_pair (b, c))

  val e = list_vt_concat (d)

  val () = loop (e) where {
             fun loop {n:nat} (lst: !list_vt (int, n)): void =
               case+ lst of
               | list_vt_nil () => (fold@ lst; print_newline ())
               | list_vt_cons (i, !rest) => (printf("%d ", @(i));
	                                     loop (!rest);
					     fold@ lst)
	   }

  val () = list_vt_free (e)
}
----

list_vt_tabulate
~~~~~~~~~~~~~~~~

Definition
^^^^^^^^^^
----
fun{a:vt0p}
list_vt_tabulate_funenv
  {v:view} {vt:viewtype} {n:nat} {f:eff}
  (pf: !v | f: (!v | natLt n, !vt) -<f> a, n: int n, env: !vt)
  :<f> list_vt (a, n)

fun{a:vt0p}
list_vt_tabulate_fun {n:nat} {f:eff}
  (f: natLt n -<f> a, n: int n):<f> list_vt (a, n)

fun{a:vt0p}
list_vt_tabulate_vclo {v:view} {n:nat} {f:eff}
  (pf: !v | f: &(!v | natLt n) -<clo,f> a, n: int n):<f> list_vt (a, n)

fun{a:vt0p}
list_vt_tabulate_cloptr {n:nat} {f:eff}
  (f: !(natLt n) -<cloptr,f> a, n: int n):<f> list_vt (a, n)

fun{a:vt0p}
list_vt_tabulate_vcloptr {v:view} {n:nat} {f:eff}
  (pf: !v | f: !(!v | natLt n) -<cloptr,f> a, n: int n):<f> list_vt (a, n)
----

Description
^^^^^^^^^^^
'list_vt_tabulate' is a family of functions that are used to generate a linear
list given a function. The function is called 'n' times, with 'n' given as an
argument. The result of the function is used as the element of the nth
position of the generated list.

There is a variant of 'list_vt_tabulate' for the different function types
available in ATS:

|=========================================================================
| list_vt_tabulate_funenv  | General purpose version for any function type
| list_vt_tabulate_fun     | C type functions (<fun>)
| list_vt_tabulate_vclo    | Stack allocated closures (<clo>)
| list_vt_tabulate_cloptr  | Linear closures (<cloptr>)
| list_vt_tabulate_vcloptr | Linear closures with a proof argument
|=========================================================================

Example
^^^^^^^
----
staload _ = "prelude/DATS/list_vt.dats"

implement main() = {
  val a = list_vt_tabulate_fun<int> (lam (n) =<> n * 2, 4)
  
  val () = loop (a) where {
             fun loop {n:nat} (lst: list_vt (int, n)): void =
               case+ lst of
               | ~list_vt_nil () => print_newline ()
               | ~list_vt_cons (i, rest) => (printf("%d ", @(i));
	                                     loop (rest))
	   }

}
----

list_vt_foreach
~~~~~~~~~~~~~~~

Definition
^^^^^^^^^^
----
fun{a:vt0p}
list_vt_foreach_funenv
  {v:view} {vt:viewtype} {n:int} {f:eff}
  (pf: !v | xs: !list_vt (a, n), f: !(!v | &a, !vt) -<f> void, env: !vt)
  :<f> void

fun{a:vt0p}
list_vt_foreach_fun {n:int} {f:eff}
  (xs: !list_vt (a, n), f: (&a) -<fun,f> void):<f> void

fun{a:vt0p}
list_vt_foreach_vclo {v:view} {n:int} {f:eff}
  (pf: !v | xs: !list_vt (a, n), f: &(!v | &a) -<clo,f> void):<f> void

fun{a:t0p}
list_vt_foreach_cloptr {n:int} {f:eff}
  (xs: !list_vt (a, n), f: !(&a) -<cloptr,f> void):<f> void

fun{a:t0p}
list_vt_foreach_vcloptr {v:view} {n:int} {f:eff}
  (pf: !v | xs: !list_vt (a, n), f: !(!v | &a) -<cloptr,f> void):<f> void
----

Description
^^^^^^^^^^^
'list_vt_foreach' is a family of functions that are used to iterate over a
list, calling a function for each element in the list. The function receives
a reference to the list element as an argument.

There is a variant of 'list_vt_foreach' for the different function types
available in ATS:

|========================================================================
| list_vt_foreach_funenv  | General purpose version for any function type
| list_vt_foreach_fun     | C type functions (<fun>)
| list_vt_foreach_vclo    | Stack allocated closures (<clo>)
| list_vt_foreach_cloptr  | Linear closures (<cloptr>)
| list_vt_foreach_vcloptr | Linear closures with a proof argument
|========================================================================

Note that the 'cloptr' and 'vcloptr' variants work on lists containing types,
not viewtypes like the other variants.

Example
^^^^^^^
----
staload _ = "prelude/DATS/list_vt.dats"

implement main() = {
  val a = list_vt_tabulate_fun<int> (lam (n) =<> n * 2, 4)
  val () = list_vt_foreach_fun<int> (a, lam (x) =<>
                                         $effmask_all (printf("%d ", @(x))))
  val () = list_vt_free (a)
}
----

list_vt_iforeach
~~~~~~~~~~~~~~~~

Definition
^^^^^^^^^^
----
fun{a:vt0p}
list_vt_iforeach_funenv
  {v:view} {vt:viewtype} {n:int} {f:eff} (
  pf: !v
| xs: !list_vt (a, n), f: (!v | natLt n, &a, !vt) -<fun,f> void, env: !vt
) :<f> void

fun{a:vt0p}
list_vt_iforeach_fun {n:int} {f:eff}
  (xs: !list_vt (a, n), f: (natLt n, &a) -<fun,f> void):<f> void

fun{a:vt0p}
list_vt_iforeach_vclo {v:view} {n:int} {f:eff}
  (pf: !v | xs: !list_vt (a, n), f: &(!v | natLt n, &a) -<clo,f> void):<f> void

fun{a:t0p}
list_vt_iforeach_cloptr {n:int} {f:eff}
  (xs: !list_vt (a, n), f: !(natLt n, &a) -<cloptr,f> void):<f> void

fun{a:t0p}
list_vt_iforeach_vcloptr {v:view} {n:int} {f:eff}
  (pf: !v | xs: !list_vt (a, n), f: !(!v | natLt n, &a) -<cloptr,f> void):<f> void
----

Description
^^^^^^^^^^^
'list_vt_iforeach' is a family of functions that are used to iterate over a
list, calling a function for each element in the list. The function receives
as arguments the index of the element in the list and a reference to the list
element.

There is a variant of 'list_vt_iforeach' for the different function types
available in ATS:

|=========================================================================
| list_vt_iforeach_funenv  | General purpose version for any function type
| list_vt_iforeach_fun     | C type functions (<fun>)
| list_vt_iforeach_vclo    | Stack allocated closures (<clo>)
| list_vt_iforeach_cloptr  | Linear closures (<cloptr>)
| list_vt_iforeach_vcloptr | Linear closures with a proof argument
|=========================================================================

Note that the 'cloptr' and 'vcloptr' variants work on lists containing types,
not viewtypes like the other variants.

Example
^^^^^^^
----
staload "prelude/SATS/list_vt.sats"
staload "prelude/DATS/list_vt.dats"

implement main() = {
  val a = list_vt_tabulate_fun<int> (lam (n) =<> n * 2, 4)
  val () = list_vt_iforeach_fun<int> (a, lam (i, x) =<>
                                          $effmask_all
					   (printf("%d: %d\n", @(i, x))))
  val () = list_vt_free (a)
}
----

list_vt_mergesort
~~~~~~~~~~~~~~~~~

Definition
^^^^^^^^^^
----
fun{a:vt0p}
list_vt_mergesort {n:int}
  (xs: list_vt (a, n), cmp: &(&a, &a) -<clo> int):<> list_vt (a, n)
----

Description
^^^^^^^^^^^
Sorts the list using the merge sort algorithm. Requires a function to provide
an ordering for elements in the list. 

The comparison function should be stack allocated (has tag <clo>) and requires
its arguments to be references. This means you can't use the prelude 'compare'
function directly. It should return:

|==================================================================
| negative integer | first argument less than second argument 
| 0                | first argument equals second argument
| positive integer | first argument is greater than second argument
|==================================================================

Example
^^^^^^^
----
staload _ = "prelude/DATS/list_vt.dats"

implement main() = {
  val a = list_vt_of_arraysize<int> $arrsz (10, 2, 6, 4, 8)
  val () = printf("Unsorted:\n", @())
  val () = list_vt_iforeach_fun<int> (a, lam (i, x) =<>
                                          $effmask_all
					   (printf("%d: %d\n", @(i, x))))
					   
  val () = printf("Sorted:\n", @())
  var !p_cmp = @lam (a: &int, b: &int): int =<> compare (a, b)
  val b = list_vt_mergesort (a, !p_cmp)
  val () = list_vt_iforeach_fun<int> (b, lam (i, x) =<>
                                          $effmask_all
					   (printf("%d: %d\n", @(i, x))))
  val () = list_vt_free (b)
----

list_vt_quicksort
~~~~~~~~~~~~~~~~~

Definition
^^^^^^^^^^
----
fun{a:vt0p}
list_vt_quicksort {n:int} (xs: !list_vt (a, n), cmp: (&a, &a) -<fun> int):<> void
----

Description
^^^^^^^^^^^
Sorts a list using the quicksort algorithm. Unlike 'list_vt_mergesort' this
modifies the original list rather than returning the result. 

The comparison function should be a standard C function (has tag <fun>) and requires
its arguments to be references. This means you can't use the prelude 'compare'
function directly. It should return:

|==================================================================
| negative integer | first argument less than second argument 
| 0                | first argument equals second argument
| positive integer | first argument is greater than second argument
|==================================================================

The current 'list_vt_quicksort' implementation copies the list into an array
and uses the standard C library 'qsort' function to sort it. It then copies
the data back into the list. Due to the implementation details the following
additional files must be loaded to use 'list_vt_qucksort':

* 'prelude/DATS/array.dats'
* 'libc/SATS/stdlib.sats'

Example
^^^^^^^
----
staload _ = "libc/SATS/stdlib.sats"
staload _ = "prelude/DATS/list_vt.dats"
staload _ = "prelude/DATS/array.dats"

implement main() = {
  val a = list_vt_of_arraysize<int> $arrsz (10, 2, 6, 4, 8)
  val () = printf("Unsorted:\n", @())
  val () = list_vt_iforeach_fun<int> (a, lam (i, x) =<>
                                          $effmask_all
					   (printf("%d: %d\n", @(i, x))))
					   
  val () = printf("Sorted:\n", @())
  fn cmp (a: &int, b: &int):<> int = compare (a, b)
  val () = list_vt_quicksort (a, cmp)
  val () = list_vt_iforeach_fun<int> (a, lam (i, x) =<>
                                          $effmask_all
					   (printf("%d: %d\n", @(i, x))))
  val () = list_vt_free (a)
}
----

Pointers
--------

The prelude file 'prelude/SATS/pointer.sats' provides functions for
manipulating pointers. This includes printing, comparison, pointer arithmetic
and getting/setting values stored at the pointer location.

ptr_is_gtez
~~~~~~~~~~~

Definition
^^^^^^^^^^
----
praxi ptr_is_gtez
  {l:addr} (p: ptr l):<> [l >= null] void
----

Description
^^^^^^^^^^^
Proof function asserting that a pointer cannot have a negative address.

ptr_is_null 
~~~~~~~~~~~

Definition
^^^^^^^^^^
----
fun ptr_is_null (p: ptr):<> bool
----

Description
^^^^^^^^^^^
Given a pointer, return 'true' if the pointer is NULL.

Example
^^^^^^^
----
implement main() = {
  val a = null
  val () = assertloc (ptr_is_null (a))
}
----

ptr_isnot_null 
~~~~~~~~~~~~~~

Definition
^^^^^^^^^^
----
fun ptr_isnot_null (p: ptr):<> bool
----

Description
^^^^^^^^^^^
Given a pointer, return 'true' if the pointer is not NULL.

Example
^^^^^^^
----
implement main() = {
  val a = null + 1
  val () = assertloc (ptr_isnot_null (a))
}
----

add_ptr
~~~~~~~

Definition
^^^^^^^^^^
----
fun add_ptr_int
  (p: ptr, i: int):<> ptr
overload + with add_ptr_int

fun add_ptr_size
  (p: ptr, sz: size_t):<> ptr
overload + with add_ptr_size
----

Description
^^^^^^^^^^^

'add_ptr' is a family of functions for performing pointer arithmetic on the
pointer address. The two variants, suffixed by 'int' and 'size', allow adding
an 'int' or a 'size_t' respectively. The standard '+' mathematical operator is
overloaded for these functions so pointer arithmetic can be done with normal
math operators.

Example
^^^^^^^
----
implement main() = {
  val a = null
  val () = print (a)
  val () = print_newline ()
  val b = a + 4
  val () = print (b)
  val () = print_newline ()
  val c = add_ptr_int (b, 4)
  val () = print (c)
  val () = print_newline ()
}
----

sub_ptr
~~~~~~~

Definition
^^^^^^^^^^
----
fun sub_ptr_int
  (p: ptr, i: int):<> ptr
overload - with sub_ptr_int

fun sub_ptr_size
  (p: ptr, sz: size_t):<> ptr
overload - with sub_ptr_size
----

Description
^^^^^^^^^^^
'sub_ptr' is a family of functions for performing pointer arithmetic on the
pointer address. The two variants, suffixed by 'int' and 'size', allow
subtracting an 'int' or a 'size_t' respectively. The standard '-' mathematical
operator is overloaded for these functions so pointer arithmetic can be done
with normal math operators.

Example
^^^^^^^
----
implement main() = {
  val a = null + 8
  val () = print (a)
  val () = print_newline ()
  val b = a - 4
  val () = print (b)
  val () = print_newline ()
  val c = sub_ptr_int (b, 4)
  val () = print (c)
  val () = print_newline ()
}
----

Pointer Comparison
~~~~~~~~~~~~~~~~~~

Definition
^^^^^^^^^^
----
fun lt_ptr_ptr (p1: ptr, p2: ptr):<> bool
and lte_ptr_ptr (p1: ptr, p2: ptr):<> bool

overload < with lt_ptr_ptr
overload <= with lte_ptr_ptr

fun gt_ptr_ptr (p1: ptr, p2: ptr):<> bool
and gte_ptr_ptr (p1: ptr, p2: ptr):<> bool

overload > with gt_ptr_ptr
overload >= with gte_ptr_ptr

fun eq_ptr_ptr (p1: ptr, p2: ptr):<> bool
and neq_ptr_ptr (p1: ptr, p2: ptr):<> bool
overload = with eq_ptr_ptr
overload <> with neq_ptr_ptr
overload != with neq_ptr_ptr
----

Description
^^^^^^^^^^^

This family of functions is used to compare pointers for equality, greater
than, less than, not equal, etc. The comparison operators are overloaded to
work with the comparison functions.

ptr1_of_ptr 
~~~~~~~~~~~

Definition
^^^^^^^^^^
----
castfn ptr1_of_ptr (p: ptr):<> [l:addr] ptr l
----

Description
^^^^^^^^^^^

Cast a 'ptr' to a 'ptr l', which is a dependently typed pointer indexed by its
address.

Example
^^^^^^^
----
implement main() = {
  val a = null + 4
  val b = ptr1_of_ptr (a)
  val () = print (b)
}
----

null
~~~~

Definition
^^^^^^^^^^
----
val null : ptr null
----

Description
^^^^^^^^^^^

'null' is the definition of the NULL pointer. It is a dependently typed
pointer indexed by the 'null' address value.

Example
^^^^^^^
----
implement main() = {
  val a = null
  val () = print (a)
}
----

ptr1_is_null
~~~~~~~~~~~~

Definition
^^^^^^^^^^
----
fun ptr1_is_null {l:addr}
  (p: ptr l):<> bool (l==null)
----

Description
^^^^^^^^^^^
Given a dependently typed pointer indexed by the address value, return 'true' if the pointer is NULL.

Example
^^^^^^^
----
implement main() = {
  val a = null
  val () = assertloc (ptr1_is_null (a))
}
----

ptr1_isnot_null 
~~~~~~~~~~~~~~~

Definition
^^^^^^^^^^
----
fun ptr1_isnot_null {l:addr}
  (p: ptr l):<> bool (l > null)
overload ~ with ptr1_isnot_null
----

Description
^^^^^^^^^^^
Given a dependently typed pointer indexed by the address value, return 'true'
if the pointer is not NULL.

Example
^^^^^^^
----
implement main() = {
  val a = null + 4
  val () = assertloc (ptr1_isnot_null (a))
}
----

psucc
~~~~~

Definition
^^^^^^^^^^
----
fun psucc {l:addr} (p: ptr l):<> ptr (l + 1)
overload succ with psucc
----

Description
^^^^^^^^^^^
Returns the successor of a pointer - the pointer value incremented by one.

Example
^^^^^^^
----
implement main() = {
  val a = null
  val b = psucc (a)
  val () = print (b)
}
----

ppred
~~~~~

Definition
^^^^^^^^^^
----
fun ppred {l:addr} (p: ptr l):<> ptr (l - 1)
overload pred with ppred
----

Description
^^^^^^^^^^^
Returns the predecessor of a pointer - the pointer value decremented by one.

Example
^^^^^^^
----
implement main() = {
  val a = null
  val b = psucc (a)
  val () = print (b)
  val () = print_newline ()
  val c = ppred (b)
  val () = print (c)
}
----

padd
~~~~

Definition
^^^^^^^^^^
----
symintr padd
fun padd_int
  {l:addr}
  {i:int} (
  p: ptr l, i: int i
) :<> ptr (l + i)
overload + with padd_int
overload padd with padd_int

fun padd_size
  {l:addr}
  {i:int} (
  p: ptr l, i: size_t i
) :<> ptr (l + i)
overload + with padd_size
overload padd with padd_size
----

Description
^^^^^^^^^^^
An overloaded function that adds an 'int' or 'size_t' to a pointer.

psub
~~~~

Definition
^^^^^^^^^^
----
symintr psub
fun psub_int
  {l:addr}
  {i:int} (
  p: ptr l, i: int i
) :<> ptr (l - i)
overload - with psub_int
overload psub with psub_int

fun psub_size
  {l:addr}
  {i:int} (
  p: ptr l, i: size_t i
) :<> ptr (l - i)
overload - with psub_size
overload psub with psub_size
----

Description
^^^^^^^^^^^
An overloaded function that subtracts an 'int' or 'size_t' from a pointer.

pdiff
~~~~~

Definition
^^^^^^^^^^
----
fun pdiff
  {l1,l2:addr} (
  p1: ptr l1, p2: ptr l2
) :<> ptrdiff_t (l1 - l2)
overload - with pdiff
----

Description
^^^^^^^^^^^
Subtracts 'p2' from 'p1' and returns the result as a 'ptrdiff_t'.

Indexed Pointer Comparison
~~~~~~~~~~~~~~~~~~~~~~~~~~

Definition
^^^^^^^^^^
----
fun plt {l1,l2:addr}
  (p1: ptr l1, p2: ptr l2):<> bool (l1 < l2)
and plte {l1,l2:addr}
  (p1: ptr l1, p2: ptr l2):<> bool (l1 <= l2)
overload < with plt
overload <= with plte

fun pgt {l1,l2:addr}
  (p1: ptr l1, p2: ptr l2):<> bool (l1 > l2)
and pgte {l1,l2:addr}
  (p1: ptr l1, p2: ptr l2):<> bool (l1 >= l2)
overload > with pgt
overload >= with pgte

fun peq {l1,l2:addr}
  (p1: ptr l1, p2: ptr l2):<> bool (l1 == l2)
and pneq {l1,l2:addr}
  (p1: ptr l1, p2: ptr l2):<> bool (l1 <> l2)
overload = with peq
overload <> with pneq
overload != with pneq
----

Description
^^^^^^^^^^^

This family of functions is used to compare dependently typed pointers indexed
by their address for equality, greater than, less than, not equal, etc. The
comparison operators are overloaded to work with the comparison functions.

compare_ptr_ptr
~~~~~~~~~~~~~~~

Definition
^^^^^^^^^^
----
fun compare_ptr_ptr (p1: ptr, p2: ptr):<> Sgn
overload compare with compare_ptr_ptr
----

Description
^^^^^^^^^^^
Returns a negative number if 'p1' is less than 'p2', a positive number if 'p1'
is greater than 'p2' and zero if 'p1' equals 'p2'.

fprint_ptr
~~~~~~~~~~

Definition
^^^^^^^^^^
----
fun fprint_ptr {m:file_mode}
  (pf: file_mode_lte (m, w) | out: !FILE m, x: ptr):<!exnref> void
overload fprint with fprint_ptr
----

Description
^^^^^^^^^^^
Prints a representation of the pointer value to a file.

print_ptr
~~~~~~~~~

Definition
^^^^^^^^^^
---
fun print_ptr (p: ptr):<!ref> void
overload print with print_ptr
---

Description
^^^^^^^^^^^
Prints a representation of the pointer to standard output.

prerr_ptr
~~~~~~~~~

Definition
^^^^^^^^^^
----
fun prerr_ptr (p: ptr):<!ref> void
overload prerr with prerr_ptr
----

Description
^^^^^^^^^^^
Prints a representation of the pointer to standard error.

tostring_ptr
~~~~~~~~~~~~

Definition
^^^^^^^^^^
----
fun tostring_ptr (p: ptr):<> strptr1
overload tostring with tostring_ptr
----

Description
^^^^^^^^^^^
Returns a string representation of the pointer.

free_gc_t0ype_addr_trans
~~~~~~~~~~~~~~~~~~~~~~~~

Definition
^^^^^^^^^^
----
praxi free_gc_t0ype_addr_trans
  {a1,a2:t@ype | sizeof a1 == sizeof a2} {l:addr}
  (pf_gc: !free_gc_v (a1, l) >> free_gc_v (a2, l)): void
----

Description
^^^^^^^^^^^
TODO: Is the description right?

A proof function asserting that two values of the same size and type, and at
the same memory address, can use the same view for freeing the memory.

ptr_alloc
~~~~~~~~~

Definition
^^^^^^^^^^
----
fun{a:viewt@ype} ptr_alloc ()
  :<> [l:addr | l > null] (free_gc_v (a?, l), a? @ l | ptr l)
----

Description
^^^^^^^^^^^
Template function for allocating memory for a value of type 'a'. It returns a
non-NULL pointer to the allocated memory, a view that is required to free the
memory later and a view for accessing the value stored at that addressed. The
value held at the allocated address is uninitialized.

Example
^^^^^^^
----
staload _ = "prelude/DATS/pointer.dats"

implement main() = {
  val (pf_gc, pf_int | p_int) = ptr_alloc<int> ()
  val () = !p_int := 42
  val () = print (!p_int)
  val () = ptr_free (pf_gc, pf_int | p_int)
}
----

ptr_alloc_tsz
~~~~~~~~~~~~~

Definition
^^^^^^^^^^
----
fun ptr_alloc_tsz
  {a:viewt@ype} (tsz: sizeof_t a)
  :<> [l:addr | l > null] (free_gc_v (a?, l), a? @ l | ptr l)
----

Description
^^^^^^^^^^^
Like 'ptr_alloc', this function is used for allocating memory for a value of
type 'a'. Unlike 'ptr_alloc', this is not a template function, so it takes the
type of the object as a universal variable and the size as an argument (which
must match the actual size of the given universal variable).

It returns a
non-NULL pointer to the allocated memory, a view that is required to free the
memory later and a view for accessing the value stored at that addressed. The
value held at the allocated address is uninitialized.

Example
^^^^^^^
----
implement main() = {
  val (pf_gc, pf_int | p_int) = ptr_alloc_tsz {int} (sizeof<int>)
  val () = !p_int := 42
  val () = print (!p_int)
  val () = ptr_free (pf_gc, pf_int | p_int)
}
----

ptr_free
~~~~~~~~

Definition
^^^^^^^^^^
----
fun ptr_free
  {a:t@ype} {l:addr} (
  pfgc: free_gc_v (a, l), pfat: a @ l | p: ptr l
) :<> void
----

Description
^^^^^^^^^^^
Free's the memory allocated at the address given by the pointer 'p'. Requires
the 'free_gc_v' view that was obtained when allocating the memory originally
and a view for providing access to the type 'a' at that address.

Example
^^^^^^^
See the example for 'ptr_alloc'.

NULLABLE
~~~~~~~~

Definition
^^^^^^^^^^
----
absprop NULLABLE (a: viewt@ype+) // covariant
----

Description
^^^^^^^^^^^
Abstract prop used when dealing with types that can be initialized to zero
(eg. pointers set to NULL, etc). See 'ptr_zero' for example usage.

ptr_zero
~~~~~~~~

Definition
^^^^^^^^^^
----
fun{a:viewt@ype}
ptr_zero (pf: NULLABLE (a) | x: &a? >> a):<> void
----

Description
^^^^^^^^^^^
Given a reference to an uninitialized pointer type this will result in an
initialized type set to zero using 'memset'. A proof view of 'NULLABLE' for
the type is required.

Example
^^^^^^^
----
staload _ = "prelude/DATS/pointer.dats"

implement main() = {
  var p: ptr
  val () = ptr_zero (nullable () | p) where {
             extern prfun nullable (): NULLABLE ptr
           }
  val () = print (p)	   
}
----

ptr_zero_tsz
~~~~~~~~~~~~

Definition
^^^^^^^^^^
----
fun ptr_zero_tsz
  {a:viewt@ype} (
  pf: NULLABLE (a) | x: &a? >> a, tsz: sizeof_t a
) :<> void
----

Description
^^^^^^^^^^^
Non-template version of 'ptr_zero'. Takes the type as a universable variable
and the size of that type as an argument.

Example
^^^^^^^
----
typedef foo = @{ a=int, b=ptr }

implement main() = {
  var p: foo
  val () = ptr_zero_tsz {foo} (nullable () | p, sizeof<foo>) where {
             extern prfun nullable (): NULLABLE foo
           }
  val () = print (p.a)
  val () = print_newline ()
  val () = print (p.b)
----

ptr_get_t
~~~~~~~~~

Definition
^^^^^^^^^^
----
fun{a:t@ype} ptr_get_t {l:addr} (pf: !a @ l | p: ptr l):<> a
----

Description
^^^^^^^^^^^
Returns the value held at the address of the given pointer. Requires a view of
'a @ l' proving a type of 'a' is held at that address. The following two
lines are equivalent:

----
val v = ptr_get_t<int> (pf_int | p_int)
val v = !p_int
----

In the second line the proof of 'int @ l' is implicit - it is found in scope,
whereas the 'ptr_get_t' usage requires passing it explicitly.

Example
^^^^^^^
----
staload _ = "prelude/DATS/pointer.dats"

implement main() = {
  val (pf_gc, pf_int | p_int) = ptr_alloc<int> ()
  val () = ptr_set_t<int> (pf_int | p_int, 42)
  val v = ptr_get_t<int>  (pf_int | p_int)
  val () = print (v)
  val () = ptr_free (pf_gc, pf_int | p_int)
}
----

ptr_set_t
~~~~~~~~~

Definition
^^^^^^^^^^
----
fun{a:t@ype} ptr_set_t {l:addr}
  (pf: !(a?) @ l >> a @ l | p: ptr l, x: a):<> void
----

Description
^^^^^^^^^^^
Sets the value held at the pointer address to 'x'. Requires a view of 'a @ l'
proving a type of 'a' is held at that address. The following two lines are
equivalent:

----
val () = ptr_set_t<int> (pf_int | p_int, 42)
val () = !p_int := 42 
----

In the second line the proof of 'int @ l' is implicit - it is found in scope,
whereas the 'ptr_set_t' usage requires passing it explicitly.

Example
^^^^^^^
See 'ptr_get_t' for an example of usage.

ptr_move_t
~~~~~~~~~~

Definition
^^^^^^^^^^
----
fun{a:t@ype} ptr_move_t {l1,l2:addr}
  (pf1: !a @ l1, pf2: !(a?) @ l2 >> a @ l2 | p1: ptr l1, p2: ptr l2):<> void
----

Description
^^^^^^^^^^^
Copies the value held at pointer location 'p1' into 'p2'. 

Example
^^^^^^^
----
staload _ = "prelude/DATS/pointer.dats"

implement main() = {
  val (pf_gc, pf_int | p_int) = ptr_alloc<int> ()
  var x: int = 42
  val () = ptr_move_t<int> (view@ x, pf_int | &x, p_int)
  val () = print (!p_int)
  val () = ptr_free (pf_gc, pf_int | p_int)
}
----

ptr_move_t_tsz
~~~~~~~~~~~~~~

Definition
^^^^^^^^^^
----
fun ptr_move_t_tsz {a:t@ype} {l1,l2:addr} (
    pf1: !a @ l1, pf2: !(a?) @ l2 >> a @ l2
  | p1: ptr l1, p2: ptr l2, tsz: sizeof_t a
  ) :<> void
----

Description
^^^^^^^^^^^
A non-template version of 'ptr_move_t'. The type is passed as a universal
variable and the size is an argument.

Example
^^^^^^^
----
staload _ = "prelude/DATS/pointer.dats"

typedef foo = @{ a= int, b= string }

implement main() = {
  var x: foo = @{ a= 42, b= "Hello World" }
  val (pf_gc, pf_foo | p_foo) = ptr_alloc<foo> ()
  val () = ptr_move_t_tsz {foo} (view@ x, pf_foo | &x, p_foo, sizeof<foo>)
  val () = print (!p_foo.a)
  val () = print_newline ()
  val () = print (!p_foo.b)
  val () = ptr_free (pf_gc, pf_foo | p_foo)
}
----

ptr_get_vt
~~~~~~~~~~

Definition
^^^^^^^^^^
----
fun{a:viewt@ype}
ptr_get_vt {l:addr}
  (pf: !a @ l >> (a?!) @ l | p: ptr l):<> a
----

Description
^^^^^^^^^^^
Same as 'ptr_get_t' but for viewtypes (linear types).

Example
^^^^^^^
----
staload _ = "prelude/DATS/pointer.dats"

viewtypedef foo (l:addr) = @{ a= int, b= strptr l }
viewtypedef foo = [l:addr] foo l

implement main() = {
  val x = @{ a= 42, b= sprintf ("Hello World", @()) }
  val (pf_gc, pf_foo | p_foo) = ptr_alloc<foo> ()
  val () = ptr_set_vt<foo> (pf_foo | p_foo, x)
  val v = ptr_get_vt<foo> (pf_foo | p_foo)
  val () = print (v.a)
  val () = print_newline ()
  val () = print (v.b)
  val () = strptr_free (v.b)
  val () = ptr_free (pf_gc, pf_foo | p_foo)
}
----

ptr_set_vt
~~~~~~~~~~

Definition
^^^^^^^^^^
----
fun{a:viewt@ype}
ptr_set_vt {l:addr}
  (pf: !(a?) @ l >> a @ l | p: ptr l, x: a):<> void
----

Description
^^^^^^^^^^^
Same as 'ptr_set_t' but for viewtypes (linear types).

Example
^^^^^^^
See 'ptr_get_vt' for an example of usage.

ptr_move_vt
~~~~~~~~~~~

Definition
^^^^^^^^^^
----
fun{a:viewt@ype}
ptr_move_vt {l1,l2:addr} (
    pf1: !a @ l1 >> (a?) @ l1, pf2: !(a?) @ l2 >> a @ l2
  | p1: ptr l1, p2: ptr l2
  ) :<> void
----

Description
^^^^^^^^^^^
Like 'ptr_move_t' but for viewtypes (linear types). Unlike 'ptr_move_t' this
is an actual move rather than a copy. Because the type is linear, the original
value at the pointer address is no longer accessible after the move operation
(it becomes a pointer to an uninitialized type).

Example
^^^^^^^
----
staload _ = "prelude/DATS/pointer.dats"

viewtypedef foo (l:addr) = @{ a= int, b= strptr l }
viewtypedef foo = [l:addr] foo l

implement main() = {
  var foo1: foo = @{ a= 42, b= sprintf ("Hello World", @()) }
  val (pf_gc, pf_foo | p_foo) = ptr_alloc<foo> ()
  val () = ptr_move_vt<foo> (view@ foo1, pf_foo | &foo1, p_foo)
  val () = print (!p_foo.a)
  val () = print_newline ()
  val () = print (!p_foo.b)
  val () = strptr_free (!p_foo.b)
  val () = ptr_free (pf_gc, pf_foo | p_foo)
}
----

ptr_move_vt_tsz
~~~~~~~~~~~~~~~

Definition
^^^^^^^^^^
----
fun ptr_move_vt_tsz
  {a:viewt@ype} {l1,l2:addr} (
    pf1: !a @ l1 >> (a?) @ l1, pf2: !(a?) @ l2 >> a @ l2
  | p: ptr l1, p2: ptr l2, tsz: sizeof_t a
  ) :<> void
----

Description
^^^^^^^^^^^
Non-template version of 'ptr_move_vt', where the viewtype is provided as a
universal variable and the size is passed explicitly.

Unsafe Functions
----------------

The functions and definitions in 'prelude/SATS/unsafe.sats' allow performing
operations that bypass the type system. They provide a way of saying "I know
what I'm doing". For example, casting from one type to another, dereferencing
a pointer without a proof, etc.

Some usages of the unsafe functions are to cast from different function types
to pass to higher order functions that only accept one type, casting from
linear strings to persistent strings temporarily, casting from linear types to
non-linear types to share non-linear function implementations in the linear
implementation, etc.

Unlike other prelude files, the 'unsafe.sats' file is not loaded by default
and must be explicitly loaded.

cast
~~~~

Definition
^^^^^^^^^^
----
castfn cast {to:t@ype} {from:t@ype} (x: from):<> to
----

Description
^^^^^^^^^^^
Cast from one type to another. The 'from' universal variable is often inferred
rather than provided.

Example
^^^^^^^
----
staload "prelude/SATS/unsafe.sats"

implement main() = {
  val a: int = 5
  val () = print_int (a)
  val () = print_uint (cast {uint} (a))
}
----

castvwtp1
~~~~~~~~~

Definition
^^^^^^^^^^
----
castfn castvwtp1 {to:t@ype} {from:viewt@ype} (x: !from):<> to
----

Description
^^^^^^^^^^^
Cast from a viewtype to a type. This is often used to cast from a linear
string ('strptr') to a persistent string ('string'), as a means of passing a
read-only view of the linear string. This allows functions that use strings to
mainly use the 'string' type if they don't modify the string and don't hold a
pointer to it.

Example
^^^^^^^
----
staload "prelude/sats/unsafe.sats"

implement main() = {
  val a: strptr1 = sprintf("hello world", @())
  val () = print_string (castvwtp1 {string} (a))
  val () = strptr_free (a)
}
----

cast2ptr
~~~~~~~~

Definition
^^^^^^^^^^
----
castfn cast2ptr {a:type} (x: a):<> ptr
----

Description
^^^^^^^^^^^
Cast from any type to a pointer.

cast2int
~~~~~~~~

Definition
^^^^^^^^^^
----
castfn cast2int {a:t@ype} (x: a):<> int
----

Description
^^^^^^^^^^^
Cast from any type to an int.

cast2uint
~~~~~~~~~

Definition
^^^^^^^^^^
----
castfn cast2uint {a:t@ype} (x: a):<> uint
----

Description
^^^^^^^^^^^
Cast from any type to an unsigned int.

cast2lint
~~~~~~~~~

Definition
^^^^^^^^^^
----
castfn cast2lint {a:t@ype} (x: a):<> lint
----

Description
^^^^^^^^^^^
Cast from any type to a long int.

cast2ulint
~~~~~~~~~~

Definition
^^^^^^^^^^
----
castfn cast2ulint {a:t@ype} (x: a):<> ulint
----

Description
^^^^^^^^^^^
Cast from any type to an unsigned long int.

cast2size
~~~~~~~~~

Definition
^^^^^^^^^^
----
castfn cast2size {a:t@ype} (x: a):<> size_t
----

Description
^^^^^^^^^^^
Cast from any type to a 'size_t'.

cast2ssize
~~~~~~~~~~
-----
castfn cast2ssize {a:t@ype} (x: a):<> ssize_t
----

Description
^^^^^^^^^^^
Cast from any type to a 'ssize_t'.

ptrget
~~~~~~

Definition
^^^^^^^^^^
----
fun{a:viewt@ype} ptrget (p: ptr):<> a
----

Description
^^^^^^^^^^^
Returns the value stored at the pointer address without requiring a proof that
the type is held at the address.

Example
^^^^^^^
----
staload "prelude/SATS/unsafe.sats"
staload _ = "prelude/DATS/unsafe.dats"

implement main() = {
  var a: int = 0x65666768
  val p = &a
  var ch1 = ptrget<char> (p)
  var ch2 = ptrget<char> (p + 1)
  var ch3 = ptrget<char> (p + 2)
  var ch4 = ptrget<char> (p + 3)
  val () = printf("%c %c %c %c\n", @(ch1, ch2, ch3, ch4))
}
----

ptrset
~~~~~~

Definition
^^^^^^^^^^
----
fun{a:viewt@ype} ptrset (p: ptr, x: a):<> void
----

Description
^^^^^^^^^^^
Set a value at a pointer address without requiring a proof of the type
existing at that address.

Example
^^^^^^^
----
staload "prelude/SATS/unsafe.sats"
staload _ = "prelude/DATS/unsafe.dats"

implement main() = {
  var a: int = 0
  val p = &a
  var ch1 = ptrset<char> (p, 'a')
  var ch2 = ptrset<char> (p + 1, 'b')
  var ch3 = ptrset<char> (p + 2, 'c')
  var ch4 = ptrset<char> (p + 3, 'd')
  val () = printf ("%d\n", @(a))
}
----

vtakeout
~~~~~~~~

Definition
^^^^^^^^^^
----
absview viewout (v:view) // invariant!
prfun vtakeout {v:view} (pf: !v): viewout (v)
prfun viewout_decode
  {v:view} (pf: viewout (v)): (v, v -<lin,prf> void)
----

Description
^^^^^^^^^^^
Unsure what this is for. Documentation for this appreciated.

Strings
-------

The following tables lists the main string types and what they're used
for:

|=========================================================================
| string    | A non linear string that can only be free'd by the GC
| String    | A non linear string with a length. This is sometimes referred
              to in functions as a 'string1'.
| stropt    | An optional type with states for non-null and null non linear
              strings with a length.
| Stropt    | A typedef for 'stropt' with any length.
| strbuf    | A linear array of bytes where the last byte is null
| strptr    | A linear string which must be manually free'd.
| strptr0   | An strptr that can be null.
| strptr1   | An strptr that cannot be null.
| strptrlen | A linear string with a length
|=========================================================================

A number of types are defined for characters and bytes:

|=========================================================================
| bytes (int)  | A 'byte' array with a length
| b0ytes (int) | An unintialized 'byte' array with a length
| chars (int)  | A 'char' array with a  length
| c0hars (int) | An unintialized 'char' array with a length 
| c1har        | A non-null 'char' 
| c1hars (int) | An array of non-null chars with a length
|=========================================================================