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

Defined in Ivory.Language.Cond

Methods

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

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

Requires Cond

Defined in Ivory.Language.Cond

Methods

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

CheckStored Cond

Defined in Ivory.Language.Cond

Methods

checkStored :: (IvoryVar a, IvoryRef ref, IvoryVar (ref s (Stored a))) => ref s (Stored a) -> (a -> Cond) -> 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

Defined in Ivory.Language.Cond

Methods

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

CheckStored Cond

Defined in Ivory.Language.Cond

Methods

checkStored :: (IvoryVar a, IvoryRef ref, IvoryVar (ref s (Stored a))) => ref s (Stored a) -> (a -> Cond) -> 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

Defined in Ivory.Language.Cond

Methods

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

Requires Cond

Defined in Ivory.Language.Cond

Methods

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

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

Defined in Ivory.Language.Cond

Methods

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

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

Ensures Cond

Defined in Ivory.Language.Cond

Methods

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

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

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 ()