let is_strictly_above r1 r2 = r1 `is_above` r2 && r1 <> r2
let is_strictly_above r1 r2 =
r1 `is_above` r2 && r1 <> r2
FStar.Monotonic.HyperStack.fsti.checked
prims.fst.checked FStar.Set.fsti.checked FStar.Preorder.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Monotonic.HyperHeap.fsti.checked FStar.Monotonic.Heap.fsti.checked FStar.Map.fsti.checked
FStar.Monotonic.HyperStack.fsti
FStar.Monotonic.HyperHeap.rid Prims.op_AmpAmp FStar.Monotonic.HyperStack.is_above Prims.op_disEquality Prims.bool
(*
   Copyright 2008-2014 Aseem Rastogi, 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.Monotonic.HyperStack

open FStar.Preorder
module Map = FStar.Map

include FStar.Monotonic.HyperHeap


(****** Some predicates ******)

unfold let is_in (r:rid) (h:hmap) = h `Map.contains` r

let is_stack_region r = color r > 0
let is_heap_color c = c <= 0

[@@(deprecated "FStar.HyperStack.ST.is_eternal_region")]
let is_eternal_region r  = is_heap_color (color r) && not (rid_freeable r)

unfold let is_eternal_region_hs r = is_heap_color (color r) && not (rid_freeable r)

type sid = r:rid{is_stack_region r} //stack region ids

(*
 * AR: marking these unfolds, else I think there are pattern firing issues depending on which one we use
 *)
unfold let is_above r1 r2          = r1 `includes` r2
unfold let is_just_below r1 r2     = r1 `extends`  r2
unfold let is_below r1 r2          = r2 `is_above` r1
val is_strictly_above : r1: FStar.Monotonic.HyperHeap.rid -> r2: FStar.Monotonic.HyperHeap.rid -> Prims.GTot Prims.bool
r1: FStar.Monotonic.HyperHeap.rid -> r2: FStar.Monotonic.HyperHeap.rid -> Prims.GTot Prims.bool