-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Support for programming with names and binders using GHC Generics
--   
--   Specify the binding structure of your data type with an expressive set
--   of type combinators, and unbound-generics handles the rest!
--   Automatically derives alpha-equivalence, free variable calculation,
--   capture-avoiding substitution, and more. See
--   <tt>Unbound.Generics.LocallyNameless</tt> to get started.
--   
--   This is an independent re-implementation of <a>Unbound</a> but using
--   <a>GHC.Generics</a> instead of <a>RepLib</a>. See the accompanying
--   README for some porting notes.
@package unbound-generics
@version 0.4.0


-- | Some utilities for working with Folds.
--   
--   If you are using <a>lens</a>, you don't need this module.
module Unbound.Generics.LocallyNameless.Internal.Fold
type Fold s a = forall f. (Contravariant f, Applicative f) => (a -> f a) -> s -> f s
type Traversal' s a = forall f. Applicative f => (a -> f a) -> s -> f s
toListOf :: Fold s a -> s -> [a]
filtered :: (a -> Bool) -> Traversal' a a
justFiltered :: (a -> Maybe b) -> Fold a b
foldMapOf :: Getting r s a -> (a -> r) -> s -> r

module Unbound.Generics.LocallyNameless.Internal.Iso
data Exchange a b s t
Exchange :: (s -> a) -> (b -> t) -> Exchange a b s t
type Iso s t a b = forall p f. (Profunctor p, Functor f) => p a (f b) -> p s (f t)
type AnIso s t a b = Exchange a b a (Identity b) -> Exchange a b s (Identity t)
iso :: (s -> a) -> (b -> t) -> Iso s t a b
from :: AnIso s t a b -> Iso b a t s
withIso :: AnIso s t a b -> ((s -> a) -> (b -> t) -> r) -> r
instance Data.Profunctor.Unsafe.Profunctor (Unbound.Generics.LocallyNameless.Internal.Iso.Exchange a b)

module Unbound.Generics.LocallyNameless.Internal.Lens
type Getting r s a = (a -> Const r a) -> s -> Const r s
view :: MonadReader s m => Getting a s a -> m a


-- | Names stand for values. They may be bound or free.
module Unbound.Generics.LocallyNameless.Name

-- | An abstract datatype of names <tt>Name a</tt> that stand for terms of
--   type <tt>a</tt>. The type <tt>a</tt> is used as a tag to distinguish
--   these names from names that may stand for other sorts of terms.
--   
--   Two names in a term are consider <a>aeq</a> equal when they are the
--   same name (in the sense of '(==)'). In patterns, however, any two
--   names are equal if they occur in the same place within the pattern.
--   This induces alpha equivalence on terms in general.
--   
--   Names may either be free or bound (see <a>isFreeName</a>). Free names
--   may be extracted from patterns using <a>isPat</a>. Bound names cannot
--   be.
data Name a
Fn :: String -> !Integer -> Name a
Bn :: !Integer -> !Integer -> Name a

-- | Returns <a>True</a> iff the given <tt>Name a</tt> is free.
isFreeName :: Name a -> Bool

-- | Make a free 'Name a' from a <a>String</a>
string2Name :: String -> Name a

-- | Synonym for <a>string2Name</a>.
s2n :: String -> Name a

-- | Make a name from a <a>String</a> and an <a>Integer</a> index
makeName :: String -> Integer -> Name a

-- | Get the string part of a <a>Name</a>.
name2String :: Name a -> String

-- | Get the integer part of a <a>Name</a>.
name2Integer :: Name a -> Integer

-- | An <tt>AnyName</tt> is a name that stands for a term of some
--   (existentially hidden) type.
data AnyName
[AnyName] :: Typeable a => Name a -> AnyName
instance GHC.Generics.Generic (Unbound.Generics.LocallyNameless.Name.Name a)
instance GHC.Classes.Ord (Unbound.Generics.LocallyNameless.Name.Name a)
instance GHC.Classes.Eq (Unbound.Generics.LocallyNameless.Name.Name a)
instance GHC.Show.Show Unbound.Generics.LocallyNameless.Name.AnyName
instance GHC.Classes.Eq Unbound.Generics.LocallyNameless.Name.AnyName
instance GHC.Classes.Ord Unbound.Generics.LocallyNameless.Name.AnyName
instance Control.DeepSeq.NFData (Unbound.Generics.LocallyNameless.Name.Name a)
instance GHC.Show.Show (Unbound.Generics.LocallyNameless.Name.Name a)


-- | Local freshness monad.
module Unbound.Generics.LocallyNameless.LFresh

-- | 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.
class Monad m => LFresh m

-- | Pick a new name that is fresh for the current (implicit) scope.
lfresh :: (LFresh m, Typeable a) => Name a -> m (Name a)

-- | Avoid the given names when freshening in the subcomputation, that is,
--   add the given names to the in-scope set.
avoid :: LFresh m => [AnyName] -> m a -> m a

-- | Get the set of names currently being avoided.
getAvoids :: LFresh m => m (Set AnyName)

-- | A convenient monad which is an instance of <a>LFresh</a>. It keeps
--   track of a set of names to avoid, and when asked for a fresh one will
--   choose the first unused numerical name.
type LFreshM = LFreshMT Identity

-- | Run a LFreshM computation in an empty context.
runLFreshM :: LFreshM a -> a

-- | Run a LFreshM computation given a set of names to avoid.
contLFreshM :: LFreshM a -> Set AnyName -> a

-- | 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.
newtype LFreshMT m a
LFreshMT :: ReaderT (Set AnyName) m a -> LFreshMT m a
[unLFreshMT] :: LFreshMT m a -> ReaderT (Set AnyName) m a

-- | Run an <a>LFreshMT</a> computation in an empty context.
runLFreshMT :: LFreshMT m a -> m a

-- | Run an <a>LFreshMT</a> computation given a set of names to avoid.
contLFreshMT :: LFreshMT m a -> Set AnyName -> m a
instance Control.Monad.Catch.MonadMask m => Control.Monad.Catch.MonadMask (Unbound.Generics.LocallyNameless.LFresh.LFreshMT m)
instance Control.Monad.Catch.MonadCatch m => Control.Monad.Catch.MonadCatch (Unbound.Generics.LocallyNameless.LFresh.LFreshMT m)
instance Control.Monad.Catch.MonadThrow m => Control.Monad.Catch.MonadThrow (Unbound.Generics.LocallyNameless.LFresh.LFreshMT m)
instance Control.Monad.Fix.MonadFix m => Control.Monad.Fix.MonadFix (Unbound.Generics.LocallyNameless.LFresh.LFreshMT m)
instance GHC.Base.MonadPlus m => GHC.Base.MonadPlus (Unbound.Generics.LocallyNameless.LFresh.LFreshMT m)
instance Control.Monad.IO.Class.MonadIO m => Control.Monad.IO.Class.MonadIO (Unbound.Generics.LocallyNameless.LFresh.LFreshMT m)
instance GHC.Base.Monad m => GHC.Base.Monad (Unbound.Generics.LocallyNameless.LFresh.LFreshMT m)
instance GHC.Base.Alternative m => GHC.Base.Alternative (Unbound.Generics.LocallyNameless.LFresh.LFreshMT m)
instance GHC.Base.Applicative m => GHC.Base.Applicative (Unbound.Generics.LocallyNameless.LFresh.LFreshMT m)
instance GHC.Base.Functor m => GHC.Base.Functor (Unbound.Generics.LocallyNameless.LFresh.LFreshMT m)
instance GHC.Base.Monad m => Unbound.Generics.LocallyNameless.LFresh.LFresh (Unbound.Generics.LocallyNameless.LFresh.LFreshMT m)
instance Control.Monad.Trans.Class.MonadTrans Unbound.Generics.LocallyNameless.LFresh.LFreshMT
instance Control.Monad.Cont.Class.MonadCont m => Control.Monad.Cont.Class.MonadCont (Unbound.Generics.LocallyNameless.LFresh.LFreshMT m)
instance Control.Monad.Error.Class.MonadError e m => Control.Monad.Error.Class.MonadError e (Unbound.Generics.LocallyNameless.LFresh.LFreshMT m)
instance Control.Monad.State.Class.MonadState s m => Control.Monad.State.Class.MonadState s (Unbound.Generics.LocallyNameless.LFresh.LFreshMT m)
instance Control.Monad.Reader.Class.MonadReader r m => Control.Monad.Reader.Class.MonadReader r (Unbound.Generics.LocallyNameless.LFresh.LFreshMT m)
instance Control.Monad.Writer.Class.MonadWriter w m => Control.Monad.Writer.Class.MonadWriter w (Unbound.Generics.LocallyNameless.LFresh.LFreshMT m)
instance Unbound.Generics.LocallyNameless.LFresh.LFresh m => Unbound.Generics.LocallyNameless.LFresh.LFresh (Control.Monad.Trans.Cont.ContT r m)
instance (Control.Monad.Trans.Error.Error e, Unbound.Generics.LocallyNameless.LFresh.LFresh m) => Unbound.Generics.LocallyNameless.LFresh.LFresh (Control.Monad.Trans.Error.ErrorT e m)
instance Unbound.Generics.LocallyNameless.LFresh.LFresh m => Unbound.Generics.LocallyNameless.LFresh.LFresh (Control.Monad.Trans.Except.ExceptT e m)
instance Unbound.Generics.LocallyNameless.LFresh.LFresh m => Unbound.Generics.LocallyNameless.LFresh.LFresh (Control.Monad.Trans.Identity.IdentityT m)
instance Unbound.Generics.LocallyNameless.LFresh.LFresh m => Unbound.Generics.LocallyNameless.LFresh.LFresh (Control.Monad.Trans.List.ListT m)
instance Unbound.Generics.LocallyNameless.LFresh.LFresh m => Unbound.Generics.LocallyNameless.LFresh.LFresh (Control.Monad.Trans.Maybe.MaybeT m)
instance Unbound.Generics.LocallyNameless.LFresh.LFresh m => Unbound.Generics.LocallyNameless.LFresh.LFresh (Control.Monad.Trans.Reader.ReaderT r m)
instance Unbound.Generics.LocallyNameless.LFresh.LFresh m => Unbound.Generics.LocallyNameless.LFresh.LFresh (Control.Monad.Trans.State.Lazy.StateT s m)
instance Unbound.Generics.LocallyNameless.LFresh.LFresh m => Unbound.Generics.LocallyNameless.LFresh.LFresh (Control.Monad.Trans.State.Strict.StateT s m)
instance (GHC.Base.Monoid w, Unbound.Generics.LocallyNameless.LFresh.LFresh m) => Unbound.Generics.LocallyNameless.LFresh.LFresh (Control.Monad.Trans.Writer.Lazy.WriterT w m)
instance (GHC.Base.Monoid w, Unbound.Generics.LocallyNameless.LFresh.LFresh m) => Unbound.Generics.LocallyNameless.LFresh.LFresh (Control.Monad.Trans.Writer.Strict.WriterT w m)


