{-# LANGUAGE MultiParamTypeClasses
           , FlexibleInstances
           , UndecidableInstances
           #-}
{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
----------------------------------------------------------------
--                                                  ~ 2012.03.18
-- |
-- Module      :  Control.Unification.Ranked.IntVar
-- Copyright   :  Copyright (c) 2007--2015 wren gayle romano
-- License     :  BSD
-- Maintainer  :  wren@community.haskell.org
-- Stability   :  highly experimental
-- Portability :  semi-portable (MPTCs,...)
--
-- A ranked variant of "Control.Unification.IntVar".
----------------------------------------------------------------
module Control.Unification.Ranked.IntVar
    ( IntVar(..)
    , IntRBindingState()
    , IntRBindingT()
    , runIntRBindingT
    , evalIntRBindingT
    , execIntRBindingT
    ) where

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

import qualified Data.IntMap as IM
import Control.Applicative
import Control.Monad         (MonadPlus(..), liftM)
import Control.Monad.Trans   (MonadTrans(..))
import Control.Monad.State   (MonadState(..), StateT, runStateT, evalStateT, execStateT, gets)
import Control.Monad.Logic   (MonadLogic(..))
import Control.Unification.Types
import Control.Unification.IntVar (IntVar(..))
----------------------------------------------------------------
----------------------------------------------------------------

-- | Ranked binding state for 'IntVar'.
data IntRBindingState t = IntRBindingState
    { IntRBindingState t -> Int
nextFreeVar :: {-# UNPACK #-} !Int
    , IntRBindingState t -> IntMap (Rank t IntVar)
varBindings :: IM.IntMap (Rank t IntVar)
    }

-- Can't derive this because it's an UndecidableInstance
instance (Show (t (UTerm t IntVar))) =>
    Show (IntRBindingState t)
    where
    show :: IntRBindingState t -> String
show (IntRBindingState Int
nr IntMap (Rank t IntVar)
bs) =
        String
"IntRBindingState { nextFreeVar = "String -> ShowS
forall a. [a] -> [a] -> [a]
++Int -> String
forall a. Show a => a -> String
show Int
nrString -> ShowS
forall a. [a] -> [a] -> [a]
++
        String
", varBindings = "String -> ShowS
forall a. [a] -> [a] -> [a]
++IntMap (Rank t IntVar) -> String
forall a. Show a => a -> String
show IntMap (Rank t IntVar)
bsString -> ShowS
forall a. [a] -> [a] -> [a]
++String
"}"

-- | The initial @IntRBindingState@.
emptyIntRBindingState :: IntRBindingState t
emptyIntRBindingState :: IntRBindingState t
emptyIntRBindingState = Int -> IntMap (Rank t IntVar) -> IntRBindingState t
forall (t :: * -> *).
Int -> IntMap (Rank t IntVar) -> IntRBindingState t
IntRBindingState Int
forall a. Bounded a => a
minBound IntMap (Rank t IntVar)
forall a. IntMap a
IM.empty


----------------------------------------------------------------
-- | A monad for storing 'IntVar' bindings, implemented as a 'StateT'.
-- For a plain state monad, set @m = Identity@; for a backtracking
-- state monad, set @m = Logic@.
newtype IntRBindingT t m a = IRBT { IntRBindingT t m a -> StateT (IntRBindingState t) m a
unIRBT :: StateT (IntRBindingState t) m a }

-- For portability reasons, we're intentionally avoiding
-- -XDeriveFunctor, -XGeneralizedNewtypeDeriving, and the like.

instance (Functor m) => Functor (IntRBindingT t m) where
    fmap :: (a -> b) -> IntRBindingT t m a -> IntRBindingT t m b
fmap a -> b
f = StateT (IntRBindingState t) m b -> IntRBindingT t m b
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntRBindingState t) m a -> IntRBindingT t m a
IRBT (StateT (IntRBindingState t) m b -> IntRBindingT t m b)
-> (IntRBindingT t m a -> StateT (IntRBindingState t) m b)
-> IntRBindingT t m a
-> IntRBindingT t m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b)
-> StateT (IntRBindingState t) m a
-> StateT (IntRBindingState t) m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f (StateT (IntRBindingState t) m a
 -> StateT (IntRBindingState t) m b)
-> (IntRBindingT t m a -> StateT (IntRBindingState t) m a)
-> IntRBindingT t m a
-> StateT (IntRBindingState t) m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntRBindingT t m a -> StateT (IntRBindingState t) m a
forall (t :: * -> *) (m :: * -> *) a.
IntRBindingT t m a -> StateT (IntRBindingState t) m a
unIRBT

-- N.B., it's not possible to reduce the dependency to Applicative.
instance (Functor m, Monad m) => Applicative (IntRBindingT t m) where
    pure :: a -> IntRBindingT t m a
pure    = StateT (IntRBindingState t) m a -> IntRBindingT t m a
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntRBindingState t) m a -> IntRBindingT t m a
IRBT (StateT (IntRBindingState t) m a -> IntRBindingT t m a)
-> (a -> StateT (IntRBindingState t) m a)
-> a
-> IntRBindingT t m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> StateT (IntRBindingState t) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    IntRBindingT t m (a -> b)
x <*> :: IntRBindingT t m (a -> b)
-> IntRBindingT t m a -> IntRBindingT t m b
<*> IntRBindingT t m a
y = StateT (IntRBindingState t) m b -> IntRBindingT t m b
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntRBindingState t) m a -> IntRBindingT t m a
IRBT (IntRBindingT t m (a -> b) -> StateT (IntRBindingState t) m (a -> b)
forall (t :: * -> *) (m :: * -> *) a.
IntRBindingT t m a -> StateT (IntRBindingState t) m a
unIRBT IntRBindingT t m (a -> b)
x StateT (IntRBindingState t) m (a -> b)
-> StateT (IntRBindingState t) m a
-> StateT (IntRBindingState t) m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IntRBindingT t m a -> StateT (IntRBindingState t) m a
forall (t :: * -> *) (m :: * -> *) a.
IntRBindingT t m a -> StateT (IntRBindingState t) m a
unIRBT IntRBindingT t m a
y)
    IntRBindingT t m a
