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


-- | Simple generic unification algorithms.
--   
--   Simple generic unification algorithms.
@package unification-fd
@version 0.10.0.1


-- | A continuation-passing variant of <a>Either</a> for short-circuiting
--   at failure. This code is based on <a>Control.Monad.MaybeK</a>.
module Control.Monad.EitherK

-- | A continuation-passing encoding of <a>Either</a> as an error monad;
--   also known as <tt>Codensity (Either e)</tt>, if you're familiar with
--   that terminology. N.B., this is not the 2-continuation implementation
--   based on the Church encoding of <tt>Either</tt>. The latter tends to
--   have worse performance than non-continuation based implementations.
--   
--   This is generally more efficient than using <tt>Either</tt> (or the
--   MTL's <tt>Error</tt>) for two reasons. First is that it right
--   associates all binds, ensuring that bad associativity doesn't
--   artificially introduce midpoints in short-circuiting to the nearest
--   handler. Second is that it removes the need for intermediate case
--   expressions.
--   
--   Another benefit over MTL's <tt>Error</tt> is that it doesn't
--   artificially restrict the error type. In fact, there's no reason why
--   <tt>e</tt> must denote "errors" per se. This could also denote
--   computations which short-circuit with the final answer, or similar
--   methods of non-local control flow.
--   
--   N.B., the <a>Alternative</a> and <a>MonadPlus</a> instances are
--   left-biased in <tt>a</tt> and monoidal in <tt>e</tt>. Thus, they are
--   not commutative.
data EitherK e a

-- | Execute an <tt>EitherK</tt> and return the concrete <tt>Either</tt>
--   encoding.
runEitherK :: EitherK e a -> Either e a

-- | Lift an <tt>Either</tt> into an <tt>EitherK</tt>.
toEitherK :: Either e a -> EitherK e a

-- | A version of <a>either</a> on <tt>EitherK</tt>, for convenience. N.B.,
--   using this function inserts a case match, reducing the range of
--   short-circuiting.
eitherK :: (e -> b) -> (a -> b) -> EitherK e a -> b

-- | Throw an error in the <tt>EitherK</tt> monad. This is identical to
--   <a>throwError</a>.
throwEitherK :: e -> EitherK e a

-- | Handle errors in the <tt>EitherK</tt> monad. N.B., this type is more
--   general than that of <a>catchError</a>, allowing the type of the
--   errors to change.
catchEitherK :: EitherK e a -> (e -> EitherK f a) -> EitherK f a

-- | A monad transformer version of <a>EitherK</a>.
data EitherKT e m a

-- | Execute an <tt>EitherKT</tt> and return the concrete <tt>Either</tt>
--   encoding.
runEitherKT :: (Applicative m) => EitherKT e m a -> m (Either e a)

-- | Lift an <tt>Either</tt> into an <tt>EitherKT</tt>.
toEitherKT :: (Applicative m) => Either e a -> EitherKT e m a

-- | Lift an <tt>EitherK</tt> into an <tt>EitherKT</tt>.
liftEitherK :: (Applicative m) => EitherK e a -> EitherKT e m a

-- | Lower an <tt>EitherKT</tt> into an <tt>EitherK</tt>.
lowerEitherK :: (Applicative m) => EitherKT e m a -> m (EitherK e a)

-- | Throw an error in the <tt>EitherKT</tt> monad. This is identical to
--   <a>throwError</a>.
throwEitherKT :: (Applicative m) => e -> EitherKT e m a

-- | Handle errors in the <tt>EitherKT</tt> monad. N.B., this type is more
--   general than that of <a>catchError</a>, allowing the type of the
--   errors to change.
catchEitherKT :: (Applicative m, Monad m) => EitherKT e m a -> (e -> EitherKT f m a) -> EitherKT f m a
instance GHC.Base.Functor (Control.Monad.EitherK.EitherKT e m)
instance GHC.Base.Applicative (Control.Monad.EitherK.EitherKT e m)
instance GHC.Base.Monad (Control.Monad.EitherK.EitherKT e m)
instance (GHC.Base.Applicative m, GHC.Base.Monad m, GHC.Base.Monoid e) => GHC.Base.Alternative (Control.Monad.EitherK.EitherKT e m)
instance (GHC.Base.Applicative m, GHC.Base.Monad m, GHC.Base.Monoid e) => GHC.Base.MonadPlus (Control.Monad.EitherK.EitherKT e m)
instance (GHC.Base.Applicative m, GHC.Base.Monad m) => Control.Monad.Error.Class.MonadError e (Control.Monad.EitherK.EitherKT e m)
instance Control.Monad.Trans.Class.MonadTrans (Control.Monad.EitherK.EitherKT e)
instance GHC.Base.Functor (Control.Monad.EitherK.EitherK e)
instance GHC.Base.Applicative (Control.Monad.EitherK.EitherK e)
instance GHC.Base.Monad (Control.Monad.EitherK.EitherK e)
instance GHC.Base.Monoid e => GHC.Base.Alternative (Control.Monad.EitherK.EitherK e)
instance GHC.Base.Monoid e => GHC.Base.MonadPlus (Control.Monad.EitherK.EitherK e)
instance Control.Monad.Error.Class.MonadError e (Control.Monad.EitherK.EitherK e)


-- | A continuation-passing variant of <a>Maybe</a> for short-circuiting at
--   failure. This is based largely on code from the Haskell Wiki
--   (<a>http://www.haskell.org/haskellwiki/Performance/Monads</a>) which
--   was released under a simple permissive license
--   (<a>http://www.haskell.org/haskellwiki/HaskellWiki:Copyrights</a>).
--   However, various changes and extensions have been made, which are
--   subject to the BSD license of this package.
module Control.Monad.MaybeK

-- | A continuation-passing encoding of <a>Maybe</a>; also known as
--   <tt>Codensity Maybe</tt>, if you're familiar with that terminology.
--   N.B., this is not the 2-continuation implementation based on the
--   Church encoding of <tt>Maybe</tt>. The latter tends to have worse
--   performance than non-continuation based implementations.
--   
--   This is generally more efficient than using <tt>Maybe</tt> for two
--   reasons. First is that it right associates all binds, ensuring that
--   bad associativity doesn't artificially introduce midpoints in
--   short-circuiting to the nearest handler. Second is that it removes the
--   need for intermediate case expressions.
--   
--   N.B., the <a>Alternative</a> and <a>MonadPlus</a> instances are
--   left-biased in <tt>a</tt>. Thus, they are not commutative.
data MaybeK a

-- | Execute the <tt>MaybeK</tt> and return the concrete <tt>Maybe</tt>
--   encoding.
runMaybeK :: MaybeK a -> Maybe a

-- | Lift a <tt>Maybe</tt> into <tt>MaybeK</tt>.
toMaybeK :: Maybe a -> MaybeK a

-- | A version of <a>maybe</a> for convenience. This is almost identical to
--   <a>mplus</a> but allows applying a continuation to <tt>Just</tt>
--   values as well as handling <tt>Nothing</tt> errors. If you only want
--   to handle the errors, use <a>mplus</a> instead.
maybeK :: b -> (a -> b) -> MaybeK a -> b

-- | A monad transformer version of <a>MaybeK</a>.
data MaybeKT m a

-- | Execute a <tt>MaybeKT</tt> and return the concrete <tt>Maybe</tt>
--   encoding.
runMaybeKT :: (Applicative m) => MaybeKT m a -> m (Maybe a)

-- | Lift a <tt>Maybe</tt> into an <tt>MaybeKT</tt>.
toMaybeKT :: (Applicative m) => Maybe a -> MaybeKT m a

-- | Lift an <tt>MaybeK</tt> into an <tt>MaybeKT</tt>.
liftMaybeK :: (Applicative m) => MaybeK a -> MaybeKT m a

-- | Lower an <tt>MaybeKT</tt> into an <tt>MaybeK</tt>.
lowerMaybeK :: (Applicative m) => MaybeKT m a -> m (MaybeK a)
instance GHC.Base.Functor (Control.Monad.MaybeK.MaybeKT m)
instance GHC.Base.Applicative (Control.Monad.MaybeK.MaybeKT m)
instance GHC.Base.Monad (Control.Monad.MaybeK.MaybeKT m)
instance (GHC.Base.Applicative m, GHC.Base.Monad m) => GHC.Base.Alternative (Control.Monad.MaybeK.MaybeKT m)
instance (GHC.Base.Applicative m, GHC.Base.Monad m) => GHC.Base.MonadPlus (Control.Monad.MaybeK.MaybeKT m)
instance (GHC.Base.Applicative m, GHC.Base.Monad m) => Control.Monad.Error.Class.MonadError () (Control.Monad.MaybeK.MaybeKT m)
instance Control.Monad.Trans.Class.MonadTrans Control.Monad.MaybeK.MaybeKT
instance GHC.Base.Functor Control.Monad.MaybeK.MaybeK
instance GHC.Base.Applicative Control.Monad.MaybeK.MaybeK
instance GHC.Base.Monad Control.Monad.MaybeK.MaybeK
instance GHC.Base.Alternative Control.Monad.MaybeK.MaybeK
instance GHC.Base.MonadPlus Control.Monad.MaybeK.MaybeK
instance Control.Monad.Error.Class.MonadError () Control.Monad.MaybeK.MaybeK


-- | This module defines some extra functions for
--   <a>Control.Monad.State.Lazy</a>. This package really isn't the proper
--   place for these, but we need them to be somewhere.
--   
--   TODO: patch transformers/mtl-2 with these functions.
module Control.Monad.State.UnificationExtras

-- | Lift a reader into a state monad. More particularly, this allows
--   disabling mutability in a local context within <tt>State</tt>.
liftReader :: Reader e a -> State e a

-- | Lift a reader into a state monad. More particularly, this allows
--   disabling mutability in a local context within <tt>StateT</tt>.
liftReaderT :: (Monad m) => ReaderT e m a -> StateT e m a

-- | A strict version of <tt>modify</tt>.
modify' :: (MonadState s m) => (s -> s) -> m ()

-- | Run a state action and undo the state changes at the end.
localState :: (MonadState s m) => m a -> m a


-- | This module provides a fixed point operator on functor types. For
--   Haskell the least and greatest fixed points coincide, so we needn't
--   distinguish them. This abstract nonsense is helpful in conjunction
--   with other category theoretic tricks like Swierstra's functor
--   coproducts (not provided by this package). For more on the utility of
--   two-level recursive types, see:
--   
--   <ul>
--   <li>Tim Sheard (2001) <i>Generic Unification via Two-Level Types</i>
--   <i>and Paramterized Modules</i>, Functional Pearl, ICFP.</li>
--   <li>Tim Sheard &amp; Emir Pasalic (2004) <i>Two-Level Types and</i>
--   <i>Parameterized Modules</i>. JFP 14(5): 547--587. This is an expanded
--   version of Sheard (2001) with new examples.</li>
--   <li>Wouter Swierstra (2008) <i>Data types a la carte</i>, Functional
--   Pearl. JFP 18: 423--436.</li>
--   </ul>
module Data.Functor.Fixedpoint

-- | <tt>Fix f</tt> is a fix point of the <a>Functor</a> <tt>f</tt>. Note
--   that in Haskell the least and greatest fixed points coincide, so we
--   don't need to distinguish between <tt>Mu f</tt> and <tt>Nu f</tt>.
--   This type used to be called <tt>Y</tt>, hence the naming convention
--   for all the <tt>yfoo</tt> functions.
--   
--   This type lets us invoke category theory to get recursive types and
--   operations over them without the type checker complaining about
--   infinite types. The <a>Show</a> instance doesn't print the
--   constructors, for legibility.
newtype Fix f
Fix :: f (Fix f) -> Fix f
[unFix] :: Fix f -> f (Fix f)

-- | A higher-order map taking a natural transformation <tt>(f -&gt;
--   g)</tt> and lifting it to operate on <tt>Fix</tt>.
hmap :: (Functor f, Functor g) => (forall a. f a -> g a) -> Fix f -> Fix g

-- | A monadic variant of <a>hmap</a>.
hmapM :: (Functor f, Traversable g, Monad m) => (forall a. f a -> m (g a)) -> Fix f -> m (Fix g)

-- | A version of <a>fmap</a> for endomorphisms on the fixed point. That
--   is, this maps the function over the first layer of recursive
--   structure.
ymap :: (Functor f) => (Fix f -> Fix f) -> Fix f -> Fix f

-- | A monadic variant of <a>ymap</a>.
ymapM :: (Traversable f, Monad m) => (Fix f -> m (Fix f)) -> Fix f -> m (Fix f)

-- | Take a Church encoding of a fixed point into the data representation
--   of the fixed point.
build :: (Functor f) => (forall r. (f r -> r) -> r) -> Fix f

-- | A pure catamorphism over the least fixed point of a functor. This
--   function applies the <tt>f</tt>-algebra from the bottom up over
--   <tt>Fix f</tt> to create some residual value.
cata :: (Functor f) => (f a -> a) -> (Fix f -> a)

-- | A catamorphism for monadic <tt>f</tt>-algebras. Alas, this isn't
--   wholly generic to <tt>Functor</tt> since it requires distribution of
--   <tt>f</tt> over <tt>m</tt> (provided by <a>sequence</a> or <a>mapM</a>
--   in <a>Traversable</a>).
--   
--   N.B., this orders the side effects from the bottom up.
cataM :: (Traversable f, Monad m) => (f a -> m a) -> (Fix f -> m a)

-- | A variant of <a>cata</a> which restricts the return type to being a
--   new fixpoint. Though more restrictive, it can be helpful when you
--   already have an algebra which expects the outermost <tt>Fix</tt>.
--   
--   If you don't like either <tt>fmap</tt> or <tt>cata</tt>, then maybe
--   this is what you were thinking?
ycata :: (Functor f) => (Fix f -> Fix f) -> Fix f -> Fix f

-- | Monadic variant of <a>ycata</a>.
ycataM :: (Traversable f, Monad m) => (Fix f -> m (Fix f)) -> Fix f -> m (Fix f)

-- | A pure anamorphism generating the greatest fixed point of a functor.
--   This function applies an <tt>f</tt>-coalgebra from the top down to
--   expand a seed into a <tt>Fix f</tt>.
ana :: (Functor f) => (a -> f a) -> (a -> Fix f)

-- | An anamorphism for monadic <tt>f</tt>-coalgebras. Alas, this isn't
--   wholly generic to <tt>Functor</tt> since it requires distribution of
--   <tt>f</tt> over <tt>m</tt> (provided by <a>sequence</a> or <a>mapM</a>
--   in <a>Traversable</a>).
--   
--   N.B., this orders the side effects from the top down.
anaM :: (Traversable f, Monad m) => (a -> m (f a)) -> (a -> m (Fix f))

-- | <pre>
--   hylo phi psi == cata phi . ana psi
--   </pre>
hylo :: (Functor f) => (f b -> b) -> (a -> f a) -> (a -> b)

-- | <pre>
--   hyloM phiM psiM == cataM phiM &lt;=&lt; anaM psiM
--   </pre>
hyloM :: (Traversable f, Monad m) => (f b -> m b) -> (a -> m (f a)) -> (a -> m b)
instance GHC.Show.Show (f (Data.Functor.Fixedpoint.Fix f)) => GHC.Show.Show (Data.Functor.Fixedpoint.Fix f)
instance GHC.Classes.Eq (f (Data.Functor.Fixedpoint.Fix f)) => GHC.Classes.Eq (Data.Functor.Fixedpoint.Fix f)
instance GHC.Classes.Ord (f (Data.Functor.Fixedpoint.Fix f)) => GHC.Classes.Ord (Data.Functor.Fixedpoint.Fix f)


-- | This module defines the classes and primitive types used by
--   unification and related functions.
module Control.Unification.Types

-- | The type of terms generated by structures <tt>t</tt> over variables
--   <tt>v</tt>. The structure type should implement <a>Unifiable</a> and
--   the variable type should implement <a>Variable</a>.
--   
--   The <a>Show</a> instance doesn't show the constructors, in order to
--   improve legibility for large terms.
--   
--   All the category theoretic instances (<a>Functor</a>, <a>Foldable</a>,
--   <a>Traversable</a>,...) are provided because they are often useful;
--   however, beware that since the implementations must be pure, they
--   cannot read variables bound in the current context and therefore can
--   create incoherent results. Therefore, you should apply the current
--   bindings before using any of the functions provided by those classes.
data UTerm t v

-- | A unification variable.
UVar :: !v -> UTerm t v

-- | Some structure containing subterms.
UTerm :: !(t (UTerm t v)) -> UTerm t v

-- | <i>O(n)</i>. Extract a pure term from a mutable term, or return
--   <tt>Nothing</tt> if the mutable term actually contains variables.
--   N.B., this function is pure, so you should manually apply bindings
--   before calling it.
freeze :: (Traversable t) => UTerm t v -> Maybe (Fix t)

-- | <i>O(n)</i>. Embed a pure term as a mutable term.
unfreeze :: (Functor t) => Fix t -> UTerm t v

-- | The possible failure modes that could be encountered in unification
--   and related functions. While many of the functions could be given more
--   accurate types if we used ad-hoc combinations of these constructors
--   (i.e., because they can only throw one of the errors), the extra
--   complexity is not considered worth it.
--   
--   This is a finally-tagless encoding of the <a>UFailure</a> data type so
--   that we can abstract over clients adding additional domain-specific
--   failure modes, introducing monoid instances, etc.
--   
--   <i>Since: 0.10.0</i>
class Fallible t v a

-- | A cyclic term was encountered (i.e., the variable occurs free in a
--   term it would have to be bound to in order to succeed). Infinite terms
--   like this are not generally acceptable, so we do not support them. In
--   logic programming this should simply be treated as unification
--   failure; in type checking this should result in a "could not construct
--   infinite type <tt>a = Foo a</tt>" error.
--   
--   Note that since, by default, the library uses visited-sets instead of
--   the occurs-check these errors will be thrown at the point where the
--   cycle is dereferenced/unrolled (e.g., when applying bindings), instead
--   of at the time when the cycle is created. However, the arguments to
--   this constructor should express the same context as if we had
--   performed the occurs-check, in order for error messages to be
--   intelligable.
occursFailure :: Fallible t v a => v -> UTerm t v -> a

-- | The top-most level of the terms do not match (according to
--   <a>zipMatch</a>). In logic programming this should simply be treated
--   as unification failure; in type checking this should result in a
--   "could not match expected type <tt>Foo</tt> with inferred type
--   <tt>Bar</tt>" error.
mismatchFailure :: Fallible t v a => t (UTerm t v) -> t (UTerm t v) -> a

-- | A concrete representation for the <a>Fallible</a> type class. Whenever
--   possible, you should prefer to keep the concrete representation
--   abstract by using the <a>Fallible</a> class instead.
--   
--   <i>Updated: 0.10.0</i> Used to be called <tt>UnificationFailure</tt>.
--   Removed the <tt>UnknownError</tt> constructor, and the
--   <tt>Control.Monad.Error.Error</tt> instance associated with it.
--   Renamed <tt>OccursIn</tt> constructor to <tt>OccursFailure</tt>; and
--   renamed <tt>TermMismatch</tt> constructor to <tt>MismatchFailure</tt>.
--   
--   <i>Updated: 0.8.1</i> added <a>Functor</a>, <a>Foldable</a>, and
--   <a>Traversable</a> instances.
data UFailure t v
OccursFailure :: v -> (UTerm t v) -> UFailure t v
MismatchFailure :: (t (UTerm t v)) -> (t (UTerm t v)) -> UFailure t v

-- | An implementation of syntactically unifiable structure. The
--   <tt>Traversable</tt> constraint is there because we also require terms
--   to be functors and require the distributivity of <a>sequence</a> or
--   <a>mapM</a>.
class (Traversable t) => Unifiable t

-- | Perform one level of equality testing for terms. If the term
--   constructors are unequal then return <tt>Nothing</tt>; if they are
--   equal, then return the one-level spine filled with resolved subterms
--   and/or pairs of subterms to be recursively checked.
zipMatch :: Unifiable t => t a -> t a -> Maybe (t (Either a (a, a)))

-- | An implementation of unification variables. The <a>Eq</a> requirement
--   is to determine whether two variables are equal <i>as variables</i>,
--   without considering what they are bound to. We use <a>Eq</a> rather
--   than having our own <tt>eqVar</tt> method so that clients can make use
--   of library functions which commonly assume <a>Eq</a>.
class (Eq v) => Variable v

-- | Return a unique identifier for this variable, in order to support the
--   use of visited-sets instead of occurs-checks. This function must
--   satisfy the following coherence law with respect to the <a>Eq</a>
--   instance:
--   
--   <tt>x == y</tt> if and only if <tt>getVarID x == getVarID y</tt>
getVarID :: Variable v => v -> Int

-- | The basic class for generating, reading, and writing to bindings
--   stored in a monad. These three functionalities could be split apart,
--   but are combined in order to simplify contexts. Also, because most
--   functions reading bindings will also perform path compression, there's
--   no way to distinguish "true" mutation from mere path compression.
--   
--   The superclass constraints are there to simplify contexts, since we
--   make the same assumptions everywhere we use <tt>BindingMonad</tt>.
class (Unifiable t, Variable v, Applicative m, Monad m) => BindingMonad t v m | m t -> v, v m -> t

-- | Given a variable pointing to <tt>UTerm t v</tt>, return the term it's
--   bound to, or <tt>Nothing</tt> if the variable is unbound.
lookupVar :: BindingMonad t v m => v -> m (Maybe (UTerm t v))

-- | Generate a new free variable guaranteed to be fresh in <tt>m</tt>.
freeVar :: BindingMonad t v m => m v

-- | Generate a new variable (fresh in <tt>m</tt>) bound to the given term.
--   The default implementation is:
--   
--   <pre>
--   newVar t = do { v &lt;- freeVar ; bindVar v t ; return v }
--   </pre>
newVar :: BindingMonad t v m => UTerm t v -> m v

-- | Bind a variable to a term, overriding any previous binding.
bindVar :: BindingMonad t v m => v -> UTerm t v -> m ()

-- | The target of variables for <a>RankedBindingMonad</a>s. In order to
--   support weighted path compression, each variable is bound to both
--   another term (possibly) and also a "rank" which is related to the
--   length of the variable chain to the term it's ultimately bound to.
--   
--   The rank can be at most <tt>log V</tt>, where <tt>V</tt> is the total
--   number of variables in the unification problem. Thus, A <tt>Word8</tt>
--   is sufficient for <tt>2^(2^8)</tt> variables, which is far more than
--   can be indexed by <a>getVarID</a> even on 64-bit architectures.
data Rank t v
Rank :: {-# UNPACK #-} !Word8 -> !(Maybe (UTerm t v)) -> Rank t v

-- | An advanced class for <a>BindingMonad</a>s which also support weighted
--   path compression. The weightedness adds non-trivial implementation
--   complications; so even though weighted path compression is
--   asymptotically optimal, the constant factors may make it worthwhile to
--   stick with the unweighted path compression supported by
--   <a>BindingMonad</a>.
class (BindingMonad t v m) => RankedBindingMonad t v m | m t -> v, v m -> t

-- | Given a variable pointing to <tt>UTerm t v</tt>, return its rank and
--   the term it's bound to.
lookupRankVar :: RankedBindingMonad t v m => v -> m (Rank t v)

-- | Increase the rank of a variable by one.
incrementRank :: RankedBindingMonad t v m => v -> m ()

-- | Bind a variable to a term and increment the rank at the same time. The
--   default implementation is:
--   
--   <pre>
--   incrementBindVar t v = do { incrementRank v ; bindVar v t }
--   </pre>
incrementBindVar :: RankedBindingMonad t v m => v -> UTerm t v -> m ()
instance (GHC.Show.Show v, GHC.Show.Show (t (Control.Unification.Types.UTerm t v))) => GHC.Show.Show (Control.Unification.Types.Rank t v)
instance Control.Unification.Types.Fallible t v (Control.Unification.Types.UFailure t v)
instance (GHC.Show.Show (t (Control.Unification.Types.UTerm t v)), GHC.Show.Show v) => GHC.Show.Show (Control.Unification.Types.UFailure t v)
instance GHC.Base.Functor t => GHC.Base.Functor (Control.Unification.Types.UFailure t)
instance Data.Foldable.Foldable t => Data.Foldable.Foldable (Control.Unification.Types.UFailure t)
instance Data.Traversable.Traversable t => Data.Traversable.Traversable (Control.Unification.Types.UFailure t)
instance (GHC.Show.Show v, GHC.Show.Show (t (Control.Unification.Types.UTerm t v))) => GHC.Show.Show (Control.Unification.Types.UTerm t v)
instance GHC.Base.Functor t => GHC.Base.Functor (Control.Unification.Types.UTerm t)
instance Data.Foldable.Foldable t => Data.Foldable.Foldable (Control.Unification.Types.UTerm t)
instance Data.Traversable.Traversable t => Data.Traversable.Traversable (Control.Unification.Types.UTerm t)
instance GHC.Base.Functor t => GHC.Base.Applicative (Control.Unification.Types.UTerm t)
instance GHC.Base.Functor t => GHC.Base.Monad (Control.Unification.Types.UTerm t)
instance GHC.Base.Alternative t => GHC.Base.Alternative (Control.Unification.Types.UTerm t)
instance (GHC.Base.Functor t, GHC.Base.MonadPlus t) => GHC.Base.MonadPlus (Control.Unification.Types.UTerm t)


-- | This module defines an implementation of unification variables using
--   the <a>ST</a> monad.
module Control.Unification.STVar

-- | Unification variables implemented by <a>STRef</a>s. In addition to the
--   <tt>STRef</tt> for the term itself, we also track the variable's ID
--   (to support visited-sets).
data STVar s t

-- | A monad for handling <a>STVar</a> bindings.
data STBinding s a

-- | Run the <a>ST</a> ranked binding monad. N.B., because <a>STVar</a> are
--   rank-2 quantified, this guarantees that the return value has no such
--   references. However, in order to remove the references from terms,
--   you'll need to explicitly apply the bindings and ground the term.
runSTBinding :: (forall s. STBinding s a) -> a
instance GHC.Base.Functor (Control.Unification.STVar.STBinding s)
instance GHC.Base.Applicative (Control.Unification.STVar.STBinding s)
instance GHC.Base.Monad (Control.Unification.STVar.STBinding s)
instance Control.Unification.Types.Unifiable t => Control.Unification.Types.BindingMonad t (Control.Unification.STVar.STVar s t) (Control.Unification.STVar.STBinding s)
instance GHC.Show.Show (Control.Unification.STVar.STVar s t)
instance GHC.Classes.Eq (Control.Unification.STVar.STVar s t)
instance Control.Unification.Types.Variable (Control.Unification.STVar.STVar s t)


-- | A ranked variant of <a>Control.Unification.STVar</a>.
module Control.Unification.Ranked.STVar

-- | A ranked unification variable implemented by <a>STRef</a>s. In
--   addition to the <tt>STRef</tt> for the term itself, we also track the
--   variable's ID (to support visited-sets) and rank (to support weighted
--   path compression).
data STRVar s t

-- | A monad for handling <a>STRVar</a> bindings.
data STRBinding s a

-- | Run the <a>ST</a> ranked binding monad. N.B., because <a>STRVar</a>
--   are rank-2 quantified, this guarantees that the return value has no
--   such references. However, in order to remove the references from
--   terms, you'll need to explicitly apply the bindings.
runSTRBinding :: (forall s. STRBinding s a) -> a
instance GHC.Base.Functor (Control.Unification.Ranked.STVar.STRBinding s)
instance GHC.Base.Applicative (Control.Unification.Ranked.STVar.STRBinding s)
instance GHC.Base.Monad (Control.Unification.Ranked.STVar.STRBinding s)
instance Control.Unification.Types.Unifiable t => Control.Unification.Types.BindingMonad t (Control.Unification.Ranked.STVar.STRVar s t) (Control.Unification.Ranked.STVar.STRBinding s)
instance Control.Unification.Types.Unifiable t => Control.Unification.Types.RankedBindingMonad t (Control.Unification.Ranked.STVar.STRVar s t) (Control.Unification.Ranked.STVar.STRBinding s)
instance GHC.Show.Show (Control.Unification.Ranked.STVar.STRVar s t)
instance GHC.Classes.Eq (Control.Unification.Ranked.STVar.STRVar s t)
instance Control.Unification.Types.Variable (Control.Unification.Ranked.STVar.STRVar s t)


-- | This module defines a state monad for functional pointers represented
--   by integers as keys into an <tt>IntMap</tt>. This technique was
--   independently discovered by Dijkstra et al. This module extends the
--   approach by using a state monad transformer, which can be made into a
--   backtracking state monad by setting the underlying monad to some
--   <a>MonadLogic</a> (part of the <tt>logict</tt> library, described by
--   Kiselyov et al.).
--   
--   <ul>
--   <li>Atze Dijkstra, Arie Middelkoop, S. Doaitse Swierstra (2008)
--   <i>Efficient Functional Unification and Substitution</i>, Technical
--   Report UU-CS-2008-027, Utrecht University.</li>
--   <li>Oleg Kiselyov, Chung-chieh Shan, Daniel P. Friedman, and Amr Sabry
--   (2005) <i>Backtracking, Interleaving, and</i> <i>Terminating Monad
--   Transformers</i>, ICFP.</li>
--   </ul>
module Control.Unification.IntVar

-- | A "mutable" unification variable implemented by an integer. This
--   provides an entirely pure alternative to truly mutable alternatives
--   (like <tt>STVar</tt>), which can make backtracking easier.
--   
--   N.B., because this implementation is pure, we can use it for both
--   ranked and unranked monads.
newtype IntVar
IntVar :: Int -> IntVar

-- | Binding state for <a>IntVar</a>.
data IntBindingState t

-- | A monad for storing <a>IntVar</a> bindings, implemented as a
--   <a>StateT</a>. For a plain state monad, set <tt>m = Identity</tt>; for
--   a backtracking state monad, set <tt>m = Logic</tt>.
data IntBindingT t m a
runIntBindingT :: IntBindingT t m a -> m (a, IntBindingState t)

-- | N.B., you should explicitly apply bindings before calling this
--   function, or else the bindings will be lost
evalIntBindingT :: (Monad m) => IntBindingT t m a -> m a
execIntBindingT :: (Monad m) => IntBindingT t m a -> m (IntBindingState t)
instance GHC.Classes.Eq Control.Unification.IntVar.IntVar
instance GHC.Show.Show Control.Unification.IntVar.IntVar
instance GHC.Base.Functor m => GHC.Base.Functor (Control.Unification.IntVar.IntBindingT t m)
instance (GHC.Base.Functor m, GHC.Base.Monad m) => GHC.Base.Applicative (Control.Unification.IntVar.IntBindingT t m)
instance GHC.Base.Monad m => GHC.Base.Monad (Control.Unification.IntVar.IntBindingT t m)
instance Control.Monad.Trans.Class.MonadTrans (Control.Unification.IntVar.IntBindingT t)
instance (GHC.Base.Functor m, GHC.Base.MonadPlus m) => GHC.Base.Alternative (Control.Unification.IntVar.IntBindingT t m)
instance GHC.Base.MonadPlus m => GHC.Base.MonadPlus (Control.Unification.IntVar.IntBindingT t m)
instance GHC.Base.Monad m => Control.Monad.State.Class.MonadState (Control.Unification.IntVar.IntBindingState t) (Control.Unification.IntVar.IntBindingT t m)
instance Control.Monad.Logic.Class.MonadLogic m => Control.Monad.Logic.Class.MonadLogic (Control.Unification.IntVar.IntBindingT t m)
instance (Control.Unification.Types.Unifiable t, GHC.Base.Applicative m, GHC.Base.Monad m) => Control.Unification.Types.BindingMonad t Control.Unification.IntVar.IntVar (Control.Unification.IntVar.IntBindingT t m)
instance GHC.Show.Show (t (Control.Unification.Types.UTerm t Control.Unification.IntVar.IntVar)) => GHC.Show.Show (Control.Unification.IntVar.IntBindingState t)
instance Control.Unification.Types.Variable Control.Unification.IntVar.IntVar


-- | A ranked variant of <a>Control.Unification.IntVar</a>.
module Control.Unification.Ranked.IntVar

-- | A "mutable" unification variable implemented by an integer. This
--   provides an entirely pure alternative to truly mutable alternatives
--   (like <tt>STVar</tt>), which can make backtracking easier.
--   
--   N.B., because this implementation is pure, we can use it for both
--   ranked and unranked monads.
newtype IntVar
IntVar :: Int -> IntVar

-- | Ranked binding state for <a>IntVar</a>.
data IntRBindingState t

-- | A monad for storing <a>IntVar</a> bindings, implemented as a
--   <a>StateT</a>. For a plain state monad, set <tt>m = Identity</tt>; for
--   a backtracking state monad, set <tt>m = Logic</tt>.
data IntRBindingT t m a
runIntRBindingT :: IntRBindingT t m a -> m (a, IntRBindingState t)

-- | N.B., you should explicitly apply bindings before calling this
--   function, or else the bindings will be lost
evalIntRBindingT :: (Monad m) => IntRBindingT t m a -> m a
execIntRBindingT :: (Monad m) => IntRBindingT t m a -> m (IntRBindingState t)
instance GHC.Base.Functor m => GHC.Base.Functor (Control.Unification.Ranked.IntVar.IntRBindingT t m)
instance (GHC.Base.Functor m, GHC.Base.Monad m) => GHC.Base.Applicative (Control.Unification.Ranked.IntVar.IntRBindingT t m)
instance GHC.Base.Monad m => GHC.Base.Monad (Control.Unification.Ranked.IntVar.IntRBindingT t m)
instance Control.Monad.Trans.Class.MonadTrans (Control.Unification.Ranked.IntVar.IntRBindingT t)
instance (GHC.Base.Functor m, GHC.Base.MonadPlus m) => GHC.Base.Alternative (Control.Unification.Ranked.IntVar.IntRBindingT t m)
instance GHC.Base.MonadPlus m => GHC.Base.MonadPlus (Control.Unification.Ranked.IntVar.IntRBindingT t m)
instance GHC.Base.Monad m => Control.Monad.State.Class.MonadState (Control.Unification.Ranked.IntVar.IntRBindingState t) (Control.Unification.Ranked.IntVar.IntRBindingT t m)
instance Control.Monad.Logic.Class.MonadLogic m => Control.Monad.Logic.Class.MonadLogic (Control.Unification.Ranked.IntVar.IntRBindingT t m)
instance (Control.Unification.Types.Unifiable t, GHC.Base.Applicative m, GHC.Base.Monad m) => Control.Unification.Types.BindingMonad t Control.Unification.IntVar.IntVar (Control.Unification.Ranked.IntVar.IntRBindingT t m)
instance (Control.Unification.Types.Unifiable t, GHC.Base.Applicative m, GHC.Base.Monad m) => Control.Unification.Types.RankedBindingMonad t Control.Unification.IntVar.IntVar (Control.Unification.Ranked.IntVar.IntRBindingT t m)
instance GHC.Show.Show (t (Control.Unification.Types.UTerm t Control.Unification.IntVar.IntVar)) => GHC.Show.Show (Control.Unification.Ranked.IntVar.IntRBindingState t)


-- | This module provides first-order structural unification over general
--   structure types. It also provides the standard suite of functions
--   accompanying unification (applying bindings, getting free variables,
--   etc.).
--   
--   The implementation makes use of numerous optimization techniques.
--   First, we use path compression everywhere (for weighted path
--   compression see <a>Control.Unification.Ranked</a>). Second, we replace
--   the occurs-check with visited-sets. Third, we use a technique for
--   aggressive opportunistic observable sharing; that is, we track as much
--   sharing as possible in the bindings (without introducing new
--   variables), so that we can compare bound variables directly and
--   therefore eliminate redundant unifications.
module Control.Unification

-- | The type of terms generated by structures <tt>t</tt> over variables
--   <tt>v</tt>. The structure type should implement <a>Unifiable</a> and
--   the variable type should implement <a>Variable</a>.
--   
--   The <a>Show</a> instance doesn't show the constructors, in order to
--   improve legibility for large terms.
--   
--   All the category theoretic instances (<a>Functor</a>, <a>Foldable</a>,
--   <a>Traversable</a>,...) are provided because they are often useful;
--   however, beware that since the implementations must be pure, they
--   cannot read variables bound in the current context and therefore can
--   create incoherent results. Therefore, you should apply the current
--   bindings before using any of the functions provided by those classes.
data UTerm t v

-- | A unification variable.
UVar :: !v -> UTerm t v

-- | Some structure containing subterms.
UTerm :: !(t (UTerm t v)) -> UTerm t v

-- | <i>O(n)</i>. Extract a pure term from a mutable term, or return
--   <tt>Nothing</tt> if the mutable term actually contains variables.
--   N.B., this function is pure, so you should manually apply bindings
--   before calling it.
freeze :: (Traversable t) => UTerm t v -> Maybe (Fix t)

-- | <i>O(n)</i>. Embed a pure term as a mutable term.
unfreeze :: (Functor t) => Fix t -> UTerm t v

-- | The possible failure modes that could be encountered in unification
--   and related functions. While many of the functions could be given more
--   accurate types if we used ad-hoc combinations of these constructors
--   (i.e., because they can only throw one of the errors), the extra
--   complexity is not considered worth it.
--   
--   This is a finally-tagless encoding of the <a>UFailure</a> data type so
--   that we can abstract over clients adding additional domain-specific
--   failure modes, introducing monoid instances, etc.
--   
--   <i>Since: 0.10.0</i>
class Fallible t v a

-- | A cyclic term was encountered (i.e., the variable occurs free in a
--   term it would have to be bound to in order to succeed). Infinite terms
--   like this are not generally acceptable, so we do not support them. In
--   logic programming this should simply be treated as unification
--   failure; in type checking this should result in a "could not construct
--   infinite type <tt>a = Foo a</tt>" error.
--   
--   Note that since, by default, the library uses visited-sets instead of
--   the occurs-check these errors will be thrown at the point where the
--   cycle is dereferenced/unrolled (e.g., when applying bindings), instead
--   of at the time when the cycle is created. However, the arguments to
--   this constructor should express the same context as if we had
--   performed the occurs-check, in order for error messages to be
--   intelligable.
occursFailure :: Fallible t v a => v -> UTerm t v -> a

-- | The top-most level of the terms do not match (according to
--   <a>zipMatch</a>). In logic programming this should simply be treated
--   as unification failure; in type checking this should result in a
--   "could not match expected type <tt>Foo</tt> with inferred type
--   <tt>Bar</tt>" error.
mismatchFailure :: Fallible t v a => t (UTerm t v) -> t (UTerm t v) -> a

-- | An implementation of syntactically unifiable structure. The
--   <tt>Traversable</tt> constraint is there because we also require terms
--   to be functors and require the distributivity of <a>sequence</a> or
--   <a>mapM</a>.
class (Traversable t) => Unifiable t

-- | Perform one level of equality testing for terms. If the term
--   constructors are unequal then return <tt>Nothing</tt>; if they are
--   equal, then return the one-level spine filled with resolved subterms
--   and/or pairs of subterms to be recursively checked.
zipMatch :: Unifiable t => t a -> t a -> Maybe (t (Either a (a, a)))

-- | An implementation of unification variables. The <a>Eq</a> requirement
--   is to determine whether two variables are equal <i>as variables</i>,
--   without considering what they are bound to. We use <a>Eq</a> rather
--   than having our own <tt>eqVar</tt> method so that clients can make use
--   of library functions which commonly assume <a>Eq</a>.
class (Eq v) => Variable v

-- | Return a unique identifier for this variable, in order to support the
--   use of visited-sets instead of occurs-checks. This function must
--   satisfy the following coherence law with respect to the <a>Eq</a>
--   instance:
--   
--   <tt>x == y</tt> if and only if <tt>getVarID x == getVarID y</tt>
getVarID :: Variable v => v -> Int

-- | The basic class for generating, reading, and writing to bindings
--   stored in a monad. These three functionalities could be split apart,
--   but are combined in order to simplify contexts. Also, because most
--   functions reading bindings will also perform path compression, there's
--   no way to distinguish "true" mutation from mere path compression.
--   
--   The superclass constraints are there to simplify contexts, since we
--   make the same assumptions everywhere we use <tt>BindingMonad</tt>.
class (Unifiable t, Variable v, Applicative m, Monad m) => BindingMonad t v m | m t -> v, v m -> t

-- | Given a variable pointing to <tt>UTerm t v</tt>, return the term it's
--   bound to, or <tt>Nothing</tt> if the variable is unbound.
lookupVar :: BindingMonad t v m => v -> m (Maybe (UTerm t v))

-- | Generate a new free variable guaranteed to be fresh in <tt>m</tt>.
freeVar :: BindingMonad t v m => m v

-- | Generate a new variable (fresh in <tt>m</tt>) bound to the given term.
--   The default implementation is:
--   
--   <pre>
--   newVar t = do { v &lt;- freeVar ; bindVar v t ; return v }
--   </pre>
newVar :: BindingMonad t v m => UTerm t v -> m v

-- | Bind a variable to a term, overriding any previous binding.
bindVar :: BindingMonad t v m => v -> UTerm t v -> m ()

-- | Walk a term and determine which variables are still free. N.B., this
--   function does not detect cyclic terms (i.e., throw errors), but it
--   will return the correct answer for them in finite time.
getFreeVars :: (BindingMonad t v m) => UTerm t v -> m [v]

-- | Apply the current bindings from the monad so that any remaining
--   variables in the result must, therefore, be free. N.B., this
--   expensively clones term structure and should only be performed when a
--   pure term is needed, or when <a>occursFailure</a> exceptions must be
--   forced. This function <i>does</i> preserve sharing, however that
--   sharing is no longer observed by the monad.
--   
--   If any cyclic bindings are detected, then an <a>occursFailure</a>
--   exception will be thrown.
applyBindings :: (BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m), MonadError e (em m)) => UTerm t v -> em m (UTerm t v)

-- | Freshen all variables in a term, both bound and free. This ensures
--   that the observability of sharing is maintained, while freshening the
--   free variables. N.B., this expensively clones term structure and
--   should only be performed when necessary.
--   
--   If any cyclic bindings are detected, then an <a>occursFailure</a>
--   exception will be thrown.
freshen :: (BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m), MonadError e (em m)) => UTerm t v -> em m (UTerm t v)

-- | <a>equals</a>
(===) :: (BindingMonad t v m) => UTerm t v -> UTerm t v -> m Bool
infix 4 ===

-- | <a>equiv</a>
(=~=) :: (BindingMonad t v m) => UTerm t v -> UTerm t v -> m (Maybe (IntMap Int))
infix 4 =~=

-- | <a>unify</a>
(=:=) :: (BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m), MonadError e (em m)) => UTerm t v -> UTerm t v -> em m (UTerm t v)
infix 4 =:=

