# Array slice

**URL:** <https://discourse.ats-lang.org/t/array-slice/421>\
**Category:** Google Group\
**Created:** [October 24, 2015, 8:16pm UTC](https://discourse.ats-lang.org/t/array-slice/421 "2015-10-24T20:16:05Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [October 24, 2015, 8:16pm UTC](https://discourse.ats-lang.org/t/array-slice/421/1 "2015-10-24T20:16:05Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [October 25, 2015, 4:11am UTC](https://discourse.ats-lang.org/t/array-slice/421/2 "2015-10-25T04:11:54Z")

</div>

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

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

> gmhwxi [gmh...@gmail.com](mailto: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](mailto:ats-lang-user...@googlegroups.com).  
> To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> Visit this group at [http://groups.google.com/group/ats-lang-users](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](https://groups.google.com/d/msgid/ats-lang-users/20151024204117.GB4770%40crud)  
> .

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [October 25, 2015, 5:15am UTC](https://discourse.ats-lang.org/t/array-slice/421/3 "2015-10-25T05:15:43Z")

</div>

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](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](mailto:chemoe...@chemoelectric.org)\> wrote:

> gmhwxi [gmh...@gmail.com](mailto: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](mailto:ats-lang-user...@googlegroups.com).  
> To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> Visit this group at [http://groups.google.com/group/ats-lang-users](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](https://groups.google.com/d/msgid/ats-lang-users/20151024204117.GB4770%40crud)  
> .