x  *> :: IntRBindingT t m a -> IntRBindingT t m b -> IntRBindingT t m b
*> IntRBindingT t m b
y = StateT (IntRBindingState t) m b -> IntRBindingT t m b
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntRBindingState t) m a -> IntRBindingT t m a
IRBT (IntRBindingT t m a -> StateT (IntRBindingState t) m a
forall (t :: * -> *) (m :: * -> *) a.
IntRBindingT t m a -> StateT (IntRBindingState t) m a
unIRBT IntRBindingT t m a
x  StateT (IntRBindingState t) m a
-> StateT (IntRBindingState t) m b
-> StateT (IntRBindingState t) m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> IntRBindingT t m b -> StateT (IntRBindingState t) m b
forall (t :: * -> *) (m :: * -> *) a.
IntRBindingT t m a -> StateT (IntRBindingState t) m a
unIRBT IntRBindingT t m b
y)
    IntRBindingT t m a
x <* :: IntRBindingT t m a -> IntRBindingT t m b -> IntRBindingT t m a
<*  IntRBindingT t m b
y = StateT (IntRBindingState t) m a -> IntRBindingT t m a
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntRBindingState t) m a -> IntRBindingT t m a
IRBT (IntRBindingT t m a -> StateT (IntRBindingState t) m a
forall (t :: * -> *) (m :: * -> *) a.
IntRBindingT t m a -> StateT (IntRBindingState t) m a
unIRBT IntRBindingT t m a
x StateT (IntRBindingState t) m a
-> StateT (IntRBindingState t) m b
-> StateT (IntRBindingState t) m a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<*  IntRBindingT t m b -> StateT (IntRBindingState t) m b
forall (t :: * -> *) (m :: * -> *) a.
IntRBindingT t m a -> StateT (IntRBindingState t) m a
unIRBT IntRBindingT t m b
y)

instance (Monad m) => Monad (IntRBindingT t m) where
    return :: a -> IntRBindingT t m a
return  = StateT (IntRBindingState t) m a -> IntRBindingT t m a
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntRBindingState t) m a -> IntRBindingT t m a
IRBT (StateT (IntRBindingState t) m a -> IntRBindingT t m a)
-> (a -> StateT (IntRBindingState t) m a)
-> a
-> IntRBindingT t m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> StateT (IntRBindingState t) m a
forall (m :: * -> *) a. Monad m => a -> m a
return
    IntRBindingT t m a
m >>= :: IntRBindingT t m a
-> (a -> IntRBindingT t m b) -> IntRBindingT t m b
>>= a -> IntRBindingT t m b
f = StateT (IntRBindingState t) m b -> IntRBindingT t m b
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntRBindingState t) m a -> IntRBindingT t m a
IRBT (IntRBindingT t m a -> StateT (IntRBindingState t) m a
forall (t :: * -> *) (m :: * -> *) a.
IntRBindingT t m a -> StateT (IntRBindingState t) m a
unIRBT IntRBindingT t m a
m StateT (IntRBindingState t) m a
-> (a -> StateT (IntRBindingState t) m b)
-> StateT (IntRBindingState t) m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IntRBindingT t m b -> StateT (IntRBindingState t) m b
forall (t :: * -> *) (m :: * -> *) a.
IntRBindingT t m a -> StateT (IntRBindingState t) m a
unIRBT (IntRBindingT t m b -> StateT (IntRBindingState t) m b)
-> (a -> IntRBindingT t m b)
-> a
-> StateT (IntRBindingState t) m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> IntRBindingT t m b
f)