-- | <a>subsumes</a>
(<:=) :: (BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m), MonadError e (em m)) => UTerm t v -> UTerm t v -> em m Bool
infix 4 <:=

-- | Determine if two terms are structurally equal. This is essentially
--   equivalent to <tt>(<a>==</a>)</tt> except that it does not require
--   applying bindings before comparing, so it is more efficient. N.B.,
--   this function does not consider alpha-variance, and thus variables
--   with different names are considered unequal. Cf., <a>equiv</a>.
equals :: (BindingMonad t v m) => UTerm t v -> UTerm t v -> m Bool
infix 4 `equals`

-- | Determine if two terms are structurally equivalent; that is,
--   structurally equal modulo renaming of free variables. Returns a
--   mapping from variable IDs of the left term to variable IDs of the
--   right term, indicating the renaming used.
equiv :: (BindingMonad t v m) => UTerm t v -> UTerm t v -> m (Maybe (IntMap Int))
infix 4 `equiv`

-- | Unify two terms, or throw an error with an explanation of why
--   unification failed. Since bindings are stored in the monad, the two
--   input terms and the output term are all equivalent if unification
--   succeeds. However, the returned value makes use of aggressive
--   opportunistic observable sharing, so it will be more efficient to use
--   it in future calculations than either argument.
unify :: (BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m), MonadError e (em m)) => UTerm t v -> UTerm t v -> em m (UTerm t v)
infix 4 `unify`

