{-# LANGUAGE CPP
, MultiParamTypeClasses
, FlexibleInstances
, UndecidableInstances
#-}
{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
module Control.Unification.IntVar
( IntVar(..)
, IntBindingState()
, IntBindingT()
, runIntBindingT
, evalIntBindingT
, execIntBindingT
) 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
newtype IntVar = IntVar Int
deriving (Int -> IntVar -> ShowS
[IntVar] -> ShowS
IntVar -> String
(Int -> IntVar -> ShowS)
-> (IntVar -> String) -> ([IntVar] -> ShowS) -> Show IntVar
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [IntVar] -> ShowS
$cshowList :: [IntVar] -> ShowS
show :: IntVar -> String
$cshow :: IntVar -> String
showsPrec :: Int -> IntVar -> ShowS
$cshowsPrec :: Int -> IntVar -> ShowS
Show, IntVar -> IntVar -> Bool
(IntVar -> IntVar -> Bool)
-> (IntVar -> IntVar -> Bool) -> Eq IntVar
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: IntVar -> IntVar -> Bool
$c/= :: IntVar -> IntVar -> Bool
== :: IntVar -> IntVar -> Bool
$c== :: IntVar -> IntVar -> Bool
Eq)
instance Variable IntVar where
getVarID :: IntVar -> Int
getVarID (IntVar Int
v) = Int
v
data IntBindingState t = IntBindingState
{ IntBindingState t -> Int
nextFreeVar :: {-# UNPACK #-} !Int
, IntBindingState t -> IntMap (UTerm t IntVar)
varBindings :: IM.IntMap (UTerm t IntVar)
}
instance (Show (t (UTerm t IntVar))) =>
Show (IntBindingState t)
where
show :: IntBindingState t -> String
show (IntBindingState Int
nr IntMap (UTerm t IntVar)
bs) =
String
"IntBindingState { 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 (UTerm t IntVar) -> String
forall a. Show a => a -> String
show IntMap (UTerm t IntVar)
bsString -> ShowS
forall a. [a] -> [a] -> [a]
++String
"}"
emptyIntBindingState :: IntBindingState t
emptyIntBindingState :: IntBindingState t
emptyIntBindingState = Int -> IntMap (UTerm t IntVar) -> IntBindingState t
forall (t :: * -> *).
Int -> IntMap (UTerm t IntVar) -> IntBindingState t
IntBindingState Int
forall a. Bounded a => a
minBound IntMap (UTerm t IntVar)
forall a. IntMap a
IM.empty
newtype IntBindingT t m a = IBT { IntBindingT t m a -> StateT (IntBindingState t) m a
unIBT :: StateT (IntBindingState t) m a }
instance (Functor m) => Functor (IntBindingT t m) where
fmap :: (a -> b) -> IntBindingT t m a -> IntBindingT t m b
fmap a -> b
f = StateT (IntBindingState t) m b -> IntBindingT t m b
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntBindingState t) m a -> IntBindingT t m a
IBT (StateT (IntBindingState t) m b -> IntBindingT t m b)
-> (IntBindingT t m a -> StateT (IntBindingState t) m b)
-> IntBindingT t m a
-> IntBindingT t m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b)
-> StateT (IntBindingState t) m a -> StateT (IntBindingState t) m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f (StateT (IntBindingState t) m a -> StateT (IntBindingState t) m b)
-> (IntBindingT t m a -> StateT (IntBindingState t) m a)
-> IntBindingT t m a
-> StateT (IntBindingState t) m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntBindingT t m a -> StateT (IntBindingState t) m a
forall (t :: * -> *) (m :: * -> *) a.
IntBindingT t m a -> StateT (IntBindingState t) m a
unIBT
instance (Functor m, Monad m) => Applicative (IntBindingT t m) where
pure :: a -> IntBindingT t m a
pure = StateT (IntBindingState t) m a -> IntBindingT t m a
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntBindingState t) m a -> IntBindingT t m a
IBT (StateT (IntBindingState t) m a -> IntBindingT t m a)
-> (a -> StateT (IntBindingState t) m a) -> a -> IntBindingT t m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> StateT (IntBindingState t) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
IBT StateT (IntBindingState t) m (a -> b)
m <*> :: IntBindingT t m (a -> b) -> IntBindingT t m a -> IntBindingT t m b
<*> IBT StateT (IntBindingState t) m a
n = StateT (IntBindingState t) m b -> IntBindingT t m b
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntBindingState t) m a -> IntBindingT t m a
IBT (StateT (IntBindingState t) m (a -> b)
m StateT (IntBindingState t) m (a -> b)
-> StateT (IntBindingState t) m a -> StateT (IntBindingState t) m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT (IntBindingState t) m a
n)
IBT StateT (IntBindingState t) m a
m *> :: IntBindingT t m a -> IntBindingT t m b -> IntBindingT t m b
*> IBT StateT (IntBindingState t) m b
n = StateT (IntBindingState t) m b -> IntBindingT t m b
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntBindingState t) m a -> IntBindingT t m a
IBT (StateT (IntBindingState t) m a
m StateT (IntBindingState t) m a
-> StateT (IntBindingState t) m b -> StateT (IntBindingState t) m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT (IntBindingState t) m b
n)
IBT StateT (IntBindingState t) m a
m <* :: IntBindingT t m a -> IntBindingT t m b -> IntBindingT t m a
<* IBT StateT (IntBindingState t) m b
n = StateT (IntBindingState t) m a -> IntBindingT t m a
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntBindingState t) m a -> IntBindingT t m a
IBT (StateT (IntBindingState t) m a
m StateT (IntBindingState t) m a
-> StateT (IntBindingState t) m b -> StateT (IntBindingState t) m a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* StateT (IntBindingState t) m b
n)
instance (Monad m) => Monad (IntBindingT t m) where
#if (!(MIN_VERSION_base(4,8,0)))
return = pure
#endif
IBT StateT (IntBindingState t) m a
m >>= :: IntBindingT t m a -> (a -> IntBindingT t m b) -> IntBindingT t m b
>>= a -> IntBindingT t m b
f = StateT (IntBindingState t) m b -> IntBindingT t m b
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntBindingState t) m a -> IntBindingT t m a
IBT (StateT (IntBindingState t) m a
m StateT (IntBindingState t) m a
-> (a -> StateT (IntBindingState t) m b)
-> StateT (IntBindingState t) m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IntBindingT t m b -> StateT (IntBindingState t) m b
forall (t :: * -> *) (m :: * -> *) a.
IntBindingT t m a -> StateT (IntBindingState t) m a
unIBT (IntBindingT t m b -> StateT (IntBindingState t) m b)
-> (a -> IntBindingT t m b) -> a -> StateT (IntBindingState t) m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> IntBindingT t m b
f)
instance MonadTrans (IntBindingT t) where
lift :: m a -> IntBindingT t m a
lift = StateT (IntBindingState t) m a -> IntBindingT t m a
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntBindingState t) m a -> IntBindingT t m a
IBT (StateT (IntBindingState t) m a -> IntBindingT t m a)
-> (m a -> StateT (IntBindingState t) m a)
-> m a
-> IntBindingT t m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m a -> StateT (IntBindingState t) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
instance (Functor m, MonadPlus m) => Alternative (IntBindingT t m) where
empty :: IntBindingT t m a
empty = StateT (IntBindingState t) m a -> IntBindingT t m a
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntBindingState t) m a -> IntBindingT t m a
IBT StateT (IntBindingState t) m a
forall (f :: * -> *) a. Alternative f => f a
empty
IBT StateT (IntBindingState t) m a
x <|> :: IntBindingT t m a -> IntBindingT t m a -> IntBindingT t m a
<|> IBT StateT (IntBindingState t) m a
y = StateT (IntBindingState t) m a -> IntBindingT t m a
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntBindingState t) m a -> IntBindingT t m a
IBT (StateT (IntBindingState t) m a
x StateT (IntBindingState t) m a
-> StateT (IntBindingState t) m a -> StateT (IntBindingState t) m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT (IntBindingState t) m a
y)
instance (MonadPlus m) => MonadPlus (IntBindingT t m)
#if (!(MIN_VERSION_base(4,8,0)))
where
mzero = empty
mplus = (<|>)
#endif
instance (Monad m) => MonadState (IntBindingState t) (IntBindingT t m) where
get :: IntBindingT t m (IntBindingState t)
get = StateT (IntBindingState t) m (IntBindingState t)
-> IntBindingT t m (IntBindingState t)
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntBindingState t) m a -> IntBindingT t m a
IBT StateT (IntBindingState t) m (IntBindingState t)
forall s (m :: * -> *). MonadState s m => m s
get
put :: IntBindingState t -> IntBindingT t m ()
put = StateT (IntBindingState t) m () -> IntBindingT t m ()
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntBindingState t) m a -> IntBindingT t m a
IBT (StateT (IntBindingState t) m () -> IntBindingT t m ())
-> (IntBindingState t -> StateT (IntBindingState t) m ())
-> IntBindingState t
-> IntBindingT t m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntBindingState t -> StateT (IntBindingState t) m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put
instance (MonadLogic m, MonadPlus m) => MonadLogic (IntBindingT t m) where
msplit :: IntBindingT t m a -> IntBindingT t m (Maybe (a, IntBindingT t m a))
msplit (IBT StateT (IntBindingState t) m a
m) = StateT (IntBindingState t) m (Maybe (a, IntBindingT t m a))
-> IntBindingT t m (Maybe (a, IntBindingT t m a))
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntBindingState t) m a -> IntBindingT t m a
IBT (Maybe (a, StateT (IntBindingState t) m a)
-> Maybe (a, IntBindingT t m a)
forall a (t :: * -> *) (m :: * -> *) a.
Maybe (a, StateT (IntBindingState t) m a)
-> Maybe (a, IntBindingT t m a)
coerce (Maybe (a, StateT (IntBindingState t) m a)
-> Maybe (a, IntBindingT t m a))
-> StateT
(IntBindingState t) m (Maybe (a, StateT (IntBindingState t) m a))
-> StateT (IntBindingState t) m (Maybe (a, IntBindingT t m a))
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
`liftM` StateT (IntBindingState t) m a
-> StateT
(IntBindingState t) m (Maybe (a, StateT (IntBindingState t) m a))
forall (m :: * -> *) a. MonadLogic m => m a -> m (Maybe (a, m a))
msplit StateT (IntBindingState t) m a
m)
where
coerce :: Maybe (a, StateT (IntBindingState t) m a)
-> Maybe (a, IntBindingT t m a)
coerce Maybe (a, StateT (IntBindingState t) m a)
Nothing = Maybe (a, IntBindingT t m a)
forall a. Maybe a
Nothing
coerce (Just (a
a, StateT (IntBindingState t) m a
m')) = (a, IntBindingT t m a) -> Maybe (a, IntBindingT t m a)
forall a. a -> Maybe a
Just (a
a, StateT (IntBindingState t) m a -> IntBindingT t m a
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntBindingState t) m a -> IntBindingT t m a
IBT StateT (IntBindingState t) m a
m')
interleave :: IntBindingT t m a -> IntBindingT t m a -> IntBindingT t m a
interleave (IBT StateT (IntBindingState t) m a
l) (IBT StateT (IntBindingState t) m a
r) = StateT (IntBindingState t) m a -> IntBindingT t m a
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntBindingState t) m a -> IntBindingT t m a
IBT (StateT (IntBindingState t) m a
-> StateT (IntBindingState t) m a -> StateT (IntBindingState t) m a
forall (m :: * -> *) a. MonadLogic m => m a -> m a -> m a
interleave StateT (IntBindingState t) m a
l StateT (IntBindingState t) m a
r)
IBT StateT (IntBindingState t) m a
m >>- :: IntBindingT t m a -> (a -> IntBindingT t m b) -> IntBindingT t m b
>>- a -> IntBindingT t m b
f = StateT (IntBindingState t) m b -> IntBindingT t m b
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntBindingState t) m a -> IntBindingT t m a
IBT (StateT (IntBindingState t) m a
m StateT (IntBindingState t) m a
-> (a -> StateT (IntBindingState t) m b)
-> StateT (IntBindingState t) m b
forall (m :: * -> *) a b. MonadLogic m => m a -> (a -> m b) -> m b
>>- (IntBindingT t m b -> StateT (IntBindingState t) m b
forall (t :: * -> *) (m :: * -> *) a.
IntBindingT t m a -> StateT (IntBindingState t) m a
unIBT (IntBindingT t m b -> StateT (IntBindingState t) m b)
-> (a -> IntBindingT t m b) -> a -> StateT (IntBindingState t) m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> IntBindingT t m b
f))
ifte :: IntBindingT t m a
-> (a -> IntBindingT t m b)
-> IntBindingT t m b
-> IntBindingT t m b
ifte (IBT StateT (IntBindingState t) m a
b) a -> IntBindingT t m b
t (IBT StateT (IntBindingState t) m b
f) = StateT (IntBindingState t) m b -> IntBindingT t m b
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntBindingState t) m a -> IntBindingT t m a
IBT (StateT (IntBindingState t) m a
-> (a -> StateT (IntBindingState t) m b)
-> StateT (IntBindingState t) m b
-> StateT (IntBindingState t) m b
forall (m :: * -> *) a b.
MonadLogic m =>
m a -> (a -> m b) -> m b -> m b
ifte StateT (IntBindingState t) m a
b (IntBindingT t m b -> StateT (IntBindingState t) m b
forall (t :: * -> *) (m :: * -> *) a.
IntBindingT t m a -> StateT (IntBindingState t) m a
unIBT (IntBindingT t m b -> StateT (IntBindingState t) m b)
-> (a -> IntBindingT t m b) -> a -> StateT (IntBindingState t) m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> IntBindingT t m b
t) StateT (IntBindingState t) m b
f)
once :: IntBindingT t m a -> IntBindingT t m a
once (IBT StateT (IntBindingState t) m a
m) = StateT (IntBindingState t) m a -> IntBindingT t m a
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntBindingState t) m a -> IntBindingT t m a
IBT (StateT (IntBindingState t) m a -> StateT (IntBindingState t) m a
forall (m :: * -> *) a. MonadLogic m => m a -> m a
once StateT (IntBindingState t) m a
m)
runIntBindingT :: IntBindingT t m a -> m (a, IntBindingState t)
runIntBindingT :: IntBindingT t m a -> m (a, IntBindingState t)
runIntBindingT (IBT StateT (IntBindingState t) m a
m) = StateT (IntBindingState t) m a
-> IntBindingState t -> m (a, IntBindingState t)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT (IntBindingState t) m a
m IntBindingState t
forall (t :: * -> *). IntBindingState t
emptyIntBindingState
evalIntBindingT :: (Monad m) => IntBindingT t m a -> m a
evalIntBindingT :: IntBindingT t m a -> m a
evalIntBindingT (IBT StateT (IntBindingState t) m a
m) = StateT (IntBindingState t) m a -> IntBindingState t -> m a
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT StateT (IntBindingState t) m a
m IntBindingState t
forall (t :: * -> *). IntBindingState t
emptyIntBindingState
execIntBindingT :: (Monad m) => IntBindingT t m a -> m (IntBindingState t)
execIntBindingT :: IntBindingT t m a -> m (IntBindingState t)
execIntBindingT (IBT StateT (IntBindingState t) m a
m) = StateT (IntBindingState t) m a
-> IntBindingState t -> m (IntBindingState t)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT StateT (IntBindingState t) m a
m IntBindingState t
forall (t :: * -> *). IntBindingState t
emptyIntBindingState
instance (Unifiable t, Applicative m, Monad m) =>
BindingMonad t IntVar (IntBindingT t m)
where
lookupVar :: IntVar -> IntBindingT t m (Maybe (UTerm t IntVar))
lookupVar (IntVar Int
v) = StateT (IntBindingState t) m (Maybe (UTerm t IntVar))
-> IntBindingT t m (Maybe (UTerm t IntVar))
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntBindingState t) m a -> IntBindingT t m a
IBT (StateT (IntBindingState t) m (Maybe (UTerm t IntVar))
-> IntBindingT t m (Maybe (UTerm t IntVar)))
-> StateT (IntBindingState t) m (Maybe (UTerm t IntVar))
-> IntBindingT t m (Maybe (UTerm t IntVar))
forall a b. (a -> b) -> a -> b
$ (IntBindingState t -> Maybe (UTerm t IntVar))
-> StateT (IntBindingState t) m (Maybe (UTerm t IntVar))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (Int -> IntMap (UTerm t IntVar) -> Maybe (UTerm t IntVar)
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
v (IntMap (UTerm t IntVar) -> Maybe (UTerm t IntVar))
-> (IntBindingState t -> IntMap (UTerm t IntVar))
-> IntBindingState t
-> Maybe (UTerm t IntVar)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntBindingState t -> IntMap (UTerm t IntVar)
forall (t :: * -> *). IntBindingState t -> IntMap (UTerm t IntVar)
varBindings)
freeVar :: IntBindingT t m IntVar
freeVar = StateT (IntBindingState t) m IntVar -> IntBindingT t m IntVar
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntBindingState t) m a -> IntBindingT t m a
IBT (StateT (IntBindingState t) m IntVar -> IntBindingT t m IntVar)
-> StateT (IntBindingState t) m IntVar -> IntBindingT t m IntVar
forall a b. (a -> b) -> a -> b
$ do
IntBindingState t
ibs <- StateT (IntBindingState t) m (IntBindingState t)
forall s (m :: * -> *). MonadState s m => m s
get
let v :: Int
v = IntBindingState t -> Int
forall (t :: * -> *). IntBindingState t -> Int
nextFreeVar IntBindingState 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 (IntBindingState t) m IntVar
forall a. HasCallStack => String -> a
error String
"freeVar: no more variables!"
else do
IntBindingState t -> StateT (IntBindingState t) m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (IntBindingState t -> StateT (IntBindingState t) m ())
-> IntBindingState t -> StateT (IntBindingState t) m ()
forall a b. (a -> b) -> a -> b
$ IntBindingState t
ibs { nextFreeVar :: Int
nextFreeVar = Int
vInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1 }
IntVar -> StateT (IntBindingState t) m IntVar
forall (m :: * -> *) a. Monad m => a -> m a
return (IntVar -> StateT (IntBindingState t) m IntVar)
-> IntVar -> StateT (IntBindingState t) m IntVar
forall a b. (a -> b) -> a -> b
$ Int -> IntVar
IntVar Int
v
newVar :: UTerm t IntVar -> IntBindingT t m IntVar
newVar UTerm t IntVar
t = StateT (IntBindingState t) m IntVar -> IntBindingT t m IntVar
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntBindingState t) m a -> IntBindingT t m a
IBT (StateT (IntBindingState t) m IntVar -> IntBindingT t m IntVar)
-> StateT (IntBindingState t) m IntVar -> IntBindingT t m IntVar
forall a b. (a -> b) -> a -> b
$ do
IntBindingState t
ibs <- StateT (IntBindingState t) m (IntBindingState t)
forall s (m :: * -> *). MonadState s m => m s
get
let v :: Int
v = IntBindingState t -> Int
forall (t :: * -> *). IntBindingState t -> Int
nextFreeVar IntBindingState 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 (IntBindingState t) m IntVar
forall a. HasCallStack => String -> a
error String
"newVar: no more variables!"
else do
let bs' :: IntMap (UTerm t IntVar)
bs' = Int
-> UTerm t IntVar
-> IntMap (UTerm t IntVar)
-> IntMap (UTerm t IntVar)
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
v UTerm t IntVar
t (IntBindingState t -> IntMap (UTerm t IntVar)
forall (t :: * -> *). IntBindingState t -> IntMap (UTerm t IntVar)
varBindings IntBindingState t
ibs)
IntBindingState t -> StateT (IntBindingState t) m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (IntBindingState t -> StateT (IntBindingState t) m ())
-> IntBindingState t -> StateT (IntBindingState t) m ()
forall a b. (a -> b) -> a -> b
$ IntBindingState t
ibs { nextFreeVar :: Int
nextFreeVar = Int
vInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1, varBindings :: IntMap (UTerm t IntVar)
varBindings = IntMap (UTerm t IntVar)
bs' }
IntVar -> StateT (IntBindingState t) m IntVar
forall (m :: * -> *) a. Monad m => a -> m a
return (IntVar -> StateT (IntBindingState t) m IntVar)
-> IntVar -> StateT (IntBindingState t) m IntVar
forall a b. (a -> b) -> a -> b
$ Int -> IntVar
IntVar Int
v
bindVar :: IntVar -> UTerm t IntVar -> IntBindingT t m ()
bindVar (IntVar Int
v) UTerm t IntVar
t = StateT (IntBindingState t) m () -> IntBindingT t m ()
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntBindingState t) m a -> IntBindingT t m a
IBT (StateT (IntBindingState t) m () -> IntBindingT t m ())
-> StateT (IntBindingState t) m () -> IntBindingT t m ()
forall a b. (a -> b) -> a -> b
$ do
IntBindingState t
ibs <- StateT (IntBindingState t) m (IntBindingState t)
forall s (m :: * -> *). MonadState s m => m s
get
let bs' :: IntMap (UTerm t IntVar)
bs' = Int
-> UTerm t IntVar
-> IntMap (UTerm t IntVar)
-> IntMap (UTerm t IntVar)
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
v UTerm t IntVar
t (IntBindingState t -> IntMap (UTerm t IntVar)
forall (t :: * -> *). IntBindingState t -> IntMap (UTerm t IntVar)
varBindings IntBindingState t
ibs)
IntBindingState t -> StateT (IntBindingState t) m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (IntBindingState t -> StateT (IntBindingState t) m ())
-> IntBindingState t -> StateT (IntBindingState t) m ()
forall a b. (a -> b) -> a -> b
$ IntBindingState t
ibs { varBindings :: IntMap (UTerm t IntVar)
varBindings = IntMap (UTerm t IntVar)
bs' }