{-# LANGUAGE MultiParamTypeClasses
           , FlexibleInstances
           , UndecidableInstances
           #-}
{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
----------------------------------------------------------------
--                                                  ~ 2012.03.18
-- |
-- Module      :  Control.Unification.IntVar
-- Copyright   :  Copyright (c) 2007--2015 wren gayle romano
-- License     :  BSD
-- Maintainer  :  wren@community.haskell.org
-- Stability   :  experimental
-- Portability :  semi-portable (MPTCs,...)
--
-- This module defines a state monad for functional pointers
-- represented by integers as keys into an @IntMap@. This technique
-- was independently discovered by Dijkstra et al. This module
-- extends the approach by using a state monad transformer, which
-- can be made into a backtracking state monad by setting the
-- underlying monad to some 'MonadLogic' (part of the @logict@
-- library, described by Kiselyov et al.).
--
--     * Atze Dijkstra, Arie Middelkoop, S. Doaitse Swierstra (2008)
--         /Efficient Functional Unification and Substitution/,
--         Technical Report UU-CS-2008-027, Utrecht University.
--
--     * Oleg Kiselyov, Chung-chieh Shan, Daniel P. Friedman, and
--         Amr Sabry (2005) /Backtracking, Interleaving, and/
--         /Terminating Monad Transformers/, ICFP.
----------------------------------------------------------------
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
----------------------------------------------------------------
----------------------------------------------------------------

-- | A \"mutable\" unification variable implemented by an integer.
-- This provides an entirely pure alternative to truly mutable
-- alternatives (like @STVar@), which can make backtracking easier.
--
-- N.B., because this implementation is pure, we can use it for
-- both ranked and unranked monads.
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)

{-
-- BUG: This part works, but we'd want to change Show IntBindingState too.

instance Show IntVar where
    show (IntVar i) = "IntVar " ++ show (boundedInt2Word i)

-- | Convert an integer to a word, via the continuous mapping that
-- preserves @minBound@ and @maxBound@.
boundedInt2Word :: Int -> Word
boundedInt2Word i
    | i < 0     = fromIntegral (i + maxBound + 1)
    | otherwise = fromIntegral i + fromIntegral (maxBound :: Int) + 1
-}

instance Variable IntVar where
    getVarID :: IntVar -> Int
getVarID (IntVar Int
v) = Int
v


----------------------------------------------------------------
-- | Binding state for 'IntVar'.
data IntBindingState t = IntBindingState
    { IntBindingState t -> Int
nextFreeVar :: {-# UNPACK #-} !Int
    , IntBindingState t -> IntMap (UTerm t IntVar)
varBindings :: IM.IntMap (UTerm t IntVar)
    }

-- Can't derive this because it's an UndecidableInstance
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
"}"

-- | The initial @IntBindingState@.
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


----------------------------------------------------------------
-- | 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 IntBindingT t m a = IBT { IntBindingT t m a -> StateT (IntBindingState t) m a
unIBT :: StateT (IntBindingState t) m a }

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

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

-- BUG: can't reduce dependency to Applicative because of StateT's instance.
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
    IntBindingT t m (a -> b)
x <*> :: IntBindingT t m (a -> b) -> IntBindingT t m a -> IntBindingT t m b
<*> IntBindingT t m a
y = StateT (IntBindingState t) m b -> IntBindingT t m b
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntBindingState t) m a -> IntBindingT t m a
IBT (IntBindingT t m (a -> b) -> StateT (IntBindingState t) m (a -> b)
forall (t :: * -> *) (m :: * -> *) a.
IntBindingT t m a -> StateT (IntBindingState t) m a
unIBT IntBindingT t m (a -> b)
x 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
<*> IntBindingT t m a -> StateT (IntBindingState t) m a
forall (t :: * -> *) (m :: * -> *) a.
IntBindingT t m a -> StateT (IntBindingState t) m a
unIBT IntBindingT t m a
y)
    IntBindingT t m a
x  *> :: IntBindingT t m a -> IntBindingT t m b -> IntBindingT t m b
*> IntBindingT t m b
y = StateT (IntBindingState t) m b -> IntBindingT t m b
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntBindingState t) m a -> IntBindingT t m a
IBT (IntBindingT t m a -> StateT (IntBindingState t) m a
forall (t :: * -> *) (m :: * -> *) a.
IntBindingT t m a -> StateT (IntBindingState t) m a
unIBT IntBindingT t m a
x  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
*> 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
y)
    IntBindingT t m a
x <* :: IntBindingT t m a -> IntBindingT t m b -> IntBindingT t m a
<*  IntBindingT t m b
y = StateT (IntBindingState t) m a -> IntBindingT t m a
forall (t :: * -> *) (m :: * -> *) a.
StateT (IntBindingState t) m a -> IntBindingT t m a
IBT (IntBindingT t m a -> StateT (IntBindingState t) m a
forall (t :: * -> *) (m :: * -> *) a.
IntBindingT t m a -> StateT (IntBindingState t) m a
unIBT IntBindingT t m a
x 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
<*  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
y)

instance (Monad m) => Monad (IntBindingT t m) where
    return :: a -> IntBindingT t m a
return  = 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 (m :: * -> *) a. Monad m => a -> m a
return
    IntBindingT 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 (IntBindingT t m a -> StateT (IntBindingState t) m a
forall (t :: * -> *) (m :: * -> *) a.
IntBindingT t m a -> StateT (IntBindingState t) m a
unIBT IntBindingT 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

-- BUG: can't reduce dependency to Alternative because of StateT's instance.
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
    IntBindingT t m a
x <|> :: IntBindingT t m a -> IntBindingT t m a -> IntBindingT t m a
<|> IntBindingT 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 (IntBindingT t m a -> StateT (IntBindingState t) m a
forall (t :: * -> *) (m :: * -> *) a.
IntBindingT t m a -> StateT (IntBindingState t) m a
unIBT IntBindingT 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
<|> IntBindingT t m a -> StateT (IntBindingState t) m a
forall (t :: * -> *) (m :: * -> *) a.
IntBindingT t m a -> StateT (IntBindingState t) m a
unIBT IntBindingT t m a
y)

instance (MonadPlus m) => MonadPlus (IntBindingT t m) where
    mzero :: IntBindingT t m a
mzero       = 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 (m :: * -> *) a. MonadPlus m => m a
mzero
    mplus :: IntBindingT t m a -> IntBindingT t m a -> IntBindingT t m a
mplus IntBindingT t m a
ml IntBindingT t m a
mr = 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. MonadPlus m => m a -> m a -> m a
mplus (IntBindingT t m a -> StateT (IntBindingState t) m a
forall (t :: * -> *) (m :: * -> *) a.
IntBindingT t m a -> StateT (IntBindingState t) m a
unIBT IntBindingT t m a
ml) (IntBindingT t m a -> StateT (IntBindingState t) m a
forall (t :: * -> *) (m :: * -> *) a.
IntBindingT t m a -> StateT (IntBindingState t) m a
unIBT IntBindingT t m a
mr))

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

-- 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 (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


-- | N.B., you should explicitly apply bindings before calling this
-- function, or else the bindings will be lost
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' }

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