val ptr_sel (#a: Type0) (r: ref a) : selector a (ptr r)
val ptr_sel (#a: Type0) (r: ref a) : selector a (ptr r)
let ptr_sel (#a:Type0) (r:ref a) : selector a (ptr r) = ptrp_sel r full_perm
module Steel.ArrayRef

open Steel.FractionalPermission
open Steel.Memory
open Steel.Effect.Common
open Steel.Effect
open Steel.Effect.Atomic

module A = Steel.Array

(** This module provides the same interface as Steel.Reference, however, it builds on top
    of Steel.Array to enable the interoperation between arrays and references.
    Similarly to C, a reference is defined as an array of length 1 *)

/// An abstract datatype for references
inline_for_extraction
let ref (a : Type0) : Type0 = (r: A.array a { A.length r == 1 \/ r == A.null })

/// The null pointer
[@@ noextract_to "krml"]
inline_for_extraction
val null (#a:Type0) : ref a

/// Checking whether a pointer is null can be done in a decidable way
[@@ noextract_to "krml"]
inline_for_extraction
val is_null (#a:Type0) (r:ref a) : (b:bool{b <==> r == null})

/// An abstract separation logic predicate stating that reference [r] is valid in memory.

val ptrp (#a:Type0) (r:ref a) ([@@@smt_fallback] p: perm) : slprop u#1

[@@ __steel_reduce__; __reduce__]
unfold
let ptr (#a:Type0) (r:ref a) : slprop u#1 = ptrp r full_perm

/// A selector for references, returning the value of type [a] stored in memory

val ptrp_sel (#a:Type0) (r:ref a) (p: perm) : selector a (ptrp r p)

[@@ __steel_reduce__; __reduce__]
/
Steel.Memory.fsti.checked Steel.FractionalPermission.fst.checked Steel.Effect.Common.fsti.checked Steel.Effect.Atomic.fsti.checked Steel.Effect.fsti.checked Steel.Array.fsti.checked prims.fst.checked FStar.Tactics.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
Steel.ArrayRef.fsti
r: Steel.ArrayRef.ref a -> Steel.Effect.Common.selector a (Steel.ArrayRef.ptr r)
Steel.ArrayRef.ref Steel.ArrayRef.ptrp_sel Steel.FractionalPermission.full_perm Steel.Effect.Common.selector Steel.ArrayRef.ptr
let ptr_sel (#a: Type0) (r: ref a) : selector a (ptr r) =
  
ptrp_sel r full_perm