-- | Global freshness monad.
module Unbound.Generics.LocallyNameless.Fresh

-- | The <tt>Fresh</tt> type class governs monads which can generate new
--   globally unique <a>Name</a>s based on a given <a>Name</a>.
class Monad m => Fresh m

-- | Generate a new globally unique name based on the given one.
fresh :: Fresh m => Name a -> m (Name a)

-- | The <tt>FreshM</tt> monad transformer. Keeps track of the lowest index
--   still globally unused, and increments the index every time it is asked
--   for a fresh name.
newtype FreshMT m a
FreshMT :: StateT Integer m a -> FreshMT m a
[unFreshMT] :: FreshMT m a -> StateT Integer m a

-- | Run a <a>FreshMT</a> computation (with the global index starting at
--   zero).
runFreshMT :: Monad m => FreshMT m a -> m a

-- | Run a <a>FreshMT</a> computation given a starting index for fresh name
--   generation.
contFreshMT :: Monad m => FreshMT m a -> Integer -> m a

-- | A convenient monad which is an instance of <a>Fresh</a>. It keeps
--   track of a global index used for generating fresh names, which is
--   incremented every time <a>fresh</a> is called.
type FreshM = FreshMT Identity

-- | Run a FreshM computation (with the global index starting at zero).
runFreshM :: FreshM a -> a

-- | Run a FreshM computation given a starting index.
contFreshM :: FreshM a -> Integer -> a
instance Control.Monad.Catch.MonadMask m => Control.Monad.Catch.MonadMask (Unbound.Generics.LocallyNameless.Fresh.FreshMT m)
instance Control.Monad.Catch.MonadCatch m => Control.Monad.Catch.MonadCatch (Unbound.Generics.LocallyNameless.Fresh.FreshMT m)
instance Control.Monad.Catch.MonadThrow m => Control.Monad.Catch.MonadThrow (Unbound.Generics.LocallyNameless.Fresh.FreshMT m)
instance Control.Monad.Fix.MonadFix m => Control.Monad.Fix.MonadFix (Unbound.Generics.LocallyNameless.Fresh.FreshMT m)
instance GHC.Base.MonadPlus m => GHC.Base.MonadPlus (Unbound.Generics.LocallyNameless.Fresh.FreshMT m)
instance Control.Monad.IO.Class.MonadIO m => Control.Monad.IO.Class.MonadIO (Unbound.Generics.LocallyNameless.Fresh.FreshMT m)
instance GHC.Base.Monad m => GHC.Base.Monad (Unbound.Generics.LocallyNameless.Fresh.FreshMT m)
instance GHC.Base.MonadPlus m => GHC.Base.Alternative (Unbound.Generics.LocallyNameless.Fresh.FreshMT m)
instance GHC.Base.Monad m => GHC.Base.Applicative (Unbound.Generics.LocallyNameless.Fresh.FreshMT m)
instance GHC.Base.Functor m => GHC.Base.Functor (Unbound.Generics.LocallyNameless.Fresh.FreshMT m)
instance Control.Monad.Trans.Class.MonadTrans Unbound.Generics.LocallyNameless.Fresh.FreshMT
instance Control.Monad.Cont.Class.MonadCont m => Control.Monad.Cont.Class.MonadCont (Unbound.Generics.LocallyNameless.Fresh.FreshMT m)
instance Control.Monad.Error.Class.MonadError e m => Control.Monad.Error.Class.MonadError e (Unbound.Generics.LocallyNameless.Fresh.FreshMT m)
instance Control.Monad.State.Class.MonadState s m => Control.Monad.State.Class.MonadState s (Unbound.Generics.LocallyNameless.Fresh.FreshMT m)
instance Control.Monad.Reader.Class.MonadReader r m => Control.Monad.Reader.Class.MonadReader r (Unbound.Generics.LocallyNameless.Fresh.FreshMT m)
instance Control.Monad.Writer.Class.MonadWriter w m => Control.Monad.Writer.Class.MonadWriter w (Unbound.Generics.LocallyNameless.Fresh.FreshMT m)
instance GHC.Base.Monad m => Unbound.Generics.LocallyNameless.Fresh.Fresh (Unbound.Generics.LocallyNameless.Fresh.FreshMT m)
instance (Control.Monad.Trans.Error.Error e, Unbound.Generics.LocallyNameless.Fresh.Fresh m) => Unbound.Generics.LocallyNameless.Fresh.Fresh (Control.Monad.Trans.Error.ErrorT e m)
instance Unbound.Generics.LocallyNameless.Fresh.Fresh m => Unbound.Generics.LocallyNameless.Fresh.Fresh (Control.Monad.Trans.Except.ExceptT e m)
instance Unbound.Generics.LocallyNameless.Fresh.Fresh m => Unbound.Generics.LocallyNameless.Fresh.Fresh (Control.Monad.Trans.Maybe.MaybeT m)
instance Unbound.Generics.LocallyNameless.Fresh.Fresh m => Unbound.Generics.LocallyNameless.Fresh.Fresh (Control.Monad.Trans.Reader.ReaderT r m)
instance Unbound.Generics.LocallyNameless.Fresh.Fresh m => Unbound.Generics.LocallyNameless.Fresh.Fresh (Control.Monad.Trans.State.Lazy.StateT s m)
instance Unbound.Generics.LocallyNameless.Fresh.Fresh m => Unbound.Generics.LocallyNameless.Fresh.Fresh (Control.Monad.Trans.State.Strict.StateT s m)
instance (GHC.Base.Monoid w, Unbound.Generics.LocallyNameless.Fresh.Fresh m) => Unbound.Generics.LocallyNameless.Fresh.Fresh (Control.Monad.Trans.Writer.Lazy.WriterT w m)
instance (GHC.Base.Monoid w, Unbound.Generics.LocallyNameless.Fresh.Fresh m) => Unbound.Generics.LocallyNameless.Fresh.Fresh (Control.Monad.Trans.Writer.Strict.WriterT w m)


-- | A slow, but hopefully correct implementation of permutations.
module Unbound.Generics.PermM

