{-# LANGUAGE CPP, MultiParamTypeClasses, FlexibleContexts #-}
{-# OPTIONS_GHC -Wall -fwarn-tabs -fno-warn-name-shadowing #-}

-- 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
----------------------------------------------------------------
--                                                  ~ 2015.03.29
-- |
-- Module      :  Control.Unification
-- Copyright   :  Copyright (c) 2007--2015 wren gayle romano
-- License     :  BSD
-- Maintainer  :  wren@community.haskell.org
-- Stability   :  experimental
-- Portability :  semi-portable (CPP, MPTCs, FlexibleContexts)
--
-- 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 "Control.Unification.Ranked"). 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
    (
    -- * Data types, classes, etc
    -- ** Unification terms
      UTerm(..)
    , freeze
    , unfreeze
    -- ** Errors
    , Fallible(..)
    -- ** Basic type classes
    , Unifiable(..)
    , Variable(..)
    , BindingMonad(..)
    
    -- * Operations on one term
    , getFreeVars
    , applyBindings
    , freshen
    -- freezeM     -- apply bindings and freeze in one traversal
    -- unskolemize -- convert Skolemized variables to free variables
    -- skolemize   -- convert free variables to Skolemized variables
    -- getSkolems  -- compute the skolem variables in a term; helpful?
    
    -- * Operations on two terms
    -- ** Symbolic names
    , (===)
    , (=~=)
    , (=:=)
    , (<:=)
    -- ** Textual names
    , equals
    , equiv
    , unify
    , unifyOccurs
    , subsumes
    
    -- * Operations on many terms
    , getFreeVarsAll
    , applyBindingsAll
    , freshenAll
    -- subsumesAll -- to ensure that there's a single coherent substitution allowing the schema to subsume all the terms in some collection.

    -- * Helper functions
    -- | Client code should not need to use these functions, but
    -- they are exposed just in case they are needed.
    , fullprune
    , semiprune
    , occursIn
    -- TODO: add a post-hoc occurs check in order to have a version of unify which is fast, yet is also guaranteed to fail when it ought to (rather than deferring the failure until later, as the current unify does).
    ) where

import Prelude
    hiding (mapM, mapM_, sequence, foldr, foldr1, foldl, foldl1, all, and, or)

import qualified Data.IntMap as IM
import qualified Data.IntSet as IS
import Data.Foldable
import Data.Traversable
import Control.Monad.Identity (Identity(..))
#if __GLASGOW_HASKELL__ < 710
import Control.Applicative
#endif
import Control.Monad        (MonadPlus(..))
import Control.Monad.Trans  (MonadTrans(..))
#if (MIN_VERSION_mtl(2,2,1))
-- aka: transformers(0,4,1)
import Control.Monad.Except (MonadError(..))
#else
import Control.Monad.Error  (MonadError(..))
#endif
import Control.Monad.State  (MonadState(..), StateT, evalStateT, execStateT)
import Control.Monad.MaybeK
import Control.Monad.State.UnificationExtras
import Control.Unification.Types
----------------------------------------------------------------
----------------------------------------------------------------

-- N.B., this assumes there are no directly-cyclic chains!
--
-- | 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., 'semiprune'.
fullprune :: (BindingMonad t v m) => UTerm t v -> m (UTerm t v)
fullprune :: UTerm t v -> m (UTerm t v)
fullprune t0 :: UTerm t v
t0@(UTerm t (UTerm t v)
_ ) = UTerm t v -> m (UTerm t v)
forall (m :: * -> *) a. Monad m => a -> m a
return UTerm t v
t0
fullprune t0 :: UTerm t v
t0@(UVar  v
v0) = do
    Maybe (UTerm t v)
mb <- v -> m (Maybe (UTerm t v))
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
v -> m (Maybe (UTerm t v))
lookupVar v
v0
    case Maybe (UTerm t v)
mb of
        Maybe (UTerm t v)
Nothing -> UTerm t v -> m (UTerm t v)
forall (m :: * -> *) a. Monad m => a -> m a
return UTerm t v
t0
        Just UTerm t v
t  -> do
            UTerm t v
finalTerm <- UTerm t v -> m (UTerm t v)
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
UTerm t v -> m (UTerm t v)
fullprune UTerm t v
t
            v
v0 v -> UTerm t v -> m ()
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
v -> UTerm t v -> m ()
`bindVar` UTerm t v
finalTerm
            UTerm t v -> m (UTerm t v)
forall (m :: * -> *) a. Monad m => a -> m a
return UTerm t v
finalTerm


-- N.B., this assumes there are no directly-cyclic chains!
--
-- | 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)
semiprune :: UTerm t v -> m (UTerm t v)
semiprune t0 :: UTerm t v
t0@(UTerm t (UTerm t v)
_ ) = UTerm t v -> m (UTerm t v)
forall (m :: * -> *) a. Monad m => a -> m a
return UTerm t v
t0
semiprune t0 :: UTerm t v
t0@(UVar  v
v0) = UTerm t v -> v -> m (UTerm t v)
forall (m :: * -> *) (t :: * -> *) v.
BindingMonad t v m =>
UTerm t v -> v -> m (UTerm t v)
loop UTerm t v
t0 v
v0
    where
    -- We pass the @t@ for @v@ in order to add just a little more sharing.
    loop :: UTerm t v -> v -> m (UTerm t v)
loop UTerm t v
t0 v
v0 = do
        Maybe (UTerm t v)
mb <- v -> m (Maybe (UTerm t v))
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
v -> m (Maybe (UTerm t v))
lookupVar v
v0
        case Maybe (UTerm t v)
mb of
            Maybe (UTerm t v)
Nothing -> UTerm t v -> m (UTerm t v)
forall (m :: * -> *) a. Monad m => a -> m a
return UTerm t v
t0
            Just UTerm t v
t  ->
                case UTerm t v
t  of
                UTerm t (UTerm t v)
_  -> UTerm t v -> m (UTerm t v)
forall (m :: * -> *) a. Monad m => a -> m a
return UTerm t v
t0
                UVar  v
v  -> do
                    UTerm t v
finalVar <- UTerm t v -> v -> m (UTerm t v)
loop UTerm t v
t v
v
                    v
v0 v -> UTerm t v -> m ()
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
v -> UTerm t v -> m ()
`bindVar` UTerm t v
finalVar
                    UTerm t v -> m (UTerm t v)
forall (m :: * -> *) a. Monad m => a -> m a
return UTerm t v
finalVar


