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

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

Control.Monad.Trans.FastFresh

Contents

Description

A monad transformer for passing a fast fresh name supply through a computation. It uses an Integer counter to determine the next free name.

Modeled after the mtl-2.0 library.

Synopsis

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

Instances

MonadTrans FreshT 
MonadBind k v m => MonadBind k v (FreshT m) 
MonadError e m => MonadError e (FreshT m) 
MonadReader r m => MonadReader r (FreshT m) 
MonadState s m => MonadState s (FreshT m) 
Monad m => Monad (FreshT m) 
Functor m => Functor (FreshT m) 
MonadPlus m => MonadPlus (FreshT m) 
(Monad m, Functor m) => Applicative (FreshT m) 
(Functor m, MonadPlus m) => Alternative (FreshT m) 
(Functor m, Monad m) => MonadFresh (FreshT m) 
MonadDisj m => MonadDisj (FreshT m) 

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.

freshIdentsSource

Arguments

:: Monad m 
=> Integer

number of desired identifiers

-> FreshT m Integer

The first fresh identifier.

Get k fresh identifiers.

scopeFreshness :: Monad m => FreshT m a -> FreshT m aSource

Restrict the scope of the freshness requests.