Array slice

Google Group
1

Sure. I describe an unsafe approach as follows. A safe one is
just the unsafe one plus some proofs.

val p0 = arrayref2ptr(A) // $UN.cast{ptr}(A)
val p1 = ptr_succ (p0, ofs)
val (pf, fpf | p1) = $UN.ptr_vtake{@[T][nelement]}(p1)

Then !p1 is the left-value your need.On Saturday, October 24, 2015 at 3:47:56 PM UTC-4, Barry Schwartz wrote:

Is there a way to make a left-value out of a slice of an array
(arrayref, arrayptr, @, etc.)?

2

A single-page version of the Intro-to-ATS book (htmlone):

http://www.ats-lang.org/Documents.html#INT2PROGINATSOn Sat, Oct 24, 2015 at 4:41 PM, Barry Schwartz < chemoe...@chemoelectric.org> wrote:

gmhwxi gmh...@gmail.com skribis:

Sure. I describe an unsafe approach as follows. A safe one is
just the unsafe one plus some proofs.

val p0 = arrayref2ptr(A) // $UN.cast{ptr}(A)
val p1 = ptr_succ (p0, ofs)
val (pf, fpf | p1) = $UN.ptr_vtake{@[T][nelement]}(p1)

Then !p1 is the left-value your need.

On Saturday, October 24, 2015 at 3:47:56 PM UTC-4, Barry Schwartz wrote:

Is there a way to make a left-value out of a slice of an array
(arrayref, arrayptr, @, etc.)?

That has the kinds of elements I figured would be involved but putting
them together, not so much.

The book would be much easier for me BTW if it came in a single-page
version (such as one can get optionally with Texinfo). Then browser
‘find in page’ functions work. Also then it can easily be downloaded
for offline use.

–
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/20151024204117.GB4770%40crud
.

3

Here is some code showing how to get a segment as a left-value from an
array:

https://github.com/githwxi/ATS-Postiats-test/blob/master/contrib/hwxi/TEST20/test24.datsOn Sat, Oct 24, 2015 at 4:41 PM, Barry Schwartz < chemoe...@chemoelectric.org> wrote:

gmhwxi gmh...@gmail.com skribis:

Sure. I describe an unsafe approach as follows. A safe one is
just the unsafe one plus some proofs.

val p0 = arrayref2ptr(A) // $UN.cast{ptr}(A)
val p1 = ptr_succ (p0, ofs)
val (pf, fpf | p1) = $UN.ptr_vtake{@[T][nelement]}(p1)

Then !p1 is the left-value your need.

On Saturday, October 24, 2015 at 3:47:56 PM UTC-4, Barry Schwartz wrote:

Is there a way to make a left-value out of a slice of an array
(arrayref, arrayptr, @, etc.)?

That has the kinds of elements I figured would be involved but putting
them together, not so much.

The book would be much easier for me BTW if it came in a single-page
version (such as one can get optionally with Texinfo). Then browser
‘find in page’ functions work. Also then it can easily be downloaded
for offline use.

–
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/20151024204117.GB4770%40crud
.