module Control.Unification.Ranked.STVar
( STRVar()
, STRBinding()
, runSTRBinding
) where
import Prelude hiding (mapM, sequence, foldr, foldr1, foldl, foldl1)
import Data.STRef
import Data.Word (Word8)
#if __GLASGOW_HASKELL__ < 710
import Control.Applicative (Applicative(..))
#endif
import Control.Monad (ap)
import Control.Monad.Trans (lift)
import Control.Monad.ST
import Control.Monad.Reader (ReaderT, runReaderT, ask)
import Control.Unification.Types
data STRVar s t =
STRVar
!Int
!(STRef s Word8)
!(STRef s (Maybe (UTerm t (STRVar s t))))
instance Show (STRVar s t) where
show (STRVar i _ _) = "STRVar " ++ show i
instance Eq (STRVar s t) where
(STRVar i _ _) == (STRVar j _ _) = (i == j)
instance Variable (STRVar s t) where
getVarID (STRVar i _ _) = i
newtype STRBinding s a = STRB { unSTRB :: ReaderT (STRef s Int) (ST s) a }
runSTRBinding :: (forall s. STRBinding s a) -> a
runSTRBinding stb =
runST (newSTRef minBound >>= runReaderT (unSTRB stb))
instance Functor (STRBinding s) where
fmap f = STRB . fmap f . unSTRB
instance Applicative (STRBinding s) where
pure = return
(<*>) = ap
(*>) = (>>)
x <* y = x >>= \a -> y >> return a
instance Monad (STRBinding s) where
return = STRB . return
stb >>= f = STRB (unSTRB stb >>= unSTRB . f)
_newSTRVar
:: String
-> Maybe (UTerm t (STRVar s t))
-> STRBinding s (STRVar s t)
_newSTRVar fun mb = STRB $ do
nr <- ask
lift $ do
n <- readSTRef nr
if n == maxBound
then error $ fun ++ ": no more variables!"
else do
writeSTRef nr $! n+1
rk <- newSTRef 0
ptr <- newSTRef mb
return (STRVar n rk ptr)
instance (Unifiable t) => BindingMonad t (STRVar s t) (STRBinding s) where
lookupVar (STRVar _ _ p) = STRB . lift $ readSTRef p
freeVar = _newSTRVar "freeVar" Nothing
newVar t = _newSTRVar "newVar" (Just t)
bindVar (STRVar _ _ p) t = STRB . lift $ writeSTRef p (Just t)
instance (Unifiable t) =>
RankedBindingMonad t (STRVar s t) (STRBinding s)
where
lookupRankVar (STRVar _ r p) = STRB . lift $ do
n <- readSTRef r
mb <- readSTRef p
return (Rank n mb)
incrementRank (STRVar _ r _) = STRB . lift $ do
n <- readSTRef r
writeSTRef r $! n+1