let as_ref #a (b:buffer a) = as_ref (content b)
let as_ref #a (b: buffer a) =
as_ref (content b)
FStar.Buffer.fst.checked
prims.fst.checked FStar.UInt32.fsti.checked FStar.UInt.fsti.checked FStar.TSet.fsti.checked FStar.Set.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Map.fsti.checked FStar.List.Tot.fst.checked FStar.Int32.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Heap.fst.checked FStar.Ghost.fsti.checked FStar.Classical.fsti.checked
FStar.Buffer.fst
FStar.Buffer.buffer FStar.Monotonic.HyperStack.as_ref FStar.Buffer.lseq FStar.Buffer.max_length FStar.Heap.trivial_preorder FStar.Buffer.content FStar.Monotonic.Heap.mref
(*
   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 FStar.Buffer
 
open FStar.Seq
open FStar.UInt32
module Int32 = FStar.Int32
open FStar.HyperStack
open FStar.HyperStack.ST
open FStar.Ghost


module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST

#set-options "--initial_fuel 0 --max_fuel 0"

//17-01-04 usage? move to UInt? 
let lemma_size (x:int) : Lemma (requires (UInt.size x n))
				     (ensures (x >= 0))
				     [SMTPat (UInt.size x n)]
  = ()

let lseq (a: Type) (l: nat) : Type =
  (s: seq a { Seq.length s == l } )

(* Buffer general type, fully implemented on FStar's arrays *)
noeq private type _buffer (a:Type) =
  | MkBuffer: max_length:UInt32.t
    -> content:reference (lseq a (v max_length))
    -> idx:UInt32.t
    -> length:UInt32.t{v idx + v length <= v max_length}
    -> _buffer a

(* Exposed buffer type *)
type buffer (a:Type) = _buffer a

(* Ghost getters for specifications *)
// TODO: remove `contains` after replacing all uses with `live`
let contains #a h (b:buffer a) : GTot Type0 = HS.contains h b.content
let unused_in #a (b:buffer a) h : GTot Type0 = HS.unused_in b.content h

(* In most cases `as_seq` should be used instead of this one. *)
let sel #a h (b:buffer a) : GTot (seq a) = HS.sel h b.content

let max_length #a (b:buffer a) : GTot nat = v b.max_length
let length #a (b:buffer a) : GTot nat = v b.length
let idx #a (b:buffer a) : GTot nat = v b.idx

//17-01-04 rename to container or ref? 
let content #a (b:buffer a) :
  GTot (reference (lseq a (max_length b))) = b.content
val as_ref : b: FStar.Buffer.buffer a
  -> Prims.GTot
    (FStar.Monotonic.Heap.mref (FStar.Buffer.lseq a (FStar.Buffer.max_length b))
        (FStar.Heap.trivial_preorder (FStar.Buffer.lseq a (FStar.Buffer.max_length b))))
b: FStar.Buffer.buffer a
  -> Prims.GTot
    (FStar.Monotonic.Heap.mref (FStar.Buffer.lseq a (FStar.Buffer.max_length b))
        (FStar.Heap.trivial_preorder (FStar.Buffer.lseq a (FStar.Buffer.max_length b))))