instance MonadTrans (IntRBindingT t) where
    lift :: m a -> IntRBindingT t m a
lift = StateT (IntRBindingState t) m a -> IntRBindingT t m a
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntRBindingState t) m a -> IntRBindingT t m a
IRBT (StateT (IntRBindingState t) m a -> IntRBindingT t m a)
-> (m a -> StateT (IntRBindingState t) m a)
-> m a
-> IntRBindingT t m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m a -> StateT (IntRBindingState t) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift

-- BUG: can't reduce dependency to Alternative because of StateT's instance.
instance (Functor m, MonadPlus m) => Alternative (IntRBindingT t m) where
    empty :: IntRBindingT t m a
empty   = StateT (IntRBindingState t) m a -> IntRBindingT t m a
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntRBindingState t) m a -> IntRBindingT t m a
IRBT StateT (IntRBindingState t) m a
forall (f :: * -> *) a. Alternative f => f a
empty
    IntRBindingT t m a
x <|> :: IntRBindingT t m a -> IntRBindingT t m a -> IntRBindingT t m a
<|> IntRBindingT t m a
y = StateT (IntRBindingState t) m a -> IntRBindingT t m a
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntRBindingState t) m a -> IntRBindingT t m a
IRBT (IntRBindingT t m a -> StateT (IntRBindingState t) m a
forall (t :: * -> *) (m :: * -> *) a.
IntRBindingT t m a -> StateT (IntRBindingState t) m a
unIRBT IntRBindingT t m a
x StateT (IntRBindingState t) m a
-> StateT (IntRBindingState t) m a
-> StateT (IntRBindingState t) m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> IntRBindingT t m a -> StateT (IntRBindingState t) m a
forall (t :: * -> *) (m :: * -> *) a.
IntRBindingT t m a -> StateT (IntRBindingState t) m a
unIRBT IntRBindingT t m a
y)

instance (MonadPlus m) => MonadPlus (IntRBindingT t m) where
    mzero :: IntRBindingT t m a
mzero       = StateT (IntRBindingState t) m a -> IntRBindingT t m a
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntRBindingState t) m a -> IntRBindingT t m a
IRBT StateT (IntRBindingState t) m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
    mplus :: IntRBindingT t m a -> IntRBindingT t m a -> IntRBindingT t m a
mplus IntRBindingT t m a
ml IntRBindingT t m a
mr = StateT (IntRBindingState t) m a -> IntRBindingT t m a
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntRBindingState t) m a -> IntRBindingT t m a
IRBT (StateT (IntRBindingState t) m a
-> StateT (IntRBindingState t) m a
-> StateT (IntRBindingState t) m a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus (IntRBindingT t m a -> StateT (IntRBindingState t) m a
forall (t :: * -> *) (m :: * -> *) a.
IntRBindingT t m a -> StateT (IntRBindingState t) m a
unIRBT IntRBindingT t m a
ml) (IntRBindingT t m a -> StateT (IntRBindingState t) m a
forall (t :: * -> *) (m :: * -> *) a.
IntRBindingT t m a -> StateT (IntRBindingState t) m a
unIRBT IntRBindingT t m a
mr))

instance (Monad m) => MonadState (IntRBindingState t) (IntRBindingT t m) where
    get :: IntRBindingT t m (IntRBindingState t)
get = StateT (IntRBindingState t) m (IntRBindingState t)
-> IntRBindingT t m (IntRBindingState t)
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntRBindingState t) m a -> IntRBindingT t m a
IRBT StateT (IntRBindingState t) m (IntRBindingState t)
forall s (m :: * -> *). MonadState s m => m s
get
    put :: IntRBindingState t -> IntRBindingT t m ()
put = StateT (IntRBindingState t) m () -> IntRBindingT t m ()
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntRBindingState t) m a -> IntRBindingT t m a
IRBT (StateT (IntRBindingState t) m () -> IntRBindingT t m ())
-> (IntRBindingState t -> StateT (IntRBindingState t) m ())
-> IntRBindingState t
-> IntRBindingT t m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntRBindingState t -> StateT (IntRBindingState t) m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put

-- N.B., we already have (MonadLogic m) => MonadLogic (StateT s m),
-- provided that logict is compiled against the same mtl/monads-fd
-- we're getting StateT from. Otherwise we'll get a bunch of warnings
-- here.
instance (MonadLogic m, MonadPlus m) => MonadLogic (IntRBindingT t m) where
    msplit :: IntRBindingT t m a
