{-# LANGUAGE CPP #-}
module Djinn.HCheck (
htCheckEnv,
htCheckType
) where
import Data.List (union)
#if MIN_VERSION_mtl(2,2,0)
import Control.Monad.Except ()
#else
import Control.Monad.Error ()
#endif
import Control.Monad.State
import Data.Graph (SCC (..), stronglyConnComp)
import Data.IntMap (IntMap, empty, insert, (!))
import Djinn.HTypes
#if MIN_VERSION_mtl(2,3,0)
liftM2 :: Applicative f => (a -> b -> c) -> f a -> f b -> f c
liftM2 f x y = f <$> x <*> y
#endif
type KState = (Int, IntMap (Maybe HKind))
initState :: KState
initState :: KState
initState = (Int
0, forall a. IntMap a
empty)
type M a = StateT KState (Either String) a
type KEnv = [(HSymbol, HKind)]
newKVar :: M HKind
newKVar :: M HKind
newKVar = do
(Int
i, IntMap (Maybe HKind)
m) <- forall s (m :: * -> *). MonadState s m => m s
get
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
iforall a. Num a => a -> a -> a
+Int
1, forall a. Int -> a -> IntMap a -> IntMap a
insert Int
i forall a. Maybe a
Nothing IntMap (Maybe HKind)
m)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> HKind
KVar Int
i
getVar :: Int -> M (Maybe HKind)
getVar :: Int -> M (Maybe HKind)
getVar Int
i = do
(Int
_, IntMap (Maybe HKind)
m) <- forall s (m :: * -> *). MonadState s m => m s
get
case IntMap (Maybe HKind)
mforall a. IntMap a -> Int -> a
!Int
i of
Just (KVar Int
i') -> Int -> M (Maybe HKind)
getVar Int
i'
Maybe HKind
mk -> forall (m :: * -> *) a. Monad m => a -> m a
return Maybe HKind
mk
addMap :: Int -> HKind -> M ()
addMap :: Int -> HKind -> M ()
addMap Int
i HKind
k = do
(Int
n, IntMap (Maybe HKind)
m) <- forall s (m :: * -> *). MonadState s m => m s
get
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
n, forall a. Int -> a -> IntMap a -> IntMap a
insert Int
i (forall a. a -> Maybe a
Just HKind
k) IntMap (Maybe HKind)
m)
clearState :: M ()
clearState :: M ()
clearState = forall s (m :: * -> *). MonadState s m => s -> m ()
put KState
initState
htCheckType :: [(HSymbol, ([HSymbol], HType, HKind))] -> HType -> Either String ()
htCheckType :: [(HSymbol, ([HSymbol], HType, HKind))]
-> HType -> Either HSymbol ()
htCheckType [(HSymbol, ([HSymbol], HType, HKind))]
its HType
t = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT KState
initState forall a b. (a -> b) -> a -> b
$ do
let vs :: [HSymbol]
vs = HType -> [HSymbol]
getHTVars HType
t
[HKind]
ks <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b. a -> b -> a
const M HKind
newKVar) [HSymbol]
vs
let env :: [(HSymbol, HKind)]
env = forall a b. [a] -> [b] -> [(a, b)]
zip [HSymbol]
vs [HKind]
ks forall a. [a] -> [a] -> [a]
++ [(HSymbol
i, HKind
k) | (HSymbol
i, ([HSymbol]
_, HType
_, HKind
k)) <- [(HSymbol, ([HSymbol], HType, HKind))]
its ]
[(HSymbol, HKind)] -> HType -> M ()
iHKindStar [(HSymbol, HKind)]
env HType
t
htCheckEnv :: [(HSymbol, ([HSymbol], HType, a))] -> Either String [(HSymbol, ([HSymbol], HType, HKind))]
htCheckEnv :: forall a.
[(HSymbol, ([HSymbol], HType, a))]
-> Either HSymbol [(HSymbol, ([HSymbol], HType, HKind))]
htCheckEnv [(HSymbol, ([HSymbol], HType, a))]
its =
let graph :: [((HSymbol, ([HSymbol], HType, a)), HSymbol, [HSymbol])]
graph = [ ((HSymbol, ([HSymbol], HType, a))
n, HSymbol
i, HType -> [HSymbol]
getHTCons HType
t) | n :: (HSymbol, ([HSymbol], HType, a))
n@(HSymbol
i, ([HSymbol]
_, HType
t, a
_)) <- [(HSymbol, ([HSymbol], HType, a))]
its ]
order :: [SCC (HSymbol, ([HSymbol], HType, a))]
order = forall key node. Ord key => [(node, key, [key])] -> [SCC node]
stronglyConnComp [((HSymbol, ([HSymbol], HType, a)), HSymbol, [HSymbol])]
graph
in case [ [(HSymbol, ([HSymbol], HType, a))]
c | CyclicSCC [(HSymbol, ([HSymbol], HType, a))]
c <- [SCC (HSymbol, ([HSymbol], HType, a))]
order ] of
[(HSymbol, ([HSymbol], HType, a))]
c : [[(HSymbol, ([HSymbol], HType, a))]]
_ -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ HSymbol
"Recursive types are not allowed: " forall a. [a] -> [a] -> [a]
++ [HSymbol] -> HSymbol
unwords [ HSymbol
i | (HSymbol
i, ([HSymbol], HType, a)
_) <- [(HSymbol, ([HSymbol], HType, a))]
c ]
[] -> forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT KState
initState forall a b. (a -> b) -> a -> b
$ StateT
KState (Either HSymbol) [(HSymbol, ([HSymbol], HType, HKind))]
addKinds
where addKinds :: StateT
KState (Either HSymbol) [(HSymbol, ([HSymbol], HType, HKind))]
addKinds = do
[(HSymbol, HKind)]
env <- forall a.
[(HSymbol, HKind)]
-> [(HSymbol, ([HSymbol], HType, a))] -> M [(HSymbol, HKind)]
inferHKinds [] forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\ (AcyclicSCC (HSymbol, ([HSymbol], HType, a))
n) -> (HSymbol, ([HSymbol], HType, a))
n) [SCC (HSymbol, ([HSymbol], HType, a))]
order
let getK :: HSymbol -> HKind
getK HSymbol
i = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a. HasCallStack => HSymbol -> a
error forall a b. (a -> b) -> a -> b
$ HSymbol
"htCheck " forall a. [a] -> [a] -> [a]
++ HSymbol
i) forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup HSymbol
i [(HSymbol, HKind)]
env
forall (m :: * -> *) a. Monad m => a -> m a
return [ (HSymbol
i, ([HSymbol]
vs, HType
t, HSymbol -> HKind
getK HSymbol
i)) | (HSymbol
i, ([HSymbol]
vs, HType
t, a
_)) <- [(HSymbol, ([HSymbol], HType, a))]
its ]
inferHKinds :: KEnv -> [(HSymbol, ([HSymbol], HType, a))] -> M KEnv
inferHKinds :: forall a.
[(HSymbol, HKind)]
-> [(HSymbol, ([HSymbol], HType, a))] -> M [(HSymbol, HKind)]
inferHKinds [(HSymbol, HKind)]
env [] = forall (m :: * -> *) a. Monad m => a -> m a
return [(HSymbol, HKind)]
env
inferHKinds [(HSymbol, HKind)]
env ((HSymbol
i, ([HSymbol]
vs, HType
t, a
_)) : [(HSymbol, ([HSymbol], HType, a))]
its) = do
HKind
k <- [(HSymbol, HKind)] -> [HSymbol] -> HType -> M HKind
inferHKind [(HSymbol, HKind)]
env [HSymbol]
vs HType
t
forall a.
[(HSymbol, HKind)]
-> [(HSymbol, ([HSymbol], HType, a))] -> M [(HSymbol, HKind)]
inferHKinds ((HSymbol
i, HKind
k) forall a. a -> [a] -> [a]
: [(HSymbol, HKind)]
env) [(HSymbol, ([HSymbol], HType, a))]
its
inferHKind :: KEnv -> [HSymbol] -> HType -> M HKind
inferHKind :: [(HSymbol, HKind)] -> [HSymbol] -> HType -> M HKind
inferHKind [(HSymbol, HKind)]
_ [HSymbol]
_ (HTAbstract HSymbol
_ HKind
k) = forall (m :: * -> *) a. Monad m => a -> m a
return HKind
k
inferHKind [(HSymbol, HKind)]
env [HSymbol]
vs HType
t = do
M ()
clearState
[HKind]
ks <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b. a -> b -> a
const M HKind
newKVar) [HSymbol]
vs
let env' :: [(HSymbol, HKind)]
env' = forall a b. [a] -> [b] -> [(a, b)]
zip [HSymbol]
vs [HKind]
ks forall a. [a] -> [a] -> [a]
++ [(HSymbol, HKind)]
env
HKind
k <- [(HSymbol, HKind)] -> HType -> M HKind
iHKind [(HSymbol, HKind)]
env' HType
t
HKind -> M HKind
ground forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr HKind -> HKind -> HKind
KArrow HKind
k [HKind]
ks
iHKind :: KEnv -> HType -> M HKind
iHKind :: [(HSymbol, HKind)] -> HType -> M HKind
iHKind [(HSymbol, HKind)]
env (HTApp HType
f HType
a) = do
HKind
kf <- [(HSymbol, HKind)] -> HType -> M HKind
iHKind [(HSymbol, HKind)]
env HType
f
HKind
ka <- [(HSymbol, HKind)] -> HType -> M HKind
iHKind [(HSymbol, HKind)]
env HType
a
HKind
r <- M HKind
newKVar
HKind -> HKind -> M ()
unifyK (HKind -> HKind -> HKind
KArrow HKind
ka HKind
r) HKind
kf
forall (m :: * -> *) a. Monad m => a -> m a
return HKind
r
iHKind [(HSymbol, HKind)]
env (HTVar HSymbol
v) = do
[(HSymbol, HKind)] -> HSymbol -> M HKind
getVarHKind [(HSymbol, HKind)]
env HSymbol
v
iHKind [(HSymbol, HKind)]
env (HTCon HSymbol
c) = do
[(HSymbol, HKind)] -> HSymbol -> M HKind
getConHKind [(HSymbol, HKind)]
env HSymbol
c
iHKind [(HSymbol, HKind)]
env (HTTuple [HType]
ts) = do
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([(HSymbol, HKind)] -> HType -> M ()
iHKindStar [(HSymbol, HKind)]
env) [HType]
ts
forall (m :: * -> *) a. Monad m => a -> m a
return HKind
KStar
iHKind [(HSymbol, HKind)]
env (HTArrow HType
f HType
a) = do
[(HSymbol, HKind)] -> HType -> M ()
iHKindStar [(HSymbol, HKind)]
env HType
f
[(HSymbol, HKind)] -> HType -> M ()
iHKindStar [(HSymbol, HKind)]
env HType
a
forall (m :: * -> *) a. Monad m => a -> m a
return HKind
KStar
iHKind [(HSymbol, HKind)]
env (HTUnion [(HSymbol, [HType])]
cs) = do
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (HSymbol
_, [HType]
ts) -> forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([(HSymbol, HKind)] -> HType -> M ()
iHKindStar [(HSymbol, HKind)]
env) [HType]
ts) [(HSymbol, [HType])]
cs
forall (m :: * -> *) a. Monad m => a -> m a
return HKind
KStar
iHKind [(HSymbol, HKind)]
_ (HTAbstract HSymbol
_ HKind
_) = forall a. HasCallStack => HSymbol -> a
error HSymbol
"iHKind HTAbstract"
iHKindStar :: KEnv -> HType -> M ()
iHKindStar :: [(HSymbol, HKind)] -> HType -> M ()
iHKindStar [(HSymbol, HKind)]
env HType
t = do
HKind
k <- [(HSymbol, HKind)] -> HType -> M HKind
iHKind [(HSymbol, HKind)]
env HType
t
HKind -> HKind -> M ()
unifyK HKind
k HKind
KStar
unifyK :: HKind -> HKind -> M ()
unifyK :: HKind -> HKind -> M ()
unifyK HKind
k1 HKind
k2 = do
let follow :: HKind -> M HKind
follow k :: HKind
k@(KVar Int
i) = Int -> M (Maybe HKind)
getVar Int
i forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. b -> (a -> b) -> Maybe a -> b
maybe HKind
k forall a. a -> a
id
follow HKind
k = forall (m :: * -> *) a. Monad m => a -> m a
return HKind
k
unify :: HKind -> HKind -> M ()
unify HKind
KStar HKind
KStar = forall (m :: * -> *) a. Monad m => a -> m a
return ()
unify (KArrow HKind
k11 HKind
k12) (KArrow HKind
k21 HKind
k22) = do HKind -> HKind -> M ()
unifyK HKind
k11 HKind
k21; HKind -> HKind -> M ()
unifyK HKind
k12 HKind
k22
unify (KVar Int
i1) (KVar Int
i2) | Int
i1 forall a. Eq a => a -> a -> Bool
== Int
i2 = forall (m :: * -> *) a. Monad m => a -> m a
return ()
unify (KVar Int
i) HKind
k = do Int -> HKind -> M ()
occurs Int
i HKind
k; Int -> HKind -> M ()
addMap Int
i HKind
k
unify HKind
k (KVar Int
i) = do Int -> HKind -> M ()
occurs Int
i HKind
k; Int -> HKind -> M ()
addMap Int
i HKind
k
unify HKind
_ HKind
_ = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ HSymbol
"kind error: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> HSymbol
show (HKind
k1, HKind
k2)
occurs :: Int -> HKind -> M ()
occurs Int
_ HKind
KStar = forall (m :: * -> *) a. Monad m => a -> m a
return ()
occurs Int
i (KArrow HKind
f HKind
a) = do HKind -> M HKind
follow HKind
f forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Int -> HKind -> M ()
occurs Int
i; HKind -> M HKind
follow HKind
a forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Int -> HKind -> M ()
occurs Int
i
occurs Int
i (KVar Int
i') = if Int
i forall a. Eq a => a -> a -> Bool
== Int
i' then forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left HSymbol
"cyclic kind" else forall (m :: * -> *) a. Monad m => a -> m a
return ()
HKind
k1' <- HKind -> M HKind
follow HKind
k1
HKind
k2' <- HKind -> M HKind
follow HKind
k2
HKind -> HKind -> M ()
unify HKind
k1' HKind
k2'
getVarHKind :: KEnv -> HSymbol -> M HKind
getVarHKind :: [(HSymbol, HKind)] -> HSymbol -> M HKind
getVarHKind [(HSymbol, HKind)]
env HSymbol
v = case forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup HSymbol
v [(HSymbol, HKind)]
env of
Just HKind
k -> forall (m :: * -> *) a. Monad m => a -> m a
return HKind
k
Maybe HKind
Nothing -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ HSymbol
"Undefined type variable " forall a. [a] -> [a] -> [a]
++ HSymbol
v
getConHKind :: KEnv -> HSymbol -> M HKind
getConHKind :: [(HSymbol, HKind)] -> HSymbol -> M HKind
getConHKind [(HSymbol, HKind)]
env HSymbol
v = case forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup HSymbol
v [(HSymbol, HKind)]
env of
Just HKind
k -> forall (m :: * -> *) a. Monad m => a -> m a
return HKind
k
Maybe HKind
Nothing -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ HSymbol
"Undefined type " forall a. [a] -> [a] -> [a]
++ HSymbol
v
ground :: HKind -> M HKind
ground :: HKind -> M HKind
ground HKind
KStar = forall (m :: * -> *) a. Monad m => a -> m a
return HKind
KStar
ground (KArrow HKind
k1 HKind
k2) = forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 HKind -> HKind -> HKind
KArrow (HKind -> M HKind
ground HKind
k1) (HKind -> M HKind
ground HKind
k2)
ground (KVar Int
i) = do
Maybe HKind
mk <- Int -> M (Maybe HKind)
getVar Int
i
case Maybe HKind
mk of
Just HKind
k -> forall (m :: * -> *) a. Monad m => a -> m a
return HKind
k
Maybe HKind
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return HKind
KStar
getHTCons :: HType -> [HSymbol]
getHTCons :: HType -> [HSymbol]
getHTCons (HTApp HType
f HType
a) = HType -> [HSymbol]
getHTCons HType
f forall a. Eq a => [a] -> [a] -> [a]
`union` HType -> [HSymbol]
getHTCons HType
a
getHTCons (HTVar HSymbol
_) = []
getHTCons (HTCon HSymbol
s) = [HSymbol
s]
getHTCons (HTTuple [HType]
ts) = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a. Eq a => [a] -> [a] -> [a]
union [] (forall a b. (a -> b) -> [a] -> [b]
map HType -> [HSymbol]
getHTCons [HType]
ts)
getHTCons (HTArrow HType
f HType
a) = HType -> [HSymbol]
getHTCons HType
f forall a. Eq a => [a] -> [a] -> [a]
`union` HType -> [HSymbol]
getHTCons HType
a
getHTCons (HTUnion [(HSymbol, [HType])]
alts) = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a. Eq a => [a] -> [a] -> [a]
union [] [ HType -> [HSymbol]
getHTCons HType
t | (HSymbol
_, [HType]
ts) <- [(HSymbol, [HType])]
alts, HType
t <- [HType]
ts ]
getHTCons (HTAbstract HSymbol
_ HKind
_) = []