{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TemplateHaskell #-}
module Disco.Typecheck.Solve where
import Unbound.Generics.LocallyNameless (Alpha, Name, Subst, fv,
name2Integer, string2Name,
substs)
import Data.Coerce
import GHC.Generics (Generic)
import Control.Arrow ((&&&), (***))
import Control.Lens hiding (use, (%=), (.=))
import Control.Monad (unless, zipWithM)
import Data.Bifunctor (first, second)
import Data.Either (partitionEithers)
import Data.List (find, foldl', intersect,
partition)
import Data.Map (Map, (!))
import qualified Data.Map as M
import Data.Maybe (fromJust, fromMaybe,
mapMaybe)
import Data.Monoid (First (..))
import Data.Set (Set)
import qualified Data.Set as S
import Data.Tuple
import Disco.Effects.Fresh
import Disco.Effects.State
import Polysemy
import Polysemy.Error
import Polysemy.Input
import Polysemy.Output
import Disco.Messages
import Disco.Pretty hiding ((<>))
import Disco.Subst
import qualified Disco.Subst as Subst
import Disco.Typecheck.Constraints
import Disco.Typecheck.Graph (Graph)
import qualified Disco.Typecheck.Graph as G
import Disco.Typecheck.Unify
import Disco.Types
import Disco.Types.Qualifiers
import Disco.Types.Rules
data SolveError where
NoWeakUnifier :: SolveError
NoUnify :: SolveError
UnqualBase :: Qualifier -> BaseTy -> SolveError
Unqual :: Qualifier -> Type -> SolveError
QualSkolem :: Qualifier -> Name Type -> SolveError
deriving Int -> SolveError -> ShowS
[SolveError] -> ShowS
SolveError -> String
(Int -> SolveError -> ShowS)
-> (SolveError -> String)
-> ([SolveError] -> ShowS)
-> Show SolveError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SolveError] -> ShowS
$cshowList :: [SolveError] -> ShowS
show :: SolveError -> String
$cshow :: SolveError -> String
showsPrec :: Int -> SolveError -> ShowS
$cshowsPrec :: Int -> SolveError -> ShowS
Show
instance Semigroup SolveError where
SolveError
e <> :: SolveError -> SolveError -> SolveError
<> SolveError
_ = SolveError
e
runSolve :: Sem (Fresh ': Error SolveError ': r) a -> Sem r (Either SolveError a)
runSolve :: Sem (Fresh : Error SolveError : r) a -> Sem r (Either SolveError a)
runSolve = Sem (Error SolveError : r) a -> Sem r (Either SolveError a)
forall e (r :: [(* -> *) -> * -> *]) a.
Sem (Error e : r) a -> Sem r (Either e a)
runError (Sem (Error SolveError : r) a -> Sem r (Either SolveError a))
-> (Sem (Fresh : Error SolveError : r) a
-> Sem (Error SolveError : r) a)
-> Sem (Fresh : Error SolveError : r) a
-> Sem r (Either SolveError a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem (Fresh : Error SolveError : r) a
-> Sem (Error SolveError : r) a
forall (r :: [(* -> *) -> * -> *]) a. Sem (Fresh : r) a -> Sem r a
runFresh
filterErrors :: Member (Error e) r => [Sem r a] -> Sem r [a]
filterErrors :: [Sem r a] -> Sem r [a]
filterErrors [Sem r a]
ms = do
[Either e a]
es <- (Sem r a -> Sem r (Either e a)) -> [Sem r a] -> Sem r [Either e a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Sem r a -> Sem r (Either e a)
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
Sem r a -> Sem r (Either e a)
try [Sem r a]
ms
case [Either e a] -> ([e], [a])
forall a b. [Either a b] -> ([a], [b])
partitionEithers [Either e a]
es of
(e
e:[e]
_, []) -> e -> Sem r [a]
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw e
e
([e]
_, [a]
as) -> [a] -> Sem r [a]
forall (m :: * -> *) a. Monad m => a -> m a
return [a]
as
asum' :: Member (Error e) r => [Sem r a] -> Sem r a
asum' :: [Sem r a] -> Sem r a
asum' [] = String -> Sem r a
forall a. HasCallStack => String -> a
error String
"Impossible: asum' []"
asum' [Sem r a
m] = Sem r a
m
asum' (Sem r a
m:[Sem r a]
ms) = Sem r a
m Sem r a -> (e -> Sem r a) -> Sem r a
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
Sem r a -> (e -> Sem r a) -> Sem r a
`catch` (\e
_ -> [Sem r a] -> Sem r a
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
[Sem r a] -> Sem r a
asum' [Sem r a]
ms)
data SimpleConstraint where
(:<:) :: Type -> Type -> SimpleConstraint
(:=:) :: Type -> Type -> SimpleConstraint
deriving (Int -> SimpleConstraint -> ShowS
[SimpleConstraint] -> ShowS
SimpleConstraint -> String
(Int -> SimpleConstraint -> ShowS)
-> (SimpleConstraint -> String)
-> ([SimpleConstraint] -> ShowS)
-> Show SimpleConstraint
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SimpleConstraint] -> ShowS
$cshowList :: [SimpleConstraint] -> ShowS
show :: SimpleConstraint -> String
$cshow :: SimpleConstraint -> String
showsPrec :: Int -> SimpleConstraint -> ShowS
$cshowsPrec :: Int -> SimpleConstraint -> ShowS
Show, SimpleConstraint -> SimpleConstraint -> Bool
(SimpleConstraint -> SimpleConstraint -> Bool)
-> (SimpleConstraint -> SimpleConstraint -> Bool)
-> Eq SimpleConstraint
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SimpleConstraint -> SimpleConstraint -> Bool
$c/= :: SimpleConstraint -> SimpleConstraint -> Bool
== :: SimpleConstraint -> SimpleConstraint -> Bool
$c== :: SimpleConstraint -> SimpleConstraint -> Bool
Eq, Eq SimpleConstraint
Eq SimpleConstraint
-> (SimpleConstraint -> SimpleConstraint -> Ordering)
-> (SimpleConstraint -> SimpleConstraint -> Bool)
-> (SimpleConstraint -> SimpleConstraint -> Bool)
-> (SimpleConstraint -> SimpleConstraint -> Bool)
-> (SimpleConstraint -> SimpleConstraint -> Bool)
-> (SimpleConstraint -> SimpleConstraint -> SimpleConstraint)
-> (SimpleConstraint -> SimpleConstraint -> SimpleConstraint)
-> Ord SimpleConstraint
SimpleConstraint -> SimpleConstraint -> Bool
SimpleConstraint -> SimpleConstraint -> Ordering
SimpleConstraint -> SimpleConstraint -> SimpleConstraint
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: SimpleConstraint -> SimpleConstraint -> SimpleConstraint
$cmin :: SimpleConstraint -> SimpleConstraint -> SimpleConstraint
max :: SimpleConstraint -> SimpleConstraint -> SimpleConstraint
$cmax :: SimpleConstraint -> SimpleConstraint -> SimpleConstraint
>= :: SimpleConstraint -> SimpleConstraint -> Bool
$c>= :: SimpleConstraint -> SimpleConstraint -> Bool
> :: SimpleConstraint -> SimpleConstraint -> Bool
$c> :: SimpleConstraint -> SimpleConstraint -> Bool
<= :: SimpleConstraint -> SimpleConstraint -> Bool
$c<= :: SimpleConstraint -> SimpleConstraint -> Bool
< :: SimpleConstraint -> SimpleConstraint -> Bool
$c< :: SimpleConstraint -> SimpleConstraint -> Bool
compare :: SimpleConstraint -> SimpleConstraint -> Ordering
$ccompare :: SimpleConstraint -> SimpleConstraint -> Ordering
$cp1Ord :: Eq SimpleConstraint
Ord, (forall x. SimpleConstraint -> Rep SimpleConstraint x)
-> (forall x. Rep SimpleConstraint x -> SimpleConstraint)
-> Generic SimpleConstraint
forall x. Rep SimpleConstraint x -> SimpleConstraint
forall x. SimpleConstraint -> Rep SimpleConstraint x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep SimpleConstraint x -> SimpleConstraint
$cfrom :: forall x. SimpleConstraint -> Rep SimpleConstraint x
Generic, Show SimpleConstraint
Show SimpleConstraint
-> (AlphaCtx -> SimpleConstraint -> SimpleConstraint -> Bool)
-> (forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx
-> (AnyName -> f AnyName)
-> SimpleConstraint
-> f SimpleConstraint)
-> (AlphaCtx
-> NamePatFind -> SimpleConstraint -> SimpleConstraint)
-> (AlphaCtx -> NthPatFind -> SimpleConstraint -> SimpleConstraint)
-> (SimpleConstraint -> DisjointSet AnyName)
-> (SimpleConstraint -> All)
-> (SimpleConstraint -> Bool)
-> (SimpleConstraint -> NthPatFind)
-> (SimpleConstraint -> NamePatFind)
-> (AlphaCtx
-> Perm AnyName -> SimpleConstraint -> SimpleConstraint)
-> (forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> SimpleConstraint
-> (SimpleConstraint -> Perm AnyName -> m b)
-> m b)
-> (forall (m :: * -> *).
Fresh m =>
AlphaCtx -> SimpleConstraint -> m (SimpleConstraint, Perm AnyName))
-> (AlphaCtx -> SimpleConstraint -> SimpleConstraint -> Ordering)
-> Alpha SimpleConstraint
AlphaCtx -> NthPatFind -> SimpleConstraint -> SimpleConstraint
AlphaCtx -> NamePatFind -> SimpleConstraint -> SimpleConstraint
AlphaCtx -> Perm AnyName -> SimpleConstraint -> SimpleConstraint
AlphaCtx -> SimpleConstraint -> SimpleConstraint -> Bool
AlphaCtx -> SimpleConstraint -> SimpleConstraint -> Ordering
SimpleConstraint -> Bool
SimpleConstraint -> All
SimpleConstraint -> DisjointSet AnyName
SimpleConstraint -> NthPatFind
SimpleConstraint -> NamePatFind
forall a.
Show a
-> (AlphaCtx -> a -> a -> Bool)
-> (forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> a -> f a)
-> (AlphaCtx -> NamePatFind -> a -> a)
-> (AlphaCtx -> NthPatFind -> a -> a)
-> (a -> DisjointSet AnyName)
-> (a -> All)
-> (a -> Bool)
-> (a -> NthPatFind)
-> (a -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> a -> a)
-> (forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
Fresh m =>
AlphaCtx -> a -> m (a, Perm AnyName))
-> (AlphaCtx -> a -> a -> Ordering)
-> Alpha a
forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx
-> (AnyName -> f AnyName) -> SimpleConstraint -> f SimpleConstraint
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> SimpleConstraint -> m (SimpleConstraint, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> SimpleConstraint
-> (SimpleConstraint -> Perm AnyName -> m b)
-> m b
acompare' :: AlphaCtx -> SimpleConstraint -> SimpleConstraint -> Ordering
$cacompare' :: AlphaCtx -> SimpleConstraint -> SimpleConstraint -> Ordering
freshen' :: AlphaCtx -> SimpleConstraint -> m (SimpleConstraint, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> SimpleConstraint -> m (SimpleConstraint, Perm AnyName)
lfreshen' :: AlphaCtx
-> SimpleConstraint
-> (SimpleConstraint -> Perm AnyName -> m b)
-> m b
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> SimpleConstraint
-> (SimpleConstraint -> Perm AnyName -> m b)
-> m b
swaps' :: AlphaCtx -> Perm AnyName -> SimpleConstraint -> SimpleConstraint
$cswaps' :: AlphaCtx -> Perm AnyName -> SimpleConstraint -> SimpleConstraint
namePatFind :: SimpleConstraint -> NamePatFind
$cnamePatFind :: SimpleConstraint -> NamePatFind
nthPatFind :: SimpleConstraint -> NthPatFind
$cnthPatFind :: SimpleConstraint -> NthPatFind
isEmbed :: SimpleConstraint -> Bool
$cisEmbed :: SimpleConstraint -> Bool
isTerm :: SimpleConstraint -> All
$cisTerm :: SimpleConstraint -> All
isPat :: SimpleConstraint -> DisjointSet AnyName
$cisPat :: SimpleConstraint -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> SimpleConstraint -> SimpleConstraint
$copen :: AlphaCtx -> NthPatFind -> SimpleConstraint -> SimpleConstraint
close :: AlphaCtx -> NamePatFind -> SimpleConstraint -> SimpleConstraint
$cclose :: AlphaCtx -> NamePatFind -> SimpleConstraint -> SimpleConstraint
fvAny' :: AlphaCtx
-> (AnyName -> f AnyName) -> SimpleConstraint -> f SimpleConstraint
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx
-> (AnyName -> f AnyName) -> SimpleConstraint -> f SimpleConstraint
aeq' :: AlphaCtx -> SimpleConstraint -> SimpleConstraint -> Bool
$caeq' :: AlphaCtx -> SimpleConstraint -> SimpleConstraint -> Bool
$cp1Alpha :: Show SimpleConstraint
Alpha, Subst Type)
instance Pretty SimpleConstraint where
pretty :: SimpleConstraint -> Sem r Doc
pretty = \case
Type
ty1 :<: Type
ty2 -> Type -> Sem r Doc
forall t (r :: [(* -> *) -> * -> *]).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Type
ty1 Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc
"<:" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Type -> Sem r Doc
forall t (r :: [(* -> *) -> * -> *]).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Type
ty2
Type
ty1 :=: Type
ty2 -> Type -> Sem r Doc
forall t (r :: [(* -> *) -> * -> *]).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Type
ty1 Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc
"=" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Type -> Sem r Doc
forall t (r :: [(* -> *) -> * -> *]).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Type
ty2
data TyVarInfo = TVI
{ TyVarInfo -> First Ilk
_tyVarIlk :: First Ilk
, TyVarInfo -> Sort
_tyVarSort :: Sort
}
deriving (Int -> TyVarInfo -> ShowS
[TyVarInfo] -> ShowS
TyVarInfo -> String
(Int -> TyVarInfo -> ShowS)
-> (TyVarInfo -> String)
-> ([TyVarInfo] -> ShowS)
-> Show TyVarInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TyVarInfo] -> ShowS
$cshowList :: [TyVarInfo] -> ShowS
show :: TyVarInfo -> String
$cshow :: TyVarInfo -> String
showsPrec :: Int -> TyVarInfo -> ShowS
$cshowsPrec :: Int -> TyVarInfo -> ShowS
Show)
makeLenses ''TyVarInfo
instance Pretty TyVarInfo where
pretty :: TyVarInfo -> Sem r Doc
pretty (TVI (First Maybe Ilk
ilk) Sort
s) = Sem r Doc -> (Ilk -> Sem r Doc) -> Maybe Ilk -> Sem r Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Doc -> Sem r Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
"?") Ilk -> Sem r Doc
forall t (r :: [(* -> *) -> * -> *]).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Maybe Ilk
ilk Sem r Doc -> Sem r Doc -> Sem r Doc
forall a. Semigroup a => a -> a -> a
<> Sem r Doc
"%" Sem r Doc -> Sem r Doc -> Sem r Doc
forall a. Semigroup a => a -> a -> a
<> Sort -> Sem r Doc
forall t (r :: [(* -> *) -> * -> *]).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Sort
s
mkTVI :: Ilk -> Sort -> TyVarInfo
mkTVI :: Ilk -> Sort -> TyVarInfo
mkTVI = First Ilk -> Sort -> TyVarInfo
TVI (First Ilk -> Sort -> TyVarInfo)
-> (Ilk -> First Ilk) -> Ilk -> Sort -> TyVarInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Ilk -> First Ilk
forall a. Maybe a -> First a
First (Maybe Ilk -> First Ilk) -> (Ilk -> Maybe Ilk) -> Ilk -> First Ilk
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ilk -> Maybe Ilk
forall a. a -> Maybe a
Just
instance Semigroup TyVarInfo where
TVI First Ilk
i1 Sort
s1 <> :: TyVarInfo -> TyVarInfo -> TyVarInfo
<> TVI First Ilk
i2 Sort
s2 = First Ilk -> Sort -> TyVarInfo
TVI (First Ilk
i1 First Ilk -> First Ilk -> First Ilk
forall a. Semigroup a => a -> a -> a
<> First Ilk
i2) (Sort
s1 Sort -> Sort -> Sort
forall a. Semigroup a => a -> a -> a
<> Sort
s2)
newtype TyVarInfoMap = VM { TyVarInfoMap -> Map (Name Type) TyVarInfo
unVM :: Map (Name Type) TyVarInfo }
deriving (Int -> TyVarInfoMap -> ShowS
[TyVarInfoMap] -> ShowS
TyVarInfoMap -> String
(Int -> TyVarInfoMap -> ShowS)
-> (TyVarInfoMap -> String)
-> ([TyVarInfoMap] -> ShowS)
-> Show TyVarInfoMap
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TyVarInfoMap] -> ShowS
$cshowList :: [TyVarInfoMap] -> ShowS
show :: TyVarInfoMap -> String
$cshow :: TyVarInfoMap -> String
showsPrec :: Int -> TyVarInfoMap -> ShowS
$cshowsPrec :: Int -> TyVarInfoMap -> ShowS
Show)
instance Pretty TyVarInfoMap where
pretty :: TyVarInfoMap -> Sem r Doc
pretty (VM Map (Name Type) TyVarInfo
m) = Map (Name Type) TyVarInfo -> Sem r Doc
forall t (r :: [(* -> *) -> * -> *]).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Map (Name Type) TyVarInfo
m
onVM ::
(Map (Name Type) TyVarInfo -> Map (Name Type) TyVarInfo) ->
TyVarInfoMap -> TyVarInfoMap
onVM :: (Map (Name Type) TyVarInfo -> Map (Name Type) TyVarInfo)
-> TyVarInfoMap -> TyVarInfoMap
onVM Map (Name Type) TyVarInfo -> Map (Name Type) TyVarInfo
f (VM Map (Name Type) TyVarInfo
m) = Map (Name Type) TyVarInfo -> TyVarInfoMap
VM (Map (Name Type) TyVarInfo -> Map (Name Type) TyVarInfo
f Map (Name Type) TyVarInfo
m)
lookupVM :: Name Type -> TyVarInfoMap -> Maybe TyVarInfo
lookupVM :: Name Type -> TyVarInfoMap -> Maybe TyVarInfo
lookupVM Name Type
v = Name Type -> Map (Name Type) TyVarInfo -> Maybe TyVarInfo
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name Type
v (Map (Name Type) TyVarInfo -> Maybe TyVarInfo)
-> (TyVarInfoMap -> Map (Name Type) TyVarInfo)
-> TyVarInfoMap
-> Maybe TyVarInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarInfoMap -> Map (Name Type) TyVarInfo
unVM
deleteVM :: Name Type -> TyVarInfoMap -> TyVarInfoMap
deleteVM :: Name Type -> TyVarInfoMap -> TyVarInfoMap
deleteVM = (Map (Name Type) TyVarInfo -> Map (Name Type) TyVarInfo)
-> TyVarInfoMap -> TyVarInfoMap
onVM ((Map (Name Type) TyVarInfo -> Map (Name Type) TyVarInfo)
-> TyVarInfoMap -> TyVarInfoMap)
-> (Name Type
-> Map (Name Type) TyVarInfo -> Map (Name Type) TyVarInfo)
-> Name Type
-> TyVarInfoMap
-> TyVarInfoMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name Type -> Map (Name Type) TyVarInfo -> Map (Name Type) TyVarInfo
forall k a. Ord k => k -> Map k a -> Map k a
M.delete
addSkolems :: [Name Type] -> TyVarInfoMap -> TyVarInfoMap
addSkolems :: [Name Type] -> TyVarInfoMap -> TyVarInfoMap
addSkolems [Name Type]
vs = (Map (Name Type) TyVarInfo -> Map (Name Type) TyVarInfo)
-> TyVarInfoMap -> TyVarInfoMap
onVM ((Map (Name Type) TyVarInfo -> Map (Name Type) TyVarInfo)
-> TyVarInfoMap -> TyVarInfoMap)
-> (Map (Name Type) TyVarInfo -> Map (Name Type) TyVarInfo)
-> TyVarInfoMap
-> TyVarInfoMap
forall a b. (a -> b) -> a -> b
$ \Map (Name Type) TyVarInfo
vm -> (Map (Name Type) TyVarInfo
-> Name Type -> Map (Name Type) TyVarInfo)
-> Map (Name Type) TyVarInfo
-> [Name Type]
-> Map (Name Type) TyVarInfo
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ((Name Type
-> Map (Name Type) TyVarInfo -> Map (Name Type) TyVarInfo)
-> Map (Name Type) TyVarInfo
-> Name Type
-> Map (Name Type) TyVarInfo
forall a b c. (a -> b -> c) -> b -> a -> c
flip (\Name Type
v -> Name Type
-> TyVarInfo
-> Map (Name Type) TyVarInfo
-> Map (Name Type) TyVarInfo
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Name Type
v (Ilk -> Sort -> TyVarInfo
mkTVI Ilk
Skolem Sort
forall a. Monoid a => a
mempty))) Map (Name Type) TyVarInfo
vm [Name Type]
vs
instance Semigroup TyVarInfoMap where
VM Map (Name Type) TyVarInfo
sm1 <> :: TyVarInfoMap -> TyVarInfoMap -> TyVarInfoMap
<> VM Map (Name Type) TyVarInfo
sm2 = Map (Name Type) TyVarInfo -> TyVarInfoMap
VM ((TyVarInfo -> TyVarInfo -> TyVarInfo)
-> Map (Name Type) TyVarInfo
-> Map (Name Type) TyVarInfo
-> Map (Name Type) TyVarInfo
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith TyVarInfo -> TyVarInfo -> TyVarInfo
forall a. Semigroup a => a -> a -> a
(<>) Map (Name Type) TyVarInfo
sm1 Map (Name Type) TyVarInfo
sm2)
instance Monoid TyVarInfoMap where
mempty :: TyVarInfoMap
mempty = Map (Name Type) TyVarInfo -> TyVarInfoMap
VM Map (Name Type) TyVarInfo
forall k a. Map k a
M.empty
mappend :: TyVarInfoMap -> TyVarInfoMap -> TyVarInfoMap
mappend = TyVarInfoMap -> TyVarInfoMap -> TyVarInfoMap
forall a. Semigroup a => a -> a -> a
(<>)
getSort :: TyVarInfoMap -> Name Type -> Sort
getSort :: TyVarInfoMap -> Name Type -> Sort
getSort (VM Map (Name Type) TyVarInfo
m) Name Type
v = Sort -> (TyVarInfo -> Sort) -> Maybe TyVarInfo -> Sort
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Sort
topSort (Getting Sort TyVarInfo Sort -> TyVarInfo -> Sort
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Sort TyVarInfo Sort
Lens' TyVarInfo Sort
tyVarSort) (Name Type -> Map (Name Type) TyVarInfo -> Maybe TyVarInfo
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name Type
v Map (Name Type) TyVarInfo
m)
getIlk :: TyVarInfoMap -> Name Type -> Maybe Ilk
getIlk :: TyVarInfoMap -> Name Type -> Maybe Ilk
getIlk (VM Map (Name Type) TyVarInfo
m) Name Type
v = (Map (Name Type) TyVarInfo
m Map (Name Type) TyVarInfo
-> Getting
(First (First Ilk)) (Map (Name Type) TyVarInfo) (First Ilk)
-> Maybe (First Ilk)
forall s a. s -> Getting (First a) s a -> Maybe a
^? Index (Map (Name Type) TyVarInfo)
-> Traversal'
(Map (Name Type) TyVarInfo) (IxValue (Map (Name Type) TyVarInfo))
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Index (Map (Name Type) TyVarInfo)
Name Type
v ((TyVarInfo -> Const (First (First Ilk)) TyVarInfo)
-> Map (Name Type) TyVarInfo
-> Const (First (First Ilk)) (Map (Name Type) TyVarInfo))
-> ((First Ilk -> Const (First (First Ilk)) (First Ilk))
-> TyVarInfo -> Const (First (First Ilk)) TyVarInfo)
-> Getting
(First (First Ilk)) (Map (Name Type) TyVarInfo) (First Ilk)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (First Ilk -> Const (First (First Ilk)) (First Ilk))
-> TyVarInfo -> Const (First (First Ilk)) TyVarInfo
Lens' TyVarInfo (First Ilk)
tyVarIlk) Maybe (First Ilk) -> (First Ilk -> Maybe Ilk) -> Maybe Ilk
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= First Ilk -> Maybe Ilk
forall a. First a -> Maybe a
getFirst
extendSort :: Name Type -> Sort -> TyVarInfoMap -> TyVarInfoMap
extendSort :: Name Type -> Sort -> TyVarInfoMap -> TyVarInfoMap
extendSort Name Type
x Sort
s = (Map (Name Type) TyVarInfo -> Map (Name Type) TyVarInfo)
-> TyVarInfoMap -> TyVarInfoMap
onVM (Index (Map (Name Type) TyVarInfo)
-> Lens'
(Map (Name Type) TyVarInfo)
(Maybe (IxValue (Map (Name Type) TyVarInfo)))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at Index (Map (Name Type) TyVarInfo)
Name Type
x ((Maybe TyVarInfo -> Identity (Maybe TyVarInfo))
-> Map (Name Type) TyVarInfo
-> Identity (Map (Name Type) TyVarInfo))
-> ((Sort -> Identity Sort)
-> Maybe TyVarInfo -> Identity (Maybe TyVarInfo))
-> (Sort -> Identity Sort)
-> Map (Name Type) TyVarInfo
-> Identity (Map (Name Type) TyVarInfo)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyVarInfo -> Identity TyVarInfo)
-> Maybe TyVarInfo -> Identity (Maybe TyVarInfo)
forall a b. Prism (Maybe a) (Maybe b) a b
_Just ((TyVarInfo -> Identity TyVarInfo)
-> Maybe TyVarInfo -> Identity (Maybe TyVarInfo))
-> ((Sort -> Identity Sort) -> TyVarInfo -> Identity TyVarInfo)
-> (Sort -> Identity Sort)
-> Maybe TyVarInfo
-> Identity (Maybe TyVarInfo)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Sort -> Identity Sort) -> TyVarInfo -> Identity TyVarInfo
Lens' TyVarInfo Sort
tyVarSort ((Sort -> Identity Sort)
-> Map (Name Type) TyVarInfo
-> Identity (Map (Name Type) TyVarInfo))
-> (Sort -> Sort)
-> Map (Name Type) TyVarInfo
-> Map (Name Type) TyVarInfo
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (Sort -> Sort -> Sort
forall a. Ord a => Set a -> Set a -> Set a
`S.union` Sort
s))
data SimplifyState = SS
{ SimplifyState -> TyVarInfoMap
_ssVarMap :: TyVarInfoMap
, SimplifyState -> [SimpleConstraint]
_ssConstraints :: [SimpleConstraint]
, SimplifyState -> S
_ssSubst :: S
, SimplifyState -> Set SimpleConstraint
_ssSeen :: Set SimpleConstraint
}
makeLenses ''SimplifyState
lkup :: (Ord k, Show k, Show (Map k a)) => String -> Map k a -> k -> a
lkup :: String -> Map k a -> k -> a
lkup String
messg Map k a
m k
k = a -> Maybe a -> a
forall a. a -> Maybe a -> a
fromMaybe (String -> a
forall a. HasCallStack => String -> a
error String
errMsg) (k -> Map k a -> Maybe a
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup k
k Map k a
m)
where
errMsg :: String
errMsg = [String] -> String
unlines
[ String
"Key lookup error:"
, String
" Key = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ k -> String
forall a. Show a => a -> String
show k
k
, String
" Map = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Map k a -> String
forall a. Show a => a -> String
show Map k a
m
, String
" Location: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
messg
]
solveConstraint
:: Members '[Fresh, Error SolveError, Output Message, Input TyDefCtx] r
=> Constraint -> Sem r S
solveConstraint :: Constraint -> Sem r S
solveConstraint Constraint
c = do
Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug Sem r Doc
"Solving:"
Constraint -> Sem r ()
forall (r :: [(* -> *) -> * -> *]) t.
(Member (Output Message) r, Pretty t) =>
t -> Sem r ()
debugPretty Constraint
c
Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug Sem r Doc
"------------------------------"
Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug Sem r Doc
"Decomposing constraints..."
[(TyVarInfoMap, [SimpleConstraint])]
qcList <- Constraint -> Sem r [(TyVarInfoMap, [SimpleConstraint])]
forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Constraint -> Sem r [(TyVarInfoMap, [SimpleConstraint])]
decomposeConstraint Constraint
c
[Sem r S] -> Sem r S
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
[Sem r a] -> Sem r a
asum' (((TyVarInfoMap, [SimpleConstraint]) -> Sem r S)
-> [(TyVarInfoMap, [SimpleConstraint])] -> [Sem r S]
forall a b. (a -> b) -> [a] -> [b]
map ((TyVarInfoMap -> [SimpleConstraint] -> Sem r S)
-> (TyVarInfoMap, [SimpleConstraint]) -> Sem r S
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry TyVarInfoMap -> [SimpleConstraint] -> Sem r S
forall (r :: [(* -> *) -> * -> *]).
Members
'[Fresh, Error SolveError, Output Message, Input TyDefCtx] r =>
TyVarInfoMap -> [SimpleConstraint] -> Sem r S
solveConstraintChoice) [(TyVarInfoMap, [SimpleConstraint])]
qcList)
solveConstraintChoice
:: Members '[Fresh, Error SolveError, Output Message, Input TyDefCtx] r
=> TyVarInfoMap -> [SimpleConstraint] -> Sem r S
solveConstraintChoice :: TyVarInfoMap -> [SimpleConstraint] -> Sem r S
solveConstraintChoice TyVarInfoMap
quals [SimpleConstraint]
cs = do
TyVarInfoMap -> Sem r ()
forall (r :: [(* -> *) -> * -> *]) t.
(Member (Output Message) r, Pretty t) =>
t -> Sem r ()
debugPretty TyVarInfoMap
quals
Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug (Sem r Doc -> Sem r ()) -> Sem r Doc -> Sem r ()
forall a b. (a -> b) -> a -> b
$ [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
vcat ((SimpleConstraint -> Sem r Doc)
-> [SimpleConstraint] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map SimpleConstraint -> Sem r Doc
forall t (r :: [(* -> *) -> * -> *]). Pretty t => t -> Sem r Doc
pretty' [SimpleConstraint]
cs)
TyDefCtx
tyDefns <- forall (r :: [(* -> *) -> * -> *]).
Member (Input TyDefCtx) r =>
Sem r TyDefCtx
forall i (r :: [(* -> *) -> * -> *]). Member (Input i) r => Sem r i
input @TyDefCtx
let toEqn :: SimpleConstraint -> (Type, Type)
toEqn (Type
t1 :<: Type
t2) = (Type
t1,Type
t2)
toEqn (Type
t1 :=: Type
t2) = (Type
t1,Type
t2)
S
_ <- SolveError -> Maybe S -> Sem r S
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Maybe a -> Sem r a
note SolveError
NoWeakUnifier (Maybe S -> Sem r S) -> Maybe S -> Sem r S
forall a b. (a -> b) -> a -> b
$ TyDefCtx -> [(Type, Type)] -> Maybe S
weakUnify TyDefCtx
tyDefns ((SimpleConstraint -> (Type, Type))
-> [SimpleConstraint] -> [(Type, Type)]
forall a b. (a -> b) -> [a] -> [b]
map SimpleConstraint -> (Type, Type)
toEqn [SimpleConstraint]
cs)
Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug Sem r Doc
"------------------------------"
Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug Sem r Doc
"Running simplifier..."
(TyVarInfoMap
vm, [(Atom, Atom)]
atoms, S
theta_simp) <- TyVarInfoMap
-> [SimpleConstraint] -> Sem r (TyVarInfoMap, [(Atom, Atom)], S)
forall (r :: [(* -> *) -> * -> *]).
Members '[Error SolveError, Output Message, Input TyDefCtx] r =>
TyVarInfoMap
-> [SimpleConstraint] -> Sem r (TyVarInfoMap, [(Atom, Atom)], S)
simplify TyVarInfoMap
quals [SimpleConstraint]
cs
Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug Sem r Doc
"Done running simplifier. Results:"
TyVarInfoMap -> Sem r ()
forall (r :: [(* -> *) -> * -> *]) t.
(Member (Output Message) r, Pretty t) =>
t -> Sem r ()
debugPretty TyVarInfoMap
vm
Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug (Sem r Doc -> Sem r ()) -> Sem r Doc -> Sem r ()
forall a b. (a -> b) -> a -> b
$ [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
vcat ([Sem r Doc] -> Sem r Doc) -> [Sem r Doc] -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ ((Atom, Atom) -> Sem r Doc) -> [(Atom, Atom)] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map (SimpleConstraint -> Sem r Doc
forall t (r :: [(* -> *) -> * -> *]). Pretty t => t -> Sem r Doc
pretty' (SimpleConstraint -> Sem r Doc)
-> ((Atom, Atom) -> SimpleConstraint) -> (Atom, Atom) -> Sem r Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(Atom
x,Atom
y) -> Atom -> Type
TyAtom Atom
x Type -> Type -> SimpleConstraint
:<: Atom -> Type
TyAtom Atom
y)) [(Atom, Atom)]
atoms
S -> Sem r ()
forall (r :: [(* -> *) -> * -> *]) t.
(Member (Output Message) r, Pretty t) =>
t -> Sem r ()
debugPretty S
theta_simp
Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug Sem r Doc
"------------------------------"
Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug Sem r Doc
"Generating constraint graph..."
let mkAVar :: (Name Type, First Ilk) -> Atom
mkAVar (Name Type
v, First (Just Ilk
Skolem)) = Var -> Atom
AVar (Name Type -> Var
S Name Type
v)
mkAVar (Name Type
v, First Ilk
_ ) = Var -> Atom
AVar (Name Type -> Var
U Name Type
v)
vars :: Set Atom
vars = [Atom] -> Set Atom
forall a. Ord a => [a] -> Set a
S.fromList ([Atom] -> Set Atom)
-> (TyVarInfoMap -> [Atom]) -> TyVarInfoMap -> Set Atom
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Name Type, TyVarInfo) -> Atom)
-> [(Name Type, TyVarInfo)] -> [Atom]
forall a b. (a -> b) -> [a] -> [b]
map ((Name Type, First Ilk) -> Atom
mkAVar ((Name Type, First Ilk) -> Atom)
-> ((Name Type, TyVarInfo) -> (Name Type, First Ilk))
-> (Name Type, TyVarInfo)
-> Atom
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyVarInfo -> First Ilk)
-> (Name Type, TyVarInfo) -> (Name Type, First Ilk)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (Getting (First Ilk) TyVarInfo (First Ilk) -> TyVarInfo -> First Ilk
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting (First Ilk) TyVarInfo (First Ilk)
Lens' TyVarInfo (First Ilk)
tyVarIlk)) ([(Name Type, TyVarInfo)] -> [Atom])
-> (TyVarInfoMap -> [(Name Type, TyVarInfo)])
-> TyVarInfoMap
-> [Atom]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (Name Type) TyVarInfo -> [(Name Type, TyVarInfo)]
forall k a. Map k a -> [(k, a)]
M.assocs (Map (Name Type) TyVarInfo -> [(Name Type, TyVarInfo)])
-> (TyVarInfoMap -> Map (Name Type) TyVarInfo)
-> TyVarInfoMap
-> [(Name Type, TyVarInfo)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarInfoMap -> Map (Name Type) TyVarInfo
unVM (TyVarInfoMap -> Set Atom) -> TyVarInfoMap -> Set Atom
forall a b. (a -> b) -> a -> b
$ TyVarInfoMap
vm
g :: Graph Atom
g = Set Atom -> [(Atom, Atom)] -> Graph Atom
forall a. (Show a, Ord a) => Set a -> [(a, a)] -> Graph a
mkConstraintGraph Set Atom
vars [(Atom, Atom)]
atoms
Graph Atom -> Sem r ()
forall (r :: [(* -> *) -> * -> *]) t.
(Member (Output Message) r, Pretty t) =>
t -> Sem r ()
debugPretty Graph Atom
g
Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug Sem r Doc
"------------------------------"
Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug Sem r Doc
"Checking WCCs for skolems..."
(Graph UAtom
g', S
theta_skolem) <- TyVarInfoMap -> Graph Atom -> Sem r (Graph UAtom, S)
forall (r :: [(* -> *) -> * -> *]).
Members '[Error SolveError, Output Message, Input TyDefCtx] r =>
TyVarInfoMap -> Graph Atom -> Sem r (Graph UAtom, S)
checkSkolems TyVarInfoMap
vm Graph Atom
g
S -> Sem r ()
forall (r :: [(* -> *) -> * -> *]) t.
(Member (Output Message) r, Pretty t) =>
t -> Sem r ()
debugPretty S
theta_skolem
Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug Sem r Doc
"------------------------------"
Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug Sem r Doc
"Collapsing SCCs..."
(Graph UAtom
g'', S
theta_cyc) <- TyDefCtx -> Graph UAtom -> Sem r (Graph UAtom, S)
forall (r :: [(* -> *) -> * -> *]).
Members '[Error SolveError] r =>
TyDefCtx -> Graph UAtom -> Sem r (Graph UAtom, S)
elimCycles TyDefCtx
tyDefns Graph UAtom
g'
Graph UAtom -> Sem r ()
forall (r :: [(* -> *) -> * -> *]) t.
(Member (Output Message) r, Pretty t) =>
t -> Sem r ()
debugPretty Graph UAtom
g''
S -> Sem r ()
forall (r :: [(* -> *) -> * -> *]) t.
(Member (Output Message) r, Pretty t) =>
t -> Sem r ()
debugPretty S
theta_cyc
let sortOK :: (Name Type, Type) -> Bool
sortOK (Name Type
x, TyAtom (ABase BaseTy
ty)) = BaseTy -> Sort -> Bool
hasSort BaseTy
ty (TyVarInfoMap -> Name Type -> Sort
getSort TyVarInfoMap
vm Name Type
x)
sortOK (Name Type
_, TyAtom (AVar (U Name Type
_))) = Bool
True
sortOK (Name Type, Type)
p = String -> Bool
forall a. HasCallStack => String -> a
error (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ String
"Impossible! sortOK " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Name Type, Type) -> String
forall a. Show a => a -> String
show (Name Type, Type)
p
Bool -> Sem r () -> Sem r ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (((Name Type, Type) -> Bool) -> [(Name Type, Type)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Name Type, Type) -> Bool
sortOK (S -> [(Name Type, Type)]
forall a. Substitution a -> [(Name a, a)]
Subst.toList S
theta_cyc))
(Sem r () -> Sem r ()) -> Sem r () -> Sem r ()
forall a b. (a -> b) -> a -> b
$ SolveError -> Sem r ()
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw SolveError
NoUnify
Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug Sem r Doc
"Old sort map:"
TyVarInfoMap -> Sem r ()
forall (r :: [(* -> *) -> * -> *]) t.
(Member (Output Message) r, Pretty t) =>
t -> Sem r ()
debugPretty TyVarInfoMap
vm
let vm' :: TyVarInfoMap
vm' = ((Name Type, Type) -> TyVarInfoMap -> TyVarInfoMap)
-> TyVarInfoMap -> [(Name Type, Type)] -> TyVarInfoMap
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Name Type, Type) -> TyVarInfoMap -> TyVarInfoMap
updateVarMap TyVarInfoMap
vm (S -> [(Name Type, Type)]
forall a. Substitution a -> [(Name a, a)]
Subst.toList S
theta_cyc)
where
updateVarMap :: (Name Type, Type) -> TyVarInfoMap -> TyVarInfoMap
updateVarMap :: (Name Type, Type) -> TyVarInfoMap -> TyVarInfoMap
updateVarMap (Name Type
x, TyAtom (AVar (U Name Type
y))) TyVarInfoMap
vmm = Name Type -> Sort -> TyVarInfoMap -> TyVarInfoMap
extendSort Name Type
y (TyVarInfoMap -> Name Type -> Sort
getSort TyVarInfoMap
vmm Name Type
x) TyVarInfoMap
vmm
updateVarMap (Name Type, Type)
_ TyVarInfoMap
vmm = TyVarInfoMap
vmm
Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug Sem r Doc
"Updated sort map:"
TyVarInfoMap -> Sem r ()
forall (r :: [(* -> *) -> * -> *]) t.
(Member (Output Message) r, Pretty t) =>
t -> Sem r ()
debugPretty TyVarInfoMap
vm
Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug Sem r Doc
"------------------------------"
Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug Sem r Doc
"Solving for type variables..."
S
theta_sol <- TyVarInfoMap -> Graph UAtom -> Sem r S
forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Output Message] r =>
TyVarInfoMap -> Graph UAtom -> Sem r S
solveGraph TyVarInfoMap
vm' Graph UAtom
g''
S -> Sem r ()
forall (r :: [(* -> *) -> * -> *]) t.
(Member (Output Message) r, Pretty t) =>
t -> Sem r ()
debugPretty S
theta_sol
Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug Sem r Doc
"------------------------------"
Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug Sem r Doc
"Composing final substitution..."
let theta_final :: S
theta_final = S
theta_sol S -> S -> S
forall a.
Subst a a =>
Substitution a -> Substitution a -> Substitution a
@@ S
theta_cyc S -> S -> S
forall a.
Subst a a =>
Substitution a -> Substitution a -> Substitution a
@@ S
theta_skolem S -> S -> S
forall a.
Subst a a =>
Substitution a -> Substitution a -> Substitution a
@@ S
theta_simp
S -> Sem r ()
forall (r :: [(* -> *) -> * -> *]) t.
(Member (Output Message) r, Pretty t) =>
t -> Sem r ()
debugPretty S
theta_final
S -> Sem r S
forall (m :: * -> *) a. Monad m => a -> m a
return S
theta_final
decomposeConstraint
:: Members '[Fresh, Error SolveError, Input TyDefCtx] r
=> Constraint -> Sem r [(TyVarInfoMap, [SimpleConstraint])]
decomposeConstraint :: Constraint -> Sem r [(TyVarInfoMap, [SimpleConstraint])]
decomposeConstraint (CSub Type
t1 Type
t2) = [(TyVarInfoMap, [SimpleConstraint])]
-> Sem r [(TyVarInfoMap, [SimpleConstraint])]
forall (m :: * -> *) a. Monad m => a -> m a
return [(TyVarInfoMap
forall a. Monoid a => a
mempty, [Type
t1 Type -> Type -> SimpleConstraint
:<: Type
t2])]
decomposeConstraint (CEq Type
t1 Type
t2) = [(TyVarInfoMap, [SimpleConstraint])]
-> Sem r [(TyVarInfoMap, [SimpleConstraint])]
forall (m :: * -> *) a. Monad m => a -> m a
return [(TyVarInfoMap
forall a. Monoid a => a
mempty, [Type
t1 Type -> Type -> SimpleConstraint
:=: Type
t2])]
decomposeConstraint (CQual Qualifier
q Type
ty) = ((TyVarInfoMap, [SimpleConstraint])
-> [(TyVarInfoMap, [SimpleConstraint])]
-> [(TyVarInfoMap, [SimpleConstraint])]
forall a. a -> [a] -> [a]
:[]) ((TyVarInfoMap, [SimpleConstraint])
-> [(TyVarInfoMap, [SimpleConstraint])])
-> (TyVarInfoMap -> (TyVarInfoMap, [SimpleConstraint]))
-> TyVarInfoMap
-> [(TyVarInfoMap, [SimpleConstraint])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (, []) (TyVarInfoMap -> [(TyVarInfoMap, [SimpleConstraint])])
-> Sem r TyVarInfoMap -> Sem r [(TyVarInfoMap, [SimpleConstraint])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Qualifier -> Sem r TyVarInfoMap
forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Type -> Qualifier -> Sem r TyVarInfoMap
decomposeQual Type
ty Qualifier
q
decomposeConstraint (CAnd [Constraint]
cs) = ([(TyVarInfoMap, [SimpleConstraint])]
-> (TyVarInfoMap, [SimpleConstraint]))
-> [[(TyVarInfoMap, [SimpleConstraint])]]
-> [(TyVarInfoMap, [SimpleConstraint])]
forall a b. (a -> b) -> [a] -> [b]
map [(TyVarInfoMap, [SimpleConstraint])]
-> (TyVarInfoMap, [SimpleConstraint])
forall a. Monoid a => [a] -> a
mconcat ([[(TyVarInfoMap, [SimpleConstraint])]]
-> [(TyVarInfoMap, [SimpleConstraint])])
-> ([[(TyVarInfoMap, [SimpleConstraint])]]
-> [[(TyVarInfoMap, [SimpleConstraint])]])
-> [[(TyVarInfoMap, [SimpleConstraint])]]
-> [(TyVarInfoMap, [SimpleConstraint])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[(TyVarInfoMap, [SimpleConstraint])]]
-> [[(TyVarInfoMap, [SimpleConstraint])]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ([[(TyVarInfoMap, [SimpleConstraint])]]
-> [(TyVarInfoMap, [SimpleConstraint])])
-> Sem r [[(TyVarInfoMap, [SimpleConstraint])]]
-> Sem r [(TyVarInfoMap, [SimpleConstraint])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Constraint -> Sem r [(TyVarInfoMap, [SimpleConstraint])])
-> [Constraint] -> Sem r [[(TyVarInfoMap, [SimpleConstraint])]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Constraint -> Sem r [(TyVarInfoMap, [SimpleConstraint])]
forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Constraint -> Sem r [(TyVarInfoMap, [SimpleConstraint])]
decomposeConstraint [Constraint]
cs
decomposeConstraint Constraint
CTrue = [(TyVarInfoMap, [SimpleConstraint])]
-> Sem r [(TyVarInfoMap, [SimpleConstraint])]
forall (m :: * -> *) a. Monad m => a -> m a
return [(TyVarInfoMap, [SimpleConstraint])
forall a. Monoid a => a
mempty]
decomposeConstraint (CAll Bind [Name Type] Constraint
ty) = do
([Name Type]
vars, Constraint
c) <- Bind [Name Type] Constraint -> Sem r ([Name Type], Constraint)
forall (r :: [(* -> *) -> * -> *]) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind Bind [Name Type] Constraint
ty
let c' :: Constraint
c' = [(Name Type, Type)] -> Constraint -> Constraint
forall b a. Subst b a => [(Name b, b)] -> a -> a
substs ([Name Type] -> [(Name Type, Type)]
mkSkolems [Name Type]
vars) Constraint
c
(((TyVarInfoMap, [SimpleConstraint])
-> (TyVarInfoMap, [SimpleConstraint]))
-> [(TyVarInfoMap, [SimpleConstraint])]
-> [(TyVarInfoMap, [SimpleConstraint])]
forall a b. (a -> b) -> [a] -> [b]
map (((TyVarInfoMap, [SimpleConstraint])
-> (TyVarInfoMap, [SimpleConstraint]))
-> [(TyVarInfoMap, [SimpleConstraint])]
-> [(TyVarInfoMap, [SimpleConstraint])])
-> ([Name Type]
-> (TyVarInfoMap, [SimpleConstraint])
-> (TyVarInfoMap, [SimpleConstraint]))
-> [Name Type]
-> [(TyVarInfoMap, [SimpleConstraint])]
-> [(TyVarInfoMap, [SimpleConstraint])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyVarInfoMap -> TyVarInfoMap)
-> (TyVarInfoMap, [SimpleConstraint])
-> (TyVarInfoMap, [SimpleConstraint])
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ((TyVarInfoMap -> TyVarInfoMap)
-> (TyVarInfoMap, [SimpleConstraint])
-> (TyVarInfoMap, [SimpleConstraint]))
-> ([Name Type] -> TyVarInfoMap -> TyVarInfoMap)
-> [Name Type]
-> (TyVarInfoMap, [SimpleConstraint])
-> (TyVarInfoMap, [SimpleConstraint])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name Type] -> TyVarInfoMap -> TyVarInfoMap
addSkolems) [Name Type]
vars ([(TyVarInfoMap, [SimpleConstraint])]
-> [(TyVarInfoMap, [SimpleConstraint])])
-> Sem r [(TyVarInfoMap, [SimpleConstraint])]
-> Sem r [(TyVarInfoMap, [SimpleConstraint])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Constraint -> Sem r [(TyVarInfoMap, [SimpleConstraint])]
forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Constraint -> Sem r [(TyVarInfoMap, [SimpleConstraint])]
decomposeConstraint Constraint
c'
where
mkSkolems :: [Name Type] -> [(Name Type, Type)]
mkSkolems :: [Name Type] -> [(Name Type, Type)]
mkSkolems = (Name Type -> (Name Type, Type))
-> [Name Type] -> [(Name Type, Type)]
forall a b. (a -> b) -> [a] -> [b]
map (Name Type -> Name Type
forall a. a -> a
id (Name Type -> Name Type)
-> (Name Type -> Type) -> Name Type -> (Name Type, Type)
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& Name Type -> Type
TySkolem)
decomposeConstraint (COr [Constraint]
cs) = [[(TyVarInfoMap, [SimpleConstraint])]]
-> [(TyVarInfoMap, [SimpleConstraint])]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(TyVarInfoMap, [SimpleConstraint])]]
-> [(TyVarInfoMap, [SimpleConstraint])])
-> Sem r [[(TyVarInfoMap, [SimpleConstraint])]]
-> Sem r [(TyVarInfoMap, [SimpleConstraint])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Sem r [(TyVarInfoMap, [SimpleConstraint])]]
-> Sem r [[(TyVarInfoMap, [SimpleConstraint])]]
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
[Sem r a] -> Sem r [a]
filterErrors ((Constraint -> Sem r [(TyVarInfoMap, [SimpleConstraint])])
-> [Constraint] -> [Sem r [(TyVarInfoMap, [SimpleConstraint])]]
forall a b. (a -> b) -> [a] -> [b]
map Constraint -> Sem r [(TyVarInfoMap, [SimpleConstraint])]
forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Constraint -> Sem r [(TyVarInfoMap, [SimpleConstraint])]
decomposeConstraint [Constraint]
cs)
decomposeQual
:: Members '[Fresh, Error SolveError, Input TyDefCtx] r
=> Type -> Qualifier -> Sem r TyVarInfoMap
decomposeQual :: Type -> Qualifier -> Sem r TyVarInfoMap
decomposeQual = Set (String, [Type], Qualifier)
-> Type -> Qualifier -> Sem r TyVarInfoMap
forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Set (String, [Type], Qualifier)
-> Type -> Qualifier -> Sem r TyVarInfoMap
go Set (String, [Type], Qualifier)
forall a. Set a
S.empty
where
go :: Members '[Fresh, Error SolveError, Input TyDefCtx] r
=> Set (String, [Type], Qualifier) -> Type -> Qualifier -> Sem r TyVarInfoMap
go :: Set (String, [Type], Qualifier)
-> Type -> Qualifier -> Sem r TyVarInfoMap
go Set (String, [Type], Qualifier)
_ (TyAtom Atom
a) Qualifier
q = Qualifier -> Atom -> Sem r TyVarInfoMap
forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError] r =>
Qualifier -> Atom -> Sem r TyVarInfoMap
checkQual Qualifier
q Atom
a
go Set (String, [Type], Qualifier)
seen (TyCon (CUser String
t) [Type]
tys) Qualifier
q = do
case (String
t, [Type]
tys, Qualifier
q) (String, [Type], Qualifier)
-> Set (String, [Type], Qualifier) -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set (String, [Type], Qualifier)
seen of
Bool
True -> TyVarInfoMap -> Sem r TyVarInfoMap
forall (m :: * -> *) a. Monad m => a -> m a
return TyVarInfoMap
forall a. Monoid a => a
mempty
Bool
False -> do
TyDefCtx
tyDefns <- forall (r :: [(* -> *) -> * -> *]).
Member (Input TyDefCtx) r =>
Sem r TyDefCtx
forall i (r :: [(* -> *) -> * -> *]). Member (Input i) r => Sem r i
input @TyDefCtx
case String -> TyDefCtx -> Maybe TyDefBody
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
t TyDefCtx
tyDefns of
Maybe TyDefBody
Nothing -> String -> Sem r TyVarInfoMap
forall a. HasCallStack => String -> a
error (String -> Sem r TyVarInfoMap) -> String -> Sem r TyVarInfoMap
forall a b. (a -> b) -> a -> b
$ ShowS
forall a. Show a => a -> String
show String
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" not in ty defn map!!"
Just (TyDefBody [String]
_ [Type] -> Type
body) -> do
let ty' :: Type
ty' = [Type] -> Type
body [Type]
tys
Set (String, [Type], Qualifier)
-> Type -> Qualifier -> Sem r TyVarInfoMap
forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Set (String, [Type], Qualifier)
-> Type -> Qualifier -> Sem r TyVarInfoMap
go ((String, [Type], Qualifier)
-> Set (String, [Type], Qualifier)
-> Set (String, [Type], Qualifier)
forall a. Ord a => a -> Set a -> Set a
S.insert (String
t, [Type]
tys, Qualifier
q) Set (String, [Type], Qualifier)
seen) Type
ty' Qualifier
q
go Set (String, [Type], Qualifier)
seen (TyCon (CContainer (AVar Var
_)) [Type]
tys) Qualifier
q = Set (String, [Type], Qualifier)
-> Type -> Qualifier -> Sem r TyVarInfoMap
forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Set (String, [Type], Qualifier)
-> Type -> Qualifier -> Sem r TyVarInfoMap
go Set (String, [Type], Qualifier)
seen (Con -> [Type] -> Type
TyCon Con
CList [Type]
tys) Qualifier
q
go Set (String, [Type], Qualifier)
seen ty :: Type
ty@(TyCon Con
c [Type]
tys) Qualifier
q = case Con -> Qualifier -> Maybe [Maybe Qualifier]
qualRules Con
c Qualifier
q of
Maybe [Maybe Qualifier]
Nothing -> SolveError -> Sem r TyVarInfoMap
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw (SolveError -> Sem r TyVarInfoMap)
-> SolveError -> Sem r TyVarInfoMap
forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> SolveError
Unqual Qualifier
q Type
ty
Just [Maybe Qualifier]
qs -> [TyVarInfoMap] -> TyVarInfoMap
forall a. Monoid a => [a] -> a
mconcat ([TyVarInfoMap] -> TyVarInfoMap)
-> Sem r [TyVarInfoMap] -> Sem r TyVarInfoMap
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type -> Maybe Qualifier -> Sem r TyVarInfoMap)
-> [Type] -> [Maybe Qualifier] -> Sem r [TyVarInfoMap]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (Sem r TyVarInfoMap
-> (Qualifier -> Sem r TyVarInfoMap)
-> Maybe Qualifier
-> Sem r TyVarInfoMap
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (TyVarInfoMap -> Sem r TyVarInfoMap
forall (m :: * -> *) a. Monad m => a -> m a
return TyVarInfoMap
forall a. Monoid a => a
mempty) ((Qualifier -> Sem r TyVarInfoMap)
-> Maybe Qualifier -> Sem r TyVarInfoMap)
-> (Type -> Qualifier -> Sem r TyVarInfoMap)
-> Type
-> Maybe Qualifier
-> Sem r TyVarInfoMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (String, [Type], Qualifier)
-> Type -> Qualifier -> Sem r TyVarInfoMap
forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Set (String, [Type], Qualifier)
-> Type -> Qualifier -> Sem r TyVarInfoMap
go Set (String, [Type], Qualifier)
seen) [Type]
tys [Maybe Qualifier]
qs
checkQual
:: Members '[Fresh, Error SolveError] r
=> Qualifier -> Atom -> Sem r TyVarInfoMap
checkQual :: Qualifier -> Atom -> Sem r TyVarInfoMap
checkQual Qualifier
q (AVar (U Name Type
v)) = TyVarInfoMap -> Sem r TyVarInfoMap
forall (m :: * -> *) a. Monad m => a -> m a
return (TyVarInfoMap -> Sem r TyVarInfoMap)
-> (TyVarInfo -> TyVarInfoMap) -> TyVarInfo -> Sem r TyVarInfoMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (Name Type) TyVarInfo -> TyVarInfoMap
VM (Map (Name Type) TyVarInfo -> TyVarInfoMap)
-> (TyVarInfo -> Map (Name Type) TyVarInfo)
-> TyVarInfo
-> TyVarInfoMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name Type -> TyVarInfo -> Map (Name Type) TyVarInfo
forall k a. k -> a -> Map k a
M.singleton Name Type
v (TyVarInfo -> Sem r TyVarInfoMap)
-> TyVarInfo -> Sem r TyVarInfoMap
forall a b. (a -> b) -> a -> b
$ Ilk -> Sort -> TyVarInfo
mkTVI Ilk
Unification (Qualifier -> Sort
forall a. a -> Set a
S.singleton Qualifier
q)
checkQual Qualifier
q (AVar (S Name Type
v)) = SolveError -> Sem r TyVarInfoMap
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw (SolveError -> Sem r TyVarInfoMap)
-> SolveError -> Sem r TyVarInfoMap
forall a b. (a -> b) -> a -> b
$ Qualifier -> Name Type -> SolveError
QualSkolem Qualifier
q Name Type
v
checkQual Qualifier
q (ABase BaseTy
bty) =
case BaseTy -> Qualifier -> Bool
hasQual BaseTy
bty Qualifier
q of
Bool
True -> TyVarInfoMap -> Sem r TyVarInfoMap
forall (m :: * -> *) a. Monad m => a -> m a
return TyVarInfoMap
forall a. Monoid a => a
mempty
Bool
False -> SolveError -> Sem r TyVarInfoMap
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw (SolveError -> Sem r TyVarInfoMap)
-> SolveError -> Sem r TyVarInfoMap
forall a b. (a -> b) -> a -> b
$ Qualifier -> BaseTy -> SolveError
UnqualBase Qualifier
q BaseTy
bty
simplify
:: Members '[Error SolveError, Output Message, Input TyDefCtx] r
=> TyVarInfoMap -> [SimpleConstraint] -> Sem r (TyVarInfoMap, [(Atom, Atom)], S)
simplify :: TyVarInfoMap
-> [SimpleConstraint] -> Sem r (TyVarInfoMap, [(Atom, Atom)], S)
simplify TyVarInfoMap
origVM [SimpleConstraint]
cs
= (\(SS TyVarInfoMap
vm' [SimpleConstraint]
cs' S
s' Set SimpleConstraint
_) -> (TyVarInfoMap
vm', (SimpleConstraint -> (Atom, Atom))
-> [SimpleConstraint] -> [(Atom, Atom)]
forall a b. (a -> b) -> [a] -> [b]
map SimpleConstraint -> (Atom, Atom)
extractAtoms [SimpleConstraint]
cs', S
s'))
(SimplifyState -> (TyVarInfoMap, [(Atom, Atom)], S))
-> Sem r SimplifyState -> Sem r (TyVarInfoMap, [(Atom, Atom)], S)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Integer -> Sem (Fresh : r) SimplifyState -> Sem r SimplifyState
forall (r :: [(* -> *) -> * -> *]) a.
Integer -> Sem (Fresh : r) a -> Sem r a
runFresh' Integer
n (SimplifyState
-> Sem (State SimplifyState : Fresh : r) ()
-> Sem (Fresh : r) SimplifyState
forall s (r :: [(* -> *) -> * -> *]) a.
s -> Sem (State s : r) a -> Sem r s
execState (TyVarInfoMap
-> [SimpleConstraint] -> S -> Set SimpleConstraint -> SimplifyState
SS TyVarInfoMap
origVM [SimpleConstraint]
cs S
forall a. Substitution a
idS Set SimpleConstraint
forall a. Set a
S.empty) Sem (State SimplifyState : Fresh : r) ()
forall (r :: [(* -> *) -> * -> *]).
Members
'[State SimplifyState, Fresh, Error SolveError, Output Message,
Input TyDefCtx]
r =>
Sem r ()
simplify')
where
fvNums :: Alpha a => [a] -> [Integer]
fvNums :: [a] -> [Integer]
fvNums = (Name Type -> Integer) -> [Name Type] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map (Name Type -> Integer
forall a. Name a -> Integer
name2Integer :: Name Type -> Integer) ([Name Type] -> [Integer])
-> ([a] -> [Name Type]) -> [a] -> [Integer]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting (Endo [Name Type]) [a] (Name Type) -> [a] -> [Name Type]
forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf Getting (Endo [Name Type]) [a] (Name Type)
forall a (f :: * -> *) b.
(Alpha a, Typeable b, Contravariant f, Applicative f) =>
(Name b -> f (Name b)) -> a -> f a
fv
n1 :: Integer
n1 = [Integer] -> Integer
forall p. (Num p, Ord p) => [p] -> p
maximum0 ([Integer] -> Integer)
-> ([SimpleConstraint] -> [Integer])
-> [SimpleConstraint]
-> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SimpleConstraint] -> [Integer]
forall a. Alpha a => [a] -> [Integer]
fvNums ([SimpleConstraint] -> Integer) -> [SimpleConstraint] -> Integer
forall a b. (a -> b) -> a -> b
$ [SimpleConstraint]
cs
n :: Integer
n = Integer -> Integer
forall a. Enum a => a -> a
succ (Integer -> Integer)
-> (TyVarInfoMap -> Integer) -> TyVarInfoMap -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Integer] -> Integer)
-> (TyVarInfoMap -> [Integer]) -> TyVarInfoMap -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer
n1Integer -> [Integer] -> [Integer]
forall a. a -> [a] -> [a]
:) ([Integer] -> [Integer])
-> (TyVarInfoMap -> [Integer]) -> TyVarInfoMap -> [Integer]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name Type] -> [Integer]
forall a. Alpha a => [a] -> [Integer]
fvNums ([Name Type] -> [Integer])
-> (TyVarInfoMap -> [Name Type]) -> TyVarInfoMap -> [Integer]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (Name Type) TyVarInfo -> [Name Type]
forall k a. Map k a -> [k]
M.keys (Map (Name Type) TyVarInfo -> [Name Type])
-> (TyVarInfoMap -> Map (Name Type) TyVarInfo)
-> TyVarInfoMap
-> [Name Type]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarInfoMap -> Map (Name Type) TyVarInfo
unVM (TyVarInfoMap -> Integer) -> TyVarInfoMap -> Integer
forall a b. (a -> b) -> a -> b
$ TyVarInfoMap
origVM
maximum0 :: [p] -> p
maximum0 [] = p
0
maximum0 [p]
xs = [p] -> p
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [p]
xs
extractAtoms :: SimpleConstraint -> (Atom, Atom)
extractAtoms :: SimpleConstraint -> (Atom, Atom)
extractAtoms (TyAtom Atom
a1 :<: TyAtom Atom
a2) = (Atom
a1, Atom
a2)
extractAtoms SimpleConstraint
c = String -> (Atom, Atom)
forall a. HasCallStack => String -> a
error (String -> (Atom, Atom)) -> String -> (Atom, Atom)
forall a b. (a -> b) -> a -> b
$ String
"Impossible: simplify left non-atomic or non-subtype constraint " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SimpleConstraint -> String
forall a. Show a => a -> String
show SimpleConstraint
c
simplify'
:: Members '[State SimplifyState, Fresh, Error SolveError, Output Message, Input TyDefCtx] r
=> Sem r ()
simplify' :: Sem r ()
simplify' = do
Maybe SimpleConstraint
mc <- Sem r (Maybe SimpleConstraint)
forall (r :: [(* -> *) -> * -> *]).
Members '[State SimplifyState, Fresh, Error SolveError] r =>
Sem r (Maybe SimpleConstraint)
pickSimplifiable
case Maybe SimpleConstraint
mc of
Maybe SimpleConstraint
Nothing -> () -> Sem r ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just SimpleConstraint
s -> do
Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug (Sem r Doc -> Sem r ()) -> Sem r Doc -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Sem r Doc
"Simplifying:" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> SimpleConstraint -> Sem r Doc
forall t (r :: [(* -> *) -> * -> *]). Pretty t => t -> Sem r Doc
pretty' SimpleConstraint
s
SimpleConstraint -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Members
'[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx]
r =>
SimpleConstraint -> Sem r ()
simplifyOne SimpleConstraint
s
Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Members
'[State SimplifyState, Fresh, Error SolveError, Output Message,
Input TyDefCtx]
r =>
Sem r ()
simplify'
pickSimplifiable
:: Members '[State SimplifyState, Fresh, Error SolveError] r
=> Sem r (Maybe SimpleConstraint)
pickSimplifiable :: Sem r (Maybe SimpleConstraint)
pickSimplifiable = do
[SimpleConstraint]
curCs <- Getter SimplifyState [SimpleConstraint] -> Sem r [SimpleConstraint]
forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Getter s a -> Sem r a
use Lens' SimplifyState [SimpleConstraint]
Getter SimplifyState [SimpleConstraint]
ssConstraints
case (SimpleConstraint -> Bool)
-> [SimpleConstraint]
-> Maybe (SimpleConstraint, [SimpleConstraint])
forall a. (a -> Bool) -> [a] -> Maybe (a, [a])
pick SimpleConstraint -> Bool
simplifiable [SimpleConstraint]
curCs of
Maybe (SimpleConstraint, [SimpleConstraint])
Nothing -> Maybe SimpleConstraint -> Sem r (Maybe SimpleConstraint)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe SimpleConstraint
forall a. Maybe a
Nothing
Just (SimpleConstraint
a,[SimpleConstraint]
as) -> do
Lens' SimplifyState [SimpleConstraint]
ssConstraints Lens' SimplifyState [SimpleConstraint]
-> [SimpleConstraint] -> Sem r ()
forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Lens' s a -> a -> Sem r ()
.= [SimpleConstraint]
as
Maybe SimpleConstraint -> Sem r (Maybe SimpleConstraint)
forall (m :: * -> *) a. Monad m => a -> m a
return (SimpleConstraint -> Maybe SimpleConstraint
forall a. a -> Maybe a
Just SimpleConstraint
a)
pick :: (a -> Bool) -> [a] -> Maybe (a,[a])
pick :: (a -> Bool) -> [a] -> Maybe (a, [a])
pick a -> Bool
_ [] = Maybe (a, [a])
forall a. Maybe a
Nothing
pick a -> Bool
p (a
a:[a]
as)
| a -> Bool
p a
a = (a, [a]) -> Maybe (a, [a])
forall a. a -> Maybe a
Just (a
a,[a]
as)
| Bool
otherwise = ([a] -> [a]) -> (a, [a]) -> (a, [a])
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (a
aa -> [a] -> [a]
forall a. a -> [a] -> [a]
:) ((a, [a]) -> (a, [a])) -> Maybe (a, [a]) -> Maybe (a, [a])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> Bool) -> [a] -> Maybe (a, [a])
forall a. (a -> Bool) -> [a] -> Maybe (a, [a])
pick a -> Bool
p [a]
as
simplifiable :: SimpleConstraint -> Bool
simplifiable :: SimpleConstraint -> Bool
simplifiable (Type
_ :=: Type
_) = Bool
True
simplifiable (TyCon {} :<: TyCon {}) = Bool
True
simplifiable (TyVar {} :<: TyCon {}) = Bool
True
simplifiable (TyCon {} :<: TyVar {}) = Bool
True
simplifiable (TyCon (CUser String
_) [Type]
_ :<: Type
_) = Bool
True
simplifiable (Type
_ :<: TyCon (CUser String
_) [Type]
_) = Bool
True
simplifiable (TyAtom (ABase BaseTy
_) :<: TyAtom (ABase BaseTy
_)) = Bool
True
simplifiable SimpleConstraint
_ = Bool
False
simplifyOne
:: Members '[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx] r
=> SimpleConstraint -> Sem r ()
simplifyOne :: SimpleConstraint -> Sem r ()
simplifyOne SimpleConstraint
c = do
Set SimpleConstraint
seen <- Getter SimplifyState (Set SimpleConstraint)
-> Sem r (Set SimpleConstraint)
forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Getter s a -> Sem r a
use Lens' SimplifyState (Set SimpleConstraint)
Getter SimplifyState (Set SimpleConstraint)
ssSeen
case SimpleConstraint
c SimpleConstraint -> Set SimpleConstraint -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set SimpleConstraint
seen of
Bool
True -> () -> Sem r ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Bool
False -> do
Lens' SimplifyState (Set SimpleConstraint)
ssSeen Lens' SimplifyState (Set SimpleConstraint)
-> (Set SimpleConstraint -> Set SimpleConstraint) -> Sem r ()
forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Lens' s a -> (a -> a) -> Sem r ()
%= SimpleConstraint -> Set SimpleConstraint -> Set SimpleConstraint
forall a. Ord a => a -> Set a -> Set a
S.insert SimpleConstraint
c
SimpleConstraint -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Members
'[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx]
r =>
SimpleConstraint -> Sem r ()
simplifyOne' SimpleConstraint
c
simplifyOne'
:: Members '[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx] r
=> SimpleConstraint -> Sem r ()
simplifyOne' :: SimpleConstraint -> Sem r ()
simplifyOne' (Type
ty1 :=: Type
ty2) = do
TyDefCtx
tyDefns <- forall (r :: [(* -> *) -> * -> *]).
Member (Input TyDefCtx) r =>
Sem r TyDefCtx
forall i (r :: [(* -> *) -> * -> *]). Member (Input i) r => Sem r i
input @TyDefCtx
case TyDefCtx -> [(Type, Type)] -> Maybe S
unify TyDefCtx
tyDefns [(Type
ty1, Type
ty2)] of
Maybe S
Nothing -> SolveError -> Sem r ()
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw SolveError
NoUnify
Just S
s' -> S -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Members
'[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx]
r =>
S -> Sem r ()
extendSubst S
s'
simplifyOne' (ty1 :: Type
ty1@(TyCon (CUser String
_) [Type]
_) :<: ty2 :: Type
ty2@TyVar{})
= SimpleConstraint -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Members
'[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx]
r =>
SimpleConstraint -> Sem r ()
simplifyOne' (Type
ty1 Type -> Type -> SimpleConstraint
:=: Type
ty2)
simplifyOne' (TyCon (CUser String
t) [Type]
ts :<: Type
ty2) = do
TyDefCtx
tyDefns <- forall (r :: [(* -> *) -> * -> *]).
Member (Input TyDefCtx) r =>
Sem r TyDefCtx
forall i (r :: [(* -> *) -> * -> *]). Member (Input i) r => Sem r i
input @TyDefCtx
case String -> TyDefCtx -> Maybe TyDefBody
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
t TyDefCtx
tyDefns of
Maybe TyDefBody
Nothing -> String -> Sem r ()
forall a. HasCallStack => String -> a
error (String -> Sem r ()) -> String -> Sem r ()
forall a b. (a -> b) -> a -> b
$ ShowS
forall a. Show a => a -> String
show String
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" not in ty defn map!"
Just (TyDefBody [String]
_ [Type] -> Type
body) ->
Lens' SimplifyState [SimpleConstraint]
ssConstraints Lens' SimplifyState [SimpleConstraint]
-> ([SimpleConstraint] -> [SimpleConstraint]) -> Sem r ()
forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Lens' s a -> (a -> a) -> Sem r ()
%= (([Type] -> Type
body [Type]
ts Type -> Type -> SimpleConstraint
:<: Type
ty2) SimpleConstraint -> [SimpleConstraint] -> [SimpleConstraint]
forall a. a -> [a] -> [a]
:)
simplifyOne' (ty1 :: Type
ty1@TyVar{} :<: ty2 :: Type
ty2@(TyCon (CUser String
_) [Type]
_))
= SimpleConstraint -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Members
'[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx]
r =>
SimpleConstraint -> Sem r ()
simplifyOne' (Type
ty1 Type -> Type -> SimpleConstraint
:=: Type
ty2)
simplifyOne' (Type
ty1 :<: TyCon (CUser String
t) [Type]
ts) = do
TyDefCtx
tyDefns <- forall (r :: [(* -> *) -> * -> *]).
Member (Input TyDefCtx) r =>
Sem r TyDefCtx
forall i (r :: [(* -> *) -> * -> *]). Member (Input i) r => Sem r i
input @TyDefCtx
case String -> TyDefCtx -> Maybe TyDefBody
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
t TyDefCtx
tyDefns of
Maybe TyDefBody
Nothing -> String -> Sem r ()
forall a. HasCallStack => String -> a
error (String -> Sem r ()) -> String -> Sem r ()
forall a b. (a -> b) -> a -> b
$ ShowS
forall a. Show a => a -> String
show String
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" not in ty defn map!"
Just (TyDefBody [String]
_ [Type] -> Type
body) ->
Lens' SimplifyState [SimpleConstraint]
ssConstraints Lens' SimplifyState [SimpleConstraint]
-> ([SimpleConstraint] -> [SimpleConstraint]) -> Sem r ()
forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Lens' s a -> (a -> a) -> Sem r ()
%= ((Type
ty1 Type -> Type -> SimpleConstraint
:<: [Type] -> Type
body [Type]
ts) SimpleConstraint -> [SimpleConstraint] -> [SimpleConstraint]
forall a. a -> [a] -> [a]
:)
simplifyOne' (TyCon c1 :: Con
c1@(CContainer Atom
ctr1) [Type]
tys1 :<: TyCon (CContainer Atom
ctr2) [Type]
tys2) =
Lens' SimplifyState [SimpleConstraint]
ssConstraints Lens' SimplifyState [SimpleConstraint]
-> ([SimpleConstraint] -> [SimpleConstraint]) -> Sem r ()
forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Lens' s a -> (a -> a) -> Sem r ()
%=
(( (Atom -> Type
TyAtom Atom
ctr1 Type -> Type -> SimpleConstraint
:<: Atom -> Type
TyAtom Atom
ctr2)
SimpleConstraint -> [SimpleConstraint] -> [SimpleConstraint]
forall a. a -> [a] -> [a]
: (Variance -> Type -> Type -> SimpleConstraint)
-> [Variance] -> [Type] -> [Type] -> [SimpleConstraint]
forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 Variance -> Type -> Type -> SimpleConstraint
variance (Con -> [Variance]
arity Con
c1) [Type]
tys1 [Type]
tys2
)
[SimpleConstraint] -> [SimpleConstraint] -> [SimpleConstraint]
forall a. [a] -> [a] -> [a]
++)
simplifyOne' (TyCon Con
c1 [Type]
tys1 :<: TyCon Con
c2 [Type]
tys2)
| Con
c1 Con -> Con -> Bool
forall a. Eq a => a -> a -> Bool
/= Con
c2 = SolveError -> Sem r ()
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw SolveError
NoUnify
| Bool
otherwise =
Lens' SimplifyState [SimpleConstraint]
ssConstraints Lens' SimplifyState [SimpleConstraint]
-> ([SimpleConstraint] -> [SimpleConstraint]) -> Sem r ()
forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Lens' s a -> (a -> a) -> Sem r ()
%= ((Variance -> Type -> Type -> SimpleConstraint)
-> [Variance] -> [Type] -> [Type] -> [SimpleConstraint]
forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 Variance -> Type -> Type -> SimpleConstraint
variance (Con -> [Variance]
arity Con
c1) [Type]
tys1 [Type]
tys2 [SimpleConstraint] -> [SimpleConstraint] -> [SimpleConstraint]
forall a. [a] -> [a] -> [a]
++)
simplifyOne' con :: SimpleConstraint
con@(TyVar Name Type
a :<: TyCon Con
c [Type]
_) = Name Type -> Con -> SimpleConstraint -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Members
'[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx]
r =>
Name Type -> Con -> SimpleConstraint -> Sem r ()
expandStruct Name Type
a Con
c SimpleConstraint
con
simplifyOne' con :: SimpleConstraint
con@(TyCon Con
c [Type]
_ :<: TyVar Name Type
a ) = Name Type -> Con -> SimpleConstraint -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Members
'[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx]
r =>
Name Type -> Con -> SimpleConstraint -> Sem r ()
expandStruct Name Type
a Con
c SimpleConstraint
con
simplifyOne' (TyAtom (ABase BaseTy
b1) :<: TyAtom (ABase BaseTy
b2)) = do
case BaseTy -> BaseTy -> Bool
isSubB BaseTy
b1 BaseTy
b2 of
Bool
True -> () -> Sem r ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Bool
False -> SolveError -> Sem r ()
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw SolveError
NoUnify
simplifyOne' (Type
s :<: Type
t) =
String -> Sem r ()
forall a. HasCallStack => String -> a
error (String -> Sem r ()) -> String -> Sem r ()
forall a b. (a -> b) -> a -> b
$ String
"Impossible! simplifyOne' " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" :<: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
t
expandStruct
:: Members '[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx] r
=> Name Type -> Con -> SimpleConstraint -> Sem r ()
expandStruct :: Name Type -> Con -> SimpleConstraint -> Sem r ()
expandStruct Name Type
a Con
c SimpleConstraint
con = do
[Type]
as <- (Variance -> Sem r Type) -> [Variance] -> Sem r [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Sem r Type -> Variance -> Sem r Type
forall a b. a -> b -> a
const (Name Type -> Type
TyVar (Name Type -> Type) -> Sem r (Name Type) -> Sem r Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name Type -> Sem r (Name Type)
forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh (String -> Name Type
forall a. String -> Name a
string2Name String
"a"))) (Con -> [Variance]
arity Con
c)
let s' :: S
s' = Name Type
a Name Type -> Type -> S
forall a. Name a -> a -> Substitution a
|-> Con -> [Type] -> Type
TyCon Con
c [Type]
as
Lens' SimplifyState [SimpleConstraint]
ssConstraints Lens' SimplifyState [SimpleConstraint]
-> ([SimpleConstraint] -> [SimpleConstraint]) -> Sem r ()
forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Lens' s a -> (a -> a) -> Sem r ()
%= (SimpleConstraint
conSimpleConstraint -> [SimpleConstraint] -> [SimpleConstraint]
forall a. a -> [a] -> [a]
:)
S -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Members
'[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx]
r =>
S -> Sem r ()
extendSubst S
s'
extendSubst
:: Members '[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx] r
=> S -> Sem r ()
extendSubst :: S -> Sem r ()
extendSubst S
s' = do
Lens' SimplifyState S
ssSubst Lens' SimplifyState S -> (S -> S) -> Sem r ()
forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Lens' s a -> (a -> a) -> Sem r ()
%= (S
s'S -> S -> S
forall a.
Subst a a =>
Substitution a -> Substitution a -> Substitution a
@@)
Lens' SimplifyState [SimpleConstraint]
ssConstraints Lens' SimplifyState [SimpleConstraint]
-> ([SimpleConstraint] -> [SimpleConstraint]) -> Sem r ()
forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Lens' s a -> (a -> a) -> Sem r ()
%= S -> [SimpleConstraint] -> [SimpleConstraint]
forall b a. Subst b a => Substitution b -> a -> a
applySubst S
s'
S -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Members
'[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx]
r =>
S -> Sem r ()
substVarMap S
s'
substVarMap
:: Members '[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx] r
=> S -> Sem r ()
substVarMap :: S -> Sem r ()
substVarMap S
s' = do
TyVarInfoMap
vm <- Getter SimplifyState TyVarInfoMap -> Sem r TyVarInfoMap
forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Getter s a -> Sem r a
use Lens' SimplifyState TyVarInfoMap
Getter SimplifyState TyVarInfoMap
ssVarMap
let tySorts :: [(Type, Sort)]
tySorts :: [(Type, Sort)]
tySorts = ((Type, TyVarInfo) -> (Type, Sort))
-> [(Type, TyVarInfo)] -> [(Type, Sort)]
forall a b. (a -> b) -> [a] -> [b]
map ((TyVarInfo -> Sort) -> (Type, TyVarInfo) -> (Type, Sort)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (Getting Sort TyVarInfo Sort -> TyVarInfo -> Sort
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Sort TyVarInfo Sort
Lens' TyVarInfo Sort
tyVarSort)) ([(Type, TyVarInfo)] -> [(Type, Sort)])
-> ([(Name Type, Type)] -> [(Type, TyVarInfo)])
-> [(Name Type, Type)]
-> [(Type, Sort)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Name Type, Type) -> Maybe (Type, TyVarInfo))
-> [(Name Type, Type)] -> [(Type, TyVarInfo)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ((Name Type -> Maybe TyVarInfo)
-> (Type, Name Type) -> Maybe (Type, TyVarInfo)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Name Type -> TyVarInfoMap -> Maybe TyVarInfo
`lookupVM` TyVarInfoMap
vm) ((Type, Name Type) -> Maybe (Type, TyVarInfo))
-> ((Name Type, Type) -> (Type, Name Type))
-> (Name Type, Type)
-> Maybe (Type, TyVarInfo)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name Type, Type) -> (Type, Name Type)
forall a b. (a, b) -> (b, a)
swap) ([(Name Type, Type)] -> [(Type, Sort)])
-> [(Name Type, Type)] -> [(Type, Sort)]
forall a b. (a -> b) -> a -> b
$ S -> [(Name Type, Type)]
forall a. Substitution a -> [(Name a, a)]
Subst.toList S
s'
tyQualList :: [(Type, Qualifier)]
tyQualList :: [(Type, Qualifier)]
tyQualList = ((Type, Sort) -> [(Type, Qualifier)])
-> [(Type, Sort)] -> [(Type, Qualifier)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((Type, [Qualifier]) -> [(Type, Qualifier)]
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA ((Type, [Qualifier]) -> [(Type, Qualifier)])
-> ((Type, Sort) -> (Type, [Qualifier]))
-> (Type, Sort)
-> [(Type, Qualifier)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Sort -> [Qualifier]) -> (Type, Sort) -> (Type, [Qualifier])
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second Sort -> [Qualifier]
forall a. Set a -> [a]
S.toList) [(Type, Sort)]
tySorts
TyVarInfoMap
vm' <- [TyVarInfoMap] -> TyVarInfoMap
forall a. Monoid a => [a] -> a
mconcat ([TyVarInfoMap] -> TyVarInfoMap)
-> Sem r [TyVarInfoMap] -> Sem r TyVarInfoMap
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Type, Qualifier) -> Sem r TyVarInfoMap)
-> [(Type, Qualifier)] -> Sem r [TyVarInfoMap]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Type -> Qualifier -> Sem r TyVarInfoMap)
-> (Type, Qualifier) -> Sem r TyVarInfoMap
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Type -> Qualifier -> Sem r TyVarInfoMap
forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Type -> Qualifier -> Sem r TyVarInfoMap
decomposeQual) [(Type, Qualifier)]
tyQualList
Lens' SimplifyState TyVarInfoMap
ssVarMap Lens' SimplifyState TyVarInfoMap -> TyVarInfoMap -> Sem r ()
forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Lens' s a -> a -> Sem r ()
.= TyVarInfoMap
vm' TyVarInfoMap -> TyVarInfoMap -> TyVarInfoMap
forall a. Semigroup a => a -> a -> a
<> (TyVarInfoMap -> Name Type -> TyVarInfoMap)
-> TyVarInfoMap -> Set (Name Type) -> TyVarInfoMap
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ((Name Type -> TyVarInfoMap -> TyVarInfoMap)
-> TyVarInfoMap -> Name Type -> TyVarInfoMap
forall a b c. (a -> b -> c) -> b -> a -> c
flip Name Type -> TyVarInfoMap -> TyVarInfoMap
deleteVM) TyVarInfoMap
vm (S -> Set (Name Type)
forall a. Substitution a -> Set (Name a)
dom S
s')
variance :: Variance -> Type -> Type -> SimpleConstraint
variance Variance
Co Type
ty1 Type
ty2 = Type
ty1 Type -> Type -> SimpleConstraint
:<: Type
ty2
variance Variance
Contra Type
ty1 Type
ty2 = Type
ty2 Type -> Type -> SimpleConstraint
:<: Type
ty1
mkConstraintGraph :: (Show a, Ord a) => Set a -> [(a, a)] -> Graph a
mkConstraintGraph :: Set a -> [(a, a)] -> Graph a
mkConstraintGraph Set a
as [(a, a)]
cs = Set a -> Set (a, a) -> Graph a
forall a. (Show a, Ord a) => Set a -> Set (a, a) -> Graph a
G.mkGraph Set a
nodes ([(a, a)] -> Set (a, a)
forall a. Ord a => [a] -> Set a
S.fromList [(a, a)]
cs)
where
nodes :: Set a
nodes = Set a
as Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
`S.union` [a] -> Set a
forall a. Ord a => [a] -> Set a
S.fromList ([(a, a)]
cs [(a, a)] -> Getting (Endo [a]) [(a, a)] a -> [a]
forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. ((a, a) -> Const (Endo [a]) (a, a))
-> [(a, a)] -> Const (Endo [a]) [(a, a)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (((a, a) -> Const (Endo [a]) (a, a))
-> [(a, a)] -> Const (Endo [a]) [(a, a)])
-> ((a -> Const (Endo [a]) a) -> (a, a) -> Const (Endo [a]) (a, a))
-> Getting (Endo [a]) [(a, a)] a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Const (Endo [a]) a) -> (a, a) -> Const (Endo [a]) (a, a)
forall s t a b. Each s t a b => Traversal s t a b
each)
checkSkolems
:: Members '[Error SolveError, Output Message, Input TyDefCtx] r
=> TyVarInfoMap -> Graph Atom -> Sem r (Graph UAtom, S)
checkSkolems :: TyVarInfoMap -> Graph Atom -> Sem r (Graph UAtom, S)
checkSkolems TyVarInfoMap
vm Graph Atom
graph = do
let skolemWCCs :: [Set Atom]
skolemWCCs :: [Set Atom]
skolemWCCs = (Set Atom -> Bool) -> [Set Atom] -> [Set Atom]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Atom -> Bool) -> Set Atom -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Atom -> Bool
isSkolem) ([Set Atom] -> [Set Atom]) -> [Set Atom] -> [Set Atom]
forall a b. (a -> b) -> a -> b
$ Graph Atom -> [Set Atom]
forall a. Ord a => Graph a -> [Set a]
G.wcc Graph Atom
graph
ok :: Set Atom -> Bool
ok Set Atom
wcc = Set Atom -> Int
forall a. Set a -> Int
S.size ((Atom -> Bool) -> Set Atom -> Set Atom
forall a. (a -> Bool) -> Set a -> Set a
S.filter Atom -> Bool
isSkolem Set Atom
wcc) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1
Bool -> Bool -> Bool
&& (Atom -> Bool) -> Set Atom -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\case { ABase BaseTy
_ -> Bool
False
; AVar (S Name Type
_) -> Bool
True
; AVar (U Name Type
v) -> Bool -> (TyVarInfo -> Bool) -> Maybe TyVarInfo -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (Sort -> Bool
forall a. Set a -> Bool
S.null (Sort -> Bool) -> (TyVarInfo -> Sort) -> TyVarInfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting Sort TyVarInfo Sort -> TyVarInfo -> Sort
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Sort TyVarInfo Sort
Lens' TyVarInfo Sort
tyVarSort) (Name Type -> TyVarInfoMap -> Maybe TyVarInfo
lookupVM Name Type
v TyVarInfoMap
vm) })
Set Atom
wcc
([Set Atom]
good, [Set Atom]
bad) = (Set Atom -> Bool) -> [Set Atom] -> ([Set Atom], [Set Atom])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Set Atom -> Bool
ok [Set Atom]
skolemWCCs
Bool -> Sem r () -> Sem r ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Set Atom] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Set Atom]
bad) (Sem r () -> Sem r ()) -> Sem r () -> Sem r ()
forall a b. (a -> b) -> a -> b
$ SolveError -> Sem r ()
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw SolveError
NoUnify
Graph Atom -> S -> [Set Atom] -> Sem r (Graph UAtom, S)
forall (r :: [(* -> *) -> * -> *]).
Members '[Error SolveError, Output Message, Input TyDefCtx] r =>
Graph Atom -> S -> [Set Atom] -> Sem r (Graph UAtom, S)
unifyWCCs Graph Atom
graph S
forall a. Substitution a
idS [Set Atom]
good
where
noSkolems :: Atom -> UAtom
noSkolems :: Atom -> UAtom
noSkolems (ABase BaseTy
b) = BaseTy -> UAtom
UB BaseTy
b
noSkolems (AVar (U Name Type
v)) = Name Type -> UAtom
UV Name Type
v
noSkolems (AVar (S Name Type
v)) = String -> UAtom
forall a. HasCallStack => String -> a
error (String -> UAtom) -> String -> UAtom
forall a b. (a -> b) -> a -> b
$ String
"Skolem " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name Type -> String
forall a. Show a => a -> String
show Name Type
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" remaining in noSkolems"
unifyWCCs
:: Members '[Error SolveError, Output Message, Input TyDefCtx] r
=> Graph Atom -> S -> [Set Atom] -> Sem r (Graph UAtom, S)
unifyWCCs :: Graph Atom -> S -> [Set Atom] -> Sem r (Graph UAtom, S)
unifyWCCs Graph Atom
g S
s [] = (Graph UAtom, S) -> Sem r (Graph UAtom, S)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Atom -> UAtom) -> Graph Atom -> Graph UAtom
forall b a. Ord b => (a -> b) -> Graph a -> Graph b
G.map Atom -> UAtom
noSkolems Graph Atom
g, S
s)
unifyWCCs Graph Atom
g S
s (Set Atom
u:[Set Atom]
us) = do
Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug (Sem r Doc -> Sem r ()) -> Sem r Doc -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Sem r Doc
"Unifying" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> [Set Atom] -> Sem r Doc
forall t (r :: [(* -> *) -> * -> *]). Pretty t => t -> Sem r Doc
pretty' (Set Atom
uSet Atom -> [Set Atom] -> [Set Atom]
forall a. a -> [a] -> [a]
:[Set Atom]
us) Sem r Doc -> Sem r Doc -> Sem r Doc
forall a. Semigroup a => a -> a -> a
<> Sem r Doc
"..."
TyDefCtx
tyDefns <- forall (r :: [(* -> *) -> * -> *]).
Member (Input TyDefCtx) r =>
Sem r TyDefCtx
forall i (r :: [(* -> *) -> * -> *]). Member (Input i) r => Sem r i
input @TyDefCtx
let g' :: Graph Atom
g' = (Graph Atom -> Atom -> Graph Atom)
-> Graph Atom -> Set Atom -> Graph Atom
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ((Atom -> Graph Atom -> Graph Atom)
-> Graph Atom -> Atom -> Graph Atom
forall a b c. (a -> b -> c) -> b -> a -> c
flip Atom -> Graph Atom -> Graph Atom
forall a. (Show a, Ord a) => a -> Graph a -> Graph a
G.delete) Graph Atom
g Set Atom
u
ms' :: Maybe (Substitution Atom)
ms' = TyDefCtx -> [Atom] -> Maybe (Substitution Atom)
unifyAtoms TyDefCtx
tyDefns (Set Atom -> [Atom]
forall a. Set a -> [a]
S.toList Set Atom
u)
case Maybe (Substitution Atom)
ms' of
Maybe (Substitution Atom)
Nothing -> SolveError -> Sem r (Graph UAtom, S)
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw SolveError
NoUnify
Just Substitution Atom
s' -> Graph Atom -> S -> [Set Atom] -> Sem r (Graph UAtom, S)
forall (r :: [(* -> *) -> * -> *]).
Members '[Error SolveError, Output Message, Input TyDefCtx] r =>
Graph Atom -> S -> [Set Atom] -> Sem r (Graph UAtom, S)
unifyWCCs Graph Atom
g' (Substitution Atom -> S
atomToTypeSubst Substitution Atom
s' S -> S -> S
forall a.
Subst a a =>
Substitution a -> Substitution a -> Substitution a
@@ S
s) [Set Atom]
us
elimCycles
:: Members '[Error SolveError] r
=> TyDefCtx -> Graph UAtom -> Sem r (Graph UAtom, S)
elimCycles :: TyDefCtx -> Graph UAtom -> Sem r (Graph UAtom, S)
elimCycles TyDefCtx
tyDefns = (Substitution UAtom -> S)
-> ([UAtom] -> Maybe (Substitution UAtom))
-> Graph UAtom
-> Sem r (Graph UAtom, S)
forall a b (r :: [(* -> *) -> * -> *]).
(Subst a a, Ord a, Members '[Error SolveError] r) =>
(Substitution a -> Substitution b)
-> ([a] -> Maybe (Substitution a))
-> Graph a
-> Sem r (Graph a, Substitution b)
elimCyclesGen Substitution UAtom -> S
uatomToTypeSubst (TyDefCtx -> [UAtom] -> Maybe (Substitution UAtom)
unifyUAtoms TyDefCtx
tyDefns)
elimCyclesGen
:: forall a b r. (Subst a a, Ord a, Members '[Error SolveError] r)
=> (Substitution a -> Substitution b) -> ([a] -> Maybe (Substitution a))
-> Graph a -> Sem r (Graph a, Substitution b)
elimCyclesGen :: (Substitution a -> Substitution b)
-> ([a] -> Maybe (Substitution a))
-> Graph a
-> Sem r (Graph a, Substitution b)
elimCyclesGen Substitution a -> Substitution b
genSubst [a] -> Maybe (Substitution a)
genUnify Graph a
g
= SolveError
-> Maybe (Graph a, Substitution b)
-> Sem r (Graph a, Substitution b)
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Maybe a -> Sem r a
note SolveError
NoUnify
(Maybe (Graph a, Substitution b)
-> Sem r (Graph a, Substitution b))
-> Maybe (Graph a, Substitution b)
-> Sem r (Graph a, Substitution b)
forall a b. (a -> b) -> a -> b
$ (((a, Substitution a) -> a) -> Graph (a, Substitution a) -> Graph a
forall b a. Ord b => (a -> b) -> Graph a -> Graph b
G.map (a, Substitution a) -> a
forall a b. (a, b) -> a
fst (Graph (a, Substitution a) -> Graph a)
-> (Graph (a, Substitution a) -> Substitution b)
-> Graph (a, Substitution a)
-> (Graph a, Substitution b)
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& (Substitution a -> Substitution b
genSubst (Substitution a -> Substitution b)
-> (Graph (a, Substitution a) -> Substitution a)
-> Graph (a, Substitution a)
-> Substitution b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (Substitution a) -> Substitution a
forall a (t :: * -> *).
(Subst a a, Foldable t) =>
t (Substitution a) -> Substitution a
compose (Set (Substitution a) -> Substitution a)
-> (Graph (a, Substitution a) -> Set (Substitution a))
-> Graph (a, Substitution a)
-> Substitution a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a, Substitution a) -> Substitution a)
-> Set (a, Substitution a) -> Set (Substitution a)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (a, Substitution a) -> Substitution a
forall a b. (a, b) -> b
snd (Set (a, Substitution a) -> Set (Substitution a))
-> (Graph (a, Substitution a) -> Set (a, Substitution a))
-> Graph (a, Substitution a)
-> Set (Substitution a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Graph (a, Substitution a) -> Set (a, Substitution a)
forall a. Graph a -> Set a
G.nodes)) (Graph (a, Substitution a) -> (Graph a, Substitution b))
-> Maybe (Graph (a, Substitution a))
-> Maybe (Graph a, Substitution b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Graph (a, Substitution a))
g'
where
g' :: Maybe (Graph (a, Substitution a))
g' :: Maybe (Graph (a, Substitution a))
g' = Graph (Maybe (a, Substitution a))
-> Maybe (Graph (a, Substitution a))
forall a. Ord a => Graph (Maybe a) -> Maybe (Graph a)
G.sequenceGraph (Graph (Maybe (a, Substitution a))
-> Maybe (Graph (a, Substitution a)))
-> Graph (Maybe (a, Substitution a))
-> Maybe (Graph (a, Substitution a))
forall a b. (a -> b) -> a -> b
$ (Set a -> Maybe (a, Substitution a))
-> Graph (Set a) -> Graph (Maybe (a, Substitution a))
forall b a. Ord b => (a -> b) -> Graph a -> Graph b
G.map Set a -> Maybe (a, Substitution a)
unifySCC (Graph a -> Graph (Set a)
forall a. Ord a => Graph a -> Graph (Set a)
G.condensation Graph a
g)
unifySCC :: Set a -> Maybe (a, Substitution a)
unifySCC :: Set a -> Maybe (a, Substitution a)
unifySCC Set a
uatoms = case Set a -> [a]
forall a. Set a -> [a]
S.toList Set a
uatoms of
[] -> String -> Maybe (a, Substitution a)
forall a. HasCallStack => String -> a
error String
"Impossible! unifySCC on the empty set"
as :: [a]
as@(a
a:[a]
_) -> ((Substitution a -> a -> a) -> a -> Substitution a -> a
forall a b c. (a -> b -> c) -> b -> a -> c
flip Substitution a -> a -> a
forall b a. Subst b a => Substitution b -> a -> a
applySubst a
a (Substitution a -> a)
-> (Substitution a -> Substitution a)
-> Substitution a
-> (a, Substitution a)
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& Substitution a -> Substitution a
forall a. a -> a
id) (Substitution a -> (a, Substitution a))
-> Maybe (Substitution a) -> Maybe (a, Substitution a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a] -> Maybe (Substitution a)
genUnify [a]
as
data Rels = Rels
{ Rels -> Set BaseTy
baseRels :: Set BaseTy
, Rels -> Set (Name Type)
varRels :: Set (Name Type)
}
deriving (Int -> Rels -> ShowS
[Rels] -> ShowS
Rels -> String
(Int -> Rels -> ShowS)
-> (Rels -> String) -> ([Rels] -> ShowS) -> Show Rels
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Rels] -> ShowS
$cshowList :: [Rels] -> ShowS
show :: Rels -> String
$cshow :: Rels -> String
showsPrec :: Int -> Rels -> ShowS
$cshowsPrec :: Int -> Rels -> ShowS
Show, Rels -> Rels -> Bool
(Rels -> Rels -> Bool) -> (Rels -> Rels -> Bool) -> Eq Rels
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Rels -> Rels -> Bool
$c/= :: Rels -> Rels -> Bool
== :: Rels -> Rels -> Bool
$c== :: Rels -> Rels -> Bool
Eq)
newtype RelMap = RelMap { RelMap -> Map (Name Type, Dir) Rels
unRelMap :: Map (Name Type, Dir) Rels}
instance Pretty RelMap where
pretty :: RelMap -> Sem r Doc
pretty (RelMap Map (Name Type, Dir) Rels
rm) = [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
vcat (((Rels, Name Type, Rels) -> Sem r Doc)
-> [(Rels, Name Type, Rels)] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Rels, Name Type, Rels) -> Sem r Doc
forall (r :: [(* -> *) -> * -> *]) t.
(Member (Reader PA) r, Member LFresh r, Pretty t) =>
(Rels, t, Rels) -> Sem r Doc
prettyVar [(Rels, Name Type, Rels)]
byVar)
where
vars :: Set (Name Type)
vars = ((Name Type, Dir) -> Name Type)
-> Set (Name Type, Dir) -> Set (Name Type)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (Name Type, Dir) -> Name Type
forall a b. (a, b) -> a
fst (Map (Name Type, Dir) Rels -> Set (Name Type, Dir)
forall k a. Map k a -> Set k
M.keysSet Map (Name Type, Dir) Rels
rm)
byVar :: [(Rels, Name Type, Rels)]
byVar = (Name Type -> (Rels, Name Type, Rels))
-> [Name Type] -> [(Rels, Name Type, Rels)]
forall a b. (a -> b) -> [a] -> [b]
map (\Name Type
x -> (Map (Name Type, Dir) Rels
rmMap (Name Type, Dir) Rels -> (Name Type, Dir) -> Rels
forall k a. Ord k => Map k a -> k -> a
!(Name Type
x,Dir
SubTy), Name Type
x, Map (Name Type, Dir) Rels
rmMap (Name Type, Dir) Rels -> (Name Type, Dir) -> Rels
forall k a. Ord k => Map k a -> k -> a
!(Name Type
x,Dir
SuperTy))) (Set (Name Type) -> [Name Type]
forall a. Set a -> [a]
S.toList Set (Name Type)
vars)
prettyVar :: (Rels, t, Rels) -> Sem r Doc
prettyVar (Rels
subs, t
x, Rels
sups) = [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep [Rels -> Sem r Doc
forall (r :: [(* -> *) -> * -> *]).
(Member (Reader PA) r, Member LFresh r) =>
Rels -> Sem r Doc
prettyRel Rels
subs, Sem r Doc
"<:", t -> Sem r Doc
forall t (r :: [(* -> *) -> * -> *]).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty t
x, Sem r Doc
"<:", Rels -> Sem r Doc
forall (r :: [(* -> *) -> * -> *]).
(Member (Reader PA) r, Member LFresh r) =>
Rels -> Sem r Doc
prettyRel Rels
sups]
prettyRel :: Rels -> Sem r Doc
prettyRel Rels
rs = Set BaseTy -> Sem r Doc
forall t (r :: [(* -> *) -> * -> *]).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty (Rels -> Set BaseTy
baseRels Rels
rs) Sem r Doc -> Sem r Doc -> Sem r Doc
forall a. Semigroup a => a -> a -> a
<> Sem r Doc
", " Sem r Doc -> Sem r Doc -> Sem r Doc
forall a. Semigroup a => a -> a -> a
<> Set (Name Type) -> Sem r Doc
forall t (r :: [(* -> *) -> * -> *]).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty (Rels -> Set (Name Type)
varRels Rels
rs)
substRel :: Name Type -> BaseTy -> RelMap -> RelMap
substRel :: Name Type -> BaseTy -> RelMap -> RelMap
substRel Name Type
x BaseTy
ty
= Map (Name Type, Dir) Rels -> RelMap
RelMap
(Map (Name Type, Dir) Rels -> RelMap)
-> (RelMap -> Map (Name Type, Dir) Rels) -> RelMap -> RelMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name Type, Dir)
-> Map (Name Type, Dir) Rels -> Map (Name Type, Dir) Rels
forall k a. Ord k => k -> Map k a -> Map k a
M.delete (Name Type
x,Dir
SuperTy)
(Map (Name Type, Dir) Rels -> Map (Name Type, Dir) Rels)
-> (RelMap -> Map (Name Type, Dir) Rels)
-> RelMap
-> Map (Name Type, Dir) Rels
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name Type, Dir)
-> Map (Name Type, Dir) Rels -> Map (Name Type, Dir) Rels
forall k a. Ord k => k -> Map k a -> Map k a
M.delete (Name Type
x,Dir
SubTy)
(Map (Name Type, Dir) Rels -> Map (Name Type, Dir) Rels)
-> (RelMap -> Map (Name Type, Dir) Rels)
-> RelMap
-> Map (Name Type, Dir) Rels
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rels -> Rels)
-> Map (Name Type, Dir) Rels -> Map (Name Type, Dir) Rels
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (\r :: Rels
r@(Rels Set BaseTy
b Set (Name Type)
v) -> if Name Type
x Name Type -> Set (Name Type) -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set (Name Type)
v then Set BaseTy -> Set (Name Type) -> Rels
Rels (BaseTy -> Set BaseTy -> Set BaseTy
forall a. Ord a => a -> Set a -> Set a
S.insert BaseTy
ty Set BaseTy
b) (Name Type -> Set (Name Type) -> Set (Name Type)
forall a. Ord a => a -> Set a -> Set a
S.delete Name Type
x Set (Name Type)
v) else Rels
r)
(Map (Name Type, Dir) Rels -> Map (Name Type, Dir) Rels)
-> (RelMap -> Map (Name Type, Dir) Rels)
-> RelMap
-> Map (Name Type, Dir) Rels
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RelMap -> Map (Name Type, Dir) Rels
unRelMap
dirtypesBySort :: TyVarInfoMap -> RelMap -> Dir -> BaseTy -> Sort -> Set (Name Type) -> [BaseTy]
dirtypesBySort :: TyVarInfoMap
-> RelMap -> Dir -> BaseTy -> Sort -> Set (Name Type) -> [BaseTy]
dirtypesBySort TyVarInfoMap
vm (RelMap Map (Name Type, Dir) Rels
relMap) Dir
dir BaseTy
t Sort
s Set (Name Type)
x
= [BaseTy] -> (BaseTy -> Bool) -> [BaseTy]
forall a. [a] -> (a -> Bool) -> [a]
keep (Dir -> BaseTy -> [BaseTy]
dirtypes Dir
dir BaseTy
t) ((BaseTy -> Bool) -> [BaseTy]) -> (BaseTy -> Bool) -> [BaseTy]
forall a b. (a -> b) -> a -> b
$ \BaseTy
t' ->
BaseTy -> Sort -> Bool
hasSort BaseTy
t' Sort
s Bool -> Bool -> Bool
&&
Set (Name Type) -> (Name Type -> Bool) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> (a -> Bool) -> Bool
forAll Set (Name Type)
x (\Name Type
beta ->
[BaseTy] -> (BaseTy -> Bool) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> (a -> Bool) -> Bool
exists (Dir -> BaseTy -> [BaseTy]
dirtypes (Dir -> Dir
other Dir
dir) BaseTy
t') ((BaseTy -> Bool) -> Bool) -> (BaseTy -> Bool) -> Bool
forall a b. (a -> b) -> a -> b
$ \BaseTy
t'' ->
BaseTy -> Sort -> Bool
hasSort BaseTy
t'' (TyVarInfoMap -> Name Type -> Sort
getSort TyVarInfoMap
vm Name Type
beta) Bool -> Bool -> Bool
&&
Set BaseTy -> (BaseTy -> Bool) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> (a -> Bool) -> Bool
forAll (Rels -> Set BaseTy
baseRels (String -> Map (Name Type, Dir) Rels -> (Name Type, Dir) -> Rels
forall k a.
(Ord k, Show k, Show (Map k a)) =>
String -> Map k a -> k -> a
lkup String
"dirtypesBySort, beta rel" Map (Name Type, Dir) Rels
relMap (Name Type
beta, Dir -> Dir
other Dir
dir)))
(Dir -> BaseTy -> BaseTy -> Bool
isDirB Dir
dir BaseTy
t''))
where
forAll, exists :: Foldable t => t a -> (a -> Bool) -> Bool
forAll :: t a -> (a -> Bool) -> Bool
forAll = ((a -> Bool) -> t a -> Bool) -> t a -> (a -> Bool) -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> Bool) -> t a -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all
exists :: t a -> (a -> Bool) -> Bool
exists = ((a -> Bool) -> t a -> Bool) -> t a -> (a -> Bool) -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> Bool) -> t a -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any
keep :: [a] -> (a -> Bool) -> [a]
keep = ((a -> Bool) -> [a] -> [a]) -> [a] -> (a -> Bool) -> [a]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
filter
limBySort :: TyVarInfoMap -> RelMap -> Dir -> [BaseTy] -> Sort -> Set (Name Type) -> Maybe BaseTy
limBySort :: TyVarInfoMap
-> RelMap
-> Dir
-> [BaseTy]
-> Sort
-> Set (Name Type)
-> Maybe BaseTy
limBySort TyVarInfoMap
vm RelMap
rm Dir
dir [BaseTy]
ts Sort
s Set (Name Type)
x
= (\[BaseTy]
is -> (BaseTy -> Bool) -> [BaseTy] -> Maybe BaseTy
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\BaseTy
lim -> (BaseTy -> Bool) -> [BaseTy] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\BaseTy
u -> Dir -> BaseTy -> BaseTy -> Bool
isDirB Dir
dir BaseTy
u BaseTy
lim) [BaseTy]
is) [BaseTy]
is)
([BaseTy] -> Maybe BaseTy)
-> ([BaseTy] -> [BaseTy]) -> [BaseTy] -> Maybe BaseTy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[BaseTy]] -> [BaseTy]
isects
([[BaseTy]] -> [BaseTy])
-> ([BaseTy] -> [[BaseTy]]) -> [BaseTy] -> [BaseTy]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (BaseTy -> [BaseTy]) -> [BaseTy] -> [[BaseTy]]
forall a b. (a -> b) -> [a] -> [b]
map (\BaseTy
t -> TyVarInfoMap
-> RelMap -> Dir -> BaseTy -> Sort -> Set (Name Type) -> [BaseTy]
dirtypesBySort TyVarInfoMap
vm RelMap
rm Dir
dir BaseTy
t Sort
s Set (Name Type)
x)
([BaseTy] -> Maybe BaseTy) -> [BaseTy] -> Maybe BaseTy
forall a b. (a -> b) -> a -> b
$ [BaseTy]
ts
where
isects :: [[BaseTy]] -> [BaseTy]
isects = ([BaseTy] -> [BaseTy] -> [BaseTy]) -> [[BaseTy]] -> [BaseTy]
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 [BaseTy] -> [BaseTy] -> [BaseTy]
forall a. Eq a => [a] -> [a] -> [a]
intersect
lubBySort, glbBySort :: TyVarInfoMap -> RelMap -> [BaseTy] -> Sort -> Set (Name Type) -> Maybe BaseTy
lubBySort :: TyVarInfoMap
-> RelMap -> [BaseTy] -> Sort -> Set (Name Type) -> Maybe BaseTy
lubBySort TyVarInfoMap
vm RelMap
rm = TyVarInfoMap
-> RelMap
-> Dir
-> [BaseTy]
-> Sort
-> Set (Name Type)
-> Maybe BaseTy
limBySort TyVarInfoMap
vm RelMap
rm Dir
SuperTy
glbBySort :: TyVarInfoMap
-> RelMap -> [BaseTy] -> Sort -> Set (Name Type) -> Maybe BaseTy
glbBySort TyVarInfoMap
vm RelMap
rm = TyVarInfoMap
-> RelMap
-> Dir
-> [BaseTy]
-> Sort
-> Set (Name Type)
-> Maybe BaseTy
limBySort TyVarInfoMap
vm RelMap
rm Dir
SubTy
solveGraph
:: Members '[Fresh, Error SolveError, Output Message] r
=> TyVarInfoMap -> Graph UAtom -> Sem r S
solveGraph :: TyVarInfoMap -> Graph UAtom -> Sem r S
solveGraph TyVarInfoMap
vm Graph UAtom
g = Substitution Atom -> S
atomToTypeSubst (Substitution Atom -> S)
-> (Substitution BaseTy -> Substitution Atom)
-> Substitution BaseTy
-> S
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Substitution BaseTy -> Substitution Atom
unifyWCC (Substitution BaseTy -> S)
-> Sem r (Substitution BaseTy) -> Sem r S
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RelMap -> Sem r (Substitution BaseTy)
forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Output Message] r =>
RelMap -> Sem r (Substitution BaseTy)
go RelMap
topRelMap
where
unifyWCC :: Substitution BaseTy -> Substitution Atom
unifyWCC :: Substitution BaseTy -> Substitution Atom
unifyWCC Substitution BaseTy
s = [Substitution Atom] -> Substitution Atom
forall a (t :: * -> *).
(Subst a a, Foldable t) =>
t (Substitution a) -> Substitution a
compose ((Set (Name Type) -> Substitution Atom)
-> [Set (Name Type)] -> [Substitution Atom]
forall a b. (a -> b) -> [a] -> [b]
map Set (Name Type) -> Substitution Atom
mkEquateSubst [Set (Name Type)]
wccVarGroups) Substitution Atom -> Substitution Atom -> Substitution Atom
forall a.
Subst a a =>
Substitution a -> Substitution a -> Substitution a
@@ (BaseTy -> Atom) -> Substitution BaseTy -> Substitution Atom
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap BaseTy -> Atom
ABase Substitution BaseTy
s
where
wccVarGroups :: [Set (Name Type)]
wccVarGroups :: [Set (Name Type)]
wccVarGroups = (Set UAtom -> Set (Name Type)) -> [Set UAtom] -> [Set (Name Type)]
forall a b. (a -> b) -> [a] -> [b]
map ((UAtom -> Name Type) -> Set UAtom -> Set (Name Type)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map UAtom -> Name Type
getVar) ([Set UAtom] -> [Set (Name Type)])
-> ([Set UAtom] -> [Set UAtom]) -> [Set UAtom] -> [Set (Name Type)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set UAtom -> Bool) -> [Set UAtom] -> [Set UAtom]
forall a. (a -> Bool) -> [a] -> [a]
filter ((UAtom -> Bool) -> Set UAtom -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all UAtom -> Bool
uisVar) ([Set UAtom] -> [Set UAtom])
-> ([Set UAtom] -> [Set UAtom]) -> [Set UAtom] -> [Set UAtom]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Substitution BaseTy -> [Set UAtom] -> [Set UAtom]
forall b a. Subst b a => Substitution b -> a -> a
applySubst Substitution BaseTy
s ([Set UAtom] -> [Set (Name Type)])
-> [Set UAtom] -> [Set (Name Type)]
forall a b. (a -> b) -> a -> b
$ Graph UAtom -> [Set UAtom]
forall a. Ord a => Graph a -> [Set a]
G.wcc Graph UAtom
g
getVar :: UAtom -> Name Type
getVar (UV Name Type
v) = Name Type
v
getVar (UB BaseTy
b) = String -> Name Type
forall a. HasCallStack => String -> a
error
(String -> Name Type) -> String -> Name Type
forall a b. (a -> b) -> a -> b
$ String
"Impossible! Base type " String -> ShowS
forall a. [a] -> [a] -> [a]
++ BaseTy -> String
forall a. Show a => a -> String
show BaseTy
b String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" in solveGraph.getVar"
mkEquateSubst :: Set (Name Type) -> Substitution Atom
mkEquateSubst :: Set (Name Type) -> Substitution Atom
mkEquateSubst = [Name Type] -> Substitution Atom
mkEquations ([Name Type] -> Substitution Atom)
-> (Set (Name Type) -> [Name Type])
-> Set (Name Type)
-> Substitution Atom
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (Name Type) -> [Name Type]
forall a. Set a -> [a]
S.toList
mkEquations :: [Name Type] -> Substitution Atom
mkEquations (Name Type
a:[Name Type]
as) = [(Name Atom, Atom)] -> Substitution Atom
forall a. [(Name a, a)] -> Substitution a
Subst.fromList ([(Name Atom, Atom)] -> Substitution Atom)
-> ([Name Type] -> [(Name Atom, Atom)])
-> [Name Type]
-> Substitution Atom
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name Type -> (Name Atom, Atom))
-> [Name Type] -> [(Name Atom, Atom)]
forall a b. (a -> b) -> [a] -> [b]
map (\Name Type
v -> (Name Type -> Name Atom
coerce Name Type
v, Var -> Atom
AVar (Name Type -> Var
U Name Type
a))) ([Name Type] -> Substitution Atom)
-> [Name Type] -> Substitution Atom
forall a b. (a -> b) -> a -> b
$ [Name Type]
as
mkEquations [] = String -> Substitution Atom
forall a. HasCallStack => String -> a
error String
"Impossible! Empty set of names in mkEquateSubst"
topRelMap :: RelMap
topRelMap :: RelMap
topRelMap
= Map (Name Type, Dir) Rels -> RelMap
RelMap
(Map (Name Type, Dir) Rels -> RelMap)
-> (Map (Name Type, Dir) (Set UAtom) -> Map (Name Type, Dir) Rels)
-> Map (Name Type, Dir) (Set UAtom)
-> RelMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set UAtom -> Rels)
-> Map (Name Type, Dir) (Set UAtom) -> Map (Name Type, Dir) Rels
forall a b k. (a -> b) -> Map k a -> Map k b
M.map ((Set BaseTy -> Set (Name Type) -> Rels)
-> (Set BaseTy, Set (Name Type)) -> Rels
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Set BaseTy -> Set (Name Type) -> Rels
Rels ((Set BaseTy, Set (Name Type)) -> Rels)
-> (Set UAtom -> (Set BaseTy, Set (Name Type)))
-> Set UAtom
-> Rels
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([BaseTy] -> Set BaseTy
forall a. Eq a => [a] -> Set a
S.fromAscList ([BaseTy] -> Set BaseTy)
-> ([Name Type] -> Set (Name Type))
-> ([BaseTy], [Name Type])
-> (Set BaseTy, Set (Name Type))
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** [Name Type] -> Set (Name Type)
forall a. Eq a => [a] -> Set a
S.fromAscList)
(([BaseTy], [Name Type]) -> (Set BaseTy, Set (Name Type)))
-> (Set UAtom -> ([BaseTy], [Name Type]))
-> Set UAtom
-> (Set BaseTy, Set (Name Type))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Either BaseTy (Name Type)] -> ([BaseTy], [Name Type])
forall a b. [Either a b] -> ([a], [b])
partitionEithers ([Either BaseTy (Name Type)] -> ([BaseTy], [Name Type]))
-> (Set UAtom -> [Either BaseTy (Name Type)])
-> Set UAtom
-> ([BaseTy], [Name Type])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UAtom -> Either BaseTy (Name Type))
-> [UAtom] -> [Either BaseTy (Name Type)]
forall a b. (a -> b) -> [a] -> [b]
map UAtom -> Either BaseTy (Name Type)
uatomToEither ([UAtom] -> [Either BaseTy (Name Type)])
-> (Set UAtom -> [UAtom])
-> Set UAtom
-> [Either BaseTy (Name Type)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set UAtom -> [UAtom]
forall a. Set a -> [a]
S.toList)
(Map (Name Type, Dir) (Set UAtom) -> RelMap)
-> Map (Name Type, Dir) (Set UAtom) -> RelMap
forall a b. (a -> b) -> a -> b
$ (Name Type -> (Name Type, Dir))
-> Map (Name Type) (Set UAtom) -> Map (Name Type, Dir) (Set UAtom)
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeys (,Dir
SuperTy) Map (Name Type) (Set UAtom)
subMap Map (Name Type, Dir) (Set UAtom)
-> Map (Name Type, Dir) (Set UAtom)
-> Map (Name Type, Dir) (Set UAtom)
forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` (Name Type -> (Name Type, Dir))
-> Map (Name Type) (Set UAtom) -> Map (Name Type, Dir) (Set UAtom)
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeys (,Dir
SubTy) Map (Name Type) (Set UAtom)
superMap
subMap, superMap :: Map (Name Type) (Set UAtom)
(Map (Name Type) (Set UAtom)
subMap, Map (Name Type) (Set UAtom)
superMap) = (Map UAtom (Set UAtom) -> Map (Name Type) (Set UAtom)
onlyVars (Map UAtom (Set UAtom) -> Map (Name Type) (Set UAtom))
-> (Map UAtom (Set UAtom) -> Map (Name Type) (Set UAtom))
-> (Map UAtom (Set UAtom), Map UAtom (Set UAtom))
-> (Map (Name Type) (Set UAtom), Map (Name Type) (Set UAtom))
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** Map UAtom (Set UAtom) -> Map (Name Type) (Set UAtom)
onlyVars) ((Map UAtom (Set UAtom), Map UAtom (Set UAtom))
-> (Map (Name Type) (Set UAtom), Map (Name Type) (Set UAtom)))
-> (Map UAtom (Set UAtom), Map UAtom (Set UAtom))
-> (Map (Name Type) (Set UAtom), Map (Name Type) (Set UAtom))
forall a b. (a -> b) -> a -> b
$ Graph UAtom -> (Map UAtom (Set UAtom), Map UAtom (Set UAtom))
forall a.
(Show a, Ord a) =>
Graph a -> (Map a (Set a), Map a (Set a))
G.cessors Graph UAtom
g
onlyVars :: Map UAtom (Set UAtom) -> Map (Name Type) (Set UAtom)
onlyVars :: Map UAtom (Set UAtom) -> Map (Name Type) (Set UAtom)
onlyVars = (UAtom -> Name Type)
-> Map UAtom (Set UAtom) -> Map (Name Type) (Set UAtom)
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeys UAtom -> Name Type
fromVar (Map UAtom (Set UAtom) -> Map (Name Type) (Set UAtom))
-> (Map UAtom (Set UAtom) -> Map UAtom (Set UAtom))
-> Map UAtom (Set UAtom)
-> Map (Name Type) (Set UAtom)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UAtom -> Set UAtom -> Bool)
-> Map UAtom (Set UAtom) -> Map UAtom (Set UAtom)
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
M.filterWithKey (\UAtom
a Set UAtom
_ -> UAtom -> Bool
uisVar UAtom
a)
where
fromVar :: UAtom -> Name Type
fromVar (UV Name Type
x) = Name Type
x
fromVar UAtom
_ = String -> Name Type
forall a. HasCallStack => String -> a
error String
"Impossible! UB but uisVar."
go
:: Members '[Fresh, Error SolveError, Output Message] r
=> RelMap -> Sem r (Substitution BaseTy)
go :: RelMap -> Sem r (Substitution BaseTy)
go relMap :: RelMap
relMap@(RelMap Map (Name Type, Dir) Rels
rm) = RelMap -> Sem r ()
forall (r :: [(* -> *) -> * -> *]) t.
(Member (Output Message) r, Pretty t) =>
t -> Sem r ()
debugPretty RelMap
relMap Sem r ()
-> Sem r (Substitution BaseTy) -> Sem r (Substitution BaseTy)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> case [Name Type]
as of
[] -> Substitution BaseTy -> Sem r (Substitution BaseTy)
forall (m :: * -> *) a. Monad m => a -> m a
return Substitution BaseTy
forall a. Substitution a
idS
(Name Type
a:[Name Type]
_) -> do
Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug (Sem r Doc -> Sem r ()) -> Sem r Doc -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Sem r Doc
"Solving for" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Name Type -> Sem r Doc
forall t (r :: [(* -> *) -> * -> *]). Pretty t => t -> Sem r Doc
pretty' Name Type
a
case Name Type -> Maybe (Substitution BaseTy)
solveVar Name Type
a of
Maybe (Substitution BaseTy)
Nothing -> do
Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug (Sem r Doc -> Sem r ()) -> Sem r Doc -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Sem r Doc
"Couldn't solve for" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Name Type -> Sem r Doc
forall t (r :: [(* -> *) -> * -> *]). Pretty t => t -> Sem r Doc
pretty' Name Type
a
SolveError -> Sem r (Substitution BaseTy)
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw SolveError
NoUnify
Just Substitution BaseTy
s -> do
Substitution BaseTy -> Sem r ()
forall (r :: [(* -> *) -> * -> *]) t.
(Member (Output Message) r, Pretty t) =>
t -> Sem r ()
debugPretty Substitution BaseTy
s
(Substitution BaseTy -> Substitution BaseTy -> Substitution BaseTy
forall a.
Subst a a =>
Substitution a -> Substitution a -> Substitution a
@@ Substitution BaseTy
s) (Substitution BaseTy -> Substitution BaseTy)
-> Sem r (Substitution BaseTy) -> Sem r (Substitution BaseTy)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RelMap -> Sem r (Substitution BaseTy)
forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Output Message] r =>
RelMap -> Sem r (Substitution BaseTy)
go (Name Type -> BaseTy -> RelMap -> RelMap
substRel Name Type
a (Maybe BaseTy -> BaseTy
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe BaseTy -> BaseTy) -> Maybe BaseTy -> BaseTy
forall a b. (a -> b) -> a -> b
$ Name BaseTy -> Substitution BaseTy -> Maybe BaseTy
forall a. Name a -> Substitution a -> Maybe a
Subst.lookup (Name Type -> Name BaseTy
coerce Name Type
a) Substitution BaseTy
s) RelMap
relMap)
where
asBase :: [Name Type]
asBase
= ((Name Type, Dir) -> Name Type)
-> [(Name Type, Dir)] -> [Name Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name Type, Dir) -> Name Type
forall a b. (a, b) -> a
fst
([(Name Type, Dir)] -> [Name Type])
-> ([(Name Type, Dir)] -> [(Name Type, Dir)])
-> [(Name Type, Dir)]
-> [Name Type]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Name Type, Dir) -> Bool)
-> [(Name Type, Dir)] -> [(Name Type, Dir)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> ((Name Type, Dir) -> Bool) -> (Name Type, Dir) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set BaseTy -> Bool
forall a. Set a -> Bool
S.null (Set BaseTy -> Bool)
-> ((Name Type, Dir) -> Set BaseTy) -> (Name Type, Dir) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rels -> Set BaseTy
baseRels (Rels -> Set BaseTy)
-> ((Name Type, Dir) -> Rels) -> (Name Type, Dir) -> Set BaseTy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Map (Name Type, Dir) Rels -> (Name Type, Dir) -> Rels
forall k a.
(Ord k, Show k, Show (Map k a)) =>
String -> Map k a -> k -> a
lkup String
"solveGraph.go.as" Map (Name Type, Dir) Rels
rm)
([(Name Type, Dir)] -> [Name Type])
-> [(Name Type, Dir)] -> [Name Type]
forall a b. (a -> b) -> a -> b
$ Map (Name Type, Dir) Rels -> [(Name Type, Dir)]
forall k a. Map k a -> [k]
M.keys Map (Name Type, Dir) Rels
rm
as :: [Name Type]
as = case [Name Type]
asBase of
[] -> (Name Type -> Bool) -> [Name Type] -> [Name Type]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
/= Sort
topSort) (Sort -> Bool) -> (Name Type -> Sort) -> Name Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarInfoMap -> Name Type -> Sort
getSort TyVarInfoMap
vm) ([Name Type] -> [Name Type])
-> ([(Name Type, Dir)] -> [Name Type])
-> [(Name Type, Dir)]
-> [Name Type]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Name Type, Dir) -> Name Type)
-> [(Name Type, Dir)] -> [Name Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name Type, Dir) -> Name Type
forall a b. (a, b) -> a
fst ([(Name Type, Dir)] -> [Name Type])
-> [(Name Type, Dir)] -> [Name Type]
forall a b. (a -> b) -> a -> b
$ Map (Name Type, Dir) Rels -> [(Name Type, Dir)]
forall k a. Map k a -> [k]
M.keys Map (Name Type, Dir) Rels
rm
[Name Type]
_ -> [Name Type]
asBase
solveVar :: Name Type -> Maybe (Substitution BaseTy)
solveVar :: Name Type -> Maybe (Substitution BaseTy)
solveVar Name Type
v =
case ((Name Type
v,Dir
SuperTy), (Name Type
v,Dir
SubTy)) ((Name Type, Dir), (Name Type, Dir))
-> (((Name Type, Dir), (Name Type, Dir)) -> ([BaseTy], [BaseTy]))
-> ([BaseTy], [BaseTy])
forall a b. a -> (a -> b) -> b
& ASetter
((Name Type, Dir), (Name Type, Dir))
([BaseTy], [BaseTy])
(Name Type, Dir)
[BaseTy]
-> ((Name Type, Dir) -> [BaseTy])
-> ((Name Type, Dir), (Name Type, Dir))
-> ([BaseTy], [BaseTy])
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
((Name Type, Dir), (Name Type, Dir))
([BaseTy], [BaseTy])
(Name Type, Dir)
[BaseTy]
forall (r :: * -> * -> *) a b.
Bitraversable r =>
Traversal (r a a) (r b b) a b
both (Set BaseTy -> [BaseTy]
forall a. Set a -> [a]
S.toList (Set BaseTy -> [BaseTy])
-> ((Name Type, Dir) -> Set BaseTy) -> (Name Type, Dir) -> [BaseTy]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rels -> Set BaseTy
baseRels (Rels -> Set BaseTy)
-> ((Name Type, Dir) -> Rels) -> (Name Type, Dir) -> Set BaseTy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Map (Name Type, Dir) Rels -> (Name Type, Dir) -> Rels
forall k a.
(Ord k, Show k, Show (Map k a)) =>
String -> Map k a -> k -> a
lkup String
"solveGraph.solveVar" Map (Name Type, Dir) Rels
rm) of
([], []) ->
(Name Type -> Name BaseTy
coerce Name Type
v Name BaseTy -> BaseTy -> Substitution BaseTy
forall a. Name a -> a -> Substitution a
|->) (BaseTy -> Substitution BaseTy)
-> Maybe BaseTy -> Maybe (Substitution BaseTy)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyVarInfoMap
-> RelMap -> [BaseTy] -> Sort -> Set (Name Type) -> Maybe BaseTy
lubBySort TyVarInfoMap
vm RelMap
relMap [BaseTy
N] (TyVarInfoMap -> Name Type -> Sort
getSort TyVarInfoMap
vm Name Type
v)
(Rels -> Set (Name Type)
varRels (String -> Map (Name Type, Dir) Rels -> (Name Type, Dir) -> Rels
forall k a.
(Ord k, Show k, Show (Map k a)) =>
String -> Map k a -> k -> a
lkup String
"solveVar none, rels" Map (Name Type, Dir) Rels
rm (Name Type
v,Dir
SubTy)))
([BaseTy]
bsupers, []) ->
(Name Type -> Name BaseTy
coerce Name Type
v Name BaseTy -> BaseTy -> Substitution BaseTy
forall a. Name a -> a -> Substitution a
|->) (BaseTy -> Substitution BaseTy)
-> Maybe BaseTy -> Maybe (Substitution BaseTy)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyVarInfoMap
-> RelMap -> [BaseTy] -> Sort -> Set (Name Type) -> Maybe BaseTy
glbBySort TyVarInfoMap
vm RelMap
relMap [BaseTy]
bsupers (TyVarInfoMap -> Name Type -> Sort
getSort TyVarInfoMap
vm Name Type
v)
(Rels -> Set (Name Type)
varRels (String -> Map (Name Type, Dir) Rels -> (Name Type, Dir) -> Rels
forall k a.
(Ord k, Show k, Show (Map k a)) =>
String -> Map k a -> k -> a
lkup String
"solveVar bsupers, rels" Map (Name Type, Dir) Rels
rm (Name Type
v,Dir
SuperTy)))
([], [BaseTy]
bsubs) ->
(Name Type -> Name BaseTy
coerce Name Type
v Name BaseTy -> BaseTy -> Substitution BaseTy
forall a. Name a -> a -> Substitution a
|->) (BaseTy -> Substitution BaseTy)
-> Maybe BaseTy -> Maybe (Substitution BaseTy)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyVarInfoMap
-> RelMap -> [BaseTy] -> Sort -> Set (Name Type) -> Maybe BaseTy
lubBySort TyVarInfoMap
vm RelMap
relMap [BaseTy]
bsubs (TyVarInfoMap -> Name Type -> Sort
getSort TyVarInfoMap
vm Name Type
v)
(Rels -> Set (Name Type)
varRels (String -> Map (Name Type, Dir) Rels -> (Name Type, Dir) -> Rels
forall k a.
(Ord k, Show k, Show (Map k a)) =>
String -> Map k a -> k -> a
lkup String
"solveVar bsubs, rels" Map (Name Type, Dir) Rels
rm (Name Type
v,Dir
SubTy)))
([BaseTy]
bsupers, [BaseTy]
bsubs) -> do
BaseTy
ub <- TyVarInfoMap
-> RelMap -> [BaseTy] -> Sort -> Set (Name Type) -> Maybe BaseTy
glbBySort TyVarInfoMap
vm RelMap
relMap [BaseTy]
bsupers (TyVarInfoMap -> Name Type -> Sort
getSort TyVarInfoMap
vm Name Type
v)
(Rels -> Set (Name Type)
varRels (Map (Name Type, Dir) Rels
rm Map (Name Type, Dir) Rels -> (Name Type, Dir) -> Rels
forall k a. Ord k => Map k a -> k -> a
! (Name Type
v,Dir
SuperTy)))
BaseTy
lb <- TyVarInfoMap
-> RelMap -> [BaseTy] -> Sort -> Set (Name Type) -> Maybe BaseTy
lubBySort TyVarInfoMap
vm RelMap
relMap [BaseTy]
bsubs (TyVarInfoMap -> Name Type -> Sort
getSort TyVarInfoMap
vm Name Type
v)
(Rels -> Set (Name Type)
varRels (Map (Name Type, Dir) Rels
rm Map (Name Type, Dir) Rels -> (Name Type, Dir) -> Rels
forall k a. Ord k => Map k a -> k -> a
! (Name Type
v,Dir
SubTy)))
case BaseTy -> BaseTy -> Bool
isSubB BaseTy
lb BaseTy
ub of
Bool
True -> Substitution BaseTy -> Maybe (Substitution BaseTy)
forall a. a -> Maybe a
Just (Name Type -> Name BaseTy
coerce Name Type
v Name BaseTy -> BaseTy -> Substitution BaseTy
forall a. Name a -> a -> Substitution a
|-> BaseTy
lb)
Bool
False -> Maybe (Substitution BaseTy)
forall a. Maybe a
Nothing