-> IntRBindingT t m (Maybe (a, IntRBindingT t m a))
msplit (IRBT StateT (IntRBindingState t) m a
m) = StateT (IntRBindingState t) m (Maybe (a, IntRBindingT t m a))
-> IntRBindingT t m (Maybe (a, IntRBindingT t m a))
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntRBindingState t) m a -> IntRBindingT t m a
IRBT (Maybe (a, StateT (IntRBindingState t) m a)
-> Maybe (a, IntRBindingT t m a)
forall a (t :: * -> *) (m :: * -> *) a.
Maybe (a, StateT (IntRBindingState t) m a)
-> Maybe (a, IntRBindingT t m a)
coerce (Maybe (a, StateT (IntRBindingState t) m a)
 -> Maybe (a, IntRBindingT t m a))
-> StateT
     (IntRBindingState t) m (Maybe (a, StateT (IntRBindingState t) m a))
-> StateT (IntRBindingState t) m (Maybe (a, IntRBindingT t m a))
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
`liftM` StateT (IntRBindingState t) m a
-> StateT
     (IntRBindingState t) m (Maybe (a, StateT (IntRBindingState t) m a))
forall (m :: * -> *) a. MonadLogic m => m a -> m (Maybe (a, m a))
msplit StateT (IntRBindingState t) m a
m)
        where
        coerce :: Maybe (a, StateT (IntRBindingState t) m a)
-> Maybe (a, IntRBindingT t m a)
coerce Maybe (a, StateT (IntRBindingState t) m a)
Nothing        = Maybe (a, IntRBindingT t m a)
forall a. Maybe a
Nothing
        coerce (Just (a
a, StateT (IntRBindingState t) m a
m')) = (a, IntRBindingT t m a) -> Maybe (a, IntRBindingT t m a)
forall a. a -> Maybe a
Just (a
a, StateT (IntRBindingState t) m a -> IntRBindingT t m a
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntRBindingState t) m a -> IntRBindingT t m a
IRBT StateT (IntRBindingState t) m a
m')
    
    interleave :: IntRBindingT t m a -> IntRBindingT t m a -> IntRBindingT t m a
interleave (IRBT StateT (IntRBindingState t) m a
l) (IRBT StateT (IntRBindingState t) m a
r) = StateT (IntRBindingState t) m a -> IntRBindingT t m a
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntRBindingState t) m a -> IntRBindingT t m a
IRBT (StateT (IntRBindingState t) m a
-> StateT (IntRBindingState t) m a
-> StateT (IntRBindingState t) m a
forall (m :: * -> *) a. MonadLogic m => m a -> m a -> m a
interleave StateT (IntRBindingState t) m a
l StateT (IntRBindingState t) m a
r)
    
    IRBT StateT (IntRBindingState t) m a
m >>- :: IntRBindingT t m a
-> (a -> IntRBindingT t m b) -> IntRBindingT t m b
>>- a -> IntRBindingT t m b
f = StateT (IntRBindingState t) m b -> IntRBindingT t m b
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntRBindingState t) m a -> IntRBindingT t m a
IRBT (StateT (IntRBindingState t) m a
m StateT (IntRBindingState t) m a
-> (a -> StateT (IntRBindingState t) m b)
-> StateT (IntRBindingState t) m b
forall (m :: * -> *) a b. MonadLogic m => m a -> (a -> m b) -> m b
>>- (IntRBindingT t m b -> StateT (IntRBindingState t) m b
forall (t :: * -> *) (m :: * -> *) a.
IntRBindingT t m a -> StateT (IntRBindingState t) m a
unIRBT (IntRBindingT t m b -> StateT (IntRBindingState t) m b)
-> (a -> IntRBindingT t m b)
-> a
-> StateT (IntRBindingState t) m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> IntRBindingT t m b
f))
    
    ifte :: IntRBindingT t m a
-> (a -> IntRBindingT t m b)
-> IntRBindingT t m b
-> IntRBindingT t m b
ifte (IRBT StateT (IntRBindingState t) m a
b) a -> IntRBindingT t m b
t (IRBT StateT (IntRBindingState t) m b
f) = StateT (IntRBindingState t) m b -> IntRBindingT t m b
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntRBindingState t) m a -> IntRBindingT t m a
IRBT (StateT (IntRBindingState t) m a
-> (a -> StateT (IntRBindingState t) m b)
-> StateT (IntRBindingState t) m b
-> StateT (IntRBindingState t) m b
forall (m :: * -> *) a b.
MonadLogic m =>
m a -> (a -> m b) -> m b -> m b
ifte StateT (IntRBindingState t) m a
b (IntRBindingT t m b -> StateT (IntRBindingState t) m b
forall (t :: * -> *) (m :: * -> *) a.
IntRBindingT t m a -> StateT (IntRBindingState t) m a
unIRBT (IntRBindingT t m b -> StateT (IntRBindingState t) m b)
-> (a -> IntRBindingT t m b)
-> a
-> StateT (IntRBindingState t) m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> IntRBindingT t m b
t) StateT (IntRBindingState t) m b
f)
    
    once :: IntRBindingT t m a -> IntRBindingT t m a
