Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP

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.
base fork: doublec/ats-reference
base: cd22e5bfff
...
head fork: doublec/ats-reference
compare: f0c989a08d
  • 6 commits
  • 9 files changed
  • 0 commit comments
  • 1 contributor
View
318 ats-reference.txt
@@ -1621,3 +1621,321 @@ 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.
+
+
View
37 pointer/Makefile
@@ -9,7 +9,14 @@ all: ptr_is_null \
psucc \
ppred \
ptr_alloc \
- ptr_alloc_tsz
+ ptr_alloc_tsz \
+ ptr_zero \
+ ptr_zero_tsz \
+ ptr_get_t \
+ ptr_move_t \
+ ptr_move_t_tsz \
+ ptr_get_vt \
+ ptr_move_vt
ptr_is_null: ptr_is_null.dats
atscc -o ptr_is_null ptr_is_null.dats
@@ -47,6 +54,27 @@ ptr_alloc: ptr_alloc.dats
ptr_alloc_tsz: ptr_alloc_tsz.dats
atscc -o ptr_alloc_tsz ptr_alloc_tsz.dats
+ptr_zero: ptr_zero.dats
+ atscc -o ptr_zero ptr_zero.dats
+
+ptr_zero_tsz: ptr_zero_tsz.dats
+ atscc -o ptr_zero_tsz ptr_zero_tsz.dats
+
+ptr_get_t: ptr_get_t.dats
+ atscc -o ptr_get_t ptr_get_t.dats
+
+ptr_move_t: ptr_move_t.dats
+ atscc -o ptr_move_t ptr_move_t.dats
+
+ptr_move_t_tsz: ptr_move_t_tsz.dats
+ atscc -o ptr_move_t_tsz ptr_move_t_tsz.dats
+
+ptr_get_vt: ptr_get_vt.dats
+ atscc -o ptr_get_vt ptr_get_vt.dats
+
+ptr_move_vt: ptr_move_vt.dats
+ atscc -o ptr_move_vt ptr_move_vt.dats
+
clean:
-rm *_dats.c
@@ -63,5 +91,12 @@ clean:
-rm ppred
-rm ptr_alloc
-rm ptr_alloc_tsz
+ -rm ptr_zero
+ -rm ptr_zero_tsz
+ -rm ptr_get_t
+ -rm ptr_move_t
+ -rm ptr_move_t_tsz
+ -rm ptr_get_vt
+ -rm ptr_move_vt
View
9 pointer/ptr_get_t.dats
@@ -0,0 +1,9 @@
+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)
+}
View
16 pointer/ptr_get_vt.dats
@@ -0,0 +1,16 @@
+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)
+}
View
9 pointer/ptr_move_t.dats
@@ -0,0 +1,9 @@
+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)
+}
View
13 pointer/ptr_move_t_tsz.dats
@@ -0,0 +1,13 @@
+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)
+}
View
15 pointer/ptr_move_vt.dats
@@ -0,0 +1,15 @@
+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)
+}
View
9 pointer/ptr_zero.dats
@@ -0,0 +1,9 @@
+staload _ = "prelude/DATS/pointer.dats"
+
+implement main() = {
+ var p: ptr
+ val () = ptr_zero (nullable () | p) where {
+ extern prfun nullable (): NULLABLE ptr
+ }
+ val () = print (p)
+}
View
11 pointer/ptr_zero_tsz.dats
@@ -0,0 +1,11 @@
+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)
+}

No commit comments for this range

Something went wrong with that request. Please try again.