-- | A variant of <a>unify</a> which uses <a>occursIn</a> instead of
--   visited-sets. This should only be used when eager throwing of
--   <a>occursFailure</a> errors is absolutely essential (or for testing
--   the correctness of <tt>unify</tt>). Performing the occurs-check is
--   expensive. Not only is it slow, it's asymptotically slow since it can
--   cause the same subterm to be traversed multiple times.
unifyOccurs :: (BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m), MonadError e (em m)) => UTerm t v -> UTerm t v -> em m (UTerm t v)

-- | Determine whether the left term subsumes the right term. That is,
--   whereas <tt>(tl =:= tr)</tt> will compute the most general
--   substitution <tt>s</tt> such that <tt>(s tl === s tr)</tt>, <tt>(tl
--   &lt;:= tr)</tt> computes the most general substitution <tt>s</tt> such
--   that <tt>(s tl === tr)</tt>. This means that <tt>tl</tt> is less
--   defined than and consistent with <tt>tr</tt>.
--   
--   <i>N.B.</i>, this function updates the monadic bindings just like
--   <a>unify</a> does. However, while the use cases for unification often
--   want to keep the bindings around, the use cases for subsumption
--   usually do not. Thus, you'll probably want to use a binding monad
--   which supports backtracking in order to undo the changes.
--   Unfortunately, leaving the monadic bindings unaltered and returning
--   the necessary substitution directly imposes a performance penalty or
--   else requires specifying too much about the implementation of
--   variables.
subsumes :: (BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m), MonadError e (em m)) => UTerm t v -> UTerm t v -> em m Bool
infix 4 `subsumes`