once (IRBT StateT (IntRBindingState t) m a
m) = StateT (IntRBindingState t) m a -> IntRBindingT t m a
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntRBindingState t) m a -> IntRBindingT t m a
IRBT (StateT (IntRBindingState t) m a -> StateT (IntRBindingState t) m a
forall (m :: * -> *) a. MonadLogic m => m a -> m a
once StateT (IntRBindingState t) m a
m)

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

runIntRBindingT :: IntRBindingT t m a -> m (a, IntRBindingState t)
runIntRBindingT :: IntRBindingT t m a -> m (a, IntRBindingState t)
runIntRBindingT (IRBT StateT (IntRBindingState t) m a
m) = StateT (IntRBindingState t) m a
-> IntRBindingState t -> m (a, IntRBindingState t)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT (IntRBindingState t) m a
m IntRBindingState t
forall (t :: * -> *). IntRBindingState t
emptyIntRBindingState


-- | N.B., you should explicitly apply bindings before calling this
-- function, or else the bindings will be lost
evalIntRBindingT :: (Monad m) => IntRBindingT t m a -> m a
evalIntRBindingT :: IntRBindingT t m a -> m a
evalIntRBindingT (IRBT StateT (IntRBindingState t) m a
m) = StateT (IntRBindingState t) m a -> IntRBindingState t -> m a
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT StateT (IntRBindingState t) m a
m IntRBindingState t
forall (t :: * -> *). IntRBindingState t
emptyIntRBindingState


execIntRBindingT :: (Monad m) => IntRBindingT t m a -> m (IntRBindingState t)
execIntRBindingT :: IntRBindingT t m a -> m (IntRBindingState t)
execIntRBindingT (IRBT StateT (IntRBindingState t) m a
m) = StateT (IntRBindingState t) m a
-> IntRBindingState t -> m (IntRBindingState t)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT StateT (IntRBindingState t) m a
m IntRBindingState t
forall (t :: * -> *). IntRBindingState t
emptyIntRBindingState

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

instance (Unifiable t, Applicative m, Monad m) =>
    BindingMonad t IntVar (IntRBindingT t m)
    where
    
    lookupVar :: IntVar -> IntRBindingT t m (Maybe (UTerm t IntVar))
lookupVar (IntVar Int
v) = StateT (IntRBindingState t) m (Maybe (UTerm t IntVar))
-> IntRBindingT t m (Maybe (UTerm t IntVar))
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntRBindingState t) m a -> IntRBindingT t m a
IRBT (StateT (IntRBindingState t) m (Maybe (UTerm t IntVar))
 -> IntRBindingT t m (Maybe (UTerm t IntVar)))
-> StateT (IntRBindingState t) m (Maybe (UTerm t IntVar))
-> IntRBindingT t m (Maybe (UTerm t IntVar))
forall a b. (a -> b) -> a -> b
$ do
        Maybe (Rank t IntVar)
mb <- (IntRBindingState t -> Maybe (Rank t IntVar))
-> StateT (IntRBindingState t) m (Maybe (Rank t IntVar))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (Int -> IntMap (Rank t IntVar) -> Maybe (Rank t IntVar)
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
v (IntMap (Rank t IntVar) -> Maybe (Rank t IntVar))
-> (IntRBindingState t -> IntMap (Rank t IntVar))
-> IntRBindingState t
-> Maybe (Rank t IntVar)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntRBindingState t -> IntMap (Rank t IntVar)
forall (t :: * -> *). IntRBindingState t -> IntMap (Rank t IntVar)
varBindings)
        case Maybe (Rank t IntVar)
mb of
            Maybe (Rank t IntVar)
Nothing           -> Maybe (UTerm t IntVar)
-> StateT (IntRBindingState t) m (Maybe (UTerm t IntVar))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (UTerm t IntVar)
forall a. Maybe a
Nothing
            Just (Rank Word8
_ Maybe (UTerm t IntVar)
mb') -> Maybe (UTerm t IntVar)
-> StateT (IntRBindingState t) m (Maybe (UTerm t IntVar))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (UTerm t IntVar)
mb'
    
    freeVar :: IntRBindingT t m IntVar
freeVar = StateT (IntRBindingState t) m IntVar -> IntRBindingT t m IntVar
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntRBindingState t) m a -> IntRBindingT t m a
IRBT (StateT (IntRBindingState t) m IntVar -> IntRBindingT t m IntVar)
-> StateT (IntRBindingState t) m IntVar -> IntRBindingT t m IntVar
forall a b. (a -> b) -> a -> b
$ do
        IntRBindingState t
