module Ivory.Language.Cond where
import Ivory.Language.Area
import Ivory.Language.IBool
import Ivory.Language.Monad
import Ivory.Language.Proc
import Ivory.Language.Proxy
import Ivory.Language.Ref
import Ivory.Language.Type
import qualified Ivory.Language.Syntax as I
import Data.Monoid(Monoid(..))
emitPreCond :: I.Require -> Ivory eff ()
emitPreCond r = emits mempty { blockRequires = [r] }
emitPostCond :: I.Ensure -> Ivory eff ()
emitPostCond e = emits mempty { blockEnsures = [e] }
newtype Cond = Cond
{ runCond :: forall eff. Ivory eff I.Cond
}
check :: IBool -> Cond
check bool = Cond (return (I.CondBool (unwrapExpr bool)))
checkStored :: forall ref s a.
(IvoryVar a, IvoryRef ref, IvoryVar (ref s (Stored a)))
=> ref s (Stored a) -> (a -> IBool) -> Cond
checkStored ref prop = Cond $ do
n <- freshVar "pre"
let ty = ivoryType (Proxy :: Proxy a)
b <- runCond $ check $ prop $ wrapVar n
return (I.CondDeref ty (unwrapExpr ref) n b)
class Requires c where
requires :: IvoryType r => c -> Body r -> Body r
requires' :: (Requires c, IvoryType r) => (c -> Cond) -> c -> Body r -> Body r
requires' chk prop b = Body $ do
req <- runCond $ chk $ prop
emitPreCond (I.Require req)
runBody b
instance Requires IBool where
requires = requires' check
instance Requires Cond where
requires = requires' id
class Ensures c where
ensures :: IvoryVar r => (r -> c) -> Body r -> Body r
ensures' :: (Ensures c, IvoryVar r)
=> (c -> Cond) -> (r -> c) -> Body r -> Body r
ensures' chk prop b = Body $ do
c <- runCond $ chk $ prop $ wrapVar I.retval
emitPostCond (I.Ensure c)
runBody b
instance Ensures IBool where
ensures = ensures' check
instance Ensures Cond where
ensures = ensures' id