-- | Same as <a>getFreeVars</a>, but works on several terms simultaneously.
--   This is more efficient than getting the free variables for each of the
--   terms separately because we can make use of sharing across the whole
--   collection. That is, each time we move to the next term, we still
--   remember the bound variables we've already looked at (and therefore do
--   not need to traverse, since we've already seen whatever free variables
--   there are down there); whereas we would forget between each call to
--   <tt>getFreeVars</tt>.
--   
--   <i>Since: 0.7.0</i>
getFreeVarsAll :: (BindingMonad t v m, Foldable s) => s (UTerm t v) -> m [v]

-- | Same as <a>applyBindings</a>, but works on several terms
--   simultaneously. This function preserves sharing across the entire
--   collection of terms, whereas applying the bindings to each term
--   separately would only preserve sharing within each term.
--   
--   <i>Since: 0.7.0</i>
applyBindingsAll :: (BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m), MonadError e (em m), Traversable s) => s (UTerm t v) -> em m (s (UTerm t v))

-- | Same as <a>freshen</a>, but works on several terms simultaneously.
--   This is different from freshening each term separately, because
--   <tt>freshenAll</tt> preserves the relationship between the terms. For
--   instance, the result of
--   
--   <pre>
--   mapM freshen [UVar 1, UVar 1]
--   </pre>
--   
--   would be <tt>[UVar 2, UVar 3]</tt> or something alpha-equivalent,
--   whereas the result of
--   
--   <pre>
--   freshenAll [UVar 1, UVar 1]
--   </pre>
--   
--   would be <tt>[UVar 2, UVar 2]</tt> or something alpha-equivalent.
--   
--   <i>Since: 0.7.0</i>
freshenAll :: (BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m), MonadError e (em m), Traversable s) => s (UTerm t v) -> em m (s (UTerm t v))

