Copyright	(c) 2011 Stephanie Weirich
License	BSD3 (See LFresh.hs)
Maintainer	Aleksey Kliger
Stability	experimental
Safe Haskell	None
Language	Haskell2010
Extensions	Cpp UndecidableInstances StandaloneDeriving TypeSynonymInstances FlexibleInstances ConstrainedClassMethods MultiParamTypeClasses GeneralizedNewtypeDeriving

Unbound.Generics.LocallyNameless.LFresh

Contents

The LFresh class

Description

Local freshness monad.

Synopsis

class Monad m => LFresh (m :: Type -> Type) where
- lfresh :: Typeable a => Name a -> m (Name a)
- avoid :: [AnyName] -> m a -> m a
- getAvoids :: m (Set AnyName)
type LFreshM = LFreshMT Identity
runLFreshM :: LFreshM a -> a
contLFreshM :: LFreshM a -> Set AnyName -> a
newtype LFreshMT (m :: Type -> Type) a = LFreshMT {
- unLFreshMT :: ReaderT (Set AnyName) m a
}
runLFreshMT :: LFreshMT m a -> m a
contLFreshMT :: LFreshMT m a -> Set AnyName -> m a

The `LFresh` class

class Monad m => LFresh (m :: Type -> Type) where Source #

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 :: Typeable a => Name a -> m (Name a) Source #

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

avoid :: [AnyName] -> m a -> m a Source #

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

Instances details

LFresh m => LFresh (MaybeT m) Source #
Instance details Defined in Unbound.Generics.LocallyNameless.LFresh Methods lfresh :: Typeable a => Name a -> MaybeT m (Name a) Source # avoid :: [AnyName] -> MaybeT m a -> MaybeT m a Source # getAvoids :: MaybeT m (Set AnyName) Source #
Monad m => LFresh (LFreshMT m) Source #
Instance details Defined in Unbound.Generics.LocallyNameless.LFresh Methods lfresh :: Typeable a => Name a -> LFreshMT m (Name a) Source # avoid :: [AnyName] -> LFreshMT m a -> LFreshMT m a Source # getAvoids :: LFreshMT m (Set AnyName) Source #
LFresh m => LFresh (ExceptT e m) Source #
Instance details Defined in Unbound.Generics.LocallyNameless.LFresh Methods lfresh :: Typeable a => Name a -> ExceptT e m (Name a) Source # avoid :: [AnyName] -> ExceptT e m a -> ExceptT e m a Source # getAvoids :: ExceptT e m (Set AnyName) Source #
LFresh m => LFresh (IdentityT m) Source #
Instance details Defined in Unbound.Generics.LocallyNameless.LFresh Methods lfresh :: Typeable a => Name a -> IdentityT m (Name a) Source # avoid :: [AnyName] -> IdentityT m a -> IdentityT m a Source # getAvoids :: IdentityT m (Set AnyName) Source #
LFresh m => LFresh (ReaderT r m) Source #
Instance details Defined in Unbound.Generics.LocallyNameless.LFresh Methods lfresh :: Typeable a => Name a -> ReaderT r m (Name a) Source # avoid :: [AnyName] -> ReaderT r m a -> ReaderT r m a Source # getAvoids :: ReaderT r m (Set AnyName) Source #
LFresh m => LFresh (StateT s m) Source #
Instance details Defined in Unbound.Generics.LocallyNameless.LFresh Methods lfresh :: Typeable a => Name a -> StateT s m (Name a) Source # avoid :: [AnyName] -> StateT s m a -> StateT s m a Source # getAvoids :: StateT s m (Set AnyName) Source #
LFresh m => LFresh (StateT s m) Source #
Instance details Defined in Unbound.Generics.LocallyNameless.LFresh Methods lfresh :: Typeable a => Name a -> StateT s m (Name a) Source # avoid :: [AnyName] -> StateT s m a -> StateT s m a Source # getAvoids :: StateT s m (Set AnyName) Source #
(Monoid w, LFresh m) => LFresh (WriterT w m) Source #
Instance details Defined in Unbound.Generics.LocallyNameless.LFresh Methods lfresh :: Typeable a => Name a -> WriterT w m (Name a) Source # avoid :: [AnyName] -> WriterT w m a -> WriterT w m a Source # getAvoids :: WriterT w m (Set AnyName) Source #
(Monoid w, LFresh m) => LFresh (WriterT w m) Source #
Instance details Defined in Unbound.Generics.LocallyNameless.LFresh Methods lfresh :: Typeable a => Name a -> WriterT w m (Name a) Source # avoid :: [AnyName] -> WriterT w m a -> WriterT w m a Source # getAvoids :: WriterT w m (Set AnyName) Source #
LFresh m => LFresh (ContT r m) Source #
Instance details Defined in Unbound.Generics.LocallyNameless.LFresh Methods lfresh :: Typeable a => Name a -> ContT r m (Name a) Source # avoid :: [AnyName] -> ContT r m a -> ContT r m a Source # getAvoids :: ContT r m (Set AnyName) Source #

type LFreshM = LFreshMT Identity Source #

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 -> a Source #

Run a LFreshM computation in an empty context.

contLFreshM :: LFreshM a -> Set AnyName -> a Source #

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

newtype LFreshMT (m :: Type -> Type) 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

Instances

Instances details

