How to partition/split an array

Google Group
1

Suppose I have a an array :

val (pf , pfree | p) = array_ptr_tabulate (i2sz(10))

Assume that I have implemented “array_tabulate$fopr”

Now I want to split it into two array views :

prval (pf1,pf2) = array_v_split{int}{…}{10}{1} (pf)

Now I can do :

val () = fprint_array_sep(stdout_ref , !p , i2sz(1), “,”)

!p has a proof in pf1 right ?

How do I print the of array associated with pf2 . How I get a pointer
which is associated with pf2 ?

val p2 =???

val () = fprint_array_sep(stdout_ref , !p2 , i2sz(9), “,”)

I tried to use pointer arithmetic , but it not working . I am pretty sure I
am missing some thing or making some stupid mistake.

Any idea what I might be doing wrong.

Thanks

2

In my experience with linear types, the main limiting factor is not
knowing about certain proof-related functions like viewptr_match. I’m
not sure of the best way to organize a list (or a “cheat sheat”) of
these. But if suggestions are made, I’d be happy to take the
initiative on the wiki or elsewhere; maybe make a pdf and just link to
it on the wiki.
Brandon Barker
brandon…@gmail.comOn Mon, Mar 17, 2014 at 11:38 AM, gmhwxi gmh...@gmail.com wrote:

See:

https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/ATS-QA-LIST/qa-list-229.dats

On Monday, March 17, 2014 8:54:53 AM UTC-4, chotu s wrote:

Suppose I have a an array :

val (pf , pfree | p) = array_ptr_tabulate (i2sz(10))

Assume that I have implemented “array_tabulate$fopr”

Now I want to split it into two array views :

prval (pf1,pf2) = array_v_split{int}{…}{10}{1} (pf)

Now I can do :

val () = fprint_array_sep(stdout_ref , !p , i2sz(1), “,”)

!p has a proof in pf1 right ?

How do I print the of array associated with pf2 . How I get a pointer
which is associated with pf2 ?

val p2 =???

val () = fprint_array_sep(stdout_ref , !p2 , i2sz(9), “,”)

I tried to use pointer arithmetic , but it not working . I am pretty sure
I am missing some thing or making some stupid mistake.

Any idea what I might be doing wrong.

Thanks

–
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.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/fc246379-bc28-49d0-b852-2e3da4d6dd54%40googlegroups.com.

3

See:

https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/ATS-QA-LIST/qa-list-229.datsOn Monday, March 17, 2014 8:54:53 AM UTC-4, chotu s wrote:

Suppose I have a an array :

val (pf , pfree | p) = array_ptr_tabulate (i2sz(10))

Assume that I have implemented “array_tabulate$fopr”

Now I want to split it into two array views :

prval (pf1,pf2) = array_v_split{int}{…}{10}{1} (pf)

Now I can do :

val () = fprint_array_sep(stdout_ref , !p , i2sz(1), “,”)

!p has a proof in pf1 right ?

How do I print the of array associated with pf2 . How I get a pointer
which is associated with pf2 ?

val p2 =???

val () = fprint_array_sep(stdout_ref , !p2 , i2sz(9), “,”)

I tried to use pointer arithmetic , but it not working . I am pretty sure
I am missing some thing or making some stupid mistake.

Any idea what I might be doing wrong.

Thanks

4

The file uses the following function:

castfn
viewptr_match
{a:vt0p}{l1,l2:addr | l1==l2}
(pf: INV(a) @ l1 | p: ptr l2):<> [l:addr | l==l1] (a @ l | ptr l)
// end of [viewptr_match]

Why use the extra l2 in the input and l in the output?

Say p is of the type ptr(L) for some L. When seeing !p, the typechecker tries to
find a proof of the view T @ L for some T; if there is a proof pf2 of the view T @ L2
for some L2 such that L and L2 are equal but of different syntactical forms (e.g.,
1+2=3 but 1+2 and 3 are of different forms), then the typechecker cannot pick this pf2.
Under such a situation, the proof function ‘viewptr_match’ can be called to unify L and L2
syntactically.On Monday, March 17, 2014 11:38:31 AM UTC-4, gmhwxi wrote:

See:

https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/ATS-QA-LIST/qa-list-229.dats

On Monday, March 17, 2014 8:54:53 AM UTC-4, chotu s wrote:

Suppose I have a an array :

val (pf , pfree | p) = array_ptr_tabulate (i2sz(10))

Assume that I have implemented “array_tabulate$fopr”

Now I want to split it into two array views :

prval (pf1,pf2) = array_v_split{int}{…}{10}{1} (pf)

Now I can do :

val () = fprint_array_sep(stdout_ref , !p , i2sz(1), “,”)

!p has a proof in pf1 right ?

How do I print the of array associated with pf2 . How I get a pointer
which is associated with pf2 ?

val p2 =???

val () = fprint_array_sep(stdout_ref , !p2 , i2sz(9), “,”)

I tried to use pointer arithmetic , but it not working . I am pretty sure
I am missing some thing or making some stupid mistake.

Any idea what I might be doing wrong.

Thanks