-- | Canonicalize a chain of variables so they all point directly to the
--   term at the end of the chain (or the free variable, if the chain is
--   unbound), and return that end.
--   
--   N.B., this is almost never the function you want. Cf.,
--   <a>semiprune</a>.
fullprune :: (BindingMonad t v m) => UTerm t v -> m (UTerm t v)

-- | Canonicalize a chain of variables so they all point directly to the
--   last variable in the chain, regardless of whether it is bound or not.
--   This allows detecting many cases where multiple variables point to the
--   same term, thereby allowing us to avoid re-unifying the term they
--   point to.
semiprune :: (BindingMonad t v m) => UTerm t v -> m (UTerm t v)

-- | Determine if a variable appears free somewhere inside a term. Since
--   occurs checks only make sense when we're about to bind the variable to
--   the term, we do not bother checking for the possibility of the
--   variable occuring bound in the term.
occursIn :: (BindingMonad t v m) => v -> UTerm t v -> m Bool


-- | This module provides the API of <a>Control.Unification</a> except
--   using <a>RankedBindingMonad</a> where appropriate. This module (and
--   the binding implementations for it) are highly experimental and
--   subject to change in future versions.
module Control.Unification.Ranked

-- | Walk a term and determine which variables are still free. N.B., this
--   function does not detect cyclic terms (i.e., throw errors), but it
--   will return the correct answer for them in finite time.
getFreeVars :: (BindingMonad t v m) => UTerm t v -> m [v]

