{-# LANGUAGE CPP, MultiParamTypeClasses, FlexibleContexts #-}
{-# OPTIONS_GHC -Wall -fwarn-tabs -fno-warn-name-shadowing #-}
----------------------------------------------------------------
--                                                  ~ 2015.03.29
-- |
-- Module      :  Control.Unification.Ranked
-- Copyright   :  Copyright (c) 2007--2015 wren gayle romano
-- License     :  BSD
-- Maintainer  :  wren@community.haskell.org
-- Stability   :  highly experimental
-- Portability :  semi-portable (CPP, MPTCs, FlexibleContexts)
--
-- This module provides the API of "Control.Unification" except
-- using 'RankedBindingMonad' where appropriate. This module (and
-- the binding implementations for it) are highly experimental and
-- subject to change in future versions.
----------------------------------------------------------------
module Control.Unification.Ranked
    (
    -- * Data types, classes, etc
      module Control.Unification.Types
    
    -- * 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
    ) where

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

import qualified Data.IntMap as IM
import Data.Traversable
#if __GLASGOW_HASKELL__ < 710
import Control.Applicative
#endif
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)
import Control.Monad.State.UnificationExtras
import Control.Unification.Types
import Control.Unification hiding (unify, (=:=))
----------------------------------------------------------------
----------------------------------------------------------------

-- | 'unify'
(=:=)
    ::  ( RankedBindingMonad 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 :: (* -> *) -> * -> *).
(RankedBindingMonad t v m, Fallible t v e, MonadTrans em,
 Functor (em m), MonadError e (em m)) =>
UTerm t v -> UTerm t v -> em m (UTerm t v)
unify
{-# INLINE (=:=) #-}
infix 4 =:=, `unify`


-- HACK: apparently this wasn't exported from Control.Unification; so c&p
-- TODO: use IM.insertWith or the like to do this in one pass
--
-- | Update the visited-set with a seclaration 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: keep in sync as we verify correctness.
--
-- | Unify two terms, or throw an error with an explanation of why
-- unification failed. Since bindings are stored in the monad, the
-- two input terms and the output term are all equivalent if
-- unification succeeds. However, the returned value makes use of
-- aggressive opportunistic observable sharing, so it will be more
-- efficient to use it in future calculations than either argument.
unify
    ::  ( RankedBindingMonad t v m
        , Fallible t v e
        , MonadTrans em
        , Functor (em m) -- 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), MonadTrans em, RankedBindingMonad t v m,
 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 -> m (UTerm t v)
=: UTerm t v
t = v -> UTerm t v -> m ()
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
v -> UTerm t v -> m ()
bindVar v
v UTerm t v
t m () -> m (UTerm t v) -> m (UTerm t v)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> UTerm t v -> m (UTerm t v)
forall (m :: * -> *) a. Monad m => a -> m a
return UTerm t v
t
    
    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
                    Rank Word8
rl Maybe (UTerm t v)
mtl <- em m (Rank t v)
-> StateT (IntMap (t (UTerm t v))) (em m) (Rank t v)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (em m (Rank t v)
 -> StateT (IntMap (t (UTerm t v))) (em m) (Rank t v))
-> (m (Rank t v) -> em m (Rank t v))
-> m (Rank t v)
-> StateT (IntMap (t (UTerm t v))) (em m) (Rank t v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (Rank t v) -> em m (Rank t v)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Rank t v) -> StateT (IntMap (t (UTerm t v))) (em m) (Rank t v))
-> m (Rank t v)
-> StateT (IntMap (t (UTerm t v))) (em m) (Rank t v)
forall a b. (a -> b) -> a -> b
$ v -> m (Rank t v)
forall (t :: * -> *) v (m :: * -> *).
RankedBindingMonad t v m =>
v -> m (Rank t v)
lookupRankVar v
vl
                    Rank Word8
rr Maybe (UTerm t v)
mtr <- em m (Rank t v)
-> StateT (IntMap (t (UTerm t v))) (em m) (Rank t v)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (em m (Rank t v)
 -> StateT (IntMap (t (UTerm t v))) (em m) (Rank t v))
-> (m (Rank t v) -> em m (Rank t v))
-> m (Rank t v)
-> StateT (IntMap (t (UTerm t v))) (em m) (Rank t v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (Rank t v) -> em m (Rank t v)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Rank t v) -> StateT (IntMap (t (UTerm t v))) (em m) (Rank t v))
-> m (Rank t v)
-> StateT (IntMap (t (UTerm t v))) (em m) (Rank t v)
forall a b. (a -> b) -> a -> b
$ v -> m (Rank t v)
forall (t :: * -> *) v (m :: * -> *).
RankedBindingMonad t v m =>
v -> m (Rank t v)
lookupRankVar v
vr
                    let cmp :: Ordering
