-- 
-- (c) Susumu Katayama
--

Everything written in this module can be rewritten using StateT.
When I wrote this first (around 2003?) I did not know the term `Monad Transformer' and I reinvented it....

\begin{code}
{-# LANGUAGE CPP, FlexibleInstances #-}
module MagicHaskeller.PriorSubsts where

import Control.Monad
import Control.Applicative -- necessary for backward compatibility
import Control.Monad.Search.Combinatorial
-- import Control.Monad.Search.BalancedMerge
import MagicHaskeller.Types
import Data.Array.IArray
#ifdef SEMIGROUP
import Data.Semigroup
#endif
import Data.Monoid
import MagicHaskeller.T10(mergeWithBy)

-- import T10(nubSortBy)
import Data.List

import Debug.Trace

-- sumPS :: [PriorSubsts Matrix a] -> PriorSubsts Matrix a
-- sumPS pss = PS $ \s i -> sumMx [ f s i | PS f <- pss]

substOKPS :: (Functor m, Monad m) => String -> PriorSubsts m ()
substOKPS :: String -> PriorSubsts m ()
substOKPS String
str = do Subst
subst <- PriorSubsts m Subst
forall (m :: * -> *). Monad m => PriorSubsts m Subst
getSubst
                   if Subst -> Bool
substOK Subst
subst then () -> PriorSubsts m ()
forall (m :: * -> *) a. Monad m => a -> m a
return () else String -> PriorSubsts m ()
forall a. HasCallStack => String -> a
error (String
str String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"subst not OK. subst = "String -> String -> String
forall a. [a] -> [a] -> [a]
++Subst -> String
forall a. Show a => a -> String
show Subst
subst)

monsubst :: (Functor m, Monad m) => PriorSubsts m ()
monsubst :: PriorSubsts m ()
monsubst = do Subst
s <- PriorSubsts m Subst
forall (m :: * -> *). Monad m => PriorSubsts m Subst
getSubst
              String -> PriorSubsts m () -> PriorSubsts m ()
forall a. String -> a -> a
trace (String
"subst = "String -> String -> String
forall a. [a] -> [a] -> [a]
++Subst -> String
forall a. Show a => a -> String
show Subst
s) (PriorSubsts m () -> PriorSubsts m ())
-> PriorSubsts m () -> PriorSubsts m ()
forall a b. (a -> b) -> a -> b
$ () -> PriorSubsts m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

mkPS :: Monad m => m a -> PriorSubsts m a
mkPS :: m a -> PriorSubsts m a
mkPS m a
x = (Subst -> TyVar -> m (a, Subst, TyVar)) -> PriorSubsts m a
forall (m :: * -> *) a.
(Subst -> TyVar -> m (a, Subst, TyVar)) -> PriorSubsts m a
PS (\Subst
subst TyVar
mx -> m a
x m a -> (a -> m (a, Subst, TyVar)) -> m (a, Subst, TyVar)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
a -> (a, Subst, TyVar) -> m (a, Subst, TyVar)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
a,Subst
subst,TyVar
mx))


runPS :: Monad m => PriorSubsts m a -> m a
runPS :: PriorSubsts m a -> m a
runPS (PS Subst -> TyVar -> m (a, Subst, TyVar)
f) = do (a
x,Subst
_,TyVar
_) <- Subst -> TyVar -> m (a, Subst, TyVar)
f Subst
forall a. [a]
emptySubst TyVar
0
                  a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x

-- delayPS :: (Delay (m a)) => PriorSubsts m a -> PriorSubsts m a
-- delayPS = convertPS delay
delayPS :: PriorSubsts m a -> PriorSubsts m a
delayPS (PS Subst -> TyVar -> m (a, Subst, TyVar)
f) = (Subst -> TyVar -> m (a, Subst, TyVar)) -> PriorSubsts m a
forall (m :: * -> *) a.
(Subst -> TyVar -> m (a, Subst, TyVar)) -> PriorSubsts m a
PS Subst -> TyVar -> m (a, Subst, TyVar)
g where g :: Subst -> TyVar -> m (a, Subst, TyVar)
g Subst
s TyVar
i = m (a, Subst, TyVar) -> m (a, Subst, TyVar)
forall (m :: * -> *) a. Delay m => m a -> m a
delay (Subst -> TyVar -> m (a, Subst, TyVar)
f Subst
s TyVar
i)
ndelayPS :: Int -> PriorSubsts m a -> PriorSubsts m a
ndelayPS Int
n (PS Subst -> TyVar -> m (a, Subst, TyVar)
f) = (Subst -> TyVar -> m (a, Subst, TyVar)) -> PriorSubsts m a
forall (m :: * -> *) a.
(Subst -> TyVar -> m (a, Subst, TyVar)) -> PriorSubsts m a
PS Subst -> TyVar -> m (a, Subst, TyVar)
g where g :: Subst -> TyVar -> m (a, Subst, TyVar)
g Subst
s TyVar
i = Int -> m (a, Subst, TyVar) -> m (a, Subst, TyVar)
forall (m :: * -> *) a. Delay m => Int -> m a -> m a
ndelay Int
n (Subst -> TyVar -> m (a, Subst, TyVar)
f Subst
s TyVar
i)

{-# SPECIALIZE convertPS :: ([(a,Subst,TyVar)] -> Recomp (a,Subst,TyVar)) -> PriorSubsts [] a -> PriorSubsts Recomp a #-}
{-# SPECIALIZE convertPS :: ([(a,Subst,TyVar)] -> [(a,Subst,TyVar)]) -> PriorSubsts [] a -> PriorSubsts [] a #-}
convertPS :: (m (a,Subst,TyVar) -> n (b,Subst,TyVar)) -> PriorSubsts m a -> PriorSubsts n b
convertPS :: (m (a, Subst, TyVar) -> n (b, Subst, TyVar))
-> PriorSubsts m a -> PriorSubsts n b
convertPS m (a, Subst, TyVar) -> n (b, Subst, TyVar)
f (PS Subst -> TyVar -> m (a, Subst, TyVar)
g) = (Subst -> TyVar -> n (b, Subst, TyVar)) -> PriorSubsts n b
forall (m :: * -> *) a.
(Subst -> TyVar -> m (a, Subst, TyVar)) -> PriorSubsts m a
PS Subst -> TyVar -> n (b, Subst, TyVar)
h where h :: Subst -> TyVar -> n (b, Subst, TyVar)
h Subst
s TyVar
i = m (a, Subst, TyVar) -> n (b, Subst, TyVar)
f (Subst -> TyVar -> m (a, Subst, TyVar)
g Subst
s TyVar
i)

newtype PriorSubsts m a = PS {PriorSubsts m a -> Subst -> TyVar -> m (a, Subst, TyVar)
unPS :: Subst -> TyVar -> m (a, Subst, TyVar)}
instance (Functor m, Monad m) => Applicative (PriorSubsts m) where
    {-# SPECIALIZE instance Applicative (PriorSubsts []) #-}
    pure :: a -> PriorSubsts m a
pure a
x = (Subst -> TyVar -> m (a, Subst, TyVar)) -> PriorSubsts m a
forall (m :: * -> *) a.
(Subst -> TyVar -> m (a, Subst, TyVar)) -> PriorSubsts m a
PS (\Subst
s TyVar
m -> (a, Subst, TyVar) -> m (a, Subst, TyVar)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
x, Subst
s, TyVar
m))
    <*> :: PriorSubsts m (a -> b) -> PriorSubsts m a -> PriorSubsts m b
(<*>)  = PriorSubsts m (a -> b) -> PriorSubsts m a -> PriorSubsts m b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
instance (Functor m, Monad m) => Monad (PriorSubsts m) where
    {-# SPECIALIZE instance Monad (PriorSubsts []) #-}
    return :: a -> PriorSubsts m a
return     = a -> PriorSubsts m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    PS Subst -> TyVar -> m (a, Subst, TyVar)
x >>= :: PriorSubsts m a -> (a -> PriorSubsts m b) -> PriorSubsts m b
>>= a -> PriorSubsts m b
f = (Subst -> TyVar -> m (b, Subst, TyVar)) -> PriorSubsts m b
forall (m :: * -> *) a.
(Subst -> TyVar -> m (a, Subst, TyVar)) -> PriorSubsts m a
PS (\Subst
s TyVar
i -> do (a
a,Subst
t,TyVar
j) <- Subst -> TyVar -> m (a, Subst, TyVar)
x Subst
s TyVar
i
                                PriorSubsts m b -> Subst -> TyVar -> m (b, Subst, TyVar)
forall (m :: * -> *) a.
PriorSubsts m a -> Subst -> TyVar -> m (a, Subst, TyVar)
unPS (a -> PriorSubsts m b
f a
a) Subst
t TyVar
j)
--    {-# INLINE (>>=) #-} 意味なかった．
--    PS x >>= f = x `thenPS` f これも意味なかった．まあ，Monadはデフォルトでinlineしてるかも？

-- {-# INLINE listThenPS #-}
-- {-# INLINE thenPS #-}
-- x `thenPS` f = PS (\s i -> do (a,t,j) <- x s i
--                               unPS (f a) t j)
-- x `listThenPS` f = PS (\s i -> [ (b, u, k) | (a, t, j) <- x s i, (b, u, k) <- unPS (f a) t j ])
-- {-# RULES "listThenPS" thenPS = listThenPS #-}

-- distPS is also used to implement ifDepthPS
distPS :: (m (a, Subst, TyVar) -> m (a, Subst, TyVar) -> m (a, Subst, TyVar))
-> PriorSubsts m a -> PriorSubsts m a -> PriorSubsts m a
distPS m (a, Subst, TyVar) -> m (a, Subst, TyVar) -> m (a, Subst, TyVar)
op (PS Subst -> TyVar -> m (a, Subst, TyVar)
f) (PS Subst -> TyVar -> m (a, Subst, TyVar)
g) = (Subst -> TyVar -> m (a, Subst, TyVar)) -> PriorSubsts m a
forall (m :: * -> *) a.
(Subst -> TyVar -> m (a, Subst, TyVar)) -> PriorSubsts m a
PS (\Subst
s TyVar
i -> Subst -> TyVar -> m (a, Subst, TyVar)
f Subst
s TyVar
i m (a, Subst, TyVar) -> m (a, Subst, TyVar) -> m (a, Subst, TyVar)
`op` Subst -> TyVar -> m (a, Subst, TyVar)
g Subst
s TyVar
i)

instance (Functor m, MonadPlus m) => Alternative (PriorSubsts m) where
    {-# SPECIALIZE instance Alternative (PriorSubsts []) #-}
    empty :: PriorSubsts m a
empty = PriorSubsts m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
    <|> :: PriorSubsts m a -> PriorSubsts m a -> PriorSubsts m a
(<|>) = PriorSubsts m a -> PriorSubsts m a -> PriorSubsts m a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus
instance (Functor m, MonadPlus m) => MonadPlus (PriorSubsts m) where
    {-# SPECIALIZE instance MonadPlus (PriorSubsts []) #-}
    mzero :: PriorSubsts m a
mzero = (Subst -> TyVar -> m (a, Subst, TyVar)) -> PriorSubsts m a
forall (m :: * -> *) a.
(Subst -> TyVar -> m (a, Subst, TyVar)) -> PriorSubsts m a
PS (\Subst
_ TyVar
_->m (a, Subst, TyVar)
forall (m :: * -> *) a. MonadPlus m => m a
mzero)
    mplus :: PriorSubsts m a -> PriorSubsts m a -> PriorSubsts m a
mplus = (m (a, Subst, TyVar) -> m (a, Subst, TyVar) -> m (a, Subst, TyVar))
-> PriorSubsts m a -> PriorSubsts m a -> PriorSubsts m a
forall (m :: * -> *) a (m :: * -> *) a (m :: * -> *) a.
(m (a, Subst, TyVar) -> m (a, Subst, TyVar) -> m (a, Subst, TyVar))
-> PriorSubsts m a -> PriorSubsts m a -> PriorSubsts m a
distPS m (a, Subst, TyVar) -> m (a, Subst, TyVar) -> m (a, Subst, TyVar)
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus
instance Delay m => Delay (PriorSubsts m) where
  delay :: PriorSubsts m a -> PriorSubsts m a
delay (PS Subst -> TyVar -> m (a, Subst, TyVar)
f) = (Subst -> TyVar -> m (a, Subst, TyVar)) -> PriorSubsts m a
forall (m :: * -> *) a.
(Subst -> TyVar -> m (a, Subst, TyVar)) -> PriorSubsts m a
PS ((Subst -> TyVar -> m (a, Subst, TyVar)) -> PriorSubsts m a)
-> (Subst -> TyVar -> m (a, Subst, TyVar)) -> PriorSubsts m a
forall a b. (a -> b) -> a -> b
$ \Subst
s TyVar
i -> m (a, Subst, TyVar) -> m (a, Subst, TyVar)
forall (m :: * -> *) a. Delay m => m a -> m a
delay (m (a, Subst, TyVar) -> m (a, Subst, TyVar))
-> m (a, Subst, TyVar) -> m (a, Subst, TyVar)
forall a b. (a -> b) -> a -> b
$ Subst -> TyVar -> m (a, Subst, TyVar)
f Subst
s TyVar
i

#ifdef SEMIGROUP
instance Semigroup a => Semigroup (PriorSubsts [] a) where
    <> :: PriorSubsts [] a -> PriorSubsts [] a -> PriorSubsts [] a
(<>) = ([(a, Subst, TyVar)] -> [(a, Subst, TyVar)] -> [(a, Subst, TyVar)])
-> PriorSubsts [] a -> PriorSubsts [] a -> PriorSubsts [] a
forall (m :: * -> *) a (m :: * -> *) a (m :: * -> *) a.
(m (a, Subst, TyVar) -> m (a, Subst, TyVar) -> m (a, Subst, TyVar))
-> PriorSubsts m a -> PriorSubsts m a -> PriorSubsts m a
distPS (([(a, Subst, TyVar)]
  -> [(a, Subst, TyVar)] -> [(a, Subst, TyVar)])
 -> PriorSubsts [] a -> PriorSubsts [] a -> PriorSubsts [] a)
-> ([(a, Subst, TyVar)]
    -> [(a, Subst, TyVar)] -> [(a, Subst, TyVar)])
-> PriorSubsts [] a
-> PriorSubsts [] a
-> PriorSubsts [] a
forall a b. (a -> b) -> a -> b
$ ((a, Subst, TyVar) -> (a, Subst, TyVar) -> (a, Subst, TyVar))
-> ((a, Subst, TyVar) -> (a, Subst, TyVar) -> Ordering)
-> [(a, Subst, TyVar)]
-> [(a, Subst, TyVar)]
-> [(a, Subst, TyVar)]
forall k.
(k -> k -> k) -> (k -> k -> Ordering) -> [k] -> [k] -> [k]
mergeWithBy (\(a
xs,Subst
k,TyVar
i) (a
ys,Subst
_,TyVar
_) -> (a
xs a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
ys, Subst
k, TyVar
i)) (\ (a
_,Subst
k,TyVar
_) (a
_,Subst
l,TyVar
_) -> Subst
k Subst -> Subst -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Subst
l)
instance Semigroup a => Semigroup (PriorSubsts Recomp a) where
    PS Subst -> TyVar -> Recomp (a, Subst, TyVar)
f <> :: PriorSubsts Recomp a
-> PriorSubsts Recomp a -> PriorSubsts Recomp a
<> PS Subst -> TyVar -> Recomp (a, Subst, TyVar)
g = (Subst -> TyVar -> Recomp (a, Subst, TyVar))
-> PriorSubsts Recomp a
forall (m :: * -> *) a.
(Subst -> TyVar -> m (a, Subst, TyVar)) -> PriorSubsts m a
PS ((Subst -> TyVar -> Recomp (a, Subst, TyVar))
 -> PriorSubsts Recomp a)
-> (Subst -> TyVar -> Recomp (a, Subst, TyVar))
-> PriorSubsts Recomp a
forall a b. (a -> b) -> a -> b
$ \Subst
s TyVar
i -> (Int -> Bag (a, Subst, TyVar)) -> Recomp (a, Subst, TyVar)
forall a. (Int -> Bag a) -> Recomp a
Rc ((Int -> Bag (a, Subst, TyVar)) -> Recomp (a, Subst, TyVar))
-> (Int -> Bag (a, Subst, TyVar)) -> Recomp (a, Subst, TyVar)
forall a b. (a -> b) -> a -> b
$ \Int
dep -> ((a, Subst, TyVar) -> (a, Subst, TyVar) -> (a, Subst, TyVar))
-> ((a, Subst, TyVar) -> (a, Subst, TyVar) -> Ordering)
-> Bag (a, Subst, TyVar)
-> Bag (a, Subst, TyVar)
-> Bag (a, Subst, TyVar)
forall k.
(k -> k -> k) -> (k -> k -> Ordering) -> [k] -> [k] -> [k]
mergeWithBy (\(a
xs,Subst
k,TyVar
i) (a
ys,Subst
_,TyVar
_) -> (a
xs a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
ys, Subst
k, TyVar
i)) (\ (a
_,Subst
k,TyVar
_) (a
_,Subst
l,TyVar
_) -> Subst
k Subst -> Subst -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Subst
l) (Recomp (a, Subst, TyVar) -> Int -> Bag (a, Subst, TyVar)
forall a. Recomp a -> Int -> Bag a
unRc (Subst -> TyVar -> Recomp (a, Subst, TyVar)
f Subst
s TyVar
i) Int
dep) (Recomp (a, Subst, TyVar) -> Int -> Bag (a, Subst, TyVar)
forall a. Recomp a -> Int -> Bag a
unRc (Subst -> TyVar -> Recomp (a, Subst, TyVar)
g Subst
s TyVar
i) Int
dep)

instance Semigroup a => Monoid (PriorSubsts [] a) where
    mempty :: PriorSubsts [] a
mempty = (Subst -> TyVar -> [(a, Subst, TyVar)]) -> PriorSubsts [] a
forall (m :: * -> *) a.
(Subst -> TyVar -> m (a, Subst, TyVar)) -> PriorSubsts m a
PS (\Subst
_ TyVar
_ -> [])
    mappend :: PriorSubsts [] a -> PriorSubsts [] a -> PriorSubsts [] a
mappend = PriorSubsts [] a -> PriorSubsts [] a -> PriorSubsts [] a
forall a. Semigroup a => a -> a -> a
(<>)
instance Semigroup a => Monoid (PriorSubsts Recomp a) where
    mempty :: PriorSubsts Recomp a
mempty = (Subst -> TyVar -> Recomp (a, Subst, TyVar))
-> PriorSubsts Recomp a
forall (m :: * -> *) a.
(Subst -> TyVar -> m (a, Subst, TyVar)) -> PriorSubsts m a
PS (\Subst
_ TyVar
_ -> Recomp (a, Subst, TyVar)
forall (m :: * -> *) a. MonadPlus m => m a
mzero)
    mappend :: PriorSubsts Recomp a
-> PriorSubsts Recomp a -> PriorSubsts Recomp a
mappend = PriorSubsts Recomp a
-> PriorSubsts Recomp a -> PriorSubsts Recomp a
forall a. Semigroup a => a -> a -> a
(<>)
#else
instance Monoid a => Monoid (PriorSubsts [] a) where
    mempty = PS (\_ _ -> [])
    mappend = distPS $ mergeWithBy (\(xs,k,i) (ys,_,_) -> (xs `mappend` ys, k, i)) (\ (_,k,_) (_,l,_) -> k `compare` l)
instance Monoid a => Monoid (PriorSubsts Recomp a) where
    mempty = PS (\_ _ -> mzero)
    PS f `mappend` PS g = PS $ \s i -> Rc $ \dep -> mergeWithBy (\(xs,k,i) (ys,_,_) -> (xs `mappend` ys, k, i)) (\ (_,k,_) (_,l,_) -> k `compare` l) (unRc (f s i) dep) (unRc (g s i) dep)
#endif

instance Functor m => Functor (PriorSubsts m) where
    fmap :: (a -> b) -> PriorSubsts m a -> PriorSubsts m b
fmap a -> b
f (PS Subst -> TyVar -> m (a, Subst, TyVar)
g) = (Subst -> TyVar -> m (b, Subst, TyVar)) -> PriorSubsts m b
forall (m :: * -> *) a.
(Subst -> TyVar -> m (a, Subst, TyVar)) -> PriorSubsts m a
PS (\Subst
s TyVar
i -> ((a, Subst, TyVar) -> (b, Subst, TyVar))
-> m (a, Subst, TyVar) -> m (b, Subst, TyVar)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ (a
x, Subst
s', TyVar
i') -> (a -> b
f a
x, Subst
s', TyVar
i')) (Subst -> TyVar -> m (a, Subst, TyVar)
g Subst
s TyVar
i))

{-# RULES "fmap/fmap" [2] forall f g x. fmap f (fmap g x) = fmap (f . g) x #-}


{-# SPECIALIZE applyPS :: Type -> PriorSubsts [] Type #-}
applyPS :: Monad m => Type -> PriorSubsts m Type
applyPS :: Type -> PriorSubsts m Type
applyPS  Type
ty    = (Subst -> TyVar -> m (Type, Subst, TyVar)) -> PriorSubsts m Type
forall (m :: * -> *) a.
(Subst -> TyVar -> m (a, Subst, TyVar)) -> PriorSubsts m a
PS (\Subst
s TyVar
i -> (Type, Subst, TyVar) -> m (Type, Subst, TyVar)
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst -> Type -> Type
apply Subst
s Type
ty, Subst
s, TyVar
i))
{-# SPECIALIZE updatePS :: Subst -> PriorSubsts [] () #-}
updatePS :: Monad m => Subst -> PriorSubsts m ()
updatePS :: Subst -> PriorSubsts m ()
updatePS Subst
subst = (Subst -> TyVar -> m ((), Subst, TyVar)) -> PriorSubsts m ()
forall (m :: * -> *) a.
(Subst -> TyVar -> m (a, Subst, TyVar)) -> PriorSubsts m a
PS (\Subst
s TyVar
i -> ((), Subst, TyVar) -> m ((), Subst, TyVar)
forall (m :: * -> *) a. Monad m => a -> m a
return ((), Subst
subst Subst -> Subst -> Subst
`plusSubst` Subst
s, TyVar
i))
{-# SPECIALIZE updateSubstPS :: (Subst -> [] Subst) -> PriorSubsts [] () #-}
updateSubstPS :: Monad m => (Subst -> m Subst) -> PriorSubsts m ()
updateSubstPS :: (Subst -> m Subst) -> PriorSubsts m ()
updateSubstPS Subst -> m Subst
f = (Subst -> TyVar -> m ((), Subst, TyVar)) -> PriorSubsts m ()
forall (m :: * -> *) a.
(Subst -> TyVar -> m (a, Subst, TyVar)) -> PriorSubsts m a
PS (\Subst
s TyVar
i -> Subst -> m Subst
f Subst
s m Subst -> (Subst -> m ((), Subst, TyVar)) -> m ((), Subst, TyVar)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Subst
s' -> ((), Subst, TyVar) -> m ((), Subst, TyVar)
forall (m :: * -> *) a. Monad m => a -> m a
return ((), Subst
s', TyVar
i))

{-# SPECIALIZE setSubst :: Subst -> PriorSubsts [] () #-}
setSubst :: Monad m => Subst -> PriorSubsts m ()
setSubst :: Subst -> PriorSubsts m ()
setSubst Subst
subst = (Subst -> m Subst) -> PriorSubsts m ()
forall (m :: * -> *).
Monad m =>
(Subst -> m Subst) -> PriorSubsts m ()
updateSubstPS (\Subst
_ -> Subst -> m Subst
forall (m :: * -> *) a. Monad m => a -> m a
return Subst
subst)

{-# SPECIALIZE mguPS :: Type -> Type -> PriorSubsts [] () #-}
mguPS, matchPS :: (Functor m, MonadPlus m) => Type -> Type -> PriorSubsts m ()
mguPS :: Type -> Type -> PriorSubsts m ()
mguPS Type
t0 Type
t1 = do Subst
subst <- Type -> Type -> PriorSubsts m Subst
forall (m :: * -> *). MonadPlus m => Type -> Type -> m Subst
mgu Type
t0 Type
t1
                 Subst -> PriorSubsts m ()
forall (m :: * -> *). Monad m => Subst -> PriorSubsts m ()
updatePS Subst
subst
-- てゆーかmgtPSをmguPSの定義にしてもいいくらい．
mgtPS :: (Functor m, MonadPlus m) => Type -> Type -> PriorSubsts m Type
mgtPS :: Type -> Type -> PriorSubsts m Type
mgtPS Type
t1 Type
t2 = do Type -> Type -> PriorSubsts m ()
forall (m :: * -> *).
(Functor m, MonadPlus m) =>
Type -> Type -> PriorSubsts m ()
mguPS Type
t1 Type
t2
                 Type -> PriorSubsts m Type
forall (m :: * -> *). Monad m => Type -> PriorSubsts m Type
applyPS Type
t1
{-# SPECIALIZE varBindPS :: TyVar -> Type -> PriorSubsts [] () #-}
varBindPS :: (Functor m, MonadPlus m) => TyVar -> Type -> PriorSubsts m ()
varBindPS :: TyVar -> Type -> PriorSubsts m ()
varBindPS TyVar
v Type
t = do Subst
subst <- TyVar -> Type -> PriorSubsts m Subst
forall (m :: * -> *). MonadPlus m => TyVar -> Type -> m Subst
varBind TyVar
v Type
t
                   Subst -> PriorSubsts m ()
forall (m :: * -> *). Monad m => Subst -> PriorSubsts m ()
updatePS Subst
subst
matchPS :: Type -> Type -> PriorSubsts m ()
matchPS Type
t0 Type
t1 = do Subst
subst <- Type -> Type -> PriorSubsts m Subst
forall (m :: * -> *). MonadPlus m => Type -> Type -> m Subst
match Type
t0 Type
t1
                   Subst -> PriorSubsts m ()
forall (m :: * -> *). Monad m => Subst -> PriorSubsts m ()
updatePS Subst
subst
{-
symPlusPS :: MonadPlus m => Subst -> PriorSubsts m ()
symPlusPS subst = do s0 <- getSubst
                     s1 <- symPlus subst s0
                     setSubst s1
-}

lookupSubstPS :: (Functor m, MonadPlus m) => TyVar -> PriorSubsts m Type
lookupSubstPS :: TyVar -> PriorSubsts m Type
lookupSubstPS TyVar
tvid = do Subst
subst <- PriorSubsts m Subst
forall (m :: * -> *). Monad m => PriorSubsts m Subst
getSubst
                        case Subst -> TyVar -> Maybe Type
forall (m :: * -> *). MonadPlus m => Subst -> TyVar -> m Type
lookupSubst Subst
subst TyVar
tvid of Maybe Type
Nothing -> PriorSubsts m Type
forall (m :: * -> *) a. MonadPlus m => m a
mzero
                                                       Just Type
ty -> Type -> PriorSubsts m Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty

-- what follow are mainly used by module Infer, but can be reused if necessary.
{-# SPECIALIZE getSubst :: PriorSubsts [] Subst #-}
getSubst :: Monad m => PriorSubsts m Subst
getSubst :: PriorSubsts m Subst
getSubst = (Subst -> TyVar -> m (Subst, Subst, TyVar)) -> PriorSubsts m Subst
forall (m :: * -> *) a.
(Subst -> TyVar -> m (a, Subst, TyVar)) -> PriorSubsts m a
PS (\Subst
s TyVar
i -> (Subst, Subst, TyVar) -> m (Subst, Subst, TyVar)
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
s,Subst
s,TyVar
i))
{-# SPECIALIZE getMx :: PriorSubsts [] TyVar #-}
getMx    :: Monad m => PriorSubsts m TyVar
getMx :: PriorSubsts m TyVar
getMx    = (Subst -> TyVar -> m (TyVar, Subst, TyVar)) -> PriorSubsts m TyVar
forall (m :: * -> *) a.
(Subst -> TyVar -> m (a, Subst, TyVar)) -> PriorSubsts m a
PS (\Subst
s TyVar
i -> (TyVar, Subst, TyVar) -> m (TyVar, Subst, TyVar)
forall (m :: * -> *) a. Monad m => a -> m a
return (TyVar
i,Subst
s,TyVar
i))
{-# SPECIALIZE updateMx :: (TyVar->TyVar) -> PriorSubsts [] () #-}
updateMx :: Monad m => (TyVar->TyVar) -> PriorSubsts m ()
updateMx :: (TyVar -> TyVar) -> PriorSubsts m ()
updateMx TyVar -> TyVar
f = (Subst -> TyVar -> m ((), Subst, TyVar)) -> PriorSubsts m ()
forall (m :: * -> *) a.
(Subst -> TyVar -> m (a, Subst, TyVar)) -> PriorSubsts m a
PS (\Subst
s TyVar
i -> ((), Subst, TyVar) -> m ((), Subst, TyVar)
forall (m :: * -> *) a. Monad m => a -> m a
return ((), Subst
s, TyVar -> TyVar
f TyVar
i))
{-# SPECIALIZE unify :: Type -> Type -> PriorSubsts [] () #-}
unify :: (Functor m, MonadPlus m) => Type -> Type -> PriorSubsts m ()
unify :: Type -> Type -> PriorSubsts m ()
unify Type
t1 Type
t2 = do Subst
s <- PriorSubsts m Subst
forall (m :: * -> *). Monad m => PriorSubsts m Subst
getSubst
                 Subst
u <- Type -> Type -> PriorSubsts m Subst
forall (m :: * -> *). MonadPlus m => Type -> Type -> m Subst
mgu (Subst -> Type -> Type
apply Subst
s Type
t1) (Subst -> Type -> Type
apply Subst
s Type
t2)
                 Subst -> PriorSubsts m ()
forall (m :: * -> *). Monad m => Subst -> PriorSubsts m ()
updatePS Subst
u

newTVar :: Monad m => PriorSubsts m TyVar
newTVar :: PriorSubsts m TyVar
newTVar = (Subst -> TyVar -> m (TyVar, Subst, TyVar)) -> PriorSubsts m TyVar
forall (m :: * -> *) a.
(Subst -> TyVar -> m (a, Subst, TyVar)) -> PriorSubsts m a
PS (\ Subst
s TyVar
n -> (TyVar, Subst, TyVar) -> m (TyVar, Subst, TyVar)
forall (m :: * -> *) a. Monad m => a -> m a
return (TyVar
n, Subst
s, TyVar
nTyVar -> TyVar -> TyVar
forall a. Num a => a -> a -> a
+TyVar
1))

-- I do not remember why this was removed. It has come back with the coming back of Infer.lhs as TICE.hs.
freshInst :: (Functor m, Monad m) => Type -> PriorSubsts m Type
freshInst :: Type -> PriorSubsts m Type
freshInst Type
ty = do TyVar
tv <- TyVar -> PriorSubsts m TyVar
forall (m :: * -> *). Monad m => TyVar -> PriorSubsts m TyVar
reserveTVars (TyVar -> PriorSubsts m TyVar) -> TyVar -> PriorSubsts m TyVar
forall a b. (a -> b) -> a -> b
$ Type -> TyVar
maxVarID Type
ty TyVar -> TyVar -> TyVar
forall a. Num a => a -> a -> a
+ TyVar
1
                  Type -> PriorSubsts m Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> PriorSubsts m Type) -> Type -> PriorSubsts m Type
forall a b. (a -> b) -> a -> b
$ (TyVar -> TyVar) -> Type -> Type
mapTV (TyVar
tvTyVar -> TyVar -> TyVar
forall a. Num a => a -> a -> a
+) Type
ty
{-
freshInst ty = do let tvs = tyvars ty
		  ntvs <- mapM (const newTVar) tvs
		  let ar = array (0,maxVarID ty) (zip (map tvID tvs) ntvs) 
		  return (inst ar ty)
    where inst :: Array Int TyVar -> Type -> Type
	  -- inst ar = mapTV (\tv -> ar ! tvID tv) -- mapTVはType.lhsからexportしない方が良さそうなので．てゆーか単に，Type.unifyFunAp(QTy)でmapTV相当のものを実装すれば良いのか？
	  inst ar (TA l r) = TA (inst ar l) (inst ar r)
	  inst ar (l:->r)  = inst ar l :-> inst ar r
	  inst ar (TV tv)  = TV (ar ! tvID tv)
	  inst _  t@(TC _) = t
-}



-- 同じ名前の関数がallifdefs/PSList.hsにもあったりする．役割も似たようなもん．
psListToPSRecomp :: (Int -> PriorSubsts [] a) -> PriorSubsts Recomp a
psListToPSRecomp :: (Int -> PriorSubsts [] a) -> PriorSubsts Recomp a
psListToPSRecomp Int -> PriorSubsts [] a
f = (Subst -> TyVar -> Recomp (a, Subst, TyVar))
-> PriorSubsts Recomp a
forall (m :: * -> *) a.
(Subst -> TyVar -> m (a, Subst, TyVar)) -> PriorSubsts m a
PS (\Subst
subst TyVar
int -> (Int -> Bag (a, Subst, TyVar)) -> Recomp (a, Subst, TyVar)
forall a. (Int -> Bag a) -> Recomp a
Rc (\Int
dep -> case Int -> PriorSubsts [] a
f Int
dep of PS Subst -> TyVar -> Bag (a, Subst, TyVar)
g -> Subst -> TyVar -> Bag (a, Subst, TyVar)
g Subst
subst TyVar
int))
psRecompToPSList :: PriorSubsts Recomp a -> Int -> PriorSubsts [] a
psRecompToPSList :: PriorSubsts Recomp a -> Int -> PriorSubsts [] a
psRecompToPSList (PS Subst -> TyVar -> Recomp (a, Subst, TyVar)
f) Int
dep = (Subst -> TyVar -> [(a, Subst, TyVar)]) -> PriorSubsts [] a
forall (m :: * -> *) a.
(Subst -> TyVar -> m (a, Subst, TyVar)) -> PriorSubsts m a
PS (\Subst
subst TyVar
int -> case Subst -> TyVar -> Recomp (a, Subst, TyVar)
f Subst
subst TyVar
int of Rc Int -> [(a, Subst, TyVar)]
g -> Int -> [(a, Subst, TyVar)]
g Int
dep)

psListToPSDBound :: (Int -> PriorSubsts [] (a,Int)) -> PriorSubsts DBound a
psListToPSDBound :: (Int -> PriorSubsts [] (a, Int)) -> PriorSubsts DBound a
psListToPSDBound Int -> PriorSubsts [] (a, Int)
f = (Subst -> TyVar -> DBound (a, Subst, TyVar))
-> PriorSubsts DBound a
forall (m :: * -> *) a.
(Subst -> TyVar -> m (a, Subst, TyVar)) -> PriorSubsts m a
PS (\Subst
subst TyVar
int -> (Int -> Bag ((a, Subst, TyVar), Int)) -> DBound (a, Subst, TyVar)
forall a. (Int -> Bag (a, Int)) -> DBound a
DB (\Int
dep -> case Int -> PriorSubsts [] (a, Int)
f Int
dep of PS Subst -> TyVar -> [((a, Int), Subst, TyVar)]
g -> (((a, Int), Subst, TyVar) -> ((a, Subst, TyVar), Int))
-> [((a, Int), Subst, TyVar)] -> Bag ((a, Subst, TyVar), Int)
forall a b. (a -> b) -> [a] -> [b]
map ((a, Int), Subst, TyVar) -> ((a, Subst, TyVar), Int)
forall a b b c. ((a, b), b, c) -> ((a, b, c), b)
tup23 ([((a, Int), Subst, TyVar)] -> Bag ((a, Subst, TyVar), Int))
-> [((a, Int), Subst, TyVar)] -> Bag ((a, Subst, TyVar), Int)
forall a b. (a -> b) -> a -> b
$ Subst -> TyVar -> [((a, Int), Subst, TyVar)]
g Subst
subst TyVar
int))
psDBoundToPSList :: PriorSubsts DBound a -> Int -> PriorSubsts [] (a,Int)
psDBoundToPSList :: PriorSubsts DBound a -> Int -> PriorSubsts [] (a, Int)
psDBoundToPSList (PS Subst -> TyVar -> DBound (a, Subst, TyVar)
f) Int
dep = (Subst -> TyVar -> [((a, Int), Subst, TyVar)])
-> PriorSubsts [] (a, Int)
forall (m :: * -> *) a.
(Subst -> TyVar -> m (a, Subst, TyVar)) -> PriorSubsts m a
PS (\Subst
subst TyVar
int -> case Subst -> TyVar -> DBound (a, Subst, TyVar)
f Subst
subst TyVar
int of DB Int -> Bag ((a, Subst, TyVar), Int)
g -> (((a, Subst, TyVar), Int) -> ((a, Int), Subst, TyVar))
-> Bag ((a, Subst, TyVar), Int) -> [((a, Int), Subst, TyVar)]
forall a b. (a -> b) -> [a] -> [b]
map ((a, Subst, TyVar), Int) -> ((a, Int), Subst, TyVar)
forall a b c b. ((a, b, c), b) -> ((a, b), b, c)
tup32 (Bag ((a, Subst, TyVar), Int) -> [((a, Int), Subst, TyVar)])
-> Bag ((a, Subst, TyVar), Int) -> [((a, Int), Subst, TyVar)]
forall a b. (a -> b) -> a -> b
$ Int -> Bag ((a, Subst, TyVar), Int)
g Int
dep)

tup23 :: ((a, b), b, c) -> ((a, b, c), b)
tup23 ((a
a,b
i),b
k,c
m) = ((a
a,b
k,c
m),b
i)
tup32 :: ((a, b, c), b) -> ((a, b), b, c)
tup32 ((a
a,b
k,c
m),b
i) = ((a
a,b
i),b
k,c
m)

nubSortBy :: (a -> a -> Ordering) -> [a] -> [a]
nubSortBy :: (a -> a -> Ordering) -> [a] -> [a]
nubSortBy a -> a -> Ordering
cmp = (a -> a -> Bool) -> [a] -> [a]
forall a. (a -> a -> Bool) -> [a] -> [a]
uniqBy (\a
a a
b->a -> a -> Ordering
cmp a
a a
bOrdering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
==Ordering
EQ) ([a] -> [a]) -> ([a] -> [a]) -> [a] -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> a -> Ordering) -> [a] -> [a]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy a -> a -> Ordering
cmp
uniqBy :: (a->a->Bool) -> [a] -> [a]
uniqBy :: (a -> a -> Bool) -> [a] -> [a]
uniqBy a -> a -> Bool
eq []     = []
uniqBy a -> a -> Bool
eq (a
x:[a]
xs) = case (a -> Bool) -> [a] -> ([a], [a])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (a -> a -> Bool
eq a
x) [a]
xs of ([a]
_,[a]
ns) -> a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: (a -> a -> Bool) -> [a] -> [a]
forall a. (a -> a -> Bool) -> [a] -> [a]
uniqBy a -> a -> Bool
eq [a]
ns


-- | reserveTVars takes the number of requested tvIDs, reserves consecutive tvIDs, and returns the first tvID. 
reserveTVars :: Monad m => TyVar -> PriorSubsts m TyVar
reserveTVars :: TyVar -> PriorSubsts m TyVar
reserveTVars TyVar
n = (Subst -> TyVar -> m (TyVar, Subst, TyVar)) -> PriorSubsts m TyVar
forall (m :: * -> *) a.
(Subst -> TyVar -> m (a, Subst, TyVar)) -> PriorSubsts m a
PS (\Subst
s TyVar
i -> (TyVar, Subst, TyVar) -> m (TyVar, Subst, TyVar)
forall (m :: * -> *) a. Monad m => a -> m a
return (TyVar
i,Subst
s,TyVar
iTyVar -> TyVar -> TyVar
forall a. Num a => a -> a -> a
+TyVar
n))
{- こっちの定義にしたら阿呆みたいに時間を食った．訳ワカメ
reserveTVars n = do i <- getMx
                    updateMx (n+)
                    return i
-}


{-
flatten :: PriorSubsts [a] -> PriorSubsts a
flatten (PS sbb) = PS (\s i -> map cat $ unMx (sbb s i))
cat :: Bag ([a], Subst, TyVar) -> Bag (a, Subst, TyVar)
cat xs = [ (y, s, i) | (ys, s, i) <- xs, y <- ys ]
-}
\end{code}