ibs <- StateT (IntRBindingState t) m (IntRBindingState t)
forall s (m :: * -> *). MonadState s m => m s
get
        let v :: Int
v = IntRBindingState t -> Int
forall (t :: * -> *). IntRBindingState t -> Int
nextFreeVar IntRBindingState t
ibs
        if  Int
v Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
forall a. Bounded a => a
maxBound
            then String -> StateT (IntRBindingState t) m IntVar
forall a. HasCallStack => String -> a
error String
"freeVar: no more variables!"
            else do
                IntRBindingState t -> StateT (IntRBindingState t) m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (IntRBindingState t -> StateT (IntRBindingState t) m ())
-> IntRBindingState t -> StateT (IntRBindingState t) m ()
forall a b. (a -> b) -> a -> b
$ IntRBindingState t
ibs { nextFreeVar :: Int
nextFreeVar = Int
vInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1 }
                IntVar -> StateT (IntRBindingState t) m IntVar
forall (m :: * -> *) a. Monad m => a -> m a
return (IntVar -> StateT (IntRBindingState t) m IntVar)
-> IntVar -> StateT (IntRBindingState t) m IntVar
forall a b. (a -> b) -> a -> b
$ Int -> IntVar
IntVar Int
v
    
    newVar :: UTerm t IntVar -> IntRBindingT t m IntVar
newVar UTerm t IntVar
t = StateT (IntRBindingState t) m IntVar -> IntRBindingT t m IntVar
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntRBindingState t) m a -> IntRBindingT t m a
IRBT (StateT (IntRBindingState t) m IntVar -> IntRBindingT t m IntVar)
-> StateT (IntRBindingState t) m IntVar -> IntRBindingT t m IntVar
forall a b. (a -> b) -> a -> b
$ do
        IntRBindingState t
ibs <- StateT (IntRBindingState t) m (IntRBindingState t)
forall s (m :: * -> *). MonadState s m => m s
get
        let v :: Int
v = IntRBindingState t -> Int
forall (t :: * -> *). IntRBindingState t -> Int
nextFreeVar IntRBindingState t
ibs
        if  Int
v Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
forall a. Bounded a => a
maxBound
            then String -> StateT (IntRBindingState t) m IntVar
forall a. HasCallStack => String -> a
error String
"newVar: no more variables!"
            else do
                let bs' :: IntMap (Rank t IntVar)
bs' = Int
-> Rank t IntVar
-> IntMap (Rank t IntVar)
-> IntMap (Rank t IntVar)
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
v (Word8 -> Maybe (UTerm t IntVar) -> Rank t IntVar
forall (t :: * -> *) v. Word8 -> Maybe (UTerm t v) -> Rank t v
Rank Word8
0 (UTerm t IntVar -> Maybe (UTerm t IntVar)
forall a. a -> Maybe a
Just UTerm t IntVar
t)) (IntRBindingState t -> IntMap (Rank t IntVar)
forall (t :: * -> *). IntRBindingState t -> IntMap (Rank t IntVar)
varBindings IntRBindingState t
ibs)
                IntRBindingState t -> StateT (IntRBindingState t) m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (IntRBindingState t -> StateT (IntRBindingState t) m ())
-> IntRBindingState t -> StateT (IntRBindingState t) m ()
forall a b. (a -> b) -> a -> b
$ IntRBindingState t
ibs { nextFreeVar :: Int
nextFreeVar = Int
vInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1, varBindings :: IntMap (Rank t IntVar)
varBindings = IntMap (Rank t IntVar)
bs' }
                IntVar -> StateT (IntRBindingState t) m IntVar
forall (m :: * -> *) a. Monad m => a -> m a
return (IntVar -> StateT (IntRBindingState t) m IntVar)
-> IntVar -> StateT (IntRBindingState t) m IntVar
forall a b. (a -> b) -> a -> b
$ Int -> IntVar
IntVar Int
v
    
    bindVar :: IntVar -> UTerm t IntVar -> IntRBindingT t m ()
bindVar (IntVar Int
v) UTerm t IntVar
t = StateT (IntRBindingState t) m () -> IntRBindingT t m ()
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntRBindingState t) m a -> IntRBindingT t m a
IRBT (StateT (IntRBindingState t) m () -> IntRBindingT t m ())
-> StateT (IntRBindingState t) m () -> IntRBindingT t m ()
forall a b. (a -> b) -> a -> b
$ do
        IntRBindingState t
ibs <- StateT (IntRBindingState t) m (IntRBindingState t)
forall s (m :: * -> *). MonadState s m => m s
get
        let bs' :: IntMap (Rank t IntVar)