-- | 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
{-# INLINE occursIn #-}
occursIn :: v -> UTerm t v -> m Bool
occursIn v
v0 UTerm t v
t0 = do
    UTerm t v
t0 <- UTerm t v -> m (UTerm t v)
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
UTerm t v -> m (UTerm t v)
fullprune UTerm t v
t0
    case UTerm t v
t0 of
        UTerm t (UTerm t v)
t -> t Bool -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or (t Bool -> Bool) -> m (t Bool) -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (UTerm t v -> m Bool) -> t (UTerm t v) -> m (t Bool)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (v
v0 v -> UTerm t v -> m Bool
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
v -> UTerm t v -> m Bool
`occursIn`) t (UTerm t v)
t
            -- TODO: benchmark the following for shortcircuiting
            -- > Traversable.foldlM (\b t' -> if b then return True else v0 `occursIn` t') t
        UVar  v
v -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$! v
v0 v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
v


-- TODO: what was the reason for the MonadTrans madness?
-- TODO: use IM.insertWith or the like to do this in one pass
--
-- | Update the visited-set with a declaration that a variable has
-- been seen with a given binding, or throw 'occursFailure' if the
-- variable has already been seen.
seenAs
    ::  ( BindingMonad t v m
        , Fallible t v e
        , MonadTrans em
        , MonadError e (em m)
        )
    => v -- ^
    -> t (UTerm t v) -- ^
    -> StateT (IM.IntMap (t (UTerm t v))) (em m) () -- ^
{-# INLINE seenAs #-}
seenAs :: v -> t (UTerm t v) -> StateT (IntMap (t (UTerm t v))) (em m) ()
seenAs v
v0 t (UTerm t v)
t0 = do
    IntMap (t (UTerm t v))
seenVars <- StateT (IntMap (t (UTerm t v))) (em m) (IntMap (t (UTerm t v)))
forall s (m :: * -> *). MonadState s m => m s
get
    case Key -> IntMap (t (UTerm t v)) -> Maybe (t (UTerm t v))
forall a. Key -> IntMap a -> Maybe a
IM.lookup (v -> Key
forall v. Variable v => v -> Key
getVarID v
v0) IntMap (t (UTerm t v))
seenVars of
        Just t (UTerm t v)
t  -> em m () -> StateT (IntMap (t (UTerm t v))) (em m) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (em m () -> StateT (IntMap (t (UTerm t v))) (em m) ())
-> (e -> em m ()) -> e -> StateT (IntMap (t (UTerm t v))) (em m) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> em m ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (e -> StateT (IntMap (t (UTerm t v))) (em m) ())
-> e -> StateT (IntMap (t (UTerm t v))) (em m) ()
forall a b. (a -> b) -> a -> b
$ v -> UTerm t v -> e
forall (t :: * -> *) v a. Fallible t v a => v -> UTerm t v -> a
occursFailure v
v0 (t (UTerm t v) -> UTerm t v
forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm t (UTerm t v)
t)
        Maybe (t (UTerm t v))
Nothing -> IntMap (t (UTerm t v)) -> StateT (IntMap (t (UTerm t v))) (em m) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (IntMap (t (UTerm t v))
 -> StateT (IntMap (t (UTerm t v))) (em m) ())
-> IntMap (t (UTerm t v))
-> StateT (IntMap (t (UTerm t v))) (em m) ()
forall a b. (a -> b) -> a -> b
$! Key
-> t (UTerm t v)
-> IntMap (t (UTerm t v))
-> IntMap (t (UTerm t v))
forall a. Key -> a -> IntMap a -> IntMap a
IM.insert (v -> Key
forall v. Variable v => v -> Key
getVarID v
v0) t (UTerm t v)
t0 IntMap (t (UTerm t v))
seenVars

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

-- TODO: these assume pure variables, hence the spine cloning; but
-- we may want to make variants for impure variables with explicit
-- rollback on backtracking.

-- TODO: See if MTL still has that overhead over doing things manually.

-- TODO: Figure out how to abstract the left-catamorphism from these.


-- | 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]
getFreeVars :: UTerm t v -> m [v]
getFreeVars = Identity (UTerm t v) -> m [v]
forall (t :: * -> *) v (m :: * -> *) (s :: * -> *).
(BindingMonad t v m, Foldable s) =>
s (UTerm t v) -> m [v]
getFreeVarsAll (Identity (UTerm t v) -> m [v])
-> (UTerm t v -> Identity (UTerm t v)) -> UTerm t v -> m [v]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UTerm t v -> Identity (UTerm t v)
forall a. a -> Identity a
Identity


-- TODO: Should we return the IntMap instead?
--
-- | Same as 'getFreeVars', 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 @getFreeVars@.
--
-- /Since: 0.7.0/
getFreeVarsAll
    :: (BindingMonad t v m, Foldable s)
    => s (UTerm t v) -> m [v]
getFreeVarsAll :: s (UTerm t v) -> m [v]
getFreeVarsAll s (UTerm t v)
ts0 =
    IntMap v -> [v]
forall a. IntMap a -> [a]
IM.elems (IntMap v -> [v]) -> m (IntMap v) -> m [v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IntSet m (IntMap v) -> IntSet -> m (IntMap v)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (s (UTerm t v) -> StateT IntSet m (IntMap v)
loopAll s (UTerm t v)
ts0) IntSet
IS.empty
    where
    -- TODO: is that the most efficient direction/associativity?
    loopAll :: s (UTerm t v) -> StateT IntSet m (IntMap v)
loopAll = (UTerm t v -> IntMap v -> StateT IntSet m (IntMap v))
-> IntMap v -> s (UTerm t v) -> StateT IntSet m (IntMap v)
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM (\UTerm t v
t IntMap v
r -> IntMap v -> IntMap v -> IntMap v
forall a. IntMap a -> IntMap a -> IntMap a
IM.union IntMap v
r (IntMap v -> IntMap v)
-> StateT IntSet m (IntMap v) -> StateT IntSet m (IntMap v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UTerm t v -> StateT IntSet m (IntMap v)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) (t :: * -> *) a.
(MonadTrans t, BindingMonad t a m, MonadState IntSet (t m)) =>
UTerm t a -> t m (IntMap a)
loop UTerm t v
t) IntMap v
forall a. IntMap a
IM.empty

    loop :: UTerm t a -> t m (IntMap a)
loop UTerm t a
t0 = do
        UTerm t a
t0 <- m (UTerm t a) -> t m (UTerm t a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (UTerm t a) -> t m (UTerm t a))
-> m (UTerm t a) -> t m (UTerm t a)
forall a b. (a -> b) -> a -> b
$ UTerm t a -> m (UTerm t a)
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
UTerm t v -> m (UTerm t v)
semiprune UTerm t a
t0
        case UTerm t a
t0 of
            UTerm t (UTerm t a)
t -> t (IntMap a) -> IntMap a
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (t (IntMap a) -> IntMap a) -> t m (t (IntMap a)) -> t m (IntMap a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (UTerm t a -> t m (IntMap a))
-> t (UTerm t a) -> t m (t (IntMap a))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM UTerm t a -> t m (IntMap a)
loop t (UTerm t a)
t
                -- TODO: benchmark using the following instead:
                -- > foldMapM f = foldlM (\a b -> mappend a <$> f b) mempty
            UVar  a
v -> do
                IntSet
seenVars <- t m IntSet
forall s (m :: * -> *). MonadState s m => m s
get
                let i :: Key
i = a -> Key
forall v. Variable v => v -> Key
getVarID a
v
                if Key -> IntSet -> Bool
IS.member Key
i IntSet
seenVars
                    then IntMap a -> t m (IntMap a)
forall (m :: * -> *) a. Monad m => a -> m a
return IntMap a
forall a. IntMap a
IM.empty -- no (more) free vars down here
                    else do
                        IntSet -> t m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (IntSet -> t m ()) -> IntSet -> t m ()
forall a b. (a -> b) -> a -> b
$! Key -> IntSet -> IntSet
IS.insert Key
i IntSet
seenVars
                        Maybe (UTerm t a)
mb <- m (Maybe (UTerm t a)) -> t m (Maybe (UTerm t a))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Maybe (UTerm t a)) -> t m (Maybe (UTerm t a)))
-> m (Maybe (UTerm t a)) -> t m (Maybe (UTerm t a))
forall a b. (a -> b) -> a -> b
$ a -> m (Maybe (UTerm t a))
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
v -> m (Maybe (UTerm t v))
lookupVar a
v
                        case Maybe (UTerm t a)
mb of
                            Just UTerm t a
t' -> UTerm t a -> t m (IntMap a)
loop UTerm t a
t'
                            Maybe (UTerm t a)
Nothing -> IntMap a -> t m (IntMap a)
forall (m :: * -> *) a. Monad m => a -> m a
return (IntMap a -> t m (IntMap a)) -> IntMap a -> t m (IntMap a)
forall a b. (a -> b) -> a -> b
$ Key -> a -> IntMap a
forall a. Key -> a -> IntMap a
IM.singleton Key
i a
v


-- TODO: what was the reason for the MonadTrans madness?
--
-- | 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 'occursFailure' exceptions
-- must be forced. This function /does/ preserve sharing, however
-- that sharing is no longer observed by the monad.
--
-- If any cyclic bindings are detected, then an 'occursFailure'
-- exception will be thrown.
applyBindings
    ::  ( BindingMonad t v m
        , Fallible t v e
        , MonadTrans em
        , Functor (em m) -- Grr, Monad(em m) should imply Functor(em m)
        , MonadError e (em m)
        )
    => UTerm t v       -- ^
    -> em m (UTerm t v) -- ^
applyBindings :: UTerm t v -> em m (UTerm t v)
applyBindings = (Identity (UTerm t v) -> UTerm t v)
-> em m (Identity (UTerm t v)) -> em m (UTerm t v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Identity (UTerm t v) -> UTerm t v
forall a. Identity a -> a
runIdentity (em m (Identity (UTerm t v)) -> em m (UTerm t v))
-> (UTerm t v -> em m (Identity (UTerm t v)))
-> UTerm t v
-> em m (UTerm t v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity (UTerm t v) -> em m (Identity (UTerm t v))
forall (t :: * -> *) v (m :: * -> *) e (em :: (* -> *) -> * -> *)
       (s :: * -> *).
(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))
applyBindingsAll (Identity (UTerm t v) -> em m (Identity (UTerm t v)))
-> (UTerm t v -> Identity (UTerm t v))
-> UTerm t v
-> em m (Identity (UTerm t v))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UTerm t v -> Identity (UTerm t v)
forall a. a -> Identity a
Identity


-- TODO: what was the reason for the MonadTrans madness?
--
-- | Same as 'applyBindings', 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.
--
-- /Since: 0.7.0/
applyBindingsAll
    ::  ( BindingMonad t v m
        , Fallible t v e
        , MonadTrans em
        , Functor (em m) -- Grr, Monad(em m) should imply Functor(em m)
        , MonadError e (em m)
        , Traversable s
        )
    => s (UTerm t v)        -- ^
    -> em m (s (UTerm t v)) -- ^
applyBindingsAll :: s (UTerm t v) -> em m (s (UTerm t v))
applyBindingsAll s (UTerm t v)
ts0 = StateT
  (IntMap (Either (UTerm t v) (UTerm t v))) (em m) (s (UTerm t v))
-> IntMap (Either (UTerm t v) (UTerm t v)) -> em m (s (UTerm t v))
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT ((UTerm t v
 -> StateT
      (IntMap (Either (UTerm t v) (UTerm t v))) (em m) (UTerm t v))
-> s (UTerm t v)
-> StateT
     (IntMap (Either (UTerm t v) (UTerm t v))) (em m) (s (UTerm t v))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM UTerm t v
-> StateT
     (IntMap (Either (UTerm t v) (UTerm t v))) (em m) (UTerm t v)
forall (t :: * -> *) v (t :: (* -> *) -> * -> *)
       (t :: (* -> *) -> * -> *) (m :: * -> *) e.
(MonadState (IntMap (Either (UTerm t v) (UTerm t v))) (t (t m)),
 Fallible t v e, MonadError e (t m), BindingMonad t v m,
 MonadTrans t, MonadTrans t) =>
UTerm t v -> t (t m) (UTerm t v)
loop s (UTerm t v)
ts0) IntMap (Either (UTerm t v) (UTerm t v))
forall a. IntMap a
IM.empty
    where
    loop :: UTerm t v -> t (t m) (UTerm t v)
loop UTerm t v
t0 = do
        UTerm t v
t0 <- t m (UTerm t v) -> t (t m) (UTerm t v)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (t m (UTerm t v) -> t (t m) (UTerm t v))
-> (m (UTerm t v) -> t m (UTerm t v))
-> m (UTerm t v)
-> t (t m) (UTerm t v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (UTerm t v) -> t m (UTerm t v)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (UTerm t v) -> t (t m) (UTerm t v))
-> m (UTerm t v) -> t (t m) (UTerm t v)
forall a b. (a -> b) -> a -> b
$ UTerm t v -> m (UTerm t v)
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
UTerm t v -> m (UTerm t v)
semiprune UTerm t v
t0
        case UTerm t v
t0 of
            UTerm t (UTerm t v)
t -> 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)
-> t (t m) (t (UTerm t v)) -> t (t m) (UTerm t v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (UTerm t v -> t (t m) (UTerm t v))
-> t (UTerm t v) -> t (t m) (t (UTerm t v))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM UTerm t v -> t (t m) (UTerm t v)
loop t (UTerm t v)
t
            UVar  v
v -> do
                let i :: Key
i = v -> Key
forall v. Variable v => v -> Key
getVarID v
v
                Maybe (Either (UTerm t v) (UTerm t v))
mb <- Key
-> IntMap (Either (UTerm t v) (UTerm t v))
-> Maybe (Either (UTerm t v) (UTerm t v))
forall a. Key -> IntMap a -> Maybe a
IM.lookup Key
i (IntMap (Either (UTerm t v) (UTerm t v))
 -> Maybe (Either (UTerm t v) (UTerm t v)))
-> t (t m) (IntMap (Either (UTerm t v) (UTerm t v)))
-> t (t m) (Maybe (Either (UTerm t v) (UTerm t v)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t (t m) (IntMap (Either (UTerm t v) (UTerm t v)))
forall s (m :: * -> *). MonadState s m => m s
get
                case Maybe (Either (UTerm t v) (UTerm t v))
mb of
                    Just (Right UTerm t v
t) -> UTerm t v -> t (t m) (UTerm t v)
forall (m :: * -> *) a. Monad m => a -> m a
return UTerm t v
t
                    Just (Left  UTerm t v
t) -> t m (UTerm t v) -> t (t m) (UTerm t v)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (t m (UTerm t v) -> t (t m) (UTerm t v))
-> (e -> t m (UTerm t v)) -> e -> t (t m) (UTerm t v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> t m (UTerm t v)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (e -> t (t m) (UTerm t v)) -> e -> t (t m) (UTerm t v)
forall a b. (a -> b) -> a -> b
$ v -> UTerm t v -> e
forall (t :: * -> *) v a. Fallible t v a => v -> UTerm t v -> a
occursFailure v
v UTerm t v
t
                    Maybe (Either (UTerm t v) (UTerm t v))
Nothing -> do
                        Maybe (UTerm t v)
mb' <- t m (Maybe (UTerm t v)) -> t (t m) (Maybe (UTerm t v))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (t m (Maybe (UTerm t v)) -> t (t m) (Maybe (UTerm t v)))
-> (m (Maybe (UTerm t v)) -> t m (Maybe (UTerm t v)))
-> m (Maybe (UTerm t v))
-> t (t m) (Maybe (UTerm t v))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (Maybe (UTerm t v)) -> t m (Maybe (UTerm t v))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Maybe (UTerm t v)) -> t (t m) (Maybe (UTerm t v)))
-> m (Maybe (UTerm t v)) -> t (t m) (Maybe (UTerm t v))
forall a b. (a -> b) -> a -> b
$ v -> m (Maybe (UTerm t v))
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
v -> m (Maybe (UTerm t v))
lookupVar v
v
                        case Maybe (UTerm t v)
mb' of
                            Maybe (UTerm t v)
Nothing -> UTerm t v -> t (t m) (UTerm t v)
forall (m :: * -> *) a. Monad m => a -> m a
return UTerm t v
t0
                            Just UTerm t v
t  -> do
                                (IntMap (Either (UTerm t v) (UTerm t v))
 -> IntMap (Either (UTerm t v) (UTerm t v)))
-> t (t m) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' ((IntMap (Either (UTerm t v) (UTerm t v))
  -> IntMap (Either (UTerm t v) (UTerm t v)))
 -> t (t m) ())
-> (Either (UTerm t v) (UTerm t v)
    -> IntMap (Either (UTerm t v) (UTerm t v))
    -> IntMap (Either (UTerm t v) (UTerm t v)))
-> Either (UTerm t v) (UTerm t v)
-> t (t m) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Key
-> Either (UTerm t v) (UTerm t v)
-> IntMap (Either (UTerm t v) (UTerm t v))
-> IntMap (Either (UTerm t v) (UTerm t v))
forall a. Key -> a -> IntMap a -> IntMap a
IM.insert Key
i (Either (UTerm t v) (UTerm t v) -> t (t m) ())
-> Either (UTerm t v) (UTerm t v) -> t (t m) ()
forall a b. (a -> b) -> a -> b
$ UTerm t v -> Either (UTerm t v) (UTerm t v)
forall a b. a -> Either a b
Left UTerm t v
t
                                UTerm t v
t' <- UTerm t v -> t (t m) (UTerm t v)
loop UTerm t v
t
                                (IntMap (Either (UTerm t v) (UTerm t v))
 -> IntMap (Either (UTerm t v) (UTerm t v)))
-> t (t m) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' ((IntMap (Either (UTerm t v) (UTerm t v))
  -> IntMap (Either (UTerm t v) (UTerm t v)))
 -> t (t m) ())
-> (Either (UTerm t v) (UTerm t v)
    -> IntMap (Either (UTerm t v) (UTerm t v))
    -> IntMap (Either (UTerm t v) (UTerm t v)))
