How to partition/split an array

[chotu s]

Suppose I have a an array :

val (pf , pfree | p) = array_ptr_tabulate<int> (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

[gmhwxi]

See:

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

[gmhwxi]

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.

[Brandon Barker]

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

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