-- | A <i>permutation</i> is a bijective function from names to names which
--   is the identity on all but a finite set of names. They form the basis
--   for nominal approaches to binding, but can also be useful in general.
newtype Perm a
Perm :: Map a a -> Perm a

-- | <tt><a>permValid</a> p</tt> returns <tt>True</tt> iff the perumation
--   is <i>valid</i>: if each value in the range of the permutation is also
--   a key.
permValid :: Ord a => Perm a -> Bool

-- | Create a permutation which swaps two elements.
single :: Ord a => a -> a -> Perm a

-- | Compose two permutations. The right-hand permutation will be applied
--   first.
compose :: Ord a => Perm a -> Perm a -> Perm a

-- | Apply a permutation to an element of the domain.
apply :: Ord a => Perm a -> a -> a

-- | The <i>support</i> of a permutation is the set of elements which are
--   not fixed.
support :: Ord a => Perm a -> [a]

-- | Is this the identity permutation?
isid :: Ord a => Perm a -> Bool

-- | <i>Join</i> two permutations by taking the union of their relation
--   graphs. Fail if they are inconsistent, i.e. map the same element to
--   two different elements.
join :: Ord a => Perm a -> Perm a -> Maybe (Perm a)

-- | The empty (identity) permutation.
empty :: Perm a

-- | Restrict a permutation to a certain domain.
restrict :: Ord a => Perm a -> [a] -> Perm a

-- | <tt>mkPerm l1 l2</tt> creates a permutation that sends <tt>l1</tt> to
--   <tt>l2</tt>. Fail if there is no such permutation, either because the
--   lists have different lengths or because they are inconsistent (which
--   can only happen if <tt>l1</tt> or <tt>l2</tt> have repeated elements).
mkPerm :: Ord a => [a] -> [a] -> Maybe (Perm a)
instance GHC.Show.Show a => GHC.Show.Show (Unbound.Generics.PermM.PartialPerm a)
instance GHC.Classes.Ord a => GHC.Classes.Eq (Unbound.Generics.PermM.Perm a)
instance GHC.Show.Show a => GHC.Show.Show (Unbound.Generics.PermM.Perm a)
instance GHC.Classes.Ord a => GHC.Base.Semigroup (Unbound.Generics.PermM.Perm a)
instance GHC.Classes.Ord a => GHC.Base.Monoid (Unbound.Generics.PermM.Perm a)


-- | Use the <a>Alpha</a> typeclass to mark types that may contain
--   <a>Name</a>s.
module Unbound.Generics.LocallyNameless.Alpha

-- | Types that are instances of <tt>Alpha</tt> may participate in name
--   representation.
--   
--   Minimal instance is entirely empty, provided that your type is an
--   instance of <a>Generic</a>.
class (Show a) => Alpha a

-- | See <a>aeq</a>.
aeq' :: Alpha a => AlphaCtx -> a -> a -> Bool

-- | See <a>aeq</a>.
aeq' :: (Alpha a, Generic a, GAlpha (Rep a)) => AlphaCtx -> a -> a -> Bool

-- | See <a>fvAny</a>.
--   
--   <pre>
--   fvAny' :: Fold a AnyName
--   </pre>
fvAny' :: (Alpha a, Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> a -> f a

-- | See <a>fvAny</a>.
--   
--   <pre>
--   fvAny' :: Fold a AnyName
--   </pre>
fvAny' :: (Alpha a, Generic a, GAlpha (Rep a), Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> a -> f a

-- | Replace free names by bound names.
close :: Alpha a => AlphaCtx -> NamePatFind -> a -> a

-- | Replace free names by bound names.
close :: (Alpha a, Generic a, GAlpha (Rep a)) => AlphaCtx -> NamePatFind -> a -> a

-- | Replace bound names by free names.
open :: Alpha a => AlphaCtx -> NthPatFind -> a -> a

-- | Replace bound names by free names.
open :: (Alpha a, Generic a, GAlpha (Rep a)) => AlphaCtx -> NthPatFind -> a -> a

-- | <tt>isPat x</tt> dynamically checks whether <tt>x</tt> can be used as
--   a valid pattern.
isPat :: Alpha a => a -> DisjointSet AnyName

-- | <tt>isPat x</tt> dynamically checks whether <tt>x</tt> can be used as
--   a valid pattern.
isPat :: (Alpha a, Generic a, GAlpha (Rep a)) => a -> DisjointSet AnyName

-- | <tt>isPat x</tt> dynamically checks whether <tt>x</tt> can be used as
--   a valid term.
isTerm :: Alpha a => a -> All

-- | <tt>isPat x</tt> dynamically checks whether <tt>x</tt> can be used as
--   a valid term.
isTerm :: (Alpha a, Generic a, GAlpha (Rep a)) => a -> All

-- | <tt>isEmbed</tt> is needed internally for the implementation of
--   <a>isPat</a>. <tt>isEmbed</tt> is true for terms wrapped in
--   <tt>Embed</tt> and zero or more occurrences of <tt>Shift</tt>. The
--   default implementation simply returns <tt>False</tt>.
isEmbed :: Alpha a => a -> Bool

-- | If <tt>a</tt> is a pattern, finds the <tt>n</tt>th name in the pattern
--   (starting from zero), returning the number of names encountered if not
--   found.
nthPatFind :: Alpha a => a -> NthPatFind

-- | If <tt>a</tt> is a pattern, finds the <tt>n</tt>th name in the pattern
--   (starting from zero), returning the number of names encountered if not
--   found.
nthPatFind :: (Alpha a, Generic a, GAlpha (Rep a)) => a -> NthPatFind

-- | If <tt>a</tt> is a pattern, find the index of the given name in the
--   pattern.
namePatFind :: Alpha a => a -> NamePatFind

-- | If <tt>a</tt> is a pattern, find the index of the given name in the
--   pattern.
namePatFind :: (Alpha a, Generic a, GAlpha (Rep a)) => a -> NamePatFind

-- | See <a>swaps</a>. Apply the given permutation of variable names to the
--   given pattern.
swaps' :: Alpha a => AlphaCtx -> Perm AnyName -> a -> a

-- | See <a>swaps</a>. Apply the given permutation of variable names to the
--   given pattern.
swaps' :: (Alpha a, Generic a, GAlpha (Rep a)) => AlphaCtx -> Perm AnyName -> a -> a

-- | See <a>freshen</a>.
lfreshen' :: (Alpha a, LFresh m) => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b

-- | See <a>freshen</a>.
lfreshen' :: (Alpha a, LFresh m, Generic a, GAlpha (Rep a)) => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b

-- | See <a>freshen</a>. Rename the free variables in the given term to be
--   distinct from all other names seen in the monad <tt>m</tt>.
freshen' :: (Alpha a, Fresh m) => AlphaCtx -> a -> m (a, Perm AnyName)

-- | See <a>freshen</a>. Rename the free variables in the given term to be
--   distinct from all other names seen in the monad <tt>m</tt>.
freshen' :: (Alpha a, Generic a, GAlpha (Rep a), Fresh m) => AlphaCtx -> a -> m (a, Perm AnyName)

-- | See <a>acompare</a>. An alpha-respecting total order on terms
--   involving binders.
acompare' :: Alpha a => AlphaCtx -> a -> a -> Ordering

-- | See <a>acompare</a>. An alpha-respecting total order on terms
--   involving binders.
acompare' :: (Alpha a, Generic a, GAlpha (Rep a)) => AlphaCtx -> a -> a -> Ordering

-- | A <tt>DisjointSet a</tt> is a <a>Just</a> a list of distinct
--   <tt>a</tt>s. In addition to a monoidal structure, a disjoint set also
--   has an annihilator <a>inconsistentDisjointSet</a>.
--   
--   <pre>
--   inconsistentDisjointSet &lt;&gt; s == inconsistentDisjointSet
--   s &lt;&gt; inconsistentDisjoinSet == inconsistentDisjointSet
--   </pre>
newtype DisjointSet a
DisjointSet :: Maybe [a] -> DisjointSet a

-- | Returns a <tt>DisjointSet a</tt> that is the annihilator element for
--   the <a>Monoid</a> instance of <a>DisjointSet</a>.
inconsistentDisjointSet :: DisjointSet a

-- | <tt>singletonDisjointSet x</tt> a <tt>DisjointSet a</tt> that contains
--   the single element <tt>x</tt>
singletonDisjointSet :: a -> DisjointSet a

-- | <tt>isConsistentDisjointSet</tt> returns <tt>True</tt> iff the given
--   disjoint set is not inconsistent.
isConsistentDisjointSet :: DisjointSet a -> Bool

