scyther-proof-0.3.0: Automatic generation of Isabelle/HOL correctness proofs for security protocols.

Control.Monad.Label

Description

A monad supporting labeling of values and a monad transformer supporting the consistent labeling of keys.

TODO: Split module into transformer part and type class instance part along the lines of the transformers package.

Synopsis

Documentation

class (Applicative m, Monad m) => MonadLabel k l m whereSource

A monad allowing for labelling keys.

Methods

label :: k -> m lSource

Instances

MonadLabel k l m => MonadLabel k l (ReaderT r m) 
MonadLabel k l m => MonadLabel k l (StateT s m) 
(Ord k, Applicative m, Monad m) => MonadLabel k l (ConsistentLabelsT k l m) 

newtype ConsistentLabelsT k l m a Source

A monad transformer implementing consistent (equal keys get equal labels) labeling of keys with a sequence of labels.

Constructors

ConsistentLabelsT 

Fields

unConsistentLabelsT :: StateT ([l], Map k l) m a
 

runConsistentLabelsT :: ConsistentLabelsT k l m a -> [l] -> m (a, ([l], Map k l))Source

Run a computation requiring consistent labels.

evalConsistentLabelsT :: Functor m => ConsistentLabelsT k l m a -> [l] -> m aSource

Evaluate a computation requiring consistent labels.

execConsistentLabelsT :: Functor m => ConsistentLabelsT k l m a -> [l] -> m ([l], Map k l)Source

Execute a computation requiring consistent labels.

runConsistentLabels :: ConsistentLabels k l a -> [l] -> (a, ([l], Map k l))Source

Run a computation requiring consistent labels.

evalConsistentLabels :: ConsistentLabels k l a -> [l] -> aSource

Evaluate a computation requiring consistent labels.

execConsistentLabels :: ConsistentLabels k l a -> [l] -> ([l], Map k l)Source

Execute a computation requiring consistent labels.