-- | Apply the current bindings from the monad so that any remaining
--   variables in the result must, therefore, be free. N.B., this
--   expensively clones term structure and should only be performed when a
--   pure term is needed, or when <a>occursFailure</a> exceptions must be
--   forced. This function <i>does</i> preserve sharing, however that
--   sharing is no longer observed by the monad.
--   
--   If any cyclic bindings are detected, then an <a>occursFailure</a>
--   exception will be thrown.
applyBindings :: (BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m), MonadError e (em m)) => UTerm t v -> em m (UTerm t v)

-- | Freshen all variables in a term, both bound and free. This ensures
--   that the observability of sharing is maintained, while freshening the
--   free variables. N.B., this expensively clones term structure and
--   should only be performed when necessary.
--   
--   If any cyclic bindings are detected, then an <a>occursFailure</a>
--   exception will be thrown.
freshen :: (BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m), MonadError e (em m)) => UTerm t v -> em m (UTerm t v)

-- | <a>equals</a>
(===) :: (BindingMonad t v m) => UTerm t v -> UTerm t v -> m Bool
infix 4 ===

-- | <a>equiv</a>
(=~=) :: (BindingMonad t v m) => UTerm t v -> UTerm t v -> m (Maybe (IntMap Int))
infix 4 =~=

-- | <a>unify</a>
(=:=) :: (RankedBindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m), MonadError e (em m)) => UTerm t v -> UTerm t v -> em m (UTerm t v)
infix 4 =:=