-- | <tt>isNullDisjointSet</tt> return <tt>True</tt> iff the given disjoint
--   set is <a>mempty</a>.
isNullDisjointSet :: DisjointSet a -> Bool

-- | The result of <tt><a>nthPatFind</a> a i</tt> is <tt>Left k</tt> where
--   <tt>i-k</tt> is the number of names in pattern <tt>a</tt> (with <tt>k
--   &lt; i</tt>) or <tt>Right x</tt> where <tt>x</tt> is the <tt>i</tt>th
--   name in <tt>a</tt>
newtype NthPatFind
NthPatFind :: (Integer -> Either Integer AnyName) -> NthPatFind
[runNthPatFind] :: NthPatFind -> Integer -> Either Integer AnyName

-- | The result of <tt><a>namePatFind</a> a x</tt> is either <tt>Left
--   i</tt> if <tt>a</tt> is a pattern that contains <tt>i</tt> free names
--   none of which are <tt>x</tt>, or <tt>Right j</tt> if <tt>x</tt> is the
--   <tt>j</tt>th name in <tt>a</tt>
newtype NamePatFind
NamePatFind :: (AnyName -> Either Integer Integer) -> NamePatFind
[runNamePatFind] :: NamePatFind -> AnyName -> Either Integer Integer

-- | Some <a>Alpha</a> operations need to record information about their
--   progress. Instances should just pass it through unchanged.
--   
--   The context records whether we are currently operating on terms or
--   patterns, and how many binding levels we've descended.
data AlphaCtx

-- | The starting context for alpha operations: we are expecting to work on
--   terms and we are under no binders.
initialCtx :: AlphaCtx

-- | Switches to a context where we expect to operate on patterns.
patternCtx :: AlphaCtx -> AlphaCtx

-- | Switches to a context where we expect to operate on terms.
termCtx :: AlphaCtx -> AlphaCtx

-- | Returns <a>True</a> iff we are in a context where we expect to see
--   terms.
isTermCtx :: AlphaCtx -> Bool

-- | Increment the number of binders that we are operating under.
incrLevelCtx :: AlphaCtx -> AlphaCtx

-- | Decrement the number of binders that we are operating under.
decrLevelCtx :: AlphaCtx -> AlphaCtx

-- | Are we operating under no binders?
isZeroLevelCtx :: AlphaCtx -> Bool
gaeq :: GAlpha f => AlphaCtx -> f a -> f a -> Bool
gfvAny :: (GAlpha f, Contravariant g, Applicative g) => AlphaCtx -> (AnyName -> g AnyName) -> f a -> g (f a)
gclose :: GAlpha f => AlphaCtx -> NamePatFind -> f a -> f a
gopen :: GAlpha f => AlphaCtx -> NthPatFind -> f a -> f a
gisPat :: GAlpha f => f a -> DisjointSet AnyName
gisTerm :: GAlpha f => f a -> All
gnthPatFind :: GAlpha f => f a -> NthPatFind
gnamePatFind :: GAlpha f => f a -> NamePatFind
gswaps :: GAlpha f => AlphaCtx -> Perm AnyName -> f a -> f a
gfreshen :: (GAlpha f, Fresh m) => AlphaCtx -> f a -> FFM m (f a, Perm AnyName)
glfreshen :: (GAlpha f, LFresh m) => AlphaCtx -> f a -> (f a -> Perm AnyName -> m b) -> m b
gacompare :: GAlpha f => AlphaCtx -> f a -> f a -> Ordering
data FFM f a
liftFFM :: Monad m => m a -> FFM m a
retractFFM :: Monad m => FFM m a -> m a
instance GHC.Classes.Eq Unbound.Generics.LocallyNameless.Alpha.Mode
instance Unbound.Generics.LocallyNameless.Alpha.Alpha c => Unbound.Generics.LocallyNameless.Alpha.GAlpha (GHC.Generics.K1 i c)
instance Unbound.Generics.LocallyNameless.Alpha.Alpha GHC.Types.Int
instance Unbound.Generics.LocallyNameless.Alpha.Alpha GHC.Types.Char
instance Unbound.Generics.LocallyNameless.Alpha.Alpha GHC.Integer.Type.Integer
instance Unbound.Generics.LocallyNameless.Alpha.Alpha GHC.Types.Float
instance Unbound.Generics.LocallyNameless.Alpha.Alpha GHC.Types.Double
instance (GHC.Real.Integral n, Unbound.Generics.LocallyNameless.Alpha.Alpha n) => Unbound.Generics.LocallyNameless.Alpha.Alpha (GHC.Real.Ratio n)
instance Unbound.Generics.LocallyNameless.Alpha.Alpha GHC.Types.Bool
instance Unbound.Generics.LocallyNameless.Alpha.Alpha a => Unbound.Generics.LocallyNameless.Alpha.Alpha (GHC.Maybe.Maybe a)
instance Unbound.Generics.LocallyNameless.Alpha.Alpha a => Unbound.Generics.LocallyNameless.Alpha.Alpha [a]
instance Unbound.Generics.LocallyNameless.Alpha.Alpha ()
instance (Unbound.Generics.LocallyNameless.Alpha.Alpha a, Unbound.Generics.LocallyNameless.Alpha.Alpha b) => Unbound.Generics.LocallyNameless.Alpha.Alpha (Data.Either.Either a b)
instance (Unbound.Generics.LocallyNameless.Alpha.Alpha a, Unbound.Generics.LocallyNameless.Alpha.Alpha b) => Unbound.Generics.LocallyNameless.Alpha.Alpha (a, b)
instance (Unbound.Generics.LocallyNameless.Alpha.Alpha a, Unbound.Generics.LocallyNameless.Alpha.Alpha b, Unbound.Generics.LocallyNameless.Alpha.Alpha c) => Unbound.Generics.LocallyNameless.Alpha.Alpha (a, b, c)
instance (Unbound.Generics.LocallyNameless.Alpha.Alpha a, Unbound.Generics.LocallyNameless.Alpha.Alpha b, Unbound.Generics.LocallyNameless.Alpha.Alpha c, Unbound.Generics.LocallyNameless.Alpha.Alpha d) => Unbound.Generics.LocallyNameless.Alpha.Alpha (a, b, c, d)
instance (Unbound.Generics.LocallyNameless.Alpha.Alpha a, Unbound.Generics.LocallyNameless.Alpha.Alpha b, Unbound.Generics.LocallyNameless.Alpha.Alpha c, Unbound.Generics.LocallyNameless.Alpha.Alpha d, Unbound.Generics.LocallyNameless.Alpha.Alpha e) => Unbound.Generics.LocallyNameless.Alpha.Alpha (a, b, c, d, e)
instance Data.Typeable.Internal.Typeable a => Unbound.Generics.LocallyNameless.Alpha.Alpha (Unbound.Generics.LocallyNameless.Name.Name a)
instance Unbound.Generics.LocallyNameless.Alpha.Alpha Unbound.Generics.LocallyNameless.Name.AnyName
instance Unbound.Generics.LocallyNameless.Alpha.GAlpha f => Unbound.Generics.LocallyNameless.Alpha.GAlpha (GHC.Generics.M1 i c f)
instance Unbound.Generics.LocallyNameless.Alpha.GAlpha GHC.Generics.U1
instance Unbound.Generics.LocallyNameless.Alpha.GAlpha GHC.Generics.V1
instance (Unbound.Generics.LocallyNameless.Alpha.GAlpha f, Unbound.Generics.LocallyNameless.Alpha.GAlpha g) => Unbound.Generics.LocallyNameless.Alpha.GAlpha (f GHC.Generics.:*: g)
instance (Unbound.Generics.LocallyNameless.Alpha.GAlpha f, Unbound.Generics.LocallyNameless.Alpha.GAlpha g) => Unbound.Generics.LocallyNameless.Alpha.GAlpha (f GHC.Generics.:+: g)
instance GHC.Base.Semigroup Unbound.Generics.LocallyNameless.Alpha.NamePatFind
instance GHC.Base.Monoid Unbound.Generics.LocallyNameless.Alpha.NamePatFind
instance GHC.Base.Semigroup Unbound.Generics.LocallyNameless.Alpha.NthPatFind
instance GHC.Base.Monoid Unbound.Generics.LocallyNameless.Alpha.NthPatFind
instance GHC.Base.Functor (Unbound.Generics.LocallyNameless.Alpha.FFM f)
instance GHC.Base.Applicative (Unbound.Generics.LocallyNameless.Alpha.FFM f)
instance GHC.Base.Monad (Unbound.Generics.LocallyNameless.Alpha.FFM f)
instance Unbound.Generics.LocallyNameless.Fresh.Fresh m => Unbound.Generics.LocallyNameless.Fresh.Fresh (Unbound.Generics.LocallyNameless.Alpha.FFM m)
instance GHC.Classes.Eq a => GHC.Base.Semigroup (Unbound.Generics.LocallyNameless.Alpha.DisjointSet a)
instance GHC.Classes.Eq a => GHC.Base.Monoid (Unbound.Generics.LocallyNameless.Alpha.DisjointSet a)
instance Data.Foldable.Foldable Unbound.Generics.LocallyNameless.Alpha.DisjointSet