bs' = (Rank t IntVar -> Rank t IntVar -> Rank t IntVar)
-> Int
-> Rank t IntVar
-> IntMap (Rank t IntVar)
-> IntMap (Rank t IntVar)
forall a. (a -> a -> a) -> Int -> a -> IntMap a -> IntMap a
IM.insertWith Rank t IntVar -> Rank t IntVar -> Rank t IntVar
forall (t :: * -> *) v (t :: * -> *) v.
Rank t v -> Rank t v -> Rank t v
f Int
v (Word8 -> Maybe (UTerm t IntVar) -> Rank t IntVar
forall (t :: * -> *) v. Word8 -> Maybe (UTerm t v) -> Rank t v
Rank Word8
0 (UTerm t IntVar -> Maybe (UTerm t IntVar)
forall a. a -> Maybe a
Just UTerm t IntVar
t)) (IntRBindingState t -> IntMap (Rank t IntVar)
forall (t :: * -> *). IntRBindingState t -> IntMap (Rank t IntVar)
varBindings IntRBindingState t
ibs)
            f :: Rank t v -> Rank t v -> Rank t v
f (Rank Word8
_0 Maybe (UTerm t v)
jt) (Rank Word8
r Maybe (UTerm t v)
_) = Word8 -> Maybe (UTerm t v) -> Rank t v
forall (t :: * -> *) v. Word8 -> Maybe (UTerm t v) -> Rank t v
Rank Word8
r Maybe (UTerm t v)
jt
        IntRBindingState t -> StateT (IntRBindingState t) m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (IntRBindingState t -> StateT (IntRBindingState t) m ())
-> IntRBindingState t -> StateT (IntRBindingState t) m ()
forall a b. (a -> b) -> a -> b
$ IntRBindingState t
ibs { varBindings :: IntMap (Rank t IntVar)
varBindings = IntMap (Rank t IntVar)
bs' }
    
    
instance (Unifiable t, Applicative m, Monad m) =>
    RankedBindingMonad t IntVar (IntRBindingT t m)
    where
    lookupRankVar :: IntVar -> IntRBindingT t m (Rank t IntVar)
lookupRankVar (IntVar Int
v) = StateT (IntRBindingState t) m (Rank t IntVar)
-> IntRBindingT t m (Rank t IntVar)
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntRBindingState t) m a -> IntRBindingT t m a
IRBT (StateT (IntRBindingState t) m (Rank t IntVar)
 -> IntRBindingT t m (Rank t IntVar))
-> StateT (IntRBindingState t) m (Rank t IntVar)
-> IntRBindingT t m (Rank t IntVar)
forall a b. (a -> b) -> a -> b
$ do
        Maybe (Rank t IntVar)
mb <- (IntRBindingState t -> Maybe (Rank t IntVar))
-> StateT (IntRBindingState t) m (Maybe (Rank t IntVar))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (Int -> IntMap (Rank t IntVar) -> Maybe (Rank t IntVar)
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
v (IntMap (Rank t IntVar) -> Maybe (Rank t IntVar))
-> (IntRBindingState t -> IntMap (Rank t IntVar))
-> IntRBindingState t
-> Maybe (Rank t IntVar)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntRBindingState t -> IntMap (Rank t IntVar)
forall (t :: * -> *). IntRBindingState t -> IntMap (Rank t IntVar)
varBindings)
        case Maybe (Rank t IntVar)
mb of
            Maybe (Rank t IntVar)
Nothing -> Rank t IntVar -> StateT (IntRBindingState t) m (Rank t IntVar)
forall (m :: * -> *) a. Monad m => a -> m a
return (Word8 -> Maybe (UTerm t IntVar) -> Rank t IntVar
forall (t :: * -> *) v. Word8 -> Maybe (UTerm t v) -> Rank t v
Rank Word8
0 Maybe (UTerm t IntVar)
forall a. Maybe a
Nothing)
            Just Rank t IntVar
rk -> Rank t IntVar -> StateT (IntRBindingState t) m (Rank t IntVar)
forall (m :: * -> *) a. Monad m => a -> m a
return Rank t IntVar
rk
    
    incrementRank :: IntVar -> IntRBindingT t m ()
incrementRank (IntVar Int
v) = StateT (IntRBindingState t) m () -> IntRBindingT t m ()
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntRBindingState t) m a -> IntRBindingT t m a
IRBT (StateT (IntRBindingState t) m () -> IntRBindingT t m ())
-> StateT (IntRBindingState t) m () -> IntRBindingT t m ()
forall a b. (a -> b) -> a -> b
$ do
        IntRBindingState t
ibs <- StateT (IntRBindingState t) m (IntRBindingState t)
forall s (m :: * -> *). MonadState s m => m s
get
        let bs' :: IntMap (Rank t IntVar)