-> Either (UTerm t v) (UTerm t v)
-> t (t m) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Key
-> Either (UTerm t v) (UTerm t v)
-> IntMap (Either (UTerm t v) (UTerm t v))
-> IntMap (Either (UTerm t v) (UTerm t v))
forall a. Key -> a -> IntMap a -> IntMap a
IM.insert Key
i (Either (UTerm t v) (UTerm t v) -> t (t m) ())
-> Either (UTerm t v) (UTerm t v) -> t (t m) ()
forall a b. (a -> b) -> a -> b
$ UTerm t v -> Either (UTerm t v) (UTerm t v)
forall a b. b -> Either a b
Right UTerm t v
t'
                                UTerm t v -> t (t m) (UTerm t v)
forall (m :: * -> *) a. Monad m => a -> m a
return UTerm t v
t'


-- TODO: what was the reason for the MonadTrans madness?
--
-- | 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 'occursFailure'
-- exception will be thrown.
freshen
    ::  ( BindingMonad t v m
        , Fallible t v e
        , MonadTrans em
        , Functor (em m) -- Grr, Monad(em m) should imply Functor(em m)
        , MonadError e (em m)
        )
    => UTerm t v       -- ^
    -> em m (UTerm t v) -- ^
freshen :: UTerm t v -> em m (UTerm t v)
freshen = (Identity (UTerm t v) -> UTerm t v)
-> em m (Identity (UTerm t v)) -> em m (UTerm t v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Identity (UTerm t v) -> UTerm t v
forall a. Identity a -> a
runIdentity (em m (Identity (UTerm t v)) -> em m (UTerm t v))
-> (UTerm t v -> em m (Identity (UTerm t v)))
-> UTerm t v
-> em m (UTerm t v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity (UTerm t v) -> em m (Identity (UTerm t v))
forall (t :: * -> *) v (m :: * -> *) e (em :: (* -> *) -> * -> *)
       (s :: * -> *).
(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))
freshenAll (Identity (UTerm t v) -> em m (Identity (UTerm t v)))
-> (UTerm t v -> Identity (UTerm t v))
-> UTerm t v
-> em m (Identity (UTerm t v))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UTerm t v -> Identity (UTerm t v)
forall a. a -> Identity a
Identity


-- TODO: what was the reason for the MonadTrans madness?
--
-- | Same as 'freshen', but works on several terms simultaneously.
-- This is different from freshening each term separately, because
-- @freshenAll@ preserves the relationship between the terms. For
-- instance, the result of
--
-- > mapM freshen [UVar 1, UVar 1]
--
-- would be @[UVar 2, UVar 3]@ or something alpha-equivalent, whereas
-- the result of
--
-- > freshenAll [UVar 1, UVar 1]
--
-- would be @[UVar 2, UVar 2]@ or something alpha-equivalent.
--
-- /Since: 0.7.0/
freshenAll
    ::  ( BindingMonad t v m
        , Fallible t v e
        , MonadTrans em
        , Functor (em m) -- Grr, Monad(em m) should imply Functor(em m)
        , MonadError e (em m)
        , Traversable s
        )
    => s (UTerm t v)        -- ^
    -> em m (s (UTerm t v)) -- ^
freshenAll :: s (UTerm t v) -> em m (s (UTerm t v))
freshenAll s (UTerm t v)
ts0 = StateT
  (IntMap (Either (UTerm t v) (UTerm t v))) (em m) (s (UTerm t v))
-> IntMap (Either (UTerm t v) (UTerm t v)) -> em m (s (UTerm t v))
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT ((UTerm t v
 -> StateT
      (IntMap (Either (UTerm t v) (UTerm t v))) (em m) (UTerm t v))
-> s (UTerm t v)
-> StateT
     (IntMap (Either (UTerm t v) (UTerm t v))) (em m) (s (UTerm t v))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM UTerm t v
-> StateT
     (IntMap (Either (UTerm t v) (UTerm t v))) (em m) (UTerm t v)
forall (t :: * -> *) v (t :: (* -> *) -> * -> *)
       (t :: (* -> *) -> * -> *) (m :: * -> *) e.
(MonadState (IntMap (Either (UTerm t v) (UTerm t v))) (t (t m)),
 Fallible t v e, BindingMonad t v m, MonadError e (t m),
 MonadTrans t, MonadTrans t) =>
UTerm t v -> t (t m) (UTerm t v)
loop s (UTerm t v)
ts0) IntMap (Either (UTerm t v) (UTerm t v))
forall a. IntMap a
IM.empty
    where
    loop :: UTerm t v -> t (t m) (UTerm t v)
loop UTerm t v
t0 = do
        UTerm t v
t0 <- t m (UTerm t v) -> t (t m) (UTerm t v)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (t m (UTerm t v) -> t (t m) (UTerm t v))
-> (m (UTerm t v) -> t m (UTerm t v))
-> m (UTerm t v)
-> t (t m) (UTerm t v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (UTerm t v) -> t m (UTerm t v)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (UTerm t v) -> t (t m) (UTerm t v))
-> m (UTerm t v) -> t (t m) (UTerm t v)
forall a b. (a -> b) -> a -> b
$ UTerm t v -> m (UTerm t v)
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
UTerm t v -> m (UTerm t v)
semiprune UTerm t v
t0
        case UTerm t v
t0 of
            UTerm t (UTerm t v)
t -> 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)
-> t (t m) (t (UTerm t v)) -> t (t m) (UTerm t v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (UTerm t v -> t (t m) (UTerm t v))
-> t (UTerm t v) -> t (t m) (t (UTerm t v))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM UTerm t v -> t (t m) (UTerm t v)
loop t (UTerm t v)
t
            UVar  v
v -> do
                let i :: Key
i = v -> Key
forall v. Variable v => v -> Key
getVarID v
v
                IntMap (Either (UTerm t v) (UTerm t v))
seenVars <- t (t m) (IntMap (Either (UTerm t v) (UTerm t v)))
forall s (m :: * -> *). MonadState s m => m s
get
                case Key
-> IntMap (Either (UTerm t v) (UTerm t v))
-> Maybe (Either (UTerm t v) (UTerm t v))
forall a. Key -> IntMap a -> Maybe a
IM.lookup Key
i IntMap (Either (UTerm t v) (UTerm t v))
seenVars of
                    Just (Right UTerm t v
t) -> UTerm t v -> t (t m) (UTerm t v)
forall (m :: * -> *) a. Monad m => a -> m a
return UTerm t v
t
                    Just (Left  UTerm t v
t) -> t m (UTerm t v) -> t (t m) (UTerm t v)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (t m (UTerm t v) -> t (t m) (UTerm t v))
-> (e -> t m (UTerm t v)) -> e -> t (t m) (UTerm t v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> t m (UTerm t v)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (e -> t (t m) (UTerm t v)) -> e -> t (t m) (UTerm t v)
forall a b. (a -> b) -> a -> b
$ v -> UTerm t v -> e
forall (t :: * -> *) v a. Fallible t v a => v -> UTerm t v -> a
occursFailure v
v UTerm t v
t
                    Maybe (Either (UTerm t v) (UTerm t v))
Nothing -> do
                        Maybe (UTerm t v)
mb <- t m (Maybe (UTerm t v)) -> t (t m) (Maybe (UTerm t v))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (t m (Maybe (UTerm t v)) -> t (t m) (Maybe (UTerm t v)))
-> (m (Maybe (UTerm t v)) -> t m (Maybe (UTerm t v)))
-> m (Maybe (UTerm t v))
-> t (t m) (Maybe (UTerm t v))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (Maybe (UTerm t v)) -> t m (Maybe (UTerm t v))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Maybe (UTerm t v)) -> t (t m) (Maybe (UTerm t v)))
-> m (Maybe (UTerm t v)) -> t (t m) (Maybe (UTerm t v))
forall a b. (a -> b) -> a -> b
$ v -> m (Maybe (UTerm t v))
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
v -> m (Maybe (UTerm t v))
lookupVar v
v
                        case Maybe (UTerm t v)
mb of
                            Maybe (UTerm t v)
Nothing -> do
                                UTerm t v
