val varrayp_sel
  (#elt: Type) (a: array elt) (p: P.perm)
: Tot (selector (Seq.lseq elt (length a)) (varrayp_hp a p))
let varrayp_sel a p = mk_selector_vprop_sel _ (pts_to'_inj a p)
val varrayp_sel
  (#elt: Type) (a: array elt) (p: P.perm)
: Tot (selector (Seq.lseq elt (length a)) (varrayp_hp a p))
let varrayp_sel a p =
mk_selector_vprop_sel _ (pts_to'_inj a p)
Steel.Array.fst.checked
prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked
Steel.Array.fst
Steel.ST.Array.array Steel.FractionalPermission.perm Steel.Effect.Atomic.mk_selector_vprop_sel FStar.Seq.Properties.lseq Steel.ST.Array.length Steel.Array.pts_to' Steel.Array.pts_to'_inj Steel.Effect.Common.selector Steel.Array.varrayp_hp
(*
   Copyright 2020, 2021, 2022 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 Steel.Array

/// Definition of the selector and its vprop

let pts_to' // necessary because of the selector return type
  (#elt: Type0) (a: array elt)
  (p: P.perm)
  (s: Seq.lseq elt (length a))
: Tot vprop
= pts_to a p s

let pts_to'_inj
  (#elt: Type0) (a: array elt)
  (p: P.perm)
: Tot (interp_hp_of_injective (pts_to' a p))
= fun x1 x2 m -> pts_to_inj a p x1 p x2 m

// _hp and _sel are declared in the interface so that
// [@@__steel_reduce__] gives users the selector return type by
// normalization. Alternatively, we could define varrayp directly with
// mk_selector_vprop in the interface, but to strengthen the selector
// return type, we would then need to declare pts_to' and pts_to'_inj
// in the interface.
val varrayp_sel
  (#elt: Type) (a: array elt) (p: P.perm)
: Tot (selector (Seq.lseq elt (length a)) (varrayp_hp a p))
a: Steel.ST.Array.array elt -> p: Steel.FractionalPermission.perm
  -> Steel.Effect.Common.selector (FStar.Seq.Properties.lseq elt (Steel.ST.Array.length a))
      (Steel.Array.varrayp_hp a p)