{-# LANGUAGE GeneralizedNewtypeDeriving, FlexibleInstances, PatternGuards, RankNTypes, FlexibleContexts #-}
module Language.Javascript.JMacro.TypeCheck where
import Language.Javascript.JMacro.Base
import Language.Javascript.JMacro.Types
import Control.Applicative
import Control.Monad
import Control.Monad.Identity
import Control.Monad.State
import Control.Monad.Reader
import Control.Monad.Writer
import Control.Monad.Error
import Data.Either
import Data.Map (Map)
import Data.Maybe(catMaybes)
import Data.List(intercalate, nub, transpose)
import qualified Data.Traversable as T
import qualified Data.Foldable as F
import qualified Data.Map as M
import qualified Data.Text.Lazy as T
import Data.Set(Set)
import qualified Data.Set as S
import Text.PrettyPrint.Leijen.Text hiding ((<$>))
eitherIsLeft :: Either a b -> Bool
eitherIsLeft :: Either a b -> Bool
eitherIsLeft (Left _) = Bool
True
eitherIsLeft _ = Bool
False
partitionOut :: (a -> Maybe b) -> [a] -> ([b],[a])
partitionOut :: (a -> Maybe b) -> [a] -> ([b], [a])
partitionOut f :: a -> Maybe b
f xs' :: [a]
xs' = (a -> ([b], [a]) -> ([b], [a])) -> ([b], [a]) -> [a] -> ([b], [a])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> ([b], [a]) -> ([b], [a])
go ([],[]) [a]
xs'
where go :: a -> ([b], [a]) -> ([b], [a])
go x :: a
x ~(bs :: [b]
bs,as :: [a]
as)
| Just b :: b
b <- a -> Maybe b
f a
x = (b
bb -> [b] -> [b]
forall a. a -> [a] -> [a]
:[b]
bs,[a]
as)
| Bool
otherwise = ([b]
bs,a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
as)
zipWithOrChange :: (a -> a -> b) -> (a -> b) -> [a] -> [a] -> [b]
zipWithOrChange :: (a -> a -> b) -> (a -> b) -> [a] -> [a] -> [b]
zipWithOrChange f :: a -> a -> b
f g :: a -> b
g xss :: [a]
xss yss :: [a]
yss = [a] -> [a] -> [b]
go [a]
xss [a]
yss
where go :: [a] -> [a] -> [b]
go (x :: a
x:xs :: [a]
xs) (y :: a
y:ys :: [a]
ys) = a -> a -> b
f a
x a
y b -> [b] -> [b]
forall a. a -> [a] -> [a]
: [a] -> [a] -> [b]
go [a]
xs [a]
ys
go xs :: [a]
xs@(_:_) _ = (a -> b) -> [a] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map a -> b
g [a]
xs
go _ ys :: [a]
ys = (a -> b) -> [a] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map a -> b
g [a]
ys
zipWithOrIdM :: Monad m => (a -> a -> m a) -> [a] -> [a] -> m [a]
zipWithOrIdM :: (a -> a -> m a) -> [a] -> [a] -> m [a]
zipWithOrIdM f :: a -> a -> m a
f xs :: [a]
xs ys :: [a]
ys = [m a] -> m [a]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ([m a] -> m [a]) -> [m a] -> m [a]
forall a b. (a -> b) -> a -> b
$ (a -> a -> m a) -> (a -> m a) -> [a] -> [a] -> [m a]
forall a b. (a -> a -> b) -> (a -> b) -> [a] -> [a] -> [b]
zipWithOrChange a -> a -> m a
f a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return [a]
xs [a]
ys
unionWithM :: (Monad m, Ord key) => (val -> val -> m val) -> Map key val -> Map key val -> m (Map key val)
unionWithM :: (val -> val -> m val)
-> Map key val -> Map key val -> m (Map key val)
unionWithM f :: val -> val -> m val
f m1 :: Map key val
m1 m2 :: Map key val
m2 = Map key (m val) -> m (Map key val)
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
T.sequence (Map key (m val) -> m (Map key val))
-> Map key (m val) -> m (Map key val)
forall a b. (a -> b) -> a -> b
$ (m val -> m val -> m val)
-> Map key (m val) -> Map key (m val) -> Map key (m val)
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith (\xm :: m val
xm ym :: m val
ym -> m (m val) -> m val
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (m (m val) -> m val) -> m (m val) -> m val
forall a b. (a -> b) -> a -> b
$ (val -> val -> m val) -> m val -> m val -> m (m val)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 val -> val -> m val
f m val
xm m val
ym) ((val -> m val) -> Map key val -> Map key (m val)
forall a b k. (a -> b) -> Map k a -> Map k b
M.map val -> m val
forall (m :: * -> *) a. Monad m => a -> m a
return Map key val
m1) ((val -> m val) -> Map key val -> Map key (m val)
forall a b k. (a -> b) -> Map k a -> Map k b
M.map val -> m val
forall (m :: * -> *) a. Monad m => a -> m a
return Map key val
m2)
intersectionWithM :: (Monad m, Ord key) => (val -> val -> m b) -> Map key val -> Map key val -> m (Map key b)
intersectionWithM :: (val -> val -> m b) -> Map key val -> Map key val -> m (Map key b)
intersectionWithM f :: val -> val -> m b
f m1 :: Map key val
m1 m2 :: Map key val
m2 = Map key (m b) -> m (Map key b)
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
T.sequence (Map key (m b) -> m (Map key b)) -> Map key (m b) -> m (Map key b)
forall a b. (a -> b) -> a -> b
$ (val -> val -> m b) -> Map key val -> Map key val -> Map key (m b)
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith val -> val -> m b
f Map key val
m1 Map key val
m2
class Compos1 t where
compos1 :: (forall a. a -> m a) -> (forall a b. m (a -> b) -> m a -> m b)
-> (t -> m t) -> t -> m t
instance Compos1 JType where
compos1 :: (forall a. a -> m a)
-> (forall a b. m (a -> b) -> m a -> m b)
-> (JType -> m JType)
-> JType
-> m JType
compos1 ret :: forall a. a -> m a
ret app :: forall a b. m (a -> b) -> m a -> m b
app f :: JType -> m JType
f v :: JType
v =
case JType
v of
JTFunc args :: [JType]
args body :: JType
body -> ([JType] -> JType -> JType) -> m ([JType] -> JType -> JType)
forall a. a -> m a
ret [JType] -> JType -> JType
JTFunc m ([JType] -> JType -> JType) -> m [JType] -> m (JType -> JType)
forall a b. m (a -> b) -> m a -> m b
`app` (JType -> m JType) -> [JType] -> m [JType]
forall (t :: * -> *) a a. Foldable t => (a -> m a) -> t a -> m [a]
mapM' JType -> m JType
f [JType]
args m (JType -> JType) -> m JType -> m JType
forall a b. m (a -> b) -> m a -> m b
`app` JType -> m JType
f JType
body
JTForall vars :: [VarRef]
vars t :: JType
t -> ([VarRef] -> JType -> JType) -> m ([VarRef] -> JType -> JType)
forall a. a -> m a
ret [VarRef] -> JType -> JType
JTForall m ([VarRef] -> JType -> JType) -> m [VarRef] -> m (JType -> JType)
forall a b. m (a -> b) -> m a -> m b
`app` [VarRef] -> m [VarRef]
forall a. a -> m a
ret [VarRef]
vars m (JType -> JType) -> m JType -> m JType
forall a b. m (a -> b) -> m a -> m b
`app` JType -> m JType
f JType
t
JTList t :: JType
t -> (JType -> JType) -> m (JType -> JType)
forall a. a -> m a
ret JType -> JType
JTList m (JType -> JType) -> m JType -> m JType
forall a b. m (a -> b) -> m a -> m b
`app` JType -> m JType
f JType
t
JTMap t :: JType
t -> (JType -> JType) -> m (JType -> JType)
forall a. a -> m a
ret JType -> JType
JTMap m (JType -> JType) -> m JType -> m JType
forall a b. m (a -> b) -> m a -> m b
`app` JType -> m JType
f JType
t
JTRecord t :: JType
t m :: Map String JType
m -> (JType -> Map String JType -> JType)
-> m (JType -> Map String JType -> JType)
forall a. a -> m a
ret JType -> Map String JType -> JType
JTRecord m (JType -> Map String JType -> JType)
-> m JType -> m (Map String JType -> JType)
forall a b. m (a -> b) -> m a -> m b
`app` JType -> m JType
f JType
t m (Map String JType -> JType) -> m (Map String JType) -> m JType
forall a b. m (a -> b) -> m a -> m b
`app` m (Map String JType)
m'
where (ls :: [String]
ls,ts :: [JType]
ts) = [(String, JType)] -> ([String], [JType])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(String, JType)] -> ([String], [JType]))
-> [(String, JType)] -> ([String], [JType])
forall a b. (a -> b) -> a -> b
$ Map String JType -> [(String, JType)]
forall k a. Map k a -> [(k, a)]
M.toList Map String JType
m
m' :: m (Map String JType)
m' = ([JType] -> Map String JType) -> m ([JType] -> Map String JType)
forall a. a -> m a
ret ([(String, JType)] -> Map String JType
forall k a. Eq k => [(k, a)] -> Map k a
M.fromAscList ([(String, JType)] -> Map String JType)
-> ([JType] -> [(String, JType)]) -> [JType] -> Map String JType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> [JType] -> [(String, JType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [String]
ls) m ([JType] -> Map String JType)
-> m [JType] -> m (Map String JType)
forall a b. m (a -> b) -> m a -> m b
`app` (JType -> m JType) -> [JType] -> m [JType]
forall (t :: * -> *) a a. Foldable t => (a -> m a) -> t a -> m [a]
mapM' JType -> m JType
f [JType]
ts
x :: JType
x -> JType -> m JType
forall a. a -> m a
ret JType
x
where
mapM' :: (a -> m a) -> t a -> m [a]
mapM' g :: a -> m a
g = (a -> m [a] -> m [a]) -> m [a] -> t a -> m [a]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (m ([a] -> [a]) -> m [a] -> m [a]
forall a b. m (a -> b) -> m a -> m b
app (m ([a] -> [a]) -> m [a] -> m [a])
-> (a -> m ([a] -> [a])) -> a -> m [a] -> m [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (a -> [a] -> [a]) -> m a -> m ([a] -> [a])
forall a b. m (a -> b) -> m a -> m b
app ((a -> [a] -> [a]) -> m (a -> [a] -> [a])
forall a. a -> m a
ret (:)) (m a -> m ([a] -> [a])) -> (a -> m a) -> a -> m ([a] -> [a])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> m a
g) ([a] -> m [a]
forall a. a -> m a
ret [])
composOp1 :: Compos1 t => (t -> t) -> t -> t
composOp1 :: (t -> t) -> t -> t
composOp1 f :: t -> t
f = Identity t -> t
forall a. Identity a -> a
runIdentity (Identity t -> t) -> (t -> Identity t) -> t -> t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (t -> Identity t) -> t -> Identity t
forall t (m :: * -> *).
(Compos1 t, Monad m) =>
(t -> m t) -> t -> m t
composOpM1 (t -> Identity t
forall a. a -> Identity a
Identity (t -> Identity t) -> (t -> t) -> t -> Identity t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> t
f)
composOpM1 :: (Compos1 t, Monad m) => (t -> m t) -> t -> m t
composOpM1 :: (t -> m t) -> t -> m t
composOpM1 = (forall a. a -> m a)
-> (forall a b. m (a -> b) -> m a -> m b) -> (t -> m t) -> t -> m t
forall t (m :: * -> *).
Compos1 t =>
(forall a. a -> m a)
-> (forall a b. m (a -> b) -> m a -> m b) -> (t -> m t) -> t -> m t
compos1 forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. m (a -> b) -> m a -> m b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
composOpM1_ :: (Compos1 t, Monad m) => (t -> m ()) -> t -> m ()
composOpM1_ :: (t -> m ()) -> t -> m ()
composOpM1_ = m () -> (m () -> m () -> m ()) -> (t -> m ()) -> t -> m ()
forall t b. Compos1 t => b -> (b -> b -> b) -> (t -> b) -> t -> b
composOpFold1 (() -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()) m () -> m () -> m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
(>>)
composOpFold1 :: Compos1 t => b -> (b -> b -> b) -> (t -> b) -> t -> b
composOpFold1 :: b -> (b -> b -> b) -> (t -> b) -> t -> b
composOpFold1 z :: b
z c :: b -> b -> b
c f :: t -> b
f = C b t -> b
forall b a. C b a -> b
unC (C b t -> b) -> (t -> C b t) -> t -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. a -> C b a)
-> (forall a b. C b (a -> b) -> C b a -> C b b)
-> (t -> C b t)
-> t
-> C b t
forall t (m :: * -> *).
Compos1 t =>
(forall a. a -> m a)
-> (forall a b. m (a -> b) -> m a -> m b) -> (t -> m t) -> t -> m t
compos1 (\_ -> b -> C b a
forall b a. b -> C b a
C b
z) (\(C x) (C y) -> b -> C b b
forall b a. b -> C b a
C (b -> b -> b
c b
x b
y)) (b -> C b t
forall b a. b -> C b a
C (b -> C b t) -> (t -> b) -> t -> C b t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> b
f)
newtype C b a = C { C b a -> b
unC :: b }
data StoreVal = SVType JType
| SVConstrained (Set Constraint)
deriving Int -> StoreVal -> ShowS
[StoreVal] -> ShowS
StoreVal -> String
(Int -> StoreVal -> ShowS)
-> (StoreVal -> String) -> ([StoreVal] -> ShowS) -> Show StoreVal
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [StoreVal] -> ShowS
$cshowList :: [StoreVal] -> ShowS
show :: StoreVal -> String
$cshow :: StoreVal -> String
showsPrec :: Int -> StoreVal -> ShowS
$cshowsPrec :: Int -> StoreVal -> ShowS
Show
data TCState = TCS {TCState -> [Map Ident JType]
tc_env :: [Map Ident JType],
TCState -> Map Int StoreVal
tc_vars :: Map Int StoreVal,
TCState -> [Set Int]
tc_stack :: [Set Int],
TCState -> Set Int
tc_frozen :: Set Int,
TCState -> Int
tc_varCt :: Int,
TCState -> [TMonad String]
tc_context :: [TMonad String]}
instance Show TCState where
show :: TCState -> String
show (TCS env :: [Map Ident JType]
env vars :: Map Int StoreVal
vars stack :: [Set Int]
stack frozen :: Set Int
frozen varCt :: Int
varCt cxt :: [TMonad String]
cxt) =
"env: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Map Ident JType] -> String
forall a. Show a => a -> String
show [Map Ident JType]
env String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
"vars: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Map Int StoreVal -> String
forall a. Show a => a -> String
show Map Int StoreVal
vars String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
"stack: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Set Int] -> String
forall a. Show a => a -> String
show [Set Int]
stack String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
"frozen: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Set Int -> String
forall a. Show a => a -> String
show Set Int
frozen String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
"varCt: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
varCt
tcStateEmpty :: TCState
tcStateEmpty :: TCState
tcStateEmpty = [Map Ident JType]
-> Map Int StoreVal
-> [Set Int]
-> Set Int
-> Int
-> [TMonad String]
-> TCState
TCS [Map Ident JType
forall k a. Map k a
M.empty] Map Int StoreVal
forall k a. Map k a
M.empty [Set Int
forall a. Set a
S.empty] Set Int
forall a. Set a
S.empty 0 []
newtype TMonad a = TMonad (ErrorT String (State TCState) a) deriving (a -> TMonad b -> TMonad a
(a -> b) -> TMonad a -> TMonad b
(forall a b. (a -> b) -> TMonad a -> TMonad b)
-> (forall a b. a -> TMonad b -> TMonad a) -> Functor TMonad
forall a b. a -> TMonad b -> TMonad a
forall a b. (a -> b) -> TMonad a -> TMonad b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> TMonad b -> TMonad a
$c<$ :: forall a b. a -> TMonad b -> TMonad a
fmap :: (a -> b) -> TMonad a -> TMonad b
$cfmap :: forall a b. (a -> b) -> TMonad a -> TMonad b
Functor, Applicative TMonad
a -> TMonad a
Applicative TMonad =>
(forall a b. TMonad a -> (a -> TMonad b) -> TMonad b)
-> (forall a b. TMonad a -> TMonad b -> TMonad b)
-> (forall a. a -> TMonad a)
-> Monad TMonad
TMonad a -> (a -> TMonad b) -> TMonad b
TMonad a -> TMonad b -> TMonad b
forall a. a -> TMonad a
forall a b. TMonad a -> TMonad b -> TMonad b
forall a b. TMonad a -> (a -> TMonad b) -> TMonad b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> TMonad a
$creturn :: forall a. a -> TMonad a
>> :: TMonad a -> TMonad b -> TMonad b
$c>> :: forall a b. TMonad a -> TMonad b -> TMonad b
>>= :: TMonad a -> (a -> TMonad b) -> TMonad b
$c>>= :: forall a b. TMonad a -> (a -> TMonad b) -> TMonad b
$cp1Monad :: Applicative TMonad
Monad, MonadState TCState, MonadError String)
instance Applicative TMonad where
pure :: a -> TMonad a
pure = a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return
<*> :: TMonad (a -> b) -> TMonad a -> TMonad b
(<*>) = TMonad (a -> b) -> TMonad a -> TMonad b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
class JTypeCheck a where
typecheck :: a -> TMonad JType
evalTMonad :: TMonad a -> Either String a
evalTMonad :: TMonad a -> Either String a
evalTMonad (TMonad x :: ErrorT String (State TCState) a
x) = State TCState (Either String a) -> TCState -> Either String a
forall s a. State s a -> s -> a
evalState (ErrorT String (State TCState) a -> State TCState (Either String a)
forall e (m :: * -> *) a. ErrorT e m a -> m (Either e a)
runErrorT ErrorT String (State TCState) a
x) TCState
tcStateEmpty
runTMonad :: TMonad a -> (Either String a, TCState)
runTMonad :: TMonad a -> (Either String a, TCState)
runTMonad (TMonad x :: ErrorT String (State TCState) a
x) = State TCState (Either String a)
-> TCState -> (Either String a, TCState)
forall s a. State s a -> s -> (a, s)
runState (ErrorT String (State TCState) a -> State TCState (Either String a)
forall e (m :: * -> *) a. ErrorT e m a -> m (Either e a)
runErrorT ErrorT String (State TCState) a
x) TCState
tcStateEmpty
withContext :: TMonad a -> TMonad String -> TMonad a
withContext :: TMonad a -> TMonad String -> TMonad a
withContext act :: TMonad a
act cxt :: TMonad String
cxt = do
[TMonad String]
cs <- TCState -> [TMonad String]
tc_context (TCState -> [TMonad String])
-> TMonad TCState -> TMonad [TMonad String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TMonad TCState
forall s (m :: * -> *). MonadState s m => m s
get
(TCState -> TCState) -> TMonad ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\s :: TCState
s -> TCState
s {tc_context :: [TMonad String]
tc_context = TMonad String
cxt TMonad String -> [TMonad String] -> [TMonad String]
forall a. a -> [a] -> [a]
: [TMonad String]
cs})
a
res <- TMonad a
act
(TCState -> TCState) -> TMonad ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\s :: TCState
s -> TCState
s {tc_context :: [TMonad String]
tc_context = [TMonad String]
cs})
a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return a
res
traversem_ :: (F.Foldable t, Monad f) => (a -> f b) -> t a -> f ()
traversem_ :: (a -> f b) -> t a -> f ()
traversem_ f :: a -> f b
f = (a -> f () -> f ()) -> f () -> t a -> f ()
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
F.foldr (f b -> f () -> f ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
(>>) (f b -> f () -> f ()) -> (a -> f b) -> a -> f () -> f ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> f b
f) (() -> f ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
freeVarsWithNames :: JType -> TMonad (Map Int String)
freeVarsWithNames :: JType -> TMonad (Map Int String)
freeVarsWithNames x :: JType
x =
Map Int (Either String Int) -> Map Int String
forall k. Map k (Either String Int) -> Map k String
intsToNames (Map Int (Either String Int) -> Map Int String)
-> ((Map Int (Either String Int), Set String, Int)
-> Map Int (Either String Int))
-> (Map Int (Either String Int), Set String, Int)
-> Map Int String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(a :: Map Int (Either String Int)
a,_,_) -> Map Int (Either String Int)
a) ((Map Int (Either String Int), Set String, Int) -> Map Int String)
-> TMonad (Map Int (Either String Int), Set String, Int)
-> TMonad (Map Int String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
StateT (Map Int (Either String Int), Set String, Int) TMonad ()
-> (Map Int (Either String Int), Set String, Int)
-> TMonad (Map Int (Either String Int), Set String, Int)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT (JType
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
go JType
x) (Map Int (Either String Int)
forall k a. Map k a
M.empty, Set String
forall a. Set a
S.empty, 0)
where
go :: JType -> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
go :: JType
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
go (JTFree vr :: VarRef
vr) = VarRef
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
handleVR VarRef
vr
go (JTRigid vr :: VarRef
vr cs :: Set Constraint
cs) = VarRef
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
handleVR VarRef
vr StateT (Map Int (Either String Int), Set String, Int) TMonad ()
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Constraint
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ())
-> Set Constraint
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Monad f) =>
(a -> f b) -> t a -> f ()
traversem_ (JType
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
go (JType
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ())
-> (Constraint -> JType)
-> Constraint
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constraint -> JType
fromC) Set Constraint
cs
go v :: JType
v = (JType
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ())
-> JType
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
forall t (m :: * -> *).
(Compos1 t, Monad m) =>
(t -> m ()) -> t -> m ()
composOpM1_ JType
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
go JType
v
handleVR :: VarRef
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
handleVR (mbName :: Maybe String
mbName, ref :: Int
ref) = do
(m :: Map Int (Either String Int)
m,ns :: Set String
ns,ct :: Int
ct) <- StateT
(Map Int (Either String Int), Set String, Int)
TMonad
(Map Int (Either String Int), Set String, Int)
forall s (m :: * -> *). MonadState s m => m s
get
case Int -> Map Int (Either String Int) -> Maybe (Either String Int)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Int
ref Map Int (Either String Int)
m of
Just (Left _) -> ()
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just (Right _) -> case Maybe String
mbName of
Just name :: String
name -> String
-> Int
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
forall (m :: * -> *) k b c.
(MonadState (Map k (Either String b), Set String, c) m, Ord k) =>
String -> k -> m ()
putName String
name Int
ref
Nothing -> ()
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Nothing -> do
case Maybe String
mbName of
Just name :: String
name -> String
-> Int
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
forall (m :: * -> *) k b c.
(MonadState (Map k (Either String b), Set String, c) m, Ord k) =>
String -> k -> m ()
putName String
name Int
ref
Nothing -> (Map Int (Either String Int), Set String, Int)
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
-> Either String Int
-> Map Int (Either String Int)
-> Map Int (Either String Int)
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Int
ref (Int -> Either String Int
forall a b. b -> Either a b
Right Int
ct) Map Int (Either String Int)
m, Set String
ns, Int
ct Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)
(Constraint
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ())
-> [Constraint]
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Monad f) =>
(a -> f b) -> t a -> f ()
mapM_ (JType
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
go (JType
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ())
-> (Constraint -> JType)
-> Constraint
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constraint -> JType
fromC) ([Constraint]
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ())
-> StateT
(Map Int (Either String Int), Set String, Int) TMonad [Constraint]
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TMonad [Constraint]
-> StateT
(Map Int (Either String Int), Set String, Int) TMonad [Constraint]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (VarRef -> TMonad [Constraint]
lookupConstraintsList (Maybe String
mbName, Int
ref))
putName :: String -> k -> m ()
putName n :: String
n ref :: k
ref = do
(m :: Map k (Either String b)
m,ns :: Set String
ns,ct :: c
ct) <- m (Map k (Either String b), Set String, c)
forall s (m :: * -> *). MonadState s m => m s
get
let n' :: String
n' = Set String -> String -> Int -> String
mkUnique Set String
ns String
n 0
(Map k (Either String b), Set String, c) -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (k
-> Either String b
-> Map k (Either String b)
-> Map k (Either String b)
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert k
ref (String -> Either String b
forall a b. a -> Either a b
Left String
n') Map k (Either String b)
m, String -> Set String -> Set String
forall a. Ord a => a -> Set a -> Set a
S.insert String
n' Set String
ns, c
ct)
mkUnique :: Set String -> String -> Int -> String
mkUnique :: Set String -> String -> Int -> String
mkUnique ns :: Set String
ns n :: String
n i :: Int
i
| String
n' String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set String
ns = Set String -> String -> Int -> String
mkUnique Set String
ns String
n (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)
| Bool
otherwise = String
n'
where n' :: String
n' | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0 = String
n
| Bool
otherwise = String
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
fromC :: Constraint -> JType
fromC (Sub t :: JType
t) = JType
t
fromC (Super t :: JType
t) = JType
t
intsToNames :: Map k (Either String Int) -> Map k String
intsToNames x :: Map k (Either String Int)
x = (Either String Int -> String)
-> Map k (Either String Int) -> Map k String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ShowS -> (Int -> String) -> Either String Int -> String
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ShowS
forall a. a -> a
id Int -> String
go) Map k (Either String Int)
x
where go :: Int -> String
go i :: Int
i = Set String -> String -> Int -> String
mkUnique ([String] -> Set String
forall a. Ord a => [a] -> Set a
S.fromList ([String] -> Set String) -> [String] -> Set String
forall a b. (a -> b) -> a -> b
$ [Either String Int] -> [String]
forall a b. [Either a b] -> [a]
lefts ([Either String Int] -> [String])
-> [Either String Int] -> [String]
forall a b. (a -> b) -> a -> b
$ Map k (Either String Int) -> [Either String Int]
forall k a. Map k a -> [a]
M.elems Map k (Either String Int)
x) (Int -> String
int2Name Int
i) 0
int2Name :: Int -> String
int2Name i :: Int
i | Int
q Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0 = [Char
letter]
| Bool
otherwise = Char
letter Char -> ShowS
forall a. a -> [a] -> [a]
: Int -> String
forall a. Show a => a -> String
show Int
q
where (q :: Int
q,r :: Int
r) = Int -> Int -> (Int, Int)
forall a. Integral a => a -> a -> (a, a)
divMod Int
i 26
letter :: Char
letter = Int -> Char
forall a. Enum a => Int -> a
toEnum (Char -> Int
forall a. Enum a => a -> Int
fromEnum 'a' Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
r)
prettyType :: JType -> TMonad String
prettyType :: JType -> TMonad String
prettyType x :: JType
x = do
JType
xt <- JType -> TMonad JType
resolveType JType
x
Map Int String
names <- JType -> TMonad (Map Int String)
freeVarsWithNames JType
xt
let replaceNames :: JType -> JType
replaceNames (JTFree ref :: VarRef
ref) = VarRef -> JType
JTFree (VarRef -> JType) -> VarRef -> JType
forall a b. (a -> b) -> a -> b
$ VarRef -> VarRef
forall a. (a, Int) -> VarRef
fixRef VarRef
ref
replaceNames (JTForall refs :: [VarRef]
refs t :: JType
t) = [VarRef] -> JType -> JType
JTForall ((VarRef -> VarRef) -> [VarRef] -> [VarRef]
forall a b. (a -> b) -> [a] -> [b]
map VarRef -> VarRef
forall a. (a, Int) -> VarRef
fixRef [VarRef]
refs) (JType -> JType) -> JType -> JType
forall a b. (a -> b) -> a -> b
$ JType -> JType
replaceNames JType
t
replaceNames v :: JType
v = (JType -> JType) -> JType -> JType
forall t. Compos1 t => (t -> t) -> t -> t
composOp1 JType -> JType
replaceNames JType
v
fixRef :: (a, Int) -> VarRef
fixRef (_,ref :: Int
ref) = (Int -> Map Int String -> Maybe String
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Int
ref Map Int String
names, Int
ref)
prettyConstraints :: Int -> TMonad [String]
prettyConstraints ref :: Int
ref = (Constraint -> String) -> [Constraint] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Constraint -> String
go ([Constraint] -> [String])
-> TMonad [Constraint] -> TMonad [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VarRef -> TMonad [Constraint]
lookupConstraintsList (Maybe String
forall a. Maybe a
Nothing, Int
ref)
where
myName :: String
myName = case Int -> Map Int String -> Maybe String
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Int
ref Map Int String
names of
Just n :: String
n -> String
n
Nothing -> "t_"String -> ShowS
forall a. [a] -> [a] -> [a]
++Int -> String
forall a. Show a => a -> String
show Int
ref
go :: Constraint -> String
go (Sub t :: JType
t) = String
myName String -> ShowS
forall a. [a] -> [a] -> [a]
++ " <: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ JType -> Doc
forall a. JsToDoc a => a -> Doc
jsToDoc (JType -> Doc) -> JType -> Doc
forall a b. (a -> b) -> a -> b
$ JType -> JType
replaceNames JType
t)
go (Super t :: JType
t) = (Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ JType -> Doc
forall a. JsToDoc a => a -> Doc
jsToDoc (JType -> Doc) -> JType -> Doc
forall a b. (a -> b) -> a -> b
$ JType -> JType
replaceNames JType
t) String -> ShowS
forall a. [a] -> [a] -> [a]
++ " <: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
myName
[String]
constraintStrings <- [String] -> [String]
forall a. Eq a => [a] -> [a]
nub ([String] -> [String])
-> ([[String]] -> [String]) -> [[String]] -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[String]] -> [String]) -> TMonad [[String]] -> TMonad [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int -> TMonad [String]) -> [Int] -> TMonad [[String]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Int -> TMonad [String]
prettyConstraints (Map Int String -> [Int]
forall k a. Map k a -> [k]
M.keys Map Int String
names)
let constraintStr :: String
constraintStr
| [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
constraintStrings = ""
| Bool
otherwise = "(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate ", " [String]
constraintStrings String -> ShowS
forall a. [a] -> [a] -> [a]
++ ") => "
String -> TMonad String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> TMonad String) -> String -> TMonad String
forall a b. (a -> b) -> a -> b
$ String
constraintStr String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (JType -> Doc) -> JType -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. JType -> Doc
forall a. JsToDoc a => a -> Doc
jsToDoc (JType -> String) -> JType -> String
forall a b. (a -> b) -> a -> b
$ JType -> JType
replaceNames JType
xt)
tyErr0 :: String -> TMonad a
tyErr0 :: String -> TMonad a
tyErr0 x :: String
x = String -> TMonad a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
x
tyErr1 :: String -> JType -> TMonad b
tyErr1 :: String -> JType -> TMonad b
tyErr1 s :: String
s t :: JType
t = do
String
st <- JType -> TMonad String
prettyType JType
t
String -> TMonad b
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> TMonad b) -> String -> TMonad b
forall a b. (a -> b) -> a -> b
$ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ ": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
st
tyErr2ext :: String -> String -> String -> JType -> JType -> TMonad a
tyErr2ext :: String -> String -> String -> JType -> JType -> TMonad a
tyErr2ext s :: String
s s1 :: String
s1 s2 :: String
s2 t :: JType
t t' :: JType
t' = do
String
st <- JType -> TMonad String
prettyType JType
t
String
st' <- JType -> TMonad String
prettyType JType
t'
String -> TMonad a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> TMonad a) -> String -> TMonad a
forall a b. (a -> b) -> a -> b
$ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ ". " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ ": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
st String -> ShowS
forall a. [a] -> [a] -> [a]
++ ", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ ": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
st'
tyErr2Sub :: JType -> JType -> TMonad a
tyErr2Sub :: JType -> JType -> TMonad a
tyErr2Sub t :: JType
t t' :: JType
t' = String -> String -> String -> JType -> JType -> TMonad a
forall a. String -> String -> String -> JType -> JType -> TMonad a
tyErr2ext "Couldn't apply subtype relation" "Subtype" "Supertype" JType
t JType
t'
prettyEnv :: TMonad [Map Ident String]
prettyEnv :: TMonad [Map Ident String]
prettyEnv = (Map Ident JType -> TMonad (Map Ident String))
-> [Map Ident JType] -> TMonad [Map Ident String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((JType -> TMonad String)
-> Map Ident JType -> TMonad (Map Ident String)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
T.mapM JType -> TMonad String
prettyType) ([Map Ident JType] -> TMonad [Map Ident String])
-> (TCState -> [Map Ident JType])
-> TCState
-> TMonad [Map Ident String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCState -> [Map Ident JType]
tc_env (TCState -> TMonad [Map Ident String])
-> TMonad TCState -> TMonad [Map Ident String]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TMonad TCState
forall s (m :: * -> *). MonadState s m => m s
get
runTypecheckRaw :: JTypeCheck a => a -> (Either String JType, TCState)
runTypecheckRaw :: a -> (Either String JType, TCState)
runTypecheckRaw x :: a
x = TMonad JType -> (Either String JType, TCState)
forall a. TMonad a -> (Either String a, TCState)
runTMonad (a -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheckMain a
x)
runTypecheckFull :: JTypeCheck a => a -> (Either String (String, [Map Ident String]), TCState)
runTypecheckFull :: a -> (Either String (String, [Map Ident String]), TCState)
runTypecheckFull x :: a
x = TMonad (String, [Map Ident String])
-> (Either String (String, [Map Ident String]), TCState)
forall a. TMonad a -> (Either String a, TCState)
runTMonad (TMonad (String, [Map Ident String])
-> (Either String (String, [Map Ident String]), TCState))
-> TMonad (String, [Map Ident String])
-> (Either String (String, [Map Ident String]), TCState)
forall a b. (a -> b) -> a -> b
$ do
String
r <- JType -> TMonad String
prettyType (JType -> TMonad String) -> TMonad JType -> TMonad String
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< a -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheckMain a
x
[Map Ident String]
e <- TMonad [Map Ident String]
prettyEnv
(String, [Map Ident String]) -> TMonad (String, [Map Ident String])
forall (m :: * -> *) a. Monad m => a -> m a
return (String
r,[Map Ident String]
e)
runTypecheck :: JTypeCheck a => a -> Either String String
runTypecheck :: a -> Either String String
runTypecheck x :: a
x = TMonad String -> Either String String
forall a. TMonad a -> Either String a
evalTMonad (TMonad String -> Either String String)
-> TMonad String -> Either String String
forall a b. (a -> b) -> a -> b
$ JType -> TMonad String
prettyType (JType -> TMonad String) -> TMonad JType -> TMonad String
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< a -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheckMain a
x
evalTypecheck :: JTypeCheck a => a -> Either String [Map Ident String]
evalTypecheck :: a -> Either String [Map Ident String]
evalTypecheck x :: a
x = TMonad [Map Ident String] -> Either String [Map Ident String]
forall a. TMonad a -> Either String a
evalTMonad (TMonad [Map Ident String] -> Either String [Map Ident String])
-> TMonad [Map Ident String] -> Either String [Map Ident String]
forall a b. (a -> b) -> a -> b
$ do
JType
_ <- a -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheckMain a
x
[Map Ident String]
e <- TMonad [Map Ident String]
prettyEnv
[Map Ident String] -> TMonad [Map Ident String]
forall (m :: * -> *) a. Monad m => a -> m a
return [Map Ident String]
e
typecheckMain :: JTypeCheck a => a -> TMonad JType
typecheckMain :: a -> TMonad JType
typecheckMain x :: a
x = TMonad JType
go TMonad JType -> (String -> TMonad JType) -> TMonad JType
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` String -> TMonad JType
forall a. String -> TMonad a
handler
where go :: TMonad JType
go = do
JType
r <- a -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck a
x
Set Int -> TMonad ()
setFrozen (Set Int -> TMonad ())
-> (TCState -> Set Int) -> TCState -> TMonad ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Set Int] -> Set Int
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ([Set Int] -> Set Int)
-> (TCState -> [Set Int]) -> TCState -> Set Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCState -> [Set Int]
tc_stack (TCState -> TMonad ()) -> TMonad TCState -> TMonad ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TMonad TCState
forall s (m :: * -> *). MonadState s m => m s
get
TMonad ()
tryCloseFrozenVars
JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
r
handler :: String -> TMonad b
handler e :: String
e = do
[TMonad String]
cxt <- TCState -> [TMonad String]
tc_context (TCState -> [TMonad String])
-> TMonad TCState -> TMonad [TMonad String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TMonad TCState
forall s (m :: * -> *). MonadState s m => m s
get
String -> TMonad b
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> TMonad b) -> TMonad String -> TMonad b
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ([String] -> String
unlines ([String] -> String)
-> ([String] -> [String]) -> [String] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
eString -> [String] -> [String]
forall a. a -> [a] -> [a]
:) ([String] -> String) -> TMonad [String] -> TMonad String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TMonad String] -> TMonad [String]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [TMonad String]
cxt)
addToStack :: Ord a => a -> [Set a] -> [Set a]
addToStack :: a -> [Set a] -> [Set a]
addToStack v :: a
v (s :: Set a
s:ss :: [Set a]
ss) = a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
S.insert a
v Set a
s Set a -> [Set a] -> [Set a]
forall a. a -> [a] -> [a]
: [Set a]
ss
addToStack _ _ = String -> [Set a]
forall a. HasCallStack => String -> a
error "addToStack: no sets"
newVarRef :: TMonad VarRef
newVarRef :: TMonad VarRef
newVarRef = do
Int
v <- TCState -> Int
tc_varCt (TCState -> Int) -> TMonad TCState -> TMonad Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TMonad TCState
forall s (m :: * -> *). MonadState s m => m s
get
(TCState -> TCState) -> TMonad ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\s :: TCState
s -> TCState
s {tc_varCt :: Int
tc_varCt = Int
v Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1,
tc_stack :: [Set Int]
tc_stack = Int -> [Set Int] -> [Set Int]
forall a. Ord a => a -> [Set a] -> [Set a]
addToStack Int
v (TCState -> [Set Int]
tc_stack TCState
s)})
VarRef -> TMonad VarRef
forall (m :: * -> *) a. Monad m => a -> m a
return (VarRef -> TMonad VarRef) -> VarRef -> TMonad VarRef
forall a b. (a -> b) -> a -> b
$ (Maybe String
forall a. Maybe a
Nothing, Int
v)
newTyVar :: TMonad JType
newTyVar :: TMonad JType
newTyVar = VarRef -> JType
JTFree (VarRef -> JType) -> TMonad VarRef -> TMonad JType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TMonad VarRef
newVarRef
mapConstraint :: (Monad m, Functor m) => (JType -> m JType) -> Constraint -> m Constraint
mapConstraint :: (JType -> m JType) -> Constraint -> m Constraint
mapConstraint f :: JType -> m JType
f (Sub t :: JType
t) = JType -> Constraint
Sub (JType -> Constraint) -> m JType -> m Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> JType -> m JType
f JType
t
mapConstraint f :: JType -> m JType
f (Super t :: JType
t) = JType -> Constraint
Super (JType -> Constraint) -> m JType -> m Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> JType -> m JType
f JType
t
partitionCs :: [Constraint] -> ([JType],[JType])
partitionCs :: [Constraint] -> ([JType], [JType])
partitionCs [] = ([],[])
partitionCs (Sub t :: JType
t:cs :: [Constraint]
cs) = (JType
tJType -> [JType] -> [JType]
forall a. a -> [a] -> [a]
:[JType]
subs,[JType]
sups)
where (subs :: [JType]
subs,sups :: [JType]
sups) = [Constraint] -> ([JType], [JType])
partitionCs [Constraint]
cs
partitionCs (Super t :: JType
t:cs :: [Constraint]
cs) = ([JType]
subs,JType
tJType -> [JType] -> [JType]
forall a. a -> [a] -> [a]
:[JType]
sups)
where (subs :: [JType]
subs,sups :: [JType]
sups) = [Constraint] -> ([JType], [JType])
partitionCs [Constraint]
cs
lookupConstraintsList :: VarRef -> TMonad [Constraint]
lookupConstraintsList :: VarRef -> TMonad [Constraint]
lookupConstraintsList vr :: VarRef
vr@(_,ref :: Int
ref) = do
Map Int StoreVal
vars <- TCState -> Map Int StoreVal
tc_vars (TCState -> Map Int StoreVal)
-> TMonad TCState -> TMonad (Map Int StoreVal)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TMonad TCState
forall s (m :: * -> *). MonadState s m => m s
get
case Int -> Map Int StoreVal -> Maybe StoreVal
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Int
ref Map Int StoreVal
vars of
(Just (SVConstrained cs :: Set Constraint
cs)) -> (Constraint -> Bool) -> [Constraint] -> [Constraint]
forall a. (a -> Bool) -> [a] -> [a]
filter Constraint -> Bool
notLoop ([Constraint] -> [Constraint])
-> ([Constraint] -> [Constraint]) -> [Constraint] -> [Constraint]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Constraint] -> [Constraint]
forall a. Eq a => [a] -> [a]
nub ([Constraint] -> [Constraint])
-> TMonad [Constraint] -> TMonad [Constraint]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Constraint -> TMonad Constraint)
-> [Constraint] -> TMonad [Constraint]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((JType -> TMonad JType) -> Constraint -> TMonad Constraint
forall (m :: * -> *).
(Monad m, Functor m) =>
(JType -> m JType) -> Constraint -> m Constraint
mapConstraint JType -> TMonad JType
resolveType) (Set Constraint -> [Constraint]
forall a. Set a -> [a]
S.toList Set Constraint
cs)
(Just (SVType t :: JType
t)) -> String -> JType -> TMonad [Constraint]
forall b. String -> JType -> TMonad b
tyErr1 "lookupConstraints on instantiated type" JType
t
Nothing -> [Constraint] -> TMonad [Constraint]
forall (m :: * -> *) a. Monad m => a -> m a
return []
where
notLoop :: Constraint -> Bool
notLoop (Super (JTFree (_,ref' :: Int
ref'))) | Int
ref Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ref' = Bool
False
notLoop (Sub (JTFree (_,ref' :: Int
ref'))) | Int
ref Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ref' = Bool
False
notLoop _ = Bool
True
instantiateVarRef :: VarRef -> JType -> TMonad ()
instantiateVarRef :: VarRef -> JType -> TMonad ()
instantiateVarRef vr :: VarRef
vr@(_,ref :: Int
ref) (JTFree (_,ref' :: Int
ref')) | Int
ref Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ref' = do
[Constraint]
cs <- VarRef -> TMonad [Constraint]
lookupConstraintsList VarRef
vr
let cs' :: [Constraint]
cs' = [Constraint] -> [Constraint]
simplify [Constraint]
cs
(TCState -> TCState) -> TMonad ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\s :: TCState
s -> TCState
s {tc_vars :: Map Int StoreVal
tc_vars = Int -> StoreVal -> Map Int StoreVal -> Map Int StoreVal
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Int
ref (Set Constraint -> StoreVal
SVConstrained ([Constraint] -> Set Constraint
forall a. Ord a => [a] -> Set a
S.fromList [Constraint]
cs')) (TCState -> Map Int StoreVal
tc_vars TCState
s)})
where simplify :: [Constraint] -> [Constraint]
simplify (Sub (JTFree (_,r :: Int
r)):cs :: [Constraint]
cs) | Int
r Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ref = [Constraint]
cs
simplify (Super (JTFree (_,r :: Int
r)):cs :: [Constraint]
cs) | Int
r Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ref = [Constraint]
cs
simplify (c :: Constraint
c:cs :: [Constraint]
cs) = Constraint
c Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
: [Constraint] -> [Constraint]
simplify [Constraint]
cs
simplify x :: [Constraint]
x = [Constraint]
x
instantiateVarRef vr :: VarRef
vr@(_,ref :: Int
ref) t :: JType
t = do
Int -> JType -> TMonad ()
occursCheck Int
ref JType
t
[Constraint]
cs <- VarRef -> TMonad [Constraint]
lookupConstraintsList VarRef
vr
(TCState -> TCState) -> TMonad ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\s :: TCState
s -> TCState
s {tc_vars :: Map Int StoreVal
tc_vars = Int -> StoreVal -> Map Int StoreVal -> Map Int StoreVal
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Int
ref (JType -> StoreVal
SVType JType
t) (TCState -> Map Int StoreVal
tc_vars TCState
s)})
JType -> [Constraint] -> TMonad ()
checkConstraints JType
t [Constraint]
cs
occursCheck :: Int -> JType -> TMonad ()
occursCheck :: Int -> JType -> TMonad ()
occursCheck ref :: Int
ref (JTFree (_,i :: Int
i))
| Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ref = String -> JType -> TMonad ()
forall b. String -> JType -> TMonad b
tyErr1 "Occurs check: cannot construct infinite type" (VarRef -> JType
JTFree (Maybe String
forall a. Maybe a
Nothing,Int
i))
occursCheck ref :: Int
ref x :: JType
x = (JType -> TMonad ()) -> JType -> TMonad ()
forall t (m :: * -> *).
(Compos1 t, Monad m) =>
(t -> m ()) -> t -> m ()
composOpM1_ (Int -> JType -> TMonad ()
occursCheck Int
ref) JType
x
checkConstraints :: JType -> [Constraint] -> TMonad ()
checkConstraints :: JType -> [Constraint] -> TMonad ()
checkConstraints t :: JType
t cs :: [Constraint]
cs = (Constraint -> TMonad ()) -> [Constraint] -> TMonad ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Monad f) =>
(a -> f b) -> t a -> f ()
mapM_ Constraint -> TMonad ()
go [Constraint]
cs
where go :: Constraint -> TMonad ()
go (Sub t2 :: JType
t2) = JType
t JType -> JType -> TMonad ()
<: JType
t2
go (Super t2 :: JType
t2) = JType
t2 JType -> JType -> TMonad ()
<: JType
t
addConstraint :: VarRef -> Constraint -> TMonad ()
addConstraint :: VarRef -> Constraint -> TMonad ()
addConstraint vr :: VarRef
vr@(_,ref :: Int
ref) c :: Constraint
c = case Constraint
c of
Sub t :: JType
t -> case JType
t of
JTFree _ -> Constraint -> TMonad ()
addC Constraint
c
JTForall vars :: [VarRef]
vars t :: JType
t -> [Constraint] -> TMonad ()
normalizeConstraints ([Constraint] -> TMonad ())
-> ([Constraint] -> [Constraint]) -> [Constraint] -> TMonad ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Constraint
c Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
: ) ([Constraint] -> TMonad ()) -> TMonad [Constraint] -> TMonad ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< VarRef -> TMonad [Constraint]
lookupConstraintsList VarRef
vr
JTFunc args :: [JType]
args res :: JType
res -> do
(JType -> TMonad ()) -> [JType] -> TMonad ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Monad f) =>
(a -> f b) -> t a -> f ()
mapM_ (Int -> JType -> TMonad ()
occursCheck Int
ref) (JType
resJType -> [JType] -> [JType]
forall a. a -> [a] -> [a]
:[JType]
args)
[Constraint] -> TMonad ()
normalizeConstraints ([Constraint] -> TMonad ())
-> ([Constraint] -> [Constraint]) -> [Constraint] -> TMonad ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Constraint
c Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
:) ([Constraint] -> TMonad ()) -> TMonad [Constraint] -> TMonad ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< VarRef -> TMonad [Constraint]
lookupConstraintsList VarRef
vr
JTRecord t :: JType
t m :: Map String JType
m -> Int -> JType -> TMonad ()
occursCheck Int
ref JType
t TMonad () -> TMonad () -> TMonad ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
(JType -> TMonad ()) -> Map String JType -> TMonad ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Monad f) =>
(a -> f b) -> t a -> f ()
F.mapM_ (Int -> JType -> TMonad ()
occursCheck Int
ref) Map String JType
m TMonad () -> TMonad () -> TMonad ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
Either (Map String JType, JType) (Map String JType, JType)
-> TMonad ()
addRecConstraint ((Map String JType, JType)
-> Either (Map String JType, JType) (Map String JType, JType)
forall a b. a -> Either a b
Left (Map String JType
m,JType
t))
JTList t' :: JType
t' -> do
VarRef
vr' <- TMonad VarRef
newVarRef
VarRef -> Constraint -> TMonad ()
addConstraint VarRef
vr' (JType -> Constraint
Sub JType
t')
VarRef -> JType -> TMonad ()
instantiateVarRef VarRef
vr (JType -> JType
JTList (VarRef -> JType
JTFree VarRef
vr'))
JTMap t' :: JType
t' -> do
VarRef
vr' <- TMonad VarRef
newVarRef
VarRef -> Constraint -> TMonad ()
addConstraint VarRef
vr' (JType -> Constraint
Sub JType
t')
VarRef -> JType -> TMonad ()
instantiateVarRef VarRef
vr (JType -> JType
JTMap (VarRef -> JType
JTFree VarRef
vr'))
JTRigid _ cs :: Set Constraint
cs -> do
(subs :: [JType]
subs,sups :: [JType]
sups) <- [Constraint] -> ([JType], [JType])
partitionCs ([Constraint] -> ([JType], [JType]))
-> TMonad [Constraint] -> TMonad ([JType], [JType])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VarRef -> TMonad [Constraint]
lookupConstraintsList VarRef
vr
let (subs1 :: [JType]
subs1,sups1 :: [JType]
sups1) = [Constraint] -> ([JType], [JType])
partitionCs ([Constraint] -> ([JType], [JType]))
-> [Constraint] -> ([JType], [JType])
forall a b. (a -> b) -> a -> b
$ Set Constraint -> [Constraint]
forall a. Set a -> [a]
S.toList Set Constraint
cs
Bool -> TMonad () -> TMonad ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (([JType] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [JType]
sups1 Bool -> Bool -> Bool
&& (Bool -> Bool
not (Bool -> Bool) -> ([JType] -> Bool) -> [JType] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [JType] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [JType]
sups) Bool -> Bool -> Bool
||
([JType] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [JType]
subs1 Bool -> Bool -> Bool
&& (Bool -> Bool
not (Bool -> Bool) -> ([JType] -> Bool) -> [JType] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [JType] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [JType]
subs)) (TMonad () -> TMonad ()) -> TMonad () -> TMonad ()
forall a b. (a -> b) -> a -> b
$ JType -> JType -> TMonad ()
forall a. JType -> JType -> TMonad a
tyErr2Sub (VarRef -> JType
JTFree VarRef
vr) JType
t
((JType, JType) -> TMonad ()) -> [(JType, JType)] -> TMonad ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Monad f) =>
(a -> f b) -> t a -> f ()
mapM_ ((JType -> JType -> TMonad ()) -> (JType, JType) -> TMonad ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry JType -> JType -> TMonad ()
(<:)) [(JType
x,JType
y) | JType
x <- [JType]
subs, JType
y <- [JType]
subs1]
((JType, JType) -> TMonad ()) -> [(JType, JType)] -> TMonad ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Monad f) =>
(a -> f b) -> t a -> f ()
mapM_ ((JType -> JType -> TMonad ()) -> (JType, JType) -> TMonad ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry JType -> JType -> TMonad ()
(<:)) [(JType
y,JType
x) | JType
x <- [JType]
sups, JType
y <- [JType]
sups1]
(TCState -> TCState) -> TMonad ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\s :: TCState
s -> TCState
s {tc_vars :: Map Int StoreVal
tc_vars = Int -> StoreVal -> Map Int StoreVal -> Map Int StoreVal
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Int
ref (JType -> StoreVal
SVType JType
t) (TCState -> Map Int StoreVal
tc_vars TCState
s)})
_ -> VarRef -> JType -> TMonad ()
instantiateVarRef VarRef
vr JType
t
Super t :: JType
t -> case JType
t of
JTFree _ -> Constraint -> TMonad ()
addC Constraint
c
JTForall vars :: [VarRef]
vars t :: JType
t -> [Constraint] -> TMonad ()
normalizeConstraints ([Constraint] -> TMonad ())
-> ([Constraint] -> [Constraint]) -> [Constraint] -> TMonad ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Constraint
c Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
: ) ([Constraint] -> TMonad ()) -> TMonad [Constraint] -> TMonad ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< VarRef -> TMonad [Constraint]
lookupConstraintsList VarRef
vr
JTFunc args :: [JType]
args res :: JType
res -> do
(JType -> TMonad ()) -> [JType] -> TMonad ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Monad f) =>
(a -> f b) -> t a -> f ()
mapM_ (Int -> JType -> TMonad ()
occursCheck Int
ref) (JType
resJType -> [JType] -> [JType]
forall a. a -> [a] -> [a]
:[JType]
args)
[Constraint] -> TMonad ()
normalizeConstraints ([Constraint] -> TMonad ())
-> ([Constraint] -> [Constraint]) -> [Constraint] -> TMonad ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Constraint
c Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
:) ([Constraint] -> TMonad ()) -> TMonad [Constraint] -> TMonad ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< VarRef -> TMonad [Constraint]
lookupConstraintsList VarRef
vr
JTRecord t :: JType
t m :: Map String JType
m -> Int -> JType -> TMonad ()
occursCheck Int
ref JType
t TMonad () -> TMonad () -> TMonad ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
(JType -> TMonad ()) -> Map String JType -> TMonad ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Monad f) =>
(a -> f b) -> t a -> f ()
F.mapM_ (Int -> JType -> TMonad ()
occursCheck Int
ref) Map String JType
m TMonad () -> TMonad () -> TMonad ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
Either (Map String JType, JType) (Map String JType, JType)
-> TMonad ()
addRecConstraint ((Map String JType, JType)
-> Either (Map String JType, JType) (Map String JType, JType)
forall a b. b -> Either a b
Right (Map String JType
m,JType
t))
JTList t' :: JType
t' -> do
VarRef
vr' <- TMonad VarRef
newVarRef
VarRef -> Constraint -> TMonad ()
addConstraint VarRef
vr' (JType -> Constraint
Super JType
t')
VarRef -> JType -> TMonad ()
instantiateVarRef VarRef
vr (JType -> JType
JTList (VarRef -> JType
JTFree VarRef
vr'))
JTMap t' :: JType
t' -> do
VarRef
vr' <- TMonad VarRef
newVarRef
VarRef -> Constraint -> TMonad ()
addConstraint VarRef
vr' (JType -> Constraint
Super JType
t')
VarRef -> JType -> TMonad ()
instantiateVarRef VarRef
vr (JType -> JType
JTMap (VarRef -> JType
JTFree VarRef
vr'))
JTRigid _ cs :: Set Constraint
cs -> do
(subs :: [JType]
subs,sups :: [JType]
sups) <- [Constraint] -> ([JType], [JType])
partitionCs ([Constraint] -> ([JType], [JType]))
-> TMonad [Constraint] -> TMonad ([JType], [JType])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VarRef -> TMonad [Constraint]
lookupConstraintsList VarRef
vr
let (subs1 :: [JType]
subs1,sups1 :: [JType]
sups1) = [Constraint] -> ([JType], [JType])
partitionCs ([Constraint] -> ([JType], [JType]))
-> [Constraint] -> ([JType], [JType])
forall a b. (a -> b) -> a -> b
$ Set Constraint -> [Constraint]
forall a. Set a -> [a]
S.toList Set Constraint
cs
Bool -> TMonad () -> TMonad ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (([JType] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [JType]
sups1 Bool -> Bool -> Bool
&& (Bool -> Bool
not (Bool -> Bool) -> ([JType] -> Bool) -> [JType] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [JType] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [JType]
sups) Bool -> Bool -> Bool
||
([JType] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [JType]
subs1 Bool -> Bool -> Bool
&& (Bool -> Bool
not (Bool -> Bool) -> ([JType] -> Bool) -> [JType] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [JType] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [JType]
subs)) (TMonad () -> TMonad ()) -> TMonad () -> TMonad ()
forall a b. (a -> b) -> a -> b
$ JType -> JType -> TMonad ()
forall a. JType -> JType -> TMonad a
tyErr2Sub (VarRef -> JType
JTFree VarRef
vr) JType
t
((JType, JType) -> TMonad ()) -> [(JType, JType)] -> TMonad ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Monad f) =>
(a -> f b) -> t a -> f ()
mapM_ ((JType -> JType -> TMonad ()) -> (JType, JType) -> TMonad ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry JType -> JType -> TMonad ()
(<:)) [(JType
y,JType
x) | JType
x <- [JType]
subs, JType
y <- [JType]
subs1]
((JType, JType) -> TMonad ()) -> [(JType, JType)] -> TMonad ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Monad f) =>
(a -> f b) -> t a -> f ()
mapM_ ((JType -> JType -> TMonad ()) -> (JType, JType) -> TMonad ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry JType -> JType -> TMonad ()
(<:)) [(JType
x,JType
y) | JType
x <- [JType]
sups, JType
y <- [JType]
sups1]
(TCState -> TCState) -> TMonad ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\s :: TCState
s -> TCState
s {tc_vars :: Map Int StoreVal
tc_vars = Int -> StoreVal -> Map Int StoreVal -> Map Int StoreVal
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Int
ref (JType -> StoreVal
SVType JType
t) (TCState -> Map Int StoreVal
tc_vars TCState
s)})
_ -> VarRef -> JType -> TMonad ()
instantiateVarRef VarRef
vr JType
t
where
putCs :: [Constraint] -> m ()
putCs cs :: [Constraint]
cs =
(TCState -> TCState) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\s :: TCState
s -> TCState
s {tc_vars :: Map Int StoreVal
tc_vars = Int -> StoreVal -> Map Int StoreVal -> Map Int StoreVal
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Int
ref (Set Constraint -> StoreVal
SVConstrained (Set Constraint -> StoreVal) -> Set Constraint -> StoreVal
forall a b. (a -> b) -> a -> b
$ [Constraint] -> Set Constraint
forall a. Ord a => [a] -> Set a
S.fromList ([Constraint] -> Set Constraint) -> [Constraint] -> Set Constraint
forall a b. (a -> b) -> a -> b
$ [Constraint]
cs) (TCState -> Map Int StoreVal
tc_vars TCState
s)})
addC :: Constraint -> TMonad ()
addC constraint :: Constraint
constraint = do
[Constraint]
cs <- VarRef -> TMonad [Constraint]
lookupConstraintsList VarRef
vr
(TCState -> TCState) -> TMonad ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\s :: TCState
s -> TCState
s {tc_vars :: Map Int StoreVal
tc_vars = Int -> StoreVal -> Map Int StoreVal -> Map Int StoreVal
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Int
ref (Set Constraint -> StoreVal
SVConstrained ([Constraint] -> Set Constraint
forall a. Ord a => [a] -> Set a
S.fromList ([Constraint] -> Set Constraint) -> [Constraint] -> Set Constraint
forall a b. (a -> b) -> a -> b
$ Constraint
constraintConstraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
:[Constraint]
cs)) (TCState -> Map Int StoreVal
tc_vars TCState
s)})
findRecordSubs :: [Constraint] -> ([(Map String JType, JType)], [Constraint])
findRecordSubs cs :: [Constraint]
cs = (Constraint -> Maybe (Map String JType, JType))
-> [Constraint] -> ([(Map String JType, JType)], [Constraint])
forall a b. (a -> Maybe b) -> [a] -> ([b], [a])
partitionOut Constraint -> Maybe (Map String JType, JType)
go [Constraint]
cs
where go :: Constraint -> Maybe (Map String JType, JType)
go (Sub (JTRecord t :: JType
t m :: Map String JType
m)) = (Map String JType, JType) -> Maybe (Map String JType, JType)
forall a. a -> Maybe a
Just (Map String JType
m,JType
t)
go _ = Maybe (Map String JType, JType)
forall a. Maybe a
Nothing
findRecordSups :: [Constraint] -> ([(Map String JType, JType)], [Constraint])
findRecordSups cs :: [Constraint]
cs = (Constraint -> Maybe (Map String JType, JType))
-> [Constraint] -> ([(Map String JType, JType)], [Constraint])
forall a b. (a -> Maybe b) -> [a] -> ([b], [a])
partitionOut Constraint -> Maybe (Map String JType, JType)
go [Constraint]
cs
where go :: Constraint -> Maybe (Map String JType, JType)
go (Super (JTRecord t :: JType
t m :: Map String JType
m)) = (Map String JType, JType) -> Maybe (Map String JType, JType)
forall a. a -> Maybe a
Just (Map String JType
m,JType
t)
go _ = Maybe (Map String JType, JType)
forall a. Maybe a
Nothing
addRecConstraint :: Either (Map String JType, JType) (Map String JType, JType)
-> TMonad ()
addRecConstraint eM :: Either (Map String JType, JType) (Map String JType, JType)
eM = do
(subs :: [(Map String JType, JType)]
subs,restCs :: [Constraint]
restCs) <- [Constraint] -> ([(Map String JType, JType)], [Constraint])
findRecordSubs ([Constraint] -> ([(Map String JType, JType)], [Constraint]))
-> TMonad [Constraint]
-> TMonad ([(Map String JType, JType)], [Constraint])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VarRef -> TMonad [Constraint]
lookupConstraintsList VarRef
vr
let (sups :: [(Map String JType, JType)]
sups,restCs' :: [Constraint]
restCs') = [Constraint] -> ([(Map String JType, JType)], [Constraint])
findRecordSups [Constraint]
restCs
mergeSubs :: [(Map key JType, JType)] -> TMonad (Maybe (Map key JType, JType))
mergeSubs [] = Maybe (Map key JType, JType)
-> TMonad (Maybe (Map key JType, JType))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Map key JType, JType)
forall a. Maybe a
Nothing
mergeSubs [m :: (Map key JType, JType)
m] = Maybe (Map key JType, JType)
-> TMonad (Maybe (Map key JType, JType))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Map key JType, JType)
-> TMonad (Maybe (Map key JType, JType)))
-> Maybe (Map key JType, JType)
-> TMonad (Maybe (Map key JType, JType))
forall a b. (a -> b) -> a -> b
$ (Map key JType, JType) -> Maybe (Map key JType, JType)
forall a. a -> Maybe a
Just (Map key JType, JType)
m
mergeSubs (m :: (Map key JType, JType)
m:ms :: [(Map key JType, JType)]
ms) = (Map key JType, JType) -> Maybe (Map key JType, JType)
forall a. a -> Maybe a
Just ((Map key JType, JType) -> Maybe (Map key JType, JType))
-> TMonad (Map key JType, JType)
-> TMonad (Maybe (Map key JType, JType))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Map key JType, JType)
-> (Map key JType, JType) -> TMonad (Map key JType, JType))
-> (Map key JType, JType)
-> [(Map key JType, JType)]
-> TMonad (Map key JType, JType)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\(mp :: Map key JType
mp,t :: JType
t) (mp' :: Map key JType
mp',t' :: JType
t') -> do
Map key JType
mp'' <- (JType -> JType -> TMonad JType)
-> Map key JType -> Map key JType -> TMonad (Map key JType)
forall (m :: * -> *) key val.
(Monad m, Ord key) =>
(val -> val -> m val)
-> Map key val -> Map key val -> m (Map key val)
unionWithM (\x :: JType
x y :: JType
y -> [JType] -> TMonad JType
someLowerBound [JType
x,JType
y]) Map key JType
mp Map key JType
mp'
JType
t'' <- [JType] -> TMonad JType
someLowerBound [JType
t,JType
t']
(Map key JType, JType) -> TMonad (Map key JType, JType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map key JType
mp'',JType
t'')
) (Map key JType, JType)
m [(Map key JType, JType)]
ms
mergeSups :: [(Map key JType, JType)] -> TMonad (Maybe (Map key JType, JType))
mergeSups [] = Maybe (Map key JType, JType)
-> TMonad (Maybe (Map key JType, JType))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Map key JType, JType)
forall a. Maybe a
Nothing
mergeSups [m :: (Map key JType, JType)
m] = Maybe (Map key JType, JType)
-> TMonad (Maybe (Map key JType, JType))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Map key JType, JType)
-> TMonad (Maybe (Map key JType, JType)))
-> Maybe (Map key JType, JType)
-> TMonad (Maybe (Map key JType, JType))
forall a b. (a -> b) -> a -> b
$ (Map key JType, JType) -> Maybe (Map key JType, JType)
forall a. a -> Maybe a
Just (Map key JType, JType)
m
mergeSups (m :: (Map key JType, JType)
m:ms :: [(Map key JType, JType)]
ms) = (Map key JType, JType) -> Maybe (Map key JType, JType)
forall a. a -> Maybe a
Just ((Map key JType, JType) -> Maybe (Map key JType, JType))
-> TMonad (Map key JType, JType)
-> TMonad (Maybe (Map key JType, JType))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Map key JType, JType)
-> (Map key JType, JType) -> TMonad (Map key JType, JType))
-> (Map key JType, JType)
-> [(Map key JType, JType)]
-> TMonad (Map key JType, JType)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\(mp :: Map key JType
mp,t :: JType
t) (mp' :: Map key JType
mp',t' :: JType
t') -> do
Map key JType
mp'' <- (JType -> JType -> TMonad JType)
-> Map key JType -> Map key JType -> TMonad (Map key JType)
forall (m :: * -> *) key val b.
(Monad m, Ord key) =>
(val -> val -> m b) -> Map key val -> Map key val -> m (Map key b)
intersectionWithM (\x :: JType
x y :: JType
y -> [JType] -> TMonad JType
someUpperBound [JType
x,JType
y]) Map key JType
mp Map key JType
mp'
JType
t'' <- [JType] -> TMonad JType
someUpperBound [JType
t,JType
t']
(Map key JType, JType) -> TMonad (Map key JType, JType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map key JType
mp'',JType
t'')
) (Map key JType, JType)
m [(Map key JType, JType)]
ms
Maybe (Map String JType, JType)
mbSub <- [(Map String JType, JType)]
-> TMonad (Maybe (Map String JType, JType))
forall key.
Ord key =>
[(Map key JType, JType)] -> TMonad (Maybe (Map key JType, JType))
mergeSubs ([(Map String JType, JType)]
-> TMonad (Maybe (Map String JType, JType)))
-> [(Map String JType, JType)]
-> TMonad (Maybe (Map String JType, JType))
forall a b. (a -> b) -> a -> b
$ case Either (Map String JType, JType) (Map String JType, JType)
eM of
Left mt :: (Map String JType, JType)
mt -> (Map String JType, JType)
mt (Map String JType, JType)
-> [(Map String JType, JType)] -> [(Map String JType, JType)]
forall a. a -> [a] -> [a]
: [(Map String JType, JType)]
subs
_ -> [(Map String JType, JType)]
subs
Maybe (Map String JType, JType)
mbSup <- [(Map String JType, JType)]
-> TMonad (Maybe (Map String JType, JType))
forall key.
Ord key =>
[(Map key JType, JType)] -> TMonad (Maybe (Map key JType, JType))
mergeSups ([(Map String JType, JType)]
-> TMonad (Maybe (Map String JType, JType)))
-> [(Map String JType, JType)]
-> TMonad (Maybe (Map String JType, JType))
forall a b. (a -> b) -> a -> b
$ case Either (Map String JType, JType) (Map String JType, JType)
eM of
Right mt :: (Map String JType, JType)
mt -> (Map String JType, JType)
mt (Map String JType, JType)
-> [(Map String JType, JType)] -> [(Map String JType, JType)]
forall a. a -> [a] -> [a]
: [(Map String JType, JType)]
sups
_ -> [(Map String JType, JType)]
sups
[Constraint] -> TMonad ()
normalizeConstraints ([Constraint] -> TMonad ()) -> TMonad [Constraint] -> TMonad ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< case (Maybe (Map String JType, JType)
mbSub, Maybe (Map String JType, JType)
mbSup) of
(Just (subm :: Map String JType
subm,subt :: JType
subt), Just (supm :: Map String JType
supm,supt :: JType
supt)) -> do
Bool -> TMonad () -> TMonad ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (JType -> JType -> Bool)
-> Map String JType -> Map String JType -> Bool
forall k a b.
Ord k =>
(a -> b -> Bool) -> Map k a -> Map k b -> Bool
M.isSubmapOfBy (\_ _ -> Bool
True) Map String JType
subm Map String JType
supm) (TMonad () -> TMonad ()) -> TMonad () -> TMonad ()
forall a b. (a -> b) -> a -> b
$ String -> String -> String -> JType -> JType -> TMonad ()
forall a. String -> String -> String -> JType -> JType -> TMonad a
tyErr2ext "Incompatible constraints" "Subtype constraint" "Supertype constraint" (JType -> Map String JType -> JType
JTRecord JType
subt Map String JType
subm) (JType -> Map String JType -> JType
JTRecord JType
supt Map String JType
supm)
Map String ()
_ <- (JType -> JType -> TMonad ())
-> Map String JType -> Map String JType -> TMonad (Map String ())
forall (m :: * -> *) key val b.
(Monad m, Ord key) =>
(val -> val -> m b) -> Map key val -> Map key val -> m (Map key b)
intersectionWithM (\x :: JType
x y :: JType
y -> JType
y JType -> JType -> TMonad ()
<: JType
x) Map String JType
subm Map String JType
supm
()
_ <- JType
supt JType -> JType -> TMonad ()
<: JType
subt
[Constraint] -> TMonad [Constraint]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Constraint] -> TMonad [Constraint])
-> [Constraint] -> TMonad [Constraint]
forall a b. (a -> b) -> a -> b
$ JType -> Constraint
Sub (JType -> Map String JType -> JType
JTRecord JType
subt Map String JType
subm) Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
: JType -> Constraint
Super (JType -> Map String JType -> JType
JTRecord JType
supt Map String JType
supm) Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
: [Constraint]
restCs'
(Just (subm :: Map String JType
subm,subt :: JType
subt), Nothing) -> [Constraint] -> TMonad [Constraint]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Constraint] -> TMonad [Constraint])
-> [Constraint] -> TMonad [Constraint]
forall a b. (a -> b) -> a -> b
$ JType -> Constraint
Sub (JType -> Map String JType -> JType
JTRecord JType
subt Map String JType
subm) Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
: [Constraint]
restCs'
(Nothing , Just (supm :: Map String JType
supm,supt :: JType
supt)) -> [Constraint] -> TMonad [Constraint]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Constraint] -> TMonad [Constraint])
-> [Constraint] -> TMonad [Constraint]
forall a b. (a -> b) -> a -> b
$ JType -> Constraint
Super (JType -> Map String JType -> JType
JTRecord JType
supt Map String JType
supm) Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
: [Constraint]
restCs'
_ -> [Constraint] -> TMonad [Constraint]
forall (m :: * -> *) a. Monad m => a -> m a
return [Constraint]
restCs'
normalizeConstraints :: [Constraint] -> TMonad ()
normalizeConstraints cl :: [Constraint]
cl = [Constraint] -> TMonad ()
forall (m :: * -> *). MonadState TCState m => [Constraint] -> m ()
putCs ([Constraint] -> TMonad ()) -> TMonad [Constraint] -> TMonad ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Constraint] -> TMonad [Constraint]
cannonicalizeConstraints [Constraint]
cl
cannonicalizeConstraints :: [Constraint] -> TMonad [Constraint]
cannonicalizeConstraints :: [Constraint] -> TMonad [Constraint]
cannonicalizeConstraints constraintList :: [Constraint]
constraintList = do
let (subs :: [([VarRef], JType)]
subs,restCs :: [Constraint]
restCs) = [Constraint] -> ([([VarRef], JType)], [Constraint])
findForallSubs [Constraint]
constraintList
(sups :: [([VarRef], JType)]
sups,restCs' :: [Constraint]
restCs') = [Constraint] -> ([([VarRef], JType)], [Constraint])
findForallSups [Constraint]
restCs
Maybe JType
mbSub <- [([VarRef], JType)] -> TMonad (Maybe JType)
mergeSubs [([VarRef], JType)]
subs
Maybe JType
mbSup <- [([VarRef], JType)] -> TMonad (Maybe JType)
mergeSups [([VarRef], JType)]
sups
case (Maybe JType
mbSub, Maybe JType
mbSup) of
(Just sub :: JType
sub, Just sup :: JType
sup) -> do
JType
sup JType -> JType -> TMonad ()
<: JType
sub
[Constraint] -> TMonad [Constraint]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Constraint] -> TMonad [Constraint])
-> [Constraint] -> TMonad [Constraint]
forall a b. (a -> b) -> a -> b
$ JType -> Constraint
Sub JType
sub Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
: JType -> Constraint
Super JType
sup Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
: [Constraint]
restCs'
(Just sub :: JType
sub, Nothing) -> [Constraint] -> TMonad [Constraint]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Constraint] -> TMonad [Constraint])
-> [Constraint] -> TMonad [Constraint]
forall a b. (a -> b) -> a -> b
$ JType -> Constraint
Sub JType
sub Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
: [Constraint]
restCs'
(Nothing , Just sup :: JType
sup) -> [Constraint] -> TMonad [Constraint]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Constraint] -> TMonad [Constraint])
-> [Constraint] -> TMonad [Constraint]
forall a b. (a -> b) -> a -> b
$ JType -> Constraint
Super JType
sup Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
: [Constraint]
restCs'
_ -> [Constraint] -> TMonad [Constraint]
forall (m :: * -> *) a. Monad m => a -> m a
return [Constraint]
restCs'
where
findForallSubs :: [Constraint] -> ([([VarRef], JType)], [Constraint])
findForallSubs cs :: [Constraint]
cs = (Constraint -> Maybe ([VarRef], JType))
-> [Constraint] -> ([([VarRef], JType)], [Constraint])
forall a b. (a -> Maybe b) -> [a] -> ([b], [a])
partitionOut Constraint -> Maybe ([VarRef], JType)
go [Constraint]
cs
where go :: Constraint -> Maybe ([VarRef], JType)
go (Sub (JTForall vars :: [VarRef]
vars t :: JType
t)) = ([VarRef], JType) -> Maybe ([VarRef], JType)
forall a. a -> Maybe a
Just ([VarRef]
vars,JType
t)
go (Sub (JTFree _)) = Maybe ([VarRef], JType)
forall a. Maybe a
Nothing
go (Sub x :: JType
x) = ([VarRef], JType) -> Maybe ([VarRef], JType)
forall a. a -> Maybe a
Just ([],JType
x)
go _ = Maybe ([VarRef], JType)
forall a. Maybe a
Nothing
findForallSups :: [Constraint] -> ([([VarRef], JType)], [Constraint])
findForallSups cs :: [Constraint]
cs = (Constraint -> Maybe ([VarRef], JType))
-> [Constraint] -> ([([VarRef], JType)], [Constraint])
forall a b. (a -> Maybe b) -> [a] -> ([b], [a])
partitionOut Constraint -> Maybe ([VarRef], JType)
go [Constraint]
cs
where go :: Constraint -> Maybe ([VarRef], JType)
go (Super (JTForall vars :: [VarRef]
vars t :: JType
t)) = ([VarRef], JType) -> Maybe ([VarRef], JType)
forall a. a -> Maybe a
Just ([VarRef]
vars,JType
t)
go (Super (JTFree _)) = Maybe ([VarRef], JType)
forall a. Maybe a
Nothing
go (Super x :: JType
x) = ([VarRef], JType) -> Maybe ([VarRef], JType)
forall a. a -> Maybe a
Just ([],JType
x)
go _ = Maybe ([VarRef], JType)
forall a. Maybe a
Nothing
findFuncs :: [JType] -> ([([JType], JType)], [JType])
findFuncs cs :: [JType]
cs = (JType -> Maybe ([JType], JType))
-> [JType] -> ([([JType], JType)], [JType])
forall a b. (a -> Maybe b) -> [a] -> ([b], [a])
partitionOut JType -> Maybe ([JType], JType)
go [JType]
cs
where go :: JType -> Maybe ([JType], JType)
go (JTFunc args :: [JType]
args ret :: JType
ret) = ([JType], JType) -> Maybe ([JType], JType)
forall a. a -> Maybe a
Just ([JType]
args, JType
ret)
go _ = Maybe ([JType], JType)
forall a. Maybe a
Nothing
mergeSubs :: [([VarRef], JType)] -> TMonad (Maybe JType)
mergeSubs [] = Maybe JType -> TMonad (Maybe JType)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe JType
forall a. Maybe a
Nothing
mergeSubs [([],t :: JType
t)] = Maybe JType -> TMonad (Maybe JType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe JType -> TMonad (Maybe JType))
-> Maybe JType -> TMonad (Maybe JType)
forall a b. (a -> b) -> a -> b
$ JType -> Maybe JType
forall a. a -> Maybe a
Just (JType -> Maybe JType) -> JType -> Maybe JType
forall a b. (a -> b) -> a -> b
$ JType
t
mergeSubs [s :: ([VarRef], JType)
s] = Maybe JType -> TMonad (Maybe JType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe JType -> TMonad (Maybe JType))
-> Maybe JType -> TMonad (Maybe JType)
forall a b. (a -> b) -> a -> b
$ JType -> Maybe JType
forall a. a -> Maybe a
Just (JType -> Maybe JType) -> JType -> Maybe JType
forall a b. (a -> b) -> a -> b
$ ([VarRef] -> JType -> JType) -> ([VarRef], JType) -> JType
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [VarRef] -> JType -> JType
JTForall ([VarRef], JType)
s
mergeSubs ss :: [([VarRef], JType)]
ss = do
JType
rt <- TMonad JType
newTyVar
(_,frame :: Set Int
frame) <- TMonad () -> TMonad ((), Set Int)
forall a. TMonad a -> TMonad (a, Set Int)
withLocalScope (TMonad () -> TMonad ((), Set Int))
-> TMonad () -> TMonad ((), Set Int)
forall a b. (a -> b) -> a -> b
$ do
[JType]
instantiatedTypes <- (([VarRef], JType) -> TMonad JType)
-> [([VarRef], JType)] -> TMonad [JType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (([VarRef] -> JType -> TMonad JType)
-> ([VarRef], JType) -> TMonad JType
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [VarRef] -> JType -> TMonad JType
instantiateScheme) [([VarRef], JType)]
ss
let (funcTypes :: [([JType], JType)]
funcTypes, otherTypes :: [JType]
otherTypes) = [JType] -> ([([JType], JType)], [JType])
findFuncs [JType]
instantiatedTypes
Bool -> TMonad () -> TMonad ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (Bool -> Bool)
-> ([([JType], JType)] -> Bool) -> [([JType], JType)] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [([JType], JType)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([([JType], JType)] -> Bool) -> [([JType], JType)] -> Bool
forall a b. (a -> b) -> a -> b
$ [([JType], JType)]
funcTypes) (TMonad () -> TMonad ()) -> TMonad () -> TMonad ()
forall a b. (a -> b) -> a -> b
$ do
let (argss :: [[JType]]
argss,rets :: [JType]
rets) = [([JType], JType)] -> ([[JType]], [JType])
forall a b. [(a, b)] -> ([a], [b])
unzip [([JType], JType)]
funcTypes
lft :: Int
lft = [([JType], JType)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [([JType], JType)]
funcTypes
[JType]
args' <- ([JType] -> TMonad JType) -> [[JType]] -> TMonad [JType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM [JType] -> TMonad JType
someUpperBound ([[JType]] -> TMonad [JType]) -> [[JType]] -> TMonad [JType]
forall a b. (a -> b) -> a -> b
$ ([JType] -> Bool) -> [[JType]] -> [[JType]]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
lft) (Int -> Bool) -> ([JType] -> Int) -> [JType] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [JType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length) ([[JType]] -> [[JType]]) -> [[JType]] -> [[JType]]
forall a b. (a -> b) -> a -> b
$ [[JType]] -> [[JType]]
forall a. [[a]] -> [[a]]
transpose [[JType]]
argss
JType
ret' <- [JType] -> TMonad JType
someLowerBound [JType]
rets
JType
rt JType -> JType -> TMonad ()
<: [JType] -> JType -> JType
JTFunc [JType]
args' JType
ret'
(JType -> TMonad ()) -> [JType] -> TMonad ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Monad f) =>
(a -> f b) -> t a -> f ()
mapM_ (JType
rt JType -> JType -> TMonad ()
<:) [JType]
otherTypes
JType
rt' <- JType -> TMonad JType
resolveType JType
rt
case JType
rt' of
(JTFunc args :: [JType]
args res :: JType
res) -> do
Set Int
freeVarsInArgs <- [Set Int] -> Set Int
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ([Set Int] -> Set Int) -> TMonad [Set Int] -> TMonad (Set Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (JType -> TMonad (Set Int)) -> [JType] -> TMonad [Set Int]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM JType -> TMonad (Set Int)
freeVars [JType]
args
Set Int
freeVarsInRes <- JType -> TMonad (Set Int)
freeVars JType
res
Set Int -> TMonad ()
setFrozen (Set Int -> TMonad ()) -> Set Int -> TMonad ()
forall a b. (a -> b) -> a -> b
$ Set Int
frame Set Int -> Set Int -> Set Int
forall a. Ord a => Set a -> Set a -> Set a
`S.difference` (Set Int
freeVarsInArgs Set Int -> Set Int -> Set Int
forall a. Ord a => Set a -> Set a -> Set a
`S.intersection` Set Int
freeVarsInRes)
_ -> Set Int -> TMonad ()
setFrozen Set Int
frame
JType -> Maybe JType
forall a. a -> Maybe a
Just (JType -> Maybe JType) -> TMonad JType -> TMonad (Maybe JType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> JType -> TMonad JType
resolveType ([VarRef] -> JType -> JType
JTForall (Set Int -> [VarRef]
forall t a. Set t -> [(Maybe a, t)]
frame2VarRefs Set Int
frame) JType
rt')
mergeSups :: [([VarRef], JType)] -> TMonad (Maybe JType)
mergeSups [] = Maybe JType -> TMonad (Maybe JType)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe JType
forall a. Maybe a
Nothing
mergeSups [([],t :: JType
t)] = Maybe JType -> TMonad (Maybe JType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe JType -> TMonad (Maybe JType))
-> Maybe JType -> TMonad (Maybe JType)
forall a b. (a -> b) -> a -> b
$ JType -> Maybe JType
forall a. a -> Maybe a
Just (JType -> Maybe JType) -> JType -> Maybe JType
forall a b. (a -> b) -> a -> b
$ JType
t
mergeSups [s :: ([VarRef], JType)
s] = Maybe JType -> TMonad (Maybe JType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe JType -> TMonad (Maybe JType))
-> Maybe JType -> TMonad (Maybe JType)
forall a b. (a -> b) -> a -> b
$ JType -> Maybe JType
forall a. a -> Maybe a
Just (JType -> Maybe JType) -> JType -> Maybe JType
forall a b. (a -> b) -> a -> b
$ ([VarRef] -> JType -> JType) -> ([VarRef], JType) -> JType
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [VarRef] -> JType -> JType
JTForall ([VarRef], JType)
s
mergeSups ss :: [([VarRef], JType)]
ss = do
JType
rt <- TMonad JType
newTyVar
(_,frame :: Set Int
frame) <- TMonad () -> TMonad ((), Set Int)
forall a. TMonad a -> TMonad (a, Set Int)
withLocalScope (TMonad () -> TMonad ((), Set Int))
-> TMonad () -> TMonad ((), Set Int)
forall a b. (a -> b) -> a -> b
$ do
[JType]
instantiatedTypes <- (([VarRef], JType) -> TMonad JType)
-> [([VarRef], JType)] -> TMonad [JType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (([VarRef] -> JType -> TMonad JType)
-> ([VarRef], JType) -> TMonad JType
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [VarRef] -> JType -> TMonad JType
instantiateScheme) [([VarRef], JType)]
ss
let (funcTypes :: [([JType], JType)]
funcTypes, otherTypes :: [JType]
otherTypes) = [JType] -> ([([JType], JType)], [JType])
findFuncs [JType]
instantiatedTypes
Bool -> TMonad () -> TMonad ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (Bool -> Bool)
-> ([([JType], JType)] -> Bool) -> [([JType], JType)] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [([JType], JType)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([([JType], JType)] -> Bool) -> [([JType], JType)] -> Bool
forall a b. (a -> b) -> a -> b
$ [([JType], JType)]
funcTypes) (TMonad () -> TMonad ()) -> TMonad () -> TMonad ()
forall a b. (a -> b) -> a -> b
$ do
let (argss :: [[JType]]
argss,rets :: [JType]
rets) = [([JType], JType)] -> ([[JType]], [JType])
forall a b. [(a, b)] -> ([a], [b])
unzip [([JType], JType)]
funcTypes
[JType]
args' <- ([JType] -> TMonad JType) -> [[JType]] -> TMonad [JType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM [JType] -> TMonad JType
someLowerBound ([[JType]] -> TMonad [JType]) -> [[JType]] -> TMonad [JType]
forall a b. (a -> b) -> a -> b
$ [[JType]] -> [[JType]]
forall a. [[a]] -> [[a]]
transpose [[JType]]
argss
JType
ret' <- [JType] -> TMonad JType
someUpperBound [JType]
rets
JType
rt JType -> JType -> TMonad ()
<: [JType] -> JType -> JType
JTFunc [JType]
args' JType
ret'
(JType -> TMonad ()) -> [JType] -> TMonad ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Monad f) =>
(a -> f b) -> t a -> f ()
mapM_ (JType -> JType -> TMonad ()
<: JType
rt) [JType]
otherTypes
JType
rt' <- JType -> TMonad JType
resolveType JType
rt
case JType
rt' of
(JTFunc args :: [JType]
args res :: JType
res) -> do
Set Int
freeVarsInArgs <- [Set Int] -> Set Int
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ([Set Int] -> Set Int) -> TMonad [Set Int] -> TMonad (Set Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (JType -> TMonad (Set Int)) -> [JType] -> TMonad [Set Int]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM JType -> TMonad (Set Int)
freeVars [JType]
args
Set Int
freeVarsInRes <- JType -> TMonad (Set Int)
freeVars JType
res
Set Int -> TMonad ()
setFrozen (Set Int -> TMonad ()) -> Set Int -> TMonad ()
forall a b. (a -> b) -> a -> b
$ Set Int
frame Set Int -> Set Int -> Set Int
forall a. Ord a => Set a -> Set a -> Set a
`S.difference` (Set Int
freeVarsInArgs Set Int -> Set Int -> Set Int
forall a. Ord a => Set a -> Set a -> Set a
`S.intersection` Set Int
freeVarsInRes)
_ -> Set Int -> TMonad ()
setFrozen Set Int
frame
JType -> Maybe JType
forall a. a -> Maybe a
Just (JType -> Maybe JType) -> TMonad JType -> TMonad (Maybe JType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> JType -> TMonad JType
resolveType ([VarRef] -> JType -> JType
JTForall (Set Int -> [VarRef]
forall t a. Set t -> [(Maybe a, t)]
frame2VarRefs Set Int
frame) JType
rt')
tryCloseFrozenVars :: TMonad ()
tryCloseFrozenVars :: TMonad ()
tryCloseFrozenVars = ReaderT [Either Int Int] TMonad () -> [Either Int Int] -> TMonad ()
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (Set Int -> ReaderT [Either Int Int] TMonad ()
loop (Set Int -> ReaderT [Either Int Int] TMonad ())
-> (TCState -> Set Int)
-> TCState
-> ReaderT [Either Int Int] TMonad ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCState -> Set Int
tc_frozen (TCState -> ReaderT [Either Int Int] TMonad ())
-> ReaderT [Either Int Int] TMonad TCState
-> ReaderT [Either Int Int] TMonad ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ReaderT [Either Int Int] TMonad TCState
forall s (m :: * -> *). MonadState s m => m s
get) []
where
loop :: Set Int -> ReaderT [Either Int Int] TMonad ()
loop frozen :: Set Int
frozen = do
(Int -> ReaderT [Either Int Int] TMonad ())
-> [Int] -> ReaderT [Either Int Int] TMonad ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Monad f) =>
(a -> f b) -> t a -> f ()
mapM_ Int -> ReaderT [Either Int Int] TMonad ()
go ([Int] -> ReaderT [Either Int Int] TMonad ())
-> [Int] -> ReaderT [Either Int Int] TMonad ()
forall a b. (a -> b) -> a -> b
$ Set Int -> [Int]
forall a. Set a -> [a]
S.toList Set Int
frozen
Set Int
newFrozen <- TCState -> Set Int
tc_frozen (TCState -> Set Int)
-> ReaderT [Either Int Int] TMonad TCState
-> ReaderT [Either Int Int] TMonad (Set Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TMonad TCState -> ReaderT [Either Int Int] TMonad TCState
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TMonad TCState
forall s (m :: * -> *). MonadState s m => m s
get
if Set Int -> Bool
forall a. Set a -> Bool
S.null (Set Int
newFrozen Set Int -> Set Int -> Set Int
forall a. Ord a => Set a -> Set a -> Set a
`S.difference` Set Int
frozen)
then () -> ReaderT [Either Int Int] TMonad ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
else Set Int -> ReaderT [Either Int Int] TMonad ()
loop Set Int
newFrozen
go :: Int -> ReaderT [Either Int Int] TMonad ()
go :: Int -> ReaderT [Either Int Int] TMonad ()
go i :: Int
i = do
[Either Int Int]
s <- ReaderT [Either Int Int] TMonad [Either Int Int]
forall r (m :: * -> *). MonadReader r m => m r
ask
case Int -> [Either Int Int] -> Maybe (Maybe [Int])
forall a. Eq a => a -> [Either a a] -> Maybe (Maybe [a])
findLoop Int
i [Either Int Int]
s of
Just Nothing -> () -> ReaderT [Either Int Int] TMonad ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just (Just vrs :: [Int]
vrs) -> [Int] -> ReaderT [Either Int Int] TMonad ()
unifyGroup [Int]
vrs
Nothing -> do
JType
t <- TMonad JType -> ReaderT [Either Int Int] TMonad JType
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TMonad JType -> ReaderT [Either Int Int] TMonad JType)
-> TMonad JType -> ReaderT [Either Int Int] TMonad JType
forall a b. (a -> b) -> a -> b
$ JType -> TMonad JType
resolveTypeShallow (VarRef -> JType
JTFree (Maybe String
forall a. Maybe a
Nothing, Int
i))
case JType
t of
(JTFree vr :: VarRef
vr) -> do
[Constraint]
l <- VarRef -> ReaderT [Either Int Int] TMonad [Constraint]
tryClose VarRef
vr
case [Constraint]
l of
[] -> () -> ReaderT [Either Int Int] TMonad ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
cl :: [Constraint]
cl -> do
(Constraint -> ReaderT [Either Int Int] TMonad ())
-> [Constraint] -> ReaderT [Either Int Int] TMonad ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Monad f) =>
(a -> f b) -> t a -> f ()
mapM_ (VarRef -> Constraint -> ReaderT [Either Int Int] TMonad ()
forall a.
(a, Int) -> Constraint -> ReaderT [Either Int Int] TMonad ()
go' VarRef
vr) [Constraint]
cl
TMonad () -> ReaderT [Either Int Int] TMonad ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift ((Constraint -> TMonad Constraint) -> [Constraint] -> TMonad ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Monad f) =>
(a -> f b) -> t a -> f ()
mapM_ ((JType -> TMonad JType) -> Constraint -> TMonad Constraint
forall (m :: * -> *).
(Monad m, Functor m) =>
(JType -> m JType) -> Constraint -> m Constraint
mapConstraint JType -> TMonad JType
resolveType) [Constraint]
cl)
_ -> () -> ReaderT [Either Int Int] TMonad ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
go' :: (a, Int) -> Constraint -> ReaderT [Either Int Int] TMonad ()
go' (_,ref :: Int
ref) (Sub (JTFree (_,i :: Int
i)))
| Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ref = () -> ReaderT [Either Int Int] TMonad ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise =
([Either Int Int] -> [Either Int Int])
-> ReaderT [Either Int Int] TMonad ()
-> ReaderT [Either Int Int] TMonad ()
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\s :: [Either Int Int]
s -> Int -> Either Int Int
forall a b. a -> Either a b
Left Int
ref Either Int Int -> [Either Int Int] -> [Either Int Int]
forall a. a -> [a] -> [a]
: [Either Int Int]
s) (ReaderT [Either Int Int] TMonad ()
-> ReaderT [Either Int Int] TMonad ())
-> ReaderT [Either Int Int] TMonad ()
-> ReaderT [Either Int Int] TMonad ()
forall a b. (a -> b) -> a -> b
$ Int -> ReaderT [Either Int Int] TMonad ()
go Int
i
go' (_,ref :: Int
ref) (Super (JTFree (_,i :: Int
i)))
| Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ref = () -> ReaderT [Either Int Int] TMonad ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise =
([Either Int Int] -> [Either Int Int])
-> ReaderT [Either Int Int] TMonad ()
-> ReaderT [Either Int Int] TMonad ()
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\s :: [Either Int Int]
s -> Int -> Either Int Int
forall a b. b -> Either a b
Right Int
ref Either Int Int -> [Either Int Int] -> [Either Int Int]
forall a. a -> [a] -> [a]
: [Either Int Int]
s) (ReaderT [Either Int Int] TMonad ()
-> ReaderT [Either Int Int] TMonad ())
-> ReaderT [Either Int Int] TMonad ()
-> ReaderT [Either Int Int] TMonad ()
forall a b. (a -> b) -> a -> b
$ Int -> ReaderT [Either Int Int] TMonad ()
go Int
i
go' _ _ = () -> ReaderT [Either Int Int] TMonad ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
unifyGroup :: [Int] -> ReaderT [Either Int Int] TMonad ()
unifyGroup :: [Int] -> ReaderT [Either Int Int] TMonad ()
unifyGroup (vr :: Int
vr:vrs :: [Int]
vrs) = TMonad () -> ReaderT [Either Int Int] TMonad ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TMonad () -> ReaderT [Either Int Int] TMonad ())
-> TMonad () -> ReaderT [Either Int Int] TMonad ()
forall a b. (a -> b) -> a -> b
$ (Int -> TMonad ()) -> [Int] -> TMonad ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Monad f) =>
(a -> f b) -> t a -> f ()
mapM_ (\x :: Int
x -> VarRef -> JType -> TMonad ()
instantiateVarRef (Maybe String
forall a. Maybe a
Nothing, Int
x) (VarRef -> JType
JTFree (Maybe String
forall a. Maybe a
Nothing,Int
vr))) [Int]
vrs
unifyGroup [] = () -> ReaderT [Either Int Int] TMonad ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
findLoop :: a -> [Either a a] -> Maybe (Maybe [a])
findLoop i :: a
i cs :: [Either a a]
cs@(c :: Either a a
c:_) = [a] -> [Either a a] -> Maybe (Maybe [a])
go [] [Either a a]
cs
where
cTyp :: Bool
cTyp = Either a a -> Bool
forall a b. Either a b -> Bool
eitherIsLeft Either a a
c
go :: [a] -> [Either a a] -> Maybe (Maybe [a])
go accum :: [a]
accum (r :: Either a a
r:rs :: [Either a a]
rs)
| (a -> a) -> (a -> a) -> Either a a -> a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> a
forall a. a -> a
id a -> a
forall a. a -> a
id Either a a
r a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
i Bool -> Bool -> Bool
&& Either a a -> Bool
forall a b. Either a b -> Bool
eitherIsLeft Either a a
r Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
cTyp = Maybe [a] -> Maybe (Maybe [a])
forall a. a -> Maybe a
Just (Maybe [a] -> Maybe (Maybe [a])) -> Maybe [a] -> Maybe (Maybe [a])
forall a b. (a -> b) -> a -> b
$ [a] -> Maybe [a]
forall a. a -> Maybe a
Just ((a -> a) -> (a -> a) -> Either a a -> a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> a
forall a. a -> a
id a -> a
forall a. a -> a
id Either a a
r a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
accum)
| (a -> a) -> (a -> a) -> Either a a -> a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> a
forall a. a -> a
id a -> a
forall a. a -> a
id Either a a
r a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
i = Maybe [a] -> Maybe (Maybe [a])
forall a. a -> Maybe a
Just Maybe [a]
forall a. Maybe a
Nothing
| Either a a -> Bool
forall a b. Either a b -> Bool
eitherIsLeft Either a a
r Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
/= Bool
cTyp = Maybe (Maybe [a])
forall a. Maybe a
Nothing
| Bool
otherwise = [a] -> [Either a a] -> Maybe (Maybe [a])
go ((a -> a) -> (a -> a) -> Either a a -> a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> a
forall a. a -> a
id a -> a
forall a. a -> a
id Either a a
r a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
accum) [Either a a]
rs
go _ [] = Maybe (Maybe [a])
forall a. Maybe a
Nothing
findLoop i :: a
i [] = Maybe (Maybe [a])
forall a. Maybe a
Nothing
tryClose :: VarRef -> ReaderT [Either Int Int] TMonad [Constraint]
tryClose vr :: VarRef
vr@(_,i :: Int
i) = do
[Constraint]
cl <- TMonad [Constraint] -> ReaderT [Either Int Int] TMonad [Constraint]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift(TMonad [Constraint]
-> ReaderT [Either Int Int] TMonad [Constraint])
-> TMonad [Constraint]
-> ReaderT [Either Int Int] TMonad [Constraint]
forall a b. (a -> b) -> a -> b
$ [Constraint] -> TMonad [Constraint]
cannonicalizeConstraints ([Constraint] -> TMonad [Constraint])
-> TMonad [Constraint] -> TMonad [Constraint]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< VarRef -> TMonad [Constraint]
lookupConstraintsList VarRef
vr
case [Constraint] -> ([JType], [JType])
partitionCs [Constraint]
cl of
(_,[s :: JType
s]) -> TMonad () -> ReaderT [Either Int Int] TMonad ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (VarRef -> JType -> TMonad ()
instantiateVarRef VarRef
vr JType
s) ReaderT [Either Int Int] TMonad ()
-> ReaderT [Either Int Int] TMonad ()
-> ReaderT [Either Int Int] TMonad ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Int -> ReaderT [Either Int Int] TMonad ()
go Int
i ReaderT [Either Int Int] TMonad ()
-> ReaderT [Either Int Int] TMonad [Constraint]
-> ReaderT [Either Int Int] TMonad [Constraint]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Constraint] -> ReaderT [Either Int Int] TMonad [Constraint]
forall (m :: * -> *) a. Monad m => a -> m a
return []
([s :: JType
s],_) -> TMonad () -> ReaderT [Either Int Int] TMonad ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (VarRef -> JType -> TMonad ()
instantiateVarRef VarRef
vr JType
s) ReaderT [Either Int Int] TMonad ()
-> ReaderT [Either Int Int] TMonad ()
-> ReaderT [Either Int Int] TMonad ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Int -> ReaderT [Either Int Int] TMonad ()
go Int
i ReaderT [Either Int Int] TMonad ()
-> ReaderT [Either Int Int] TMonad [Constraint]
-> ReaderT [Either Int Int] TMonad [Constraint]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Constraint] -> ReaderT [Either Int Int] TMonad [Constraint]
forall (m :: * -> *) a. Monad m => a -> m a
return []
_ -> [Constraint] -> ReaderT [Either Int Int] TMonad [Constraint]
forall (m :: * -> *) a. Monad m => a -> m a
return [Constraint]
cl
withLocalScope :: TMonad a -> TMonad (a, Set Int)
withLocalScope :: TMonad a -> TMonad (a, Set Int)
withLocalScope act :: TMonad a
act = do
(TCState -> TCState) -> TMonad ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\s :: TCState
s -> TCState
s {tc_env :: [Map Ident JType]
tc_env = Map Ident JType
forall k a. Map k a
M.empty Map Ident JType -> [Map Ident JType] -> [Map Ident JType]
forall a. a -> [a] -> [a]
: TCState -> [Map Ident JType]
tc_env TCState
s,
tc_stack :: [Set Int]
tc_stack = Set Int
forall a. Set a
S.empty Set Int -> [Set Int] -> [Set Int]
forall a. a -> [a] -> [a]
: TCState -> [Set Int]
tc_stack TCState
s})
a
res <- TMonad a
act
Set Int
frame <- [Set Int] -> Set Int
forall a. [a] -> a
head ([Set Int] -> Set Int)
-> (TCState -> [Set Int]) -> TCState -> Set Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCState -> [Set Int]
tc_stack (TCState -> Set Int) -> TMonad TCState -> TMonad (Set Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TMonad TCState
forall s (m :: * -> *). MonadState s m => m s
get
(TCState -> TCState) -> TMonad ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\s :: TCState
s -> TCState
s {tc_env :: [Map Ident JType]
tc_env = Int -> [Map Ident JType] -> [Map Ident JType]
forall a. Int -> [a] -> [a]
drop 1 ([Map Ident JType] -> [Map Ident JType])
-> [Map Ident JType] -> [Map Ident JType]
forall a b. (a -> b) -> a -> b
$ TCState -> [Map Ident JType]
tc_env TCState
s,
tc_stack :: [Set Int]
tc_stack = Int -> [Set Int] -> [Set Int]
forall a. Int -> [a] -> [a]
drop 1 ([Set Int] -> [Set Int]) -> [Set Int] -> [Set Int]
forall a b. (a -> b) -> a -> b
$ TCState -> [Set Int]
tc_stack TCState
s})
(a, Set Int) -> TMonad (a, Set Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
res, Set Int
frame)
setFrozen :: Set Int -> TMonad ()
setFrozen :: Set Int -> TMonad ()
setFrozen x :: Set Int
x = (TCState -> TCState) -> TMonad ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\s :: TCState
s -> TCState
s {tc_frozen :: Set Int
tc_frozen = TCState -> Set Int
tc_frozen TCState
s Set Int -> Set Int -> Set Int
forall a. Ord a => Set a -> Set a -> Set a
`S.union` Set Int
x})
frame2VarRefs :: Set t -> [(Maybe a, t)]
frame2VarRefs :: Set t -> [(Maybe a, t)]
frame2VarRefs frame :: Set t
frame = (\x :: t
x -> (Maybe a
forall a. Maybe a
Nothing,t
x)) (t -> (Maybe a, t)) -> [t] -> [(Maybe a, t)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set t -> [t]
forall a. Set a -> [a]
S.toList Set t
frame
addEnv :: Ident -> JType -> TMonad ()
addEnv :: Ident -> JType -> TMonad ()
addEnv ident :: Ident
ident typ :: JType
typ = do
[Map Ident JType]
envstack <- TCState -> [Map Ident JType]
tc_env (TCState -> [Map Ident JType])
-> TMonad TCState -> TMonad [Map Ident JType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TMonad TCState
forall s (m :: * -> *). MonadState s m => m s
get
case [Map Ident JType]
envstack of
(e :: Map Ident JType
e:es :: [Map Ident JType]
es) -> (TCState -> TCState) -> TMonad ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\s :: TCState
s -> TCState
s {tc_env :: [Map Ident JType]
tc_env = Ident -> JType -> Map Ident JType -> Map Ident JType
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Ident
ident JType
typ Map Ident JType
e Map Ident JType -> [Map Ident JType] -> [Map Ident JType]
forall a. a -> [a] -> [a]
: [Map Ident JType]
es})
_ -> String -> TMonad ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError "empty env stack (this should never happen)"
newVarDecl :: Ident -> TMonad JType
newVarDecl :: Ident -> TMonad JType
newVarDecl ident :: Ident
ident = do
JType
v <- TMonad JType
newTyVar
Ident -> JType -> TMonad ()
addEnv Ident
ident JType
v
JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
v
resolveTypeGen :: ((JType -> TMonad JType) -> JType -> TMonad JType) -> JType -> TMonad JType
resolveTypeGen :: ((JType -> TMonad JType) -> JType -> TMonad JType)
-> JType -> TMonad JType
resolveTypeGen f :: (JType -> TMonad JType) -> JType -> TMonad JType
f typ :: JType
typ = JType -> TMonad JType
go JType
typ
where
go :: JType -> TMonad JType
go :: JType -> TMonad JType
go x :: JType
x@(JTFree (_, ref :: Int
ref)) = do
Map Int StoreVal
vars <- TCState -> Map Int StoreVal
tc_vars (TCState -> Map Int StoreVal)
-> TMonad TCState -> TMonad (Map Int StoreVal)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TMonad TCState
forall s (m :: * -> *). MonadState s m => m s
get
case Int -> Map Int StoreVal -> Maybe StoreVal
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Int
ref Map Int StoreVal
vars of
Just (SVType t :: JType
t) -> do
JType
res <- JType -> TMonad JType
go JType
t
Bool -> TMonad () -> TMonad ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (JType
res JType -> JType -> Bool
forall a. Eq a => a -> a -> Bool
/= JType
t) (TMonad () -> TMonad ()) -> TMonad () -> TMonad ()
forall a b. (a -> b) -> a -> b
$ (TCState -> TCState) -> TMonad ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\s :: TCState
s -> TCState
s {tc_vars :: Map Int StoreVal
tc_vars = Int -> StoreVal -> Map Int StoreVal -> Map Int StoreVal
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Int
ref (JType -> StoreVal
SVType JType
res) (Map Int StoreVal -> Map Int StoreVal)
-> Map Int StoreVal -> Map Int StoreVal
forall a b. (a -> b) -> a -> b
$ TCState -> Map Int StoreVal
tc_vars TCState
s})
JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
res
_ -> JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
x
go (JTForall refs :: [VarRef]
refs t :: JType
t) = do
[VarRef]
refs' <- [Maybe VarRef] -> [VarRef]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe VarRef] -> [VarRef])
-> TMonad [Maybe VarRef] -> TMonad [VarRef]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (VarRef -> TMonad (Maybe VarRef))
-> [VarRef] -> TMonad [Maybe VarRef]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM VarRef -> TMonad (Maybe VarRef)
forall (m :: * -> *) a.
MonadState TCState m =>
(a, Int) -> m (Maybe (a, Int))
checkRef [VarRef]
refs
if [VarRef] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [VarRef]
refs'
then JType -> TMonad JType
go JType
t
else [VarRef] -> JType -> JType
JTForall [VarRef]
refs' (JType -> JType) -> TMonad JType -> TMonad JType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> JType -> TMonad JType
go JType
t
go x :: JType
x = (JType -> TMonad JType) -> JType -> TMonad JType
f JType -> TMonad JType
go JType
x
checkRef :: (a, Int) -> m (Maybe (a, Int))
checkRef x :: (a, Int)
x@(_, ref :: Int
ref) = do
Map Int StoreVal
vars <- TCState -> Map Int StoreVal
tc_vars (TCState -> Map Int StoreVal) -> m TCState -> m (Map Int StoreVal)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m TCState
forall s (m :: * -> *). MonadState s m => m s
get
case Int -> Map Int StoreVal -> Maybe StoreVal
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Int
ref Map Int StoreVal
vars of
Just (SVType t :: JType
t) -> Maybe (a, Int) -> m (Maybe (a, Int))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (a, Int)
forall a. Maybe a
Nothing
_ -> Maybe (a, Int) -> m (Maybe (a, Int))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (a, Int) -> m (Maybe (a, Int)))
-> Maybe (a, Int) -> m (Maybe (a, Int))
forall a b. (a -> b) -> a -> b
$ (a, Int) -> Maybe (a, Int)
forall a. a -> Maybe a
Just (a, Int)
x
resolveType :: JType -> TMonad JType
resolveType = ((JType -> TMonad JType) -> JType -> TMonad JType)
-> JType -> TMonad JType
resolveTypeGen (JType -> TMonad JType) -> JType -> TMonad JType
forall t (m :: * -> *).
(Compos1 t, Monad m) =>
(t -> m t) -> t -> m t
composOpM1
resolveTypeShallow :: JType -> TMonad JType
resolveTypeShallow = ((JType -> TMonad JType) -> JType -> TMonad JType)
-> JType -> TMonad JType
resolveTypeGen ((JType -> TMonad JType)
-> (JType -> TMonad JType) -> JType -> TMonad JType
forall a b. a -> b -> a
const JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return)
integrateLocalType :: JLocalType -> TMonad JType
integrateLocalType :: JLocalType -> TMonad JType
integrateLocalType (env :: [(VarRef, Constraint)]
env,typ :: JType
typ) = do
(r :: JType
r, frame :: Set Int
frame) <- TMonad JType -> TMonad (JType, Set Int)
forall a. TMonad a -> TMonad (a, Set Int)
withLocalScope (TMonad JType -> TMonad (JType, Set Int))
-> TMonad JType -> TMonad (JType, Set Int)
forall a b. (a -> b) -> a -> b
$ (StateT (Map Int JType) TMonad JType
-> Map Int JType -> TMonad JType)
-> Map Int JType
-> StateT (Map Int JType) TMonad JType
-> TMonad JType
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT (Map Int JType) TMonad JType
-> Map Int JType -> TMonad JType
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT Map Int JType
forall k a. Map k a
M.empty (StateT (Map Int JType) TMonad JType -> TMonad JType)
-> StateT (Map Int JType) TMonad JType -> TMonad JType
forall a b. (a -> b) -> a -> b
$ do
((VarRef, Constraint) -> StateT (Map Int JType) TMonad ())
-> [(VarRef, Constraint)] -> StateT (Map Int JType) TMonad ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Monad f) =>
(a -> f b) -> t a -> f ()
mapM_ (VarRef, Constraint) -> StateT (Map Int JType) TMonad ()
forall (t :: (* -> *) -> * -> *).
(MonadState (Map Int JType) (t TMonad), MonadTrans t) =>
(VarRef, Constraint) -> t TMonad ()
integrateEnv [(VarRef, Constraint)]
env
JType -> StateT (Map Int JType) TMonad JType
forall (t :: (* -> *) -> * -> *).
(MonadState (Map Int JType) (t TMonad), MonadTrans t) =>
JType -> t TMonad JType
cloneType JType
typ
JType -> TMonad JType
resolveType (JType -> TMonad JType) -> JType -> TMonad JType
forall a b. (a -> b) -> a -> b
$ [VarRef] -> JType -> JType
JTForall (Set Int -> [VarRef]
forall t a. Set t -> [(Maybe a, t)]
frame2VarRefs Set Int
frame) JType
r
where
getRef :: (Maybe String, k) -> t TMonad JType
getRef (mbName :: Maybe String
mbName, ref :: k
ref) = do
Map k JType
m <- t TMonad (Map k JType)
forall s (m :: * -> *). MonadState s m => m s
get
case k -> Map k JType -> Maybe JType
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup k
ref Map k JType
m of
Just newTy :: JType
newTy -> JType -> t TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
newTy
Nothing -> do
JType
newTy <- (\x :: VarRef
x -> VarRef -> JType
JTFree (Maybe String
mbName, VarRef -> Int
forall a b. (a, b) -> b
snd VarRef
x)) (VarRef -> JType) -> t TMonad VarRef -> t TMonad JType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TMonad VarRef -> t TMonad VarRef
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TMonad VarRef
newVarRef
Map k JType -> t TMonad ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Map k JType -> t TMonad ()) -> Map k JType -> t TMonad ()
forall a b. (a -> b) -> a -> b
$ k -> JType -> Map k JType -> Map k JType
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert k
ref JType
newTy Map k JType
m
JType -> t TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
newTy
integrateEnv :: (VarRef, Constraint) -> t TMonad ()
integrateEnv (vr :: VarRef
vr,c :: Constraint
c) = do
JType
newTy <- VarRef -> t TMonad JType
forall (t :: (* -> *) -> * -> *) k.
(MonadState (Map k JType) (t TMonad), Ord k, MonadTrans t) =>
(Maybe String, k) -> t TMonad JType
getRef VarRef
vr
case Constraint
c of
(Sub t :: JType
t) -> TMonad () -> t TMonad ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TMonad () -> t TMonad ())
-> (JType -> TMonad ()) -> JType -> t TMonad ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (JType
newTy JType -> JType -> TMonad ()
<:) (JType -> t TMonad ()) -> t TMonad JType -> t TMonad ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< JType -> t TMonad JType
forall (t :: (* -> *) -> * -> *).
(MonadState (Map Int JType) (t TMonad), MonadTrans t) =>
JType -> t TMonad JType
cloneType JType
t
(Super t :: JType
t) -> TMonad () -> t TMonad ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TMonad () -> t TMonad ())
-> (JType -> TMonad ()) -> JType -> t TMonad ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (JType -> JType -> TMonad ()
<: JType
newTy) (JType -> t TMonad ()) -> t TMonad JType -> t TMonad ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< JType -> t TMonad JType
forall (t :: (* -> *) -> * -> *).
(MonadState (Map Int JType) (t TMonad), MonadTrans t) =>
JType -> t TMonad JType
cloneType JType
t
cloneType :: JType -> t TMonad JType
cloneType (JTFree vr :: VarRef
vr) = VarRef -> t TMonad JType
forall (t :: (* -> *) -> * -> *) k.
(MonadState (Map k JType) (t TMonad), Ord k, MonadTrans t) =>
(Maybe String, k) -> t TMonad JType
getRef VarRef
vr
cloneType x :: JType
x = (JType -> t TMonad JType) -> JType -> t TMonad JType
forall t (m :: * -> *).
(Compos1 t, Monad m) =>
(t -> m t) -> t -> m t
composOpM1 JType -> t TMonad JType
cloneType JType
x
lookupEnv :: Ident -> TMonad JType
lookupEnv :: Ident -> TMonad JType
lookupEnv ident :: Ident
ident = JType -> TMonad JType
resolveType (JType -> TMonad JType) -> TMonad JType -> TMonad JType
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Map Ident JType] -> TMonad JType
forall a. [Map Ident a] -> TMonad a
go ([Map Ident JType] -> TMonad JType)
-> (TCState -> [Map Ident JType]) -> TCState -> TMonad JType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCState -> [Map Ident JType]
tc_env (TCState -> TMonad JType) -> TMonad TCState -> TMonad JType
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TMonad TCState
forall s (m :: * -> *). MonadState s m => m s
get
where go :: [Map Ident a] -> TMonad a
go (e :: Map Ident a
e:es :: [Map Ident a]
es) = case Ident -> Map Ident a -> Maybe a
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Ident
ident Map Ident a
e of
Just t :: a
t -> a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return a
t
Nothing -> [Map Ident a] -> TMonad a
go [Map Ident a]
es
go _ = String -> TMonad a
forall a. String -> TMonad a
tyErr0 (String -> TMonad a) -> String -> TMonad a
forall a b. (a -> b) -> a -> b
$ "unable to resolve variable name: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ Ident -> Doc
forall a. JsToDoc a => a -> Doc
jsToDoc (Ident -> Doc) -> Ident -> Doc
forall a b. (a -> b) -> a -> b
$ Ident
ident)
freeVars :: JType -> TMonad (Set Int)
freeVars :: JType -> TMonad (Set Int)
freeVars t :: JType
t = WriterT (Set Int) TMonad () -> TMonad (Set Int)
forall (m :: * -> *) w a. Monad m => WriterT w m a -> m w
execWriterT (WriterT (Set Int) TMonad () -> TMonad (Set Int))
-> (JType -> WriterT (Set Int) TMonad ())
-> JType
-> TMonad (Set Int)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. JType -> WriterT (Set Int) TMonad ()
forall (m :: * -> *). MonadWriter (Set Int) m => JType -> m ()
go (JType -> TMonad (Set Int)) -> TMonad JType -> TMonad (Set Int)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< JType -> TMonad JType
resolveType JType
t
where go :: JType -> m ()
go (JTFree (_, ref :: Int
ref)) = Set Int -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Int -> Set Int
forall a. a -> Set a
S.singleton Int
ref)
go x :: JType
x = (JType -> m ()) -> JType -> m ()
forall t (m :: * -> *).
(Compos1 t, Monad m) =>
(t -> m ()) -> t -> m ()
composOpM1_ JType -> m ()
go JType
x
instantiateScheme :: [VarRef] -> JType -> TMonad JType
instantiateScheme :: [VarRef] -> JType -> TMonad JType
instantiateScheme vrs :: [VarRef]
vrs t :: JType
t = StateT (Map Int JType) TMonad JType
-> Map Int JType -> TMonad JType
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (JType -> StateT (Map Int JType) TMonad JType
go JType
t) Map Int JType
forall k a. Map k a
M.empty
where
schemeVars :: Set Int
schemeVars = [Int] -> Set Int
forall a. Ord a => [a] -> Set a
S.fromList ([Int] -> Set Int) -> [Int] -> Set Int
forall a b. (a -> b) -> a -> b
$ (VarRef -> Int) -> [VarRef] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map VarRef -> Int
forall a b. (a, b) -> b
snd [VarRef]
vrs
go :: JType -> StateT (Map Int JType) TMonad JType
go :: JType -> StateT (Map Int JType) TMonad JType
go (JTFree vr :: VarRef
vr@(mbName :: Maybe String
mbName, ref :: Int
ref))
| Int
ref Int -> Set Int -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set Int
schemeVars = do
Map Int JType
m <- StateT (Map Int JType) TMonad (Map Int JType)
forall s (m :: * -> *). MonadState s m => m s
get
case Int -> Map Int JType -> Maybe JType
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Int
ref Map Int JType
m of
Just newTy :: JType
newTy -> JType -> StateT (Map Int JType) TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
newTy
Nothing -> do
VarRef
newRef <- (\x :: VarRef
x -> (Maybe String
mbName, VarRef -> Int
forall a b. (a, b) -> b
snd VarRef
x)) (VarRef -> VarRef)
-> StateT (Map Int JType) TMonad VarRef
-> StateT (Map Int JType) TMonad VarRef
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TMonad VarRef -> StateT (Map Int JType) TMonad VarRef
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TMonad VarRef
newVarRef
Map Int JType -> StateT (Map Int JType) TMonad ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Map Int JType -> StateT (Map Int JType) TMonad ())
-> Map Int JType -> StateT (Map Int JType) TMonad ()
forall a b. (a -> b) -> a -> b
$ Int -> JType -> Map Int JType -> Map Int JType
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Int
ref (VarRef -> JType
JTFree VarRef
newRef) Map Int JType
m
(Constraint -> StateT (Map Int JType) TMonad ())
-> [Constraint] -> StateT (Map Int JType) TMonad ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Monad f) =>
(a -> f b) -> t a -> f ()
mapM_ (TMonad () -> StateT (Map Int JType) TMonad ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TMonad () -> StateT (Map Int JType) TMonad ())
-> (Constraint -> TMonad ())
-> Constraint
-> StateT (Map Int JType) TMonad ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarRef -> Constraint -> TMonad ()
addConstraint VarRef
newRef (Constraint -> StateT (Map Int JType) TMonad ())
-> (Constraint -> StateT (Map Int JType) TMonad Constraint)
-> Constraint
-> StateT (Map Int JType) TMonad ()
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< (JType -> StateT (Map Int JType) TMonad JType)
-> Constraint -> StateT (Map Int JType) TMonad Constraint
forall (m :: * -> *).
(Monad m, Functor m) =>
(JType -> m JType) -> Constraint -> m Constraint
mapConstraint JType -> StateT (Map Int JType) TMonad JType
go) ([Constraint] -> StateT (Map Int JType) TMonad ())
-> StateT (Map Int JType) TMonad [Constraint]
-> StateT (Map Int JType) TMonad ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TMonad [Constraint] -> StateT (Map Int JType) TMonad [Constraint]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (VarRef -> TMonad [Constraint]
lookupConstraintsList VarRef
vr)
JType -> StateT (Map Int JType) TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return (VarRef -> JType
JTFree VarRef
newRef)
go x :: JType
x = (JType -> StateT (Map Int JType) TMonad JType)
-> JType -> StateT (Map Int JType) TMonad JType
forall t (m :: * -> *).
(Compos1 t, Monad m) =>
(t -> m t) -> t -> m t
composOpM1 JType -> StateT (Map Int JType) TMonad JType
go JType
x
instantiateRigidScheme :: [VarRef] -> JType -> TMonad JType
instantiateRigidScheme :: [VarRef] -> JType -> TMonad JType
instantiateRigidScheme vrs :: [VarRef]
vrs t :: JType
t = StateT (Map Int JType) TMonad JType
-> Map Int JType -> TMonad JType
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (JType -> StateT (Map Int JType) TMonad JType
go JType
t) Map Int JType
forall k a. Map k a
M.empty
where
schemeVars :: Set Int
schemeVars = [Int] -> Set Int
forall a. Ord a => [a] -> Set a
S.fromList ([Int] -> Set Int) -> [Int] -> Set Int
forall a b. (a -> b) -> a -> b
$ (VarRef -> Int) -> [VarRef] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map VarRef -> Int
forall a b. (a, b) -> b
snd [VarRef]
vrs
go :: JType -> StateT (Map Int JType) TMonad JType
go :: JType -> StateT (Map Int JType) TMonad JType
go (JTFree vr :: VarRef
vr@(mbName :: Maybe String
mbName, ref :: Int
ref))
| Int
ref Int -> Set Int -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set Int
schemeVars = do
Map Int JType
m <- StateT (Map Int JType) TMonad (Map Int JType)
forall s (m :: * -> *). MonadState s m => m s
get
case Int -> Map Int JType -> Maybe JType
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Int
ref Map Int JType
m of
Just newTy :: JType
newTy -> JType -> StateT (Map Int JType) TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
newTy
Nothing -> do
JType
newRef <- VarRef -> Set Constraint -> JType
JTRigid VarRef
vr (Set Constraint -> JType)
-> ([Constraint] -> Set Constraint) -> [Constraint] -> JType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Constraint] -> Set Constraint
forall a. Ord a => [a] -> Set a
S.fromList ([Constraint] -> JType)
-> StateT (Map Int JType) TMonad [Constraint]
-> StateT (Map Int JType) TMonad JType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TMonad [Constraint] -> StateT (Map Int JType) TMonad [Constraint]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (VarRef -> TMonad [Constraint]
lookupConstraintsList VarRef
vr)
Map Int JType -> StateT (Map Int JType) TMonad ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Map Int JType -> StateT (Map Int JType) TMonad ())
-> Map Int JType -> StateT (Map Int JType) TMonad ()
forall a b. (a -> b) -> a -> b
$ Int -> JType -> Map Int JType -> Map Int JType
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Int
ref JType
newRef Map Int JType
m
JType -> StateT (Map Int JType) TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
newRef
go x :: JType
x = (JType -> StateT (Map Int JType) TMonad JType)
-> JType -> StateT (Map Int JType) TMonad JType
forall t (m :: * -> *).
(Compos1 t, Monad m) =>
(t -> m t) -> t -> m t
composOpM1 JType -> StateT (Map Int JType) TMonad JType
go JType
x
checkEscapedVars :: [VarRef] -> JType -> TMonad ()
checkEscapedVars :: [VarRef] -> JType -> TMonad ()
checkEscapedVars vrs :: [VarRef]
vrs t :: JType
t = JType -> TMonad ()
go JType
t
where
vs :: Set Int
vs = [Int] -> Set Int
forall a. Ord a => [a] -> Set a
S.fromList ([Int] -> Set Int) -> [Int] -> Set Int
forall a b. (a -> b) -> a -> b
$ (VarRef -> Int) -> [VarRef] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map VarRef -> Int
forall a b. (a, b) -> b
snd [VarRef]
vrs
go :: JType -> TMonad ()
go t :: JType
t@(JTRigid (_,ref :: Int
ref) _)
| Int
ref Int -> Set Int -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set Int
vs = String -> JType -> TMonad ()
forall b. String -> JType -> TMonad b
tyErr1 "Qualified var escapes into environment" JType
t
| Bool
otherwise = () -> TMonad ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
go x :: JType
x = (JType -> TMonad ()) -> JType -> TMonad ()
forall t (m :: * -> *).
(Compos1 t, Monad m) =>
(t -> m ()) -> t -> m ()
composOpM1_ JType -> TMonad ()
go JType
x
(<:) :: JType -> JType -> TMonad ()
x :: JType
x <: :: JType -> JType -> TMonad ()
<: y :: JType
y = do
JType
xt <- JType -> TMonad JType
resolveTypeShallow JType
x
JType
yt <- JType -> TMonad JType
resolveTypeShallow JType
y
if JType
xt JType -> JType -> Bool
forall a. Eq a => a -> a -> Bool
== JType
yt
then () -> TMonad ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
else JType -> JType -> TMonad ()
go JType
xt JType
yt TMonad () -> TMonad String -> TMonad ()
forall a. TMonad a -> TMonad String -> TMonad a
`withContext` (do
String
xt <- JType -> TMonad String
prettyType JType
x
String
yt <- JType -> TMonad String
prettyType JType
y
String -> TMonad String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> TMonad String) -> String -> TMonad String
forall a b. (a -> b) -> a -> b
$ "When applying subtype constraint: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
xt String -> ShowS
forall a. [a] -> [a] -> [a]
++ " <: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
yt)
where
go :: JType -> JType -> TMonad ()
go _ JTStat = () -> TMonad ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
go JTImpossible _ = () -> TMonad ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
go xt :: JType
xt@(JTFree ref :: VarRef
ref) yt :: JType
yt@(JTFree ref2 :: VarRef
ref2) = VarRef -> Constraint -> TMonad ()
addConstraint VarRef
ref (JType -> Constraint
Sub JType
yt) TMonad () -> TMonad () -> TMonad ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
VarRef -> Constraint -> TMonad ()
addConstraint VarRef
ref2 (JType -> Constraint
Super JType
xt)
go (JTFree ref :: VarRef
ref) yt :: JType
yt = VarRef -> Constraint -> TMonad ()
addConstraint VarRef
ref (JType -> Constraint
Sub JType
yt)
go xt :: JType
xt (JTFree ref :: VarRef
ref) = VarRef -> Constraint -> TMonad ()
addConstraint VarRef
ref (JType -> Constraint
Super JType
xt)
go xt :: JType
xt yt :: JType
yt@(JTForall vars :: [VarRef]
vars t :: JType
t) = do
JType
t' <- [VarRef] -> JType -> TMonad JType
instantiateRigidScheme [VarRef]
vars JType
t
JType -> JType -> TMonad ()
go JType
xt JType
t'
[VarRef] -> JType -> TMonad ()
checkEscapedVars [VarRef]
vars (JType -> TMonad ()) -> TMonad JType -> TMonad ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< JType -> TMonad JType
resolveType JType
xt
go (JTForall vars :: [VarRef]
vars t :: JType
t) yt :: JType
yt = do
JType
t' <- [VarRef] -> JType -> TMonad JType
instantiateScheme [VarRef]
vars JType
t
JType -> JType -> TMonad ()
go JType
t' JType
yt
go xt :: JType
xt@(JTFunc argsx :: [JType]
argsx retx :: JType
retx) yt :: JType
yt@(JTFunc argsy :: [JType]
argsy rety :: JType
rety) = do
Bool -> TMonad () -> TMonad ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([JType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [JType]
argsy Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [JType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [JType]
argsx) (TMonad () -> TMonad ()) -> TMonad () -> TMonad ()
forall a b. (a -> b) -> a -> b
$ JType -> JType -> TMonad ()
forall a. JType -> JType -> TMonad a
tyErr2Sub JType
xt JType
yt
(JType -> JType -> TMonad ()) -> [JType] -> [JType] -> TMonad ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ JType -> JType -> TMonad ()
(<:) [JType]
argsy [JType]
argsx
JType
retx JType -> JType -> TMonad ()
<: JType
rety
go (JTList xt :: JType
xt) (JTList yt :: JType
yt) = JType
xt JType -> JType -> TMonad ()
<: JType
yt
go (JTMap xt :: JType
xt) (JTMap yt :: JType
yt) = JType
xt JType -> JType -> TMonad ()
<: JType
yt
go (JTRecord xt :: JType
xt xm :: Map String JType
xm) (JTRecord yt :: JType
yt ym :: Map String JType
ym)
| (JType -> JType -> Bool)
-> Map String JType -> Map String JType -> Bool
forall k a b.
Ord k =>
(a -> b -> Bool) -> Map k a -> Map k b -> Bool
M.isSubmapOfBy (\_ _ -> Bool
True) Map String JType
ym Map String JType
xm = JType
xt JType -> JType -> TMonad ()
<: JType
yt TMonad () -> TMonad (Map String ()) -> TMonad (Map String ())
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (JType -> JType -> TMonad ())
-> Map String JType -> Map String JType -> TMonad (Map String ())
forall (m :: * -> *) key val b.
(Monad m, Ord key) =>
(val -> val -> m b) -> Map key val -> Map key val -> m (Map key b)
intersectionWithM JType -> JType -> TMonad ()
(<:) Map String JType
xm Map String JType
ym TMonad (Map String ()) -> TMonad () -> TMonad ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> TMonad ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
go xt :: JType
xt yt :: JType
yt = JType -> JType -> TMonad ()
forall a. JType -> JType -> TMonad a
tyErr2Sub JType
xt JType
yt
(<<:>) :: TMonad JType -> TMonad JType -> TMonad ()
x :: TMonad JType
x <<:> :: TMonad JType -> TMonad JType -> TMonad ()
<<:> y :: TMonad JType
y = TMonad (TMonad ()) -> TMonad ()
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (TMonad (TMonad ()) -> TMonad ())
-> TMonad (TMonad ()) -> TMonad ()
forall a b. (a -> b) -> a -> b
$ (JType -> JType -> TMonad ())
-> TMonad JType -> TMonad JType -> TMonad (TMonad ())
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 JType -> JType -> TMonad ()
(<:) TMonad JType
x TMonad JType
y
someUpperBound :: [JType] -> TMonad JType
someUpperBound :: [JType] -> TMonad JType
someUpperBound [] = JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTStat
someUpperBound xs :: [JType]
xs = do
JType
res <- TMonad JType
newTyVar
Bool
b <- ((JType -> TMonad ()) -> [JType] -> TMonad ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Monad f) =>
(a -> f b) -> t a -> f ()
mapM_ (JType -> JType -> TMonad ()
<: JType
res) [JType]
xs TMonad () -> TMonad Bool -> TMonad Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> TMonad Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True) TMonad Bool -> (String -> TMonad Bool) -> TMonad Bool
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \e :: String
e -> Bool -> TMonad Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
if Bool
b then JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
res else JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTStat
someLowerBound :: [JType] -> TMonad JType
someLowerBound :: [JType] -> TMonad JType
someLowerBound [] = JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTImpossible
someLowerBound xs :: [JType]
xs = do
JType
res <- TMonad JType
newTyVar
(JType -> TMonad ()) -> [JType] -> TMonad ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Monad f) =>
(a -> f b) -> t a -> f ()
mapM_ (JType
res JType -> JType -> TMonad ()
<:) [JType]
xs
JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
res
(=.=) :: JType -> JType -> TMonad JType
x :: JType
x =.= :: JType -> JType -> TMonad JType
=.= y :: JType
y = do
JType
x JType -> JType -> TMonad ()
<: JType
y
JType
y JType -> JType -> TMonad ()
<: JType
x
JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
x
instance JTypeCheck JExpr where
typecheck :: JExpr -> TMonad JType
typecheck (ValExpr e :: JVal
e) = JVal -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JVal
e
typecheck (SelExpr e :: JExpr
e (StrI i :: String
i)) =
do JType
et <- JExpr -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JExpr
e
case JType
et of
(JTRecord t :: JType
t m :: Map String JType
m) -> case String -> Map String JType -> Maybe JType
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
i Map String JType
m of
Just res :: JType
res -> JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
res
Nothing -> String -> JType -> TMonad JType
forall b. String -> JType -> TMonad b
tyErr1 ("Record contains no field named " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
i) JType
et
(JTFree r :: VarRef
r) -> do
JType
res <- TMonad JType
newTyVar
VarRef -> Constraint -> TMonad ()
addConstraint VarRef
r (JType -> Constraint
Sub (JType -> Map String JType -> JType
JTRecord JType
res (String -> JType -> Map String JType
forall k a. k -> a -> Map k a
M.singleton String
i JType
res)))
JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
res
_ -> String -> JType -> TMonad JType
forall b. String -> JType -> TMonad b
tyErr1 "Cannot use record selector on this value" JType
et
typecheck (IdxExpr e :: JExpr
e e1 :: JExpr
e1) = TMonad JType
forall a. HasCallStack => a
undefined
typecheck (InfixExpr s :: String
s e :: JExpr
e e1 :: JExpr
e1)
| String
s String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ["-","/","*"] = JType -> TMonad ()
setFixed JType
JTNum TMonad () -> TMonad JType -> TMonad JType
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTNum
| String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "+" = JType -> TMonad ()
setFixed JType
JTNum TMonad () -> TMonad JType -> TMonad JType
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTNum
| String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "++" = JType -> TMonad ()
setFixed JType
JTString TMonad () -> TMonad JType -> TMonad JType
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTString
| String
s String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [">","<"] = JType -> TMonad ()
setFixed JType
JTNum TMonad () -> TMonad JType -> TMonad JType
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTBool
| String
s String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ["==","/="] = do
JType
et <- JExpr -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JExpr
e
JType
e1t <- JExpr -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JExpr
e1
JType
_ <- JType
et JType -> JType -> TMonad JType
=.= JType
e1t
JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTBool
| String
s String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ["||","&&"] = JType -> TMonad ()
setFixed JType
JTBool TMonad () -> TMonad JType -> TMonad JType
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTBool
| Bool
otherwise = String -> TMonad JType
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> TMonad JType) -> String -> TMonad JType
forall a b. (a -> b) -> a -> b
$ "Unhandled operator: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s
where setFixed :: JType -> TMonad ()
setFixed t :: JType
t = do
JExpr -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JExpr
e TMonad JType -> TMonad JType -> TMonad ()
<<:> JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
t
JExpr -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JExpr
e1 TMonad JType -> TMonad JType -> TMonad ()
<<:> JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
t
typecheck (PPostExpr _ _ e :: JExpr
e) = case JExpr
e of
(SelExpr _ _) -> TMonad JType
go
(ValExpr (JVar _)) -> TMonad JType
go
(IdxExpr _ _) -> TMonad JType
go
_ -> String -> JType -> TMonad JType
forall b. String -> JType -> TMonad b
tyErr1 "Value not compatible with postfix assignment" (JType -> TMonad JType) -> TMonad JType -> TMonad JType
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< JExpr -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JExpr
e
where go :: TMonad JType
go = (JExpr -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JExpr
e TMonad JType -> TMonad JType -> TMonad ()
<<:> JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTNum) TMonad () -> TMonad JType -> TMonad JType
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTNum
typecheck (IfExpr e :: JExpr
e e1 :: JExpr
e1 e2 :: JExpr
e2) = do
JExpr -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JExpr
e TMonad JType -> TMonad JType -> TMonad ()
<<:> JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTBool
TMonad (TMonad JType) -> TMonad JType
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (TMonad (TMonad JType) -> TMonad JType)
-> TMonad (TMonad JType) -> TMonad JType
forall a b. (a -> b) -> a -> b
$ (JType -> JType -> TMonad JType)
-> TMonad JType -> TMonad JType -> TMonad (TMonad JType)
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (\x :: JType
x y :: JType
y -> [JType] -> TMonad JType
someUpperBound [JType
x,JType
y]) (JExpr -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JExpr
e1) (JExpr -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JExpr
e2)
typecheck (NewExpr e :: JExpr
e) = TMonad JType
forall a. HasCallStack => a
undefined
typecheck (ApplExpr e :: JExpr
e appArgse :: [JExpr]
appArgse) = do
JType
et <- JExpr -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JExpr
e
[JType]
appArgst <- (JExpr -> TMonad JType) -> [JExpr] -> TMonad [JType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM JExpr -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck [JExpr]
appArgse
let go :: JType -> TMonad JType
go (JTForall vars :: [VarRef]
vars t :: JType
t) = JType -> TMonad JType
go (JType -> TMonad JType) -> TMonad JType -> TMonad JType
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [VarRef] -> JType -> TMonad JType
instantiateScheme [VarRef]
vars JType
t
go (JTFunc argst :: [JType]
argst rett :: JType
rett) = do
(JType -> JType -> TMonad ()) -> [JType] -> [JType] -> TMonad ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ JType -> JType -> TMonad ()
(<:) ([JType]
appArgst [JType] -> [JType] -> [JType]
forall a. [a] -> [a] -> [a]
++ JType -> [JType]
forall a. a -> [a]
repeat JType
JTStat) [JType]
argst
JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
rett
go (JTFree vr :: VarRef
vr) = do
JType
ret <- TMonad JType
newTyVar
VarRef -> Constraint -> TMonad ()
addConstraint VarRef
vr (JType -> Constraint
Sub ([JType] -> JType -> JType
JTFunc [JType]
appArgst JType
ret))
JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
ret
go x :: JType
x = String -> JType -> TMonad JType
forall b. String -> JType -> TMonad b
tyErr1 "Cannot apply value as function" JType
x
JType -> TMonad JType
go JType
et
typecheck (UnsatExpr _) = TMonad JType
forall a. HasCallStack => a
undefined
typecheck (AntiExpr s :: String
s) = String -> TMonad JType
forall a. HasCallStack => String -> a
error (String -> TMonad JType) -> String -> TMonad JType
forall a b. (a -> b) -> a -> b
$ "Antiquoted expression not provided with explicit signature: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
s
typecheck (TypeExpr forceType :: Bool
forceType e :: JExpr
e t :: JLocalType
t)
| Bool
forceType = JLocalType -> TMonad JType
integrateLocalType JLocalType
t
| Bool
otherwise = do
JType
t1 <- JLocalType -> TMonad JType
integrateLocalType JLocalType
t
JExpr -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JExpr
e TMonad JType -> TMonad JType -> TMonad ()
<<:> JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
t1
JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
t1
instance JTypeCheck JVal where
typecheck :: JVal -> TMonad JType
typecheck (JVar i :: Ident
i) =
case Ident
i of
StrI "true" -> JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTBool
StrI "false" -> JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTBool
StrI "null" -> TMonad JType
newTyVar
StrI _ -> Ident -> TMonad JType
lookupEnv Ident
i
typecheck (JInt _) = JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTNum
typecheck (JDouble _) = JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTNum
typecheck (JStr _) = JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTString
typecheck (JList xs :: [JExpr]
xs) = JVal -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck (Map String JExpr -> JVal
JHash (Map String JExpr -> JVal) -> Map String JExpr -> JVal
forall a b. (a -> b) -> a -> b
$ [(String, JExpr)] -> Map String JExpr
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(String, JExpr)] -> Map String JExpr)
-> [(String, JExpr)] -> Map String JExpr
forall a b. (a -> b) -> a -> b
$ [String] -> [JExpr] -> [(String, JExpr)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((Int -> String) -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Int -> String
forall a. Show a => a -> String
show [(0::Int)..]) [JExpr]
xs)
typecheck (JRegEx _) = TMonad JType
forall a. HasCallStack => a
undefined
typecheck (JHash mp :: Map String JExpr
mp) = do
Map String JType
mp' <- (JExpr -> TMonad JType)
-> Map String JExpr -> TMonad (Map String JType)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
T.mapM JExpr -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck Map String JExpr
mp
JType
t <- if Map String JType -> Bool
forall k a. Map k a -> Bool
M.null Map String JType
mp'
then JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTImpossible
else [JType] -> TMonad JType
someUpperBound ([JType] -> TMonad JType) -> [JType] -> TMonad JType
forall a b. (a -> b) -> a -> b
$ Map String JType -> [JType]
forall k a. Map k a -> [a]
M.elems Map String JType
mp'
JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return (JType -> TMonad JType) -> JType -> TMonad JType
forall a b. (a -> b) -> a -> b
$ JType -> Map String JType -> JType
JTRecord JType
t Map String JType
mp'
typecheck (JFunc args :: [Ident]
args body :: JStat
body) = do
((argst' :: [JType]
argst',res' :: JType
res'), frame :: Set Int
frame) <- TMonad ([JType], JType) -> TMonad (([JType], JType), Set Int)
forall a. TMonad a -> TMonad (a, Set Int)
withLocalScope (TMonad ([JType], JType) -> TMonad (([JType], JType), Set Int))
-> TMonad ([JType], JType) -> TMonad (([JType], JType), Set Int)
forall a b. (a -> b) -> a -> b
$ do
[JType]
argst <- (Ident -> TMonad JType) -> [Ident] -> TMonad [JType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Ident -> TMonad JType
newVarDecl [Ident]
args
JType
res <- JStat -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JStat
body
([JType], JType) -> TMonad ([JType], JType)
forall (m :: * -> *) a. Monad m => a -> m a
return ([JType]
argst,JType
res)
JType
rt <- JType -> TMonad JType
resolveType (JType -> TMonad JType) -> JType -> TMonad JType
forall a b. (a -> b) -> a -> b
$ [JType] -> JType -> JType
JTFunc [JType]
argst' JType
res'
Set Int
freeVarsInArgs <- [Set Int] -> Set Int
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ([Set Int] -> Set Int) -> TMonad [Set Int] -> TMonad (Set Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (JType -> TMonad (Set Int)) -> [JType] -> TMonad [Set Int]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM JType -> TMonad (Set Int)
freeVars [JType]
argst'
Set Int
freeVarsInRes <- JType -> TMonad (Set Int)
freeVars JType
res'
Set Int -> TMonad ()
setFrozen (Set Int -> TMonad ()) -> Set Int -> TMonad ()
forall a b. (a -> b) -> a -> b
$ Set Int
frame Set Int -> Set Int -> Set Int
forall a. Ord a => Set a -> Set a -> Set a
`S.difference` (Set Int
freeVarsInArgs Set Int -> Set Int -> Set Int
forall a. Ord a => Set a -> Set a -> Set a
`S.intersection` Set Int
freeVarsInRes)
TMonad ()
tryCloseFrozenVars
JType -> TMonad JType
resolveType (JType -> TMonad JType) -> JType -> TMonad JType
forall a b. (a -> b) -> a -> b
$ [VarRef] -> JType -> JType
JTForall (Set Int -> [VarRef]
forall t a. Set t -> [(Maybe a, t)]
frame2VarRefs Set Int
frame) JType
rt
typecheck (UnsatVal _) = TMonad JType
forall a. HasCallStack => a
undefined
instance JTypeCheck JStat where
typecheck :: JStat -> TMonad JType
typecheck (DeclStat ident :: Ident
ident Nothing) = Ident -> TMonad JType
newVarDecl Ident
ident TMonad JType -> TMonad JType -> TMonad JType
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTStat
typecheck (DeclStat ident :: Ident
ident (Just t :: JLocalType
t)) = JLocalType -> TMonad JType
integrateLocalType JLocalType
t TMonad JType -> (JType -> TMonad ()) -> TMonad ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Ident -> JType -> TMonad ()
addEnv Ident
ident TMonad () -> TMonad JType -> TMonad JType
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTStat
typecheck (ReturnStat e :: JExpr
e) = JExpr -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JExpr
e
typecheck (IfStat e :: JExpr
e s :: JStat
s s1 :: JStat
s1) = do
JExpr -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JExpr
e TMonad JType -> TMonad JType -> TMonad ()
<<:> JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTBool
TMonad (TMonad JType) -> TMonad JType
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (TMonad (TMonad JType) -> TMonad JType)
-> TMonad (TMonad JType) -> TMonad JType
forall a b. (a -> b) -> a -> b
$ (JType -> JType -> TMonad JType)
-> TMonad JType -> TMonad JType -> TMonad (TMonad JType)
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (\x :: JType
x y :: JType
y -> [JType] -> TMonad JType
someUpperBound [JType
x,JType
y]) (JStat -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JStat
s) (JStat -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JStat
s1)
typecheck (WhileStat _ e :: JExpr
e s :: JStat
s) = do
JExpr -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JExpr
e TMonad JType -> TMonad JType -> TMonad ()
<<:> JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTBool
JStat -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JStat
s
typecheck (ForInStat _ _ _ _) = TMonad JType
forall a. HasCallStack => a
undefined
typecheck (SwitchStat e :: JExpr
e xs :: [(JExpr, JStat)]
xs d :: JStat
d) = TMonad JType
forall a. HasCallStack => a
undefined
typecheck (TryStat _ _ _ _) = TMonad JType
forall a. HasCallStack => a
undefined
typecheck (BlockStat xs :: [JStat]
xs) = do
[JType]
ts <- (JStat -> TMonad JType) -> [JStat] -> TMonad [JType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM JStat -> TMonad JType
forall a. (JsToDoc a, JMacro a, JTypeCheck a) => a -> TMonad JType
typecheckWithBlock [JStat]
xs
[JType] -> TMonad JType
someUpperBound ([JType] -> TMonad JType) -> [JType] -> TMonad JType
forall a b. (a -> b) -> a -> b
$ [JType] -> [JType]
stripStat [JType]
ts
where stripStat :: [JType] -> [JType]
stripStat (JTStat:ts :: [JType]
ts) = [JType] -> [JType]
stripStat [JType]
ts
stripStat (t :: JType
t:ts :: [JType]
ts) = JType
t JType -> [JType] -> [JType]
forall a. a -> [a] -> [a]
: [JType] -> [JType]
stripStat [JType]
ts
stripStat t :: [JType]
t = [JType]
t
typecheck (ApplStat args :: JExpr
args body :: [JExpr]
body) = JExpr -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck (JExpr -> [JExpr] -> JExpr
ApplExpr JExpr
args [JExpr]
body) TMonad JType -> TMonad JType -> TMonad JType
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTStat
typecheck (PPostStat b :: Bool
b s :: String
s e :: JExpr
e) = JExpr -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck (Bool -> String -> JExpr -> JExpr
PPostExpr Bool
b String
s JExpr
e) TMonad JType -> TMonad JType -> TMonad JType
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTStat
typecheck (AssignStat e :: JExpr
e e1 :: JExpr
e1) = do
JExpr -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JExpr
e1 TMonad JType -> TMonad JType -> TMonad ()
<<:> JExpr -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JExpr
e
JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTStat
typecheck (UnsatBlock _) = TMonad JType
forall a. HasCallStack => a
undefined
typecheck (AntiStat _) = TMonad JType
forall a. HasCallStack => a
undefined
typecheck (BreakStat _) = JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTStat
typecheck (ForeignStat i :: Ident
i t :: JLocalType
t) = JLocalType -> TMonad JType
integrateLocalType JLocalType
t TMonad JType -> (JType -> TMonad ()) -> TMonad ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Ident -> JType -> TMonad ()
addEnv Ident
i TMonad () -> TMonad JType -> TMonad JType
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> JType -> TMonad JType
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTStat
typecheckWithBlock :: (JsToDoc a, JMacro a, JTypeCheck a) => a -> TMonad JType
typecheckWithBlock :: a -> TMonad JType
typecheckWithBlock stat :: a
stat = a -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck a
stat TMonad JType -> TMonad String -> TMonad JType
forall a. TMonad a -> TMonad String -> TMonad a
`withContext` (String -> TMonad String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> TMonad String) -> String -> TMonad String
forall a b. (a -> b) -> a -> b
$ "In statement: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Text -> String
T.unpack (Text -> String) -> (Doc -> Text) -> Doc -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleDoc -> Text
displayT (SimpleDoc -> Text) -> (Doc -> SimpleDoc) -> Doc -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> SimpleDoc
renderCompact (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ a -> Doc
forall a. (JsToDoc a, JMacro a) => a -> Doc
renderJs a
stat))