-- | Template Haskell methods to construct instances of <a>Alpha</a> for
--   datatypes that don't contain any names and don't participate in
--   <a>Alpha</a> operations in any non-trivial way.
module Unbound.Generics.LocallyNameless.TH
makeClosedAlpha :: Name -> DecsQ


-- | The pattern <tt><a>Rebind</a> p1 p2</tt> binds the names in
--   <tt>p1</tt> and <tt>p2</tt> just as <tt>(p1, p2)</tt> would, however
--   it additionally also brings the names of <tt>p1</tt> into scope in
--   <tt>p2</tt>.
module Unbound.Generics.LocallyNameless.Rebind

-- | <tt><a>Rebind</a> p1 p2</tt> is a pattern that binds the names of
--   <tt>p1</tt> and <tt>p2</tt>, and additionally brings the names of
--   <tt>p1</tt> into scope over <tt>p2</tt>.
--   
--   This may be used, for example, to faithfully represent Scheme's
--   <tt>let*</tt> binding form, defined by:
--   
--   <pre>
--   (let* () body) ≙ body
--   (let* ([v1, e1] binds ...) body) ≙ (let ([v1, e1]) (let* (binds ...) body))
--   </pre>
--   
--   using the following AST:
--   
--   <pre>
--   type Var = Name Expr
--   data Lets = EmptyLs
--             | ConsLs (Rebind (Var, Embed Expr) Lets)
--   data Expr = ...
--             | LetStar (Bind Lets Expr)
--             | ...
--   </pre>
data Rebind p1 p2
Rebnd :: p1 -> p2 -> Rebind p1 p2
instance (GHC.Classes.Eq p1, GHC.Classes.Eq p2) => GHC.Classes.Eq (Unbound.Generics.LocallyNameless.Rebind.Rebind p1 p2)
instance GHC.Generics.Generic (Unbound.Generics.LocallyNameless.Rebind.Rebind p1 p2)
instance (Control.DeepSeq.NFData p1, Control.DeepSeq.NFData p2) => Control.DeepSeq.NFData (Unbound.Generics.LocallyNameless.Rebind.Rebind p1 p2)
instance (GHC.Show.Show p1, GHC.Show.Show p2) => GHC.Show.Show (Unbound.Generics.LocallyNameless.Rebind.Rebind p1 p2)
instance (Unbound.Generics.LocallyNameless.Alpha.Alpha p1, Unbound.Generics.LocallyNameless.Alpha.Alpha p2) => Unbound.Generics.LocallyNameless.Alpha.Alpha (Unbound.Generics.LocallyNameless.Rebind.Rebind p1 p2)


-- | Ignores a term for the purposes of alpha-equality and substitution
module Unbound.Generics.LocallyNameless.Ignore

-- | Ignores a term <tt>t</tt> for the purpose of alpha-equality and
--   substitution
data Ignore t
I :: !t -> Ignore t
instance GHC.Generics.Generic (Unbound.Generics.LocallyNameless.Ignore.Ignore t)
instance Control.DeepSeq.NFData t => Control.DeepSeq.NFData (Unbound.Generics.LocallyNameless.Ignore.Ignore t)
instance GHC.Show.Show t => GHC.Show.Show (Unbound.Generics.LocallyNameless.Ignore.Ignore t)
instance GHC.Show.Show t => Unbound.Generics.LocallyNameless.Alpha.Alpha (Unbound.Generics.LocallyNameless.Ignore.Ignore t)


-- | The pattern <tt><a>Embed</a> t</tt> contains a term <tt>t</tt>.
module Unbound.Generics.LocallyNameless.Embed

-- | <tt>Embed</tt> allows for terms to be <i>embedded</i> within patterns.
--   Such embedded terms do not bind names along with the rest of the
--   pattern. For examples, see the tutorial or examples directories.
--   
--   If <tt>t</tt> is a <i>term type</i>, then <tt>Embed t</tt> is a
--   <i>pattern type</i>.
--   
--   <tt>Embed</tt> is not abstract since it involves no binding, and hence
--   it is safe to manipulate directly. To create and destruct
--   <tt>Embed</tt> terms, you may use the <tt>Embed</tt> constructor
--   directly. (You may also use the functions <tt>embed</tt> and
--   <tt>unembed</tt>, which additionally can construct or destruct any
--   number of enclosing <tt>Shift</tt>s at the same time.)
newtype Embed t
Embed :: t -> Embed t
class IsEmbed e where {
    
    -- | The term type embedded in the embedding <tt>e</tt>
    type family Embedded e :: *;
}

-- | Insert or extract the embedded term. If you're not using the lens
--   library, see <a>embed</a> and <a>unembed</a> otherwise <a>embedded</a>
--   is an isomorphism that you can use with lens. <tt> embedded :: Iso'
--   (Embedded e) e </tt>
embedded :: (IsEmbed e, Profunctor p, Functor f) => p (Embedded e) (f (Embedded e)) -> p e (f e)
instance GHC.Generics.Generic (Unbound.Generics.LocallyNameless.Embed.Embed t)
instance GHC.Classes.Ord t => GHC.Classes.Ord (Unbound.Generics.LocallyNameless.Embed.Embed t)
instance GHC.Classes.Eq t => GHC.Classes.Eq (Unbound.Generics.LocallyNameless.Embed.Embed t)
instance Unbound.Generics.LocallyNameless.Embed.IsEmbed (Unbound.Generics.LocallyNameless.Embed.Embed t)
instance Control.DeepSeq.NFData t => Control.DeepSeq.NFData (Unbound.Generics.LocallyNameless.Embed.Embed t)
instance GHC.Show.Show a => GHC.Show.Show (Unbound.Generics.LocallyNameless.Embed.Embed a)
instance Unbound.Generics.LocallyNameless.Alpha.Alpha t => Unbound.Generics.LocallyNameless.Alpha.Alpha (Unbound.Generics.LocallyNameless.Embed.Embed t)


-- | The pattern <tt><a>Shift</a> e</tt> shifts the scope of the embedded
--   term in <tt>e</tt> one level outwards.
module Unbound.Generics.LocallyNameless.Shift

-- | The type <tt>Shift e</tt> is an embedding pattern that shifts the
--   scope of the free variables of the embedded term <tt><a>Embedded</a>
--   e</tt> up by one level.
newtype Shift e
Shift :: e -> Shift e
instance GHC.Base.Functor Unbound.Generics.LocallyNameless.Shift.Shift
instance Unbound.Generics.LocallyNameless.Embed.IsEmbed e => Unbound.Generics.LocallyNameless.Embed.IsEmbed (Unbound.Generics.LocallyNameless.Shift.Shift e)
instance Control.DeepSeq.NFData e => Control.DeepSeq.NFData (Unbound.Generics.LocallyNameless.Shift.Shift e)
instance GHC.Show.Show e => GHC.Show.Show (Unbound.Generics.LocallyNameless.Shift.Shift e)
instance Unbound.Generics.LocallyNameless.Alpha.Alpha e => Unbound.Generics.LocallyNameless.Alpha.Alpha (Unbound.Generics.LocallyNameless.Shift.Shift e)


-- | The fundamental binding form. The type <tt><a>Bind</a> p t</tt> allows
--   you to place a pattern <tt>p</tt> in a term <tt>t</tt> such that the
--   names in the pattern scope over the term. Use <a>bind</a> and
--   <a>unbind</a> and <a>lunbind</a> to work with <tt><a>Bind</a> p t</tt>
module Unbound.Generics.LocallyNameless.Bind

