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


-- | Generic first-order unification
--   
--   Generic first-order unification
@package monad-unify
@version 0.2.2


module Control.Monad.Unify

-- | Untyped unification variables
type Unknown = Int

-- | A type which can contain unification variables
class Partial t
unknown :: Partial t => Unknown -> t
isUnknown :: Partial t => t -> Maybe Unknown
unknowns :: Partial t => t -> [Unknown]
($?) :: Partial t => Substitution t -> t -> t

-- | Identifies types which support unification
class Partial t => Unifiable m t | t -> m
(=?=) :: Unifiable m t => t -> t -> UnifyT t m ()

-- | A substitution maintains a mapping from unification variables to their
--   values
data Substitution t
Substitution :: HashMap Int t -> Substitution t
runSubstitution :: Substitution t -> HashMap Int t

-- | State required for type checking
data UnifyState t
UnifyState :: Int -> Substitution t -> UnifyState t

-- | The next fresh unification variable
unifyNextVar :: UnifyState t -> Int

-- | The current substitution
unifyCurrentSubstitution :: UnifyState t -> Substitution t

-- | An empty <tt>UnifyState</tt>
defaultUnifyState :: Partial t => UnifyState t

-- | The type checking monad, which provides the state of the type checker,
--   and error reporting capabilities
newtype UnifyT t m a
UnifyT :: StateT (UnifyState t) m a -> UnifyT t m a
unUnify :: UnifyT t m a -> StateT (UnifyState t) m a

-- | Run a computation in the Unify monad, failing with an error, or
--   succeeding with a return value and the new next unification variable
runUnify :: UnifyState t -> UnifyT t m a -> m (a, UnifyState t)

-- | Substitute a single unification variable
substituteOne :: Partial t => Unknown -> t -> Substitution t

-- | Replace a unification variable with the specified value in the current
--   substitution
(=:=) :: (Error e, Monad m, MonadError e m, Unifiable m t) => Unknown -> t -> UnifyT t m ()

-- | Perform the occurs check, to make sure a unification variable does not
--   occur inside a value
occursCheck :: (Error e, Monad m, MonadError e m, Partial t) => Unknown -> t -> UnifyT t m ()

-- | Generate a fresh untyped unification variable
fresh' :: Monad m => UnifyT t m Unknown

-- | Generate a fresh unification variable at a specific type
fresh :: (Monad m, Partial t) => UnifyT t m t
instance Functor m => Functor (UnifyT t m)
instance Monad m => Monad (UnifyT t m)
instance (Monad m, Functor m) => Applicative (UnifyT t m)
instance MonadPlus m => MonadPlus (UnifyT t m)
instance MonadError e m => MonadError e (UnifyT t m)
instance MonadState s m => MonadState s (UnifyT t m)
instance Partial t => Monoid (Substitution t)