v' <- t m (UTerm t v) -> t (t m) (UTerm t v)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (t m (UTerm t v) -> t (t m) (UTerm t v))
-> (m (UTerm t v) -> t m (UTerm t v))
-> m (UTerm t v)
-> t (t m) (UTerm t v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (UTerm t v) -> t m (UTerm t v)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (UTerm t v) -> t (t m) (UTerm t v))
-> m (UTerm t v) -> t (t m) (UTerm t v)
forall a b. (a -> b) -> a -> b
$ v -> UTerm t v
forall (t :: * -> *) v. v -> UTerm t v
UVar (v -> UTerm t v) -> m v -> m (UTerm t v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m v
forall (t :: * -> *) v (m :: * -> *). BindingMonad t v m => m v
freeVar
                                IntMap (Either (UTerm t v) (UTerm t v)) -> t (t m) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (IntMap (Either (UTerm t v) (UTerm t v)) -> t (t m) ())
-> IntMap (Either (UTerm t v) (UTerm t v)) -> t (t m) ()
forall a b. (a -> b) -> a -> b
$! Key
-> Either (UTerm t v) (UTerm t v)
-> IntMap (Either (UTerm t v) (UTerm t v))
-> IntMap (Either (UTerm t v) (UTerm t v))
forall a. Key -> a -> IntMap a -> IntMap a
IM.insert Key
i (UTerm t v -> Either (UTerm t v) (UTerm t v)
forall a b. b -> Either a b
Right UTerm t v
v') IntMap (Either (UTerm t v) (UTerm t v))
seenVars
                                UTerm t v -> t (t m) (UTerm t v)
forall (m :: * -> *) a. Monad m => a -> m a
return UTerm t v
v'
                            Just UTerm t v
t  -> do
                                IntMap (Either (UTerm t v) (UTerm t v)) -> t (t m) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (IntMap (Either (UTerm t v) (UTerm t v)) -> t (t m) ())
-> IntMap (Either (UTerm t v) (UTerm t v)) -> t (t m) ()
forall a b. (a -> b) -> a -> b
$! Key
-> Either (UTerm t v) (UTerm t v)
-> IntMap (Either (UTerm t v) (UTerm t v))
-> IntMap (Either (UTerm t v) (UTerm t v))
forall a. Key -> a -> IntMap a -> IntMap a
IM.insert Key
i (UTerm t v -> Either (UTerm t v) (UTerm t v)
forall a b. a -> Either a b
Left UTerm t v
t) IntMap (Either (UTerm t v) (UTerm t v))
seenVars
                                UTerm t v
t' <- UTerm t v -> t (t m) (UTerm t v)
loop UTerm t v
t
                                UTerm t v
v' <- t m (UTerm t v) -> t (t m) (UTerm t v)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (t m (UTerm t v) -> t (t m) (UTerm t v))
-> (m (UTerm t v) -> t m (UTerm t v))
-> m (UTerm t v)
-> t (t m) (UTerm t v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (UTerm t v) -> t m (UTerm t v)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (UTerm t v) -> t (t m) (UTerm t v))
-> m (UTerm t v) -> t (t m) (UTerm t v)
forall a b. (a -> b) -> a -> b
$ v -> UTerm t v
forall (t :: * -> *) v. v -> UTerm t v
UVar (v -> UTerm t v) -> m v -> m (UTerm t v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UTerm t v -> m v
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
UTerm t v -> m v
newVar UTerm t v
t'
                                (IntMap (Either (UTerm t v) (UTerm t v))
 -> IntMap (Either (UTerm t v) (UTerm t v)))
-> t (t m) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' ((IntMap (Either (UTerm t v) (UTerm t v))
  -> IntMap (Either (UTerm t v) (UTerm t v)))
 -> t (t m) ())
-> (IntMap (Either (UTerm t v) (UTerm t v))
    -> IntMap (Either (UTerm t v) (UTerm t v)))
-> t (t m) ()
forall a b. (a -> b) -> a -> b
$ Key
-> Either (UTerm t v) (UTerm t v)
-> IntMap (Either (UTerm t v) (UTerm t v))
-> IntMap (Either (UTerm t v) (UTerm t v))
forall a. Key -> a -> IntMap a -> IntMap a
IM.insert Key
i (UTerm t v -> Either (UTerm t v) (UTerm t v)
forall a b. b -> Either a b
Right UTerm t v
v')
                                UTerm t v -> t (t m) (UTerm t v)
forall (m :: * -> *) a. Monad m => a -> m a
return UTerm t v
v'

----------------------------------------------------------------
----------------------------------------------------------------
-- BUG: have to give the signatures for Haddock :(

-- | 'equals'
(===)
    :: (BindingMonad t v m)
    => UTerm t v  -- ^
    -> UTerm t v  -- ^
    -> m Bool     -- ^
=== :: UTerm t v -> UTerm t v -> m Bool
(===) = UTerm t v -> UTerm t v -> m Bool
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
UTerm t v -> UTerm t v -> m Bool
equals
{-# INLINE (===) #-}
infix 4 ===, `equals`


-- | 'equiv'
(=~=)
    :: (BindingMonad t v m)
    => UTerm t v                 -- ^
    -> UTerm t v                 -- ^
    -> m (Maybe (IM.IntMap Int)) -- ^
=~= :: UTerm t v -> UTerm t v -> m (Maybe (IntMap Key))
(=~=) = UTerm t v -> UTerm t v -> m (Maybe (IntMap Key))
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
UTerm t v -> UTerm t v -> m (Maybe (IntMap Key))
equiv
{-# INLINE (=~=) #-}
infix 4 =~=, `equiv`


-- TODO: what was the reason for the MonadTrans madness?
-- | 'unify'
(=:=)
    ::  ( BindingMonad t v m
        , Fallible t v e
        , MonadTrans em
        , Functor (em m) -- Grr, Monad(em m) should imply Functor(em m)
        , MonadError e (em m)
        )
    => UTerm t v        -- ^
    -> UTerm t v        -- ^
    -> em m (UTerm t v) -- ^
=:= :: UTerm t v -> UTerm t v -> em m (UTerm t v)
(=:=) = UTerm t v -> UTerm t v -> em m (UTerm t v)
forall (t :: * -> *) v (m :: * -> *) e (em :: (* -> *) -> * -> *).
(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)
unify
{-# INLINE (=:=) #-}
infix 4 =:=, `unify`


-- TODO: what was the reason for the MonadTrans madness?
-- | 'subsumes'
(<:=)
    ::  ( BindingMonad t v m
        , Fallible t v e
        , MonadTrans em
        , Functor (em m) -- Grr, Monad(em m) should imply Functor(em m)
        , MonadError e (em m)
        )
    => UTerm t v -- ^
    -> UTerm t v -- ^
    -> em m Bool -- ^
<:= :: UTerm t v -> UTerm t v -> em m Bool
(<:=) = UTerm t v -> UTerm t v -> em m Bool
forall (t :: * -> *) v (m :: * -> *) e (em :: (* -> *) -> * -> *).
(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
subsumes
{-# INLINE (<:=) #-}
infix 4 <:=, `subsumes`

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

{- BUG:
If we don't use anything special, then there's a 2x overhead for
calling 'equals' (and probably the rest of them too). If we add a
SPECIALIZE pragma, or if we try to use MaybeT instead of MaybeKT
then that jumps up to 4x overhead. However, if we add an INLINE
pragma then it gets faster than the same implementation in the
benchmark file. I've no idea what's going on here...
-}

-- TODO: should we offer a variant which gives the reason for failure?
--
-- | Determine if two terms are structurally equal. This is essentially
-- equivalent to @('==')@ 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., 'equiv'.
equals
    :: (BindingMonad t v m)
    => UTerm t v  -- ^
    -> UTerm t v  -- ^
    -> m Bool     -- ^
equals :: UTerm t v -> UTerm t v -> m Bool
equals UTerm t v
tl0 UTerm t v
tr0 = do
    Maybe ()
mb <- MaybeKT m () -> m (Maybe ())
forall (m :: * -> *) a. Applicative m => MaybeKT m a -> m (Maybe a)
runMaybeKT (UTerm t v -> UTerm t v -> MaybeKT m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) (t :: * -> *) v.
(MonadTrans t, BindingMonad t v m, MonadPlus (t m)) =>
UTerm t v -> UTerm t v -> t m ()
loop UTerm t v
tl0 UTerm t v
tr0)
    case Maybe ()
mb of
        Maybe ()
Nothing -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
        Just () -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    where
    loop :: UTerm t v -> UTerm t v -> t m ()
loop UTerm t v
tl0 UTerm t v
tr0 = do
        UTerm t v
tl0 <- m (UTerm t v) -> t m (UTerm t v)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (UTerm t v) -> t m (UTerm t v))
-> m (UTerm t v) -> t m (UTerm t v)
forall a b. (a -> b) -> a -> b
$ UTerm t v -> m (UTerm t v)
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
UTerm t v -> m (UTerm t v)
semiprune UTerm t v
tl0
        UTerm t v
tr0 <- m (UTerm t v) -> t m (UTerm t v)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (UTerm t v) -> t m (UTerm t v))
-> m (UTerm t v) -> t m (UTerm t v)
forall a b. (a -> b) -> a -> b
$ UTerm t v -> m (UTerm t v)
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
UTerm t v -> m (UTerm t v)
semiprune UTerm t v
tr0
        case (UTerm t v
tl0, UTerm t v
tr0) of
            (UVar v
vl, UVar v
vr)
                | v
vl v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
vr  -> () -> t m ()
forall (m :: * -> *) a. Monad m => a -> m a
return () -- success
                | Bool
otherwise -> do
                    Maybe (UTerm t v)
mtl <- m (Maybe (UTerm t v)) -> t m (Maybe (UTerm t v))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Maybe (UTerm t v)) -> t m (Maybe (UTerm t v)))
-> m (Maybe (UTerm t v)) -> t m (Maybe (UTerm t v))
forall a b. (a -> b) -> a -> b
$ v -> m (Maybe (UTerm t v))
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
v -> m (Maybe (UTerm t v))
lookupVar v
vl
                    Maybe (UTerm t v)
mtr <- m (Maybe (UTerm t v)) -> t m (Maybe (UTerm t v))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Maybe (UTerm t v)) -> t m (Maybe (UTerm t v)))
-> m (Maybe (UTerm t v)) -> t m (Maybe (UTerm t v))
forall a b. (a -> b) -> a -> b
$ v -> m (Maybe (UTerm t v))
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
v -> m (Maybe (UTerm t v))
lookupVar v
vr
                    case (Maybe (UTerm t v)
mtl, Maybe (UTerm t v)
mtr) of
                        (Maybe (UTerm t v)
Nothing,         Maybe (UTerm t v)
Nothing)         -> t m ()
forall (m :: * -> *) a. MonadPlus m => m a
mzero
                        (Maybe (UTerm t v)
Nothing,         Just UTerm t v
_ )         -> t m ()
forall (m :: * -> *) a. MonadPlus m => m a
mzero
                        (Just UTerm t v
_,          Maybe (UTerm t v)
Nothing)         -> t m ()
forall (m :: * -> *) a. MonadPlus m => m a
mzero
                        (Just (UTerm t (UTerm t v)
tl), Just (UTerm t (UTerm t v)
tr)) -> t (UTerm t v) -> t (UTerm t v) -> t m ()
match t (UTerm t v)
tl t (UTerm t v)
tr
                        (Maybe (UTerm t v), Maybe (UTerm t v))
_ -> [Char] -> t m ()
forall a. HasCallStack => [Char] -> a
error [Char]
_impossible_equals
            (UVar  v
_,  UTerm t (UTerm t v)
_ ) -> t m ()
forall (m :: * -> *) a. MonadPlus m => m a
mzero
            (UTerm t (UTerm t v)
_,  UVar  v
_ ) -> t m ()
forall (m :: * -> *) a. MonadPlus m => m a
mzero
            (UTerm t (UTerm t v)
tl, UTerm t (UTerm t v)
tr) -> t (UTerm t v) -> t (UTerm t v) -> t m ()
match t (UTerm t v)
tl t (UTerm t v)
tr
    
    match :: t (UTerm t v) -> t (UTerm t v) -> t m ()
match t (UTerm t v)
tl t (UTerm t v)
tr =
        case t (UTerm t v)
-> t (UTerm t v)
-> Maybe (t (Either (UTerm t v) (UTerm t v, UTerm t v)))
forall (t :: * -> *) a.
Unifiable t =>
t a -> t a -> Maybe (t (Either a (a, a)))
zipMatch t (UTerm t v)
tl t (UTerm t v)
tr of
        Maybe (t (Either (UTerm t v) (UTerm t v, UTerm t v)))
Nothing  -> t m ()
forall (m :: * -> *) a. MonadPlus m => m a
mzero
        Just t (Either (UTerm t v) (UTerm t v, UTerm t v))
tlr -> (Either (UTerm t v) (UTerm t v, UTerm t v) -> t m ())
-> t (Either (UTerm t v) (UTerm t v, UTerm t v)) -> t m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Either (UTerm t v) (UTerm t v, UTerm t v) -> t m ()
loop_ t (Either (UTerm t v) (UTerm t v, UTerm t v))
tlr
    
    loop_ :: Either (UTerm t v) (UTerm t v, UTerm t v) -> t m ()
loop_ (Left  UTerm t v
_)       = () -> t m ()
forall (m :: * -> *) a. Monad m => a -> m a
return () -- success
    loop_ (Right (UTerm t v
tl,UTerm t v
tr)) = UTerm t v -> UTerm t v -> t m ()
loop UTerm t v
tl UTerm t v
tr

_impossible_equals :: String
{-# NOINLINE _impossible_equals #-}
_impossible_equals :: [Char]
_impossible_equals = [Char]
"equals: the impossible happened"


-- TODO: is that the most helpful return type?
--
-- | 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 (IM.IntMap Int)) -- ^
equiv :: UTerm t v -> UTerm t v -> m (Maybe (IntMap Key))
equiv UTerm t v
tl0 UTerm t v
tr0 = MaybeKT m (IntMap Key) -> m (Maybe (IntMap Key))
forall (m :: * -> *) a. Applicative m => MaybeKT m a -> m (Maybe a)
runMaybeKT (StateT (IntMap Key) (MaybeKT m) ()
-> IntMap Key -> MaybeKT m (IntMap Key)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT (UTerm t v -> UTerm t v -> StateT (IntMap Key) (MaybeKT m) ()
forall (t :: (* -> *) -> * -> *) (t :: (* -> *) -> * -> *)
       (m :: * -> *) (t :: * -> *) v.
(MonadTrans t, MonadTrans t, BindingMonad t v m,
 MonadState (IntMap Key) (t (t m)), MonadPlus (t m)) =>
UTerm t v -> UTerm t v -> t (t m) ()
loop UTerm t v
tl0 UTerm t v
tr0) IntMap Key
forall a. IntMap a
IM.empty)
    where
    loop :: UTerm t v -> UTerm t v -> t (t m) ()
loop UTerm t v
tl0 UTerm t v
tr0 = do
        UTerm t v
tl0 <- t m (UTerm t v) -> t (t m) (UTerm t v)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (t m (UTerm t v) -> t (t m) (UTerm t v))
-> (m (UTerm t v) -> t m (UTerm t v))
-> m (UTerm t v)
-> t (t m) (UTerm t v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (UTerm t v) -> t m (UTerm t v)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (UTerm t v) -> t (t m) (UTerm t v))
-> m (UTerm t v) -> t (t m) (UTerm t v)
forall a b. (a -> b) -> a -> b
$ UTerm t v -> m (UTerm t v)
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
UTerm t v -> m (UTerm t v)
fullprune UTerm t v
tl0
        UTerm t v
tr0 <- t m (UTerm t v) -> t (t m) (UTerm t v)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (t m (UTerm t v) -> t (t m) (UTerm t v))
-> (m (UTerm t v) -> t m (UTerm t v))
-> m (UTerm t v)
-> t (t m) (UTerm t v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (UTerm t v) -> t m (UTerm t v)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (UTerm t v) -> t (t m) (UTerm t v))
-> m (UTerm t v) -> t (t m) (UTerm t v)
forall a b. (a -> b) -> a -> b
$ UTerm t v -> m (UTerm t v)
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
UTerm t v -> m (UTerm t v)
fullprune UTerm t v
tr0
        case (UTerm t v
tl0, UTerm t v
tr0) of
            (UVar v
vl,  UVar  v
vr) -> do
                let il :: Key
il = v -> Key
forall v. Variable v => v -> Key
getVarID v
vl
                let ir :: Key
ir = v -> Key
forall v. Variable v => v -> Key
getVarID v
vr
                IntMap Key
xs <- t (t m) (IntMap Key)
forall s (m :: * -> *). MonadState s m => m s
get
                case Key -> IntMap Key -> Maybe Key
forall a. Key -> IntMap a -> Maybe a
IM.lookup Key
il IntMap Key
xs of
                    Just Key
x
                        | Key
x Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
== Key
ir   -> () -> t (t m) ()
forall (m :: * -> *) a. Monad m => a -> m a
return () -- success; no changes
                        | Bool
otherwise -> t m () -> t (t m) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift t m ()
forall (m :: * -> *) a. MonadPlus m => m a
mzero
                    Maybe Key
Nothing         -> IntMap Key -> t (t m) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (IntMap Key -> t (t m) ()) -> IntMap Key -> t (t m) ()
forall a b. (a -> b) -> a -> b
$! Key -> Key -> IntMap Key -> IntMap Key
forall a. Key -> a -> IntMap a -> IntMap a
IM.insert Key
il Key
ir IntMap Key
xs
            
            (UVar  v
_,  UTerm t (UTerm t v)
_ ) -> t m () -> t (t m) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift t m ()
forall (m :: * -> *) a. MonadPlus m => m a
mzero
            (UTerm t (UTerm t v)
_,  UVar  v
_ ) -> t m () -> t (t m) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift t m ()
forall (m :: * -> *) a. MonadPlus m => m a
mzero
            (UTerm t (UTerm t v)
tl, UTerm t (UTerm t v)
tr) ->
                case t (UTerm t v)
-> t (UTerm t v)
-> Maybe (t (Either (UTerm t v) (UTerm t v, UTerm t v)))
forall (t :: * -> *) a.
Unifiable t =>
t a -> t a -> Maybe (t (Either a (a, a)))
zipMatch t (UTerm t v)
tl t (UTerm t v)
tr of
                Maybe (t (Either (UTerm t v) (UTerm t v, UTerm t v)))
Nothing  -> t m () -> t (t m) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift t m ()
forall (m :: * -> *) a. MonadPlus m => m a
mzero
                Just t (Either (UTerm t v) (UTerm t v, UTerm t v))
tlr -> (Either (UTerm t v) (UTerm t v, UTerm t v) -> t (t m) ())
-> t (Either (UTerm t v) (UTerm t v, UTerm t v)) -> t (t m) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Either (UTerm t v) (UTerm t v, UTerm t v) -> t (t m) ()
loop_ t (Either (UTerm t v) (UTerm t v, UTerm t v))
tlr
    
    loop_ :: Either (UTerm t v) (UTerm t v, UTerm t v) -> t (t m) ()
loop_ (Left  UTerm t v
_)       = () -> t (t m) ()
forall (m :: * -> *) a. Monad m => a -> m a
return () -- success; no changes
    loop_ (Right (UTerm t v
tl,UTerm t v
tr)) = UTerm t v -> UTerm t v -> t (t m) ()
loop UTerm t v
tl UTerm t v
tr


----------------------------------------------------------------
-- Not quite unify2 from the benchmarks, since we do AOOS.
-- TODO: what was the reason for the MonadTrans madness?
--
-- | A variant of 'unify' which uses 'occursIn' instead of visited-sets.
-- This should only be used when eager throwing of 'occursFailure'
-- errors is absolutely essential (or for testing the correctness
-- of @unify@). 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) -- Grr, Monad(em m) should imply Functor(em m)
        , MonadError e (em m)
        )
    => UTerm t v        -- ^
    -> UTerm t v        -- ^
    -> em m (UTerm t v) -- ^
