-- Required for Show instances
{-# LANGUAGE FlexibleContexts, UndecidableInstances #-}
-- Required for cleaning up Haddock messages for GHC 7.10
{-# LANGUAGE CPP #-}
-- For the generic Unifiable instances. N.B., while the lower bound
-- for 'Generic1' stuff is nominally base-4.6.0, those early versions
-- lack a 'Traversable' instance, making them useless for us. Thus,
-- the actual lower bound is GHC-8.0.2 aka base-4.9.1.0.
#if MIN_VERSION_base(4,9,1)
{-# LANGUAGE TypeOperators
           , ScopedTypeVariables
           , DefaultSignatures
           #-}
#endif
-- Required more generally
{-# LANGUAGE MultiParamTypeClasses
           , FunctionalDependencies
           , FlexibleInstances
           #-}
{-# OPTIONS_GHC -Wall -fwarn-tabs #-}

-- HACK: in GHC 7.10, Haddock complains about unused imports; but,
-- if we use CPP to avoid including them under Haddock, then it
-- will fail!
#ifdef __HADDOCK__
{-# OPTIONS_GHC -fno-warn-unused-imports #-}
#endif

----------------------------------------------------------------
--                                                  ~ 2017.06.21
-- |
-- Module      :  Control.Unification.Types
-- Copyright   :  Copyright (c) 2007--2017 wren gayle romano
-- License     :  BSD
-- Maintainer  :  wren@community.haskell.org
-- Stability   :  experimental
-- Portability :  semi-portable (MPTCs, fundeps,...)
--
-- This module defines the classes and primitive types used by
-- unification and related functions.
----------------------------------------------------------------
module Control.Unification.Types
    (
    -- * Unification terms
      UTerm(..)
    , freeze
    , unfreeze
    -- * Errors
    , Fallible(..)
    , UFailure(..)
    -- * Basic type classes
    , Unifiable(..)
    , Variable(..)
    , BindingMonad(..)
    -- * Weighted path compression
    , Rank(..)
    , RankedBindingMonad(..)
    ) where

import Prelude hiding (mapM, sequence, foldr, foldr1, foldl, foldl1)

import Data.Word               (Word8)
import Data.Functor.Fixedpoint (Fix(..), unFix)
#if __GLASGOW_HASKELL__ < 810
import Data.Monoid             ((<>))
#endif
import Data.Traversable        (Traversable(..))
#if __GLASGOW_HASKELL__ < 710
import Data.Foldable           (Foldable(..))
import Control.Applicative     (Applicative(..), (<$>))
#endif
#if MIN_VERSION_base(4,9,1)
-- for the generic Unifiable instances
import GHC.Generics
#endif

----------------------------------------------------------------
----------------------------------------------------------------

-- TODO: incorporate Ed's cheaper free monads, at least as a view.

-- | The type of terms generated by structures @t@ over variables
-- @v@. The structure type should implement 'Unifiable' and the
-- variable type should implement 'Variable'.
--
-- The 'Show' instance doesn't show the constructors, in order to
-- improve legibility for large terms.
--
-- All the category theoretic instances ('Functor', 'Foldable',
-- 'Traversable',...) 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
    = UVar  !v               -- ^ A unification variable.
    | UTerm !(t (UTerm t v)) -- ^ Some structure containing subterms.

instance (Show v, Show (t (UTerm t v))) => Show (UTerm t v) where
    showsPrec :: Int -> UTerm t v -> ShowS
showsPrec Int
p (UVar  v
v) = Int -> v -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p v
v
    showsPrec Int
p (UTerm t (UTerm t v)
t) = Int -> t (UTerm t v) -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p t (UTerm t v)
t

instance (Functor t) => Functor (UTerm t) where
    fmap :: (a -> b) -> UTerm t a -> UTerm t b
fmap a -> b
f (UVar  a
v) = b -> UTerm t b
forall (t :: * -> *) v. v -> UTerm t v
UVar  (a -> b
f a
v)
    fmap a -> b
f (UTerm t (UTerm t a)
t) = t (UTerm t b) -> UTerm t b
forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm ((UTerm t a -> UTerm t b) -> t (UTerm t a) -> t (UTerm t b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> b) -> UTerm t a -> UTerm t b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f) t (UTerm t a)
t)

instance (Foldable t) => Foldable (UTerm t) where
    foldMap :: (a -> m) -> UTerm t a -> m
foldMap a -> m
f (UVar  a
v) = a -> m
f a
v
    foldMap a -> m
f (UTerm t (UTerm t a)
t) = (UTerm t a -> m) -> t (UTerm t a) -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((a -> m) -> UTerm t a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f) t (UTerm t a)
t

instance (Traversable t) => Traversable (UTerm t) where
    traverse :: (a -> f b) -> UTerm t a -> f (UTerm t b)
traverse a -> f b
f (UVar  a
v) = b -> UTerm t b
forall (t :: * -> *) v. v -> UTerm t v
UVar  (b -> UTerm t b) -> f b -> f (UTerm t b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
f a
v
    traverse a -> f b
f (UTerm t (UTerm t a)
t) = t (UTerm t b) -> UTerm t b
forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm (t (UTerm t b) -> UTerm t b) -> f (t (UTerm t b)) -> f (UTerm t b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (UTerm t a -> f (UTerm t b)) -> t (UTerm t a) -> f (t (UTerm t b))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((a -> f b) -> UTerm t a -> f (UTerm t b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f b
f) t (UTerm t a)
t

-- Does this even make sense for UTerm? Having variables of function
-- type for @(<*>)@ is very strange; but even if we rephrase things
-- with 'liftA2', we'd still be forming new variables as a function
-- of two old variables, which is still odd...
instance (Functor t) => Applicative (UTerm t) where
    pure :: a -> UTerm t a
pure                  = a -> UTerm t a
forall (t :: * -> *) v. v -> UTerm t v
UVar
    UVar  a -> b
a  <*> :: UTerm t (a -> b) -> UTerm t a -> UTerm t b
<*> UVar  a
b  = b -> UTerm t b
forall (t :: * -> *) v. v -> UTerm t v
UVar  (a -> b
a a
b)
    UVar  a -> b
a  <*> UTerm t (UTerm t a)
mb = t (UTerm t b) -> UTerm t b
forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm ((a -> b) -> UTerm t a -> UTerm t b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
a  (UTerm t a -> UTerm t b) -> t (UTerm t a) -> t (UTerm t b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t (UTerm t a)
mb)
    UTerm t (UTerm t (a -> b))
ma <*> UTerm t a
b        = t (UTerm t b) -> UTerm t b
forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm ((UTerm t (a -> b) -> UTerm t a -> UTerm t b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UTerm t a
b) (UTerm t (a -> b) -> UTerm t b)
-> t (UTerm t (a -> b)) -> t (UTerm t b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t (UTerm t (a -> b))
ma)

-- Does this even make sense for UTerm? It may be helpful for
-- building terms at least; though bind is inefficient for that.
-- Should use the cheaper free...
instance (Functor t) => Monad (UTerm t) where
    return :: a -> UTerm t a
return        = a -> UTerm t a
forall (t :: * -> *) v. v -> UTerm t v
UVar
    UVar  a
v >>= :: UTerm t a -> (a -> UTerm t b) -> UTerm t b
>>= a -> UTerm t b
f = a -> UTerm t b
f a
v
    UTerm t (UTerm t a)
t >>= a -> UTerm t b
f = t (UTerm t b) -> UTerm t b
forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm ((UTerm t a -> (a -> UTerm t b) -> UTerm t b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> UTerm t b
f) (UTerm t a -> UTerm t b) -> t (UTerm t a) -> t (UTerm t b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t (UTerm t a)
t)

{-
-- TODO: how to fill in the missing cases to make these work? In
-- full generality we'd need @Monoid v@ and for it to be a two-sided
-- action over @Alternative t@.
instance (Alternative t) => Alternative (UTerm t) where
    empty               = UTerm empty
    UVar  x <|> UVar  y =
    UVar  x <|> UTerm b =
    UTerm a <|> UVar  y =
    UTerm a <|> UTerm b = UTerm (a <|> b)

instance (Functor t, MonadPlus t) => MonadPlus (UTerm t) where
    mzero                   = UTerm mzero
    UVar  x `mplus` UVar  y =
    UVar  x `mplus` UTerm b =
    UTerm a `mplus` UVar  y =
    UTerm a `mplus` UTerm b = UTerm (a `mplus` b)
-}

-- There's also MonadTrans, MonadWriter, MonadReader, MonadState,
-- MonadError, MonadCont; which make even less sense for us. See
-- Ed Kmett's free package for the implementations.


-- | /O(n)/. Embed a pure term as a mutable term.
unfreeze :: (Functor t) => Fix t -> UTerm t v
unfreeze :: Fix t -> UTerm t v
unfreeze = t (UTerm t v) -> UTerm t v
forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm (t (UTerm t v) -> UTerm t v)
-> (Fix t -> t (UTerm t v)) -> Fix t -> UTerm t v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Fix t -> UTerm t v) -> t (Fix t) -> t (UTerm t v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Fix t -> UTerm t v
forall (t :: * -> *) v. Functor t => Fix t -> UTerm t v
unfreeze (t (Fix t) -> t (UTerm t v))
-> (Fix t -> t (Fix t)) -> Fix t -> t (UTerm t v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fix t -> t (Fix t)
forall (f :: * -> *). Fix f -> f (Fix f)
unFix


-- | /O(n)/. Extract a pure term from a mutable term, or return
-- @Nothing@ 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)
freeze :: UTerm t v -> Maybe (Fix t)
freeze (UVar  v
_) = Maybe (Fix t)
forall a. Maybe a
Nothing
freeze (UTerm t (UTerm t v)
t) = t (Fix t) -> Fix t
forall (f :: * -> *). f (Fix f) -> Fix f
Fix (t (Fix t) -> Fix t) -> Maybe (t (Fix t)) -> Maybe (Fix t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (UTerm t v -> Maybe (Fix t)) -> t (UTerm t v) -> Maybe (t (Fix t))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM UTerm t v -> Maybe (Fix t)
forall (t :: * -> *) v. Traversable t => UTerm t v -> Maybe (Fix t)
freeze t (UTerm t v)
t


----------------------------------------------------------------
-- TODO: provide zipper context so better error messages can be generated.
--
-- | 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 'UFailure' data type
-- so that we can abstract over clients adding additional domain-specific
-- failure modes, introducing monoid instances, etc.
--
-- /Since: 0.10.0/
class Fallible t v a where
    -- | 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
    -- @a = Foo a@\" 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 :: v -> UTerm t v -> a

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


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


instance Fallible t v (UFailure t v) where
    occursFailure :: v -> UTerm t v -> UFailure t v
occursFailure   = v -> UTerm t v -> UFailure t v
forall (t :: * -> *) v. v -> UTerm t v -> UFailure t v
OccursFailure
    mismatchFailure :: t (UTerm t v) -> t (UTerm t v) -> UFailure t v
mismatchFailure = t (UTerm t v) -> t (UTerm t v) -> UFailure t v
forall (t :: * -> *) v.
t (UTerm t v) -> t (UTerm t v) -> UFailure t v
MismatchFailure


-- Can't derive this because it's an UndecidableInstance
instance (Show (t (UTerm t v)), Show v) =>
    Show (UFailure t v)
    where
    showsPrec :: Int -> UFailure t v -> ShowS
showsPrec Int
p (OccursFailure v
v UTerm t v
t) =
        Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9)
            ( String -> ShowS
showString String
"OccursFailure "
            ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> v -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 v
v
            ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" "
            ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> UTerm t v -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 UTerm t v
t
            )
    showsPrec Int
p (MismatchFailure t (UTerm t v)
tl t (UTerm t v)
tr) =
        Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9)
            ( String -> ShowS
showString String
"MismatchFailure "
            ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> t (UTerm t v) -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 t (UTerm t v)
tl
            ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" "
            ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> t (UTerm t v) -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 t (UTerm t v)
tr
            )


instance (Functor t) => Functor (UFailure t) where
    fmap :: (a -> b) -> UFailure t a -> UFailure t b
fmap a -> b
f (OccursFailure a
v UTerm t a
t) =
        b -> UTerm t b -> UFailure t b
forall (t :: * -> *) v. v -> UTerm t v -> UFailure t v
OccursFailure (a -> b
f a
v) ((a -> b) -> UTerm t a -> UTerm t b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f UTerm t a
t)

    fmap a -> b
f (MismatchFailure t (UTerm t a)
tl t (UTerm t a)
tr) =
        t (UTerm t b) -> t (UTerm t b) -> UFailure t b
forall (t :: * -> *) v.
t (UTerm t v) -> t (UTerm t v) -> UFailure t v
MismatchFailure ((a -> b) -> UTerm t a -> UTerm t b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f (UTerm t a -> UTerm t b) -> t (UTerm t a) -> t (UTerm t b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t (UTerm t a)
tl) ((a -> b) -> UTerm t a -> UTerm t b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f (UTerm t a -> UTerm t b) -> t (UTerm t a) -> t (UTerm t b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t (UTerm t a)
tr)

instance (Foldable t) => Foldable (UFailure t) where
    foldMap :: (a -> m) -> UFailure t a -> m
foldMap a -> m
f (OccursFailure a
v UTerm t a
t) =
        a -> m
f a
v m -> m -> m
forall a. Semigroup a => a -> a -> a
<> (a -> m) -> UTerm t a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f UTerm t a
t

    foldMap a -> m
f (MismatchFailure t (UTerm t a)
tl t (UTerm t a)
tr) =
        (UTerm t a -> m) -> t (UTerm t a) -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((a -> m) -> UTerm t a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f) t (UTerm t a)
tl m -> m -> m
forall a. Semigroup a => a -> a -> a
<> (UTerm t a -> m) -> t (UTerm t a) -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((a -> m) -> UTerm t a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f) t (UTerm t a)
tr

instance (Traversable t) => Traversable (UFailure t) where
    traverse :: (a -> f b) -> UFailure t a -> f (UFailure t b)
traverse a -> f b
f (OccursFailure a
v UTerm t a
t) =
        b -> UTerm t b -> UFailure t b
forall (t :: * -> *) v. v -> UTerm t v -> UFailure t v
OccursFailure (b -> UTerm t b -> UFailure t b)
-> f b -> f (UTerm t b -> UFailure t b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
f a
v f (UTerm t b -> UFailure t b) -> f (UTerm t b) -> f (UFailure t b)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (a -> f b) -> UTerm t a -> f (UTerm t b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f b
f UTerm t a
t

    traverse a -> f b
f (MismatchFailure t (UTerm t a)
tl t (UTerm t a)
tr) =
        t (UTerm t b) -> t (UTerm t b) -> UFailure t b
forall (t :: * -> *) v.
t (UTerm t v) -> t (UTerm t v) -> UFailure t v
MismatchFailure (t (UTerm t b) -> t (UTerm t b) -> UFailure t b)
-> f (t (UTerm t b)) -> f (t (UTerm t b) -> UFailure t b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (UTerm t a -> f (UTerm t b)) -> t (UTerm t a) -> f (t (UTerm t b))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((a -> f b) -> UTerm t a -> f (UTerm t b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f b
f) t (UTerm t a)
tl
                        f (t (UTerm t b) -> UFailure t b)
-> f (t (UTerm t b)) -> f (UFailure t b)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (UTerm t a -> f (UTerm t b)) -> t (UTerm t a) -> f (t (UTerm t b))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((a -> f b) -> UTerm t a -> f (UTerm t b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f b
f) t (UTerm t a)
tr

----------------------------------------------------------------

-- | An implementation of syntactically unifiable structure. The
-- @Traversable@ constraint is there because we also require terms
-- to be functors and require the distributivity of 'sequence' or
-- 'mapM'.
--
-- /Updated: 0.11/ This class can now be derived so long as you
-- have a 'Generic1' instance.
class (Traversable t) => Unifiable t where

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

#if MIN_VERSION_base(4,9,1)
    default zipMatch
      :: (Generic1 t, Unifiable (Rep1 t))
      => t a -> t a -> Maybe (t (Either a (a,a)))
    zipMatch t a
a t a
b = Rep1 t (Either a (a, a)) -> t (Either a (a, a))
forall k (f :: k -> *) (a :: k). Generic1 f => Rep1 f a -> f a
to1 (Rep1 t (Either a (a, a)) -> t (Either a (a, a)))
-> Maybe (Rep1 t (Either a (a, a))) -> Maybe (t (Either a (a, a)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Rep1 t a -> Rep1 t a -> Maybe (Rep1 t (Either a (a, a)))
forall (t :: * -> *) a.
Unifiable t =>
t a -> t a -> Maybe (t (Either a (a, a)))
zipMatch (t a -> Rep1 t a
forall k (f :: k -> *) (a :: k). Generic1 f => f a -> Rep1 f a
from1 t a
a) (t a -> Rep1 t a
forall k (f :: k -> *) (a :: k). Generic1 f => f a -> Rep1 f a
from1 t a
b)
#endif


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

    -- | 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 'Eq' instance:
    --
    -- @x == y@ if and only if @getVarID x == getVarID y@
    getVarID :: 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 @BindingMonad@.

class (Unifiable t, Variable v, Applicative m, Monad m) =>
    BindingMonad t v m | m t -> v, v m -> t
    where

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

    -- | Generate a new free variable guaranteed to be fresh in
    -- @m@.
    freeVar :: m v

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

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


----------------------------------------------------------------
-- | The target of variables for 'RankedBindingMonad'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 @log V@, where @V@ is the total number
-- of variables in the unification problem. Thus, A @Word8@ is
-- sufficient for @2^(2^8)@ variables, which is far more than can
-- be indexed by 'getVarID' even on 64-bit architectures.
data Rank t v =
    Rank {-# UNPACK #-} !Word8 !(Maybe (UTerm t v))

-- Can't derive this because it's an UndecidableInstance
instance (Show v, Show (t (UTerm t v))) => Show (Rank t v) where
    show :: Rank t v -> String
show (Rank Word8
n Maybe (UTerm t v)
mb) = String
"Rank "String -> ShowS
forall a. [a] -> [a] -> [a]
++Word8 -> String
forall a. Show a => a -> String
show Word8
nString -> ShowS
forall a. [a] -> [a] -> [a]
++String
" "String -> ShowS
forall a. [a] -> [a] -> [a]
++Maybe (UTerm t v) -> String
forall a. Show a => a -> String
show Maybe (UTerm t v)
mb

-- TODO: flatten the Rank.Maybe.UTerm so that we can tell that if
-- semiprune returns a bound variable then it's bound to a term
-- (not another var)?

{-
instance Monoid (Rank t v) where
    mempty = Rank 0 Nothing
    mappend (Rank l mb) (Rank r _) = Rank (max l r) mb
-}


-- | An advanced class for 'BindingMonad'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 'BindingMonad'.
class (BindingMonad t v m) =>
    RankedBindingMonad t v m | m t -> v, v m -> t
    where

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

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

    -- | Bind a variable to a term and increment the rank at the
    -- same time. The default implementation is:
    --
    -- > incrementBindVar t v = do { incrementRank v ; bindVar v t }
    incrementBindVar :: v -> UTerm t v -> m ()
    incrementBindVar v
v UTerm t v
t = do { v -> m ()
forall (t :: * -> *) v (m :: * -> *).
RankedBindingMonad t v m =>
v -> m ()
incrementRank v
v ; v -> UTerm t v -> m ()
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
v -> UTerm t v -> m ()
bindVar v
v UTerm t v
t }

----------------------------------------------------------------
-- Generic 'Unifiable' instances.

#if MIN_VERSION_base(4,9,1)
instance Unifiable V1 where
    zipMatch :: V1 a -> V1 a -> Maybe (V1 (Either a (a, a)))
zipMatch V1 a
a V1 a
_ = V1 (Either a (a, a)) -> Maybe (V1 (Either a (a, a)))
forall a. a -> Maybe a
Just (V1 (Either a (a, a)) -> Maybe (V1 (Either a (a, a))))
-> V1 (Either a (a, a)) -> Maybe (V1 (Either a (a, a)))
forall a b. (a -> b) -> a -> b
$ a -> Either a (a, a)
forall a b. a -> Either a b
Left (a -> Either a (a, a)) -> V1 a -> V1 (Either a (a, a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> V1 a
a

instance Unifiable U1 where
    zipMatch :: U1 a -> U1 a -> Maybe (U1 (Either a (a, a)))
zipMatch U1 a
a U1 a
_ = U1 (Either a (a, a)) -> Maybe (U1 (Either a (a, a)))
forall a. a -> Maybe a
Just (U1 (Either a (a, a)) -> Maybe (U1 (Either a (a, a))))
-> U1 (Either a (a, a)) -> Maybe (U1 (Either a (a, a)))
forall a b. (a -> b) -> a -> b
$ a -> Either a (a, a)
forall a b. a -> Either a b
Left (a -> Either a (a, a)) -> U1 a -> U1 (Either a (a, a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> U1 a
a

instance Unifiable Par1 where
    zipMatch :: Par1 a -> Par1 a -> Maybe (Par1 (Either a (a, a)))
zipMatch (Par1 a
a) (Par1 a
b) = Par1 (Either a (a, a)) -> Maybe (Par1 (Either a (a, a)))
forall a. a -> Maybe a
Just (Par1 (Either a (a, a)) -> Maybe (Par1 (Either a (a, a))))
-> (Either a (a, a) -> Par1 (Either a (a, a)))
-> Either a (a, a)
-> Maybe (Par1 (Either a (a, a)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either a (a, a) -> Par1 (Either a (a, a))
forall p. p -> Par1 p
Par1 (Either a (a, a) -> Maybe (Par1 (Either a (a, a))))
-> Either a (a, a) -> Maybe (Par1 (Either a (a, a)))
forall a b. (a -> b) -> a -> b
$ (a, a) -> Either a (a, a)
forall a b. b -> Either a b
Right (a
a,a
b)

instance Unifiable f => Unifiable (Rec1 f) where
    zipMatch :: Rec1 f a -> Rec1 f a -> Maybe (Rec1 f (Either a (a, a)))
zipMatch (Rec1 f a
a) (Rec1 f a
b) = f (Either a (a, a)) -> Rec1 f (Either a (a, a))
forall k (f :: k -> *) (p :: k). f p -> Rec1 f p
Rec1 (f (Either a (a, a)) -> Rec1 f (Either a (a, a)))
-> Maybe (f (Either a (a, a))) -> Maybe (Rec1 f (Either a (a, a)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a -> f a -> Maybe (f (Either a (a, a)))
forall (t :: * -> *) a.
Unifiable t =>
t a -> t a -> Maybe (t (Either a (a, a)))
zipMatch f a
a f a
b

instance Eq c => Unifiable (K1 i c) where
    zipMatch :: K1 i c a -> K1 i c a -> Maybe (K1 i c (Either a (a, a)))
zipMatch (K1 c
a) (K1 c
b)
        | c
a c -> c -> Bool
forall a. Eq a => a -> a -> Bool
== c
b    = K1 i c (Either a (a, a)) -> Maybe (K1 i c (Either a (a, a)))
forall a. a -> Maybe a
Just (c -> K1 i c (Either a (a, a))
forall k i c (p :: k). c -> K1 i c p
K1 c
a)
        | Bool
otherwise = Maybe (K1 i c (Either a (a, a)))
forall a. Maybe a
Nothing

instance Unifiable f => Unifiable (M1 i c f) where
    zipMatch :: M1 i c f a -> M1 i c f a -> Maybe (M1 i c f (Either a (a, a)))
zipMatch (M1 f a
a) (M1 f a
b) = f (Either a (a, a)) -> M1 i c f (Either a (a, a))
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (f (Either a (a, a)) -> M1 i c f (Either a (a, a)))
-> Maybe (f (Either a (a, a)))
-> Maybe (M1 i c f (Either a (a, a)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a -> f a -> Maybe (f (Either a (a, a)))
forall (t :: * -> *) a.
Unifiable t =>
t a -> t a -> Maybe (t (Either a (a, a)))
zipMatch f a
a f a
b

instance (Unifiable f, Unifiable g) => Unifiable (f :+: g) where
    zipMatch :: (:+:) f g a -> (:+:) f g a -> Maybe ((:+:) f g (Either a (a, a)))
zipMatch (L1 f a
a) (L1 f a
b) = f (Either a (a, a)) -> (:+:) f g (Either a (a, a))
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (f (Either a (a, a)) -> (:+:) f g (Either a (a, a)))
-> Maybe (f (Either a (a, a)))
-> Maybe ((:+:) f g (Either a (a, a)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a -> f a -> Maybe (f (Either a (a, a)))
forall (t :: * -> *) a.
Unifiable t =>
t a -> t a -> Maybe (t (Either a (a, a)))
zipMatch f a
a f a
b
    zipMatch (R1 g a
a) (R1 g a
b) = g (Either a (a, a)) -> (:+:) f g (Either a (a, a))
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (g (Either a (a, a)) -> (:+:) f g (Either a (a, a)))
-> Maybe (g (Either a (a, a)))
-> Maybe ((:+:) f g (Either a (a, a)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> g a -> Maybe (g (Either a (a, a)))
forall (t :: * -> *) a.
Unifiable t =>
t a -> t a -> Maybe (t (Either a (a, a)))
zipMatch g a
a g a
b
    zipMatch (:+:) f g a
_ (:+:) f g a
_ = Maybe ((:+:) f g (Either a (a, a)))
forall a. Maybe a
Nothing

instance (Unifiable f, Unifiable g) => Unifiable (f :*: g) where
    zipMatch :: (:*:) f g a -> (:*:) f g a -> Maybe ((:*:) f g (Either a (a, a)))
zipMatch (f a
a1 :*: g a
a2) (f a
b1 :*: g a
b2) =
        f (Either a (a, a))
-> g (Either a (a, a)) -> (:*:) f g (Either a (a, a))
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
(:*:) (f (Either a (a, a))
 -> g (Either a (a, a)) -> (:*:) f g (Either a (a, a)))
-> Maybe (f (Either a (a, a)))
-> Maybe (g (Either a (a, a)) -> (:*:) f g (Either a (a, a)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a -> f a -> Maybe (f (Either a (a, a)))
forall (t :: * -> *) a.
Unifiable t =>
t a -> t a -> Maybe (t (Either a (a, a)))
zipMatch f a
a1 f a
b1 Maybe (g (Either a (a, a)) -> (:*:) f g (Either a (a, a)))
-> Maybe (g (Either a (a, a)))
-> Maybe ((:*:) f g (Either a (a, a)))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> g a -> g a -> Maybe (g (Either a (a, a)))
forall (t :: * -> *) a.
Unifiable t =>
t a -> t a -> Maybe (t (Either a (a, a)))
zipMatch g a
a2 g a
b2

instance (Unifiable f, Unifiable g) => Unifiable (f :.: g) where
    zipMatch :: (:.:) f g a -> (:.:) f g a -> Maybe ((:.:) f g (Either a (a, a)))
zipMatch (Comp1 f (g a)
fga) (Comp1 f (g a)
fgb) =
        f (g (Either a (a, a))) -> (:.:) f g (Either a (a, a))
forall k2 k1 (f :: k2 -> *) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
Comp1 (f (g (Either a (a, a))) -> (:.:) f g (Either a (a, a)))
-> Maybe (f (g (Either a (a, a))))
-> Maybe ((:.:) f g (Either a (a, a)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Either (g a) (g a, g a) -> Maybe (g (Either a (a, a))))
-> f (Either (g a) (g a, g a)) -> Maybe (f (g (Either a (a, a))))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Either (g a) (g a, g a) -> Maybe (g (Either a (a, a)))
forall (f :: * -> *) a.
Unifiable f =>
Either (f a) (f a, f a) -> Maybe (f (Either a (a, a)))
step (f (Either (g a) (g a, g a)) -> Maybe (f (g (Either a (a, a)))))
-> Maybe (f (Either (g a) (g a, g a)))
-> Maybe (f (g (Either a (a, a))))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< f (g a) -> f (g a) -> Maybe (f (Either (g a) (g a, g a)))
forall (t :: * -> *) a.
Unifiable t =>
t a -> t a -> Maybe (t (Either a (a, a)))
zipMatch f (g a)
fga f (g a)
fgb)
        where
        -- TODO: can we avoid mapping 'Left' all the way down?
        step :: Either (f a) (f a, f a) -> Maybe (f (Either a (a, a)))
step (Left  f a
gx)       = f (Either a (a, a)) -> Maybe (f (Either a (a, a)))
forall a. a -> Maybe a
Just (a -> Either a (a, a)
forall a b. a -> Either a b
Left (a -> Either a (a, a)) -> f a -> f (Either a (a, a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a
gx)
        step (Right (f a
ga, f a
gb)) = f a -> f a -> Maybe (f (Either a (a, a)))
forall (t :: * -> *) a.
Unifiable t =>
t a -> t a -> Maybe (t (Either a (a, a)))
zipMatch f a
ga f a
gb
#endif

----------------------------------------------------------------
----------------------------------------------------------- fin.