Convert from array to pointer

Google Group
1

hello,
I would like to use an API that take a pointer as argument ( lets say a
@[float][3] ) and I start from array(float, 3).
How can I convert from one to another ?

I have seen this definition in array.dats

assume array_viewt0ype_int_type
(a:viewt@ype, n:int) = [l:addr] @{
data= ptr l, view= vbox (array_v (a, n, l))
} // end of [array_viewt0ype_int_type]

that make me think I can do like this :

staload _(anonymous)=“prelude/DATS/array.dats”

implement main(argc, argv) = let
fun {a:t@ype} vec3_create (x: a, y: a, z: a): array(a, 3) = let
val (_, pf|p, sz) = $arrsz {a}(x, y, z)
in array_make_view_ptr(pf|p) end

val my_vec3: array(float, 3) = vec3_create(1.0f, 0.0f, 0.0f)
val () = printf("%f, %f, %f\n", @(double_of my_vec3[0], double_of my_vec3[
1], double_of my_vec3[2]))

fun do_nothing (t: &(@[float][3])): void = ()
val p = my_vec3.data // <- ERROR
prval vbox pf = my_vec3.view
in
do_nothing(!p)
end

Unfortunately I have this error :
arr.dats: 445(line=12, offs=11) – 457(line=12, offs=23): error(3): the
type [S2Eapp(S2Ecst(array_viewt0ype_int_type); S2Ecst(float), S2Eint(3))]
is expected to be a record or union but it is not.

I took the code from array.dats :

fun{a:t@ype}
array_get_elt_at {n:int}
{i:nat | i < n} (A: array (a, n), i: size_t i):<!ref> a

…

implement{a}
array_get_elt_at (A, i) = let
val A_data = A.data; prval vbox pf = A.view in !A_data.[i]
end // end of [array_get_elt]

thanks :wink:

2

thank you now I understand better data encapsulation with abstract type.

working example is :

staload _(anonymous)=“prelude/DATS/array.dats”

implement main(argc, argv) = let
fun{a:t@ype} vec3_create (x: a, y: a, z: a): array(a, 3) = let
val (_, pf|p, sz) = $arrsz {a}(x, y, z)
in array_make_view_ptr(pf|p) end

fun do_print{n:nat|n>2} (t: &(@[float][n])): void =
printf("-> %f, %f, %f\n", @(double_of t[0], double_of t[1], double_of t[
2]))

val my_vec3: array(float, 3) = vec3_create(1.0f, 0.0f, 0.0f)
val (vbox pf1|p1) = array_get_view_ptr(my_vec3)
val () = $effmask_ref(do_print(!p1))

val (_, pf2|p2, sz) = $arrsz {float}(1.1f, 2.2f, 3.3f)
extern prfun __leak {v:view} (pf: v): void
val () = $effmask_ref(do_print(!p2))
prval () = __leak(pf2)
in
end

Some questions about array_get_view_ptr :

  • Is it because vbox convert to linear view that I don’t have to consume
    the pf1 proof ?
  • Why the vbox disallow [ref] effect even for the p2 pointer ?

thanks for your precious help :wink:

3

thank you I will study your paper about safe resource sharing

I just discarded the gc proof to use the garbage collector.
I will gradually manage my memory by hand afterward :wink:

4

It is great that you made it to work.

Properly using the abstype mechanism in ATS is really essential for
programming in ATS
effectively. As far as program structuring/organization is concerned,
abstype is kind of like
class in OOP (but without support for inheritance).

  • Is it because vbox convert to linear view that I don’t have to consume
    the pf1 proof ?

viewbox (vbox) is just like a box; the typechecker makes sure that the
proof taken out
of a vbox is returned. If you consume the proof, then the typechecker will
report a type-error.

  • Why the vbox disallow [ref] effect even for the p2 pointer ?

This one is a bit hard to explain. It has something to do with re-entrant
code. Basically,
if a function uses vbox in its body, then this function is not re-entrant
(and thus not thread-safe).
Here is a paper that explains vbox (and other related issues):

5

By the way, I would like to point out that the first pattern _
in the following code discards a linear proof:

val (_, pf2|p2, sz) = $arrsz {float}(1.1f, 2.2f, 3.3f)

If you don’t want to discard it, please do

val (pf2gc, pf2|p2, sz) = $arrsz {float}(1.1f, 2.2f, 3.3f)

Then you can free the array later by calling array_ptr_free,
which will consume both pf2gc and pf2. pf2gc is just a certificate
indicating that the pointer [p2] is allowed to be freed.

6

‘array’ is an abstract type. Only in array.dats, its definition is
revealed. Outside array.dats,
A.data causes a type-error. Try to use the following function to get the
ptr and the view of
a given array:

array_get_view_ptr