unifyOccurs :: UTerm t v -> UTerm t v -> em m (UTerm t v)
unifyOccurs = UTerm t v -> UTerm t v -> em m (UTerm t v)
forall e (t :: (* -> *) -> * -> *) (m :: * -> *) (t :: * -> *) v.
(MonadError e (t m), MonadTrans t, BindingMonad t v m,
 Fallible t v e) =>
UTerm t v -> UTerm t v -> t m (UTerm t v)
loop
    where
    {-# INLINE (=:) #-}
    v
v =: :: v -> UTerm t v -> t m ()
=: UTerm t v
t = m () -> t m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> t m ()) -> m () -> t m ()
forall a b. (a -> b) -> a -> b
$ v
v v -> UTerm t v -> m ()
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
v -> UTerm t v -> m ()
`bindVar` UTerm t v
t
    
    {-# INLINE acyclicBindVar #-}
    acyclicBindVar :: v -> UTerm t v -> t m ()
acyclicBindVar v
v UTerm t v
t = do
        Bool
b <- m Bool -> t m Bool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m Bool -> t m Bool) -> m Bool -> t m Bool
forall a b. (a -> b) -> a -> b
$ v
v v -> UTerm t v -> m Bool
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
v -> UTerm t v -> m Bool
`occursIn` UTerm t v
t
        if Bool
b
            then e -> t m ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (e -> t m ()) -> e -> t m ()
forall a b. (a -> b) -> a -> b
$ v -> UTerm t v -> e
forall (t :: * -> *) v a. Fallible t v a => v -> UTerm t v -> a
occursFailure v
v UTerm t v
t
            else v
v v -> UTerm t v -> t m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) (t :: * -> *) v.
(MonadTrans t, BindingMonad t v m) =>
v -> UTerm t v -> t m ()
=: UTerm t v
t
    
    -- TODO: cf todos in 'unify'
    loop :: UTerm t v -> UTerm t v -> t m (UTerm t v)
loop UTerm t v
tl0 UTerm t v
tr0 = do
        UTerm t v
tl0 <- m (UTerm t v) -> t m (UTerm t v)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (UTerm t v) -> t m (UTerm t v))
-> m (UTerm t v) -> t m (UTerm t v)
forall a b. (a -> b) -> a -> b
$ UTerm t v -> m (UTerm t v)
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
UTerm t v -> m (UTerm t v)
semiprune UTerm t v
tl0
        UTerm t v
tr0 <- m (UTerm t v) -> t m (UTerm t v)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (UTerm t v) -> t m (UTerm t v))
-> m (UTerm t v) -> t m (UTerm t v)
forall a b. (a -> b) -> a -> b
$ UTerm t v -> m (UTerm t v)
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
UTerm t v -> m (UTerm t v)
semiprune UTerm t v
tr0
        case (UTerm t v
tl0, UTerm t v
tr0) of
            (UVar v
vl, UVar v
vr)
                | v
vl v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
vr  -> UTerm t v -> t m (UTerm t v)
forall (m :: * -> *) a. Monad m => a -> m a
return UTerm t v
tr0
                | Bool
otherwise -> do
                    Maybe (UTerm t v)
mtl <- m (Maybe (UTerm t v)) -> t m (Maybe (UTerm t v))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Maybe (UTerm t v)) -> t m (Maybe (UTerm t v)))
-> m (Maybe (UTerm t v)) -> t m (Maybe (UTerm t v))
forall a b. (a -> b) -> a -> b
$ v -> m (Maybe (UTerm t v))
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
v -> m (Maybe (UTerm t v))
lookupVar v
vl
                    Maybe (UTerm t v)
mtr <- m (Maybe (UTerm t v)) -> t m (Maybe (UTerm t v))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Maybe (UTerm t v)) -> t m (Maybe (UTerm t v)))
-> m (Maybe (UTerm t v)) -> t m (Maybe (UTerm t v))
forall a b. (a -> b) -> a -> b
$ v -> m (Maybe (UTerm t v))
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
v -> m (Maybe (UTerm t v))
lookupVar v
vr
                    case (Maybe (UTerm t v)
mtl, Maybe (UTerm t v)
mtr) of
                        (Maybe (UTerm t v)
Nothing, Maybe (UTerm t v)
Nothing) -> do
                            v
vl v -> UTerm t v -> t m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) (t :: * -> *) v.
(MonadTrans t, BindingMonad t v m) =>
v -> UTerm t v -> t m ()
=: UTerm t v
tr0
                            UTerm t v -> t m (UTerm t v)
forall (m :: * -> *) a. Monad m => a -> m a
return UTerm t v
tr0
                        (Maybe (UTerm t v)
Nothing, Just UTerm t v
_ ) -> do
                            v
vl v -> UTerm t v -> t m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) (t :: * -> *) v e.
(MonadTrans t, BindingMonad t v m, MonadError e (t m),
 Fallible t v e) =>
v -> UTerm t v -> t m ()
`acyclicBindVar` UTerm t v
tr0
                            UTerm t v -> t m (UTerm t v)
forall (m :: * -> *) a. Monad m => a -> m a
return UTerm t v
tr0
                        (Just UTerm t v
_ , Maybe (UTerm t v)
Nothing) -> do
                            v
vr v -> UTerm t v -> t m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) (t :: * -> *) v e.
(MonadTrans t, BindingMonad t v m, MonadError e (t m),
 Fallible t v e) =>
v -> UTerm t v -> t m ()
`acyclicBindVar` UTerm t v
tl0
                            UTerm t v -> t m (UTerm t v)
forall (m :: * -> *) a. Monad m => a -> m a
return UTerm t v
tl0
                        (Just (UTerm t (UTerm t v)
tl), Just (UTerm t (UTerm t v)
tr)) -> do
                            UTerm t v
t <- t (UTerm t v) -> t (UTerm t v) -> t m (UTerm t v)
match t (UTerm t v)
tl t (UTerm t v)
tr
                            v
vr v -> UTerm t v -> t m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) (t :: * -> *) v.
(MonadTrans t, BindingMonad t v m) =>
v -> UTerm t v -> t m ()
=: UTerm t v
t
                            v
vl v -> UTerm t v -> t m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) (t :: * -> *) v.
(MonadTrans t, BindingMonad t v m) =>
v -> UTerm t v -> t m ()
=: UTerm t v
tr0
                            UTerm t v -> t m (UTerm t v)
forall (m :: * -> *) a. Monad m => a -> m a
return UTerm t v
tr0
                        (Maybe (UTerm t v), Maybe (UTerm t v))
_ -> [Char] -> t m (UTerm t v)
forall a. HasCallStack => [Char] -> a
error [Char]
_impossible_unifyOccurs
            
            (UVar v
vl, UTerm t (UTerm t v)
tr) -> do
                Maybe (UTerm t v)
mtl <- m (Maybe (UTerm t v)) -> t m (Maybe (UTerm t v))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Maybe (UTerm t v)) -> t m (Maybe (UTerm t v)))
-> m (Maybe (UTerm t v)) -> t m (Maybe (UTerm t v))
forall a b. (a -> b) -> a -> b
$ v -> m (Maybe (UTerm t v))
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
v -> m (Maybe (UTerm t v))
lookupVar v
vl
                case Maybe (UTerm t v)
mtl of
                    Maybe (UTerm t v)
Nothing  -> do
                        v
vl v -> UTerm t v -> t m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) (t :: * -> *) v e.
(MonadTrans t, BindingMonad t v m, MonadError e (t m),
 Fallible t v e) =>
v -> UTerm t v -> t m ()
`acyclicBindVar` UTerm t v
tr0
                        UTerm t v -> t m (UTerm t v)
forall (m :: * -> *) a. Monad m => a -> m a
return UTerm t v
tl0
                    Just (UTerm t (UTerm t v)
tl) -> do
                        UTerm t v
t <- t (UTerm t v) -> t (UTerm t v) -> t m (UTerm t v)
match t (UTerm t v)
tl t (UTerm t v)
tr
                        v
vl v -> UTerm t v -> t m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) (t :: * -> *) v.
(MonadTrans t, BindingMonad t v m) =>
v -> UTerm t v -> t m ()
=: UTerm t v
t
                        UTerm t v -> t m (UTerm t v)
forall (m :: * -> *) a. Monad m => a -> m a
return UTerm t v
tl0
                    Maybe (UTerm t v)
_ -> [Char] -> t m (UTerm t v)
forall a. HasCallStack => [Char] -> a
error [Char]
_impossible_unifyOccurs
            
            (UTerm t (UTerm t v)
tl, UVar v
vr) -> do
                Maybe (UTerm t v)
mtr <- m (Maybe (UTerm t v)) -> t m (Maybe (UTerm t v))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Maybe (UTerm t v)) -> t m (Maybe (UTerm t v)))
-> m (Maybe (UTerm t v)) -> t m (Maybe (UTerm t v))
forall a b. (a -> b) -> a -> b
$ v -> m (Maybe (UTerm t v))
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
v -> m (Maybe (UTerm t v))
lookupVar v
vr
                case Maybe (UTerm t v)
mtr of
                    Maybe (UTerm t v)
Nothing  -> do
                        v
vr v -> UTerm t v -> t m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) (t :: * -> *) v e.
(MonadTrans t, BindingMonad t v m, MonadError e (t m),
 Fallible t v e) =>
