tamarin-prover-utils-0.8.5.0: Utility library for the tamarin prover.

PortabilityGHC only
MaintainerSimon Meier <iridcode@gmail.com>
Safe HaskellNone

Control.Monad.Fresh

Contents

Description

Computations that need a fresh name supply.

Synopsis

MonadFresh class

class (Applicative m, Monad m) => MonadFresh m whereSource

Methods

freshIdentSource

Arguments

:: String

Desired name

-> m Integer 

Get the integer of the next fresh identifier of this name.

freshIdentsSource

Arguments

:: Integer

Number of desired fresh identifiers.

-> m Integer

The first Fresh identifier.

Get a number of fresh identifiers. This reserves the required number of identifiers on all names.

scopeFreshness :: m a -> m aSource

Scope the freshIdent and freshIdents requests such that these variables are not marked as used once the scope is left.

The Fresh monad

runFresh :: Fresh a -> FreshState -> (a, FreshState)Source

Run a computation with a fresh name supply.

evalFresh :: Fresh a -> FreshState -> aSource

Evaluate a computation with a fresh name supply.

execFresh :: Fresh a -> FreshState -> FreshStateSource

Execute a computation with a fresh name supply.

The fast FreshT monad transformer

newtype FreshT m a Source

A computation that can generate fresh variables from name hints.

Constructors

FreshT 

Fields

unFreshT :: StateT FreshState m a
 

freshT :: (FreshState -> m (a, FreshState)) -> FreshT m aSource

Construct a FreshT action from a FreshState modification.

runFreshT :: FreshT m a -> FreshState -> m (a, FreshState)Source

Run a computation with a fresh name supply.

evalFreshT :: Monad m => FreshT m a -> FreshState -> m aSource

Evaluate a computation with a fresh name supply.

execFreshT :: Monad m => FreshT m a -> FreshState -> m FreshStateSource

Execute a computation with a fresh name supply.

Fresh name generation

type FreshState = IntegerSource

The state of the name supply: the first unused sequence number of every name.

nothingUsed :: FreshStateSource

The empty fresh state.