Ivory.Language.Cond

Documentation

emitPreCond :: Require -> Ivory eff ()

Emit a pre-condition.

XXX do not export

emitPostCond :: Ensure -> Ivory eff ()

Emit a post-condition.

XXX do not export

newtype Cond

Constructors

Cond

Fields

runCond :: forall eff. Ivory eff Cond

Use the naming environment from the Ivory monad.

Instances

Ensures Cond

Requires Cond

CheckStored Cond

check :: IBool -> Cond

Checkable a boolean expression.

checkStored' :: forall ref s a c. (CheckStored c, IvoryVar a, IvoryRef ref, IvoryVar (ref s (Stored a))) => (c -> Cond) -> ref s (Stored a) -> (a -> c) -> Cond

class CheckStored c where

Methods

checkStored :: (IvoryVar a, IvoryRef ref, IvoryVar (ref s (Stored a))) => ref s (Stored a) -> (a -> c) -> Cond

Instances

CheckStored IBool

CheckStored Cond

class Requires c where

Proc bodies that have pre-conditions. Multiple pre-conditions may be provided, for which the conjunction must hold.

Methods

requires :: (WrapIvory m, IvoryType r) => c -> m r -> m r

Instances

Requires IBool

Requires Cond

requires' :: (WrapIvory m, Requires c, IvoryType r) => (c -> Cond) -> c -> m r -> m r

class Ensures c where

Proc bodies that have post-conditions. Multiple post-conditions may be provided, for which the conjunction must hold.

Methods

ensures :: (WrapIvory m, IvoryVar r) => (r -> c) -> m r -> m r

ensures_ :: WrapIvory m => c -> m () -> m ()

Instances

Ensures IBool

Ensures Cond

ensures' :: (WrapIvory m, Ensures c, IvoryVar r) => (c -> Cond) -> (r -> c) -> m r -> m r

ensures_' :: (WrapIvory m, Ensures c) => (c -> Cond) -> c -> m () -> m ()