v -> UTerm t v -> t m ()
`acyclicBindVar` UTerm t v
tl0
                        UTerm t v -> t m (UTerm t v)
forall (m :: * -> *) a. Monad m => a -> m a
return UTerm t v
tr0
                    Just (UTerm t (UTerm t v)
tr) -> do
                        UTerm t v
t <- t (UTerm t v) -> t (UTerm t v) -> t m (UTerm t v)
match t (UTerm t v)
tl t (UTerm t v)
tr
                        v
vr v -> UTerm t v -> t m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) (t :: * -> *) v.
(MonadTrans t, BindingMonad t v m) =>
v -> UTerm t v -> t m ()
=: UTerm t v
t
                        UTerm t v -> t m (UTerm t v)
forall (m :: * -> *) a. Monad m => a -> m a
return UTerm t v
tr0
                    Maybe (UTerm t v)
_ -> [Char] -> t m (UTerm t v)
forall a. HasCallStack => [Char] -> a
error [Char]
_impossible_unifyOccurs
            
            (UTerm t (UTerm t v)
tl, UTerm t (UTerm t v)
tr) -> t (UTerm t v) -> t (UTerm t v) -> t m (UTerm t v)
match t (UTerm t v)
tl t (UTerm t v)
tr
    
    match :: t (UTerm t v) -> t (UTerm t v) -> t m (UTerm t v)
match t (UTerm t v)
tl t (UTerm t v)
tr =
        case t (UTerm t v)
-> t (UTerm t v)
-> Maybe (t (Either (UTerm t v) (UTerm t v, UTerm t v)))
forall (t :: * -> *) a.
Unifiable t =>
t a -> t a -> Maybe (t (Either a (a, a)))
zipMatch t (UTerm t v)
tl t (UTerm t v)
tr of
        Maybe (t (Either (UTerm t v) (UTerm t v, UTerm t v)))
Nothing  -> e -> t m (UTerm t v)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (e -> t m (UTerm t v)) -> e -> t m (UTerm t v)
forall a b. (a -> b) -> a -> b
$ t (UTerm t v) -> t (UTerm t v) -> e
forall (t :: * -> *) v a.
Fallible t v a =>
t (UTerm t v) -> t (UTerm t v) -> a
mismatchFailure t (UTerm t v)
tl t (UTerm t v)
tr
        Just t (Either (UTerm t v) (UTerm t v, UTerm t v))
tlr -> 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)
-> t m (t (UTerm t v)) -> t m (UTerm t v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Either (UTerm t v) (UTerm t v, UTerm t v) -> t m (UTerm t v))
-> t (Either (UTerm t v) (UTerm t v, UTerm t v))
-> t m (t (UTerm t v))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Either (UTerm t v) (UTerm t v, UTerm t v) -> t m (UTerm t v)
loop_ t (Either (UTerm t v) (UTerm t v, UTerm t v))
tlr
    
    loop_ :: Either (UTerm t v) (UTerm t v, UTerm t v) -> t m (UTerm t v)
loop_ (Left  UTerm t v
t)       = UTerm t v -> t m (UTerm t v)
forall (m :: * -> *) a. Monad m => a -> m a
return UTerm t v
t
    loop_ (Right (UTerm t v
tl,UTerm t v
tr)) = UTerm t v -> UTerm t v -> t m (UTerm t v)
loop UTerm t v
tl UTerm t v
tr

_impossible_unifyOccurs :: String
{-# NOINLINE _impossible_unifyOccurs #-}
_impossible_unifyOccurs :: [Char]
_impossible_unifyOccurs = [Char]
"unifyOccurs: the impossible happened"


----------------------------------------------------------------
-- TODO: verify correctness, especially for the visited-set stuff.
-- TODO: return Maybe(UTerm t v) in the loop so we can avoid updating bindings trivially
-- TODO: figure out why unifyOccurs is so much faster on pure ground terms!! The only difference there is in lifting over StateT...
-- TODO: what was the reason for the MonadTrans madness?
--
-- | 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) -- Grr, Monad(em m) should imply Functor(em m)
        , MonadError e (em m)
        )
    => UTerm t v        -- ^
    -> UTerm t v        -- ^
    -> em m (UTerm t v) -- ^
unify :: UTerm t v -> UTerm t v -> em m (UTerm t v)
unify UTerm t v
tl0 UTerm t v
tr0 = StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
-> IntMap (t (UTerm t v)) -> em m (UTerm t v)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (UTerm t v
-> UTerm t v -> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
forall e (em :: (* -> *) -> * -> *) (m :: * -> *) (t :: * -> *) v.
(MonadError e (em m), BindingMonad t v m, MonadTrans em,
 Fallible t v e) =>
UTerm t v
-> UTerm t v -> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
loop UTerm t v
tl0 UTerm t v
tr0) IntMap (t (UTerm t v))
forall a. IntMap a
IM.empty
    where
    {-# INLINE (=:) #-}
    v
v =: :: v -> UTerm t v -> t (t m) ()
=: UTerm t v
t = t m () -> t (t m) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (t m () -> t (t m) ()) -> (m () -> t m ()) -> m () -> t (t m) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m () -> t m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> t (t m) ()) -> m () -> t (t m) ()
forall a b. (a -> b) -> a -> b
$ v
v v -> UTerm t v -> m ()
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
v -> UTerm t v -> m ()
`bindVar` UTerm t v
t
    
    -- TODO: would it be beneficial to manually fuse @x <- lift m; y <- lift n@ to @(x,y) <- lift (m;n)@ everywhere we can?
    loop :: UTerm t v
-> UTerm t v -> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
loop UTerm t v
tl0 UTerm t v
tr0 = do
        UTerm t v
tl0 <- em m (UTerm t v)
-> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (em m (UTerm t v)
 -> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v))
-> (m (UTerm t v) -> em m (UTerm t v))
-> m (UTerm t v)
-> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (UTerm t v) -> em m (UTerm t v)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (UTerm t v)
 -> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v))
-> m (UTerm t v)
-> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
forall a b. (a -> b) -> a -> b
$ UTerm t v -> m (UTerm t v)
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
UTerm t v -> m (UTerm t v)
semiprune UTerm t v
tl0
        UTerm t v
tr0 <- em m (UTerm t v)
-> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (em m (UTerm t v)
 -> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v))
-> (m (UTerm t v) -> em m (UTerm t v))
-> m (UTerm t v)
-> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (UTerm t v) -> em m (UTerm t v)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (UTerm t v)
 -> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v))
-> m (UTerm t v)
-> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
forall a b. (a -> b) -> a -> b
$ UTerm t v -> m (UTerm t v)
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
UTerm t v -> m (UTerm t v)
semiprune UTerm t v
tr0
        case (UTerm t v
tl0, UTerm t v
tr0) of
            (UVar v
vl, UVar v
vr)
                | v
vl v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
vr  -> UTerm t v -> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
forall (m :: * -> *) a. Monad m => a -> m a
return UTerm t v
tr0
                | Bool
otherwise -> do
                    Maybe (UTerm t v)
mtl <- em m (Maybe (UTerm t v))
-> StateT (IntMap (t (UTerm t v))) (em m) (Maybe (UTerm t v))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (em m (Maybe (UTerm t v))
 -> StateT (IntMap (t (UTerm t v))) (em m) (Maybe (UTerm t v)))
-> (m (Maybe (UTerm t v)) -> em m (Maybe (UTerm t v)))
-> m (Maybe (UTerm t v))
-> StateT (IntMap (t (UTerm t v))) (em m) (Maybe (UTerm t v))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (Maybe (UTerm t v)) -> em m (Maybe (UTerm t v))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Maybe (UTerm t v))
 -> StateT (IntMap (t (UTerm t v))) (em m) (Maybe (UTerm t v)))
-> m (Maybe (UTerm t v))
-> StateT (IntMap (t (UTerm t v))) (em m) (Maybe (UTerm t v))
forall a b. (a -> b) -> a -> b
$ v -> m (Maybe (UTerm t v))
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
v -> m (Maybe (UTerm t v))
lookupVar v
vl
                    Maybe (UTerm t v)
mtr <- em m (Maybe (UTerm t v))
-> StateT (IntMap (t (UTerm t v))) (em m) (Maybe (UTerm t v))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (em m (Maybe (UTerm t v))
 -> StateT (IntMap (t (UTerm t v))) (em m) (Maybe (UTerm t v)))
-> (m (Maybe (UTerm t v)) -> em m (Maybe (UTerm t v)))
-> m (Maybe (UTerm t v))
-> StateT (IntMap (t (UTerm t v))) (em m) (Maybe (UTerm t v))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (Maybe (UTerm t v)) -> em m (Maybe (UTerm t v))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Maybe (UTerm t v))
 -> StateT (IntMap (t (UTerm t v))) (em m) (Maybe (UTerm t v)))
-> m (Maybe (UTerm t v))
-> StateT (IntMap (t (UTerm t v))) (em m) (Maybe (UTerm t v))
forall a b. (a -> b) -> a -> b
$ v -> m (Maybe (UTerm t v))
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
v -> m (Maybe (UTerm t v))
lookupVar v
vr
                    case (Maybe (UTerm t v)
mtl, Maybe (UTerm t v)
mtr) of
                        (Maybe (UTerm t v)
Nothing, Maybe (UTerm t v)
Nothing) -> do v
vl v -> UTerm t v -> StateT (IntMap (t (UTerm t v))) (em m) ()
forall (t :: (* -> *) -> * -> *) (t :: (* -> *) -> * -> *)
       (m :: * -> *) (t :: * -> *) v.
(MonadTrans t, MonadTrans t, Monad (t m), BindingMonad t v m) =>
v -> UTerm t v -> t (t m) ()
=: UTerm t v
tr0 ; UTerm t v -> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
forall (m :: * -> *) a. Monad m => a -> m a
return UTerm t v
tr0
                        (Maybe (UTerm t v)
Nothing, Just UTerm t v
_ ) -> do v
vl v -> UTerm t v -> StateT (IntMap (t (UTerm t v))) (em m) ()
forall (t :: (* -> *) -> * -> *) (t :: (* -> *) -> * -> *)
       (m :: * -> *) (t :: * -> *) v.
(MonadTrans t, MonadTrans t, Monad (t m), BindingMonad t v m) =>
v -> UTerm t v -> t (t m) ()
=: UTerm t v
tr0 ; UTerm t v -> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
forall (m :: * -> *) a. Monad m => a -> m a
return UTerm t v
tr0
                        (Just UTerm t v
_ , Maybe (UTerm t v)
Nothing) -> do v
vr v -> UTerm t v -> StateT (IntMap (t (UTerm t v))) (em m) ()
forall (t :: (* -> *) -> * -> *) (t :: (* -> *) -> * -> *)
       (m :: * -> *) (t :: * -> *) v.
(MonadTrans t, MonadTrans t, Monad (t m), BindingMonad t v m) =>
v -> UTerm t v -> t (t m) ()
=: UTerm t v
tl0 ; UTerm t v -> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
forall (m :: * -> *) a. Monad m => a -> m a
return UTerm t v
tl0
                        (Just (UTerm t (UTerm t v)
tl), Just (UTerm t (UTerm t v)
tr)) -> do
                            UTerm t v
t <- StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
-> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
forall s (m :: * -> *) a. MonadState s m => m a -> m a
localState (StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
 -> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v))
-> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
-> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
forall a b. (a -> b) -> a -> b
$ do
                                v
vl v -> t (UTerm t v) -> StateT (IntMap (t (UTerm t v))) (em m) ()
forall (t :: * -> *) v (m :: * -> *) e (em :: (* -> *) -> * -> *).
(BindingMonad t v m, Fallible t v e, MonadTrans em,
 MonadError e (em m)) =>
v -> t (UTerm t v) -> StateT (IntMap (t (UTerm t v))) (em m) ()
`seenAs` t (UTerm t v)
tl
                                v
vr v -> t (UTerm t v) -> StateT (IntMap (t (UTerm t v))) (em m) ()
forall (t :: * -> *) v (m :: * -> *) e (em :: (* -> *) -> * -> *).
(BindingMonad t v m, Fallible t v e, MonadTrans em,
 MonadError e (em m)) =>
v -> t (UTerm t v) -> StateT (IntMap (t (UTerm t v))) (em m) ()
`seenAs` t (UTerm t v)
tr
                                t (UTerm t v)
-> t (UTerm t v)
-> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
match t (UTerm t v)
tl t (UTerm t v)
tr
                            v
