Skip to content

Comparing changes

Choose two branches to see what’s changed or to start a new pull request. If you need to, you can also compare across forks.

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also compare across forks.
...
  • 8 commits
  • 7 files changed
  • 0 commit comments
  • 1 contributor
Showing with 389 additions and 1 deletion.
  1. +4 −0 Makefile
  2. +337 −0 ats-reference.txt
  3. +21 −1 pointer/Makefile
  4. +8 −0 pointer/ppred.dats
  5. +5 −0 pointer/psucc.dats
  6. +8 −0 pointer/ptr_alloc.dats
  7. +6 −0 pointer/ptr_alloc_tsz.dats
View
4 Makefile
@@ -1,5 +1,9 @@
ats-reference.pdf: ats-reference.txt
a2x -f pdf --fop ats-reference.txt
+ats-reference.html docbook-xsl.css: ats-reference.txt
+ a2x -f xhtml ats-reference.txt
+
clean:
-rm ats-reference.pdf
+ -rm ats-reference.html docbook-xsl.css
View
337 ats-reference.txt
@@ -1284,3 +1284,340 @@ implement main() = {
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'.
+
View
22 pointer/Makefile
@@ -5,7 +5,11 @@ all: ptr_is_null \
ptr1_of_ptr \
null \
ptr1_is_null \
- ptr1_isnot_null
+ ptr1_isnot_null \
+ psucc \
+ ppred \
+ ptr_alloc \
+ ptr_alloc_tsz
ptr_is_null: ptr_is_null.dats
atscc -o ptr_is_null ptr_is_null.dats
@@ -31,6 +35,18 @@ ptr1_is_null: ptr1_is_null.dats
ptr1_isnot_null: ptr1_isnot_null.dats
atscc -o ptr1_isnot_null ptr1_isnot_null.dats
+psucc: psucc.dats
+ atscc -o psucc psucc.dats
+
+ppred: ppred.dats
+ atscc -o ppred ppred.dats
+
+ptr_alloc: ptr_alloc.dats
+ atscc -o ptr_alloc ptr_alloc.dats
+
+ptr_alloc_tsz: ptr_alloc_tsz.dats
+ atscc -o ptr_alloc_tsz ptr_alloc_tsz.dats
+
clean:
-rm *_dats.c
@@ -43,5 +59,9 @@ clean:
-rm null
-rm ptr1_is_null
-rm ptr1_isnot_null
+ -rm psucc
+ -rm ppred
+ -rm ptr_alloc
+ -rm ptr_alloc_tsz
View
8 pointer/ppred.dats
@@ -0,0 +1,8 @@
+implement main() = {
+ val a = null
+ val b = psucc (a)
+ val () = print (b)
+ val () = print_newline ()
+ val c = ppred (b)
+ val () = print (c)
+}
View
5 pointer/psucc.dats
@@ -0,0 +1,5 @@
+implement main() = {
+ val a = null
+ val b = psucc (a)
+ val () = print (b)
+}
View
8 pointer/ptr_alloc.dats
@@ -0,0 +1,8 @@
+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)
+}
View
6 pointer/ptr_alloc_tsz.dats
@@ -0,0 +1,6 @@
+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)
+}

No commit comments for this range

Something went wrong with that request. Please try again.