cmp = Word8 -> Word8 -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Word8
rl Word8
rr
                    case (Maybe (UTerm t v)
mtl, Maybe (UTerm t v)
mtr) of
                        (Maybe (UTerm t v)
Nothing, Maybe (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))
-> (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
$
                            case Ordering
cmp of
                            Ordering
LT -> do {                    v
vl v -> UTerm t v -> m (UTerm t v)
forall (m :: * -> *) (t :: * -> *) v.
BindingMonad t v m =>
v -> UTerm t v -> m (UTerm t v)
=: UTerm t v
tr0 }
                            Ordering
EQ -> do { v -> m ()
forall (t :: * -> *) v (m :: * -> *).
RankedBindingMonad t v m =>
v -> m ()
incrementRank v
vr ; v
vl v -> UTerm t v -> m (UTerm t v)
forall (m :: * -> *) (t :: * -> *) v.
BindingMonad t v m =>
v -> UTerm t v -> m (UTerm t v)
=: UTerm t v
tr0 }
                            Ordering
GT -> do {                    v
vr v -> UTerm t v -> m (UTerm t v)
forall (m :: * -> *) (t :: * -> *) v.
BindingMonad t v m =>
v -> UTerm t v -> m (UTerm t v)
=: UTerm t v
tl0 }
                      
                        (Maybe (UTerm t v)
Nothing, Just UTerm t v
tr) -> 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
$
                            case Ordering
cmp of
                            Ordering
LT -> do {                    v
vl v -> UTerm t v -> m (UTerm t v)
forall (m :: * -> *) (t :: * -> *) v.
BindingMonad t v m =>
v -> UTerm t v -> m (UTerm t v)
=: UTerm t v
tr0 }
                            Ordering
EQ -> do { v -> m ()
forall (t :: * -> *) v (m :: * -> *).
RankedBindingMonad t v m =>
v -> m ()
incrementRank v
vr ; v
vl v -> UTerm t v -> m (UTerm t v)
forall (m :: * -> *) (t :: * -> *) v.
BindingMonad t v m =>
v -> UTerm t v -> m (UTerm t v)
=: UTerm t v
tr0 }
                            Ordering
GT -> do { v
vl v -> UTerm t v -> m ()
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
v -> UTerm t v -> m ()
`bindVar` UTerm t v
tr  ; v
vr v -> UTerm t v -> m (UTerm t v)
forall (m :: * -> *) (t :: * -> *) v.
BindingMonad t v m =>
v -> UTerm t v -> m (UTerm t v)
=: UTerm t v
tl0 }
                        
                        (Just UTerm t v
tl, Maybe (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))
-> (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
$
                            case Ordering
cmp of
                            Ordering
LT -> do { v
vr v -> UTerm t v -> m ()
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
v -> UTerm t v -> m ()
`bindVar` UTerm t v
tl  ; v
vl v -> UTerm t v -> m (UTerm t v)
forall (m :: * -> *) (t :: * -> *) v.
BindingMonad t v m =>
v -> UTerm t v -> m (UTerm t v)
=: UTerm t v
tr0 }
                            Ordering
EQ -> do { v -> m ()
forall (t :: * -> *) v (m :: * -> *).
RankedBindingMonad t v m =>
v -> m ()
incrementRank v
vl ; v
vr v -> UTerm t v -> m (UTerm t v)
forall (m :: * -> *) (t :: * -> *) v.
BindingMonad t v m =>
v -> UTerm t v -> m (UTerm t v)
=: UTerm t v
tl0 }
                            Ordering
GT -> do {                    v
vr v -> UTerm t v -> m (UTerm t v)
forall (m :: * -> *) (t :: * -> *) v.
BindingMonad t v m =>
v -> UTerm t v -> m (UTerm t v)
=: 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
                            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
$
                                case Ordering
cmp of
                                Ordering
LT -> do { v
vr v -> UTerm t v -> m ()
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
v -> UTerm t v -> m ()
`bindVar` UTerm t v
t        ; v
vl v -> UTerm t v -> m (UTerm t v)
forall (m :: * -> *) (t :: * -> *) v.
BindingMonad t v m =>
v -> UTerm t v -> m (UTerm t v)
=: UTerm t v
tr0 }
                                Ordering
EQ -> do { v -> UTerm t v -> m ()
forall (t :: * -> *) v (m :: * -> *).
RankedBindingMonad t v m =>
v -> UTerm t v -> m ()
incrementBindVar v
vl UTerm t v
t ; v
vr v -> UTerm t v -> m (UTerm t v)
forall (m :: * -> *) (t :: * -> *) v.
BindingMonad t v m =>
v -> UTerm t v -> m (UTerm t v)
=: UTerm t v
tl0 }
                                Ordering
GT -> do { v
vl v -> UTerm t v -> m ()
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
v -> UTerm t v -> m ()
`bindVar` UTerm t v
t        ; v
vr v -> UTerm t v -> m (UTerm t v)
forall (m :: * -> *) (t :: * -> *) v.
BindingMonad t v m =>
v -> UTerm t v -> m (UTerm t v)
=: UTerm t v
tl0 }
                        (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
                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
$ do
                    v
vl v -> UTerm t v -> m ()
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
v -> UTerm t v -> m ()
`bindVar` UTerm t v
t
                    UTerm t v -> 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
                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
$ do
                    v
vr v -> UTerm t v -> m ()
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
v -> UTerm t v -> m ()
`bindVar` UTerm t v
t
                    UTerm t v -> 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"

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