vr v -> UTerm t v -> StateT (IntMap (t (UTerm t v))) (em m) ()
forall (t :: (* -> *) -> * -> *) (t :: (* -> *) -> * -> *)
       (m :: * -> *) (t :: * -> *) v.
(MonadTrans t, MonadTrans t, Monad (t m), BindingMonad t v m) =>
v -> UTerm t v -> t (t m) ()
=: UTerm t v
t
                            v
vl v -> UTerm t v -> StateT (IntMap (t (UTerm t v))) (em m) ()
forall (t :: (* -> *) -> * -> *) (t :: (* -> *) -> * -> *)
       (m :: * -> *) (t :: * -> *) v.
(MonadTrans t, MonadTrans t, Monad (t m), BindingMonad t v m) =>
v -> UTerm t v -> t (t m) ()
=: UTerm t v
tr0
                            UTerm t v -> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
forall (m :: * -> *) a. Monad m => a -> m a
return UTerm t v
tr0
                        (Maybe (UTerm t v), Maybe (UTerm t v))
_ -> [Char] -> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
forall a. HasCallStack => [Char] -> a
error [Char]
_impossible_unify
            
            (UVar v
vl, UTerm t (UTerm t v)
tr) -> do
                UTerm t v
t <- do
                    Maybe (UTerm t v)
mtl <- em m (Maybe (UTerm t v))
-> StateT (IntMap (t (UTerm t v))) (em m) (Maybe (UTerm t v))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (em m (Maybe (UTerm t v))
 -> StateT (IntMap (t (UTerm t v))) (em m) (Maybe (UTerm t v)))
-> (m (Maybe (UTerm t v)) -> em m (Maybe (UTerm t v)))
-> m (Maybe (UTerm t v))
-> StateT (IntMap (t (UTerm t v))) (em m) (Maybe (UTerm t v))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (Maybe (UTerm t v)) -> em m (Maybe (UTerm t v))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Maybe (UTerm t v))
 -> StateT (IntMap (t (UTerm t v))) (em m) (Maybe (UTerm t v)))
-> m (Maybe (UTerm t v))
-> StateT (IntMap (t (UTerm t v))) (em m) (Maybe (UTerm t v))
forall a b. (a -> b) -> a -> b
$ v -> m (Maybe (UTerm t v))
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
v -> m (Maybe (UTerm t v))
lookupVar v
vl
                    case Maybe (UTerm t v)
mtl of
                        Maybe (UTerm t v)
Nothing         -> UTerm t v -> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
forall (m :: * -> *) a. Monad m => a -> m a
return UTerm t v
tr0
                        Just (UTerm t (UTerm t v)
tl) -> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
-> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
forall s (m :: * -> *) a. MonadState s m => m a -> m a
localState (StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
 -> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v))
-> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
-> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
forall a b. (a -> b) -> a -> b
$ do
                            v
vl v -> t (UTerm t v) -> StateT (IntMap (t (UTerm t v))) (em m) ()
forall (t :: * -> *) v (m :: * -> *) e (em :: (* -> *) -> * -> *).
(BindingMonad t v m, Fallible t v e, MonadTrans em,
 MonadError e (em m)) =>
v -> t (UTerm t v) -> StateT (IntMap (t (UTerm t v))) (em m) ()
`seenAs` t (UTerm t v)
tl
                            t (UTerm t v)
-> t (UTerm t v)
-> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
match t (UTerm t v)
tl t (UTerm t v)
tr
                        Maybe (UTerm t v)
_ -> [Char] -> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
forall a. HasCallStack => [Char] -> a
error [Char]
_impossible_unify
                v
vl v -> UTerm t v -> StateT (IntMap (t (UTerm t v))) (em m) ()
forall (t :: (* -> *) -> * -> *) (t :: (* -> *) -> * -> *)
       (m :: * -> *) (t :: * -> *) v.
(MonadTrans t, MonadTrans t, Monad (t m), BindingMonad t v m) =>
v -> UTerm t v -> t (t m) ()
=: UTerm t v
t
                UTerm t v -> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
forall (m :: * -> *) a. Monad m => a -> m a
return UTerm t v
tl0
            
            (UTerm t (UTerm t v)
tl, UVar v
vr) -> do
                UTerm t v
t <- do
                    Maybe (UTerm t v)
mtr <- em m (Maybe (UTerm t v))
-> StateT (IntMap (t (UTerm t v))) (em m) (Maybe (UTerm t v))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (em m (Maybe (UTerm t v))
 -> StateT (IntMap (t (UTerm t v))) (em m) (Maybe (UTerm t v)))
-> (m (Maybe (UTerm t v)) -> em m (Maybe (UTerm t v)))
-> m (Maybe (UTerm t v))
-> StateT (IntMap (t (UTerm t v))) (em m) (Maybe (UTerm t v))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (Maybe (UTerm t v)) -> em m (Maybe (UTerm t v))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Maybe (UTerm t v))
 -> StateT (IntMap (t (UTerm t v))) (em m) (Maybe (UTerm t v)))
-> m (Maybe (UTerm t v))
-> StateT (IntMap (t (UTerm t v))) (em m) (Maybe (UTerm t v))
forall a b. (a -> b) -> a -> b
$ v -> m (Maybe (UTerm t v))
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
v -> m (Maybe (UTerm t v))
lookupVar v
vr
                    case Maybe (UTerm t v)
mtr of
                        Maybe (UTerm t v)
Nothing         -> UTerm t v -> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
forall (m :: * -> *) a. Monad m => a -> m a
return UTerm t v
tl0
                        Just (UTerm t (UTerm t v)
tr) -> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
-> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
forall s (m :: * -> *) a. MonadState s m => m a -> m a
localState (StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
 -> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v))
-> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
-> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
forall a b. (a -> b) -> a -> b
$ do
                            v
vr v -> t (UTerm t v) -> StateT (IntMap (t (UTerm t v))) (em m) ()
forall (t :: * -> *) v (m :: * -> *) e (em :: (* -> *) -> * -> *).
(BindingMonad t v m, Fallible t v e, MonadTrans em,
 MonadError e (em m)) =>
v -> t (UTerm t v) -> StateT (IntMap (t (UTerm t v))) (em m) ()
`seenAs` t (UTerm t v)
tr
                            t (UTerm t v)
-> t (UTerm t v)
-> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
match t (UTerm t v)
tl t (UTerm t v)
tr
                        Maybe (UTerm t v)
_ -> [Char] -> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
forall a. HasCallStack => [Char] -> a
error [Char]
_impossible_unify
                v
vr v -> UTerm t v -> StateT (IntMap (t (UTerm t v))) (em m) ()
forall (t :: (* -> *) -> * -> *) (t :: (* -> *) -> * -> *)
       (m :: * -> *) (t :: * -> *) v.
(MonadTrans t, MonadTrans t, Monad (t m), BindingMonad t v m) =>
v -> UTerm t v -> t (t m) ()
=: UTerm t v
t
                UTerm t v -> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
forall (m :: * -> *) a. Monad m => a -> m a
return UTerm t v
tr0
            
            (UTerm t (UTerm t v)
tl, UTerm t (UTerm t v)
tr) -> t (UTerm t v)
-> t (UTerm t v)
-> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
match t (UTerm t v)
tl t (UTerm t v)
tr
    
    match :: t (UTerm t v)
-> t (UTerm t v)
-> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
match t (UTerm t v)
tl t (UTerm t v)
tr =
        case t (UTerm t v)
-> t (UTerm t v)
-> Maybe (t (Either (UTerm t v) (UTerm t v, UTerm t v)))
forall (t :: * -> *) a.
Unifiable t =>
t a -> t a -> Maybe (t (Either a (a, a)))
zipMatch t (UTerm t v)
tl t (UTerm t v)
tr of
        Maybe (t (Either (UTerm t v) (UTerm t v, UTerm t v)))
Nothing  -> em m (UTerm t v)
-> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (em m (UTerm t v)
 -> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v))
-> (e -> em m (UTerm t v))
-> e
-> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> em m (UTerm t v)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (e -> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v))
-> e -> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
forall a b. (a -> b) -> a -> b
$ t (UTerm t v) -> t (UTerm t v) -> e
forall (t :: * -> *) v a.
Fallible t v a =>
t (UTerm t v) -> t (UTerm t v) -> a
mismatchFailure t (UTerm t v)
tl t (UTerm t v)
tr
        Just t (Either (UTerm t v) (UTerm t v, UTerm t v))
tlr -> 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)
-> StateT (IntMap (t (UTerm t v))) (em m) (t (UTerm t v))
-> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Either (UTerm t v) (UTerm t v, UTerm t v)
 -> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v))
-> t (Either (UTerm t v) (UTerm t v, UTerm t v))
-> StateT (IntMap (t (UTerm t v))) (em m) (t (UTerm t v))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Either (UTerm t v) (UTerm t v, UTerm t v)
-> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
loop_ t (Either (UTerm t v) (UTerm t v, UTerm t v))
tlr
    
    loop_ :: Either (UTerm t v) (UTerm t v, UTerm t v)
-> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
loop_ (Left  UTerm t v
t)       = UTerm t v -> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
forall (m :: * -> *) a. Monad m => a -> m a
return UTerm t v
t
    loop_ (Right (UTerm t v
tl,UTerm t v
tr)) = UTerm t v
-> UTerm t v -> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
loop UTerm t v
tl UTerm t v
tr

_impossible_unify :: String
{-# NOINLINE _impossible_unify #-}
_impossible_unify :: [Char]
_impossible_unify = [Char]
"unify: the impossible happened"

----------------------------------------------------------------
-- TODO: can we find an efficient way to return the bindings directly
-- instead of altering the monadic bindings? Maybe another StateT
-- IntMap taking getVarID to the variable and its pseudo-bound term?
--
-- TODO: verify correctness
-- TODO: redo with some codensity
-- TODO: there should be some way to catch occursFailure errors and repair the bindings...
-- TODO: what was the reason for the MonadTrans madness?

-- | Determine whether the left term subsumes the right term. That
-- is, whereas @(tl =:= tr)@ will compute the most general substitution
-- @s@ such that @(s tl === s tr)@, @(tl <:= tr)@ computes the most
-- general substitution @s@ such that @(s tl === tr)@. This means
-- that @tl@ is less defined than and consistent with @tr@.
--
-- /N.B./, this function updates the monadic bindings just like
-- 'unify' 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) -- Grr, Monad(em m) should imply Functor(em m)
        , MonadError e (em m)
        )
    => UTerm t v -- ^
    -> UTerm t v -- ^
    -> em m Bool -- ^
subsumes :: UTerm t v -> UTerm t v -> em m Bool
subsumes UTerm t v
tl0 UTerm t v
tr0 = StateT (IntMap (t (UTerm t v))) (em m) Bool
-> IntMap (t (UTerm t v)) -> em m Bool
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (UTerm t v
-> UTerm t v -> StateT (IntMap (t (UTerm t v))) (em m) Bool
forall e (em :: (* -> *) -> * -> *) (m :: * -> *) (t :: * -> *) v.
(MonadError e (em m), Fallible t v e, MonadTrans em,
 BindingMonad t v m) =>
UTerm t v
-> UTerm t v -> StateT (IntMap (t (UTerm t v))) (em m) Bool
loop UTerm t v
tl0 UTerm t v
tr0) IntMap (t (UTerm t v))
forall a. IntMap a
IM.empty
    where
    {-# INLINE (=:) #-}
    v
v =: :: v -> UTerm t v -> t (t m) Bool
=: UTerm t v
t = t m Bool -> t (t m) Bool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (t m Bool -> t (t m) Bool)
-> (m Bool -> t m Bool) -> m Bool -> t (t m) Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m Bool -> t m Bool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m Bool -> t (t m) Bool) -> m Bool -> t (t m) Bool
forall a b. (a -> b) -> a -> b
$ do v
v v -> UTerm t v -> m ()
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
v -> UTerm t v -> m ()
`bindVar` UTerm t v
t ; Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    
    -- TODO: cf todos in 'unify'
    loop :: UTerm t v
-> UTerm t v -> StateT (IntMap (t (UTerm t v))) (em m) Bool
loop UTerm t v
tl0 UTerm t v
tr0 = do
        UTerm t v
tl0 <- em m (UTerm t v)
-> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (em m (UTerm t v)
 -> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v))
-> (m (UTerm t v) -> em m (UTerm t v))
-> m (UTerm t v)
-> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (UTerm t v) -> em m (UTerm t v)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (UTerm t v)
 -> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v))