-- | Determine if two terms are structurally equal. This is essentially
--   equivalent to <tt>(<a>==</a>)</tt> except that it does not require
--   applying bindings before comparing, so it is more efficient. N.B.,
--   this function does not consider alpha-variance, and thus variables
--   with different names are considered unequal. Cf., <a>equiv</a>.
equals :: (BindingMonad t v m) => UTerm t v -> UTerm t v -> m Bool
infix 4 `equals`

-- | Determine if two terms are structurally equivalent; that is,
--   structurally equal modulo renaming of free variables. Returns a
--   mapping from variable IDs of the left term to variable IDs of the
--   right term, indicating the renaming used.
equiv :: (BindingMonad t v m) => UTerm t v -> UTerm t v -> m (Maybe (IntMap Int))
infix 4 `equiv`

-- | Unify two terms, or throw an error with an explanation of why
--   unification failed. Since bindings are stored in the monad, the two
--   input terms and the output term are all equivalent if unification
--   succeeds. However, the returned value makes use of aggressive
--   opportunistic observable sharing, so it will be more efficient to use
--   it in future calculations than either argument.
unify :: (RankedBindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m), MonadError e (em m)) => UTerm t v -> UTerm t v -> em m (UTerm t v)
infix 4 `unify`

-- | Same as <a>getFreeVars</a>, but works on several terms simultaneously.
--   This is more efficient than getting the free variables for each of the
--   terms separately because we can make use of sharing across the whole
--   collection. That is, each time we move to the next term, we still
--   remember the bound variables we've already looked at (and therefore do
--   not need to traverse, since we've already seen whatever free variables
--   there are down there); whereas we would forget between each call to
--   <tt>getFreeVars</tt>.
--   
--   <i>Since: 0.7.0</i>
getFreeVarsAll :: (BindingMonad t v m, Foldable s) => s (UTerm t v) -> m [v]

-- | Same as <a>applyBindings</a>, but works on several terms
--   simultaneously. This function preserves sharing across the entire
--   collection of terms, whereas applying the bindings to each term
--   separately would only preserve sharing within each term.
--   
--   <i>Since: 0.7.0</i>
applyBindingsAll :: (BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m), MonadError e (em m), Traversable s) => s (UTerm t v) -> em m (s (UTerm t v))

-- | Same as <a>freshen</a>, but works on several terms simultaneously.
--   This is different from freshening each term separately, because
--   <tt>freshenAll</tt> preserves the relationship between the terms. For
--   instance, the result of
--   
--   <pre>
--   mapM freshen [UVar 1, UVar 1]
--   </pre>
--   
--   would be <tt>[UVar 2, UVar 3]</tt> or something alpha-equivalent,
--   whereas the result of
--   
--   <pre>
--   freshenAll [UVar 1, UVar 1]
--   </pre>
--   
--   would be <tt>[UVar 2, UVar 2]</tt> or something alpha-equivalent.
--   
--   <i>Since: 0.7.0</i>
freshenAll :: (BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m), MonadError e (em m), Traversable s) => s (UTerm t v) -> em m (s (UTerm t v))
