{-# 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 ((<$>))


-- Utility

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' = (a -> ([b], [a]) -> ([b], [a])) -> ([b], [a]) -> [a] -> ([b], [a])
forall a b. (a -> b -> b) -> b -> [a] -> b
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
bb -> [b] -> [b]
forall a. a -> [a] -> [a]
:[b]
bs,[a]
as)
             | Bool
otherwise = ([b]
bs,a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
as)

zipWithOrChange :: (a -> a -> b) -> (a -> b) -> [a] -> [a] -> [b]
zipWithOrChange :: 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 b -> [b] -> [b]
forall a. a -> [a] -> [a]
: [a] -> [a] -> [b]
go [a]
xs [a]
ys
          go xs :: [a]
xs@(a
_:[a]
_) [a]
_ = (a -> b) -> [a] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map a -> b
g [a]
xs
          go [a]
_ [a]
ys = (a -> b) -> [a] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map a -> b
g [a]
ys

zipWithOrIdM :: Monad m => (a -> a -> m a) -> [a] -> [a] -> m [a]
zipWithOrIdM :: forall (m :: * -> *) a.
Monad m =>
(a -> a -> m a) -> [a] -> [a] -> m [a]
zipWithOrIdM a -> a -> m a
f [a]
xs [a]
ys = [m a] -> m [a]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence ([m a] -> m [a]) -> [m a] -> m [a]
forall a b. (a -> b) -> a -> b
$ (a -> a -> m a) -> (a -> m a) -> [a] -> [a] -> [m a]
forall a b. (a -> a -> b) -> (a -> b) -> [a] -> [a] -> [b]
zipWithOrChange a -> a -> m a
f a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return [a]
xs [a]
ys

unionWithM :: (Monad m, Ord key) => (val -> val -> m val) -> Map key val -> Map key val -> m (Map key val)
unionWithM :: 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 = Map key (m val) -> m (Map key val)
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => Map key (m a) -> m (Map key a)
T.sequence (Map key (m val) -> m (Map key val))
-> Map key (m val) -> m (Map key val)
forall a b. (a -> b) -> a -> b
$ (m val -> m val -> m val)
-> Map key (m val) -> Map key (m val) -> Map key (m val)
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith (\m val
xm m val
ym -> m (m val) -> m val
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (m (m val) -> m val) -> m (m val) -> m val
forall a b. (a -> b) -> a -> b
$ (val -> val -> m val) -> m val -> m val -> m (m val)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 val -> val -> m val
f m val
xm m val
ym) ((val -> m val) -> Map key val -> Map key (m val)
forall a b k. (a -> b) -> Map k a -> Map k b
M.map val -> m val
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Map key val
m1) ((val -> m val) -> Map key val -> Map key (m val)
forall a b k. (a -> b) -> Map k a -> Map k b
M.map val -> m val
forall a. a -> m a
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 = Map key (m b) -> m (Map key b)
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => Map key (m a) -> m (Map key a)
T.sequence (Map key (m b) -> m (Map key b)) -> Map key (m b) -> m (Map key b)
forall a b. (a -> b) -> a -> b
$ (val -> val -> m b) -> Map key val -> Map key val -> Map key (m b)
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith val -> val -> m b
f Map key val
m1 Map key val
m2

class Compos1 t where
    compos1 :: (forall a. a -> m a) -> (forall a b. m (a -> b) -> m a -> m b)
           -> (t -> m t) -> t -> m t

instance Compos1 JType where
    compos1 :: forall (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 -> ([JType] -> JType -> JType) -> m ([JType] -> JType -> JType)
forall a. a -> m a
ret [JType] -> JType -> JType
JTFunc m ([JType] -> JType -> JType) -> m [JType] -> m (JType -> JType)
forall a b. m (a -> b) -> m a -> m b
`app` (JType -> m JType) -> [JType] -> m [JType]
forall {t :: * -> *} {a} {a}.
Foldable t =>
(a -> m a) -> t a -> m [a]
mapM' JType -> m JType
f [JType]
args m (JType -> JType) -> m JType -> m JType
forall a b. m (a -> b) -> m a -> m b
`app` JType -> m JType
f JType
body
          JTForall [VarRef]
vars JType
t -> ([VarRef] -> JType -> JType) -> m ([VarRef] -> JType -> JType)
forall a. a -> m a
ret [VarRef] -> JType -> JType
JTForall m ([VarRef] -> JType -> JType) -> m [VarRef] -> m (JType -> JType)
forall a b. m (a -> b) -> m a -> m b
`app` [VarRef] -> m [VarRef]
forall a. a -> m a
ret [VarRef]
vars m (JType -> JType) -> m JType -> m JType
forall a b. m (a -> b) -> m a -> m b
`app` JType -> m JType
f JType
t
          JTList JType
t -> (JType -> JType) -> m (JType -> JType)
forall a. a -> m a
ret JType -> JType
JTList m (JType -> JType) -> m JType -> m JType
forall a b. m (a -> b) -> m a -> m b
`app` JType -> m JType
f JType
t
          JTMap JType
t -> (JType -> JType) -> m (JType -> JType)
forall a. a -> m a
ret JType -> JType
JTMap m (JType -> JType) -> m JType -> m JType
forall a b. m (a -> b) -> m a -> m b
`app` JType -> m JType
f JType
t
          JTRecord JType
t Map String JType
m -> (JType -> Map String JType -> JType)
-> m (JType -> Map String JType -> JType)
forall a. a -> m a
ret JType -> Map String JType -> JType
JTRecord m (JType -> Map String JType -> JType)
-> m JType -> m (Map String JType -> JType)
forall a b. m (a -> b) -> m a -> m b
`app` JType -> m JType
f JType
t m (Map String JType -> JType) -> m (Map String JType) -> m JType
forall a b. m (a -> b) -> m a -> m b
`app` m (Map String JType)
m'
              where ([String]
ls,[JType]
ts) = [(String, JType)] -> ([String], [JType])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(String, JType)] -> ([String], [JType]))
-> [(String, JType)] -> ([String], [JType])
forall a b. (a -> b) -> a -> b
$ Map String JType -> [(String, JType)]
forall k a. Map k a -> [(k, a)]
M.toList Map String JType
m
                    m' :: m (Map String JType)
