content: {-@ LIQUID "--expect-any-error" @-}
  module RG where
  
  import Data.IORef as R
  
  {- Liquid Rely-Guarantee References / RG-Haskell
  
     This is an embedding of a slightly simplified rely-guarantee reference system.
     (See "Rely-Guarantee References for Refinement Types over Aliased Mutable Data,"
     by Gordon, Ernst, and Grossman, PLDI'13.  I promise to never use such a long paper
     title ever again.)
  
     The key idea in that paper is to augment each reference with a predicate refining
     the referent and heap reachable from it, and binary relations describing permitted
     local actions (the guarantee) and possible remote actions (the rely):
  
                  ref{T|P}[R,G]
  
     The terminology comes from rely-guarantee reasoning, from the concurrent program
     logic literature.  As long as
     each reference's guarantee relation is a subrelation of any alias's rely (plus some
     subtle side conditions about nested references), any predicate P that is /stable/
     with respect to a rely R on a given reference (forall x y, P x -> R x y -> P y)
     is trivially preserved by any update through an alias that respects that alias's
     guarantee relation.
  
     Embedding into Liquid Haskell instead of Coq requires a few weakenings of the
     original design, so we lose expressiveness but gain substantially from automation
     and being a refinement of a language with real programs!  The main simplifications are:
      - TEMPORARILY, rely and guarantee are the same, until we get rolling.  In general,
        we must always have that the guarantee implies the rely, since Haskell wouldn't
        respect the substructural restrictions.  Leaving them the same makes weakening the
        guarantee unsound, so we should fix this soon.
      - Predicates and relations can refer only to the immediate referent for now.
      - Folding (pushing a local restriction through to new references reached via
        dereference) doesn't exist in this system, mostly because all predicates and
        relations can restrict only one cell.
  
  -}
  
  {- We wrap IORefs in a new constructor to add ghost parameters for the predicate and
     relation(s).  It is a standard GHC optimization to eliminate the overhead since there is a single
     constructor with one physical argument, so at runtime these will look the same as IORefs:
     we won't pay time or space overhead. -}
  {-@ data RGRef a <p :: a -> Bool, r :: a -> a -> Bool>
  	= Wrap { rr :: IORef a<p> } @-}
  data RGRef a = Wrap (R.IORef a)
  
  {- A stability proof can be embedded into LH as a function of type:
      x:a<p> -> y:a<r x> -> {v:a<p> | v = y}
      This encodes the requirement that knowing P x and R x y is sufficient to deduce P y.
  -}
  -- Requires explicit type anno for LH type to refine the inferred Haskell type
  {-@ stable_monocount :: x:{v:Int | v > 0 } -> y:{v:Int | x <= v } -> {v:Int | ((v = y) && (v > 0)) } @-}
  stable_monocount :: Int -> Int -> Int
  stable_monocount x y = y
  
  -- Testing / debugging function
  {-@ generic_accept_stable :: forall <p :: a -> Bool, r :: a -> a -> Bool >.
                      f:(x:a<p> -> y:a<r x> -> {v:a<p> | (v = y)}) ->
                      ()
                      @-}
  generic_accept_stable :: (a -> a -> a) -> ()
  generic_accept_stable pf = ()
  
  {-@ proves_reflexivity :: x:{v:Int | v > 0} -> y:{v:Int | v > 0} -> {v:Int | v > 0} @-}
  proves_reflexivity :: Int -> Int -> Int
  proves_reflexivity x y = x
  
  test :: ()
  test = generic_accept_stable proves_reflexivity
  
  {-@ proves_nothing :: x:a -> y:a -> {v:a | (v = y)} @-}
  proves_nothing :: a -> a -> a
  proves_nothing x y = y --proves_nothing x y
  
  {- TODO: e2 is a hack to sidestep the inference of false for r,
     it forces r to be inhabited. -}
  {-@ newRGRef :: forall <p :: a -> Bool, r :: a -> a -> Bool >.
                      e:a<p> ->
                      e2:a<r e> ->
                      f:(x:a<p> -> y:a<r x> -> {v:a<p> | (v = y)}) ->
                      IO (RGRef <p, r> a) @-}
  newRGRef :: a -> a -> (a -> a -> a) -> IO (RGRef a)
  newRGRef e e2 stabilityPf = do {
                              r <- newIORef e;
                              return (Wrap r)
                           }
  
  -- LH's assume statement seems to only affect spec files
  {-@ readRGRef :: forall <p :: a -> Bool, r :: a -> a -> Bool >.
                      RGRef<p, r> a -> IO (a<p>) @-}
  readRGRef (Wrap x) = readIORef x
  
  -- TODO: full spec, fix pf type
  writeRGRef :: RGRef a -> a -> (a -> a -> Bool) -> IO ()
  writeRGRef  (Wrap x) e pf = writeIORef x e
  
  
  {- modifyRGRef :: forall <p :: a -> Bool, r :: a -> a -> Bool >.
                      r:(RGRef<p, r> a) ->
                      f:(x:a<p> -> a<r x>) ->
                      pf:(x:a<p> -> y:a<r x> -> {v:a<p> | (v = y)}) ->
                      IO () @-}
  modifyRGRef :: RGRef a -> (a -> a) -> (a -> a -> a) -> IO ()
  modifyRGRef (Wrap x) f pf = modifyIORef x (\ v -> pf v (f v))
  --
  --{- modifyRGRef' :: forall <p :: a -> Bool, r :: a -> a -> Bool >.
  --                    RGRef<p, r> a ->
  --                    f:(x:a<p> -> a<r x>) ->
  --                    IO () @-}
  ---- TODO: strictify, so we don't de-optimize modifyIORef' calls
  --modifyRGRef' (Wrap x) f = modifyIORef x f
  --
  --
  main = do {
            r <- newRGRef 1 3 stable_monocount; -- SHOULD BE ref{Int|>0}[<=,<=]
            -- Instead we get ref{Int|>0}[false,false] !
            r2 <- newRGRef 2 9 proves_nothing;  -- SHOULD BE ref{Int|>0}[havoc,havoc].
            -- Instead we get ref{Int|>0}[false,false] !
            --r3 <- newRGRef 3 10 proves_reflexivity; -- BAD, correctly rejected
            return ()
         }
  
  
  -- What are the subtyping rules for data structure params that aren't
  -- used within the structure?
  {-@ unused_contra :: RGRef <{\x -> x > 0}, {\x y -> x <= y}> Int -> RGRef <{\x -> x > 0}, {\x y -> false}> Int @-}
  unused_contra :: RGRef Int -> RGRef Int
  unused_contra r = r
  
  
  {-@ unused_covar :: RGRef <{\x -> x > 0}, {\x y -> false}> Int -> RGRef <{\x -> x > 0}, {\x y -> x <= y}> Int @-}
  unused_covar :: RGRef Int -> RGRef Int
  unused_covar r = r
  -- It looks like there's simply no constraint!
  