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

check :: IBool -> Cond

Checkable a boolean expression.

checkStored :: forall ref s a. (IvoryVar a, IvoryRef ref, IvoryVar (ref s (Stored a))) => ref s (Stored a) -> (a -> IBool) -> 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 :: IvoryType r => c -> Body r -> Body r

Instances

Requires IBool

Requires Cond

requires' :: (Requires c, IvoryType r) => (c -> Cond) -> c -> Body r -> Body 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 :: IvoryVar r => (r -> c) -> Body r -> Body r

Instances

Ensures IBool

Ensures Cond

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