{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections     #-}

-- | Constraint-based typing from the presentation in Pierce's book.
module Kempe.TyAssign ( TypeM
                      , runTypeM
                      , checkModule
                      , assignModule
                      ) where

import           Control.Composition        (thread, (.$))
import           Control.Monad              (foldM, replicateM, unless, when, zipWithM_)
import           Control.Monad.Except       (throwError)
import           Control.Monad.State.Strict (StateT, get, gets, modify, put, runStateT)
import           Data.Bifunctor             (bimap, second)
import           Data.Foldable              (traverse_)
import           Data.Functor               (void, ($>))
import qualified Data.IntMap                as IM
import           Data.List                  (foldl')
import           Data.List.NonEmpty         (NonEmpty (..))
import           Data.Semigroup             ((<>))
import qualified Data.Set                   as S
import qualified Data.Text                  as T
import           Data.Tuple.Extra           (fst3)
import           Kempe.AST
import           Kempe.Error
import           Kempe.Name
import           Kempe.Unique
import           Lens.Micro                 (Lens', over)
import           Lens.Micro.Mtl             (modifying, (.=))
import           Prettyprinter              (Doc, Pretty (pretty), hardline, indent, vsep, (<+>))
import           Prettyprinter.Ext

type TyEnv a = IM.IntMap (StackType a)

data TyState a = TyState { TyState a -> Int
maxU             :: Int -- ^ For renamer
                         , TyState a -> TyEnv a
tyEnv            :: TyEnv a
                         , TyState a -> IntMap Kind
kindEnv          :: IM.IntMap Kind
                         , TyState a -> IntMap Int
renames          :: IM.IntMap Int
                         , TyState a -> IntMap (StackType a)
constructorTypes :: IM.IntMap (StackType a)
                         , TyState a -> Set (KempeTy a, KempeTy a)
constraints      :: S.Set (KempeTy a, KempeTy a) -- Just need equality between simple types? (do have tyapp but yeah)
                         }

(<#*>) :: Doc a -> Doc a -> Doc a
<#*> :: Doc a -> Doc a -> Doc a
(<#*>) Doc a
x Doc a
y = Doc a
x Doc a -> Doc a -> Doc a
forall a. Semigroup a => a -> a -> a
<> Doc a
forall ann. Doc ann
hardline Doc a -> Doc a -> Doc a
forall a. Semigroup a => a -> a -> a
<> Int -> Doc a -> Doc a
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 Doc a
y

instance Pretty (TyState a) where
    pretty :: TyState a -> Doc ann
pretty (TyState Int
_ TyEnv a
te IntMap Kind
_ IntMap Int
r TyEnv a
_ Set (KempeTy a, KempeTy a)
cs) =
        Doc ann
"type environment:" Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
<#> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep ((Int, StackType a) -> Doc ann
forall a b. (Int, StackType a) -> Doc b
prettyBound ((Int, StackType a) -> Doc ann)
-> [(Int, StackType a)] -> [Doc ann]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyEnv a -> [(Int, StackType a)]
forall a. IntMap a -> [(Int, a)]
IM.toList TyEnv a
te)
            Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
<#> Doc ann
"renames:" Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
<#*> IntMap Int -> Doc ann
forall b a. Pretty b => IntMap b -> Doc a
prettyDumpBinds IntMap Int
r
            Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
<#> Doc ann
"constraints:" Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
<#> Set (KempeTy a, KempeTy a) -> Doc ann
forall a ann. Set (KempeTy a, KempeTy a) -> Doc ann
prettyConstraints Set (KempeTy a, KempeTy a)
cs

prettyConstraints :: S.Set (KempeTy a, KempeTy a) -> Doc ann
prettyConstraints :: Set (KempeTy a, KempeTy a) -> Doc ann
prettyConstraints Set (KempeTy a, KempeTy a)
cs = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep ((KempeTy a, KempeTy a) -> Doc ann
forall a ann. (KempeTy a, KempeTy a) -> Doc ann
prettyEq ((KempeTy a, KempeTy a) -> Doc ann)
-> [(KempeTy a, KempeTy a)] -> [Doc ann]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set (KempeTy a, KempeTy a) -> [(KempeTy a, KempeTy a)]
forall a. Set a -> [a]
S.toList Set (KempeTy a, KempeTy a)
cs)

prettyBound :: (Int, StackType a) -> Doc b
prettyBound :: (Int, StackType a) -> Doc b
prettyBound (Int
i, StackType a
e) = Int -> Doc b
forall a ann. Pretty a => a -> Doc ann
pretty Int
i Doc b -> Doc b -> Doc b
forall a. Doc a -> Doc a -> Doc a
<+> Doc b
"←" Doc b -> Doc b -> Doc b
forall a. Doc a -> Doc a -> Doc a
<#*> StackType a -> Doc b
forall a ann. Pretty a => a -> Doc ann
pretty StackType a
e

prettyEq :: (KempeTy a, KempeTy a) -> Doc ann
prettyEq :: (KempeTy a, KempeTy a) -> Doc ann
prettyEq (KempeTy a
ty, KempeTy a
ty') = KempeTy a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty KempeTy a
ty Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
<+> Doc ann
"≡" Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
<+> KempeTy a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty KempeTy a
ty'

prettyDumpBinds :: Pretty b => IM.IntMap b -> Doc a
prettyDumpBinds :: IntMap b -> Doc a
prettyDumpBinds IntMap b
b = [Doc a] -> Doc a
forall ann. [Doc ann] -> Doc ann
vsep ((Int, b) -> Doc a
forall b a. Pretty b => (Int, b) -> Doc a
prettyBind ((Int, b) -> Doc a) -> [(Int, b)] -> [Doc a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IntMap b -> [(Int, b)]
forall a. IntMap a -> [(Int, a)]
IM.toList IntMap b
b)

prettyBind :: Pretty b => (Int, b) -> Doc a
prettyBind :: (Int, b) -> Doc a
prettyBind (Int
i, b
j) = Int -> Doc a
forall a ann. Pretty a => a -> Doc ann
pretty Int
i Doc a -> Doc a -> Doc a
forall a. Doc a -> Doc a -> Doc a
<+> Doc a
"→" Doc a -> Doc a -> Doc a
forall a. Doc a -> Doc a -> Doc a
<+> b -> Doc a
forall a ann. Pretty a => a -> Doc ann
pretty b
j

emptyStackType :: StackType a
emptyStackType :: StackType a
emptyStackType = Set (Name a) -> [KempeTy a] -> [KempeTy a] -> StackType a
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType Set (Name a)
forall a. Monoid a => a
mempty [] []

maxULens :: Lens' (TyState a) Int
maxULens :: (Int -> f Int) -> TyState a -> f (TyState a)
maxULens Int -> f Int
f TyState a
s = (Int -> TyState a) -> f Int -> f (TyState a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Int
x -> TyState a
s { maxU :: Int
maxU = Int
x }) (Int -> f Int
f (TyState a -> Int
forall a. TyState a -> Int
maxU TyState a
s))

constructorTypesLens :: Lens' (TyState a) (IM.IntMap (StackType a))
constructorTypesLens :: (IntMap (StackType a) -> f (IntMap (StackType a)))
-> TyState a -> f (TyState a)
constructorTypesLens IntMap (StackType a) -> f (IntMap (StackType a))
f TyState a
s = (IntMap (StackType a) -> TyState a)
-> f (IntMap (StackType a)) -> f (TyState a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\IntMap (StackType a)
x -> TyState a
s { constructorTypes :: IntMap (StackType a)
constructorTypes = IntMap (StackType a)
x }) (IntMap (StackType a) -> f (IntMap (StackType a))
f (TyState a -> IntMap (StackType a)
forall a. TyState a -> IntMap (StackType a)
constructorTypes TyState a
s))

tyEnvLens :: Lens' (TyState a) (TyEnv a)
tyEnvLens :: (TyEnv a -> f (TyEnv a)) -> TyState a -> f (TyState a)
tyEnvLens TyEnv a -> f (TyEnv a)
f TyState a
s = (TyEnv a -> TyState a) -> f (TyEnv a) -> f (TyState a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\TyEnv a
x -> TyState a
s { tyEnv :: TyEnv a
tyEnv = TyEnv a
x }) (TyEnv a -> f (TyEnv a)
f (TyState a -> TyEnv a
forall a. TyState a -> IntMap (StackType a)
tyEnv TyState a
s))

kindEnvLens :: Lens' (TyState a) (IM.IntMap Kind)
kindEnvLens :: (IntMap Kind -> f (IntMap Kind)) -> TyState a -> f (TyState a)
kindEnvLens IntMap Kind -> f (IntMap Kind)
f TyState a
s = (IntMap Kind -> TyState a) -> f (IntMap Kind) -> f (TyState a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\IntMap Kind
x -> TyState a
s { kindEnv :: IntMap Kind
kindEnv = IntMap Kind
x }) (IntMap Kind -> f (IntMap Kind)
f (TyState a -> IntMap Kind
forall a. TyState a -> IntMap Kind
kindEnv TyState a
s))

renamesLens :: Lens' (TyState a) (IM.IntMap Int)
renamesLens :: (IntMap Int -> f (IntMap Int)) -> TyState a -> f (TyState a)
renamesLens IntMap Int -> f (IntMap Int)
f TyState a
s = (IntMap Int -> TyState a) -> f (IntMap Int) -> f (TyState a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\IntMap Int
x -> TyState a
s { renames :: IntMap Int
renames = IntMap Int
x }) (IntMap Int -> f (IntMap Int)
f (TyState a -> IntMap Int
forall a. TyState a -> IntMap Int
renames TyState a
s))

constraintsLens :: Lens' (TyState a) (S.Set (KempeTy a, KempeTy a))
constraintsLens :: (Set (KempeTy a, KempeTy a) -> f (Set (KempeTy a, KempeTy a)))
-> TyState a -> f (TyState a)
constraintsLens Set (KempeTy a, KempeTy a) -> f (Set (KempeTy a, KempeTy a))
f TyState a
s = (Set (KempeTy a, KempeTy a) -> TyState a)
-> f (Set (KempeTy a, KempeTy a)) -> f (TyState a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Set (KempeTy a, KempeTy a)
x -> TyState a
s { constraints :: Set (KempeTy a, KempeTy a)
constraints = Set (KempeTy a, KempeTy a)
x }) (Set (KempeTy a, KempeTy a) -> f (Set (KempeTy a, KempeTy a))
f (TyState a -> Set (KempeTy a, KempeTy a)
forall a. TyState a -> Set (KempeTy a, KempeTy a)
constraints TyState a
s))

dummyName :: T.Text -> TypeM () (Name ())
dummyName :: Text -> TypeM () (Name ())
dummyName Text
n = do
    Int
pSt <- (TyState () -> Int) -> StateT (TyState ()) (Either (Error ())) Int
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TyState () -> Int
forall a. TyState a -> Int
maxU
    Text -> Unique -> () -> Name ()
forall a. Text -> Unique -> a -> Name a
Name Text
n (Int -> Unique
Unique (Int -> Unique) -> Int -> Unique
forall a b. (a -> b) -> a -> b
$ Int
pSt Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) ()
        Name ()
-> StateT (TyState ()) (Either (Error ())) () -> TypeM () (Name ())
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ASetter (TyState ()) (TyState ()) Int Int
-> (Int -> Int) -> StateT (TyState ()) (Either (Error ())) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
modifying ASetter (TyState ()) (TyState ()) Int Int
forall a. Lens' (TyState a) Int
maxULens (Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)

data Kind = Star
          | TyCons Kind Kind
          deriving (Kind -> Kind -> Bool
(Kind -> Kind -> Bool) -> (Kind -> Kind -> Bool) -> Eq Kind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Kind -> Kind -> Bool
$c/= :: Kind -> Kind -> Bool
== :: Kind -> Kind -> Bool
$c== :: Kind -> Kind -> Bool
Eq)

type TypeM a = StateT (TyState a) (Either (Error a))

type UnifyMap = IM.IntMap (KempeTy ())

inContext :: UnifyMap -> KempeTy () -> KempeTy ()
inContext :: UnifyMap -> KempeTy () -> KempeTy ()
inContext UnifyMap
um ty' :: KempeTy ()
ty'@(TyVar ()
_ (Name Text
_ (Unique Int
i) ()
_)) =
    case Int -> UnifyMap -> Maybe (KempeTy ())
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
i UnifyMap
um of
        Just ty :: KempeTy ()
ty@TyVar{} -> UnifyMap -> KempeTy () -> KempeTy ()
inContext (Int -> UnifyMap -> UnifyMap
forall a. Int -> IntMap a -> IntMap a
IM.delete Int
i UnifyMap
um) KempeTy ()
ty -- prevent cyclic lookups
        Just KempeTy ()
ty         -> KempeTy ()
ty
        Maybe (KempeTy ())
Nothing         -> KempeTy ()
ty'
inContext UnifyMap
_ ty' :: KempeTy ()
ty'@TyBuiltin{} = KempeTy ()
ty'
inContext UnifyMap
_ ty' :: KempeTy ()
ty'@TyNamed{} = KempeTy ()
ty'
inContext UnifyMap
um (TyApp ()
l KempeTy ()
ty KempeTy ()
ty') = () -> KempeTy () -> KempeTy () -> KempeTy ()
forall a. a -> KempeTy a -> KempeTy a -> KempeTy a
TyApp ()
l (UnifyMap -> KempeTy () -> KempeTy ()
inContext UnifyMap
um KempeTy ()
ty) (UnifyMap -> KempeTy () -> KempeTy ()
inContext UnifyMap
um KempeTy ()
ty')

-- | Perform substitutions before handing off to 'unifyMatch'
unifyPrep :: UnifyMap
           -> [(KempeTy (), KempeTy ())]
           -> Either (Error ()) (IM.IntMap (KempeTy ()))
unifyPrep :: UnifyMap
-> [(KempeTy (), KempeTy ())] -> Either (Error ()) UnifyMap
unifyPrep UnifyMap
_ [] = UnifyMap -> Either (Error ()) UnifyMap
forall a b. b -> Either a b
Right UnifyMap
forall a. Monoid a => a
mempty
unifyPrep UnifyMap
um ((KempeTy ()
ty, KempeTy ()
ty'):[(KempeTy (), KempeTy ())]
tys) =
    let ty'' :: KempeTy ()
ty'' = UnifyMap -> KempeTy () -> KempeTy ()
inContext UnifyMap
um KempeTy ()
ty
        ty''' :: KempeTy ()
ty''' = UnifyMap -> KempeTy () -> KempeTy ()
inContext UnifyMap
um KempeTy ()
ty'
    in UnifyMap
-> [(KempeTy (), KempeTy ())] -> Either (Error ()) UnifyMap
unifyMatch UnifyMap
um ([(KempeTy (), KempeTy ())] -> Either (Error ()) UnifyMap)
-> [(KempeTy (), KempeTy ())] -> Either (Error ()) UnifyMap
forall a b. (a -> b) -> a -> b
$ (KempeTy ()
ty'', KempeTy ()
ty''')(KempeTy (), KempeTy ())
-> [(KempeTy (), KempeTy ())] -> [(KempeTy (), KempeTy ())]
forall a. a -> [a] -> [a]
:[(KempeTy (), KempeTy ())]
tys

unifyMatch :: UnifyMap -> [(KempeTy (), KempeTy ())] -> Either (Error ()) (IM.IntMap (KempeTy ()))
unifyMatch :: UnifyMap
-> [(KempeTy (), KempeTy ())] -> Either (Error ()) UnifyMap
unifyMatch UnifyMap
_ []                                                             = UnifyMap -> Either (Error ()) UnifyMap
forall a b. b -> Either a b
Right UnifyMap
forall a. Monoid a => a
mempty
unifyMatch UnifyMap
um ((ty :: KempeTy ()
ty@(TyBuiltin ()
_ BuiltinTy
b0), ty' :: KempeTy ()
ty'@(TyBuiltin ()
_ BuiltinTy
b1)):[(KempeTy (), KempeTy ())]
tys) | BuiltinTy
b0 BuiltinTy -> BuiltinTy -> Bool
forall a. Eq a => a -> a -> Bool
== BuiltinTy
b1   = UnifyMap
-> [(KempeTy (), KempeTy ())] -> Either (Error ()) UnifyMap
unifyPrep UnifyMap
um [(KempeTy (), KempeTy ())]
tys
                                                                | Bool
otherwise  = Error () -> Either (Error ()) UnifyMap
forall a b. a -> Either a b
Left (() -> KempeTy () -> KempeTy () -> Error ()
forall a. a -> KempeTy a -> KempeTy a -> Error a
UnificationFailed () KempeTy ()
ty KempeTy ()
ty')
unifyMatch UnifyMap
um ((ty :: KempeTy ()
ty@(TyNamed ()
_ Name ()
n0), ty' :: KempeTy ()
ty'@(TyNamed ()
_ Name ()
n1)):[(KempeTy (), KempeTy ())]
tys) | Name ()
n0 Name () -> Name () -> Bool
forall a. Eq a => a -> a -> Bool
== Name ()
n1       = UnifyMap
-> [(KempeTy (), KempeTy ())] -> Either (Error ()) UnifyMap
unifyPrep UnifyMap
um [(KempeTy (), KempeTy ())]
tys
                                                    | Bool
otherwise      = Error () -> Either (Error ()) UnifyMap
forall a b. a -> Either a b
Left (() -> KempeTy () -> KempeTy () -> Error ()
forall a. a -> KempeTy a -> KempeTy a -> Error a
UnificationFailed () (KempeTy () -> KempeTy ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void KempeTy ()
ty) (KempeTy () -> KempeTy ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void KempeTy ()
ty'))
unifyMatch UnifyMap
um ((ty :: KempeTy ()
ty@(TyNamed ()
_ Name ()
_), TyVar  ()
_ (Name Text
_ (Unique Int
k) ()
_)):[(KempeTy (), KempeTy ())]
tys)       = Int -> KempeTy () -> UnifyMap -> UnifyMap
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
k KempeTy ()
ty (UnifyMap -> UnifyMap)
-> Either (Error ()) UnifyMap -> Either (Error ()) UnifyMap
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UnifyMap
-> [(KempeTy (), KempeTy ())] -> Either (Error ()) UnifyMap
unifyPrep (Int -> KempeTy () -> UnifyMap -> UnifyMap
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
k KempeTy ()
ty UnifyMap
um) [(KempeTy (), KempeTy ())]
tys
unifyMatch UnifyMap
um ((TyVar ()
_ (Name Text
_ (Unique Int
k) ()
_), ty :: KempeTy ()
ty@(TyNamed ()
_ Name ()
_)):[(KempeTy (), KempeTy ())]
tys)        = Int -> KempeTy () -> UnifyMap -> UnifyMap
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
k KempeTy ()
ty (UnifyMap -> UnifyMap)
-> Either (Error ()) UnifyMap -> Either (Error ()) UnifyMap
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UnifyMap
-> [(KempeTy (), KempeTy ())] -> Either (Error ()) UnifyMap
unifyPrep (Int -> KempeTy () -> UnifyMap -> UnifyMap
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
k KempeTy ()
ty UnifyMap
um) [(KempeTy (), KempeTy ())]
tys
unifyMatch UnifyMap
um ((ty :: KempeTy ()
ty@TyBuiltin{}, TyVar  ()
_ (Name Text
_ (Unique Int
k) ()
_)):[(KempeTy (), KempeTy ())]
tys)         = Int -> KempeTy () -> UnifyMap -> UnifyMap
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
k KempeTy ()
ty (UnifyMap -> UnifyMap)
-> Either (Error ()) UnifyMap -> Either (Error ()) UnifyMap
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UnifyMap
-> [(KempeTy (), KempeTy ())] -> Either (Error ()) UnifyMap
unifyPrep (Int -> KempeTy () -> UnifyMap -> UnifyMap
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
k KempeTy ()
ty UnifyMap
um) [(KempeTy (), KempeTy ())]
tys
unifyMatch UnifyMap
um ((TyVar ()
_ (Name Text
_ (Unique Int
k) ()
_), ty :: KempeTy ()
ty@(TyBuiltin ()
_ BuiltinTy
_)):[(KempeTy (), KempeTy ())]
tys)      = Int -> KempeTy () -> UnifyMap -> UnifyMap
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
k KempeTy ()
ty (UnifyMap -> UnifyMap)
-> Either (Error ()) UnifyMap -> Either (Error ()) UnifyMap
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UnifyMap
-> [(KempeTy (), KempeTy ())] -> Either (Error ()) UnifyMap
unifyPrep (Int -> KempeTy () -> UnifyMap -> UnifyMap
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
k KempeTy ()
ty UnifyMap
um) [(KempeTy (), KempeTy ())]
tys
unifyMatch UnifyMap
um ((TyVar ()
_ (Name Text
_ (Unique Int
k) ()
_), ty :: KempeTy ()
ty@(TyVar ()
_ Name ()
_)):[(KempeTy (), KempeTy ())]
tys)          = Int -> KempeTy () -> UnifyMap -> UnifyMap
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
k KempeTy ()
ty (UnifyMap -> UnifyMap)
-> Either (Error ()) UnifyMap -> Either (Error ()) UnifyMap
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UnifyMap
-> [(KempeTy (), KempeTy ())] -> Either (Error ()) UnifyMap
unifyPrep (Int -> KempeTy () -> UnifyMap -> UnifyMap
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
k KempeTy ()
ty UnifyMap
um) [(KempeTy (), KempeTy ())]
tys
unifyMatch UnifyMap
_ ((ty :: KempeTy ()
ty@TyBuiltin{}, ty' :: KempeTy ()
ty'@TyNamed{}):[(KempeTy (), KempeTy ())]
_)                             = Error () -> Either (Error ()) UnifyMap
forall a b. a -> Either a b
Left (() -> KempeTy () -> KempeTy () -> Error ()
forall a. a -> KempeTy a -> KempeTy a -> Error a
UnificationFailed () KempeTy ()
ty KempeTy ()
ty')
unifyMatch UnifyMap
_ ((ty :: KempeTy ()
ty@TyNamed{}, ty' :: KempeTy ()
ty'@TyBuiltin{}):[(KempeTy (), KempeTy ())]
_)                             = Error () -> Either (Error ()) UnifyMap
forall a b. a -> Either a b
Left (() -> KempeTy () -> KempeTy () -> Error ()
forall a. a -> KempeTy a -> KempeTy a -> Error a
UnificationFailed () KempeTy ()
ty KempeTy ()
ty')
unifyMatch UnifyMap
_ ((ty :: KempeTy ()
ty@TyBuiltin{}, ty' :: KempeTy ()
ty'@TyApp{}):[(KempeTy (), KempeTy ())]
_)                               = Error () -> Either (Error ()) UnifyMap
forall a b. a -> Either a b
Left (() -> KempeTy () -> KempeTy () -> Error ()
forall a. a -> KempeTy a -> KempeTy a -> Error a
UnificationFailed () KempeTy ()
ty KempeTy ()
ty')
unifyMatch UnifyMap
_ ((ty :: KempeTy ()
ty@TyNamed{}, ty' :: KempeTy ()
ty'@TyApp{}):[(KempeTy (), KempeTy ())]
_)                                 = Error () -> Either (Error ()) UnifyMap
forall a b. a -> Either a b
Left (() -> KempeTy () -> KempeTy () -> Error ()
forall a. a -> KempeTy a -> KempeTy a -> Error a
UnificationFailed () KempeTy ()
ty KempeTy ()
ty')
unifyMatch UnifyMap
_ ((ty :: KempeTy ()
ty@TyApp{}, ty' :: KempeTy ()
ty'@TyBuiltin{}):[(KempeTy (), KempeTy ())]
_)                               = Error () -> Either (Error ()) UnifyMap
forall a b. a -> Either a b
Left (() -> KempeTy () -> KempeTy () -> Error ()
forall a. a -> KempeTy a -> KempeTy a -> Error a
UnificationFailed () KempeTy ()
ty KempeTy ()
ty')
unifyMatch UnifyMap
um ((TyVar ()
_ (Name Text
_ (Unique Int
k) ()
_), ty :: KempeTy ()
ty@TyApp{}):[(KempeTy (), KempeTy ())]
tys)              = Int -> KempeTy () -> UnifyMap -> UnifyMap
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
k KempeTy ()
ty (UnifyMap -> UnifyMap)
-> Either (Error ()) UnifyMap -> Either (Error ()) UnifyMap
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UnifyMap
-> [(KempeTy (), KempeTy ())] -> Either (Error ()) UnifyMap
unifyPrep (Int -> KempeTy () -> UnifyMap -> UnifyMap
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
k KempeTy ()
ty UnifyMap
um) [(KempeTy (), KempeTy ())]
tys
unifyMatch UnifyMap
um ((ty :: KempeTy ()
ty@TyApp{}, TyVar  ()
_ (Name Text
_ (Unique Int
k) ()
_)):[(KempeTy (), KempeTy ())]
tys)             = Int -> KempeTy () -> UnifyMap -> UnifyMap
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
k KempeTy ()
ty (UnifyMap -> UnifyMap)
-> Either (Error ()) UnifyMap -> Either (Error ()) UnifyMap
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UnifyMap
-> [(KempeTy (), KempeTy ())] -> Either (Error ()) UnifyMap
unifyPrep (Int -> KempeTy () -> UnifyMap -> UnifyMap
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
k KempeTy ()
ty UnifyMap
um) [(KempeTy (), KempeTy ())]
tys
unifyMatch UnifyMap
um ((TyApp ()
_ KempeTy ()
ty KempeTy ()
ty', TyApp ()
_ KempeTy ()
ty'' KempeTy ()
ty'''):[(KempeTy (), KempeTy ())]
tys)                     = UnifyMap
-> [(KempeTy (), KempeTy ())] -> Either (Error ()) UnifyMap
unifyMatch UnifyMap
um ((KempeTy ()
ty, KempeTy ()
ty'') (KempeTy (), KempeTy ())
-> [(KempeTy (), KempeTy ())] -> [(KempeTy (), KempeTy ())]
forall a. a -> [a] -> [a]
: (KempeTy ()
ty', KempeTy ()
ty''') (KempeTy (), KempeTy ())
-> [(KempeTy (), KempeTy ())] -> [(KempeTy (), KempeTy ())]
forall a. a -> [a] -> [a]
: [(KempeTy (), KempeTy ())]
tys) -- TODO: I think this is right?
unifyMatch UnifyMap
_ ((ty :: KempeTy ()
ty@TyApp{}, ty' :: KempeTy ()
ty'@TyNamed{}):[(KempeTy (), KempeTy ())]
_)                                 = Error () -> Either (Error ()) UnifyMap
forall a b. a -> Either a b
Left (() -> KempeTy () -> KempeTy () -> Error ()
forall a. a -> KempeTy a -> KempeTy a -> Error a
UnificationFailed () (KempeTy () -> KempeTy ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void KempeTy ()
ty) (KempeTy () -> KempeTy ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void KempeTy ()
ty'))

unify :: [(KempeTy (), KempeTy ())] -> Either (Error ()) (IM.IntMap (KempeTy ()))
unify :: [(KempeTy (), KempeTy ())] -> Either (Error ()) UnifyMap
unify = UnifyMap
-> [(KempeTy (), KempeTy ())] -> Either (Error ()) UnifyMap
unifyPrep UnifyMap
forall a. IntMap a
IM.empty

unifyM :: S.Set (KempeTy (), KempeTy ()) -> TypeM () (IM.IntMap (KempeTy ()))
unifyM :: Set (KempeTy (), KempeTy ()) -> TypeM () UnifyMap
unifyM Set (KempeTy (), KempeTy ())
s =
    case {-# SCC "unify" #-} [(KempeTy (), KempeTy ())] -> Either (Error ()) UnifyMap
unify (Set (KempeTy (), KempeTy ()) -> [(KempeTy (), KempeTy ())]
forall a. Set a -> [a]
S.toList Set (KempeTy (), KempeTy ())
s) of
        Right UnifyMap
x  -> UnifyMap -> TypeM () UnifyMap
forall (f :: * -> *) a. Applicative f => a -> f a
pure UnifyMap
x
        Left Error ()
err -> Error () -> TypeM () UnifyMap
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError Error ()
err

-- TODO: take constructor types as an argument?..
runTypeM :: Int -- ^ For renamer
         -> TypeM a x -> Either (Error a) (x, Int)
runTypeM :: Int -> TypeM a x -> Either (Error a) (x, Int)
runTypeM Int
maxInt = ((x, TyState a) -> (x, Int))
-> Either (Error a) (x, TyState a) -> Either (Error a) (x, Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((TyState a -> Int) -> (x, TyState a) -> (x, Int)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second TyState a -> Int
forall a. TyState a -> Int
maxU) (Either (Error a) (x, TyState a) -> Either (Error a) (x, Int))
-> (TypeM a x -> Either (Error a) (x, TyState a))
-> TypeM a x
-> Either (Error a) (x, Int)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    (TypeM a x -> TyState a -> Either (Error a) (x, TyState a))
-> TyState a -> TypeM a x -> Either (Error a) (x, TyState a)
forall a b c. (a -> b -> c) -> b -> a -> c
flip TypeM a x -> TyState a -> Either (Error a) (x, TyState a)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (Int
-> TyEnv a
-> IntMap Kind
-> IntMap Int
-> TyEnv a
-> Set (KempeTy a, KempeTy a)
-> TyState a
forall a.
Int
-> IntMap (StackType a)
-> IntMap Kind
-> IntMap Int
-> IntMap (StackType a)
-> Set (KempeTy a, KempeTy a)
-> TyState a
TyState Int
maxInt TyEnv a
forall a. Monoid a => a
mempty IntMap Kind
forall a. Monoid a => a
mempty IntMap Int
forall a. Monoid a => a
mempty TyEnv a
forall a. Monoid a => a
mempty Set (KempeTy a, KempeTy a)
forall a. Set a
S.empty)

typeOfBuiltin :: BuiltinFn -> TypeM () (StackType ())
typeOfBuiltin :: BuiltinFn -> TypeM () (StackType ())
typeOfBuiltin BuiltinFn
Drop = do
    Name ()
aN <- Text -> TypeM () (Name ())
dummyName Text
"a"
    StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StackType () -> TypeM () (StackType ()))
-> StackType () -> TypeM () (StackType ())
forall a b. (a -> b) -> a -> b
$ Set (Name ()) -> [KempeTy ()] -> [KempeTy ()] -> StackType ()
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType (Name () -> Set (Name ())
forall a. a -> Set a
S.singleton Name ()
aN) [() -> Name () -> KempeTy ()
forall a. a -> Name a -> KempeTy a
TyVar () Name ()
aN] []
typeOfBuiltin BuiltinFn
Swap = do
    Name ()
aN <- Text -> TypeM () (Name ())
dummyName Text
"a"
    Name ()
bN <- Text -> TypeM () (Name ())
dummyName Text
"b"
    StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StackType () -> TypeM () (StackType ()))
-> StackType () -> TypeM () (StackType ())
forall a b. (a -> b) -> a -> b
$ Set (Name ()) -> [KempeTy ()] -> [KempeTy ()] -> StackType ()
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType ([Name ()] -> Set (Name ())
forall a. Ord a => [a] -> Set a
S.fromList [Name ()
aN, Name ()
bN]) [() -> Name () -> KempeTy ()
forall a. a -> Name a -> KempeTy a
TyVar () Name ()
aN, () -> Name () -> KempeTy ()
forall a. a -> Name a -> KempeTy a
TyVar () Name ()
bN] [() -> Name () -> KempeTy ()
forall a. a -> Name a -> KempeTy a
TyVar () Name ()
bN, () -> Name () -> KempeTy ()
forall a. a -> Name a -> KempeTy a
TyVar () Name ()
aN]
typeOfBuiltin BuiltinFn
Dup = do
    Name ()
aN <- Text -> TypeM () (Name ())
dummyName Text
"a"
    StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StackType () -> TypeM () (StackType ()))
-> StackType () -> TypeM () (StackType ())
forall a b. (a -> b) -> a -> b
$ Set (Name ()) -> [KempeTy ()] -> [KempeTy ()] -> StackType ()
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType (Name () -> Set (Name ())
forall a. a -> Set a
S.singleton Name ()
aN) [() -> Name () -> KempeTy ()
forall a. a -> Name a -> KempeTy a
TyVar () Name ()
aN] [() -> Name () -> KempeTy ()
forall a. a -> Name a -> KempeTy a
TyVar () Name ()
aN, () -> Name () -> KempeTy ()
forall a. a -> Name a -> KempeTy a
TyVar () Name ()
aN]
typeOfBuiltin BuiltinFn
IntEq      = StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure StackType ()
intRel
typeOfBuiltin BuiltinFn
IntLeq     = StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure StackType ()
intRel
typeOfBuiltin BuiltinFn
IntLt      = StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure StackType ()
intRel
typeOfBuiltin BuiltinFn
IntMod     = StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure StackType ()
intBinOp
typeOfBuiltin BuiltinFn
IntDiv     = StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure StackType ()
intBinOp
typeOfBuiltin BuiltinFn
IntPlus    = StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure StackType ()
intBinOp
typeOfBuiltin BuiltinFn
IntTimes   = StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure StackType ()
intBinOp
typeOfBuiltin BuiltinFn
IntMinus   = StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure StackType ()
intBinOp
typeOfBuiltin BuiltinFn
IntShiftR  = StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure StackType ()
intShift
typeOfBuiltin BuiltinFn
IntShiftL  = StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure StackType ()
intBinOp
typeOfBuiltin BuiltinFn
IntXor     = StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure StackType ()
intBinOp
typeOfBuiltin BuiltinFn
WordXor    = StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure StackType ()
wordBinOp
typeOfBuiltin BuiltinFn
WordPlus   = StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure StackType ()
wordBinOp
typeOfBuiltin BuiltinFn
WordTimes  = StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure StackType ()
wordBinOp
typeOfBuiltin BuiltinFn
WordShiftR = StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure StackType ()
wordShift
typeOfBuiltin BuiltinFn
WordShiftL = StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure StackType ()
wordShift
typeOfBuiltin BuiltinFn
IntGeq     = StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure StackType ()
intBinOp
typeOfBuiltin BuiltinFn
IntNeq     = StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure StackType ()
intBinOp
typeOfBuiltin BuiltinFn
IntGt      = StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure StackType ()
intBinOp
typeOfBuiltin BuiltinFn
WordMinus  = StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure StackType ()
wordBinOp
typeOfBuiltin BuiltinFn
WordDiv    = StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure StackType ()
wordBinOp
typeOfBuiltin BuiltinFn
WordMod    = StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure StackType ()
wordBinOp
typeOfBuiltin BuiltinFn
And        = StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure StackType ()
boolOp
typeOfBuiltin BuiltinFn
Or         = StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure StackType ()
boolOp
typeOfBuiltin BuiltinFn
Xor        = StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure StackType ()
boolOp
typeOfBuiltin BuiltinFn
IntNeg     = StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StackType () -> TypeM () (StackType ()))
-> StackType () -> TypeM () (StackType ())
forall a b. (a -> b) -> a -> b
$ Set (Name ()) -> [KempeTy ()] -> [KempeTy ()] -> StackType ()
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType Set (Name ())
forall a. Set a
S.empty [() -> BuiltinTy -> KempeTy ()
forall a. a -> BuiltinTy -> KempeTy a
TyBuiltin () BuiltinTy
TyInt] [() -> BuiltinTy -> KempeTy ()
forall a. a -> BuiltinTy -> KempeTy a
TyBuiltin () BuiltinTy
TyInt]
typeOfBuiltin BuiltinFn
Popcount   = StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StackType () -> TypeM () (StackType ()))
-> StackType () -> TypeM () (StackType ())
forall a b. (a -> b) -> a -> b
$ Set (Name ()) -> [KempeTy ()] -> [KempeTy ()] -> StackType ()
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType Set (Name ())
forall a. Set a
S.empty [() -> BuiltinTy -> KempeTy ()
forall a. a -> BuiltinTy -> KempeTy a
TyBuiltin () BuiltinTy
TyWord] [() -> BuiltinTy -> KempeTy ()
forall a. a -> BuiltinTy -> KempeTy a
TyBuiltin () BuiltinTy
TyInt]

boolOp :: StackType ()
boolOp :: StackType ()
boolOp = Set (Name ()) -> [KempeTy ()] -> [KempeTy ()] -> StackType ()
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType Set (Name ())
forall a. Set a
S.empty [() -> BuiltinTy -> KempeTy ()
forall a. a -> BuiltinTy -> KempeTy a
TyBuiltin () BuiltinTy
TyBool, () -> BuiltinTy -> KempeTy ()
forall a. a -> BuiltinTy -> KempeTy a
TyBuiltin () BuiltinTy
TyBool] [() -> BuiltinTy -> KempeTy ()
forall a. a -> BuiltinTy -> KempeTy a
TyBuiltin () BuiltinTy
TyBool]

intRel :: StackType ()
intRel :: StackType ()
intRel = Set (Name ()) -> [KempeTy ()] -> [KempeTy ()] -> StackType ()
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType Set (Name ())
forall a. Set a
S.empty [() -> BuiltinTy -> KempeTy ()
forall a. a -> BuiltinTy -> KempeTy a
TyBuiltin () BuiltinTy
TyInt, () -> BuiltinTy -> KempeTy ()
forall a. a -> BuiltinTy -> KempeTy a
TyBuiltin () BuiltinTy
TyInt] [() -> BuiltinTy -> KempeTy ()
forall a. a -> BuiltinTy -> KempeTy a
TyBuiltin () BuiltinTy
TyBool]

intBinOp :: StackType ()
intBinOp :: StackType ()
intBinOp = Set (Name ()) -> [KempeTy ()] -> [KempeTy ()] -> StackType ()
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType Set (Name ())
forall a. Set a
S.empty [() -> BuiltinTy -> KempeTy ()
forall a. a -> BuiltinTy -> KempeTy a
TyBuiltin () BuiltinTy
TyInt, () -> BuiltinTy -> KempeTy ()
forall a. a -> BuiltinTy -> KempeTy a
TyBuiltin () BuiltinTy
TyInt] [() -> BuiltinTy -> KempeTy ()
forall a. a -> BuiltinTy -> KempeTy a
TyBuiltin () BuiltinTy
TyInt]

intShift :: StackType ()
intShift :: StackType ()
intShift = Set (Name ()) -> [KempeTy ()] -> [KempeTy ()] -> StackType ()
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType Set (Name ())
forall a. Set a
S.empty [() -> BuiltinTy -> KempeTy ()
forall a. a -> BuiltinTy -> KempeTy a
TyBuiltin () BuiltinTy
TyInt, () -> BuiltinTy -> KempeTy ()
forall a. a -> BuiltinTy -> KempeTy a
TyBuiltin () BuiltinTy
TyInt8] [() -> BuiltinTy -> KempeTy ()
forall a. a -> BuiltinTy -> KempeTy a
TyBuiltin () BuiltinTy
TyInt]

wordBinOp :: StackType ()
wordBinOp :: StackType ()
wordBinOp = Set (Name ()) -> [KempeTy ()] -> [KempeTy ()] -> StackType ()
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType Set (Name ())
forall a. Set a
S.empty [() -> BuiltinTy -> KempeTy ()
forall a. a -> BuiltinTy -> KempeTy a
TyBuiltin () BuiltinTy
TyWord, () -> BuiltinTy -> KempeTy ()
forall a. a -> BuiltinTy -> KempeTy a
TyBuiltin () BuiltinTy
TyWord] [() -> BuiltinTy -> KempeTy ()
forall a. a -> BuiltinTy -> KempeTy a
TyBuiltin () BuiltinTy
TyWord]

wordShift :: StackType ()
wordShift :: StackType ()
wordShift = Set (Name ()) -> [KempeTy ()] -> [KempeTy ()] -> StackType ()
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType Set (Name ())
forall a. Set a
S.empty [() -> BuiltinTy -> KempeTy ()
forall a. a -> BuiltinTy -> KempeTy a
TyBuiltin () BuiltinTy
TyWord, () -> BuiltinTy -> KempeTy ()
forall a. a -> BuiltinTy -> KempeTy a
TyBuiltin () BuiltinTy
TyInt8] [() -> BuiltinTy -> KempeTy ()
forall a. a -> BuiltinTy -> KempeTy a
TyBuiltin () BuiltinTy
TyWord]

tyLookup :: Name a -> TypeM a (StackType a)
tyLookup :: Name a -> TypeM a (StackType a)
tyLookup n :: Name a
n@(Name Text
_ (Unique Int
i) a
l) = do
    TyEnv a
st <- (TyState a -> TyEnv a)
-> StateT (TyState a) (Either (Error a)) (TyEnv a)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TyState a -> TyEnv a
forall a. TyState a -> IntMap (StackType a)
tyEnv
    case Int -> TyEnv a -> Maybe (StackType a)
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
i TyEnv a
st of
        Just StackType a
ty -> StackType a -> TypeM a (StackType a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure StackType a
ty
        Maybe (StackType a)
Nothing -> Error a -> TypeM a (StackType a)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Error a -> TypeM a (StackType a))
-> Error a -> TypeM a (StackType a)
forall a b. (a -> b) -> a -> b
$ a -> Name a -> Error a
forall a. a -> Name a -> Error a
PoorScope a
l Name a
n

consLookup :: TyName a -> TypeM a (StackType a)
consLookup :: TyName a -> TypeM a (StackType a)
consLookup tn :: TyName a
tn@(Name Text
_ (Unique Int
i) a
l) = do
    IntMap (StackType a)
st <- (TyState a -> IntMap (StackType a))
-> StateT (TyState a) (Either (Error a)) (IntMap (StackType a))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TyState a -> IntMap (StackType a)
forall a. TyState a -> IntMap (StackType a)
constructorTypes
    case Int -> IntMap (StackType a) -> Maybe (StackType a)
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
i IntMap (StackType a)
st of
        Just StackType a
ty -> StackType a -> TypeM a (StackType a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure StackType a
ty
        Maybe (StackType a)
Nothing -> Error a -> TypeM a (StackType a)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Error a -> TypeM a (StackType a))
-> Error a -> TypeM a (StackType a)
forall a b. (a -> b) -> a -> b
$ a -> TyName a -> Error a
forall a. a -> Name a -> Error a
PoorScope a
l TyName a
tn

-- expandType 1
dipify :: StackType () -> TypeM () (StackType ())
dipify :: StackType () -> TypeM () (StackType ())
dipify (StackType Set (Name ())
fvrs [KempeTy ()]
is [KempeTy ()]
os) = do
    Name ()
n <- Text -> TypeM () (Name ())
dummyName Text
"a"
    StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StackType () -> TypeM () (StackType ()))
-> StackType () -> TypeM () (StackType ())
forall a b. (a -> b) -> a -> b
$ Set (Name ()) -> [KempeTy ()] -> [KempeTy ()] -> StackType ()
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType (Name () -> Set (Name ()) -> Set (Name ())
forall a. Ord a => a -> Set a -> Set a
S.insert Name ()
n Set (Name ())
fvrs) ([KempeTy ()]
is [KempeTy ()] -> [KempeTy ()] -> [KempeTy ()]
forall a. [a] -> [a] -> [a]
++ [() -> Name () -> KempeTy ()
forall a. a -> Name a -> KempeTy a
TyVar () Name ()
n]) ([KempeTy ()]
os [KempeTy ()] -> [KempeTy ()] -> [KempeTy ()]
forall a. [a] -> [a] -> [a]
++ [() -> Name () -> KempeTy ()
forall a. a -> Name a -> KempeTy a
TyVar () Name ()
n])

tyLeaf :: (Pattern b a, [Atom b a]) -> TypeM () (StackType ())
tyLeaf :: (Pattern b a, [Atom b a]) -> TypeM () (StackType ())
tyLeaf (Pattern b a
p, [Atom b a]
as) = do
    StackType ()
tyP <- Pattern b a -> TypeM () (StackType ())
forall b a. Pattern b a -> TypeM () (StackType ())
tyPattern Pattern b a
p
    StackType ()
tyA <- [Atom b a] -> TypeM () (StackType ())
forall b a. [Atom b a] -> TypeM () (StackType ())
tyAtoms [Atom b a]
as
    StackType () -> StackType () -> TypeM () (StackType ())
catTypes StackType ()
tyP StackType ()
tyA

assignCase :: (Pattern b a, [Atom b a]) -> TypeM () (StackType (), Pattern (StackType ()) (StackType ()), [Atom (StackType ()) (StackType ())])
assignCase :: (Pattern b a, [Atom b a])
-> TypeM
     ()
     (StackType (), Pattern (StackType ()) (StackType ()),
      [Atom (StackType ()) (StackType ())])
assignCase (Pattern b a
p, [Atom b a]
as) = do
    (StackType ()
tyP, Pattern (StackType ()) (StackType ())
p') <- Pattern b a
-> TypeM () (StackType (), Pattern (StackType ()) (StackType ()))
forall b a.
Pattern b a
-> TypeM () (StackType (), Pattern (StackType ()) (StackType ()))
assignPattern Pattern b a
p
    ([Atom (StackType ()) (StackType ())]
as', StackType ()
tyA) <- [Atom b a]
-> TypeM () ([Atom (StackType ()) (StackType ())], StackType ())
forall b a.
[Atom b a]
-> TypeM () ([Atom (StackType ()) (StackType ())], StackType ())
assignAtoms [Atom b a]
as
    (,,) (StackType ()
 -> Pattern (StackType ()) (StackType ())
 -> [Atom (StackType ()) (StackType ())]
 -> (StackType (), Pattern (StackType ()) (StackType ()),
     [Atom (StackType ()) (StackType ())]))
-> TypeM () (StackType ())
-> StateT
     (TyState ())
     (Either (Error ()))
     (Pattern (StackType ()) (StackType ())
      -> [Atom (StackType ()) (StackType ())]
      -> (StackType (), Pattern (StackType ()) (StackType ()),
          [Atom (StackType ()) (StackType ())]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StackType () -> StackType () -> TypeM () (StackType ())
catTypes StackType ()
tyP StackType ()
tyA StateT
  (TyState ())
  (Either (Error ()))
  (Pattern (StackType ()) (StackType ())
   -> [Atom (StackType ()) (StackType ())]
   -> (StackType (), Pattern (StackType ()) (StackType ()),
       [Atom (StackType ()) (StackType ())]))
-> StateT
     (TyState ())
     (Either (Error ()))
     (Pattern (StackType ()) (StackType ()))
-> StateT
     (TyState ())
     (Either (Error ()))
     ([Atom (StackType ()) (StackType ())]
      -> (StackType (), Pattern (StackType ()) (StackType ()),
          [Atom (StackType ()) (StackType ())]))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Pattern (StackType ()) (StackType ())
-> StateT
     (TyState ())
     (Either (Error ()))
     (Pattern (StackType ()) (StackType ()))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Pattern (StackType ()) (StackType ())
p' StateT
  (TyState ())
  (Either (Error ()))
  ([Atom (StackType ()) (StackType ())]
   -> (StackType (), Pattern (StackType ()) (StackType ()),
       [Atom (StackType ()) (StackType ())]))
-> StateT
     (TyState ())
     (Either (Error ()))
     [Atom (StackType ()) (StackType ())]
-> TypeM
     ()
     (StackType (), Pattern (StackType ()) (StackType ()),
      [Atom (StackType ()) (StackType ())])
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Atom (StackType ()) (StackType ())]
-> StateT
     (TyState ())
     (Either (Error ()))
     [Atom (StackType ()) (StackType ())]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Atom (StackType ()) (StackType ())]
as'

tyAtom :: Atom b a -> TypeM () (StackType ())
tyAtom :: Atom b a -> TypeM () (StackType ())
tyAtom (AtBuiltin a
_ BuiltinFn
b) = BuiltinFn -> TypeM () (StackType ())
typeOfBuiltin BuiltinFn
b
tyAtom BoolLit{}       = StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StackType () -> TypeM () (StackType ()))
-> StackType () -> TypeM () (StackType ())
forall a b. (a -> b) -> a -> b
$ Set (Name ()) -> [KempeTy ()] -> [KempeTy ()] -> StackType ()
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType Set (Name ())
forall a. Monoid a => a
mempty [] [() -> BuiltinTy -> KempeTy ()
forall a. a -> BuiltinTy -> KempeTy a
TyBuiltin () BuiltinTy
TyBool]
tyAtom IntLit{}        = StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StackType () -> TypeM () (StackType ()))
-> StackType () -> TypeM () (StackType ())
forall a b. (a -> b) -> a -> b
$ Set (Name ()) -> [KempeTy ()] -> [KempeTy ()] -> StackType ()
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType Set (Name ())
forall a. Monoid a => a
mempty [] [() -> BuiltinTy -> KempeTy ()
forall a. a -> BuiltinTy -> KempeTy a
TyBuiltin () BuiltinTy
TyInt]
tyAtom Int8Lit{}       = StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StackType () -> TypeM () (StackType ()))
-> StackType () -> TypeM () (StackType ())
forall a b. (a -> b) -> a -> b
$ Set (Name ()) -> [KempeTy ()] -> [KempeTy ()] -> StackType ()
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType Set (Name ())
forall a. Monoid a => a
mempty [] [() -> BuiltinTy -> KempeTy ()
forall a. a -> BuiltinTy -> KempeTy a
TyBuiltin () BuiltinTy
TyInt8 ]
tyAtom WordLit{}       = StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StackType () -> TypeM () (StackType ()))
-> StackType () -> TypeM () (StackType ())
forall a b. (a -> b) -> a -> b
$ Set (Name ()) -> [KempeTy ()] -> [KempeTy ()] -> StackType ()
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType Set (Name ())
forall a. Monoid a => a
mempty [] [() -> BuiltinTy -> KempeTy ()
forall a. a -> BuiltinTy -> KempeTy a
TyBuiltin () BuiltinTy
TyWord]
tyAtom (AtName a
_ Name a
n)    = StackType () -> TypeM () (StackType ())
forall a. StackType a -> TypeM a (StackType a)
renameStack (StackType () -> TypeM () (StackType ()))
-> TypeM () (StackType ()) -> TypeM () (StackType ())
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Name () -> TypeM () (StackType ())
forall a. Name a -> TypeM a (StackType a)
tyLookup (Name a -> Name ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Name a
n)
tyAtom (Dip a
_ [Atom b a]
as)      = StackType () -> TypeM () (StackType ())
dipify (StackType () -> TypeM () (StackType ()))
-> TypeM () (StackType ()) -> TypeM () (StackType ())
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Atom b a] -> TypeM () (StackType ())
forall b a. [Atom b a] -> TypeM () (StackType ())
tyAtoms [Atom b a]
as
tyAtom (AtCons b
_ TyName b
tn)   = StackType () -> TypeM () (StackType ())
forall a. StackType a -> TypeM a (StackType a)
renameStack (StackType () -> TypeM () (StackType ()))
-> TypeM () (StackType ()) -> TypeM () (StackType ())
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Name () -> TypeM () (StackType ())
forall a. Name a -> TypeM a (StackType a)
consLookup (TyName b -> Name ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void TyName b
tn)
tyAtom (If a
_ [Atom b a]
as [Atom b a]
as')   = do
    StackType ()
tys <- [Atom b a] -> TypeM () (StackType ())
forall b a. [Atom b a] -> TypeM () (StackType ())
tyAtoms [Atom b a]
as
    StackType ()
tys' <- [Atom b a] -> TypeM () (StackType ())
forall b a. [Atom b a] -> TypeM () (StackType ())
tyAtoms [Atom b a]
as'
    (StackType Set (Name ())
vars [KempeTy ()]
ins [KempeTy ()]
out) <- StackType () -> StackType () -> TypeM () (StackType ())
mergeStackTypes StackType ()
tys StackType ()
tys'
    StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StackType () -> TypeM () (StackType ()))
-> StackType () -> TypeM () (StackType ())
forall a b. (a -> b) -> a -> b
$ Set (Name ()) -> [KempeTy ()] -> [KempeTy ()] -> StackType ()
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType Set (Name ())
vars ([KempeTy ()]
ins [KempeTy ()] -> [KempeTy ()] -> [KempeTy ()]
forall a. [a] -> [a] -> [a]
++ [() -> BuiltinTy -> KempeTy ()
forall a. a -> BuiltinTy -> KempeTy a
TyBuiltin () BuiltinTy
TyBool]) [KempeTy ()]
out
tyAtom (Case a
_ NonEmpty (Pattern b a, [Atom b a])
ls) = do
    NonEmpty (StackType ())
tyLs <- ((Pattern b a, [Atom b a]) -> TypeM () (StackType ()))
-> NonEmpty (Pattern b a, [Atom b a])
-> StateT
     (TyState ()) (Either (Error ())) (NonEmpty (StackType ()))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Pattern b a, [Atom b a]) -> TypeM () (StackType ())
forall b a. (Pattern b a, [Atom b a]) -> TypeM () (StackType ())
tyLeaf NonEmpty (Pattern b a, [Atom b a])
ls
    -- TODO: one-pass fold?
    NonEmpty (StackType ()) -> TypeM () (StackType ())
mergeMany NonEmpty (StackType ())
tyLs

assignAtom :: Atom b a -> TypeM () (StackType (), Atom (StackType ()) (StackType ()))
assignAtom :: Atom b a
-> TypeM () (StackType (), Atom (StackType ()) (StackType ()))
assignAtom (AtBuiltin a
_ BuiltinFn
b) = do { StackType ()
ty <- BuiltinFn -> TypeM () (StackType ())
typeOfBuiltin BuiltinFn
b ; (StackType (), Atom (StackType ()) (StackType ()))
-> TypeM () (StackType (), Atom (StackType ()) (StackType ()))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StackType ()
ty, StackType () -> BuiltinFn -> Atom (StackType ()) (StackType ())
forall c b. b -> BuiltinFn -> Atom c b
AtBuiltin StackType ()
ty BuiltinFn
b) }
assignAtom (BoolLit a
_ Bool
b)   =
    let sTy :: StackType ()
sTy = Set (Name ()) -> [KempeTy ()] -> [KempeTy ()] -> StackType ()
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType Set (Name ())
forall a. Monoid a => a
mempty [] [() -> BuiltinTy -> KempeTy ()
forall a. a -> BuiltinTy -> KempeTy a
TyBuiltin () BuiltinTy
TyBool]
        in (StackType (), Atom (StackType ()) (StackType ()))
-> TypeM () (StackType (), Atom (StackType ()) (StackType ()))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StackType ()
sTy, StackType () -> Bool -> Atom (StackType ()) (StackType ())
forall c b. b -> Bool -> Atom c b
BoolLit StackType ()
sTy Bool
b)
assignAtom (IntLit a
_ Integer
i)    =
    let sTy :: StackType ()
sTy = Set (Name ()) -> [KempeTy ()] -> [KempeTy ()] -> StackType ()
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType Set (Name ())
forall a. Monoid a => a
mempty [] [() -> BuiltinTy -> KempeTy ()
forall a. a -> BuiltinTy -> KempeTy a
TyBuiltin () BuiltinTy
TyInt]
        in (StackType (), Atom (StackType ()) (StackType ()))
-> TypeM () (StackType (), Atom (StackType ()) (StackType ()))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StackType ()
sTy, StackType () -> Integer -> Atom (StackType ()) (StackType ())
forall c b. b -> Integer -> Atom c b
IntLit StackType ()
sTy Integer
i)
assignAtom (Int8Lit a
_ Int8
i)    =
    let sTy :: StackType ()
sTy = Set (Name ()) -> [KempeTy ()] -> [KempeTy ()] -> StackType ()
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType Set (Name ())
forall a. Monoid a => a
mempty [] [() -> BuiltinTy -> KempeTy ()
forall a. a -> BuiltinTy -> KempeTy a
TyBuiltin () BuiltinTy
TyInt8]
        in (StackType (), Atom (StackType ()) (StackType ()))
-> TypeM () (StackType (), Atom (StackType ()) (StackType ()))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StackType ()
sTy, StackType () -> Int8 -> Atom (StackType ()) (StackType ())
forall c b. b -> Int8 -> Atom c b
Int8Lit StackType ()
sTy Int8
i)
assignAtom (WordLit a
_ Natural
u)    =
    let sTy :: StackType ()
sTy = Set (Name ()) -> [KempeTy ()] -> [KempeTy ()] -> StackType ()
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType Set (Name ())
forall a. Monoid a => a
mempty [] [() -> BuiltinTy -> KempeTy ()
forall a. a -> BuiltinTy -> KempeTy a
TyBuiltin () BuiltinTy
TyWord]
        in (StackType (), Atom (StackType ()) (StackType ()))
-> TypeM () (StackType (), Atom (StackType ()) (StackType ()))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StackType ()
sTy, StackType () -> Natural -> Atom (StackType ()) (StackType ())
forall c b. b -> Natural -> Atom c b
WordLit StackType ()
sTy Natural
u)
assignAtom (AtName a
_ Name a
n) = do
    StackType ()
sTy <- StackType () -> TypeM () (StackType ())
forall a. StackType a -> TypeM a (StackType a)
renameStack (StackType () -> TypeM () (StackType ()))
-> TypeM () (StackType ()) -> TypeM () (StackType ())
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Name () -> TypeM () (StackType ())
forall a. Name a -> TypeM a (StackType a)
tyLookup (Name a -> Name ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Name a
n)
    (StackType (), Atom (StackType ()) (StackType ()))
-> TypeM () (StackType (), Atom (StackType ()) (StackType ()))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StackType ()
sTy, StackType ()
-> Name (StackType ()) -> Atom (StackType ()) (StackType ())
forall c b. b -> Name b -> Atom c b
AtName StackType ()
sTy (Name a
n Name a -> StackType () -> Name (StackType ())
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> StackType ()
sTy))
assignAtom (AtCons b
_ TyName b
tn) = do
    StackType ()
sTy <- StackType () -> TypeM () (StackType ())
forall a. StackType a -> TypeM a (StackType a)
renameStack (StackType () -> TypeM () (StackType ()))
-> TypeM () (StackType ()) -> TypeM () (StackType ())
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Name () -> TypeM () (StackType ())
forall a. Name a -> TypeM a (StackType a)
consLookup (TyName b -> Name ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void TyName b
tn)
    (StackType (), Atom (StackType ()) (StackType ()))
-> TypeM () (StackType (), Atom (StackType ()) (StackType ()))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StackType ()
sTy, StackType ()
-> Name (StackType ()) -> Atom (StackType ()) (StackType ())
forall c b. c -> TyName c -> Atom c b
AtCons StackType ()
sTy (TyName b
tn TyName b -> StackType () -> Name (StackType ())
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> StackType ()
sTy))
assignAtom (Dip a
_ [Atom b a]
as)    = do { ([Atom (StackType ()) (StackType ())]
as', StackType ()
ty) <- [Atom b a]
-> TypeM () ([Atom (StackType ()) (StackType ())], StackType ())
forall b a.
[Atom b a]
-> TypeM () ([Atom (StackType ()) (StackType ())], StackType ())
assignAtoms [Atom b a]
as ; StackType ()
tyDipped <- StackType () -> TypeM () (StackType ())
dipify StackType ()
ty ; (StackType (), Atom (StackType ()) (StackType ()))
-> TypeM () (StackType (), Atom (StackType ()) (StackType ()))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StackType ()
tyDipped, StackType ()
-> [Atom (StackType ()) (StackType ())]
-> Atom (StackType ()) (StackType ())
forall c b. b -> [Atom c b] -> Atom c b
Dip StackType ()
tyDipped [Atom (StackType ()) (StackType ())]
as') }
assignAtom (If a
_ [Atom b a]
as0 [Atom b a]
as1) = do
    ([Atom (StackType ()) (StackType ())]
as0', StackType ()
tys) <- [Atom b a]
-> TypeM () ([Atom (StackType ()) (StackType ())], StackType ())
forall b a.
[Atom b a]
-> TypeM () ([Atom (StackType ()) (StackType ())], StackType ())
assignAtoms [Atom b a]
as0
    ([Atom (StackType ()) (StackType ())]
as1', StackType ()
tys') <- [Atom b a]
-> TypeM () ([Atom (StackType ()) (StackType ())], StackType ())
forall b a.
[Atom b a]
-> TypeM () ([Atom (StackType ()) (StackType ())], StackType ())
assignAtoms [Atom b a]
as1
    (StackType Set (Name ())
vars [KempeTy ()]
ins [KempeTy ()]
out) <- StackType () -> StackType () -> TypeM () (StackType ())
mergeStackTypes StackType ()
tys StackType ()
tys'
    let resType :: StackType ()
resType = Set (Name ()) -> [KempeTy ()] -> [KempeTy ()] -> StackType ()
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType Set (Name ())
vars ([KempeTy ()]
ins [KempeTy ()] -> [KempeTy ()] -> [KempeTy ()]
forall a. [a] -> [a] -> [a]
++ [() -> BuiltinTy -> KempeTy ()
forall a. a -> BuiltinTy -> KempeTy a
TyBuiltin () BuiltinTy
TyBool]) [KempeTy ()]
out
    (StackType (), Atom (StackType ()) (StackType ()))
-> TypeM () (StackType (), Atom (StackType ()) (StackType ()))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StackType ()
resType, StackType ()
-> [Atom (StackType ()) (StackType ())]
-> [Atom (StackType ()) (StackType ())]
-> Atom (StackType ()) (StackType ())
forall c b. b -> [Atom c b] -> [Atom c b] -> Atom c b
If StackType ()
resType [Atom (StackType ()) (StackType ())]
as0' [Atom (StackType ()) (StackType ())]
as1')
assignAtom (Case a
_ NonEmpty (Pattern b a, [Atom b a])
ls) = do
    NonEmpty
  (StackType (), Pattern (StackType ()) (StackType ()),
   [Atom (StackType ()) (StackType ())])
lRes <- ((Pattern b a, [Atom b a])
 -> TypeM
      ()
      (StackType (), Pattern (StackType ()) (StackType ()),
       [Atom (StackType ()) (StackType ())]))
-> NonEmpty (Pattern b a, [Atom b a])
-> StateT
     (TyState ())
     (Either (Error ()))
     (NonEmpty
        (StackType (), Pattern (StackType ()) (StackType ()),
         [Atom (StackType ()) (StackType ())]))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Pattern b a, [Atom b a])
-> TypeM
     ()
     (StackType (), Pattern (StackType ()) (StackType ()),
      [Atom (StackType ()) (StackType ())])
forall b a.
(Pattern b a, [Atom b a])
-> TypeM
     ()
     (StackType (), Pattern (StackType ()) (StackType ()),
      [Atom (StackType ()) (StackType ())])
assignCase NonEmpty (Pattern b a, [Atom b a])
ls
    StackType ()
resType <- NonEmpty (StackType ()) -> TypeM () (StackType ())
mergeMany ((StackType (), Pattern (StackType ()) (StackType ()),
 [Atom (StackType ()) (StackType ())])
-> StackType ()
forall a b c. (a, b, c) -> a
fst3 ((StackType (), Pattern (StackType ()) (StackType ()),
  [Atom (StackType ()) (StackType ())])
 -> StackType ())
-> NonEmpty
     (StackType (), Pattern (StackType ()) (StackType ()),
      [Atom (StackType ()) (StackType ())])
-> NonEmpty (StackType ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty
  (StackType (), Pattern (StackType ()) (StackType ()),
   [Atom (StackType ()) (StackType ())])
lRes)
    let newLeaves :: NonEmpty
  (Pattern (StackType ()) (StackType ()),
   [Atom (StackType ()) (StackType ())])
newLeaves = ((StackType (), Pattern (StackType ()) (StackType ()),
  [Atom (StackType ()) (StackType ())])
 -> (Pattern (StackType ()) (StackType ()),
     [Atom (StackType ()) (StackType ())]))
-> NonEmpty
     (StackType (), Pattern (StackType ()) (StackType ()),
      [Atom (StackType ()) (StackType ())])
-> NonEmpty
     (Pattern (StackType ()) (StackType ()),
      [Atom (StackType ()) (StackType ())])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (StackType (), Pattern (StackType ()) (StackType ()),
 [Atom (StackType ()) (StackType ())])
-> (Pattern (StackType ()) (StackType ()),
    [Atom (StackType ()) (StackType ())])
forall a a b. (a, a, b) -> (a, b)
dropFst NonEmpty
  (StackType (), Pattern (StackType ()) (StackType ()),
   [Atom (StackType ()) (StackType ())])
lRes
    (StackType (), Atom (StackType ()) (StackType ()))
-> TypeM () (StackType (), Atom (StackType ()) (StackType ()))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StackType ()
resType, StackType ()
-> NonEmpty
     (Pattern (StackType ()) (StackType ()),
      [Atom (StackType ()) (StackType ())])
-> Atom (StackType ()) (StackType ())
forall c b. b -> NonEmpty (Pattern c b, [Atom c b]) -> Atom c b
Case StackType ()
resType NonEmpty
  (Pattern (StackType ()) (StackType ()),
   [Atom (StackType ()) (StackType ())])
newLeaves)
    where dropFst :: (a, a, b) -> (a, b)
dropFst (a
_, a
y, b
z) = (a
y, b
z)

assignAtoms :: [Atom b a] -> TypeM () ([Atom (StackType ()) (StackType ())], StackType ())
assignAtoms :: [Atom b a]
-> TypeM () ([Atom (StackType ()) (StackType ())], StackType ())
assignAtoms = (([Atom (StackType ()) (StackType ())], StackType ())
 -> Atom b a
 -> TypeM () ([Atom (StackType ()) (StackType ())], StackType ()))
-> ([Atom (StackType ()) (StackType ())], StackType ())
-> [Atom b a]
-> TypeM () ([Atom (StackType ()) (StackType ())], StackType ())
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM
    (\([Atom (StackType ()) (StackType ())], StackType ())
seed Atom b a
a -> do { (StackType ()
ty, Atom (StackType ()) (StackType ())
r) <- Atom b a
-> TypeM () (StackType (), Atom (StackType ()) (StackType ()))
forall b a.
Atom b a
-> TypeM () (StackType (), Atom (StackType ()) (StackType ()))
assignAtom Atom b a
a ; (([Atom (StackType ()) (StackType ())], StackType ())
-> [Atom (StackType ()) (StackType ())]
forall a b. (a, b) -> a
fst ([Atom (StackType ()) (StackType ())], StackType ())
seed [Atom (StackType ()) (StackType ())]
-> [Atom (StackType ()) (StackType ())]
-> [Atom (StackType ()) (StackType ())]
forall a. [a] -> [a] -> [a]
++ [Atom (StackType ()) (StackType ())
r] ,) (StackType ()
 -> ([Atom (StackType ()) (StackType ())], StackType ()))
-> TypeM () (StackType ())
-> TypeM () ([Atom (StackType ()) (StackType ())], StackType ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StackType () -> StackType () -> TypeM () (StackType ())
catTypes (([Atom (StackType ()) (StackType ())], StackType ())
-> StackType ()
forall a b. (a, b) -> b
snd ([Atom (StackType ()) (StackType ())], StackType ())
seed) StackType ()
ty })
    ([], StackType ()
forall a. StackType a
emptyStackType)

tyAtoms :: [Atom b a] -> TypeM () (StackType ())
tyAtoms :: [Atom b a] -> TypeM () (StackType ())
tyAtoms = (StackType () -> Atom b a -> TypeM () (StackType ()))
-> StackType () -> [Atom b a] -> TypeM () (StackType ())
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM
    (\StackType ()
seed Atom b a
a -> do { StackType ()
tys' <- Atom b a -> TypeM () (StackType ())
forall b a. Atom b a -> TypeM () (StackType ())
tyAtom Atom b a
a ; StackType () -> StackType () -> TypeM () (StackType ())
catTypes StackType ()
seed StackType ()
tys' })
    StackType ()
forall a. StackType a
emptyStackType

-- from size,
mkHKT :: Int -> Kind
mkHKT :: Int -> Kind
mkHKT Int
0 = Kind
Star
mkHKT Int
i = Kind -> Kind -> Kind
TyCons (Int -> Kind
mkHKT (Int -> Kind) -> Int -> Kind
forall a b. (a -> b) -> a -> b
$ Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Kind
Star

tyInsertLeaf :: Name b -- ^ type being declared
             -> S.Set (Name b) -> (TyName a, [KempeTy b]) -> TypeM () ()
tyInsertLeaf :: Name b
-> Set (Name b)
-> (TyName a, [KempeTy b])
-> StateT (TyState ()) (Either (Error ())) ()
tyInsertLeaf n :: Name b
n@(Name Text
_ (Unique Int
k) b
_) Set (Name b)
vars (Name Text
_ (Unique Int
i) a
_, [KempeTy b]
ins) | Set (Name b) -> Bool
forall a. Set a -> Bool
S.null Set (Name b)
vars =
    ASetter
  (TyState ())
  (TyState ())
  (IntMap (StackType ()))
  (IntMap (StackType ()))
-> (IntMap (StackType ()) -> IntMap (StackType ()))
-> StateT (TyState ()) (Either (Error ())) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
modifying ASetter
  (TyState ())
  (TyState ())
  (IntMap (StackType ()))
  (IntMap (StackType ()))
forall a. Lens' (TyState a) (IntMap (StackType a))
constructorTypesLens (Int
-> StackType () -> IntMap (StackType ()) -> IntMap (StackType ())
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
i (StackType b -> StackType ()
forall a. StackType a -> StackType ()
voidStackType (StackType b -> StackType ()) -> StackType b -> StackType ()
forall a b. (a -> b) -> a -> b
$ Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType Set (Name b)
vars [KempeTy b]
ins [b -> Name b -> KempeTy b
forall a. a -> Name a -> KempeTy a
TyNamed b
forall a. HasCallStack => a
undefined Name b
n])) StateT (TyState ()) (Either (Error ())) ()
-> StateT (TyState ()) (Either (Error ())) ()
-> StateT (TyState ()) (Either (Error ())) ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*>
    ASetter (TyState ()) (TyState ()) (IntMap Kind) (IntMap Kind)
-> (IntMap Kind -> IntMap Kind)
-> StateT (TyState ()) (Either (Error ())) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
modifying ASetter (TyState ()) (TyState ()) (IntMap Kind) (IntMap Kind)
forall a. Lens' (TyState a) (IntMap Kind)
kindEnvLens (Int -> Kind -> IntMap Kind -> IntMap Kind
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
k Kind
Star)
                                               | Bool
otherwise =
    let ty :: StackType ()
ty = StackType b -> StackType ()
forall a. StackType a -> StackType ()
voidStackType (StackType b -> StackType ()) -> StackType b -> StackType ()
forall a b. (a -> b) -> a -> b
$ Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType Set (Name b)
vars [KempeTy b]
ins [KempeTy b -> [Name b] -> KempeTy b
forall a. KempeTy a -> [Name a] -> KempeTy a
app (b -> Name b -> KempeTy b
forall a. a -> Name a -> KempeTy a
TyNamed b
forall a. HasCallStack => a
undefined Name b
n) (Set (Name b) -> [Name b]
forall a. Set a -> [a]
S.toList Set (Name b)
vars)] in
    ASetter
  (TyState ())
  (TyState ())
  (IntMap (StackType ()))
  (IntMap (StackType ()))
-> (IntMap (StackType ()) -> IntMap (StackType ()))
-> StateT (TyState ()) (Either (Error ())) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
modifying ASetter
  (TyState ())
  (TyState ())
  (IntMap (StackType ()))
  (IntMap (StackType ()))
forall a. Lens' (TyState a) (IntMap (StackType a))
constructorTypesLens (Int
-> StackType () -> IntMap (StackType ()) -> IntMap (StackType ())
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
i StackType ()
ty) StateT (TyState ()) (Either (Error ())) ()
-> StateT (TyState ()) (Either (Error ())) ()
-> StateT (TyState ()) (Either (Error ())) ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*>
    ASetter (TyState ()) (TyState ()) (IntMap Kind) (IntMap Kind)
-> (IntMap Kind -> IntMap Kind)
-> StateT (TyState ()) (Either (Error ())) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
modifying ASetter (TyState ()) (TyState ()) (IntMap Kind) (IntMap Kind)
forall a. Lens' (TyState a) (IntMap Kind)
kindEnvLens (Int -> Kind -> IntMap Kind -> IntMap Kind
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
k (Int -> Kind
mkHKT (Int -> Kind) -> Int -> Kind
forall a b. (a -> b) -> a -> b
$ Set (Name b) -> Int
forall a. Set a -> Int
S.size Set (Name b)
vars))

assignTyLeaf :: Name b
             -> S.Set (Name b)
             -> (TyName a, [KempeTy b])
             -> TypeM () (TyName (StackType ()), [KempeTy ()])
assignTyLeaf :: Name b
-> Set (Name b)
-> (TyName a, [KempeTy b])
-> TypeM () (Name (StackType ()), [KempeTy ()])
assignTyLeaf n :: Name b
n@(Name Text
_ (Unique Int
k) b
_) Set (Name b)
vars (tn :: TyName a
tn@(Name Text
_ (Unique Int
i) a
_), [KempeTy b]
ins) | Set (Name b) -> Bool
forall a. Set a -> Bool
S.null Set (Name b)
vars =
    let ty :: StackType ()
ty = StackType b -> StackType ()
forall a. StackType a -> StackType ()
voidStackType (StackType b -> StackType ()) -> StackType b -> StackType ()
forall a b. (a -> b) -> a -> b
$ Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType Set (Name b)
vars [KempeTy b]
ins [b -> Name b -> KempeTy b
forall a. a -> Name a -> KempeTy a
TyNamed b
forall a. HasCallStack => a
undefined Name b
n] in
    ASetter
  (TyState ())
  (TyState ())
  (IntMap (StackType ()))
  (IntMap (StackType ()))
-> (IntMap (StackType ()) -> IntMap (StackType ()))
-> StateT (TyState ()) (Either (Error ())) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
modifying ASetter
  (TyState ())
  (TyState ())
  (IntMap (StackType ()))
  (IntMap (StackType ()))
forall a. Lens' (TyState a) (IntMap (StackType a))
constructorTypesLens (Int
-> StackType () -> IntMap (StackType ()) -> IntMap (StackType ())
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
i StackType ()
ty) StateT (TyState ()) (Either (Error ())) ()
-> StateT (TyState ()) (Either (Error ())) ()
-> StateT (TyState ()) (Either (Error ())) ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*>
    ASetter (TyState ()) (TyState ()) (IntMap Kind) (IntMap Kind)
-> (IntMap Kind -> IntMap Kind)
-> StateT (TyState ()) (Either (Error ())) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
modifying ASetter (TyState ()) (TyState ()) (IntMap Kind) (IntMap Kind)
forall a. Lens' (TyState a) (IntMap Kind)
kindEnvLens (Int -> Kind -> IntMap Kind -> IntMap Kind
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
k Kind
Star) StateT (TyState ()) (Either (Error ())) ()
-> (Name (StackType ()), [KempeTy ()])
-> TypeM () (Name (StackType ()), [KempeTy ()])
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$>
    (TyName a
tn TyName a -> StackType () -> Name (StackType ())
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> StackType ()
ty, (KempeTy b -> KempeTy ()) -> [KempeTy b] -> [KempeTy ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap KempeTy b -> KempeTy ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void [KempeTy b]
ins)
                                               | Bool
otherwise =
    let ty :: StackType ()
ty = StackType b -> StackType ()
forall a. StackType a -> StackType ()
voidStackType (StackType b -> StackType ()) -> StackType b -> StackType ()
forall a b. (a -> b) -> a -> b
$ Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType Set (Name b)
vars [KempeTy b]
ins [KempeTy b -> [Name b] -> KempeTy b
forall a. KempeTy a -> [Name a] -> KempeTy a
app (b -> Name b -> KempeTy b
forall a. a -> Name a -> KempeTy a
TyNamed b
forall a. HasCallStack => a
undefined Name b
n) (Set (Name b) -> [Name b]
forall a. Set a -> [a]
S.toList Set (Name b)
vars)] in
    ASetter
  (TyState ())
  (TyState ())
  (IntMap (StackType ()))
  (IntMap (StackType ()))
-> (IntMap (StackType ()) -> IntMap (StackType ()))
-> StateT (TyState ()) (Either (Error ())) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
modifying ASetter
  (TyState ())
  (TyState ())
  (IntMap (StackType ()))
  (IntMap (StackType ()))
forall a. Lens' (TyState a) (IntMap (StackType a))
constructorTypesLens (Int
-> StackType () -> IntMap (StackType ()) -> IntMap (StackType ())
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
i StackType ()
ty) StateT (TyState ()) (Either (Error ())) ()
-> StateT (TyState ()) (Either (Error ())) ()
-> StateT (TyState ()) (Either (Error ())) ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*>
    ASetter (TyState ()) (TyState ()) (IntMap Kind) (IntMap Kind)
-> (IntMap Kind -> IntMap Kind)
-> StateT (TyState ()) (Either (Error ())) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
modifying ASetter (TyState ()) (TyState ()) (IntMap Kind) (IntMap Kind)
forall a. Lens' (TyState a) (IntMap Kind)
kindEnvLens (Int -> Kind -> IntMap Kind -> IntMap Kind
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
k (Int -> Kind
mkHKT (Int -> Kind) -> Int -> Kind
forall a b. (a -> b) -> a -> b
$ Set (Name b) -> Int
forall a. Set a -> Int
S.size Set (Name b)
vars)) StateT (TyState ()) (Either (Error ())) ()
-> (Name (StackType ()), [KempeTy ()])
-> TypeM () (Name (StackType ()), [KempeTy ()])
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$>
    (TyName a
tn TyName a -> StackType () -> Name (StackType ())
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> StackType ()
ty, (KempeTy b -> KempeTy ()) -> [KempeTy b] -> [KempeTy ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap KempeTy b -> KempeTy ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void [KempeTy b]
ins)

app :: KempeTy a -> [Name a] -> KempeTy a
app :: KempeTy a -> [Name a] -> KempeTy a
app = (KempeTy a -> Name a -> KempeTy a)
-> KempeTy a -> [Name a] -> KempeTy a
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\KempeTy a
ty Name a
n -> a -> KempeTy a -> KempeTy a -> KempeTy a
forall a. a -> KempeTy a -> KempeTy a -> KempeTy a
TyApp a
forall a. HasCallStack => a
undefined KempeTy a
ty (a -> Name a -> KempeTy a
forall a. a -> Name a -> KempeTy a
TyVar a
forall a. HasCallStack => a
undefined Name a
n))

kindLookup :: TyName a -> TypeM a Kind
kindLookup :: TyName a -> TypeM a Kind
kindLookup n :: TyName a
n@(Name Text
_ (Unique Int
i) a
l) = do
    IntMap Kind
st <- (TyState a -> IntMap Kind)
-> StateT (TyState a) (Either (Error a)) (IntMap Kind)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TyState a -> IntMap Kind
forall a. TyState a -> IntMap Kind
kindEnv
    case Int -> IntMap Kind -> Maybe Kind
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
i IntMap Kind
st of
        Just Kind
k  -> Kind -> TypeM a Kind
forall (f :: * -> *) a. Applicative f => a -> f a
pure Kind
k
        Maybe Kind
Nothing -> Error a -> TypeM a Kind
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Error a -> TypeM a Kind) -> Error a -> TypeM a Kind
forall a b. (a -> b) -> a -> b
$ a -> TyName a -> Error a
forall a. a -> Name a -> Error a
PoorScope a
l TyName a
n

kindOf :: KempeTy a -> TypeM a Kind
kindOf :: KempeTy a -> TypeM a Kind
kindOf TyBuiltin{}        = Kind -> TypeM a Kind
forall (f :: * -> *) a. Applicative f => a -> f a
pure Kind
Star
kindOf (TyNamed a
_ TyName a
tn)     = TyName a -> TypeM a Kind
forall a. TyName a -> TypeM a Kind
kindLookup TyName a
tn
kindOf TyVar{}            = Kind -> TypeM a Kind
forall (f :: * -> *) a. Applicative f => a -> f a
pure Kind
Star
kindOf tyErr :: KempeTy a
tyErr@(TyApp a
l KempeTy a
ty KempeTy a
ty') = do
    Kind
k <- KempeTy a -> TypeM a Kind
forall a. KempeTy a -> TypeM a Kind
kindOf KempeTy a
ty
    Kind
k' <- KempeTy a -> TypeM a Kind
forall a. KempeTy a -> TypeM a Kind
kindOf KempeTy a
ty'
    case Kind
k of
        TyCons Kind
k'' Kind
k''' -> Bool
-> StateT (TyState a) (Either (Error a)) ()
-> StateT (TyState a) (Either (Error a)) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Kind
k' Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
k''') (Error a -> StateT (TyState a) (Either (Error a)) ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (a -> KempeTy a -> Error a
forall a. a -> KempeTy a -> Error a
IllKinded a
l KempeTy a
tyErr)) StateT (TyState a) (Either (Error a)) () -> Kind -> TypeM a Kind
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Kind
k''
        Kind
_               -> Error a -> TypeM a Kind
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (a -> KempeTy a -> Error a
forall a. a -> KempeTy a -> Error a
IllKinded a
l KempeTy a
tyErr)

assignDecl :: KempeDecl a c b -> TypeM () (KempeDecl () (StackType ()) (StackType ()))
assignDecl :: KempeDecl a c b
-> TypeM () (KempeDecl () (StackType ()) (StackType ()))
assignDecl (TyDecl a
_ TyName a
tn [TyName a]
ns [(TyName b, [KempeTy a])]
ls) = ()
-> Name ()
-> [Name ()]
-> [(Name (StackType ()), [KempeTy ()])]
-> KempeDecl () (StackType ()) (StackType ())
forall a c b.
a
-> TyName a
-> [TyName a]
-> [(TyName b, [KempeTy a])]
-> KempeDecl a c b
TyDecl () (TyName a -> Name ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void TyName a
tn) (TyName a -> Name ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (TyName a -> Name ()) -> [TyName a] -> [Name ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TyName a]
ns) ([(Name (StackType ()), [KempeTy ()])]
 -> KempeDecl () (StackType ()) (StackType ()))
-> StateT
     (TyState ())
     (Either (Error ()))
     [(Name (StackType ()), [KempeTy ()])]
-> TypeM () (KempeDecl () (StackType ()) (StackType ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((TyName b, [KempeTy a])
 -> TypeM () (Name (StackType ()), [KempeTy ()]))
-> [(TyName b, [KempeTy a])]
-> StateT
     (TyState ())
     (Either (Error ()))
     [(Name (StackType ()), [KempeTy ()])]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (TyName a
-> Set (TyName a)
-> (TyName b, [KempeTy a])
-> TypeM () (Name (StackType ()), [KempeTy ()])
forall b a.
Name b
-> Set (Name b)
-> (TyName a, [KempeTy b])
-> TypeM () (Name (StackType ()), [KempeTy ()])
assignTyLeaf TyName a
tn ([TyName a] -> Set (TyName a)
forall a. Ord a => [a] -> Set a
S.fromList [TyName a]
ns)) [(TyName b, [KempeTy a])]
ls
assignDecl (FunDecl b
_ TyName b
n [KempeTy a]
ins [KempeTy a]
os [Atom c b]
a) = do
    (KempeTy () -> StateT (TyState ()) (Either (Error ())) Kind)
-> [KempeTy ()] -> StateT (TyState ()) (Either (Error ())) ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ KempeTy () -> StateT (TyState ()) (Either (Error ())) Kind
forall a. KempeTy a -> TypeM a Kind
kindOf (KempeTy a -> KempeTy ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (KempeTy a -> KempeTy ()) -> [KempeTy a] -> [KempeTy ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [KempeTy a]
ins [KempeTy a] -> [KempeTy a] -> [KempeTy a]
forall a. [a] -> [a] -> [a]
++ [KempeTy a]
os)
    StackType ()
sig <- StackType () -> TypeM () (StackType ())
forall a. StackType a -> TypeM a (StackType a)
renameStack (StackType () -> TypeM () (StackType ()))
-> StackType () -> TypeM () (StackType ())
forall a b. (a -> b) -> a -> b
$ StackType a -> StackType ()
forall a. StackType a -> StackType ()
voidStackType (StackType a -> StackType ()) -> StackType a -> StackType ()
forall a b. (a -> b) -> a -> b
$ Set (TyName a) -> [KempeTy a] -> [KempeTy a] -> StackType a
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType ([KempeTy a] -> Set (TyName a)
forall a. [KempeTy a] -> Set (Name a)
freeVars ([KempeTy a]
ins [KempeTy a] -> [KempeTy a] -> [KempeTy a]
forall a. [a] -> [a] -> [a]
++ [KempeTy a]
os)) [KempeTy a]
ins [KempeTy a]
os
    ([Atom (StackType ()) (StackType ())]
as, StackType ()
inferred) <- [Atom c b]
-> TypeM () ([Atom (StackType ()) (StackType ())], StackType ())
forall b a.
[Atom b a]
-> TypeM () ([Atom (StackType ()) (StackType ())], StackType ())
assignAtoms [Atom c b]
a
    StackType ()
reconcile <- StackType () -> StackType () -> TypeM () (StackType ())
mergeStackTypes StackType ()
sig StackType ()
inferred
    -- assign comes after tyInsert
    KempeDecl () (StackType ()) (StackType ())
-> TypeM () (KempeDecl () (StackType ()) (StackType ()))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (KempeDecl () (StackType ()) (StackType ())
 -> TypeM () (KempeDecl () (StackType ()) (StackType ())))
-> KempeDecl () (StackType ()) (StackType ())
-> TypeM () (KempeDecl () (StackType ()) (StackType ()))
forall a b. (a -> b) -> a -> b
$ StackType ()
-> Name (StackType ())
-> [KempeTy ()]
-> [KempeTy ()]
-> [Atom (StackType ()) (StackType ())]
-> KempeDecl () (StackType ()) (StackType ())
forall a c b.
b
-> TyName b
-> [KempeTy a]
-> [KempeTy a]
-> [Atom c b]
-> KempeDecl a c b
FunDecl StackType ()
reconcile (TyName b
n TyName b -> StackType () -> Name (StackType ())
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> StackType ()
reconcile) (KempeTy a -> KempeTy ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (KempeTy a -> KempeTy ()) -> [KempeTy a] -> [KempeTy ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [KempeTy a]
ins) (KempeTy a -> KempeTy ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (KempeTy a -> KempeTy ()) -> [KempeTy a] -> [KempeTy ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [KempeTy a]
os) [Atom (StackType ()) (StackType ())]
as
assignDecl (ExtFnDecl b
_ TyName b
n [KempeTy a]
ins [KempeTy a]
os ByteString
cn) = do
    (KempeTy () -> StateT (TyState ()) (Either (Error ())) Kind)
-> [KempeTy ()] -> StateT (TyState ()) (Either (Error ())) ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ KempeTy () -> StateT (TyState ()) (Either (Error ())) Kind
forall a. KempeTy a -> TypeM a Kind
kindOf (KempeTy a -> KempeTy ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (KempeTy a -> KempeTy ()) -> [KempeTy a] -> [KempeTy ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [KempeTy a]
ins [KempeTy a] -> [KempeTy a] -> [KempeTy a]
forall a. [a] -> [a] -> [a]
++ [KempeTy a]
os)
    Bool
-> StateT (TyState ()) (Either (Error ())) ()
-> StateT (TyState ()) (Either (Error ())) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([KempeTy a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [KempeTy a]
os Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1) (StateT (TyState ()) (Either (Error ())) ()
 -> StateT (TyState ()) (Either (Error ())) ())
-> StateT (TyState ()) (Either (Error ())) ()
-> StateT (TyState ()) (Either (Error ())) ()
forall a b. (a -> b) -> a -> b
$
        Error () -> StateT (TyState ()) (Either (Error ())) ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Error () -> StateT (TyState ()) (Either (Error ())) ())
-> Error () -> StateT (TyState ()) (Either (Error ())) ()
forall a b. (a -> b) -> a -> b
$ () -> Name () -> Error ()
forall a. a -> Name a -> Error a
InvalidCImport () (TyName b -> Name ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void TyName b
n)
    let sig :: StackType ()
sig = StackType a -> StackType ()
forall a. StackType a -> StackType ()
voidStackType (StackType a -> StackType ()) -> StackType a -> StackType ()
forall a b. (a -> b) -> a -> b
$ Set (TyName a) -> [KempeTy a] -> [KempeTy a] -> StackType a
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType Set (TyName a)
forall a. Set a
S.empty [KempeTy a]
ins [KempeTy a]
os
    -- assign always comes after tyInsert
    KempeDecl () (StackType ()) (StackType ())
-> TypeM () (KempeDecl () (StackType ()) (StackType ()))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (KempeDecl () (StackType ()) (StackType ())
 -> TypeM () (KempeDecl () (StackType ()) (StackType ())))
-> KempeDecl () (StackType ()) (StackType ())
-> TypeM () (KempeDecl () (StackType ()) (StackType ()))
forall a b. (a -> b) -> a -> b
$ StackType ()
-> Name (StackType ())
-> [KempeTy ()]
-> [KempeTy ()]
-> ByteString
-> KempeDecl () (StackType ()) (StackType ())
forall a c b.
b
-> TyName b
-> [KempeTy a]
-> [KempeTy a]
-> ByteString
-> KempeDecl a c b
ExtFnDecl StackType ()
sig (TyName b
n TyName b -> StackType () -> Name (StackType ())
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> StackType ()
sig) (KempeTy a -> KempeTy ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (KempeTy a -> KempeTy ()) -> [KempeTy a] -> [KempeTy ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [KempeTy a]
ins) (KempeTy a -> KempeTy ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (KempeTy a -> KempeTy ()) -> [KempeTy a] -> [KempeTy ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [KempeTy a]
os) ByteString
cn
assignDecl (Export b
_ ABI
abi TyName b
n) = do
    ty :: StackType ()
ty@(StackType Set (Name ())
_ [KempeTy ()]
_ [KempeTy ()]
os) <- Name () -> TypeM () (StackType ())
forall a. Name a -> TypeM a (StackType a)
tyLookup (TyName b -> Name ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void TyName b
n)
    Bool
-> StateT (TyState ()) (Either (Error ())) ()
-> StateT (TyState ()) (Either (Error ())) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (ABI
abi ABI -> ABI -> Bool
forall a. Eq a => a -> a -> Bool
== ABI
Kabi Bool -> Bool -> Bool
|| [KempeTy ()] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [KempeTy ()]
os Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1) (StateT (TyState ()) (Either (Error ())) ()
 -> StateT (TyState ()) (Either (Error ())) ())
-> StateT (TyState ()) (Either (Error ())) ()
-> StateT (TyState ()) (Either (Error ())) ()
forall a b. (a -> b) -> a -> b
$
        Error () -> StateT (TyState ()) (Either (Error ())) ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Error () -> StateT (TyState ()) (Either (Error ())) ())
-> Error () -> StateT (TyState ()) (Either (Error ())) ()
forall a b. (a -> b) -> a -> b
$ () -> Name () -> Error ()
forall a. a -> Name a -> Error a
InvalidCExport () (TyName b -> Name ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void TyName b
n)
    StackType ()
-> ABI
-> Name (StackType ())
-> KempeDecl () (StackType ()) (StackType ())
forall a c b. b -> ABI -> TyName b -> KempeDecl a c b
Export StackType ()
ty ABI
abi (Name (StackType ()) -> KempeDecl () (StackType ()) (StackType ()))
-> StateT (TyState ()) (Either (Error ())) (Name (StackType ()))
-> TypeM () (KempeDecl () (StackType ()) (StackType ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyName b
-> StateT (TyState ()) (Either (Error ())) (Name (StackType ()))
forall a.
Name a
-> StateT (TyState ()) (Either (Error ())) (Name (StackType ()))
assignName TyName b
n

-- don't need to rename cuz it's only for exports (in theory)
assignName :: Name a -> TypeM () (Name (StackType ()))
assignName :: Name a
-> StateT (TyState ()) (Either (Error ())) (Name (StackType ()))
assignName Name a
n = do { StackType ()
ty <- Name () -> TypeM () (StackType ())
forall a. Name a -> TypeM a (StackType a)
tyLookup (Name a -> Name ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Name a
n) ; Name (StackType ())
-> StateT (TyState ()) (Either (Error ())) (Name (StackType ()))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name a
n Name a -> StackType () -> Name (StackType ())
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> StackType ()
ty) }

tyHeader :: KempeDecl a c b -> TypeM () ()
tyHeader :: KempeDecl a c b -> StateT (TyState ()) (Either (Error ())) ()
tyHeader Export{} = () -> StateT (TyState ()) (Either (Error ())) ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
tyHeader (FunDecl b
_ (Name Text
_ (Unique Int
i) b
_) [KempeTy a]
ins [KempeTy a]
out [Atom c b]
_) = do
    let sig :: StackType ()
sig = StackType a -> StackType ()
forall a. StackType a -> StackType ()
voidStackType (StackType a -> StackType ()) -> StackType a -> StackType ()
forall a b. (a -> b) -> a -> b
$ Set (Name a) -> [KempeTy a] -> [KempeTy a] -> StackType a
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType ([KempeTy a] -> Set (Name a)
forall a. [KempeTy a] -> Set (Name a)
freeVars ([KempeTy a]
ins [KempeTy a] -> [KempeTy a] -> [KempeTy a]
forall a. [a] -> [a] -> [a]
++ [KempeTy a]
out)) [KempeTy a]
ins [KempeTy a]
out
    ASetter
  (TyState ())
  (TyState ())
  (IntMap (StackType ()))
  (IntMap (StackType ()))
-> (IntMap (StackType ()) -> IntMap (StackType ()))
-> StateT (TyState ()) (Either (Error ())) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
modifying ASetter
  (TyState ())
  (TyState ())
  (IntMap (StackType ()))
  (IntMap (StackType ()))
forall a. Lens' (TyState a) (IntMap (StackType a))
tyEnvLens (Int
-> StackType () -> IntMap (StackType ()) -> IntMap (StackType ())
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
i StackType ()
sig)
tyHeader (ExtFnDecl b
_ n :: Name b
n@(Name Text
_ (Unique Int
i) b
_) [KempeTy a]
ins [KempeTy a]
os ByteString
_) = do
    Bool
-> StateT (TyState ()) (Either (Error ())) ()
-> StateT (TyState ()) (Either (Error ())) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([KempeTy a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [KempeTy a]
os Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1) (StateT (TyState ()) (Either (Error ())) ()
 -> StateT (TyState ()) (Either (Error ())) ())
-> StateT (TyState ()) (Either (Error ())) ()
-> StateT (TyState ()) (Either (Error ())) ()
forall a b. (a -> b) -> a -> b
$
        Error () -> StateT (TyState ()) (Either (Error ())) ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Error () -> StateT (TyState ()) (Either (Error ())) ())
-> Error () -> StateT (TyState ()) (Either (Error ())) ()
forall a b. (a -> b) -> a -> b
$ () -> Name () -> Error ()
forall a. a -> Name a -> Error a
InvalidCImport () (Name b -> Name ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Name b
n)
    Bool
-> StateT (TyState ()) (Either (Error ())) ()
-> StateT (TyState ()) (Either (Error ())) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set (Name a) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Set (Name a) -> Bool) -> Set (Name a) -> Bool
forall a b. (a -> b) -> a -> b
$ [KempeTy a] -> Set (Name a)
forall a. [KempeTy a] -> Set (Name a)
freeVars ([KempeTy a]
ins [KempeTy a] -> [KempeTy a] -> [KempeTy a]
forall a. [a] -> [a] -> [a]
++ [KempeTy a]
os)) (StateT (TyState ()) (Either (Error ())) ()
 -> StateT (TyState ()) (Either (Error ())) ())
-> StateT (TyState ()) (Either (Error ())) ()
-> StateT (TyState ()) (Either (Error ())) ()
forall a b. (a -> b) -> a -> b
$
        Error () -> StateT (TyState ()) (Either (Error ())) ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Error () -> StateT (TyState ()) (Either (Error ())) ())
-> Error () -> StateT (TyState ()) (Either (Error ())) ()
forall a b. (a -> b) -> a -> b
$ () -> Name () -> Error ()
forall a. a -> Name a -> Error a
TyVarExt () (Name b -> Name ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Name b
n)
    let sig :: StackType ()
sig = StackType a -> StackType ()
forall a. StackType a -> StackType ()
voidStackType (StackType a -> StackType ()) -> StackType a -> StackType ()
forall a b. (a -> b) -> a -> b
$ Set (Name a) -> [KempeTy a] -> [KempeTy a] -> StackType a
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType Set (Name a)
forall a. Set a
S.empty [KempeTy a]
ins [KempeTy a]
os -- no free variables allowed in c functions
    ASetter
  (TyState ())
  (TyState ())
  (IntMap (StackType ()))
  (IntMap (StackType ()))
-> (IntMap (StackType ()) -> IntMap (StackType ()))
-> StateT (TyState ()) (Either (Error ())) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
modifying ASetter
  (TyState ())
  (TyState ())
  (IntMap (StackType ()))
  (IntMap (StackType ()))
forall a. Lens' (TyState a) (IntMap (StackType a))
tyEnvLens (Int
-> StackType () -> IntMap (StackType ()) -> IntMap (StackType ())
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
i StackType ()
sig)
tyHeader TyDecl{} = () -> StateT (TyState ()) (Either (Error ())) ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

lessGeneral :: StackType a -> StackType a -> Bool
lessGeneral :: StackType a -> StackType a -> Bool
lessGeneral (StackType Set (Name a)
_ [KempeTy a]
is [KempeTy a]
os) (StackType Set (Name a)
_ [KempeTy a]
is' [KempeTy a]
os') = [KempeTy a] -> [KempeTy a] -> Bool
forall a. [KempeTy a] -> [KempeTy a] -> Bool
lessGenerals ([KempeTy a]
is [KempeTy a] -> [KempeTy a] -> [KempeTy a]
forall a. [a] -> [a] -> [a]
++ [KempeTy a]
os) ([KempeTy a]
is' [KempeTy a] -> [KempeTy a] -> [KempeTy a]
forall a. [a] -> [a] -> [a]
++ [KempeTy a]
os')
    where lessGeneralAtom :: KempeTy a -> KempeTy a -> Bool
          lessGeneralAtom :: KempeTy a -> KempeTy a -> Bool
lessGeneralAtom TyBuiltin{} TyVar{}                   = Bool
True
          lessGeneralAtom TyApp{} TyVar{}                       = Bool
True
          lessGeneralAtom (TyApp a
_ KempeTy a
ty KempeTy a
ty') (TyApp a
_ KempeTy a
ty'' KempeTy a
ty''') = KempeTy a -> KempeTy a -> Bool
forall a. KempeTy a -> KempeTy a -> Bool
lessGeneralAtom KempeTy a
ty KempeTy a
ty'' Bool -> Bool -> Bool
|| KempeTy a -> KempeTy a -> Bool
forall a. KempeTy a -> KempeTy a -> Bool
lessGeneralAtom KempeTy a
ty' KempeTy a
ty''' -- lazy pattern match?
          lessGeneralAtom KempeTy a
_ KempeTy a
_                                   = Bool
False
          lessGenerals :: [KempeTy a] -> [KempeTy a] -> Bool
          lessGenerals :: [KempeTy a] -> [KempeTy a] -> Bool
lessGenerals [] []               = Bool
False
          lessGenerals (KempeTy a
ty:[KempeTy a]
tys) (KempeTy a
ty':[KempeTy a]
tys') = KempeTy a -> KempeTy a -> Bool
forall a. KempeTy a -> KempeTy a -> Bool
lessGeneralAtom KempeTy a
ty KempeTy a
ty' Bool -> Bool -> Bool
|| [KempeTy a] -> [KempeTy a] -> Bool
forall a. [KempeTy a] -> [KempeTy a] -> Bool
lessGenerals [KempeTy a]
tys [KempeTy a]
tys'
          lessGenerals [KempeTy a]
_ []                = Bool
False -- shouldn't happen; will be caught later
          lessGenerals [] [KempeTy a]
_                = Bool
False

tyInsert :: KempeDecl a c b -> TypeM () ()
tyInsert :: KempeDecl a c b -> StateT (TyState ()) (Either (Error ())) ()
tyInsert (TyDecl a
_ TyName a
tn [TyName a]
ns [(TyName b, [KempeTy a])]
ls) = ((TyName b, [KempeTy a])
 -> StateT (TyState ()) (Either (Error ())) ())
-> [(TyName b, [KempeTy a])]
-> StateT (TyState ()) (Either (Error ())) ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (TyName a
-> Set (TyName a)
-> (TyName b, [KempeTy a])
-> StateT (TyState ()) (Either (Error ())) ()
forall b a.
Name b
-> Set (Name b)
-> (TyName a, [KempeTy b])
-> StateT (TyState ()) (Either (Error ())) ()
tyInsertLeaf TyName a
tn ([TyName a] -> Set (TyName a)
forall a. Ord a => [a] -> Set a
S.fromList [TyName a]
ns)) [(TyName b, [KempeTy a])]
ls
tyInsert (FunDecl b
_ TyName b
_ [KempeTy a]
ins [KempeTy a]
out [Atom c b]
as) = do
    (KempeTy () -> StateT (TyState ()) (Either (Error ())) Kind)
-> [KempeTy ()] -> StateT (TyState ()) (Either (Error ())) ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ KempeTy () -> StateT (TyState ()) (Either (Error ())) Kind
forall a. KempeTy a -> TypeM a Kind
kindOf (KempeTy a -> KempeTy ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (KempeTy a -> KempeTy ()) -> [KempeTy a] -> [KempeTy ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [KempeTy a]
ins [KempeTy a] -> [KempeTy a] -> [KempeTy a]
forall a. [a] -> [a] -> [a]
++ [KempeTy a]
out) -- FIXME: this gives sketchy results?
    StackType ()
sig <- StackType () -> TypeM () (StackType ())
forall a. StackType a -> TypeM a (StackType a)
renameStack (StackType () -> TypeM () (StackType ()))
-> StackType () -> TypeM () (StackType ())
forall a b. (a -> b) -> a -> b
$ StackType a -> StackType ()
forall a. StackType a -> StackType ()
voidStackType (StackType a -> StackType ()) -> StackType a -> StackType ()
forall a b. (a -> b) -> a -> b
$ Set (TyName a) -> [KempeTy a] -> [KempeTy a] -> StackType a
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType ([KempeTy a] -> Set (TyName a)
forall a. [KempeTy a] -> Set (Name a)
freeVars ([KempeTy a]
ins [KempeTy a] -> [KempeTy a] -> [KempeTy a]
forall a. [a] -> [a] -> [a]
++ [KempeTy a]
out)) [KempeTy a]
ins [KempeTy a]
out
    StackType ()
inferred <- [Atom c b] -> TypeM () (StackType ())
forall b a. [Atom b a] -> TypeM () (StackType ())
tyAtoms [Atom c b]
as
    StackType ()
_ <- StackType () -> StackType () -> TypeM () (StackType ())
mergeStackTypes StackType ()
sig StackType ()
inferred -- FIXME: need to verify the merged type is as general as the signature?
    Bool
-> StateT (TyState ()) (Either (Error ())) ()
-> StateT (TyState ()) (Either (Error ())) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (StackType ()
inferred StackType () -> StackType () -> Bool
forall a. StackType a -> StackType a -> Bool
`lessGeneral` StackType ()
sig) (StateT (TyState ()) (Either (Error ())) ()
 -> StateT (TyState ()) (Either (Error ())) ())
-> StateT (TyState ()) (Either (Error ())) ()
-> StateT (TyState ()) (Either (Error ())) ()
forall a b. (a -> b) -> a -> b
$
        Error () -> StateT (TyState ()) (Either (Error ())) ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Error () -> StateT (TyState ()) (Either (Error ())) ())
-> Error () -> StateT (TyState ()) (Either (Error ())) ()
forall a b. (a -> b) -> a -> b
$ () -> StackType () -> StackType () -> Error ()
forall a. a -> StackType a -> StackType a -> Error a
LessGeneral () StackType ()
sig StackType ()
inferred
tyInsert ExtFnDecl{} = () -> StateT (TyState ()) (Either (Error ())) ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure () -- TODO: kind-check
tyInsert Export{} = () -> StateT (TyState ()) (Either (Error ())) ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

tyModule :: Declarations a c b -> TypeM () ()
tyModule :: Declarations a c b -> StateT (TyState ()) (Either (Error ())) ()
tyModule Declarations a c b
m = (KempeDecl a c b -> StateT (TyState ()) (Either (Error ())) ())
-> Declarations a c b -> StateT (TyState ()) (Either (Error ())) ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ KempeDecl a c b -> StateT (TyState ()) (Either (Error ())) ()
forall a c b.
KempeDecl a c b -> StateT (TyState ()) (Either (Error ())) ()
tyHeader Declarations a c b
m StateT (TyState ()) (Either (Error ())) ()
-> StateT (TyState ()) (Either (Error ())) ()
-> StateT (TyState ()) (Either (Error ())) ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (KempeDecl a c b -> StateT (TyState ()) (Either (Error ())) ())
-> Declarations a c b -> StateT (TyState ()) (Either (Error ())) ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ KempeDecl a c b -> StateT (TyState ()) (Either (Error ())) ()
forall a c b.
KempeDecl a c b -> StateT (TyState ()) (Either (Error ())) ()
tyInsert Declarations a c b
m

checkModule :: Declarations a c b -> TypeM () ()
checkModule :: Declarations a c b -> StateT (TyState ()) (Either (Error ())) ()
checkModule Declarations a c b
m = Declarations a c b -> StateT (TyState ()) (Either (Error ())) ()
forall a c b.
Declarations a c b -> StateT (TyState ()) (Either (Error ())) ()
tyModule Declarations a c b
m StateT (TyState ()) (Either (Error ())) ()
-> TypeM () UnifyMap -> StateT (TyState ()) (Either (Error ())) ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* (Set (KempeTy (), KempeTy ()) -> TypeM () UnifyMap
unifyM (Set (KempeTy (), KempeTy ()) -> TypeM () UnifyMap)
-> StateT
     (TyState ()) (Either (Error ())) (Set (KempeTy (), KempeTy ()))
-> TypeM () UnifyMap
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (TyState () -> Set (KempeTy (), KempeTy ()))
-> StateT
     (TyState ()) (Either (Error ())) (Set (KempeTy (), KempeTy ()))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TyState () -> Set (KempeTy (), KempeTy ())
forall a. TyState a -> Set (KempeTy a, KempeTy a)
constraints)

assignModule :: Declarations a c b -> TypeM () (Declarations () (StackType ()) (StackType ()))
assignModule :: Declarations a c b
-> TypeM () (Declarations () (StackType ()) (StackType ()))
assignModule Declarations a c b
m = {-# SCC "assignModule" #-} do
    (KempeDecl a c b -> StateT (TyState ()) (Either (Error ())) ())
-> Declarations a c b -> StateT (TyState ()) (Either (Error ())) ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ KempeDecl a c b -> StateT (TyState ()) (Either (Error ())) ()
forall a c b.
KempeDecl a c b -> StateT (TyState ()) (Either (Error ())) ()
tyHeader Declarations a c b
m
    Declarations () (StackType ()) (StackType ())
m' <- (KempeDecl a c b
 -> TypeM () (KempeDecl () (StackType ()) (StackType ())))
-> Declarations a c b
-> TypeM () (Declarations () (StackType ()) (StackType ()))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse KempeDecl a c b
-> TypeM () (KempeDecl () (StackType ()) (StackType ()))
forall a c b.
KempeDecl a c b
-> TypeM () (KempeDecl () (StackType ()) (StackType ()))
assignDecl Declarations a c b
m
    UnifyMap
backNames <- Set (KempeTy (), KempeTy ()) -> TypeM () UnifyMap
unifyM (Set (KempeTy (), KempeTy ()) -> TypeM () UnifyMap)
-> StateT
     (TyState ()) (Either (Error ())) (Set (KempeTy (), KempeTy ()))
-> TypeM () UnifyMap
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (TyState () -> Set (KempeTy (), KempeTy ()))
-> StateT
     (TyState ()) (Either (Error ())) (Set (KempeTy (), KempeTy ()))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TyState () -> Set (KempeTy (), KempeTy ())
forall a. TyState a -> Set (KempeTy a, KempeTy a)
constraints
    Declarations () (StackType ()) (StackType ())
-> TypeM () (Declarations () (StackType ()) (StackType ()))
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((KempeDecl () (StackType ()) (StackType ())
 -> KempeDecl () (StackType ()) (StackType ()))
-> Declarations () (StackType ()) (StackType ())
-> Declarations () (StackType ()) (StackType ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((StackType () -> StackType ())
-> (StackType () -> StackType ())
-> KempeDecl () (StackType ()) (StackType ())
-> KempeDecl () (StackType ()) (StackType ())
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap ((StackType () -> StackType ())
 -> (StackType () -> StackType ())
 -> KempeDecl () (StackType ()) (StackType ())
 -> KempeDecl () (StackType ()) (StackType ()))
-> (StackType () -> StackType ())
-> KempeDecl () (StackType ()) (StackType ())
-> KempeDecl () (StackType ()) (StackType ())
forall (m :: * -> *) a. Monad m => m (m a) -> m a
.$ UnifyMap -> StackType () -> StackType ()
forall a. IntMap (KempeTy a) -> StackType a -> StackType a
substConstraintsStack UnifyMap
backNames) Declarations () (StackType ()) (StackType ())
m')

-- Make sure you don't have cycles in the renames map!
replaceUnique :: Unique -> TypeM a Unique
replaceUnique :: Unique -> TypeM a Unique
replaceUnique u :: Unique
u@(Unique Int
i) = do
    IntMap Int
rSt <- (TyState a -> IntMap Int)
-> StateT (TyState a) (Either (Error a)) (IntMap Int)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TyState a -> IntMap Int
forall a. TyState a -> IntMap Int
renames
    case Int -> IntMap Int -> Maybe Int
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
i IntMap Int
rSt of
        Maybe Int
Nothing -> Unique -> TypeM a Unique
forall (f :: * -> *) a. Applicative f => a -> f a
pure Unique
u
        Just Int
j  -> Unique -> TypeM a Unique
forall a. Unique -> TypeM a Unique
replaceUnique (Int -> Unique
Unique Int
j)

renameIn :: KempeTy a -> TypeM a (KempeTy a)
renameIn :: KempeTy a -> TypeM a (KempeTy a)
renameIn b :: KempeTy a
b@TyBuiltin{}    = KempeTy a -> TypeM a (KempeTy a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure KempeTy a
b
renameIn n :: KempeTy a
n@TyNamed{}      = KempeTy a -> TypeM a (KempeTy a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure KempeTy a
n
renameIn (TyApp a
l KempeTy a
ty KempeTy a
ty') = a -> KempeTy a -> KempeTy a -> KempeTy a
forall a. a -> KempeTy a -> KempeTy a -> KempeTy a
TyApp a
l (KempeTy a -> KempeTy a -> KempeTy a)
-> TypeM a (KempeTy a)
-> StateT (TyState a) (Either (Error a)) (KempeTy a -> KempeTy a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KempeTy a -> TypeM a (KempeTy a)
forall a. KempeTy a -> TypeM a (KempeTy a)
renameIn KempeTy a
ty StateT (TyState a) (Either (Error a)) (KempeTy a -> KempeTy a)
-> TypeM a (KempeTy a) -> TypeM a (KempeTy a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> KempeTy a -> TypeM a (KempeTy a)
forall a. KempeTy a -> TypeM a (KempeTy a)
renameIn KempeTy a
ty'
renameIn (TyVar a
l (Name Text
t Unique
u a
l')) = do
    Unique
u' <- Unique -> TypeM a Unique
forall a. Unique -> TypeM a Unique
replaceUnique Unique
u
    KempeTy a -> TypeM a (KempeTy a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (KempeTy a -> TypeM a (KempeTy a))
-> KempeTy a -> TypeM a (KempeTy a)
forall a b. (a -> b) -> a -> b
$ a -> Name a -> KempeTy a
forall a. a -> Name a -> KempeTy a
TyVar a
l (Text -> Unique -> a -> Name a
forall a. Text -> Unique -> a -> Name a
Name Text
t Unique
u' a
l')

-- has to use the max-iest maximum so we can't use withState
withTyState :: (TyState a -> TyState a) -> TypeM a x -> TypeM a x
withTyState :: (TyState a -> TyState a) -> TypeM a x -> TypeM a x
withTyState TyState a -> TyState a
modSt TypeM a x
act = do
    TyState a
preSt <- StateT (TyState a) (Either (Error a)) (TyState a)
forall s (m :: * -> *). MonadState s m => m s
get
    (TyState a -> TyState a)
-> StateT (TyState a) (Either (Error a)) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify TyState a -> TyState a
modSt
    x
res <- TypeM a x
act
    Int
postMax <- (TyState a -> Int) -> StateT (TyState a) (Either (Error a)) Int
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TyState a -> Int
forall a. TyState a -> Int
maxU
    TyState a -> StateT (TyState a) (Either (Error a)) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put TyState a
preSt
    (Int -> Identity Int) -> TyState a -> Identity (TyState a)
forall a. Lens' (TyState a) Int
maxULens ((Int -> Identity Int) -> TyState a -> Identity (TyState a))
-> Int -> StateT (TyState a) (Either (Error a)) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= Int
postMax
    x -> TypeM a x
forall (f :: * -> *) a. Applicative f => a -> f a
pure x
res

withName :: Name a -> TypeM a (Name a, TyState a -> TyState a)
withName :: Name a -> TypeM a (Name a, TyState a -> TyState a)
withName (Name Text
t (Unique Int
i) a
l) = do
    Int
m <- (TyState a -> Int) -> StateT (TyState a) (Either (Error a)) Int
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TyState a -> Int
forall a. TyState a -> Int
maxU
    let newUniq :: Int
newUniq = Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1
    (Int -> Identity Int) -> TyState a -> Identity (TyState a)
forall a. Lens' (TyState a) Int
maxULens ((Int -> Identity Int) -> TyState a -> Identity (TyState a))
-> Int -> StateT (TyState a) (Either (Error a)) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= Int
newUniq
    (Name a, TyState a -> TyState a)
-> TypeM a (Name a, TyState a -> TyState a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Text -> Unique -> a -> Name a
forall a. Text -> Unique -> a -> Name a
Name Text
t (Int -> Unique
Unique Int
newUniq) a
l, ASetter (TyState a) (TyState a) (IntMap Int) (IntMap Int)
-> (IntMap Int -> IntMap Int) -> TyState a -> TyState a
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter (TyState a) (TyState a) (IntMap Int) (IntMap Int)
forall a. Lens' (TyState a) (IntMap Int)
renamesLens (Int -> Int -> IntMap Int -> IntMap Int
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
i (Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)))

-- freshen the names in a stack so there aren't overlaps in quanitified variables
renameStack :: StackType a -> TypeM a (StackType a)
renameStack :: StackType a -> TypeM a (StackType a)
renameStack (StackType Set (Name a)
qs [KempeTy a]
ins [KempeTy a]
outs) = do
    [(Name a, TyState a -> TyState a)]
newQs <- (Name a
 -> StateT
      (TyState a) (Either (Error a)) (Name a, TyState a -> TyState a))
-> [Name a]
-> StateT
     (TyState a) (Either (Error a)) [(Name a, TyState a -> TyState a)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Name a
-> StateT
     (TyState a) (Either (Error a)) (Name a, TyState a -> TyState a)
forall a. Name a -> TypeM a (Name a, TyState a -> TyState a)
withName (Set (Name a) -> [Name a]
forall a. Set a -> [a]
S.toList Set (Name a)
qs)
    let ([Name a]
newNames, [TyState a -> TyState a]
localRenames) = [(Name a, TyState a -> TyState a)]
-> ([Name a], [TyState a -> TyState a])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Name a, TyState a -> TyState a)]
newQs
        newBinds :: TyState a -> TyState a
newBinds = [TyState a -> TyState a] -> TyState a -> TyState a
forall (t :: * -> *) a. Foldable t => t (a -> a) -> a -> a
thread [TyState a -> TyState a]
localRenames
    (TyState a -> TyState a)
-> TypeM a (StackType a) -> TypeM a (StackType a)
forall a x. (TyState a -> TyState a) -> TypeM a x -> TypeM a x
withTyState TyState a -> TyState a
newBinds (TypeM a (StackType a) -> TypeM a (StackType a))
-> TypeM a (StackType a) -> TypeM a (StackType a)
forall a b. (a -> b) -> a -> b
$
        Set (Name a) -> [KempeTy a] -> [KempeTy a] -> StackType a
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType ([Name a] -> Set (Name a)
forall a. Ord a => [a] -> Set a
S.fromList [Name a]
newNames) ([KempeTy a] -> [KempeTy a] -> StackType a)
-> StateT (TyState a) (Either (Error a)) [KempeTy a]
-> StateT
     (TyState a) (Either (Error a)) ([KempeTy a] -> StackType a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (KempeTy a -> StateT (TyState a) (Either (Error a)) (KempeTy a))
-> [KempeTy a] -> StateT (TyState a) (Either (Error a)) [KempeTy a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse KempeTy a -> StateT (TyState a) (Either (Error a)) (KempeTy a)
forall a. KempeTy a -> TypeM a (KempeTy a)
renameIn [KempeTy a]
ins StateT (TyState a) (Either (Error a)) ([KempeTy a] -> StackType a)
-> StateT (TyState a) (Either (Error a)) [KempeTy a]
-> TypeM a (StackType a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (KempeTy a -> StateT (TyState a) (Either (Error a)) (KempeTy a))
-> [KempeTy a] -> StateT (TyState a) (Either (Error a)) [KempeTy a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse KempeTy a -> StateT (TyState a) (Either (Error a)) (KempeTy a)
forall a. KempeTy a -> TypeM a (KempeTy a)
renameIn [KempeTy a]
outs

mergeStackTypes :: StackType () -> StackType () -> TypeM () (StackType ())
mergeStackTypes :: StackType () -> StackType () -> TypeM () (StackType ())
mergeStackTypes st0 :: StackType ()
st0@(StackType Set (Name ())
_ [KempeTy ()]
i0 [KempeTy ()]
o0) st1 :: StackType ()
st1@(StackType Set (Name ())
_ [KempeTy ()]
i1 [KempeTy ()]
o1) = do
    let li0 :: Int
li0 = [KempeTy ()] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [KempeTy ()]
i0
        li1 :: Int
li1 = [KempeTy ()] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [KempeTy ()]
i1
        toExpand :: Int
toExpand = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max (Int -> Int
forall a. Num a => a -> a
abs (Int
li0 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
li1)) (Int -> Int
forall a. Num a => a -> a
abs ([KempeTy ()] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [KempeTy ()]
o0 Int -> Int -> Int
forall a. Num a => a -> a -> a
- [KempeTy ()] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [KempeTy ()]
o1))

    (StackType Set (Name ())
q [KempeTy ()]
ins [KempeTy ()]
os) <- (if Int
li0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
li1 then Int -> StackType () -> TypeM () (StackType ())
expandType Int
toExpand else StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure) StackType ()
st0
    (StackType Set (Name ())
q' [KempeTy ()]
ins' [KempeTy ()]
os') <- (if Int
li1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
li0 then Int -> StackType () -> TypeM () (StackType ())
expandType Int
toExpand else StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure) StackType ()
st1

    Bool
-> StateT (TyState ()) (Either (Error ())) ()
-> StateT (TyState ()) (Either (Error ())) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (([KempeTy ()] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [KempeTy ()]
ins Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [KempeTy ()] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [KempeTy ()]
ins') Bool -> Bool -> Bool
|| ([KempeTy ()] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [KempeTy ()]
os Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [KempeTy ()] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [KempeTy ()]
os')) (StateT (TyState ()) (Either (Error ())) ()
 -> StateT (TyState ()) (Either (Error ())) ())
-> StateT (TyState ()) (Either (Error ())) ()
-> StateT (TyState ()) (Either (Error ())) ()
forall a b. (a -> b) -> a -> b
$
        Error () -> StateT (TyState ()) (Either (Error ())) ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Error () -> StateT (TyState ()) (Either (Error ())) ())
-> Error () -> StateT (TyState ()) (Either (Error ())) ()
forall a b. (a -> b) -> a -> b
$ () -> StackType () -> StackType () -> Error ()
forall a. a -> StackType a -> StackType a -> Error a
MismatchedLengths () StackType ()
st0 StackType ()
st1

    (KempeTy ()
 -> KempeTy () -> StateT (TyState ()) (Either (Error ())) ())
-> [KempeTy ()]
-> [KempeTy ()]
-> StateT (TyState ()) (Either (Error ())) ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ KempeTy ()
-> KempeTy () -> StateT (TyState ()) (Either (Error ())) ()
forall a. Ord a => KempeTy a -> KempeTy a -> TypeM a ()
pushConstraint [KempeTy ()]
ins [KempeTy ()]
ins'
    (KempeTy ()
 -> KempeTy () -> StateT (TyState ()) (Either (Error ())) ())
-> [KempeTy ()]
-> [KempeTy ()]
-> StateT (TyState ()) (Either (Error ())) ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ KempeTy ()
-> KempeTy () -> StateT (TyState ()) (Either (Error ())) ()
forall a. Ord a => KempeTy a -> KempeTy a -> TypeM a ()
pushConstraint [KempeTy ()]
os [KempeTy ()]
os'

    StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StackType () -> TypeM () (StackType ()))
-> StackType () -> TypeM () (StackType ())
forall a b. (a -> b) -> a -> b
$ Set (Name ()) -> [KempeTy ()] -> [KempeTy ()] -> StackType ()
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType (Set (Name ())
q Set (Name ()) -> Set (Name ()) -> Set (Name ())
forall a. Semigroup a => a -> a -> a
<> Set (Name ())
q') [KempeTy ()]
ins [KempeTy ()]
os

tyPattern :: Pattern b a -> TypeM () (StackType ())
tyPattern :: Pattern b a -> TypeM () (StackType ())
tyPattern PatternWildcard{} = do
    Name ()
aN <- Text -> TypeM () (Name ())
dummyName Text
"a"
    StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StackType () -> TypeM () (StackType ()))
-> StackType () -> TypeM () (StackType ())
forall a b. (a -> b) -> a -> b
$ Set (Name ()) -> [KempeTy ()] -> [KempeTy ()] -> StackType ()
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType (Name () -> Set (Name ())
forall a. a -> Set a
S.singleton Name ()
aN) [() -> Name () -> KempeTy ()
forall a. a -> Name a -> KempeTy a
TyVar () Name ()
aN] []
tyPattern PatternInt{} = StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StackType () -> TypeM () (StackType ()))
-> StackType () -> TypeM () (StackType ())
forall a b. (a -> b) -> a -> b
$ Set (Name ()) -> [KempeTy ()] -> [KempeTy ()] -> StackType ()
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType Set (Name ())
forall a. Set a
S.empty [() -> BuiltinTy -> KempeTy ()
forall a. a -> BuiltinTy -> KempeTy a
TyBuiltin () BuiltinTy
TyInt] []
tyPattern PatternBool{} = StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StackType () -> TypeM () (StackType ()))
-> StackType () -> TypeM () (StackType ())
forall a b. (a -> b) -> a -> b
$ Set (Name ()) -> [KempeTy ()] -> [KempeTy ()] -> StackType ()
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType Set (Name ())
forall a. Set a
S.empty [() -> BuiltinTy -> KempeTy ()
forall a. a -> BuiltinTy -> KempeTy a
TyBuiltin () BuiltinTy
TyBool] []
tyPattern (PatternCons b
_ TyName b
tn) = StackType () -> TypeM () (StackType ())
forall a. StackType a -> TypeM a (StackType a)
renameStack (StackType () -> TypeM () (StackType ()))
-> TypeM () (StackType ()) -> TypeM () (StackType ())
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (StackType () -> StackType ()
flipStackType (StackType () -> StackType ())
-> TypeM () (StackType ()) -> TypeM () (StackType ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name () -> TypeM () (StackType ())
forall a. Name a -> TypeM a (StackType a)
consLookup (TyName b -> Name ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void TyName b
tn))

assignPattern :: Pattern b a -> TypeM () (StackType (), Pattern (StackType ()) (StackType ()))
assignPattern :: Pattern b a
-> TypeM () (StackType (), Pattern (StackType ()) (StackType ()))
assignPattern (PatternInt a
_ Integer
i) =
    let sTy :: StackType ()
sTy = Set (Name ()) -> [KempeTy ()] -> [KempeTy ()] -> StackType ()
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType Set (Name ())
forall a. Set a
S.empty [() -> BuiltinTy -> KempeTy ()
forall a. a -> BuiltinTy -> KempeTy a
TyBuiltin () BuiltinTy
TyInt] []
        in (StackType (), Pattern (StackType ()) (StackType ()))
-> TypeM () (StackType (), Pattern (StackType ()) (StackType ()))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StackType ()
sTy, StackType () -> Integer -> Pattern (StackType ()) (StackType ())
forall c b. b -> Integer -> Pattern c b
PatternInt StackType ()
sTy Integer
i)
assignPattern (PatternBool a
_ Bool
i) =
    let sTy :: StackType ()
sTy = Set (Name ()) -> [KempeTy ()] -> [KempeTy ()] -> StackType ()
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType Set (Name ())
forall a. Set a
S.empty [() -> BuiltinTy -> KempeTy ()
forall a. a -> BuiltinTy -> KempeTy a
TyBuiltin () BuiltinTy
TyBool] []
        in (StackType (), Pattern (StackType ()) (StackType ()))
-> TypeM () (StackType (), Pattern (StackType ()) (StackType ()))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StackType ()
sTy, StackType () -> Bool -> Pattern (StackType ()) (StackType ())
forall c b. b -> Bool -> Pattern c b
PatternBool StackType ()
sTy Bool
i)
assignPattern (PatternCons b
_ TyName b
tn) = do { StackType ()
ty <- StackType () -> TypeM () (StackType ())
forall a. StackType a -> TypeM a (StackType a)
renameStack (StackType () -> TypeM () (StackType ()))
-> TypeM () (StackType ()) -> TypeM () (StackType ())
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (StackType () -> StackType ()
flipStackType (StackType () -> StackType ())
-> TypeM () (StackType ()) -> TypeM () (StackType ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name () -> TypeM () (StackType ())
forall a. Name a -> TypeM a (StackType a)
consLookup (TyName b -> Name ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void TyName b
tn)) ; (StackType (), Pattern (StackType ()) (StackType ()))
-> TypeM () (StackType (), Pattern (StackType ()) (StackType ()))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StackType ()
ty, StackType ()
-> Name (StackType ()) -> Pattern (StackType ()) (StackType ())
forall c b. c -> TyName c -> Pattern c b
PatternCons StackType ()
ty (TyName b
tn TyName b -> StackType () -> Name (StackType ())
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> StackType ()
ty)) }
assignPattern PatternWildcard{} = do
    Name ()
aN <- Text -> TypeM () (Name ())
dummyName Text
"a"
    let resType :: StackType ()
resType = Set (Name ()) -> [KempeTy ()] -> [KempeTy ()] -> StackType ()
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType (Name () -> Set (Name ())
forall a. a -> Set a
S.singleton Name ()
aN) [() -> Name () -> KempeTy ()
forall a. a -> Name a -> KempeTy a
TyVar () Name ()
aN] []
    (StackType (), Pattern (StackType ()) (StackType ()))
-> TypeM () (StackType (), Pattern (StackType ()) (StackType ()))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StackType ()
resType, StackType () -> Pattern (StackType ()) (StackType ())
forall c b. b -> Pattern c b
PatternWildcard StackType ()
resType)

mergeMany :: NonEmpty (StackType ()) -> TypeM () (StackType ())
mergeMany :: NonEmpty (StackType ()) -> TypeM () (StackType ())
mergeMany (StackType ()
t :| [StackType ()]
ts) = (StackType () -> StackType () -> TypeM () (StackType ()))
-> StackType () -> [StackType ()] -> TypeM () (StackType ())
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM StackType () -> StackType () -> TypeM () (StackType ())
mergeStackTypes StackType ()
t [StackType ()]
ts

-- assumes they have been renamed...
pushConstraint :: Ord a => KempeTy a -> KempeTy a -> TypeM a ()
pushConstraint :: KempeTy a -> KempeTy a -> TypeM a ()
pushConstraint KempeTy a
ty KempeTy a
ty' =
    ASetter
  (TyState a)
  (TyState a)
  (Set (KempeTy a, KempeTy a))
  (Set (KempeTy a, KempeTy a))
-> (Set (KempeTy a, KempeTy a) -> Set (KempeTy a, KempeTy a))
-> TypeM a ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
modifying ASetter
  (TyState a)
  (TyState a)
  (Set (KempeTy a, KempeTy a))
  (Set (KempeTy a, KempeTy a))
forall a. Lens' (TyState a) (Set (KempeTy a, KempeTy a))
constraintsLens ((KempeTy a, KempeTy a)
-> Set (KempeTy a, KempeTy a) -> Set (KempeTy a, KempeTy a)
forall a. Ord a => a -> Set a -> Set a
S.insert (KempeTy a
ty, KempeTy a
ty'))

expandType :: Int -> StackType () -> TypeM () (StackType ())
expandType :: Int -> StackType () -> TypeM () (StackType ())
expandType Int
n (StackType Set (Name ())
q [KempeTy ()]
i [KempeTy ()]
o) = do
    [Name ()]
newVars <- Int
-> TypeM () (Name ())
-> StateT (TyState ()) (Either (Error ())) [Name ()]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
n (Text -> TypeM () (Name ())
dummyName Text
"a")
    let newTy :: [KempeTy ()]
newTy = () -> Name () -> KempeTy ()
forall a. a -> Name a -> KempeTy a
TyVar () (Name () -> KempeTy ()) -> [Name ()] -> [KempeTy ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Name ()]
newVars
    StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StackType () -> TypeM () (StackType ()))
-> StackType () -> TypeM () (StackType ())
forall a b. (a -> b) -> a -> b
$ Set (Name ()) -> [KempeTy ()] -> [KempeTy ()] -> StackType ()
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType (Set (Name ())
q Set (Name ()) -> Set (Name ()) -> Set (Name ())
forall a. Semigroup a => a -> a -> a
<> [Name ()] -> Set (Name ())
forall a. Ord a => [a] -> Set a
S.fromList [Name ()]
newVars) ([KempeTy ()]
newTy [KempeTy ()] -> [KempeTy ()] -> [KempeTy ()]
forall a. [a] -> [a] -> [a]
++ [KempeTy ()]
i) ([KempeTy ()]
newTy [KempeTy ()] -> [KempeTy ()] -> [KempeTy ()]
forall a. [a] -> [a] -> [a]
++ [KempeTy ()]
o)

substConstraints :: IM.IntMap (KempeTy a) -> KempeTy a -> KempeTy a
substConstraints :: IntMap (KempeTy a) -> KempeTy a -> KempeTy a
substConstraints IntMap (KempeTy a)
_ ty :: KempeTy a
ty@TyNamed{}                         = KempeTy a
ty
substConstraints IntMap (KempeTy a)
_ ty :: KempeTy a
ty@TyBuiltin{}                       = KempeTy a
ty
substConstraints IntMap (KempeTy a)
tys ty :: KempeTy a
ty@(TyVar a
_ (Name Text
_ (Unique Int
k) a
_)) =
    case Int -> IntMap (KempeTy a) -> Maybe (KempeTy a)
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
k IntMap (KempeTy a)
tys of
        Just ty' :: KempeTy a
ty'@TyVar{} -> IntMap (KempeTy a) -> KempeTy a -> KempeTy a
forall a. IntMap (KempeTy a) -> KempeTy a -> KempeTy a
substConstraints (Int -> IntMap (KempeTy a) -> IntMap (KempeTy a)
forall a. Int -> IntMap a -> IntMap a
IM.delete Int
k IntMap (KempeTy a)
tys) KempeTy a
ty' -- TODO: this is to prevent cyclic lookups: is it right?
        Just KempeTy a
ty'         -> KempeTy a
ty'
        Maybe (KempeTy a)
Nothing          -> KempeTy a
ty
substConstraints IntMap (KempeTy a)
tys (TyApp a
l KempeTy a
ty KempeTy a
ty')                   =
    a -> KempeTy a -> KempeTy a -> KempeTy a
forall a. a -> KempeTy a -> KempeTy a -> KempeTy a
TyApp a
l (IntMap (KempeTy a) -> KempeTy a -> KempeTy a
forall a. IntMap (KempeTy a) -> KempeTy a -> KempeTy a
substConstraints IntMap (KempeTy a)
tys KempeTy a
ty) (IntMap (KempeTy a) -> KempeTy a -> KempeTy a
forall a. IntMap (KempeTy a) -> KempeTy a -> KempeTy a
substConstraints IntMap (KempeTy a)
tys KempeTy a
ty')

substConstraintsStack :: IM.IntMap (KempeTy a) -> StackType a -> StackType a
substConstraintsStack :: IntMap (KempeTy a) -> StackType a -> StackType a
substConstraintsStack IntMap (KempeTy a)
tys (StackType Set (Name a)
_ [KempeTy a]
is [KempeTy a]
os) = {-# SCC "substConstraintsStack" #-}
    let is' :: [KempeTy a]
is' = IntMap (KempeTy a) -> KempeTy a -> KempeTy a
forall a. IntMap (KempeTy a) -> KempeTy a -> KempeTy a
substConstraints IntMap (KempeTy a)
tys (KempeTy a -> KempeTy a) -> [KempeTy a] -> [KempeTy a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [KempeTy a]
is
        os' :: [KempeTy a]
os' = IntMap (KempeTy a) -> KempeTy a -> KempeTy a
forall a. IntMap (KempeTy a) -> KempeTy a -> KempeTy a
substConstraints IntMap (KempeTy a)
tys (KempeTy a -> KempeTy a) -> [KempeTy a] -> [KempeTy a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [KempeTy a]
os
        in Set (Name a) -> [KempeTy a] -> [KempeTy a] -> StackType a
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType ([KempeTy a] -> Set (Name a)
forall a. [KempeTy a] -> Set (Name a)
freeVars ([KempeTy a]
is' [KempeTy a] -> [KempeTy a] -> [KempeTy a]
forall a. [a] -> [a] -> [a]
++ [KempeTy a]
os')) [KempeTy a]
is' [KempeTy a]
os'

-- do renaming before this
-- | Given @x@ and @y@, return the 'StackType' of @x y@
catTypes :: StackType () -- ^ @x@
         -> StackType () -- ^ @y@
         -> TypeM () (StackType ())
catTypes :: StackType () -> StackType () -> TypeM () (StackType ())
catTypes st0 :: StackType ()
st0@(StackType Set (Name ())
_ [KempeTy ()]
_ [KempeTy ()]
osX) (StackType Set (Name ())
q1 [KempeTy ()]
insY [KempeTy ()]
osY) = do
    let lY :: Int
lY = [KempeTy ()] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [KempeTy ()]
insY
        lDiff :: Int
lDiff = Int
lY Int -> Int -> Int
forall a. Num a => a -> a -> a
- [KempeTy ()] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [KempeTy ()]
osX

    -- all of the "ins" of y have to come from x, so we expand x as needed
    (StackType Set (Name ())
q0 [KempeTy ()]
insX [KempeTy ()]
osX') <- if Int
lDiff Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0
        then Int -> StackType () -> TypeM () (StackType ())
expandType Int
lDiff StackType ()
st0
        else StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure StackType ()
st0

    -- zip the last (length insY) of osX' with insY
    (KempeTy ()
 -> KempeTy () -> StateT (TyState ()) (Either (Error ())) ())
-> [KempeTy ()]
-> [KempeTy ()]
-> StateT (TyState ()) (Either (Error ())) ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ KempeTy ()
-> KempeTy () -> StateT (TyState ()) (Either (Error ())) ()
forall a. Ord a => KempeTy a -> KempeTy a -> TypeM a ()
pushConstraint (Int -> [KempeTy ()] -> [KempeTy ()]
forall a. Int -> [a] -> [a]
drop ([KempeTy ()] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [KempeTy ()]
osX' Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
lY) [KempeTy ()]
osX') [KempeTy ()]
insY -- TODO splitAt

    StackType () -> TypeM () (StackType ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StackType () -> TypeM () (StackType ()))
-> StackType () -> TypeM () (StackType ())
forall a b. (a -> b) -> a -> b
$ Set (Name ()) -> [KempeTy ()] -> [KempeTy ()] -> StackType ()
forall b. Set (Name b) -> [KempeTy b] -> [KempeTy b] -> StackType b
StackType (Set (Name ())
q0 Set (Name ()) -> Set (Name ()) -> Set (Name ())
forall a. Semigroup a => a -> a -> a
<> Set (Name ())
q1) [KempeTy ()]
insX (Int -> [KempeTy ()] -> [KempeTy ()]
forall a. Int -> [a] -> [a]
take ([KempeTy ()] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [KempeTy ()]
osX' Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
lY) [KempeTy ()]
osX' [KempeTy ()] -> [KempeTy ()] -> [KempeTy ()]
forall a. [a] -> [a] -> [a]
++ [KempeTy ()]
osY)