-- | A term of type <tt><a>Bind</a> p t</tt> is a term that binds the free
--   variable occurrences of the variables in pattern <tt>p</tt> in the
--   term <tt>t</tt>. In the overall term, those variables are now bound.
--   See also <a>bind</a> and <a>unbind</a> and <a>lunbind</a>
data Bind p t
B :: p -> t -> Bind p t
instance GHC.Generics.Generic (Unbound.Generics.LocallyNameless.Bind.Bind p t)
instance (Control.DeepSeq.NFData p, Control.DeepSeq.NFData t) => Control.DeepSeq.NFData (Unbound.Generics.LocallyNameless.Bind.Bind p t)
instance (GHC.Show.Show p, GHC.Show.Show t) => GHC.Show.Show (Unbound.Generics.LocallyNameless.Bind.Bind p t)
instance (Unbound.Generics.LocallyNameless.Alpha.Alpha p, Unbound.Generics.LocallyNameless.Alpha.Alpha t) => Unbound.Generics.LocallyNameless.Alpha.Alpha (Unbound.Generics.LocallyNameless.Bind.Bind p t)


-- | Dangerous operations that may disturb the invariants of
--   <a>Unbind.Generics.LocallyNameless</a> or of your AST.
module Unbound.Generics.LocallyNameless.Unsafe

-- | A destructor for binders that does <i>not</i> guarantee fresh names
--   for the binders.
unsafeUnbind :: (Alpha p, Alpha t) => Bind p t -> (p, t)


-- | The pattern <tt><a>Rec</a> p</tt> binds the names in <tt>p</tt> like
--   <tt>p</tt> itself would, but additionally, the names in <tt>p</tt> are
--   scope over <tt>p</tt>.
--   
--   The term <tt><a>TRec</a> p</tt> is shorthand for <tt><a>Bind</a> (Rec
--   p) ()</tt>
module Unbound.Generics.LocallyNameless.Rec

-- | If <tt>p</tt> is a pattern type, then <tt>Rec p</tt> is also a pattern
--   type, which is <i>recursive</i> in the sense that <tt>p</tt> may bind
--   names in terms embedded within itself. Useful for encoding e.g.
--   lectrec and Agda's dot notation.
data Rec p

-- | Constructor for recursive patterns.
rec :: Alpha p => p -> Rec p

-- | Destructor for recursive patterns.
unrec :: Alpha p => Rec p -> p

-- | <tt>TRec</tt> is a standalone variant of <a>Rec</a>: the only
--   difference is that whereas <tt><a>Rec</a> p</tt> is a pattern type,
--   <tt>TRec p</tt> is a <i>term type</i>. It is isomorphic to
--   <tt><a>Bind</a> (<a>Rec</a> p) ()</tt>.
--   
--   Note that <tt>TRec</tt> corresponds to Pottier's <i>abstraction</i>
--   construct from alpha-Caml. In this context, <tt><tt>Embed</tt> t</tt>
--   corresponds to alpha-Caml's <tt>inner t</tt>, and <tt><tt>Shift</tt>
--   (<tt>Embed</tt> t)</tt> corresponds to alpha-Caml's <tt>outer t</tt>.
newtype TRec p
TRec :: Bind (Rec p) () -> TRec p
instance GHC.Generics.Generic (Unbound.Generics.LocallyNameless.Rec.TRec p)
instance GHC.Classes.Eq p => GHC.Classes.Eq (Unbound.Generics.LocallyNameless.Rec.Rec p)
instance GHC.Generics.Generic (Unbound.Generics.LocallyNameless.Rec.Rec p)
instance GHC.Show.Show a => GHC.Show.Show (Unbound.Generics.LocallyNameless.Rec.TRec a)
instance Unbound.Generics.LocallyNameless.Alpha.Alpha p => Unbound.Generics.LocallyNameless.Alpha.Alpha (Unbound.Generics.LocallyNameless.Rec.TRec p)
instance Control.DeepSeq.NFData p => Control.DeepSeq.NFData (Unbound.Generics.LocallyNameless.Rec.Rec p)
instance GHC.Show.Show a => GHC.Show.Show (Unbound.Generics.LocallyNameless.Rec.Rec a)
instance Unbound.Generics.LocallyNameless.Alpha.Alpha p => Unbound.Generics.LocallyNameless.Alpha.Alpha (Unbound.Generics.LocallyNameless.Rec.Rec p)


-- | A typeclass for types that may participate in capture-avoiding
--   substitution
--   
--   The minimal definition is empty, provided your type is an instance of
--   <a>Generic</a>
--   
--   <pre>
--   type Var = Name Factor
--   data Expr = SumOf [Summand]
--             deriving (Show, Generic)
--   data Summand = ProductOf [Factor]
--             deriving (Show, Generic)
--   instance Subst Var Expr
--   instance Subst Var Summand
--   </pre>
--   
--   The default instance just propagates the substitution into the
--   constituent factors.
--   
--   If you identify the variable occurrences by implementing the
--   <a>isvar</a> function, the derived <a>subst</a> function will be able
--   to substitute a factor for a variable.
--   
--   <pre>
--   data Factor = V Var
--               | C Int
--               | Subexpr Expr
--             deriving (Show, Generic)
--   instance Subst Var Factor where
--     isvar (V v) = Just (SubstName v)
--     isvar _     = Nothing
--   </pre>
module Unbound.Generics.LocallyNameless.Subst

-- | See <tt>isVar</tt>
data SubstName a b
[SubstName] :: a ~ b => Name a -> SubstName a b

-- | See <a>isCoerceVar</a>
data SubstCoerce a b
[SubstCoerce] :: Name b -> (b -> Maybe a) -> SubstCoerce a b

-- | Instances of <tt><a>Subst</a> b a</tt> are terms of type <tt>a</tt>
--   that may contain variables of type <tt>b</tt> that may participate in
--   capture-avoiding substitution.
class Subst b a

-- | This is the only method that must be implemented
isvar :: Subst b a => a -> Maybe (SubstName a b)

-- | This is an alternative version to <a>isvar</a>, useable in the case
--   that the substituted argument doesn't have *exactly* the same type as
--   the term it should be substituted into. The default implementation
--   always returns <a>Nothing</a>.
isCoerceVar :: Subst b a => a -> Maybe (SubstCoerce a b)

-- | <tt><a>subst</a> nm e tm</tt> substitutes <tt>e</tt> for <tt>nm</tt>
--   in <tt>tm</tt>. It has a default generic implementation in terms of
--   <tt>isvar</tt>
subst :: Subst b a => Name b -> b -> a -> a

