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