val heap_rel : h0: MRefHeap.heap -> h1: MRefHeap.heap -> Prims.logical
let heap_rel (h0:heap) (h1:heap) =
  (forall a r (m:mref a r) . contains m h0  ==> contains m h1) /\
  (forall a (r:preorder a) (m:mref a r{contains m h0}) . r (sel h0 m) (sel h1 m))
(*
   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 MRefST

open MRefHeap

open FStar.Preorder
open FStar.Monotonic.Witnessed

////////////////////////////////////////////////////////////////////////////////
// In the DM sub-language
////////////////////////////////////////////////////////////////////////////////
(* Define a state monad with the `heap` type as the state *)
let st (a: Type) = heap -> M (a * heap)

val return_st: a:Type -> x:a -> Tot (st a)
let return_st a x = fun s -> x, s

val bind_st: a:Type -> b:Type -> f:st a -> g:(a -> Tot (st b)) -> Tot (st b)
let bind_st a b f g = fun s0 ->
  let tmp = f s0 in
  let x, s1 = tmp in
  g x s1

let get (_:unit): st heap =
  fun x -> x, x

let put (x: heap): st unit =
  fun _ -> (), x

////////////////////////////////////////////////////////////////////////////////
// Instruct F* to CPS and elaborate the terms above to build a new STATE effect
////////////////////////////////////////////////////////////////////////////////

reifiable reflectable total new_effect {
  ISTATE : a:Type -> Effect
  with repr     = st
     ; bind     = bind_st
     ; return   = return_st
     ; get      = get
     ; put      = put
}


(* Swapping the reference and heap arguments of (NatHeap.contains) to
   use it in point-free style in calls to (witness) and (recall). *)

let contains (#a:Type) (#r:preorder a) (m:mref a r) (h:heap) = contains h m

val contains_lemma : #a:Type ->
                     #r:preorder a ->
                     h:heap ->
		     m:mref a r ->
		     Lemma (requires (contains m h))
			   (ensures  (MRefHeap.contains h m))
		     [SMTPat (contains m h)]
let contains_lemma #a #r h m = ()


(* Relating two heaps using the preorders associated with allocated monotonic references. *)
/
prims.fst.checked MRefHeap.fsti.checked FStar.Preorder.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Monotonic.Witnessed.fsti.checked
MRefST.fst
h0: MRefHeap.heap -> h1: MRefHeap.heap -> Prims.logical
MRefHeap.heap Prims.l_and Prims.l_Forall MRefHeap.preorder_t MRefHeap.mref Prims.l_imp MRefST.contains FStar.Preorder.preorder MRefHeap.sel Prims.logical
let heap_rel (h0 h1: heap) =
  
(forall a r (m: mref a r). contains m h0 ==> contains m h1) /\
(forall a (r: preorder a) (m: mref a r {contains m h0}). r (sel h0 m) (sel h1 m))