-- | <tt><a>subst</a> nm e tm</tt> substitutes <tt>e</tt> for <tt>nm</tt>
--   in <tt>tm</tt>. It has a default generic implementation in terms of
--   <tt>isvar</tt>
subst :: (Subst b a, Generic a, GSubst b (Rep a)) => Name b -> b -> a -> a
substs :: Subst b a => [(Name b, b)] -> a -> a
substs :: (Subst b a, Generic a, GSubst b (Rep a)) => [(Name b, b)] -> a -> a
instance Unbound.Generics.LocallyNameless.Subst.Subst b c => Unbound.Generics.LocallyNameless.Subst.GSubst b (GHC.Generics.K1 i c)
instance Unbound.Generics.LocallyNameless.Subst.Subst b GHC.Types.Int
instance Unbound.Generics.LocallyNameless.Subst.Subst b GHC.Types.Bool
instance Unbound.Generics.LocallyNameless.Subst.Subst b ()
instance Unbound.Generics.LocallyNameless.Subst.Subst b GHC.Types.Char
instance Unbound.Generics.LocallyNameless.Subst.Subst b GHC.Types.Float
instance Unbound.Generics.LocallyNameless.Subst.Subst b GHC.Types.Double
instance Unbound.Generics.LocallyNameless.Subst.Subst b GHC.Integer.Type.Integer
instance (Unbound.Generics.LocallyNameless.Subst.Subst c a, Unbound.Generics.LocallyNameless.Subst.Subst c b) => Unbound.Generics.LocallyNameless.Subst.Subst c (a, b)
instance (Unbound.Generics.LocallyNameless.Subst.Subst c a, Unbound.Generics.LocallyNameless.Subst.Subst c b, Unbound.Generics.LocallyNameless.Subst.Subst c d) => Unbound.Generics.LocallyNameless.Subst.Subst c (a, b, d)
instance (Unbound.Generics.LocallyNameless.Subst.Subst c a, Unbound.Generics.LocallyNameless.Subst.Subst c b, Unbound.Generics.LocallyNameless.Subst.Subst c d, Unbound.Generics.LocallyNameless.Subst.Subst c e) => Unbound.Generics.LocallyNameless.Subst.Subst c (a, b, d, e)
instance (Unbound.Generics.LocallyNameless.Subst.Subst c a, Unbound.Generics.LocallyNameless.Subst.Subst c b, Unbound.Generics.LocallyNameless.Subst.Subst c d, Unbound.Generics.LocallyNameless.Subst.Subst c e, Unbound.Generics.LocallyNameless.Subst.Subst c f) => Unbound.Generics.LocallyNameless.Subst.Subst c (a, b, d, e, f)
instance Unbound.Generics.LocallyNameless.Subst.Subst c a => Unbound.Generics.LocallyNameless.Subst.Subst c [a]
instance Unbound.Generics.LocallyNameless.Subst.Subst c a => Unbound.Generics.LocallyNameless.Subst.Subst c (GHC.Maybe.Maybe a)
instance (Unbound.Generics.LocallyNameless.Subst.Subst c a, Unbound.Generics.LocallyNameless.Subst.Subst c b) => Unbound.Generics.LocallyNameless.Subst.Subst c (Data.Either.Either a b)
instance Unbound.Generics.LocallyNameless.Subst.Subst b (Unbound.Generics.LocallyNameless.Name.Name a)
instance Unbound.Generics.LocallyNameless.Subst.Subst b Unbound.Generics.LocallyNameless.Name.AnyName
instance Unbound.Generics.LocallyNameless.Subst.Subst c a => Unbound.Generics.LocallyNameless.Subst.Subst c (Unbound.Generics.LocallyNameless.Embed.Embed a)
instance Unbound.Generics.LocallyNameless.Subst.Subst c e => Unbound.Generics.LocallyNameless.Subst.Subst c (Unbound.Generics.LocallyNameless.Shift.Shift e)
instance (Unbound.Generics.LocallyNameless.Subst.Subst c b, Unbound.Generics.LocallyNameless.Subst.Subst c a, Unbound.Generics.LocallyNameless.Alpha.Alpha a, Unbound.Generics.LocallyNameless.Alpha.Alpha b) => Unbound.Generics.LocallyNameless.Subst.Subst c (Unbound.Generics.LocallyNameless.Bind.Bind a b)
instance (Unbound.Generics.LocallyNameless.Subst.Subst c p1, Unbound.Generics.LocallyNameless.Subst.Subst c p2) => Unbound.Generics.LocallyNameless.Subst.Subst c (Unbound.Generics.LocallyNameless.Rebind.Rebind p1 p2)
instance Unbound.Generics.LocallyNameless.Subst.Subst c p => Unbound.Generics.LocallyNameless.Subst.Subst c (Unbound.Generics.LocallyNameless.Rec.Rec p)
instance (Unbound.Generics.LocallyNameless.Alpha.Alpha p, Unbound.Generics.LocallyNameless.Subst.Subst c p) => Unbound.Generics.LocallyNameless.Subst.Subst c (Unbound.Generics.LocallyNameless.Rec.TRec p)
instance Unbound.Generics.LocallyNameless.Subst.Subst a (Unbound.Generics.LocallyNameless.Ignore.Ignore b)
instance Unbound.Generics.LocallyNameless.Subst.GSubst b f => Unbound.Generics.LocallyNameless.Subst.GSubst b (GHC.Generics.M1 i c f)
instance Unbound.Generics.LocallyNameless.Subst.GSubst b GHC.Generics.U1
instance Unbound.Generics.LocallyNameless.Subst.GSubst b GHC.Generics.V1
instance (Unbound.Generics.LocallyNameless.Subst.GSubst b f, Unbound.Generics.LocallyNameless.Subst.GSubst b g) => Unbound.Generics.LocallyNameless.Subst.GSubst b (f GHC.Generics.:*: g)
instance (Unbound.Generics.LocallyNameless.Subst.GSubst b f, Unbound.Generics.LocallyNameless.Subst.GSubst b g) => Unbound.Generics.LocallyNameless.Subst.GSubst b (f GHC.Generics.:+: g)


-- | Operations on terms and patterns that contain names.
module Unbound.Generics.LocallyNameless.Operations

-- | <tt><a>aeq</a> t1 t2</tt> returns <tt>True</tt> iff <tt>t1</tt> and
--   <tt>t2</tt> are alpha-equivalent terms.
aeq :: Alpha a => a -> a -> Bool

-- | An alpha-respecting total order on terms involving binders.
acompare :: Alpha a => a -> a -> Ordering

-- | <tt><a>fvAny</a></tt> returns a fold over any names in a term
--   <tt>a</tt>.
--   
--   <pre>
--   fvAny :: Alpha a =&gt; Fold a AnyName
--   </pre>
fvAny :: (Alpha a, Contravariant f, Applicative f) => (AnyName -> f AnyName) -> a -> f a

-- | <tt><a>fv</a></tt> returns the free <tt>b</tt> variables of term
--   <tt>a</tt>.
--   
--   <pre>
--   fv :: (Alpha a, Typeable b) =&gt; Fold a (Name b)
--   </pre>
fv :: forall a f b. (Alpha a, Typeable b, Contravariant f, Applicative f) => (Name b -> f (Name b)) -> a -> f a

-- | Freshen a pattern by replacing all old binding <a>Name</a>s with new
--   fresh <a>Name</a>s, returning a new pattern and a <tt><a>Perm</a>
--   <a>Name</a></tt> specifying how <a>Name</a>s were replaced.
freshen :: (Alpha p, Fresh m) => p -> m (p, Perm AnyName)

-- | "Locally" freshen a pattern, replacing all binding names with new
--   names that are not already "in scope". The second argument is a
--   continuation, which takes the renamed term and a permutation that
--   specifies how the pattern has been renamed. The resulting computation
--   will be run with the in-scope set extended by the names just
--   generated.
lfreshen :: (Alpha p, LFresh m) => p -> (p -> Perm AnyName -> m b) -> m b

-- | Apply the given permutation of variable names to the given term.
swaps :: Alpha t => Perm AnyName -> t -> t

-- | A term of type <tt><a>Bind</a> p t</tt> is a term that binds the free
--   variable occurrences of the variables in pattern <tt>p</tt> in the
--   term <tt>t</tt>. In the overall term, those variables are now bound.
--   See also <a>bind</a> and <a>unbind</a> and <a>lunbind</a>
data Bind p t

-- | <tt><a>bind</a> p t</tt> closes over the variables of pattern
--   <tt>p</tt> in the term <tt>t</tt>
bind :: (Alpha p, Alpha t) => p -> t -> Bind p t

-- | <tt><a>unbind</a> b</tt> lets you descend beneath a binder <tt>b ::
--   <a>Bind</a> p t</tt> by returning the pair of the pattern <tt>p</tt>
--   and the term <tt>t</tt> where the variables in the pattern have been
--   made globally fresh with respect to the freshness monad <tt>m</tt>.
unbind :: (Alpha p, Alpha t, Fresh m) => Bind p t -> m (p, t)

-- | <tt>lunbind</tt> opens a binding in an <a>LFresh</a> monad, ensuring
--   that the names chosen for the binders are <i>locally</i> fresh. The
--   components of the binding are passed to a <i>continuation</i>, and the
--   resulting monadic action is run in a context extended to avoid
--   choosing new names which are the same as the ones chosen for this
--   binding.
--   
--   For more information, see the documentation for the <a>LFresh</a> type
--   class.
lunbind :: (LFresh m, Alpha p, Alpha t) => Bind p t -> ((p, t) -> m c) -> m c