m' = ([JType] -> Map String JType) -> m ([JType] -> Map String JType)
forall a. a -> m a
ret ([(String, JType)] -> Map String JType
forall k a. Eq k => [(k, a)] -> Map k a
M.fromAscList ([(String, JType)] -> Map String JType)
-> ([JType] -> [(String, JType)]) -> [JType] -> Map String JType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> [JType] -> [(String, JType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [String]
ls) m ([JType] -> Map String JType)
-> m [JType] -> m (Map String JType)
forall a b. m (a -> b) -> m a -> m b
`app` (JType -> m JType) -> [JType] -> m [JType]
forall {t :: * -> *} {a} {a}.
Foldable t =>
(a -> m a) -> t a -> m [a]
mapM' JType -> m JType
f [JType]
ts
          JType
x -> JType -> m JType
forall a. a -> m a
ret JType
x
      where
        mapM' :: (a -> m a) -> t a -> m [a]
mapM' a -> m a
g = (a -> m [a] -> m [a]) -> m [a] -> t a -> m [a]
forall a b. (a -> b -> b) -> b -> t a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (m ([a] -> [a]) -> m [a] -> m [a]
forall a b. m (a -> b) -> m a -> m b
app (m ([a] -> [a]) -> m [a] -> m [a])
-> (a -> m ([a] -> [a])) -> a -> m [a] -> m [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (a -> [a] -> [a]) -> m a -> m ([a] -> [a])
forall a b. m (a -> b) -> m a -> m b
app ((a -> [a] -> [a]) -> m (a -> [a] -> [a])
forall a. a -> m a
ret (:)) (m a -> m ([a] -> [a])) -> (a -> m a) -> a -> m ([a] -> [a])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> m a
g) ([a] -> m [a]
forall a. a -> m a
ret [])

composOp1 :: Compos1 t => (t -> t) -> t -> t
composOp1 :: forall t. Compos1 t => (t -> t) -> t -> t
composOp1 t -> t
f = Identity t -> t
forall a. Identity a -> a
runIdentity (Identity t -> t) -> (t -> Identity t) -> t -> t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (t -> Identity t) -> t -> Identity t
forall t (m :: * -> *).
(Compos1 t, Monad m) =>
(t -> m t) -> t -> m t
composOpM1 (t -> Identity t
forall a. a -> Identity a
Identity (t -> Identity t) -> (t -> t) -> t -> Identity t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> t
f)
composOpM1 :: (Compos1 t, Monad m) => (t -> m t) -> t -> m t
composOpM1 :: forall t (m :: * -> *).
(Compos1 t, Monad m) =>
(t -> m t) -> t -> m t
composOpM1 = (forall a. a -> m a)
-> (forall a b. m (a -> b) -> m a -> m b) -> (t -> m t) -> t -> m t
forall t (m :: * -> *).
Compos1 t =>
(forall a. a -> m a)
-> (forall a b. m (a -> b) -> m a -> m b) -> (t -> m t) -> t -> m t
forall (m :: * -> *).
(forall a. a -> m a)
-> (forall a b. m (a -> b) -> m a -> m b) -> (t -> m t) -> t -> m t
compos1 a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return m (a -> b) -> m a -> m b
forall a b. m (a -> b) -> m a -> m b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
composOpM1_ :: (Compos1 t, Monad m) => (t -> m ()) -> t -> m ()
composOpM1_ :: forall t (m :: * -> *).
(Compos1 t, Monad m) =>
(t -> m ()) -> t -> m ()
composOpM1_ = m () -> (m () -> m () -> m ()) -> (t -> m ()) -> t -> m ()
forall t b. Compos1 t => b -> (b -> b -> b) -> (t -> b) -> t -> b
composOpFold1 (() -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) m () -> m () -> m ()
forall a b. m a -> m b -> m b
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 = C b t -> b
forall b a. C b a -> b
unC (C b t -> b) -> (t -> C b t) -> t -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. a -> C b a)
-> (forall a b. C b (a -> b) -> C b a -> C b b)
-> (t -> C b t)
-> t
-> C b t
forall t (m :: * -> *).
Compos1 t =>
(forall a. a -> m a)
-> (forall a b. m (a -> b) -> m a -> m b) -> (t -> m t) -> t -> m t
forall (m :: * -> *).
(forall a. a -> m a)
-> (forall a b. m (a -> b) -> m a -> m b) -> (t -> m t) -> t -> m t
compos1 (\a
_ -> b -> C b a
forall b a. b -> C b a
C b
z) (\(C b
x) (C b
y) -> b -> C b b
forall b a. b -> C b a
C (b -> b -> b
c b
x b
y)) (b -> C b t
forall b a. b -> C b a
C (b -> C b t) -> (t -> b) -> t -> C b t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> b
f)
newtype C b a = C { forall b a. C b a -> b
unC :: b }

-- Basic Types and TMonad
data StoreVal = SVType JType
              | SVConstrained (Set Constraint)
                deriving Int -> StoreVal -> ShowS
[StoreVal] -> ShowS
StoreVal -> String
(Int -> StoreVal -> ShowS)
-> (StoreVal -> String) -> ([StoreVal] -> ShowS) -> Show StoreVal
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> StoreVal -> ShowS
showsPrec :: Int -> StoreVal -> ShowS
$cshow :: StoreVal -> String
show :: StoreVal -> String
$cshowList :: [StoreVal] -> ShowS
showList :: [StoreVal] -> ShowS
Show
              {- -- | SVFreshType Int -}

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: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Map Ident JType] -> String
forall a. Show a => a -> String
show [Map Ident JType]
env String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
        String
"vars: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Map Int StoreVal -> String
forall a. Show a => a -> String
show Map Int StoreVal
vars String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
        String
"stack: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Set Int] -> String
forall a. Show a => a -> String
show [Set Int]
stack String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
        String
"frozen: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Set Int -> String
forall a. Show a => a -> String
show Set Int
frozen String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
        String
"varCt: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
varCt

tcStateEmpty :: TCState
tcStateEmpty :: TCState
tcStateEmpty = [Map Ident JType]
-> Map Int StoreVal
-> [Set Int]
-> Set Int
-> Int
-> [TMonad String]
-> TCState
TCS [Map Ident JType
forall k a. Map k a
M.empty] Map Int StoreVal
forall k a. Map k a
M.empty [Set Int
forall a. Set a
S.empty] Set Int
forall a. Set a
S.empty Int
0 []

newtype TMonad a = TMonad (ExceptT String (State TCState) a) deriving ((forall a b. (a -> b) -> TMonad a -> TMonad b)
-> (forall a b. a -> TMonad b -> TMonad a) -> Functor TMonad
forall a b. a -> TMonad b -> TMonad a
forall a b. (a -> b) -> TMonad a -> TMonad b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> TMonad a -> TMonad b
fmap :: forall a b. (a -> b) -> TMonad a -> TMonad b
$c<$ :: forall a b. a -> TMonad b -> TMonad a
<$ :: forall a b. a -> TMonad b -> TMonad a
Functor, Applicative TMonad
Applicative TMonad =>
(forall a b. TMonad a -> (a -> TMonad b) -> TMonad b)
-> (forall a b. TMonad a -> TMonad b -> TMonad b)
-> (forall a. a -> TMonad a)
-> Monad TMonad
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
$c>>= :: forall a b. TMonad a -> (a -> TMonad b) -> TMonad b
>>= :: forall a b. TMonad a -> (a -> TMonad b) -> TMonad b
$c>> :: forall a b. TMonad a -> TMonad b -> TMonad b
>> :: forall a b. TMonad a -> TMonad b -> TMonad b
$creturn :: forall a. a -> TMonad a
return :: forall a. a -> TMonad a
Monad, MonadState TCState, MonadError String)

instance Applicative TMonad where
    pure :: forall a. a -> TMonad a
pure = a -> TMonad a
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return
    <*> :: forall a b. TMonad (a -> b) -> TMonad a -> TMonad b
(<*>) = TMonad (a -> b) -> TMonad a -> TMonad b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

class JTypeCheck a where
    typecheck :: a -> TMonad JType

evalTMonad :: TMonad a -> Either String a
evalTMonad :: forall a. TMonad a -> Either String a
evalTMonad (TMonad ExceptT String (State TCState) a
x) = State TCState (Either String a) -> TCState -> Either String a
forall s a. State s a -> s -> a
evalState (ExceptT String (State TCState) a -> State TCState (Either String a)
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) = State TCState (Either String a)
-> TCState -> (Either String a, TCState)
forall s a. State s a -> s -> (a, s)
runState (ExceptT String (State TCState) a -> State TCState (Either String a)
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
  cs <- TCState -> [TMonad String]
tc_context (TCState -> [TMonad String])
-> TMonad TCState -> TMonad [TMonad String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TMonad TCState
forall s (m :: * -> *). MonadState s m => m s
get
  modify (\TCState
s -> TCState
s {tc_context = cxt : cs})
  res <- act
  modify (\TCState
s -> TCState
s {tc_context = cs})
  return 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 = (a -> f () -> f ()) -> f () -> t a -> f ()
forall a b. (a -> b -> b) -> b -> t a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
F.foldr (f b -> f () -> f ()
forall a b. f a -> f b -> f b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
(>>) (f b -> f () -> f ()) -> (a -> f b) -> a -> f () -> f ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> f b
f) (() -> f ()
forall a. a -> f a
forall (m :: * -> *) a. Monad m => a -> m a
return ())

--assums x is resolved
freeVarsWithNames :: JType -> TMonad (Map Int String)
freeVarsWithNames :: JType -> TMonad (Map Int String)
freeVarsWithNames JType
x =
  Map Int (Either String Int) -> Map Int String
forall {k}. Map k (Either String Int) -> Map k String
intsToNames (Map Int (Either String Int) -> Map Int String)
-> ((Map Int (Either String Int), Set String, Int)
    -> Map Int (Either String Int))
-> (Map Int (Either String Int), Set String, Int)
-> Map Int String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(Map Int (Either String Int)
a,Set String
_,Int
_) -> Map Int (Either String Int)
a) ((Map Int (Either String Int), Set String, Int) -> Map Int String)
-> TMonad (Map Int (Either String Int), Set String, Int)
-> TMonad (Map Int String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
       StateT (Map Int (Either String Int), Set String, Int) TMonad ()
-> (Map Int (Either String Int), Set String, Int)
-> TMonad (Map Int (Either String Int), Set String, Int)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT (JType
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
go JType
x) (Map Int (Either String Int)
forall k a. Map k a
M.empty, Set String
forall a. Set a
S.empty, 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 StateT (Map Int (Either String Int), Set String, Int) TMonad ()
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
forall a b.
StateT (Map Int (Either String Int), Set String, Int) TMonad a
-> StateT (Map Int (Either String Int), Set String, Int) TMonad b
-> StateT (Map Int (Either String Int), Set String, Int) TMonad b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Constraint
 -> StateT (Map Int (Either String Int), Set String, Int) TMonad ())
-> Set Constraint
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Monad f) =>
(a -> f b) -> t a -> f ()
traversem_ (JType
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
go (JType
 -> StateT (Map Int (Either String Int), Set String, Int) TMonad ())
-> (Constraint -> JType)
-> Constraint
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constraint -> JType
fromC) Set Constraint
cs
      go JType
v = (JType
 -> StateT (Map Int (Either String Int), Set String, Int) TMonad ())
-> JType
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
forall t (m :: * -> *).
(Compos1 t, Monad m) =>
(t -> m ()) -> t -> m ()
composOpM1_ JType
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
go JType
v

      handleVR :: VarRef
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
handleVR (Maybe String
mbName, Int
ref) = do
        (m,ns,ct) <- StateT
  (Map Int (Either String Int), Set String, Int)
  TMonad
  (Map Int (Either String Int), Set String, Int)
forall s (m :: * -> *). MonadState s m => m s
get
        case M.lookup ref m of
          Just (Left String
_) -> ()
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
forall a.
a -> StateT (Map Int (Either String Int), Set String, Int) TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
          Just (Right Int
_) -> case Maybe String
mbName of
                              Just String
name -> String
-> Int
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
forall {m :: * -> *} {k} {b} {c}.
(MonadState (Map k (Either String b), Set String, c) m, Ord k) =>
String -> k -> m ()
putName String
name Int
ref
                              Maybe String
Nothing -> ()
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
forall a.
a -> StateT (Map Int (Either String Int), Set String, Int) TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
          Maybe (Either String Int)
Nothing -> do
            case Maybe String
mbName of
              Just String
name -> String
-> Int
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
forall {m :: * -> *} {k} {b} {c}.
(MonadState (Map k (Either String b), Set String, c) m, Ord k) =>
String -> k -> m ()
putName String
name Int
ref
              Maybe String
Nothing -> (Map Int (Either String Int), Set String, Int)
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
-> Either String Int
-> Map Int (Either String Int)
-> Map Int (Either String Int)
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Int
ref (Int -> Either String Int
forall a b. b -> Either a b
Right Int
ct) Map Int (Either String Int)
m, Set String
ns, Int
ct Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
            (Constraint
 -> StateT (Map Int (Either String Int), Set String, Int) TMonad ())
-> [Constraint]
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Monad f) =>
(a -> f b) -> t a -> f ()
mapM_ (JType
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
go (JType
 -> StateT (Map Int (Either String Int), Set String, Int) TMonad ())
-> (Constraint -> JType)
-> Constraint
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constraint -> JType
fromC) ([Constraint]
 -> StateT (Map Int (Either String Int), Set String, Int) TMonad ())
-> StateT
     (Map Int (Either String Int), Set String, Int) TMonad [Constraint]
-> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TMonad [Constraint]
-> StateT
     (Map Int (Either String Int), Set String, Int) TMonad [Constraint]
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (Map Int (Either String Int), Set String, Int) m a
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
        (m,ns,ct) <- m (Map k (Either String b), Set String, c)
forall s (m :: * -> *). MonadState s m => m s
get
        let n' = Set String -> String -> Int -> String
mkUnique Set String
ns String
n Int
0
        put (M.insert ref (Left n') m, S.insert n' ns, ct)

      mkUnique :: Set String -> String -> Int -> String
      mkUnique :: Set String -> String -> Int -> String
mkUnique Set String
ns String
n Int
i
          | String
n' String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set String
ns = Set String -> String -> Int -> String
mkUnique Set String
ns String
n (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
          | Bool
otherwise = String
n'
          where n' :: String
n' | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = String
n
                   | Bool
otherwise = String
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i

      fromC :: Constraint -> JType
fromC (Sub 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 = (Either String Int -> String)
-> Map k (Either String Int) -> Map k String
forall a b. (a -> b) -> Map k a -> Map k b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ShowS -> (Int -> String) -> Either String Int -> String
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ShowS
forall a. a -> a
id Int -> String
go) Map k (Either String Int)
x
          where go :: Int -> String
go Int
i = Set String -> String -> Int -> String
mkUnique ([String] -> Set String
forall a. Ord a => [a] -> Set a
S.fromList ([String] -> Set String) -> [String] -> Set String
forall a b. (a -> b) -> a -> b
$ [Either String Int] -> [String]
forall a b. [Either a b] -> [a]
lefts ([Either String Int] -> [String])
-> [Either String Int] -> [String]
forall a b. (a -> b) -> a -> b
$ Map k (Either String Int) -> [Either String Int]
forall k a. Map k a -> [a]
M.elems Map k (Either String Int)
x) (Int -> String
int2Name Int
i) Int
0
                int2Name :: Int -> String
int2Name Int
i | Int
q Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = [Char
letter]
                           | Bool
otherwise = Char
letter Char -> ShowS
forall a. a -> [a] -> [a]
: Int -> String
forall a. Show a => a -> String
show Int
q
                    where (Int
q,Int
r) = Int -> Int -> (Int, Int)
forall a. Integral a => a -> a -> (a, a)
divMod Int
i Int
26
                          letter :: Char
letter = Int -> Char
forall a. Enum a => Int -> a
toEnum (Char -> Int
forall a. Enum a => a -> Int
fromEnum Char
'a' Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
r)


prettyType :: JType -> TMonad String
prettyType :: JType -> TMonad String
prettyType JType
x = do
  xt <- JType -> TMonad JType
resolveType JType
x
  names <- freeVarsWithNames xt
  let replaceNames (JTFree VarRef
ref) = VarRef -> JType
JTFree (VarRef -> JType) -> VarRef -> JType
forall a b. (a -> b) -> a -> b
$ VarRef -> VarRef
forall {a}. (a, Int) -> VarRef
fixRef VarRef
ref
      replaceNames (JTForall [VarRef]
refs JType
t) = [VarRef] -> JType -> JType
JTForall ((VarRef -> VarRef) -> [VarRef] -> [VarRef]
forall a b. (a -> b) -> [a] -> [b]
map VarRef -> VarRef
forall {a}. (a, Int) -> VarRef
fixRef [VarRef]
refs) (JType -> JType) -> JType -> JType
forall a b. (a -> b) -> a -> b
$ JType -> JType
replaceNames JType
t
      replaceNames JType
v = (JType -> JType) -> JType -> JType
forall t. Compos1 t => (t -> t) -> t -> t
composOp1 JType -> JType
replaceNames JType
v

      fixRef (a
_,Int
ref) = (Int -> Map Int String -> Maybe String
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Int
ref Map Int String
names, Int
ref)

      prettyConstraints Int
ref = (Constraint -> String) -> [Constraint] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Constraint -> String
go ([Constraint] -> [String])
-> TMonad [Constraint] -> TMonad [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VarRef -> TMonad [Constraint]
lookupConstraintsList (Maybe String
forall a. Maybe a
Nothing, Int
ref)
          where
            myName :: String
myName = case Int -> Map Int String -> Maybe String
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Int
ref Map Int String
names of
                       Just String
n -> String
n
                       Maybe String
Nothing -> String
"t_"String -> ShowS
forall a. [a] -> [a] -> [a]
++Int -> String
forall a. Show a => a -> String
show Int
ref
            go :: Constraint -> String
go (Sub JType
t) = String
myName String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" <: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ JType -> Doc
forall a. JsToDoc a => a -> Doc
jsToDoc (JType -> Doc) -> JType -> Doc
forall a b. (a -> b) -> a -> b
$ JType -> JType
replaceNames JType
t)
            go (Super JType
t) = (Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ JType -> Doc
forall a. JsToDoc a => a -> Doc
jsToDoc (JType -> Doc) -> JType -> Doc
forall a b. (a -> b) -> a -> b
$ JType -> JType
replaceNames JType
t) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" <: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
myName

  constraintStrings <- nub . concat <$> mapM prettyConstraints (M.keys names)

  let constraintStr
          | [String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
constraintStrings = String
""
          | Bool
otherwise = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " [String]
constraintStrings String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
") => "

  return $ constraintStr ++ (show . jsToDoc $ replaceNames xt)

tyErr0 :: String -> TMonad a
tyErr0 :: forall a. String -> TMonad a
tyErr0 String
x = String -> TMonad a
forall a. String -> TMonad a
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
  st <- JType -> TMonad String
prettyType JType
t
  throwError $ s ++ ": " ++ 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
  st <- JType -> TMonad String
prettyType JType
t
  st' <- prettyType t'
  throwError $ s ++ ". " ++ s1 ++ ": " ++ st ++ ", " ++ s2 ++ ": " ++ st'

tyErr2Sub :: JType -> JType -> TMonad a
tyErr2Sub :: forall a. JType -> JType -> TMonad a
tyErr2Sub JType
t JType
t' = String -> String -> String -> JType -> JType -> TMonad a
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 = (Map Ident JType -> TMonad (Map Ident String))
-> [Map Ident JType] -> TMonad [Map Ident String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((JType -> TMonad String)
-> Map Ident JType -> TMonad (Map Ident String)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Map Ident a -> m (Map Ident b)
T.mapM JType -> TMonad String
prettyType) ([Map Ident JType] -> TMonad [Map Ident String])
-> (TCState -> [Map Ident JType])
-> TCState
-> TMonad [Map Ident String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCState -> [Map Ident JType]
tc_env (TCState -> TMonad [Map Ident String])
-> TMonad TCState -> TMonad [Map Ident String]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TMonad TCState
forall s (m :: * -> *). MonadState s m => m s
get

runTypecheckRaw :: JTypeCheck a => a -> (Either String JType, TCState)
runTypecheckRaw :: forall a. JTypeCheck a => a -> (Either String JType, TCState)
runTypecheckRaw a
x = TMonad JType -> (Either String JType, TCState)
forall a. TMonad a -> (Either String a, TCState)
runTMonad (a -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheckMain a
x)

runTypecheckFull :: JTypeCheck a => a -> (Either String (String, [Map Ident String]), TCState)
runTypecheckFull :: forall a.
JTypeCheck a =>
a -> (Either String (String, [Map Ident String]), TCState)
runTypecheckFull a
x = TMonad (String, [Map Ident String])
-> (Either String (String, [Map Ident String]), TCState)
forall a. TMonad a -> (Either String a, TCState)
runTMonad (TMonad (String, [Map Ident String])
 -> (Either String (String, [Map Ident String]), TCState))
-> TMonad (String, [Map Ident String])
-> (Either String (String, [Map Ident String]), TCState)
forall a b. (a -> b) -> a -> b
$ do
                       r <- JType -> TMonad String
prettyType (JType -> TMonad String) -> TMonad JType -> TMonad String
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< a -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheckMain a
x
                       e <- prettyEnv
                       return (r,e)

runTypecheck :: JTypeCheck a => a -> Either String String
runTypecheck :: forall a. JTypeCheck a => a -> Either String String
runTypecheck a
x = TMonad String -> Either String String
forall a. TMonad a -> Either String a
evalTMonad (TMonad String -> Either String String)
-> TMonad String -> Either String String
forall a b. (a -> b) -> a -> b
$ JType -> TMonad String
prettyType (JType -> TMonad String) -> TMonad JType -> TMonad String
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< a -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheckMain a
x

evalTypecheck :: JTypeCheck a => a -> Either String [Map Ident String]
evalTypecheck :: forall a. JTypeCheck a => a -> Either String [Map Ident String]
evalTypecheck a
x = TMonad [Map Ident String] -> Either String [Map Ident String]
forall a. TMonad a -> Either String a
evalTMonad (TMonad [Map Ident String] -> Either String [Map Ident String])
-> TMonad [Map Ident String] -> Either String [Map Ident String]
forall a b. (a -> b) -> a -> b
$ do
                    _ <- a -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheckMain a
x
                    e <- prettyEnv
                    return e

typecheckMain :: JTypeCheck a => a -> TMonad JType
typecheckMain :: forall a. JTypeCheck a => a -> TMonad JType
typecheckMain a
x = TMonad JType
go TMonad JType -> (String -> TMonad JType) -> TMonad JType
forall a. TMonad a -> (String -> TMonad a) -> TMonad a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` String -> TMonad JType
forall a. String -> TMonad a
handler
    where go :: TMonad JType
go = do
            r <- a -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck a
x
            setFrozen . S.unions . tc_stack =<< get
            tryCloseFrozenVars
            return r
          handler :: String -> TMonad b
handler String
e = do
                 cxt <- TCState -> [TMonad String]
tc_context (TCState -> [TMonad String])
-> TMonad TCState -> TMonad [TMonad String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TMonad TCState
forall s (m :: * -> *). MonadState s m => m s
get
                 throwError =<< (unlines . (e:) <$> sequence cxt)

-- Manipulating VarRefs and Constraints

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) = a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
S.insert a
v Set a
s Set a -> [Set a] -> [Set a]
forall a. a -> [a] -> [a]
: [Set a]
ss
addToStack a
_ [Set a]
_ = String -> [Set a]
forall a. HasCallStack => String -> a
error String
"addToStack: no sets" --[S.singleton v]

newVarRef :: TMonad VarRef
newVarRef :: TMonad VarRef
newVarRef = do
  v <- TCState -> Int
tc_varCt (TCState -> Int) -> TMonad TCState -> TMonad Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TMonad TCState
forall s (m :: * -> *). MonadState s m => m s
get
  modify (\TCState
s -> TCState
s {tc_varCt = v + 1,
                   tc_stack = addToStack v (tc_stack s)})
  return $ (Nothing, v)

newTyVar :: TMonad JType
newTyVar :: TMonad JType
newTyVar = VarRef -> JType
JTFree (VarRef -> JType) -> TMonad VarRef -> TMonad JType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TMonad VarRef
newVarRef

mapConstraint :: (Monad m, Functor m) => (JType -> m JType) -> Constraint -> m Constraint
mapConstraint :: forall (m :: * -> *).
(Monad m, Functor m) =>
(JType -> m JType) -> Constraint -> m Constraint
mapConstraint JType -> m JType
f (Sub JType
t) = JType -> Constraint
Sub (JType -> Constraint) -> m JType -> m Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> JType -> m JType
f JType
t
mapConstraint JType -> m JType
f (Super JType
t) = JType -> Constraint
Super (JType -> Constraint) -> m JType -> m Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> JType -> m JType
f JType
t

partitionCs :: [Constraint] -> ([JType],[JType])
partitionCs :: [Constraint] -> ([JType], [JType])
partitionCs [] = ([],[])
partitionCs (Sub JType
t:[Constraint]
cs) = (JType
tJType -> [JType] -> [JType]
forall 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
tJType -> [JType] -> [JType]
forall a. a -> [a] -> [a]
:[JType]
sups)
    where ([JType]
subs,[JType]
sups) = [Constraint] -> ([JType], [JType])
partitionCs [Constraint]
cs


--add mutation
lookupConstraintsList :: VarRef -> TMonad [Constraint]
lookupConstraintsList :: VarRef -> TMonad [Constraint]
lookupConstraintsList vr :: VarRef
vr@(Maybe String
_,Int
ref) = do
    vars <- TCState -> Map Int StoreVal
tc_vars (TCState -> Map Int StoreVal)
-> TMonad TCState -> TMonad (Map Int StoreVal)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TMonad TCState
forall s (m :: * -> *). MonadState s m => m s
get
    case M.lookup ref vars of
      (Just (SVConstrained Set Constraint
cs)) -> (Constraint -> Bool) -> [Constraint] -> [Constraint]
forall a. (a -> Bool) -> [a] -> [a]
filter Constraint -> Bool
notLoop ([Constraint] -> [Constraint])
-> ([Constraint] -> [Constraint]) -> [Constraint] -> [Constraint]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Constraint] -> [Constraint]
forall a. Eq a => [a] -> [a]
nub ([Constraint] -> [Constraint])
-> TMonad [Constraint] -> TMonad [Constraint]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Constraint -> TMonad Constraint)
-> [Constraint] -> TMonad [Constraint]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((JType -> TMonad JType) -> Constraint -> TMonad Constraint
forall (m :: * -> *).
(Monad m, Functor m) =>
(JType -> m JType) -> Constraint -> m Constraint
mapConstraint JType -> TMonad JType
resolveType) (Set Constraint -> [Constraint]
forall a. Set a -> [a]
S.toList Set Constraint
cs)
      (Just (SVType JType
t)) -> String -> JType -> TMonad [Constraint]
forall b. String -> JType -> TMonad b
tyErr1 String
"lookupConstraints on instantiated type" JType
t
      Maybe StoreVal
Nothing -> [Constraint] -> TMonad [Constraint]
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return []
  where
    notLoop :: Constraint -> Bool
notLoop (Super (JTFree (Maybe String
_,Int
ref'))) | Int
ref Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ref' = Bool
False
    notLoop (Sub   (JTFree (Maybe String
_,Int
ref'))) | Int
ref Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ref' = Bool
False
    notLoop Constraint
_ = Bool
True

-- if we instantiate a var to itself, then there's a good chance this results from a looping constraint -- we should be helpful and get rid of any such constraints.
instantiateVarRef :: VarRef -> JType -> TMonad ()
instantiateVarRef :: VarRef -> JType -> TMonad ()
instantiateVarRef vr :: VarRef
vr@(Maybe String
_,Int
ref) (JTFree (Maybe String
_,Int
ref')) | Int
ref Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ref' = do
    cs <- VarRef -> TMonad [Constraint]
lookupConstraintsList VarRef
vr
    let cs' = [Constraint] -> [Constraint]
simplify [Constraint]
cs
    modify (\TCState
s -> TCState
s {tc_vars = M.insert ref (SVConstrained (S.fromList cs')) (tc_vars s)})
  where simplify :: [Constraint] -> [Constraint]
simplify (Sub   (JTFree (Maybe String
_,Int
r)):[Constraint]
cs) | Int
r Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ref = [Constraint]
cs
        simplify (Super (JTFree (Maybe String
_,Int
r)):[Constraint]
cs) | Int
r Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ref = [Constraint]
cs
        simplify (Constraint
c:[Constraint]
cs) = Constraint
c Constraint -> [Constraint] -> [Constraint]
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
  cs <- VarRef -> TMonad [Constraint]
lookupConstraintsList VarRef
vr
  modify (\TCState
s -> TCState
s {tc_vars = M.insert ref (SVType t) (tc_vars s)})
  checkConstraints t cs

occursCheck :: Int -> JType -> TMonad ()
occursCheck :: Int -> JType -> TMonad ()
occursCheck Int
ref (JTFree (Maybe String
_,Int
i))
  | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ref = String -> JType -> TMonad ()
forall b. String -> JType -> TMonad b
tyErr1 String
"Occurs check: cannot construct infinite type" (VarRef -> JType
JTFree (Maybe String
forall a. Maybe a
Nothing,Int
i))
occursCheck Int
ref JType
x = (JType -> TMonad ()) -> JType -> TMonad ()
forall t (m :: * -> *).
(Compos1 t, Monad m) =>
(t -> m ()) -> t -> m ()
composOpM1_ (Int -> JType -> TMonad ()
occursCheck Int
ref) JType
x

checkConstraints :: JType -> [Constraint] -> TMonad ()
checkConstraints :: JType -> [Constraint] -> TMonad ()
checkConstraints JType
t [Constraint]
cs = (Constraint -> TMonad ()) -> [Constraint] -> TMonad ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Monad f) =>
(a -> f b) -> t a -> f ()
mapM_ Constraint -> TMonad ()
go [Constraint]
cs
    where go :: Constraint -> TMonad ()
go (Sub 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 ([Constraint] -> TMonad ())
-> ([Constraint] -> [Constraint]) -> [Constraint] -> TMonad ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Constraint
c Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
: ) ([Constraint] -> TMonad ()) -> TMonad [Constraint] -> TMonad ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< VarRef -> TMonad [Constraint]
lookupConstraintsList VarRef
vr

                  JTFunc [JType]
args JType
res -> do
                         (JType -> TMonad ()) -> [JType] -> TMonad ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Monad f) =>
(a -> f b) -> t a -> f ()
mapM_ (Int -> JType -> TMonad ()
occursCheck Int
ref) (JType
resJType -> [JType] -> [JType]
forall a. a -> [a] -> [a]
:[JType]
args)
                         [Constraint] -> TMonad ()
normalizeConstraints ([Constraint] -> TMonad ())
-> ([Constraint] -> [Constraint]) -> [Constraint] -> TMonad ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Constraint
c Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
:) ([Constraint] -> TMonad ()) -> TMonad [Constraint] -> TMonad ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< VarRef -> TMonad [Constraint]
lookupConstraintsList VarRef
vr

                  JTRecord JType
t Map String JType
m -> Int -> JType -> TMonad ()
occursCheck Int
ref JType
t TMonad () -> TMonad () -> TMonad ()
forall a b. TMonad a -> TMonad b -> TMonad b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
                                  (JType -> TMonad ()) -> Map String JType -> TMonad ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Monad f) =>
(a -> f b) -> t a -> f ()
F.mapM_ (Int -> JType -> TMonad ()
occursCheck Int
ref) Map String JType
m TMonad () -> TMonad () -> TMonad ()
forall a b. TMonad a -> TMonad b -> TMonad b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
                                  Either (Map String JType, JType) (Map String JType, JType)
-> TMonad ()
addRecConstraint ((Map String JType, JType)
-> Either (Map String JType, JType) (Map String JType, JType)
forall a b. a -> Either a b
Left (Map String JType
m,JType
t))

                  JTList JType
t' -> do
                         vr' <- TMonad VarRef
newVarRef
                         addConstraint vr' (Sub t')
                         instantiateVarRef vr (JTList (JTFree vr'))

                  JTMap JType
t' -> do
                         vr' <- TMonad VarRef
newVarRef
                         addConstraint vr' (Sub t')
                         instantiateVarRef vr (JTMap (JTFree vr'))

                  JTRigid VarRef
_ Set Constraint
cs -> do
                         (subs,sups) <- [Constraint] -> ([JType], [JType])
partitionCs ([Constraint] -> ([JType], [JType]))
-> TMonad [Constraint] -> TMonad ([JType], [JType])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VarRef -> TMonad [Constraint]
lookupConstraintsList VarRef
vr
                         let (subs1,sups1) = partitionCs $ S.toList cs
                         when ((null sups1 && (not . null) sups) ||
                               (null subs1 && (not . null) subs)) $ tyErr2Sub (JTFree vr) t
                         mapM_ (uncurry (<:)) [(x,y) | x <- subs, y <- subs1]
                         mapM_ (uncurry (<:)) [(y,x) | x <- sups, y <- sups1]

                         modify (\TCState
s -> TCState
s {tc_vars = M.insert ref (SVType t) (tc_vars s)}) --can all this be subsumed by a call to instantiate varref and casing on jtrigid carefully in the <: relationship?
                         -- a polymorphic var is a subtype of another if it is "bigger" on the lattice -- its subtypes are lower and supertypes are higher. sups a > sups b, subs a < subs b
                  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 ([Constraint] -> TMonad ())
-> ([Constraint] -> [Constraint]) -> [Constraint] -> TMonad ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Constraint
c Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
: ) ([Constraint] -> TMonad ()) -> TMonad [Constraint] -> TMonad ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< VarRef -> TMonad [Constraint]
lookupConstraintsList VarRef
vr

                  JTFunc [JType]
args JType
res -> do
                         (JType -> TMonad ()) -> [JType] -> TMonad ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Monad f) =>
(a -> f b) -> t a -> f ()
mapM_ (Int -> JType -> TMonad ()
occursCheck Int
ref) (JType
resJType -> [JType] -> [JType]
forall a. a -> [a] -> [a]
:[JType]
args)
                         [Constraint] -> TMonad ()
normalizeConstraints ([Constraint] -> TMonad ())
-> ([Constraint] -> [Constraint]) -> [Constraint] -> TMonad ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Constraint
c Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
:) ([Constraint] -> TMonad ()) -> TMonad [Constraint] -> TMonad ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< VarRef -> TMonad [Constraint]
lookupConstraintsList VarRef
vr

                  JTRecord JType
t Map String JType
m -> Int -> JType -> TMonad ()
occursCheck Int
ref JType
t TMonad () -> TMonad () -> TMonad ()
forall a b. TMonad a -> TMonad b -> TMonad b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
                                  (JType -> TMonad ()) -> Map String JType -> TMonad ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Monad f) =>
(a -> f b) -> t a -> f ()
F.mapM_ (Int -> JType -> TMonad ()
occursCheck Int
ref) Map String JType
m TMonad () -> TMonad () -> TMonad ()
forall a b. TMonad a -> TMonad b -> TMonad b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
                                  Either (Map String JType, JType) (Map String JType, JType)
-> TMonad ()
addRecConstraint ((Map String JType, JType)
-> Either (Map String JType, JType) (Map String JType, JType)
forall a b. b -> Either a b
Right (Map String JType
m,JType
t))

                  JTList JType
t' -> do
                         vr' <- TMonad VarRef
newVarRef
                         addConstraint vr' (Super t')
                         instantiateVarRef vr (JTList (JTFree vr'))

                  JTMap JType
t' -> do
                         vr' <- TMonad VarRef
newVarRef
                         addConstraint vr' (Super t')
                         instantiateVarRef vr (JTMap (JTFree vr'))

                  JTRigid VarRef
_ Set Constraint
cs -> do
                         (subs,sups) <- [Constraint] -> ([JType], [JType])
partitionCs ([Constraint] -> ([JType], [JType]))
-> TMonad [Constraint] -> TMonad ([JType], [JType])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VarRef -> TMonad [Constraint]
lookupConstraintsList VarRef
vr
                         let (subs1,sups1) = partitionCs $ S.toList cs
                         when ((null sups1 && (not . null) sups) ||
                               (null subs1 && (not . null) subs)) $ tyErr2Sub (JTFree vr) t
                         mapM_ (uncurry (<:)) [(y,x) | x <- subs, y <- subs1]
                         mapM_ (uncurry (<:)) [(x,y) | x <- sups, y <- sups1]

                         modify (\TCState
s -> TCState
s {tc_vars = M.insert ref (SVType t) (tc_vars s)}) --can all this be subsumed by a call to instantiate varref and casing on jtrigid carefully in the <: relationship?
                         -- a polymorphic var is a subtype of another if it is "bigger" on the lattice -- its subtypes are lower and supertypes are higher. sups a > sups b, subs a < subs b

                  JType
_ -> VarRef -> JType -> TMonad ()
instantiateVarRef VarRef
vr JType
t
    where
      putCs :: [Constraint] -> m ()
putCs [Constraint]
cs =
        (TCState -> TCState) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\TCState
s -> TCState
s {tc_vars = M.insert ref (SVConstrained $ S.fromList $ cs) (tc_vars s)})

      addC :: Constraint -> TMonad ()
addC Constraint
constraint = do
        cs <- VarRef -> TMonad [Constraint]
lookupConstraintsList VarRef
vr
        modify (\TCState
s -> TCState
s {tc_vars = M.insert ref (SVConstrained (S.fromList $ constraint:cs)) (tc_vars s)})

      findRecordSubs :: [Constraint] -> ([(Map String JType, JType)], [Constraint])
findRecordSubs [Constraint]
cs = (Constraint -> Maybe (Map String JType, JType))
-> [Constraint] -> ([(Map String JType, JType)], [Constraint])
forall a b. (a -> Maybe b) -> [a] -> ([b], [a])
partitionOut Constraint -> Maybe (Map String JType, JType)
go [Constraint]
cs
          where go :: Constraint -> Maybe (Map String JType, JType)
go (Sub (JTRecord JType
t Map String JType
m)) = (Map String JType, JType) -> Maybe (Map String JType, JType)
forall a. a -> Maybe a
Just (Map String JType
m,JType
t)
                go Constraint
_ = Maybe (Map String JType, JType)
forall a. Maybe a
Nothing

      findRecordSups :: [Constraint] -> ([(Map String JType, JType)], [Constraint])
findRecordSups [Constraint]
cs = (Constraint -> Maybe (Map String JType, JType))
-> [Constraint] -> ([(Map String JType, JType)], [Constraint])
forall a b. (a -> Maybe b) -> [a] -> ([b], [a])
partitionOut Constraint -> Maybe (Map String JType, JType)
go [Constraint]
cs
          where go :: Constraint -> Maybe (Map String JType, JType)
go (Super (JTRecord JType
t Map String JType
m)) = (Map String JType, JType) -> Maybe (Map String JType, JType)
forall a. a -> Maybe a
Just (Map String JType
m,JType
t)
                go Constraint
_ = Maybe (Map String JType, JType)
forall a. Maybe a
Nothing

      --left is sub, right is super
      --There really should be at most one existing sub and sup constraint
      addRecConstraint :: Either (Map String JType, JType) (Map String JType, JType)
-> TMonad ()
addRecConstraint Either (Map String JType, JType) (Map String JType, JType)
eM = do
        (subs,restCs) <- [Constraint] -> ([(Map String JType, JType)], [Constraint])
findRecordSubs ([Constraint] -> ([(Map String JType, JType)], [Constraint]))
-> TMonad [Constraint]
-> TMonad ([(Map String JType, JType)], [Constraint])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VarRef -> TMonad [Constraint]
lookupConstraintsList VarRef
vr
        let (sups,restCs') = findRecordSups restCs

            mergeSubs [] = Maybe (Map key JType, JType)
-> TMonad (Maybe (Map key JType, JType))
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Map key JType, JType)
forall a. Maybe a
Nothing
            mergeSubs [(Map key JType, JType)
m] = Maybe (Map key JType, JType)
-> TMonad (Maybe (Map key JType, JType))
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Map key JType, JType)
 -> TMonad (Maybe (Map key JType, JType)))
-> Maybe (Map key JType, JType)
-> TMonad (Maybe (Map key JType, JType))
forall a b. (a -> b) -> a -> b
$ (Map key JType, JType) -> Maybe (Map key JType, JType)
forall a. a -> Maybe a
Just (Map key JType, JType)
m
            mergeSubs ((Map key JType, JType)
m:[(Map key JType, JType)]
ms) = (Map key JType, JType) -> Maybe (Map key JType, JType)
forall a. a -> Maybe a
Just ((Map key JType, JType) -> Maybe (Map key JType, JType))
-> TMonad (Map key JType, JType)
-> TMonad (Maybe (Map key JType, JType))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Map key JType, JType)
 -> (Map key JType, JType) -> TMonad (Map key JType, JType))
-> (Map key JType, JType)
-> [(Map key JType, JType)]
-> TMonad (Map key JType, JType)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\(Map key JType
mp,JType
t) (Map key JType
mp',JType
t') -> do
                                                  mp'' <- (JType -> JType -> TMonad JType)
-> Map key JType -> Map key JType -> TMonad (Map key JType)
forall (m :: * -> *) key val.
(Monad m, Ord key) =>
(val -> val -> m val)
-> Map key val -> Map key val -> m (Map key val)
unionWithM (\JType
x JType
y -> [JType] -> TMonad JType
someLowerBound [JType
x,JType
y]) Map key JType
mp Map key JType
mp'
                                                  t'' <- someLowerBound [t,t']
                                                  return (mp'',t'')
                                              ) (Map key JType, JType)
m [(Map key JType, JType)]
ms
            mergeSups [] = Maybe (Map key JType, JType)
-> TMonad (Maybe (Map key JType, JType))
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Map key JType, JType)
forall a. Maybe a
Nothing
            mergeSups [(Map key JType, JType)
m] = Maybe (Map key JType, JType)
-> TMonad (Maybe (Map key JType, JType))
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Map key JType, JType)
 -> TMonad (Maybe (Map key JType, JType)))
-> Maybe (Map key JType, JType)
-> TMonad (Maybe (Map key JType, JType))
forall a b. (a -> b) -> a -> b
$ (Map key JType, JType) -> Maybe (Map key JType, JType)
forall a. a -> Maybe a
Just (Map key JType, JType)
m
            mergeSups ((Map key JType, JType)
m:[(Map key JType, JType)]
ms) = (Map key JType, JType) -> Maybe (Map key JType, JType)
forall a. a -> Maybe a
Just ((Map key JType, JType) -> Maybe (Map key JType, JType))
-> TMonad (Map key JType, JType)
-> TMonad (Maybe (Map key JType, JType))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Map key JType, JType)
 -> (Map key JType, JType) -> TMonad (Map key JType, JType))
-> (Map key JType, JType)
-> [(Map key JType, JType)]
-> TMonad (Map key JType, JType)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\(Map key JType
mp,JType
t) (Map key JType
mp',JType
t') -> do
                                                                mp'' <- (JType -> JType -> TMonad JType)
-> Map key JType -> Map key JType -> TMonad (Map key JType)
forall (m :: * -> *) key val b.
(Monad m, Ord key) =>
(val -> val -> m b) -> Map key val -> Map key val -> m (Map key b)
intersectionWithM (\JType
x JType
y -> [JType] -> TMonad JType
someUpperBound [JType
x,JType
y]) Map key JType
mp Map key JType
mp'
                                                                t'' <- someUpperBound [t,t']
                                                                return (mp'',t'')
                                                            ) (Map key JType, JType)
m [(Map key JType, JType)]
ms
        mbSub <- mergeSubs $ case eM of
                               Left (Map String JType, JType)
mt -> (Map String JType, JType)
mt (Map String JType, JType)
-> [(Map String JType, JType)] -> [(Map String JType, JType)]
forall a. a -> [a] -> [a]
: [(Map String JType, JType)]
subs
                               Either (Map String JType, JType) (Map String JType, JType)
_ -> [(Map String JType, JType)]
subs
        mbSup <- mergeSups $ case eM of
                               Right (Map String JType, JType)
mt -> (Map String JType, JType)
mt (Map String JType, JType)
-> [(Map String JType, JType)] -> [(Map String JType, JType)]
forall a. a -> [a] -> [a]
: [(Map String JType, JType)]
sups
                               Either (Map String JType, JType) (Map String JType, JType)
_ -> [(Map String JType, JType)]
sups
        normalizeConstraints =<< case (mbSub, mbSup) of
          (Just (Map String JType
subm,JType
subt), Just (Map String JType
supm,JType
supt)) -> do
            Bool -> TMonad () -> TMonad ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (JType -> JType -> Bool)
-> Map String JType -> Map String JType -> Bool
forall k a b.
Ord k =>
(a -> b -> Bool) -> Map k a -> Map k b -> Bool
M.isSubmapOfBy (\JType
_ JType
_ -> Bool
True) Map String JType
subm Map String JType
supm) (TMonad () -> TMonad ()) -> TMonad () -> TMonad ()
forall a b. (a -> b) -> a -> b
$ String -> String -> String -> JType -> JType -> TMonad ()
forall a. String -> String -> String -> JType -> JType -> TMonad a
tyErr2ext 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)
            _ <- (JType -> JType -> TMonad ())
-> Map String JType -> Map String JType -> TMonad (Map String ())
forall (m :: * -> *) key val b.
(Monad m, Ord key) =>
(val -> val -> m b) -> Map key val -> Map key val -> m (Map key b)
intersectionWithM (\JType
x JType
y -> JType
y JType -> JType -> TMonad ()
<: JType
x) Map String JType
subm Map String JType
supm
            _ <- supt <: subt
            return $ Sub (JTRecord subt subm) : Super (JTRecord supt supm) : restCs'
          (Just (Map String JType
subm,JType
subt), Maybe (Map String JType, JType)
Nothing)  -> [Constraint] -> TMonad [Constraint]
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Constraint] -> TMonad [Constraint])
-> [Constraint] -> TMonad [Constraint]
forall a b. (a -> b) -> a -> b
$ JType -> Constraint
Sub (JType -> Map String JType -> JType
JTRecord JType
subt Map String JType
subm) Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
: [Constraint]
restCs'
          (Maybe (Map String JType, JType)
Nothing , Just (Map String JType
supm,JType
supt)) -> [Constraint] -> TMonad [Constraint]
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Constraint] -> TMonad [Constraint])
-> [Constraint] -> TMonad [Constraint]
forall a b. (a -> b) -> a -> b
$ JType -> Constraint
Super (JType -> Map String JType -> JType
JTRecord JType
supt Map String JType
supm) Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
: [Constraint]
restCs'
          (Maybe (Map String JType, JType), Maybe (Map String JType, JType))
_ -> [Constraint] -> TMonad [Constraint]
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return [Constraint]
restCs'

      --There really should be at most one existing sub and sup constraint
      normalizeConstraints :: [Constraint] -> TMonad ()
normalizeConstraints [Constraint]
cl = [Constraint] -> TMonad ()
forall {m :: * -> *}. MonadState TCState m => [Constraint] -> m ()
putCs ([Constraint] -> TMonad ()) -> TMonad [Constraint] -> TMonad ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Constraint] -> TMonad [Constraint]
cannonicalizeConstraints [Constraint]
cl


cannonicalizeConstraints :: [Constraint] -> TMonad [Constraint]
cannonicalizeConstraints :: [Constraint] -> TMonad [Constraint]
cannonicalizeConstraints [Constraint]
constraintList = do
        -- trace ("ccl: " ++ show constraintList) $ return ()
        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
        mbSub <- [([VarRef], JType)] -> TMonad (Maybe JType)
mergeSubs [([VarRef], JType)]
subs
        mbSup <- mergeSups sups
        case (mbSub, mbSup) of
          (Just JType
sub, Just JType
sup) -> do
            JType
sup JType -> JType -> TMonad ()
<: JType
sub
            [Constraint] -> TMonad [Constraint]
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Constraint] -> TMonad [Constraint])
-> [Constraint] -> TMonad [Constraint]
forall a b. (a -> b) -> a -> b
$ JType -> Constraint
Sub JType
sub Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
: JType -> Constraint
Super JType
sup Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
: [Constraint]
restCs'
          (Just JType
sub, Maybe JType
Nothing)  -> [Constraint] -> TMonad [Constraint]
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Constraint] -> TMonad [Constraint])
-> [Constraint] -> TMonad [Constraint]
forall a b. (a -> b) -> a -> b
$ JType -> Constraint
Sub JType
sub Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
: [Constraint]
restCs'
          (Maybe JType
Nothing , Just JType
sup) -> [Constraint] -> TMonad [Constraint]
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Constraint] -> TMonad [Constraint])
-> [Constraint] -> TMonad [Constraint]
forall a b. (a -> b) -> a -> b
$ JType -> Constraint
Super JType
sup Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
: [Constraint]
restCs'
          (Maybe JType, Maybe JType)
_ -> [Constraint] -> TMonad [Constraint]
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return [Constraint]
restCs'
  where

    findForallSubs :: [Constraint] -> ([([VarRef], JType)], [Constraint])
findForallSubs [Constraint]
cs = (Constraint -> Maybe ([VarRef], JType))
-> [Constraint] -> ([([VarRef], JType)], [Constraint])
forall a b. (a -> Maybe b) -> [a] -> ([b], [a])
partitionOut Constraint -> Maybe ([VarRef], JType)
go [Constraint]
cs
      where go :: Constraint -> Maybe ([VarRef], JType)
go (Sub (JTForall [VarRef]
vars JType
t)) = ([VarRef], JType) -> Maybe ([VarRef], JType)
forall a. a -> Maybe a
Just ([VarRef]
vars,JType
t)
            go (Sub (JTFree VarRef
_)) = Maybe ([VarRef], JType)
forall a. Maybe a
Nothing
            go (Sub JType
x) = ([VarRef], JType) -> Maybe ([VarRef], JType)
forall a. a -> Maybe a
Just ([],JType
x)
            go Constraint
_ = Maybe ([VarRef], JType)
forall a. Maybe a
Nothing

    findForallSups :: [Constraint] -> ([([VarRef], JType)], [Constraint])
findForallSups [Constraint]
cs = (Constraint -> Maybe ([VarRef], JType))
-> [Constraint] -> ([([VarRef], JType)], [Constraint])
forall a b. (a -> Maybe b) -> [a] -> ([b], [a])
partitionOut Constraint -> Maybe ([VarRef], JType)
go [Constraint]
cs
      where go :: Constraint -> Maybe ([VarRef], JType)
go (Super (JTForall [VarRef]
vars JType
t)) = ([VarRef], JType) -> Maybe ([VarRef], JType)
forall a. a -> Maybe a
Just ([VarRef]
vars,JType
t)
            go (Super (JTFree VarRef
_)) = Maybe ([VarRef], JType)
forall a. Maybe a
Nothing
            go (Super JType
x) = ([VarRef], JType) -> Maybe ([VarRef], JType)
forall a. a -> Maybe a
Just ([],JType
x)
            go Constraint
_ = Maybe ([VarRef], JType)
forall a. Maybe a
Nothing

    findFuncs :: [JType] -> ([([JType], JType)], [JType])
findFuncs [JType]
cs = (JType -> Maybe ([JType], JType))
-> [JType] -> ([([JType], JType)], [JType])
forall a b. (a -> Maybe b) -> [a] -> ([b], [a])
partitionOut JType -> Maybe ([JType], JType)
go [JType]
cs
        where go :: JType -> Maybe ([JType], JType)
go (JTFunc [JType]
args JType
ret) = ([JType], JType) -> Maybe ([JType], JType)
forall a. a -> Maybe a
Just ([JType]
args, JType
ret)
              go JType
_ = Maybe ([JType], JType)
forall a. Maybe a
Nothing

    mergeSubs :: [([VarRef], JType)] -> TMonad (Maybe JType)
mergeSubs [] = Maybe JType -> TMonad (Maybe JType)
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe JType
forall a. Maybe a
Nothing
    mergeSubs [([],JType
t)] = Maybe JType -> TMonad (Maybe JType)
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe JType -> TMonad (Maybe JType))
-> Maybe JType -> TMonad (Maybe JType)
forall a b. (a -> b) -> a -> b
$ JType -> Maybe JType
forall a. a -> Maybe a
Just (JType -> Maybe JType) -> JType -> Maybe JType
forall a b. (a -> b) -> a -> b
$ JType
t
    mergeSubs [([VarRef], JType)
s] = Maybe JType -> TMonad (Maybe JType)
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe JType -> TMonad (Maybe JType))
-> Maybe JType -> TMonad (Maybe JType)
forall a b. (a -> b) -> a -> b
$ JType -> Maybe JType
forall a. a -> Maybe a
Just (JType -> Maybe JType) -> JType -> Maybe JType
forall a b. (a -> b) -> a -> b
$ ([VarRef] -> JType -> JType) -> ([VarRef], JType) -> JType
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [VarRef] -> JType -> JType
JTForall ([VarRef], JType)
s
    mergeSubs [([VarRef], JType)]
ss = do
      rt <- TMonad JType
newTyVar
      (_,frame) <- withLocalScope $ do
          instantiatedTypes <- mapM (uncurry instantiateScheme) ss
          let (funcTypes, otherTypes) = findFuncs instantiatedTypes
          when (not . null $ funcTypes) $ do
                     let (argss,rets) = unzip funcTypes
                         lft = [([JType], JType)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [([JType], JType)]
funcTypes
                     args' <- mapM someUpperBound $ filter ((== lft) . length) $ transpose argss
                     ret'  <- someLowerBound rets
                     rt <: JTFunc args' ret'
          mapM_ (rt <:) otherTypes
--        ((args',ret'):_,o:_) -> tyErr2ext "Incompatible Subtype Constraints" "Subtype constraint" "Subtype constraint" (JTFunc args' ret') o
      rt' <- resolveType rt
      case rt' of
        (JTFunc [JType]
args JType
res) -> do
          freeVarsInArgs <- [Set Int] -> Set Int
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ([Set Int] -> Set Int) -> TMonad [Set Int] -> TMonad (Set Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (JType -> TMonad (Set Int)) -> [JType] -> TMonad [Set Int]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM JType -> TMonad (Set Int)
freeVars [JType]
args
          freeVarsInRes  <- freeVars res
          setFrozen $ frame `S.difference` (freeVarsInArgs `S.intersection` freeVarsInRes)
        JType
_ -> Set Int -> TMonad ()
setFrozen Set Int
frame
      -- tryCloseFrozenVars
      Just <$> resolveType (JTForall (frame2VarRefs frame) rt')

    mergeSups :: [([VarRef], JType)] -> TMonad (Maybe JType)
mergeSups [] = Maybe JType -> TMonad (Maybe JType)
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe JType
forall a. Maybe a
Nothing
    mergeSups [([],JType
t)] = Maybe JType -> TMonad (Maybe JType)
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe JType -> TMonad (Maybe JType))
-> Maybe JType -> TMonad (Maybe JType)
forall a b. (a -> b) -> a -> b
$ JType -> Maybe JType
forall a. a -> Maybe a
Just (JType -> Maybe JType) -> JType -> Maybe JType
forall a b. (a -> b) -> a -> b
$ JType
t
    mergeSups [([VarRef], JType)
s] = Maybe JType -> TMonad (Maybe JType)
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe JType -> TMonad (Maybe JType))
-> Maybe JType -> TMonad (Maybe JType)
forall a b. (a -> b) -> a -> b
$ JType -> Maybe JType
forall a. a -> Maybe a
Just (JType -> Maybe JType) -> JType -> Maybe JType
forall a b. (a -> b) -> a -> b
$ ([VarRef] -> JType -> JType) -> ([VarRef], JType) -> JType
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [VarRef] -> JType -> JType
JTForall ([VarRef], JType)
s
    mergeSups [([VarRef], JType)]
ss = do
      rt <- TMonad JType
newTyVar
      (_,frame) <- withLocalScope $ do
           instantiatedTypes <- mapM (uncurry instantiateScheme) ss
           let (funcTypes, otherTypes) = findFuncs instantiatedTypes
           when (not . null $ funcTypes) $ do
                     let (argss,rets) = unzip funcTypes
                     args' <- mapM someLowerBound $ transpose argss
                     ret'  <- someUpperBound rets
                     rt <: JTFunc args' ret'
           mapM_ (<: rt) otherTypes
--        ((args',ret'):_,o:_) -> tyErr2ext "Incompatible Supertype Constraints" "Supertype constraint" ("Supertype constraint" ++ show o) (JTFunc args' ret') o
      rt' <- resolveType rt

      case rt' of
        (JTFunc [JType]
args JType
res) -> do
          freeVarsInArgs <- [Set Int] -> Set Int
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ([Set Int] -> Set Int) -> TMonad [Set Int] -> TMonad (Set Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (JType -> TMonad (Set Int)) -> [JType] -> TMonad [Set Int]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM JType -> TMonad (Set Int)
freeVars [JType]
args
          freeVarsInRes  <- freeVars res
          setFrozen $ frame `S.difference` (freeVarsInArgs `S.intersection` freeVarsInRes)
        JType
_ -> Set Int -> TMonad ()
setFrozen Set Int
frame
      -- tryCloseFrozenVars
      Just <$> resolveType (JTForall (frame2VarRefs frame) rt')


tryCloseFrozenVars :: TMonad ()
tryCloseFrozenVars :: TMonad ()
tryCloseFrozenVars = ReaderT [Either Int Int] TMonad () -> [Either Int Int] -> TMonad ()
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (Set Int -> ReaderT [Either Int Int] TMonad ()
loop (Set Int -> ReaderT [Either Int Int] TMonad ())
-> (TCState -> Set Int)
-> TCState
-> ReaderT [Either Int Int] TMonad ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCState -> Set Int
tc_frozen (TCState -> ReaderT [Either Int Int] TMonad ())
-> ReaderT [Either Int Int] TMonad TCState
-> ReaderT [Either Int Int] TMonad ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ReaderT [Either Int Int] TMonad TCState
forall s (m :: * -> *). MonadState s m => m s
get) []
    where
      loop :: Set Int -> ReaderT [Either Int Int] TMonad ()
loop Set Int
frozen = do
        (Int -> ReaderT [Either Int Int] TMonad ())
-> [Int] -> ReaderT [Either Int Int] TMonad ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Monad f) =>
(a -> f b) -> t a -> f ()
mapM_ Int -> ReaderT [Either Int Int] TMonad ()
go ([Int] -> ReaderT [Either Int Int] TMonad ())
-> [Int] -> ReaderT [Either Int Int] TMonad ()
forall a b. (a -> b) -> a -> b
$ Set Int -> [Int]
forall a. Set a -> [a]
S.toList Set Int
frozen
        newFrozen <- TCState -> Set Int
tc_frozen (TCState -> Set Int)
-> ReaderT [Either Int Int] TMonad TCState
-> ReaderT [Either Int Int] TMonad (Set Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TMonad TCState -> ReaderT [Either Int Int] TMonad TCState
forall (m :: * -> *) a.
Monad m =>
m a -> ReaderT [Either Int Int] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TMonad TCState
forall s (m :: * -> *). MonadState s m => m s
get
        if S.null (newFrozen  `S.difference` frozen)
           then return ()
           else loop newFrozen
      go :: Int -> ReaderT [Either Int Int] TMonad ()
      go :: Int -> ReaderT [Either Int Int] TMonad ()
go Int
i = do
        s <- ReaderT [Either Int Int] TMonad [Either Int Int]
forall r (m :: * -> *). MonadReader r m => m r
ask
        case findLoop i s of
          -- if no set is returned, then that means we just return (i.e. the constraint is dull)
          Just Maybe [Int]
Nothing  -> () -> ReaderT [Either Int Int] TMonad ()
forall a. a -> ReaderT [Either Int Int] TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
          -- if a set is returned, then all vars in the set should be tied together
          Just (Just [Int]
vrs) -> [Int] -> ReaderT [Either Int Int] TMonad ()
unifyGroup [Int]
vrs
          Maybe (Maybe [Int])
Nothing       -> do
              t <- TMonad JType -> ReaderT [Either Int Int] TMonad JType
forall (m :: * -> *) a.
Monad m =>
m a -> ReaderT [Either Int Int] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TMonad JType -> ReaderT [Either Int Int] TMonad JType)
-> TMonad JType -> ReaderT [Either Int Int] TMonad JType
forall a b. (a -> b) -> a -> b
$ JType -> TMonad JType
resolveTypeShallow (VarRef -> JType
JTFree (Maybe String
forall a. Maybe a
Nothing, Int
i))
              case t of
                (JTFree VarRef
vr) -> do
                     l <- VarRef -> ReaderT [Either Int Int] TMonad [Constraint]
tryClose VarRef
vr
                     case l of
                       [] -> () -> ReaderT [Either Int Int] TMonad ()
forall a. a -> ReaderT [Either Int Int] TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                       [Constraint]
cl -> do
                         (Constraint -> ReaderT [Either Int Int] TMonad ())
-> [Constraint] -> ReaderT [Either Int Int] TMonad ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Monad f) =>
(a -> f b) -> t a -> f ()
mapM_ (VarRef -> Constraint -> ReaderT [Either Int Int] TMonad ()
forall {a}.
(a, Int) -> Constraint -> ReaderT [Either Int Int] TMonad ()
go' VarRef
vr) [Constraint]
cl
                         TMonad () -> ReaderT [Either Int Int] TMonad ()
forall (m :: * -> *) a.
Monad m =>
m a -> ReaderT [Either Int Int] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift ((Constraint -> TMonad Constraint) -> [Constraint] -> TMonad ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Monad f) =>
(a -> f b) -> t a -> f ()
mapM_ ((JType -> TMonad JType) -> Constraint -> TMonad Constraint
forall (m :: * -> *).
(Monad m, Functor m) =>
(JType -> m JType) -> Constraint -> m Constraint
mapConstraint JType -> TMonad JType
resolveType) [Constraint]
cl)
                          -- not clear if we need to call again. if we resolve any constraints, they should point us back upwards...
                         --if cl remains free, recannonicalize it?
                JType
_ -> () -> ReaderT [Either Int Int] TMonad ()
forall a. a -> ReaderT [Either Int Int] TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      -- Left is super, right is sub
      go' :: (a, Int) -> Constraint -> ReaderT [Either Int Int] TMonad ()
go' (a
_,Int
ref) (Sub (JTFree (Maybe String
_,Int
i)))
          | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ref = () -> ReaderT [Either Int Int] TMonad ()
forall a. a -> ReaderT [Either Int Int] TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
          | Bool
otherwise = -- trace (show ("super: " ++ show (ref,i))) $
                        ([Either Int Int] -> [Either Int Int])
-> ReaderT [Either Int Int] TMonad ()
-> ReaderT [Either Int Int] TMonad ()
forall a.
([Either Int Int] -> [Either Int Int])
-> ReaderT [Either Int Int] TMonad a
-> ReaderT [Either Int Int] TMonad a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\[Either Int Int]
s -> Int -> Either Int Int
forall a b. a -> Either a b
Left Int
ref Either Int Int -> [Either Int Int] -> [Either Int Int]
forall a. a -> [a] -> [a]
: [Either Int Int]
s) (ReaderT [Either Int Int] TMonad ()
 -> ReaderT [Either Int Int] TMonad ())
-> ReaderT [Either Int Int] TMonad ()
-> ReaderT [Either Int Int] TMonad ()
forall a b. (a -> b) -> a -> b
$ Int -> ReaderT [Either Int Int] TMonad ()
go Int
i
      go' (a
_,Int
ref) (Super (JTFree (Maybe String
_,Int
i)))
          | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ref = () -> ReaderT [Either Int Int] TMonad ()
forall a. a -> ReaderT [Either Int Int] TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
          | Bool
otherwise = -- trace (show ("sub: " ++ show (ref,i))) $
                        ([Either Int Int] -> [Either Int Int])
-> ReaderT [Either Int Int] TMonad ()
-> ReaderT [Either Int Int] TMonad ()
forall a.
([Either Int Int] -> [Either Int Int])
-> ReaderT [Either Int Int] TMonad a
-> ReaderT [Either Int Int] TMonad a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\[Either Int Int]
s -> Int -> Either Int Int
forall a b. b -> Either a b
Right Int
ref Either Int Int -> [Either Int Int] -> [Either Int Int]
forall a. a -> [a] -> [a]
: [Either Int Int]
s) (ReaderT [Either Int Int] TMonad ()
 -> ReaderT [Either Int Int] TMonad ())
-> ReaderT [Either Int Int] TMonad ()
-> ReaderT [Either Int Int] TMonad ()
forall a b. (a -> b) -> a -> b
$ Int -> ReaderT [Either Int Int] TMonad ()
go Int
i
      go' (a, Int)
_ Constraint
_ = () -> ReaderT [Either Int Int] TMonad ()
forall a. a -> ReaderT [Either Int Int] TMonad a
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) = TMonad () -> ReaderT [Either Int Int] TMonad ()
forall (m :: * -> *) a.
Monad m =>
m a -> ReaderT [Either Int Int] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TMonad () -> ReaderT [Either Int Int] TMonad ())
-> TMonad () -> ReaderT [Either Int Int] TMonad ()
forall a b. (a -> b) -> a -> b
$ (Int -> TMonad ()) -> [Int] -> TMonad ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Monad f) =>
(a -> f b) -> t a -> f ()
mapM_ (\Int
x -> VarRef -> JType -> TMonad ()
instantiateVarRef (Maybe String
forall a. Maybe a
Nothing, Int
x) (VarRef -> JType
JTFree (Maybe String
forall a. Maybe a
Nothing,Int
vr))) [Int]
vrs
      unifyGroup [] = () -> ReaderT [Either Int Int] TMonad ()
forall a. a -> ReaderT [Either Int Int] TMonad a
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 = Either p p -> Bool
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)
               | (p -> p) -> (p -> p) -> Either p p -> p
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either p -> p
forall a. a -> a
id p -> p
forall a. a -> a
id Either p p
r p -> p -> Bool
forall a. Eq a => a -> a -> Bool
== p
i Bool -> Bool -> Bool
&& Either p p -> Bool
forall a b. Either a b -> Bool
eitherIsLeft Either p p
r Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
cTyp = Maybe [p] -> Maybe (Maybe [p])
forall a. a -> Maybe a
Just (Maybe [p] -> Maybe (Maybe [p])) -> Maybe [p] -> Maybe (Maybe [p])
forall a b. (a -> b) -> a -> b
$ [p] -> Maybe [p]
forall a. a -> Maybe a
Just ((p -> p) -> (p -> p) -> Either p p -> p
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either p -> p
forall a. a -> a
id p -> p
forall a. a -> a
id Either p p
r p -> [p] -> [p]
forall a. a -> [a] -> [a]
: [p]
accum)
                  -- i.e. there's a cycle to close
               | (p -> p) -> (p -> p) -> Either p p -> p
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either p -> p
forall a. a -> a
id p -> p
forall a. a -> a
id Either p p
r p -> p -> Bool
forall a. Eq a => a -> a -> Bool
== p
i = Maybe [p] -> Maybe (Maybe [p])
forall a. a -> Maybe a
Just Maybe [p]
forall a. Maybe a
Nothing
                  -- i.e. there's a "dull" cycle
               | Either p p -> Bool
forall a b. Either a b -> Bool
eitherIsLeft Either p p
r Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
/= Bool
cTyp = Maybe (Maybe [p])
forall a. Maybe a
Nothing -- we stop looking for a cycle because the chain is broken
               | Bool
otherwise = [p] -> [Either p p] -> Maybe (Maybe [p])
go ((p -> p) -> (p -> p) -> Either p p -> p
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either p -> p
forall a. a -> a
id p -> p
forall a. a -> a
id Either p p
r p -> [p] -> [p]
forall a. a -> [a] -> [a]
: [p]
accum) [Either p p]
rs
            go [p]
_ [] = Maybe (Maybe [p])
forall a. Maybe a
Nothing

      findLoop p
i [] = Maybe (Maybe [p])
forall a. Maybe a
Nothing

      tryClose :: VarRef -> ReaderT [Either Int Int] TMonad [Constraint]
tryClose vr :: VarRef
vr@(Maybe String
_,Int
i) = do
        cl <- TMonad [Constraint] -> ReaderT [Either Int Int] TMonad [Constraint]
forall (m :: * -> *) a.
Monad m =>
m a -> ReaderT [Either Int Int] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift(TMonad [Constraint]
 -> ReaderT [Either Int Int] TMonad [Constraint])
-> TMonad [Constraint]
-> ReaderT [Either Int Int] TMonad [Constraint]
forall a b. (a -> b) -> a -> b
$ [Constraint] -> TMonad [Constraint]
cannonicalizeConstraints ([Constraint] -> TMonad [Constraint])
-> TMonad [Constraint] -> TMonad [Constraint]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< VarRef -> TMonad [Constraint]
lookupConstraintsList VarRef
vr
        -- trace ("tryclose: " ++ show vr) $ trace (show cl) $ return ()
        case partitionCs cl of
          ([JType]
_,[JType
s]) -> TMonad () -> ReaderT [Either Int Int] TMonad ()
forall (m :: * -> *) a.
Monad m =>
m a -> ReaderT [Either Int Int] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (VarRef -> JType -> TMonad ()
instantiateVarRef VarRef
vr JType
s) ReaderT [Either Int Int] TMonad ()
-> ReaderT [Either Int Int] TMonad ()
-> ReaderT [Either Int Int] TMonad ()
forall a b.
ReaderT [Either Int Int] TMonad a
-> ReaderT [Either Int Int] TMonad b
-> ReaderT [Either Int Int] TMonad b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Int -> ReaderT [Either Int Int] TMonad ()
go Int
i ReaderT [Either Int Int] TMonad ()
-> ReaderT [Either Int Int] TMonad [Constraint]
-> ReaderT [Either Int Int] TMonad [Constraint]
forall a b.
ReaderT [Either Int Int] TMonad a
-> ReaderT [Either Int Int] TMonad b
-> ReaderT [Either Int Int] TMonad b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Constraint] -> ReaderT [Either Int Int] TMonad [Constraint]
forall a. a -> ReaderT [Either Int Int] TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return [] -- prefer lower bound (supertype constraint)
          ([JType
s],[JType]
_) -> TMonad () -> ReaderT [Either Int Int] TMonad ()
forall (m :: * -> *) a.
Monad m =>
m a -> ReaderT [Either Int Int] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (VarRef -> JType -> TMonad ()
instantiateVarRef VarRef
vr JType
s) ReaderT [Either Int Int] TMonad ()
-> ReaderT [Either Int Int] TMonad ()
-> ReaderT [Either Int Int] TMonad ()
forall a b.
ReaderT [Either Int Int] TMonad a
-> ReaderT [Either Int Int] TMonad b
-> ReaderT [Either Int Int] TMonad b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Int -> ReaderT [Either Int Int] TMonad ()
go Int
i ReaderT [Either Int Int] TMonad ()
-> ReaderT [Either Int Int] TMonad [Constraint]
-> ReaderT [Either Int Int] TMonad [Constraint]
forall a b.
ReaderT [Either Int Int] TMonad a
-> ReaderT [Either Int Int] TMonad b
-> ReaderT [Either Int Int] TMonad b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Constraint] -> ReaderT [Either Int Int] TMonad [Constraint]
forall a. a -> ReaderT [Either Int Int] TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return []
          ([JType], [JType])
_ -> [Constraint] -> ReaderT [Either Int Int] TMonad [Constraint]
forall a. a -> ReaderT [Either Int Int] TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return [Constraint]
cl

-- Manipulating the environment
withLocalScope :: TMonad a -> TMonad (a, Set Int)
withLocalScope :: forall a. TMonad a -> TMonad (a, Set Int)
withLocalScope TMonad a
act = do
  (TCState -> TCState) -> TMonad ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\TCState
s -> TCState
s {tc_env   = M.empty : tc_env s,
                   tc_stack = S.empty : tc_stack s})
  res <- TMonad a
act
  frame <- head . tc_stack <$> get
  modify (\TCState
s -> TCState
s {tc_env   = drop 1 $ tc_env s,
                   tc_stack = drop 1 $ tc_stack s})
  return (res, frame)

setFrozen :: Set Int -> TMonad ()
setFrozen :: Set Int -> TMonad ()
setFrozen Set Int
x = (TCState -> TCState) -> TMonad ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\TCState
s -> TCState
s {tc_frozen = tc_frozen s `S.union` x})

-- addRefsToStack x = modify (\s -> s {tc_stack = F.foldr addToStack (tc_stack s) x })

frame2VarRefs :: Set t -> [(Maybe a, t)]
frame2VarRefs :: forall t a. Set t -> [(Maybe a, t)]
frame2VarRefs Set t
frame = (\t
x -> (Maybe a
forall a. Maybe a
Nothing,t
x)) (t -> (Maybe a, t)) -> [t] -> [(Maybe a, t)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set t -> [t]
forall a. Set a -> [a]
S.toList Set t
frame

addEnv :: Ident -> JType -> TMonad ()
addEnv :: Ident -> JType -> TMonad ()
addEnv Ident
ident JType
typ = do
  envstack <- TCState -> [Map Ident JType]
tc_env (TCState -> [Map Ident JType])
-> TMonad TCState -> TMonad [Map Ident JType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TMonad TCState
forall s (m :: * -> *). MonadState s m => m s
get
  case envstack of
    (Map Ident JType
e:[Map Ident JType]
es) -> (TCState -> TCState) -> TMonad ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\TCState
s -> TCState
s {tc_env = M.insert ident typ e : es}) -- we clobber/shadow var names
    [Map Ident JType]
_ -> String -> TMonad ()
forall a. String -> TMonad a
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
  v <- TMonad JType
newTyVar
  addEnv ident v
  return 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
        vars <- TCState -> Map Int StoreVal
tc_vars (TCState -> Map Int StoreVal)
-> TMonad TCState -> TMonad (Map Int StoreVal)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TMonad TCState
forall s (m :: * -> *). MonadState s m => m s
get
        case M.lookup ref vars of
          Just (SVType JType
t) -> do
            res <- JType -> TMonad JType
go JType
t
            when (res /= t) $ modify (\TCState
s -> TCState
s {tc_vars = M.insert ref (SVType res) $ tc_vars s}) --mutation, shortcuts pointer chasing
            return res
          Maybe StoreVal
_ -> JType -> TMonad JType
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return JType
x

      -- | Eliminates resolved vars from foralls, eliminates empty foralls.
      go (JTForall [VarRef]
refs JType
t) = do
        refs' <- [Maybe VarRef] -> [VarRef]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe VarRef] -> [VarRef])
-> TMonad [Maybe VarRef] -> TMonad [VarRef]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (VarRef -> TMonad (Maybe VarRef))
-> [VarRef] -> TMonad [Maybe VarRef]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM VarRef -> TMonad (Maybe VarRef)
forall {m :: * -> *} {a}.
MonadState TCState m =>
(a, Int) -> m (Maybe (a, Int))
checkRef [VarRef]
refs
        if null refs'
           then go t
           else JTForall refs' <$> go 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
        vars <- TCState -> Map Int StoreVal
tc_vars (TCState -> Map Int StoreVal) -> m TCState -> m (Map Int StoreVal)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m TCState
forall s (m :: * -> *). MonadState s m => m s
get
        case M.lookup ref vars of
          Just (SVType JType
t) -> Maybe (a, Int) -> m (Maybe (a, Int))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (a, Int)
forall a. Maybe a
Nothing
          Maybe StoreVal
_ -> Maybe (a, Int) -> m (Maybe (a, Int))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (a, Int) -> m (Maybe (a, Int)))
-> Maybe (a, Int) -> m (Maybe (a, Int))
forall a b. (a -> b) -> a -> b
$ (a, Int) -> Maybe (a, Int)
forall a. a -> Maybe a
Just (a, Int)
x

resolveType :: JType -> TMonad JType
resolveType = ((JType -> TMonad JType) -> JType -> TMonad JType)
-> JType -> TMonad JType
resolveTypeGen (JType -> TMonad JType) -> JType -> TMonad JType
forall t (m :: * -> *).
(Compos1 t, Monad m) =>
(t -> m t) -> t -> m t
composOpM1
resolveTypeShallow :: JType -> TMonad JType
resolveTypeShallow = ((JType -> TMonad JType) -> JType -> TMonad JType)
-> JType -> TMonad JType
resolveTypeGen ((JType -> TMonad JType)
-> (JType -> TMonad JType) -> JType -> TMonad JType
forall a b. a -> b -> a
const JType -> TMonad JType
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return)

--TODO create proper bounds for records
integrateLocalType :: JLocalType -> TMonad JType
integrateLocalType :: JLocalType -> TMonad JType
integrateLocalType ([(VarRef, Constraint)]
env,JType
typ) = do
  (r, frame) <- TMonad JType -> TMonad (JType, Set Int)
forall a. TMonad a -> TMonad (a, Set Int)
withLocalScope (TMonad JType -> TMonad (JType, Set Int))
-> TMonad JType -> TMonad (JType, Set Int)
forall a b. (a -> b) -> a -> b
$ (StateT (Map Int JType) TMonad JType
 -> Map Int JType -> TMonad JType)
-> Map Int JType
-> StateT (Map Int JType) TMonad JType
-> TMonad JType
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT (Map Int JType) TMonad JType
-> Map Int JType -> TMonad JType
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT Map Int JType
forall k a. Map k a
M.empty (StateT (Map Int JType) TMonad JType -> TMonad JType)
-> StateT (Map Int JType) TMonad JType -> TMonad JType
forall a b. (a -> b) -> a -> b
$ do
                                 ((VarRef, Constraint) -> StateT (Map Int JType) TMonad ())
-> [(VarRef, Constraint)] -> StateT (Map Int JType) TMonad ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Monad f) =>
(a -> f b) -> t a -> f ()
mapM_ (VarRef, Constraint) -> StateT (Map Int JType) TMonad ()
forall {t :: (* -> *) -> * -> *}.
(MonadTrans t, MonadState (Map Int JType) (t TMonad)) =>
(VarRef, Constraint) -> t TMonad ()
integrateEnv [(VarRef, Constraint)]
env
                                 JType -> StateT (Map Int JType) TMonad JType
forall {t :: (* -> *) -> * -> *}.
(MonadState (Map Int JType) (t TMonad), MonadTrans t) =>
JType -> t TMonad JType
cloneType JType
typ
  resolveType $ JTForall (frame2VarRefs frame) r
    where
      getRef :: (Maybe String, k) -> t TMonad JType
getRef (Maybe String
mbName, k
ref) = do
            m <- t TMonad (Map k JType)
forall s (m :: * -> *). MonadState s m => m s
get
            case M.lookup ref m of
              Just JType
newTy -> JType -> t TMonad JType
forall a. a -> t TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return JType
newTy
              Maybe JType
Nothing -> do
                newTy <- (\VarRef
x -> VarRef -> JType
JTFree (Maybe String
mbName, VarRef -> Int
forall a b. (a, b) -> b
snd VarRef
x)) (VarRef -> JType) -> t TMonad VarRef -> t TMonad JType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TMonad VarRef -> t TMonad VarRef
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TMonad VarRef
newVarRef
                put $ M.insert ref newTy m
                return newTy

      integrateEnv :: (VarRef, Constraint) -> t TMonad ()
integrateEnv (VarRef
vr,Constraint
c) = do
        newTy <- VarRef -> t TMonad JType
forall {t :: (* -> *) -> * -> *} {k}.
(MonadState (Map k JType) (t TMonad), Ord k, MonadTrans t) =>
(Maybe String, k) -> t TMonad JType
getRef VarRef
vr
        case c of
          (Sub JType
t) -> TMonad () -> t TMonad ()
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TMonad () -> t TMonad ())
-> (JType -> TMonad ()) -> JType -> t TMonad ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (JType
newTy JType -> JType -> TMonad ()
<:) (JType -> t TMonad ()) -> t TMonad JType -> t TMonad ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< JType -> t TMonad JType
forall {t :: (* -> *) -> * -> *}.
(MonadState (Map Int JType) (t TMonad), MonadTrans t) =>
JType -> t TMonad JType
cloneType JType
t
          (Super JType
t) -> TMonad () -> t TMonad ()
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TMonad () -> t TMonad ())
-> (JType -> TMonad ()) -> JType -> t TMonad ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (JType -> JType -> TMonad ()
<: JType
newTy) (JType -> t TMonad ()) -> t TMonad JType -> t TMonad ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< JType -> t TMonad JType
forall {t :: (* -> *) -> * -> *}.
(MonadState (Map Int JType) (t TMonad), MonadTrans t) =>
JType -> t TMonad JType
cloneType JType
t

      cloneType :: JType -> t TMonad JType
cloneType (JTFree VarRef
vr) = VarRef -> t TMonad JType
forall {t :: (* -> *) -> * -> *} {k}.
(MonadState (Map k JType) (t TMonad), Ord k, MonadTrans t) =>
(Maybe String, k) -> t TMonad JType
getRef VarRef
vr
      cloneType JType
x = (JType -> t TMonad JType) -> JType -> t TMonad JType
forall t (m :: * -> *).
(Compos1 t, Monad m) =>
(t -> m t) -> t -> m t
composOpM1 JType -> t TMonad JType
cloneType JType
x

lookupEnv :: Ident -> TMonad JType
lookupEnv :: Ident -> TMonad JType
lookupEnv Ident
ident = JType -> TMonad JType
resolveType (JType -> TMonad JType) -> TMonad JType -> TMonad JType
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Map Ident JType] -> TMonad JType
forall {a}. [Map Ident a] -> TMonad a
go ([Map Ident JType] -> TMonad JType)
-> (TCState -> [Map Ident JType]) -> TCState -> TMonad JType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCState -> [Map Ident JType]
tc_env (TCState -> TMonad JType) -> TMonad TCState -> TMonad JType
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TMonad TCState
forall s (m :: * -> *). MonadState s m => m s
get
    where go :: [Map Ident a] -> TMonad a
go (Map Ident a
e:[Map Ident a]
es) = case Ident -> Map Ident a -> Maybe a
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Ident
ident Map Ident a
e of
                        Just a
t -> a -> TMonad a
forall a. a -> TMonad a
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]
_ = String -> TMonad a
forall a. String -> TMonad a
tyErr0 (String -> TMonad a) -> String -> TMonad a
forall a b. (a -> b) -> a -> b
$ String
"unable to resolve variable name: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ Ident -> Doc
forall a. JsToDoc a => a -> Doc
jsToDoc (Ident -> Doc) -> Ident -> Doc
forall a b. (a -> b) -> a -> b
$ Ident
ident)


freeVars :: JType -> TMonad (Set Int)
freeVars :: JType -> TMonad (Set Int)
freeVars JType
t = WriterT (Set Int) TMonad () -> TMonad (Set Int)
forall (m :: * -> *) w a. Monad m => WriterT w m a -> m w
execWriterT (WriterT (Set Int) TMonad () -> TMonad (Set Int))
-> (JType -> WriterT (Set Int) TMonad ())
-> JType
-> TMonad (Set Int)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. JType -> WriterT (Set Int) TMonad ()
forall {m :: * -> *}. MonadWriter (Set Int) m => JType -> m ()
go (JType -> TMonad (Set Int)) -> TMonad JType -> TMonad (Set Int)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< JType -> TMonad JType
resolveType JType
t
    where go :: JType -> m ()
go (JTFree (Maybe String
_, Int
ref)) = Set Int -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Int -> Set Int
forall a. a -> Set a
S.singleton Int
ref)
          go JType
x = (JType -> m ()) -> JType -> m ()
forall t (m :: * -> *).
(Compos1 t, Monad m) =>
(t -> m ()) -> t -> m ()
composOpM1_ JType -> m ()
go JType
x

--only works on resolved types
instantiateScheme :: [VarRef] -> JType -> TMonad JType
instantiateScheme :: [VarRef] -> JType -> TMonad JType
instantiateScheme [VarRef]
vrs JType
t = StateT (Map Int JType) TMonad JType
-> Map Int JType -> TMonad JType
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (JType -> StateT (Map Int JType) TMonad JType
go JType
t) Map Int JType
forall k a. Map k a
M.empty
    where
      schemeVars :: Set Int
schemeVars = [Int] -> Set Int
forall a. Ord a => [a] -> Set a
S.fromList ([Int] -> Set Int) -> [Int] -> Set Int
forall a b. (a -> b) -> a -> b
$ (VarRef -> Int) -> [VarRef] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map VarRef -> Int
forall a b. (a, b) -> b
snd [VarRef]
vrs
      go :: JType -> StateT (Map Int JType) TMonad JType
      go :: JType -> StateT (Map Int JType) TMonad JType
go (JTFree vr :: VarRef
vr@(Maybe String
mbName, Int
ref))
          | Int
ref Int -> Set Int -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set Int
schemeVars = do
                       m <- StateT (Map Int JType) TMonad (Map Int JType)
forall s (m :: * -> *). MonadState s m => m s
get
                       case M.lookup ref m of
                         Just JType
newTy -> JType -> StateT (Map Int JType) TMonad JType
forall a. a -> StateT (Map Int JType) TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return JType
newTy
                         Maybe JType
Nothing -> do
                           newRef <- (\VarRef
x -> (Maybe String
mbName, VarRef -> Int
forall a b. (a, b) -> b
snd VarRef
x)) (VarRef -> VarRef)
-> StateT (Map Int JType) TMonad VarRef
-> StateT (Map Int JType) TMonad VarRef
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TMonad VarRef -> StateT (Map Int JType) TMonad VarRef
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (Map Int JType) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TMonad VarRef
newVarRef
                           put $ M.insert ref (JTFree newRef) m
                           mapM_ (lift . addConstraint newRef <=< mapConstraint go) =<< lift (lookupConstraintsList vr)
                           return (JTFree newRef)
      go JType
x = (JType -> StateT (Map Int JType) TMonad JType)
-> JType -> StateT (Map Int JType) TMonad JType
forall t (m :: * -> *).
(Compos1 t, Monad m) =>
(t -> m t) -> t -> m t
composOpM1 JType -> StateT (Map Int JType) TMonad JType
go JType
x

--only works on resolved types
instantiateRigidScheme :: [VarRef] -> JType -> TMonad JType
instantiateRigidScheme :: [VarRef] -> JType -> TMonad JType
instantiateRigidScheme [VarRef]
vrs JType
t = StateT (Map Int JType) TMonad JType
-> Map Int JType -> TMonad JType
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (JType -> StateT (Map Int JType) TMonad JType
go JType
t) Map Int JType
forall k a. Map k a
M.empty
    where
      schemeVars :: Set Int
schemeVars = [Int] -> Set Int
forall a. Ord a => [a] -> Set a
S.fromList ([Int] -> Set Int) -> [Int] -> Set Int
forall a b. (a -> b) -> a -> b
$ (VarRef -> Int) -> [VarRef] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map VarRef -> Int
forall a b. (a, b) -> b
snd [VarRef]
vrs
      go :: JType -> StateT (Map Int JType) TMonad JType
      go :: JType -> StateT (Map Int JType) TMonad JType
go (JTFree vr :: VarRef
vr@(Maybe String
mbName, Int
ref))
          | Int
ref Int -> Set Int -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set Int
schemeVars = do
                       m <- StateT (Map Int JType) TMonad (Map Int JType)
forall s (m :: * -> *). MonadState s m => m s
get
                       case M.lookup ref m of
                         Just JType
newTy -> JType -> StateT (Map Int JType) TMonad JType
forall a. a -> StateT (Map Int JType) TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return JType
newTy
                         Maybe JType
Nothing -> do
                           newRef <- VarRef -> Set Constraint -> JType
JTRigid VarRef
vr (Set Constraint -> JType)
-> ([Constraint] -> Set Constraint) -> [Constraint] -> JType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Constraint] -> Set Constraint
forall a. Ord a => [a] -> Set a
S.fromList ([Constraint] -> JType)
-> StateT (Map Int JType) TMonad [Constraint]
-> StateT (Map Int JType) TMonad JType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TMonad [Constraint] -> StateT (Map Int JType) TMonad [Constraint]
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (Map Int JType) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (VarRef -> TMonad [Constraint]
lookupConstraintsList VarRef
vr)
                           put $ M.insert ref newRef m
                           return newRef
      go JType
x = (JType -> StateT (Map Int JType) TMonad JType)
-> JType -> StateT (Map Int JType) TMonad JType
forall t (m :: * -> *).
(Compos1 t, Monad m) =>
(t -> m t) -> t -> m t
composOpM1 JType -> StateT (Map Int JType) TMonad JType
go JType
x

--only works on resolved types
checkEscapedVars :: [VarRef] -> JType -> TMonad ()
checkEscapedVars :: [VarRef] -> JType -> TMonad ()
checkEscapedVars [VarRef]
vrs JType
t = JType -> TMonad ()
go JType
t
    where
      vs :: Set Int
vs = [Int] -> Set Int
forall a. Ord a => [a] -> Set a
S.fromList ([Int] -> Set Int) -> [Int] -> Set Int
forall a b. (a -> b) -> a -> b
$ (VarRef -> Int) -> [VarRef] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map VarRef -> Int
forall a b. (a, b) -> b
snd [VarRef]
vrs
      go :: JType -> TMonad ()
go t :: JType
t@(JTRigid (Maybe String
_,Int
ref) Set Constraint
_)
          | Int
ref Int -> Set Int -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set Int
vs = String -> JType -> TMonad ()
forall b. String -> JType -> TMonad b
tyErr1 String
"Qualified var escapes into environment" JType
t
          | Bool
otherwise = () -> TMonad ()
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      go JType
x = (JType -> TMonad ()) -> JType -> TMonad ()
forall t (m :: * -> *).
(Compos1 t, Monad m) =>
(t -> m ()) -> t -> m ()
composOpM1_ JType -> TMonad ()
go JType
x

-- Subtyping
(<:) :: JType -> JType -> TMonad ()
JType
x <: :: JType -> JType -> TMonad ()
<: JType
y = do
     xt <- JType -> TMonad JType
resolveTypeShallow JType
x --shallow because subtyping can close
     yt <- resolveTypeShallow y
     -- trace ("sub : " ++ show xt ++ ", " ++ show yt) $ return ()
     if xt == yt
        then return ()
        else go xt yt `withContext` (do
                                      xt <- prettyType x
                                      yt <- prettyType y
                                      return $ "When applying subtype constraint: " ++ xt ++ " <: " ++ yt)
  where

    go :: JType -> JType -> TMonad ()
go JType
_ JType
JTStat = () -> TMonad ()
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    go JType
JTImpossible JType
_ = () -> TMonad ()
forall a. a -> TMonad a
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) TMonad () -> TMonad () -> TMonad ()
forall a b. TMonad a -> TMonad b -> TMonad b
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)

    --above or below jtfrees ?

    -- v <: \/ a. t --> v <: t[a:=x], x not in conclusion
    go JType
xt yt :: JType
yt@(JTForall [VarRef]
vars JType
t) = do
           t' <- [VarRef] -> JType -> TMonad JType
instantiateRigidScheme [VarRef]
vars JType
t
           go xt t'
           checkEscapedVars vars =<< resolveType xt
           --then check that no fresh types appear in xt

    -- \/ a. t <: v --> [t] <: v
    go (JTForall [VarRef]
vars JType
t) JType
yt = do
           t' <- [VarRef] -> JType -> TMonad JType
instantiateScheme [VarRef]
vars JType
t
           go t' yt

    go xt :: JType
xt@(JTFunc [JType]
argsx JType
retx) yt :: JType
yt@(JTFunc [JType]
argsy JType
rety) = do
           -- TODO: zipWithM_ (<:) (appArgst ++ repeat JTStat) argst -- handle empty args cases
           Bool -> TMonad () -> TMonad ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([JType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [JType]
argsy Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [JType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [JType]
argsx) (TMonad () -> TMonad ()) -> TMonad () -> TMonad ()
forall a b. (a -> b) -> a -> b
$ JType -> JType -> TMonad ()
forall a. JType -> JType -> TMonad a
tyErr2Sub JType
xt JType
yt
           (JType -> JType -> TMonad ()) -> [JType] -> [JType] -> TMonad ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ JType -> JType -> TMonad ()
(<:) [JType]
argsy [JType]
argsx -- functions are contravariant in argument type
           JType
retx JType -> JType -> TMonad ()
<: JType
rety -- functions are covariant in return type
    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)
        | (JType -> JType -> Bool)
-> Map String JType -> Map String JType -> Bool
forall k a b.
Ord k =>
(a -> b -> Bool) -> Map k a -> Map k b -> Bool
M.isSubmapOfBy (\JType
_ JType
_ -> Bool
True) Map String JType
ym Map String JType
xm = JType
xt JType -> JType -> TMonad ()
<: JType
yt TMonad () -> TMonad (Map String ()) -> TMonad (Map String ())
forall a b. TMonad a -> TMonad b -> TMonad b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (JType -> JType -> TMonad ())
-> Map String JType -> Map String JType -> TMonad (Map String ())
forall (m :: * -> *) key val b.
(Monad m, Ord key) =>
(val -> val -> m b) -> Map key val -> Map key val -> m (Map key b)
intersectionWithM JType -> JType -> TMonad ()
(<:) Map String JType
xm Map String JType
ym TMonad (Map String ()) -> TMonad () -> TMonad ()
forall a b. TMonad a -> TMonad b -> TMonad b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> TMonad ()
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return () --TODO not right?
    go JType
xt JType
yt = JType -> JType -> TMonad ()
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 = TMonad (TMonad ()) -> TMonad ()
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (TMonad (TMonad ()) -> TMonad ())
-> TMonad (TMonad ()) -> TMonad ()
forall a b. (a -> b) -> a -> b
$ (JType -> JType -> TMonad ())
-> TMonad JType -> TMonad JType -> TMonad (TMonad ())
forall a b c. (a -> b -> c) -> TMonad a -> TMonad b -> TMonad c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 JType -> JType -> TMonad ()
(<:) TMonad JType
x TMonad JType
y

someUpperBound :: [JType] -> TMonad JType
someUpperBound :: [JType] -> TMonad JType
someUpperBound [] = JType -> TMonad JType
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTStat
someUpperBound [JType]
xs = do
  res <- TMonad JType
newTyVar
  b <- (mapM_ (<: res) xs >> return True) `catchError` \String
e -> Bool -> TMonad Bool
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
  if b then return res else return JTStat

someLowerBound :: [JType] -> TMonad JType
someLowerBound :: [JType] -> TMonad JType
someLowerBound [] = JType -> TMonad JType
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTImpossible
someLowerBound [JType]
xs = do
  res <- TMonad JType
newTyVar
  mapM_ (res <:) xs
  return res
--  b <- (mapM_ (res <:) xs >> return True) `catchError` \e -> return False
--  if b then return res else return JTImpossible

(=.=) :: 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
      JType -> TMonad JType
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return JType
x

--todo difft ixing. a[b] --num lookup, a#[b] --string lookup, a.[b] --num literal lookup (i.e. tuple projection)

instance JTypeCheck JExpr where
    typecheck :: JExpr -> TMonad JType
typecheck (ValExpr JVal
e) = JVal -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JVal
e
    typecheck (SelExpr JExpr
e (StrI String
i)) =
        do et <- JExpr -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JExpr
e
           case et of
             (JTRecord JType
t Map String JType
m) -> case String -> Map String JType -> Maybe JType
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
i Map String JType
m of
                               Just JType
res -> JType -> TMonad JType
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return JType
res
                               Maybe JType
Nothing -> String -> JType -> TMonad JType
forall b. String -> JType -> TMonad b
tyErr1 (String
"Record contains no field named " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
i) JType
et -- record extension would go here
             (JTFree VarRef
r) -> do
                            res <- TMonad JType
newTyVar
                            addConstraint r (Sub (JTRecord res (M.singleton i res)))
                            return res
             JType
_ -> String -> JType -> TMonad JType
forall b. String -> JType -> TMonad b
tyErr1 String
"Cannot use record selector on this value" JType
et
    typecheck (IdxExpr JExpr
e JExpr
e1) = TMonad JType
forall a. HasCallStack => a
undefined --this is tricky
    typecheck (InfixExpr String
s JExpr
e JExpr
e1)
        | String
s String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"-",String
"/",String
"*"] = JType -> TMonad ()
setFixed JType
JTNum TMonad () -> TMonad JType -> TMonad JType
forall a b. TMonad a -> TMonad b -> TMonad b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> JType -> TMonad JType
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTNum
        | String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"+" = JType -> TMonad ()
setFixed JType
JTNum TMonad () -> TMonad JType -> TMonad JType
forall a b. TMonad a -> TMonad b -> TMonad b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> JType -> TMonad JType
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTNum -- `orElse` setFixed JTStr --TODO: Intersection types
        | String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"++" = JType -> TMonad ()
setFixed JType
JTString TMonad () -> TMonad JType -> TMonad JType
forall a b. TMonad a -> TMonad b -> TMonad b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> JType -> TMonad JType
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTString
        | String
s String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
">",String
"<"] = JType -> TMonad ()
setFixed JType
JTNum TMonad () -> TMonad JType -> TMonad JType
forall a b. TMonad a -> TMonad b -> TMonad b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> JType -> TMonad JType
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTBool
        | String
s String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"==",String
"/="] = do
                            et <- JExpr -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JExpr
e
                            e1t <- typecheck e1
                            _ <- et =.= e1t
                            return JTBool
        | String
s String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"||",String
"&&"] = JType -> TMonad ()
setFixed JType
JTBool TMonad () -> TMonad JType -> TMonad JType
forall a b. TMonad a -> TMonad b -> TMonad b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> JType -> TMonad JType
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTBool
        | Bool
otherwise = String -> TMonad JType
forall a. String -> TMonad a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> TMonad JType) -> String -> TMonad JType
forall a b. (a -> b) -> a -> b
$ String
"Unhandled operator: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s
        where setFixed :: JType -> TMonad ()
setFixed JType
t = do
                  JExpr -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JExpr
e  TMonad JType -> TMonad JType -> TMonad ()
<<:> JType -> TMonad JType
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return JType
t
                  JExpr -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JExpr
e1 TMonad JType -> TMonad JType -> TMonad ()
<<:> JType -> TMonad JType
forall a. a -> TMonad a
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
_ -> String -> JType -> TMonad JType
forall b. String -> JType -> TMonad b
tyErr1 String
"Value not compatible with postfix assignment" (JType -> TMonad JType) -> TMonad JType -> TMonad JType
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< JExpr -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JExpr
e
        where go :: TMonad JType
go = (JExpr -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JExpr
e TMonad JType -> TMonad JType -> TMonad ()
<<:> JType -> TMonad JType
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTNum) TMonad () -> TMonad JType -> TMonad JType
forall a b. TMonad a -> TMonad b -> TMonad b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> JType -> TMonad JType
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTNum

    typecheck (IfExpr JExpr
e JExpr
e1 JExpr
e2) = do
                            JExpr -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JExpr
e TMonad JType -> TMonad JType -> TMonad ()
<<:> JType -> TMonad JType
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTBool
                            TMonad (TMonad JType) -> TMonad JType
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (TMonad (TMonad JType) -> TMonad JType)
-> TMonad (TMonad JType) -> TMonad JType
forall a b. (a -> b) -> a -> b
$ (JType -> JType -> TMonad JType)
-> TMonad JType -> TMonad JType -> TMonad (TMonad JType)
forall a b c. (a -> b -> c) -> TMonad a -> TMonad b -> TMonad c
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]) (JExpr -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JExpr
e1) (JExpr -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JExpr
e2)

    typecheck (NewExpr JExpr
e) = TMonad JType
forall a. HasCallStack => a
undefined --yipe

    --when we instantiate a scheme, all the elements of the head
    --that are not in the tail are henceforth unreachable and can be closed
    --but that's just an optimization
    typecheck (ApplExpr JExpr
e [JExpr]
appArgse) = do
                            et <- JExpr -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JExpr
e
                            appArgst <- mapM typecheck appArgse
                            let go (JTForall [VarRef]
vars JType
t) = JType -> TMonad JType
go (JType -> TMonad JType) -> TMonad JType -> TMonad JType
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [VarRef] -> JType -> TMonad JType
instantiateScheme [VarRef]
vars JType
t
                                go (JTFunc [JType]
argst JType
rett) = do
                                        (JType -> JType -> TMonad ()) -> [JType] -> [JType] -> TMonad ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ JType -> JType -> TMonad ()
(<:) ([JType]
appArgst [JType] -> [JType] -> [JType]
forall a. [a] -> [a] -> [a]
++ JType -> [JType]
forall a. a -> [a]
repeat JType
JTStat) [JType]
argst
                                        JType -> TMonad JType
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return JType
rett
                                go (JTFree VarRef
vr) = do
                                        ret <- TMonad JType
newTyVar
                                        addConstraint vr (Sub (JTFunc appArgst ret))
                                        return ret
                                go JType
x = String -> JType -> TMonad JType
forall b. String -> JType -> TMonad b
tyErr1 String
"Cannot apply value as function" JType
x
                            go et


    typecheck (UnsatExpr IdentSupply JExpr
_) = TMonad JType
forall a. HasCallStack => a
undefined --saturate (avoiding creation of existing ids) then typecheck
    typecheck (AntiExpr String
s) = String -> TMonad JType
forall a. HasCallStack => String -> a
error (String -> TMonad JType) -> String -> TMonad JType
forall a b. (a -> b) -> a -> b
$ String
"Antiquoted expression not provided with explicit signature: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
s

    --TODO: if we're typechecking a function, we can assign the types of the args to the given args
    typecheck (TypeExpr Bool
forceType JExpr
e JLocalType
t)
              | Bool
forceType = JLocalType -> TMonad JType
integrateLocalType JLocalType
t
              | Bool
otherwise = do
                            t1 <- JLocalType -> TMonad JType
integrateLocalType JLocalType
t
                            typecheck e <<:> return t1
                            return t1

instance JTypeCheck JVal where
    typecheck :: JVal -> TMonad JType
typecheck (JVar Ident
i) =
        case Ident
i of
          StrI String
"true" -> JType -> TMonad JType
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTBool
          StrI String
"false" -> JType -> TMonad JType
forall a. a -> TMonad a
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
_) = JType -> TMonad JType
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTNum
    typecheck (JDouble SaneDouble
_) = JType -> TMonad JType
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTNum
    typecheck (JStr String
_) = JType -> TMonad JType
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTString
    typecheck (JList [JExpr]
xs) = JVal -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck (Map String JExpr -> JVal
JHash (Map String JExpr -> JVal) -> Map String JExpr -> JVal
forall a b. (a -> b) -> a -> b
$ [(String, JExpr)] -> Map String JExpr
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(String, JExpr)] -> Map String JExpr)
-> [(String, JExpr)] -> Map String JExpr
forall a b. (a -> b) -> a -> b
$ [String] -> [JExpr] -> [(String, JExpr)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((Int -> String) -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Int -> String
forall a. Show a => a -> String
show [(Int
0::Int)..]) [JExpr]
xs)
                           -- fmap JTList . someUpperBound =<< mapM typecheck xs
    typecheck (JRegEx String
_) = TMonad JType
forall a. HasCallStack => a
undefined --regex object
    typecheck (JHash Map String JExpr
mp) = do
      mp' <- (JExpr -> TMonad JType)
-> Map String JExpr -> TMonad (Map String JType)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Map String a -> m (Map String b)
T.mapM JExpr -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck Map String JExpr
mp
      t <- if M.null mp'
             then return JTImpossible
             else someUpperBound $ M.elems mp'
      return $ JTRecord t mp'
    typecheck (JFunc [Ident]
args JStat
body) = do
          ((argst',res'), frame) <- TMonad ([JType], JType) -> TMonad (([JType], JType), Set Int)
forall a. TMonad a -> TMonad (a, Set Int)
withLocalScope (TMonad ([JType], JType) -> TMonad (([JType], JType), Set Int))
-> TMonad ([JType], JType) -> TMonad (([JType], JType), Set Int)
forall a b. (a -> b) -> a -> b
$ do
                                      argst <- (Ident -> TMonad JType) -> [Ident] -> TMonad [JType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Ident -> TMonad JType
newVarDecl [Ident]
args
                                      res <- typecheck body
                                      return (argst,res)
          rt <- resolveType $ JTFunc argst' res'
          freeVarsInArgs <- S.unions <$> mapM freeVars argst'
          freeVarsInRes  <- freeVars res'
          setFrozen $ frame `S.difference` (freeVarsInArgs `S.intersection` freeVarsInRes)
          tryCloseFrozenVars
          resolveType $ JTForall (frame2VarRefs frame) rt

    typecheck (UnsatVal IdentSupply JVal
_) = TMonad JType
forall a. HasCallStack => a
undefined --saturate (avoiding creation of existing ids) then typecheck

instance JTypeCheck JStat where
    typecheck :: JStat -> TMonad JType
typecheck (DeclStat Ident
ident Maybe JLocalType
Nothing) = Ident -> TMonad JType
newVarDecl Ident
ident TMonad JType -> TMonad JType -> TMonad JType
forall a b. TMonad a -> TMonad b -> TMonad b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> JType -> TMonad JType
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTStat
    typecheck (DeclStat Ident
ident (Just JLocalType
t)) = JLocalType -> TMonad JType
integrateLocalType JLocalType
t TMonad JType -> (JType -> TMonad ()) -> TMonad ()
forall a b. TMonad a -> (a -> TMonad b) -> TMonad b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Ident -> JType -> TMonad ()
addEnv Ident
ident TMonad () -> TMonad JType -> TMonad JType
forall a b. TMonad a -> TMonad b -> TMonad b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> JType -> TMonad JType
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTStat
    typecheck (ReturnStat JExpr
e) = JExpr -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JExpr
e
    typecheck (IfStat JExpr
e JStat
s JStat
s1) = do
                            JExpr -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JExpr
e TMonad JType -> TMonad JType -> TMonad ()
<<:> JType -> TMonad JType
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTBool
                            TMonad (TMonad JType) -> TMonad JType
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (TMonad (TMonad JType) -> TMonad JType)
-> TMonad (TMonad JType) -> TMonad JType
forall a b. (a -> b) -> a -> b
$ (JType -> JType -> TMonad JType)
-> TMonad JType -> TMonad JType -> TMonad (TMonad JType)
forall a b c. (a -> b -> c) -> TMonad a -> TMonad b -> TMonad c
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]) (JStat -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JStat
s) (JStat -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JStat
s1)
    typecheck (WhileStat Bool
_ JExpr
e JStat
s) = do
                            JExpr -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JExpr
e TMonad JType -> TMonad JType -> TMonad ()
<<:> JType -> TMonad JType
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTBool
                            JStat -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JStat
s
    typecheck (ForInStat Bool
_ Ident
_ JExpr
_ JStat
_) = TMonad JType
forall a. HasCallStack => a
undefined -- yipe!
    typecheck (SwitchStat JExpr
e [(JExpr, JStat)]
xs JStat
d) = TMonad JType
forall a. HasCallStack => a
undefined -- check e, unify e with firsts, check seconds, take glb of seconds
                                    --oh, hey, add typecase to language!?
    typecheck (TryStat JStat
_ Ident
_ JStat
_ JStat
_) = TMonad JType
forall a. HasCallStack => a
undefined -- should be easy
    typecheck (BlockStat [JStat]
xs) = do
                            ts <- (JStat -> TMonad JType) -> [JStat] -> TMonad [JType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM JStat -> TMonad JType
forall a. (JsToDoc a, JMacro a, JTypeCheck a) => a -> TMonad JType
typecheckWithBlock [JStat]
xs
                            someUpperBound $ stripStat ts
        where stripStat :: [JType] -> [JType]
stripStat (JType
JTStat:[JType]
ts) = [JType] -> [JType]
stripStat [JType]
ts
              stripStat (JType
t:[JType]
ts) = JType
t JType -> [JType] -> [JType]
forall a. a -> [a] -> [a]
: [JType] -> [JType]
stripStat [JType]
ts
              stripStat [JType]
t = [JType]
t
    typecheck (ApplStat JExpr
args [JExpr]
body) = JExpr -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck (JExpr -> [JExpr] -> JExpr
ApplExpr JExpr
args [JExpr]
body) TMonad JType -> TMonad JType -> TMonad JType
forall a b. TMonad a -> TMonad b -> TMonad b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> JType -> TMonad JType
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTStat
    typecheck (PPostStat Bool
b String
s JExpr
e) = JExpr -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck (Bool -> String -> JExpr -> JExpr
PPostExpr Bool
b String
s JExpr
e) TMonad JType -> TMonad JType -> TMonad JType
forall a b. TMonad a -> TMonad b -> TMonad b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> JType -> TMonad JType
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTStat
    typecheck (AssignStat JExpr
e JExpr
e1) = do
      JExpr -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JExpr
e1 TMonad JType -> TMonad JType -> TMonad ()
<<:> JExpr -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck JExpr
e
      JType -> TMonad JType
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTStat
    typecheck (UnsatBlock IdentSupply JStat
_) = TMonad JType
forall a. HasCallStack => a
undefined --oyvey
    typecheck (AntiStat String
_) = TMonad JType
forall a. HasCallStack => a
undefined --oyvey
    typecheck (BreakStat Maybe String
_) = JType -> TMonad JType
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return JType
JTStat
    typecheck (ForeignStat Ident
i JLocalType
t) = JLocalType -> TMonad JType
integrateLocalType JLocalType
t TMonad JType -> (JType -> TMonad ()) -> TMonad ()
forall a b. TMonad a -> (a -> TMonad b) -> TMonad b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Ident -> JType -> TMonad ()
addEnv Ident
i TMonad () -> TMonad JType -> TMonad JType
forall a b. TMonad a -> TMonad b -> TMonad b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> JType -> TMonad JType
forall a. a -> TMonad a
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 = a -> TMonad JType
forall a. JTypeCheck a => a -> TMonad JType
typecheck a
stat TMonad JType -> TMonad String -> TMonad JType
forall a. TMonad a -> TMonad String -> TMonad a
`withContext` (String -> TMonad String
forall a. a -> TMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> TMonad String) -> String -> TMonad String
forall a b. (a -> b) -> a -> b
$ String
"In statement: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Text -> String
T.unpack (Text -> String) -> (Doc -> Text) -> Doc -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleDoc -> Text
displayT (SimpleDoc -> Text) -> (Doc -> SimpleDoc) -> Doc -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> SimpleDoc
renderCompact (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ a -> Doc
forall a. (JsToDoc a, JMacro a) => a -> Doc
renderJs a
stat))