How to create value of type stamped_t (a, x)?

[Kiwamu Okabe]

Hi all,

Today I read interfaces of libats/SATS/gfarray.sats.

fun{a:t@ype}
gfarray_set_at
{l:addr}
{x:int}{xs1:ilist}{xs2:ilist}
{i:int}
(
pf1: UPDATE (x, xs1, i, xs2)
, pf2: !gfarray_v (a, l, xs1) >> gfarray_v (a, l, xs2)
| p: ptr l, i: size_t i, x: stamped_t (a, x)
) :<!wrt> void // end of [gfarray_set_at]

The gfarray_set_at function need stamped_t (a, x) type to change
entity of the array.

How to create value of type stamped_t (a, x)?
Need to cast for it?

Best regards,
--
Kiwamu Okabe at METASEPI DESIGN

[Hongwei Xi]

Yes, you need a  cast.

--
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/CAEvX6dkpUOnweJWKn1SQ7B0qpOJsWos3r_8OCT1%2B_Q6RzsuLnA%40mail.gmail.com.

[Hongwei Xi]

The following function is a *safe* cast:

{a:t@ype} (a) -> [x:int] stamped_t(a, x)

[Kiwamu Okabe]

On Fri, Jun 19, 2015 at 8:06 AM, Hongwei Xi <gmh...@gmail.com> wrote:
> The following function is a *safe* cast:
>
> {a:t@ype} (a) -> [x:int] stamped_t(a, x)

Use castfn?
How about define the function at prelude/basics_dyn.sats?

[gmhwxi]

Done.

castfn stamp_t : {a:t@ype} (a) -> [x:int] stamped_t(a, x)
castfn stamp_vt : {a:vt@ype} (a) -> [x:int] stamped_vt(a, x)

[Kiwamu Okabe]

On Fri, Jun 19, 2015 at 12:34 PM, gmhwxi <gmh...@gmail.com> wrote:
> Done.
>
> castfn stamp_t : {a:t@ype} (a) -> [x:int] stamped_t(a, x)
> castfn stamp_vt : {a:vt@ype} (a) -> [x:int] stamped_vt(a, x)

Thank's. It's useful.

https://github.com/jats-ug/practice-ats/commit/ccc8fbc3086402da565603a4d7f6b2e6aa6c3b86