-- | Simultaneously unbind two patterns in two terms, returning
--   <a>Nothing</a> if the two patterns don't bind the same number of
--   variables.
unbind2 :: (Fresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => Bind p1 t1 -> Bind p2 t2 -> m (Maybe (p1, t1, p2, t2))

-- | Simultaneously <a>lunbind</a> two patterns in two terms in the
--   <a>LFresh</a> monad, passing <tt>Just (p1, t1, p2, t2)</tt> to the
--   continuation such that the patterns are permuted such that they
--   introduce the same free names, or <a>Nothing</a> if the number of
--   variables differs.
lunbind2 :: (LFresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => Bind p1 t1 -> Bind p2 t2 -> (Maybe (p1, t1, p2, t2) -> m c) -> m c

-- | Simultaneously unbind two patterns in two terms, returning
--   <a>mzero</a> if the patterns don't bind the same number of variables.
unbind2Plus :: (MonadPlus m, Fresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => Bind p1 t1 -> Bind p2 t2 -> m (p1, t1, p2, t2)

-- | <tt><a>Rebind</a> p1 p2</tt> is a pattern that binds the names of
--   <tt>p1</tt> and <tt>p2</tt>, and additionally brings the names of
--   <tt>p1</tt> into scope over <tt>p2</tt>.
--   
--   This may be used, for example, to faithfully represent Scheme's
--   <tt>let*</tt> binding form, defined by:
--   
--   <pre>
--   (let* () body) ≙ body
--   (let* ([v1, e1] binds ...) body) ≙ (let ([v1, e1]) (let* (binds ...) body))
--   </pre>
--   
--   using the following AST:
--   
--   <pre>
--   type Var = Name Expr
--   data Lets = EmptyLs
--             | ConsLs (Rebind (Var, Embed Expr) Lets)
--   data Expr = ...
--             | LetStar (Bind Lets Expr)
--             | ...
--   </pre>
data Rebind p1 p2

-- | <tt><a>rebind</a> p1 p2</tt> is a smart constructor for <a>Rebind</a>.
--   It captures the variables of pattern <tt>p1</tt> that occur within
--   <tt>p2</tt> in addition to providing binding occurrences for all the
--   variables of <tt>p1</tt> and <tt>p2</tt>
rebind :: (Alpha p1, Alpha p2) => p1 -> p2 -> Rebind p1 p2

-- | <tt><a>unrebind</a> p</tt> is the elimination form for <a>Rebind</a>.
--   It is not monadic (unlike <a>unbind</a>) because a <tt>Rebind</tt>
--   pattern can only occur somewhere in a pattern position of a
--   <a>Bind</a>, and therefore <a>unbind</a> must have already been called
--   and all names apropriately <a>freshen</a>ed.
unrebind :: (Alpha p1, Alpha p2) => Rebind p1 p2 -> (p1, p2)

-- | <tt>Embed</tt> allows for terms to be <i>embedded</i> within patterns.
--   Such embedded terms do not bind names along with the rest of the
--   pattern. For examples, see the tutorial or examples directories.
--   
--   If <tt>t</tt> is a <i>term type</i>, then <tt>Embed t</tt> is a
--   <i>pattern type</i>.
--   
--   <tt>Embed</tt> is not abstract since it involves no binding, and hence
--   it is safe to manipulate directly. To create and destruct
--   <tt>Embed</tt> terms, you may use the <tt>Embed</tt> constructor
--   directly. (You may also use the functions <tt>embed</tt> and
--   <tt>unembed</tt>, which additionally can construct or destruct any
--   number of enclosing <tt>Shift</tt>s at the same time.)
newtype Embed t
Embed :: t -> Embed t
class IsEmbed e where {
    
    -- | The term type embedded in the embedding <tt>e</tt>
    type family Embedded e :: *;
}

-- | Insert or extract the embedded term. If you're not using the lens
--   library, see <a>embed</a> and <a>unembed</a> otherwise <a>embedded</a>
--   is an isomorphism that you can use with lens. <tt> embedded :: Iso'
--   (Embedded e) e </tt>
embedded :: (IsEmbed e, Profunctor p, Functor f) => p (Embedded e) (f (Embedded e)) -> p e (f e)

-- | Embeds a term in an <a>Embed</a>, or an <a>Embed</a> under some number
--   of <a>Shift</a> constructors.
embed :: IsEmbed e => Embedded e -> e

-- | <tt><a>unembed</a> p</tt> extracts the term embedded in the pattern
--   <tt>p</tt>.
unembed :: IsEmbed e => e -> Embedded e

-- | If <tt>p</tt> is a pattern type, then <tt>Rec p</tt> is also a pattern
--   type, which is <i>recursive</i> in the sense that <tt>p</tt> may bind
--   names in terms embedded within itself. Useful for encoding e.g.
--   lectrec and Agda's dot notation.
data Rec p

-- | Constructor for recursive patterns.
rec :: Alpha p => p -> Rec p

-- | Destructor for recursive patterns.
unrec :: Alpha p => Rec p -> p

-- | <tt>TRec</tt> is a standalone variant of <a>Rec</a>: the only
--   difference is that whereas <tt><a>Rec</a> p</tt> is a pattern type,
--   <tt>TRec p</tt> is a <i>term type</i>. It is isomorphic to
--   <tt><a>Bind</a> (<a>Rec</a> p) ()</tt>.
--   
--   Note that <tt>TRec</tt> corresponds to Pottier's <i>abstraction</i>
--   construct from alpha-Caml. In this context, <tt><tt>Embed</tt> t</tt>
--   corresponds to alpha-Caml's <tt>inner t</tt>, and <tt><tt>Shift</tt>
--   (<tt>Embed</tt> t)</tt> corresponds to alpha-Caml's <tt>outer t</tt>.
newtype TRec p
TRec :: Bind (Rec p) () -> TRec p

-- | Constructor for recursive abstractions.
trec :: Alpha p => p -> TRec p

-- | Destructor for recursive abstractions which picks globally fresh names
--   for the binders.
untrec :: (Alpha p, Fresh m) => TRec p -> m p

-- | Destructor for recursive abstractions which picks <i>locally</i> fresh
--   names for binders (see <a>LFresh</a>).
luntrec :: (Alpha p, LFresh m) => TRec p -> m p

-- | Ignores a term <tt>t</tt> for the purpose of alpha-equality and
--   substitution
data Ignore t

-- | Constructor for ignoring a term for the purposes of alpha-equality and
--   substs
ignore :: t -> Ignore t

-- | Destructor for ignored terms
unignore :: Ignore t -> t


-- | The purpose of <tt>unbound-genrics</tt> is to simplify the
--   construction of data structures with rich variable binding structure
--   by providing generic implementations of alpha-equivalence
--   (<a>aeq</a>), free variable permutation (<a>swaps</a>), local and
--   global variable freshness (<a>lfresh</a>, <a>fresh</a>),
--   
--   See <a>Alpha</a>, <a>Bind</a>,
--   <a>Unbound.Generics.LocallyNameless.Operations</a> for more
--   information.
module Unbound.Generics.LocallyNameless

-- | An <tt>AnyName</tt> is a name that stands for a term of some
--   (existentially hidden) type.
data AnyName
[AnyName] :: Typeable a => Name a -> AnyName

-- | An abstract datatype of names <tt>Name a</tt> that stand for terms of
--   type <tt>a</tt>. The type <tt>a</tt> is used as a tag to distinguish
--   these names from names that may stand for other sorts of terms.
--   
--   Two names in a term are consider <a>aeq</a> equal when they are the
--   same name (in the sense of '(==)'). In patterns, however, any two
--   names are equal if they occur in the same place within the pattern.
--   This induces alpha equivalence on terms in general.
--   
--   Names may either be free or bound (see <a>isFreeName</a>). Free names
--   may be extracted from patterns using <a>isPat</a>. Bound names cannot
--   be.
data Name a

-- | Returns <a>True</a> iff the given <tt>Name a</tt> is free.
isFreeName :: Name a -> Bool

-- | Make a free 'Name a' from a <a>String</a>
string2Name :: String -> Name a

-- | Synonym for <a>string2Name</a>.
s2n :: String -> Name a

-- | Make a name from a <a>String</a> and an <a>Integer</a> index
makeName :: String -> Integer -> Name a

-- | Get the integer part of a <a>Name</a>.
name2Integer :: Name a -> Integer

-- | Get the string part of a <a>Name</a>.
name2String :: Name a -> String

-- | A term of type <tt><a>Bind</a> p t</tt> is a term that binds the free
--   variable occurrences of the variables in pattern <tt>p</tt> in the
--   term <tt>t</tt>. In the overall term, those variables are now bound.
--   See also <a>bind</a> and <a>unbind</a> and <a>lunbind</a>
data Bind p t

-- | Ignores a term <tt>t</tt> for the purpose of alpha-equality and
--   substitution
data Ignore t

-- | <tt><a>Rebind</a> p1 p2</tt> is a pattern that binds the names of
--   <tt>p1</tt> and <tt>p2</tt>, and additionally brings the names of
--   <tt>p1</tt> into scope over <tt>p2</tt>.
--   
--   This may be used, for example, to faithfully represent Scheme's
--   <tt>let*</tt> binding form, defined by:
--   
--   <pre>
--   (let* () body) ≙ body
--   (let* ([v1, e1] binds ...) body) ≙ (let ([v1, e1]) (let* (binds ...) body))
--   </pre>
--   
--   using the following AST:
--   
--   <pre>
--   type Var = Name Expr
--   data Lets = EmptyLs
--             | ConsLs (Rebind (Var, Embed Expr) Lets)
--   data Expr = ...
--             | LetStar (Bind Lets Expr)
--             | ...
--   </pre>
data Rebind p1 p2