-> m (UTerm t v)
-> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
forall a b. (a -> b) -> a -> b
$ UTerm t v -> m (UTerm t v)
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
UTerm t v -> m (UTerm t v)
semiprune UTerm t v
tl0
        UTerm t v
tr0 <- em m (UTerm t v)
-> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (em m (UTerm t v)
 -> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v))
-> (m (UTerm t v) -> em m (UTerm t v))
-> m (UTerm t v)
-> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (UTerm t v) -> em m (UTerm t v)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (UTerm t v)
 -> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v))
-> m (UTerm t v)
-> StateT (IntMap (t (UTerm t v))) (em m) (UTerm t v)
forall a b. (a -> b) -> a -> b
$ UTerm t v -> m (UTerm t v)
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
UTerm t v -> m (UTerm t v)
semiprune UTerm t v
tr0
        case (UTerm t v
tl0, UTerm t v
tr0) of
            (UVar v
vl, UVar v
vr)
                | v
vl v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
vr  -> Bool -> StateT (IntMap (t (UTerm t v))) (em m) Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
                | Bool
otherwise -> do
                    Maybe (UTerm t v)
mtl <- em m (Maybe (UTerm t v))
-> StateT (IntMap (t (UTerm t v))) (em m) (Maybe (UTerm t v))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (em m (Maybe (UTerm t v))
 -> StateT (IntMap (t (UTerm t v))) (em m) (Maybe (UTerm t v)))
-> (m (Maybe (UTerm t v)) -> em m (Maybe (UTerm t v)))
-> m (Maybe (UTerm t v))
-> StateT (IntMap (t (UTerm t v))) (em m) (Maybe (UTerm t v))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (Maybe (UTerm t v)) -> em m (Maybe (UTerm t v))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Maybe (UTerm t v))
 -> StateT (IntMap (t (UTerm t v))) (em m) (Maybe (UTerm t v)))
-> m (Maybe (UTerm t v))
-> StateT (IntMap (t (UTerm t v))) (em m) (Maybe (UTerm t v))
forall a b. (a -> b) -> a -> b
$ v -> m (Maybe (UTerm t v))
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
v -> m (Maybe (UTerm t v))
lookupVar v
vl
                    Maybe (UTerm t v)
mtr <- em m (Maybe (UTerm t v))
-> StateT (IntMap (t (UTerm t v))) (em m) (Maybe (UTerm t v))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (em m (Maybe (UTerm t v))
 -> StateT (IntMap (t (UTerm t v))) (em m) (Maybe (UTerm t v)))
-> (m (Maybe (UTerm t v)) -> em m (Maybe (UTerm t v)))
-> m (Maybe (UTerm t v))
-> StateT (IntMap (t (UTerm t v))) (em m) (Maybe (UTerm t v))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (Maybe (UTerm t v)) -> em m (Maybe (UTerm t v))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Maybe (UTerm t v))
 -> StateT (IntMap (t (UTerm t v))) (em m) (Maybe (UTerm t v)))
-> m (Maybe (UTerm t v))
-> StateT (IntMap (t (UTerm t v))) (em m) (Maybe (UTerm t v))
forall a b. (a -> b) -> a -> b
$ v -> m (Maybe (UTerm t v))
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
v -> m (Maybe (UTerm t v))
lookupVar v
vr
                    case (Maybe (UTerm t v)
mtl, Maybe (UTerm t v)
mtr) of
                        (Maybe (UTerm t v)
Nothing,         Maybe (UTerm t v)
Nothing)         -> v
vl v -> UTerm t v -> StateT (IntMap (t (UTerm t v))) (em m) Bool
forall (t :: (* -> *) -> * -> *) (t :: (* -> *) -> * -> *)
       (m :: * -> *) (t :: * -> *) v.
(MonadTrans t, MonadTrans t, Monad (t m), BindingMonad t v m) =>
v -> UTerm t v -> t (t m) Bool
=: UTerm t v
tr0
                        (Maybe (UTerm t v)
Nothing,         Just UTerm t v
_ )         -> v
vl v -> UTerm t v -> StateT (IntMap (t (UTerm t v))) (em m) Bool
forall (t :: (* -> *) -> * -> *) (t :: (* -> *) -> * -> *)
       (m :: * -> *) (t :: * -> *) v.
(MonadTrans t, MonadTrans t, Monad (t m), BindingMonad t v m) =>
v -> UTerm t v -> t (t m) Bool
=: UTerm t v
tr0
                        (Just UTerm t v
_ ,         Maybe (UTerm t v)
Nothing)         -> Bool -> StateT (IntMap (t (UTerm t v))) (em m) Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
                        (Just (UTerm t (UTerm t v)
tl), Just (UTerm t (UTerm t v)
tr)) ->
                            StateT (IntMap (t (UTerm t v))) (em m) Bool
-> StateT (IntMap (t (UTerm t v))) (em m) Bool
forall s (m :: * -> *) a. MonadState s m => m a -> m a
localState (StateT (IntMap (t (UTerm t v))) (em m) Bool
 -> StateT (IntMap (t (UTerm t v))) (em m) Bool)
-> StateT (IntMap (t (UTerm t v))) (em m) Bool
-> StateT (IntMap (t (UTerm t v))) (em m) Bool
forall a b. (a -> b) -> a -> b
$ do
                                v
vl v -> t (UTerm t v) -> StateT (IntMap (t (UTerm t v))) (em m) ()
forall (t :: * -> *) v (m :: * -> *) e (em :: (* -> *) -> * -> *).
(BindingMonad t v m, Fallible t v e, MonadTrans em,
 MonadError e (em m)) =>
v -> t (UTerm t v) -> StateT (IntMap (t (UTerm t v))) (em m) ()
`seenAs` t (UTerm t v)
tl
                                v
vr v -> t (UTerm t v) -> StateT (IntMap (t (UTerm t v))) (em m) ()
forall (t :: * -> *) v (m :: * -> *) e (em :: (* -> *) -> * -> *).
(BindingMonad t v m, Fallible t v e, MonadTrans em,
 MonadError e (em m)) =>
v -> t (UTerm t v) -> StateT (IntMap (t (UTerm t v))) (em m) ()
`seenAs` t (UTerm t v)
tr
                                t (UTerm t v)
-> t (UTerm t v) -> StateT (IntMap (t (UTerm t v))) (em m) Bool
match t (UTerm t v)
tl t (UTerm t v)
tr
                        (Maybe (UTerm t v), Maybe (UTerm t v))
_ -> [Char] -> StateT (IntMap (t (UTerm t v))) (em m) Bool
forall a. HasCallStack => [Char] -> a
error [Char]
_impossible_subsumes
            
            (UVar v
vl,  UTerm t (UTerm t v)
tr) -> do
                Maybe (UTerm t v)
mtl <- em m (Maybe (UTerm t v))
-> StateT (IntMap (t (UTerm t v))) (em m) (Maybe (UTerm t v))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (em m (Maybe (UTerm t v))
 -> StateT (IntMap (t (UTerm t v))) (em m) (Maybe (UTerm t v)))
-> (m (Maybe (UTerm t v)) -> em m (Maybe (UTerm t v)))
-> m (Maybe (UTerm t v))
-> StateT (IntMap (t (UTerm t v))) (em m) (Maybe (UTerm t v))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (Maybe (UTerm t v)) -> em m (Maybe (UTerm t v))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Maybe (UTerm t v))
 -> StateT (IntMap (t (UTerm t v))) (em m) (Maybe (UTerm t v)))
-> m (Maybe (UTerm t v))
-> StateT (IntMap (t (UTerm t v))) (em m) (Maybe (UTerm t v))
forall a b. (a -> b) -> a -> b
$ v -> m (Maybe (UTerm t v))
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
v -> m (Maybe (UTerm t v))
lookupVar v
vl
                case Maybe (UTerm t v)
mtl of
                    Maybe (UTerm t v)
Nothing         -> v
vl v -> UTerm t v -> StateT (IntMap (t (UTerm t v))) (em m) Bool
forall (t :: (* -> *) -> * -> *) (t :: (* -> *) -> * -> *)
       (m :: * -> *) (t :: * -> *) v.
(MonadTrans t, MonadTrans t, Monad (t m), BindingMonad t v m) =>
v -> UTerm t v -> t (t m) Bool
=: UTerm t v
tr0
                    Just (UTerm t (UTerm t v)
tl) -> StateT (IntMap (t (UTerm t v))) (em m) Bool
-> StateT (IntMap (t (UTerm t v))) (em m) Bool
forall s (m :: * -> *) a. MonadState s m => m a -> m a
localState (StateT (IntMap (t (UTerm t v))) (em m) Bool
 -> StateT (IntMap (t (UTerm t v))) (em m) Bool)
-> StateT (IntMap (t (UTerm t v))) (em m) Bool
-> StateT (IntMap (t (UTerm t v))) (em m) Bool
forall a b. (a -> b) -> a -> b
$ do
                        v
vl v -> t (UTerm t v) -> StateT (IntMap (t (UTerm t v))) (em m) ()
forall (t :: * -> *) v (m :: * -> *) e (em :: (* -> *) -> * -> *).
(BindingMonad t v m, Fallible t v e, MonadTrans em,
 MonadError e (em m)) =>
v -> t (UTerm t v) -> StateT (IntMap (t (UTerm t v))) (em m) ()
`seenAs` t (UTerm t v)
tl
                        t (UTerm t v)
-> t (UTerm t v) -> StateT (IntMap (t (UTerm t v))) (em m) Bool
match t (UTerm t v)
tl t (UTerm t v)
tr
                    Maybe (UTerm t v)
_ -> [Char] -> StateT (IntMap (t (UTerm t v))) (em m) Bool
forall a. HasCallStack => [Char] -> a
error [Char]
_impossible_subsumes
            
            (UTerm t (UTerm t v)
_,  UVar  v
_ ) -> Bool -> StateT (IntMap (t (UTerm t v))) (em m) Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
            
            (UTerm t (UTerm t v)
tl, UTerm t (UTerm t v)
tr) -> t (UTerm t v)
-> t (UTerm t v) -> StateT (IntMap (t (UTerm t v))) (em m) Bool
match t (UTerm t v)
tl t (UTerm t v)
tr
    
    match :: t (UTerm t v)
-> t (UTerm t v) -> StateT (IntMap (t (UTerm t v))) (em m) Bool
match t (UTerm t v)
tl t (UTerm t v)
tr =
        case t (UTerm t v)
-> t (UTerm t v)
-> Maybe (t (Either (UTerm t v) (UTerm t v, UTerm t v)))
forall (t :: * -> *) a.
Unifiable t =>
t a -> t a -> Maybe (t (Either a (a, a)))
zipMatch t (UTerm t v)
tl t (UTerm t v)
tr of
        Maybe (t (Either (UTerm t v) (UTerm t v, UTerm t v)))
Nothing  -> Bool -> StateT (IntMap (t (UTerm t v))) (em m) Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
        Just t (Either (UTerm t v) (UTerm t v, UTerm t v))
tlr -> t Bool -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and (t Bool -> Bool)
-> StateT (IntMap (t (UTerm t v))) (em m) (t Bool)
-> StateT (IntMap (t (UTerm t v))) (em m) Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Either (UTerm t v) (UTerm t v, UTerm t v)
 -> StateT (IntMap (t (UTerm t v))) (em m) Bool)
-> t (Either (UTerm t v) (UTerm t v, UTerm t v))
-> StateT (IntMap (t (UTerm t v))) (em m) (t Bool)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Either (UTerm t v) (UTerm t v, UTerm t v)
-> StateT (IntMap (t (UTerm t v))) (em m) Bool
loop_ t (Either (UTerm t v) (UTerm t v, UTerm t v))
tlr -- TODO: use foldlM?
    
    loop_ :: Either (UTerm t v) (UTerm t v, UTerm t v)
-> StateT (IntMap (t (UTerm t v))) (em m) Bool
loop_ (Left  UTerm t v
_)       = Bool -> StateT (IntMap (t (UTerm t v))) (em m) Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    loop_ (Right (UTerm t v
tl,UTerm t v
tr)) = UTerm t v
-> UTerm t v -> StateT (IntMap (t (UTerm t v))) (em m) Bool
loop UTerm t v
tl UTerm t v
tr

_impossible_subsumes :: String
{-# NOINLINE _impossible_subsumes #-}
_impossible_subsumes :: [Char]
_impossible_subsumes = [Char]
"subsumes: the impossible happened"

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