diff --git a/ats-reference.txt b/ats-reference.txt index 739df9e..2d4490c 100644 --- a/ats-reference.txt +++ b/ats-reference.txt @@ -1824,3 +1824,99 @@ implement main() = { 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 () + val () = ptr_set_vt (pf_foo | p_foo, x) + val v = ptr_get_vt (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 () + val () = ptr_move_vt (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) +} +---- + diff --git a/pointer/Makefile b/pointer/Makefile index 754bd8c..914e778 100644 --- a/pointer/Makefile +++ b/pointer/Makefile @@ -14,7 +14,9 @@ all: ptr_is_null \ ptr_zero_tsz \ ptr_get_t \ ptr_move_t \ - ptr_move_t_tsz + 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 @@ -67,6 +69,12 @@ 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 @@ -88,5 +96,7 @@ clean: -rm ptr_get_t -rm ptr_move_t -rm ptr_move_t_tsz + -rm ptr_get_vt + -rm ptr_move_vt diff --git a/pointer/ptr_get_vt.dats b/pointer/ptr_get_vt.dats new file mode 100644 index 0000000..4e9b40a --- /dev/null +++ b/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 () + val () = ptr_set_vt (pf_foo | p_foo, x) + val v = ptr_get_vt (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) +} diff --git a/pointer/ptr_move_vt.dats b/pointer/ptr_move_vt.dats new file mode 100644 index 0000000..572ff57 --- /dev/null +++ b/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 () + val () = ptr_move_vt (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) +}