let sel (#a:Type) (#i:rid) (m:t) (r:rref i a) = Heap.sel (Map.sel m i) (as_ref r)
let sel (#a: Type) (#i: rid) (m: t) (r: rref i a) =
Heap.sel (Map.sel m i) (as_ref r)
FStar.TwoLevelHeap.fst.checked
prims.fst.checked FStar.Set.fsti.checked FStar.Pervasives.fsti.checked FStar.Map.fsti.checked FStar.Heap.fst.checked
FStar.TwoLevelHeap.fst
FStar.TwoLevelHeap.rid FStar.TwoLevelHeap.t FStar.TwoLevelHeap.rref FStar.Monotonic.Heap.sel FStar.Heap.trivial_preorder FStar.Map.sel FStar.Monotonic.Heap.heap FStar.TwoLevelHeap.as_ref
(*
   Copyright 2008-2014 Nikhil Swamy and 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.TwoLevelHeap
open FStar.Map
open FStar.Heap
type rid = int  //region id
type t = Map.t rid heap

let st_pre = st_pre_h t
let st_post' (a:Type) (pre:Type) = st_post_h' t a pre
let st_post  (a:Type) = st_post_h t a
let st_wp (a:Type) = st_wp_h t a
new_effect STATE = STATE_h t
effect State (a:Type) (wp:st_wp a) =
       STATE a wp
effect ST (a:Type) (pre:st_pre) (post: (h0:t -> Tot (st_post' a (pre h0)))) =
       STATE a
             (fun (p:st_post a) (h:t) -> pre h /\ (forall a h1. pre h /\ post h a h1 ==> p a h1)) (* WP *)
effect St (a:Type) =
       ST a (fun h -> True) (fun h0 r h1 -> True)
sub_effect
  DIV   ~> STATE = fun (a:Type) (wp:pure_wp a) (p:st_post a) (h:t) -> wp (fun a -> p a h)

type rref (id:rid) (a:Type) = ref a
val as_ref : #a:Type -> #id:rid -> r:rref id a -> Tot (ref a)
let as_ref #a #id r = r

private val ref_as_rref : #a:Type -> i:rid -> r:ref a -> Tot (rref i a)
let ref_as_rref #a i r = r

val lemma_as_ref_inj: #a:Type -> #i:rid -> r:rref i a
    -> Lemma (requires (True))
             (ensures ((ref_as_rref i (as_ref r) == r)))
       [SMTPat (as_ref r)]
let lemma_as_ref_inj #a #i r = ()

assume val new_region: unit -> ST rid
      (requires (fun m -> True))
      (ensures (fun (m0:t) (id:rid) (m1:t) -> exists (h:heap). not(Map.contains m0 id) /\ m1==Map.upd m0 id h))
val sel : m: FStar.TwoLevelHeap.t -> r: FStar.TwoLevelHeap.rref i a -> Prims.GTot a
m: FStar.TwoLevelHeap.t -> r: FStar.TwoLevelHeap.rref i a -> Prims.GTot a