MonadTrans LFreshMT Source #
Instance details Defined in Unbound.Generics.LocallyNameless.LFresh Methods lift :: Monad m => m a -> LFreshMT m a #
MonadError e m => MonadError e (LFreshMT m) Source #
Instance details Defined in Unbound.Generics.LocallyNameless.LFresh Methods throwError :: e -> LFreshMT m a # catchError :: LFreshMT m a -> (e -> LFreshMT m a) -> LFreshMT m a #
MonadReader r m => MonadReader r (LFreshMT m) Source #
Instance details Defined in Unbound.Generics.LocallyNameless.LFresh Methods ask :: LFreshMT m r # local :: (r -> r) -> LFreshMT m a -> LFreshMT m a # reader :: (r -> a) -> LFreshMT m a #
MonadState s m => MonadState s (LFreshMT m) Source #
Instance details Defined in Unbound.Generics.LocallyNameless.LFresh Methods get :: LFreshMT m s # put :: s -> LFreshMT m () # state :: (s -> (a, s)) -> LFreshMT m a #
MonadWriter w m => MonadWriter w (LFreshMT m) Source #
Instance details Defined in Unbound.Generics.LocallyNameless.LFresh Methods writer :: (a, w) -> LFreshMT m a # tell :: w -> LFreshMT m () # listen :: LFreshMT m a -> LFreshMT m (a, w) # pass :: LFreshMT m (a, w -> w) -> LFreshMT m a #
MonadFail m => MonadFail (LFreshMT m) Source #
Instance details Defined in Unbound.Generics.LocallyNameless.LFresh Methods fail :: String -> LFreshMT m a #
MonadFix m => MonadFix (LFreshMT m) Source #
Instance details Defined in Unbound.Generics.LocallyNameless.LFresh Methods mfix :: (a -> LFreshMT m a) -> LFreshMT m a #
MonadIO m => MonadIO (LFreshMT m) Source #
Instance details Defined in Unbound.Generics.LocallyNameless.LFresh Methods liftIO :: IO a -> LFreshMT m a #
Alternative m => Alternative (LFreshMT m) Source #
Instance details Defined in Unbound.Generics.LocallyNameless.LFresh Methods empty :: LFreshMT m a # (<\|>) :: LFreshMT m a -> LFreshMT m a -> LFreshMT m a # some :: LFreshMT m a -> LFreshMT m [a] # many :: LFreshMT m a -> LFreshMT m [a] #
Applicative m => Applicative (LFreshMT m) Source #
Instance details Defined in Unbound.Generics.LocallyNameless.LFresh Methods pure :: a -> LFreshMT m a # (<>) :: LFreshMT m (a -> b) -> LFreshMT m a -> LFreshMT m b # liftA2 :: (a -> b -> c) -> LFreshMT m a -> LFreshMT m b -> LFreshMT m c # (>) :: LFreshMT m a -> LFreshMT m b -> LFreshMT m b # (<*) :: LFreshMT m a -> LFreshMT m b -> LFreshMT m a #
Functor m => Functor (LFreshMT m) Source #
Instance details Defined in Unbound.Generics.LocallyNameless.LFresh Methods fmap :: (a -> b) -> LFreshMT m a -> LFreshMT m b # (<$) :: a -> LFreshMT m b -> LFreshMT m a #
Monad m => Monad (LFreshMT m) Source #
Instance details Defined in Unbound.Generics.LocallyNameless.LFresh Methods (>>=) :: LFreshMT m a -> (a -> LFreshMT m b) -> LFreshMT m b # (>>) :: LFreshMT m a -> LFreshMT m b -> LFreshMT m b # return :: a -> LFreshMT m a #
MonadPlus m => MonadPlus (LFreshMT m) Source #
Instance details Defined in Unbound.Generics.LocallyNameless.LFresh Methods mzero :: LFreshMT m a # mplus :: LFreshMT m a -> LFreshMT m a -> LFreshMT m a #
MonadCatch m => MonadCatch (LFreshMT m) Source #
Instance details Defined in Unbound.Generics.LocallyNameless.LFresh Methods catch :: (HasCallStack, Exception e) => LFreshMT m a -> (e -> LFreshMT m a) -> LFreshMT m a #
MonadMask m => MonadMask (LFreshMT m) Source #
Instance details Defined in Unbound.Generics.LocallyNameless.LFresh Methods mask :: HasCallStack => ((forall a. LFreshMT m a -> LFreshMT m a) -> LFreshMT m b) -> LFreshMT m b # uninterruptibleMask :: HasCallStack => ((forall a. LFreshMT m a -> LFreshMT m a) -> LFreshMT m b) -> LFreshMT m b # generalBracket :: HasCallStack => LFreshMT m a -> (a -> ExitCase b -> LFreshMT m c) -> (a -> LFreshMT m b) -> LFreshMT m (b, c) #
MonadThrow m => MonadThrow (LFreshMT m) Source #
Instance details Defined in Unbound.Generics.LocallyNameless.LFresh Methods throwM :: (HasCallStack, Exception e) => e -> LFreshMT m a #
MonadCont m => MonadCont (LFreshMT m) Source #
Instance details Defined in Unbound.Generics.LocallyNameless.LFresh Methods callCC :: ((a -> LFreshMT m b) -> LFreshMT m a) -> LFreshMT m a #
Monad m => LFresh (LFreshMT m) Source #
Instance details Defined in Unbound.Generics.LocallyNameless.LFresh Methods lfresh :: Typeable a => Name a -> LFreshMT m (Name a) Source # avoid :: [AnyName] -> LFreshMT m a -> LFreshMT m a Source # getAvoids :: LFreshMT m (Set AnyName) Source #

runLFreshMT :: LFreshMT m a -> m a Source #

Run an LFreshMT computation in an empty context.

contLFreshMT :: LFreshMT m a -> Set AnyName -> m a Source #

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

The LFresh class

Instances

Instances

The `LFresh` class