unbound-0.4.2: Generic support for programming with names and binders

Portabilityunportable (GHC 7 only)
Stabilityexperimental
MaintainerBrent Yorgey <byorgey@cis.upenn.edu>
Safe HaskellNone

Unbound.LocallyNameless.Fresh

Contents

Description

The Fresh and LFresh classes, which govern monads with fresh name generation capabilities, and the FreshM(T) and LFreshM(T) monad (transformers) which provide useful default implementations.

Synopsis

The Fresh class

class Monad m => Fresh m whereSource

The Fresh type class governs monads which can generate new globally unique Names based on a given Name.

Methods

fresh :: Name a -> m (Name a)Source

Generate a new globally unique name based on the given one.

Instances

Fresh m => Fresh (ListT m) 
Fresh m => Fresh (MaybeT m) 
Fresh m => Fresh (IdentityT m) 
Monad m => Fresh (FreshMT m) 
Fresh m => Fresh (ContT r m) 
(Error e, Fresh m) => Fresh (ErrorT e m) 
Fresh m => Fresh (ReaderT r m) 
Fresh m => Fresh (StateT s m) 
Fresh m => Fresh (StateT s m) 
(Monoid w, Fresh m) => Fresh (WriterT w m) 
(Monoid w, Fresh m) => Fresh (WriterT w m) 

type FreshM = FreshMT IdentitySource

A convenient monad which is an instance of Fresh. It keeps track of a global index used for generating fresh names, which is incremented every time fresh is called.

runFreshM :: FreshM a -> aSource

Run a FreshM computation (with the global index starting at zero).

contFreshM :: FreshM a -> Integer -> aSource

Run a FreshM computation given a starting index.

newtype FreshMT m a Source

The FreshM monad transformer. Keeps track of the lowest index still globally unused, and increments the index every time it is asked for a fresh name.

Constructors

FreshMT 

Fields

unFreshMT :: StateT Integer m a
 

runFreshMT :: Monad m => FreshMT m a -> m aSource

Run a FreshMT computation (with the global index starting at zero).

contFreshMT :: Monad m => FreshMT m a -> Integer -> m aSource

Run a FreshMT computation given a starting index for fresh name generation.

The LFresh class

class Monad m => LFresh m whereSource

This is the class of monads that support freshness in an (implicit) local scope. Generated names are fresh for the current local scope, not necessarily globally fresh.

Methods

lfresh :: Rep a => Name a -> m (Name a)Source

Pick a new name that is fresh for the current (implicit) scope.

avoid :: [AnyName] -> m a -> m aSource

Avoid the given names when freshening in the subcomputation, that is, add the given names to the in-scope set.

getAvoids :: m (Set AnyName)Source

Get the set of names currently being avoided.

Instances

LFresh m => LFresh (ListT m) 
LFresh m => LFresh (MaybeT m) 
LFresh m => LFresh (IdentityT m) 
Monad m => LFresh (LFreshMT m) 
LFresh m => LFresh (ContT r m) 
(Error e, LFresh m) => LFresh (ErrorT e m) 
LFresh m => LFresh (ReaderT r m) 
LFresh m => LFresh (StateT s m) 
LFresh m => LFresh (StateT s m) 
(Monoid w, LFresh m) => LFresh (WriterT w m) 
(Monoid w, LFresh m) => LFresh (WriterT w m) 

type LFreshM = LFreshMT IdentitySource

A convenient monad which is an instance of LFresh. It keeps track of a set of names to avoid, and when asked for a fresh one will choose the first unused numerical name.

runLFreshM :: LFreshM a -> aSource

Run a LFreshM computation in an empty context.

contLFreshM :: LFreshM a -> Set AnyName -> aSource

Run a LFreshM computation given a set of names to avoid.

newtype LFreshMT m a Source

The LFresh monad transformer. Keeps track of a set of names to avoid, and when asked for a fresh one will choose the first numeric prefix of the given name which is currently unused.

Constructors

LFreshMT 

Fields

unLFreshMT :: ReaderT (Set AnyName) m a
 

runLFreshMT :: LFreshMT m a -> m aSource

Run an LFreshMT computation in an empty context.

contLFreshMT :: LFreshMT m a -> Set AnyName -> m aSource

Run an LFreshMT computation given a set of names to avoid.