val rs_elems_inv:
  #a:Type0 -> #rst:Type -> rg:regional rst a ->
  h:HS.mem -> rs:S.seq a ->
  i:nat -> j:nat{i <= j && j <= S.length rs} ->
  GTot Type0
let rs_elems_inv #a #rst rg h rs i j =
  V.forall_seq rs i j (rg_inv rg h)
val rs_elems_inv:
  #a:Type0 -> #rst:Type -> rg:regional rst a ->
  h:HS.mem -> rs:S.seq a ->
  i:nat -> j:nat{i <= j && j <= S.length rs} ->
  GTot Type0
let rs_elems_inv #a #rst rg h rs i j =
V.forall_seq rs i j (rg_inv rg h)
LowStar.RVector.fst.checked
prims.fst.checked LowStar.Vector.fst.checked LowStar.Regional.fst.checked LowStar.Modifies.fst.checked LowStar.Buffer.fst.checked FStar.UInt32.fsti.checked FStar.Set.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Map.fsti.checked FStar.Integers.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked FStar.Classical.fsti.checked
LowStar.RVector.fst
LowStar.Regional.regional FStar.Monotonic.HyperStack.mem FStar.Seq.Base.seq FStar.Integers.nat Prims.b2t Prims.op_AmpAmp FStar.Integers.op_Less_Equals FStar.Integers.Signed FStar.Integers.Winfinite FStar.Seq.Base.length LowStar.Vector.forall_seq LowStar.Regional.rg_inv
(*
   Copyright 2008-2018 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)

module LowStar.RVector

open FStar.Classical
open FStar.Integers
open LowStar.Modifies
open LowStar.Regional
open LowStar.Vector

module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST
module S = FStar.Seq
module B = LowStar.Buffer
module V = LowStar.Vector

module U32 = FStar.UInt32

/// Utilities

/// A `regional` type `a` is also `copyable` when there exists a copy operator
/// that guarantees the same representation between `src` and `dst`.
/// For instance, the `copy` operation for `B.buffer a` is `B.blit`.
///
/// Here, no reference at run-time is kept to the state argument of the
/// regional; conceivably, the caller will already have some reference handy to
/// the instance of the regional class and can retrieve the parameter from
/// there.
inline_for_extraction
noeq type copyable (#rst:Type) (a:Type0) (rg:regional rst a) =
| Cpy:
    copy: (s:rst{s==Rgl?.state rg} -> src:a -> dst:a ->
      HST.ST unit
        (requires (fun h0 ->
          rg_inv rg h0 src /\ rg_inv rg h0 dst /\
          HS.disjoint (Rgl?.region_of rg src)
                      (Rgl?.region_of rg dst)))
        (ensures (fun h0 _ h1 ->
          modifies (loc_all_regions_from
                     false (Rgl?.region_of rg dst)) h0 h1 /\
          rg_inv rg h1 dst /\
          Rgl?.r_repr rg h1 dst == Rgl?.r_repr rg h0 src))) ->
    copyable a rg

// rst: regional state
type rvector (#a:Type0) (#rst:Type) (rg:regional rst a) = V.vector a

val loc_rvector:
  #a:Type0 -> #rst:Type -> #rg:regional rst a -> rv:rvector rg -> GTot loc
let loc_rvector #a #rst #rg rv =
  loc_all_regions_from false (V.frameOf rv)

/// The invariant of `rvector`
// Here we will define the invariant for `rvector #a` that contains
// the invariant for each element and some more about the vector itself.

val rs_elems_inv:
  #a:Type0 -> #rst:Type -> rg:regional rst a ->
  h:HS.mem -> rs:S.seq a ->
  i:nat -> j:nat{i <= j && j <= S.length rs} ->
  GTot Type0
val rs_elems_inv:
  #a:Type0 -> #rst:Type -> rg:regional rst a ->
  h:HS.mem -> rs:S.seq a ->
  i:nat -> j:nat{i <= j && j <= S.length rs} ->
  GTot Type0

    rg: LowStar.Regional.regional rst a ->
    h: FStar.Monotonic.HyperStack.mem ->
    rs: FStar.Seq.Base.seq a ->
    i: FStar.Integers.nat ->
    j: FStar.Integers.nat{i <= j && j <= FStar.Seq.Base.length rs}
  -> Prims.GTot Type0