How to use gfarray?

[Kiwamu Okabe]

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

[Hongwei Xi]

Basically, a stack-allocated array cannot be consumed.

--
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.

[Kiwamu Okabe]

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?

[Hongwei Xi]

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.

--
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.

[Kiwamu Okabe]

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

[gmhwxi]

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](100,200,300)
  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)
}

[Kiwamu Okabe]

On Mon, Jul 13, 2015 at 12:14 AM, gmhwxi <gmh...@gmail.com> 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...

[gmhwxi]

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.