How to use gfarray?

Google Group
1

Basically, a stack-allocated array cannot be consumed.On Sat, Jul 11, 2015 at 7:21 AM, Kiwamu Okabe kiw...@debian.or.jp wrote:

Hi all,

I start to write code with gfarray library.
However I catch “the linear dynamic variable [arr$view$4464(-1)] is
preserved but with an incompatible type” error.
How to fix it?

#include “share/atspre_define.hats”
#include “share/atspre_staload.hats”

staload “libats/SATS/ilist_prf.sats”
staload “libats/SATS/gfarray.sats”
staload _ = “libats/DATS/gfarray.dats”
staload UN = “prelude/SATS/unsafe.sats”

#define N 16

extern prfun
array2gfarray_v
{a:vt@ype}{l:addr}{n:nat}
(pf: array_v (a, l, n)): [xs:ilist] gfarray_v (a, l, xs)

extern prfun
consume_gfarray_v
{a:vt@ype}{l:addr}{xs:ilist}
(pf: gfarray_v (a, l, xs)): void

implement main0 () = {
var arr: @[int][N]?
prval gfarr = array2gfarray_v view@arr
prval () = consume_gfarray_v gfarr
}

Thank’s,

Kiwamu Okabe at METASEPI DESIGN

–
You received this message because you are subscribed to the Google Groups
“ats-lang-users” group.
To unsubscribe from this group and stop receiving emails from it, send an
email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/CAEvX6dmf9z7hpjUM4YERXSF66Rj5S48sKofPCf_%2B6i6JPtvgqA%40mail.gmail.com
.

2

Well, my point is that you cannot really implement a proof function like
consume_gfarray_v (without leaking resource).
Using gfarray is not different from using array. If you have a function
like consume_array_v, then you will encounter the same problem.On Sat, Jul 11, 2015 at 10:07 AM, Kiwamu Okabe kiw...@debian.or.jp wrote:

On Sat, Jul 11, 2015 at 11:04 PM, Hongwei Xi gmh...@gmail.com wrote:

Basically, a stack-allocated array cannot be consumed.

Umm… Do you have another solution to use gfarrray from application?

Thank’s,

Kiwamu Okabe at METASEPI DESIGN

–
You received this message because you are subscribed to the Google Groups
“ats-lang-users” group.
To unsubscribe from this group and stop receiving emails from it, send an
email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/CAEvX6dmnvuq40%3D3eUXUSWMDKRU7zGbfNH3TN6EESEXxpRadHPg%40mail.gmail.com
.

3

Say you implement:

sort_gfarray:
(
LENGTH(xs, n),
gfarray_v(a, l, xs) >> gfarray_v(a, l, xs2)
| ptr(l), int(n)
) : #[xs2:ilist] (SORT(xs, xs2) | (void))

You can just cast sort_gfarray into:

sort_array
(array_v(a, l, n) >> array_v(a, l, n) | ptr(l), int(n)): void

Or cast sort_gfarray into the following one:

sort_arrayptr : (!arrayptr(a, l, n), int(n)) → void

Casting individual gfarrays is too messy.On Sunday, July 12, 2015 at 11:22:45 AM UTC-4, Kiwamu Okabe wrote:

On Mon, Jul 13, 2015 at 12:14 AM, gmhwxi <gmh...@gmail.com <javascript:>> wrote:

The following is something that works. You need the latest
version of ATS2 at Github.

Thank’s a lot. It works.

I have to say that gfarray is probably not
meant to be used in this way; it is mainly for doing program
verification.

Umm… I would like to write sort application on Arduino board.
If it’s verified with ATS/LF, I’m so happy…

Thank’s,

Kiwamu Okabe at METASEPI DESIGN

4

The following is something that works. You need the latest
version of ATS2 at Github. I have to say that gfarray is probably not
meant to be used in this way; it is mainly for doing program verification.

//
#include
“share/atspre_staload.hats”
//
staload
“libats/SATS/ilist_prf.sats”
//
staload “libats/SATS/gfarray.sats”
staload _ = “libats/DATS/gfarray.dats”
//
staload UN = “prelude/SATS/unsafe.sats”
//
implement main0 () = {
var arr = @int
vtypedef VT = [xs:ilist](LENGTH(xs, 3), gfarray_v(int, arr, xs) | ptr(arr
))
val (pflen, pfarr | arr) = $UN.castvwtp0{VT}(addr@arr)
prval nth0 = NTHbas ()
prval LENGTHcons _ = pflen
val v = gfarray_get_at (nth0, pfarr | arr, i2sz(0))
val () = println! ("gfarray[0] = ", unstamp_t{int}(v))
prval () = $UN.castview0(pfarr)
}On Sunday, July 12, 2015 at 8:09:27 AM UTC-4, Kiwamu Okabe wrote:

I try to cast @[int][N] into gfarray_v (int, l, xs).
But it’s hard to access first entry of gfarray in this time…

local
#define N 16
var _global_arr: @[int][N]?
in
fun arr_takeout (): [l:addr][xs:ilist] (LENGTH (xs, N), gfarray_v
(int, l, xs) | ptr l) = let
extern castfn cast_takeout {l:addr} (ptr l):
[xs:ilist] (LENGTH (xs, N), gfarray_v (int, l, xs) | ptr l)
in
cast_takeout addr@_global_arr
end
fun arr_addback {l:addr}{xs:ilist} (pfarr: gfarray_v (int, l, xs) |
addr: ptr l): void = let
extern castfn cast_addback {l:addr}{xs:ilist} (pfarr: gfarray_v
(int, l, xs) | addr: ptr l): void
in
cast_addback (pfarr | addr)
end
end

implement main0 () = {
val (pflen, pfarr | arr) = arr_takeout ()
prval nth0 = NTHbas ()
val v = gfarray_get_at (nth0, pfarr | arr, i2sz 0)
// val () = arr_addback (pfarr | arr)
}

–
Kiwamu Okabe