module MemoryState where
import Monad(liftM)
import Memories
import MemMonads
import State


instance MemMonad (StateM Memory) Addr Word where
  rd a = liftM (\m -> lookupM m a) load
  wr a w = update (updateM a w)

mallocM n = st (malloc n)
freeM r = st (\m->((),free r m))

{-P:
property RelatedResult range =
  {| r1,r2 | {fst r1}==={fst r2} /\ EqRange range {snd r1} {snd r2} |}


property MostlyStateIndependent range =
  {| m | All mem1 . All mem2 . 
         EqRange range mem1 mem2 ==>
         RelatedResult range {runS m mem1} {runS m mem2} |}

assert ReturnS_MSI = {-#cert:ReturnS_MSI#-}
   All range . All x . MostlyStateIndependent range {return x}

assert BindS_MSI = {-#cert:BindS_MSI#-}
   All m1 . All xm2 . All range .
   MostlyStateIndependent range m1 ==>
   (All x . MostlyStateIndependent range {xm2 x}) ==>
   MostlyStateIndependent range {m1 >>= xm2}
-}