bs' = (Rank t IntVar -> Rank t IntVar -> Rank t IntVar)
-> Int
-> Rank t IntVar
-> IntMap (Rank t IntVar)
-> IntMap (Rank t IntVar)
forall a. (a -> a -> a) -> Int -> a -> IntMap a -> IntMap a
IM.insertWith Rank t IntVar -> Rank t IntVar -> Rank t IntVar
forall (t :: * -> *) v (t :: * -> *) v.
Rank t v -> Rank t v -> Rank t v
f Int
v (Word8 -> Maybe (UTerm t IntVar) -> Rank t IntVar
forall (t :: * -> *) v. Word8 -> Maybe (UTerm t v) -> Rank t v
Rank Word8
1 Maybe (UTerm t IntVar)
forall a. Maybe a
Nothing) (IntRBindingState t -> IntMap (Rank t IntVar)
forall (t :: * -> *). IntRBindingState t -> IntMap (Rank t IntVar)
varBindings IntRBindingState t
ibs)
            f :: Rank t v -> Rank t v -> Rank t v
f (Rank Word8
_1 Maybe (UTerm t v)
_n) (Rank Word8
r Maybe (UTerm t v)
mb) = Word8 -> Maybe (UTerm t v) -> Rank t v
forall (t :: * -> *) v. Word8 -> Maybe (UTerm t v) -> Rank t v
Rank (Word8
rWord8 -> Word8 -> Word8
forall a. Num a => a -> a -> a
+Word8
1) Maybe (UTerm t v)
mb
        IntRBindingState t -> StateT (IntRBindingState t) m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (IntRBindingState t -> StateT (IntRBindingState t) m ())
-> IntRBindingState t -> StateT (IntRBindingState t) m ()
forall a b. (a -> b) -> a -> b
$ IntRBindingState t
ibs { varBindings :: IntMap (Rank t IntVar)
varBindings = IntMap (Rank t IntVar)
bs' }
    
    incrementBindVar :: IntVar -> UTerm t IntVar -> IntRBindingT t m ()
incrementBindVar (IntVar Int
v) UTerm t IntVar
t = StateT (IntRBindingState t) m () -> IntRBindingT t m ()
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntRBindingState t) m a -> IntRBindingT t m a
IRBT (StateT (IntRBindingState t) m () -> IntRBindingT t m ())
-> StateT (IntRBindingState t) m () -> IntRBindingT t m ()
forall a b. (a -> b) -> a -> b
$ do
        IntRBindingState t
ibs <- StateT (IntRBindingState t) m (IntRBindingState t)
forall s (m :: * -> *). MonadState s m => m s
get
        let bs' :: IntMap (Rank t IntVar)
bs' = (Rank t IntVar -> Rank t IntVar -> Rank t IntVar)
-> Int
-> Rank t IntVar
-> IntMap (Rank t IntVar)
-> IntMap (Rank t IntVar)
forall a. (a -> a -> a) -> Int -> a -> IntMap a -> IntMap a
IM.insertWith Rank t IntVar -> Rank t IntVar -> Rank t IntVar
forall (t :: * -> *) v (t :: * -> *) v.
Rank t v -> Rank t v -> Rank t v
f Int
v (Word8 -> Maybe (UTerm t IntVar) -> Rank t IntVar
forall (t :: * -> *) v. Word8 -> Maybe (UTerm t v) -> Rank t v
Rank Word8
1 (UTerm t IntVar -> Maybe (UTerm t IntVar)
forall a. a -> Maybe a
Just UTerm t IntVar
t)) (IntRBindingState t -> IntMap (Rank t IntVar)
forall (t :: * -> *). IntRBindingState t -> IntMap (Rank t IntVar)
varBindings IntRBindingState t
ibs)
            f :: Rank t v -> Rank t v -> Rank t v
f (Rank Word8
_1 Maybe (UTerm t v)
jt) (Rank Word8
r Maybe (UTerm t v)
_) = Word8 -> Maybe (UTerm t v) -> Rank t v
forall (t :: * -> *) v. Word8 -> Maybe (UTerm t v) -> Rank t v
Rank (Word8
rWord8 -> Word8 -> Word8
forall a. Num a => a -> a -> a
+Word8
1) Maybe (UTerm t v)
jt
        IntRBindingState t -> StateT (IntRBindingState t) m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (IntRBindingState t -> StateT (IntRBindingState t) m ())
-> IntRBindingState t -> StateT (IntRBindingState t) m ()
forall a b. (a -> b) -> a -> b
$ IntRBindingState t
ibs { varBindings :: IntMap (Rank t IntVar)
varBindings = IntMap (Rank t IntVar)
bs' }

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