{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE OverloadedStrings #-}
module Disco.Typecheck.Constraints
( Constraint(..)
, cAnd
)
where
import qualified Data.List.NonEmpty as NE
import Data.Semigroup
import GHC.Generics (Generic)
import Unbound.Generics.LocallyNameless hiding (lunbind)
import Disco.Effects.LFresh
import Disco.Pretty hiding ((<>))
import Disco.Syntax.Operators (BFixity (In, InL, InR))
import Disco.Types
import Disco.Types.Rules
data Constraint where
CSub :: Type -> Type -> Constraint
CEq :: Type -> Type -> Constraint
CQual :: Qualifier -> Type -> Constraint
CAnd :: [Constraint] -> Constraint
CTrue :: Constraint
COr :: [Constraint] -> Constraint
CAll :: Bind [Name Type] Constraint -> Constraint
deriving (Int -> Constraint -> ShowS
[Constraint] -> ShowS
Constraint -> String
(Int -> Constraint -> ShowS)
-> (Constraint -> String)
-> ([Constraint] -> ShowS)
-> Show Constraint
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Constraint] -> ShowS
$cshowList :: [Constraint] -> ShowS
show :: Constraint -> String
$cshow :: Constraint -> String
showsPrec :: Int -> Constraint -> ShowS
$cshowsPrec :: Int -> Constraint -> ShowS
Show, (forall x. Constraint -> Rep Constraint x)
-> (forall x. Rep Constraint x -> Constraint) -> Generic Constraint
forall x. Rep Constraint x -> Constraint
forall x. Constraint -> Rep Constraint x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Constraint x -> Constraint
$cfrom :: forall x. Constraint -> Rep Constraint x
Generic, Show Constraint
Show Constraint
-> (AlphaCtx -> Constraint -> Constraint -> Bool)
-> (forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Constraint -> f Constraint)
-> (AlphaCtx -> NamePatFind -> Constraint -> Constraint)
-> (AlphaCtx -> NthPatFind -> Constraint -> Constraint)
-> (Constraint -> DisjointSet AnyName)
-> (Constraint -> All)
-> (Constraint -> Bool)
-> (Constraint -> NthPatFind)
-> (Constraint -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> Constraint -> Constraint)
-> (forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> Constraint -> (Constraint -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Constraint -> m (Constraint, Perm AnyName))
-> (AlphaCtx -> Constraint -> Constraint -> Ordering)
-> Alpha Constraint
AlphaCtx -> NthPatFind -> Constraint -> Constraint
AlphaCtx -> NamePatFind -> Constraint -> Constraint
AlphaCtx -> Perm AnyName -> Constraint -> Constraint
AlphaCtx -> Constraint -> Constraint -> Bool
AlphaCtx -> Constraint -> Constraint -> Ordering
Constraint -> Bool
Constraint -> All
Constraint -> DisjointSet AnyName
Constraint -> NthPatFind
Constraint -> 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) -> Constraint -> f Constraint
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Constraint -> m (Constraint, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> Constraint -> (Constraint -> Perm AnyName -> m b) -> m b
acompare' :: AlphaCtx -> Constraint -> Constraint -> Ordering
$cacompare' :: AlphaCtx -> Constraint -> Constraint -> Ordering
freshen' :: AlphaCtx -> Constraint -> m (Constraint, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Constraint -> m (Constraint, Perm AnyName)
lfreshen' :: AlphaCtx
-> Constraint -> (Constraint -> Perm AnyName -> m b) -> m b
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> Constraint -> (Constraint -> Perm AnyName -> m b) -> m b
swaps' :: AlphaCtx -> Perm AnyName -> Constraint -> Constraint
$cswaps' :: AlphaCtx -> Perm AnyName -> Constraint -> Constraint
namePatFind :: Constraint -> NamePatFind
$cnamePatFind :: Constraint -> NamePatFind
nthPatFind :: Constraint -> NthPatFind
$cnthPatFind :: Constraint -> NthPatFind
isEmbed :: Constraint -> Bool
$cisEmbed :: Constraint -> Bool
isTerm :: Constraint -> All
$cisTerm :: Constraint -> All
isPat :: Constraint -> DisjointSet AnyName
$cisPat :: Constraint -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> Constraint -> Constraint
$copen :: AlphaCtx -> NthPatFind -> Constraint -> Constraint
close :: AlphaCtx -> NamePatFind -> Constraint -> Constraint
$cclose :: AlphaCtx -> NamePatFind -> Constraint -> Constraint
fvAny' :: AlphaCtx -> (AnyName -> f AnyName) -> Constraint -> f Constraint
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Constraint -> f Constraint
aeq' :: AlphaCtx -> Constraint -> Constraint -> Bool
$caeq' :: AlphaCtx -> Constraint -> Constraint -> Bool
$cp1Alpha :: Show Constraint
Alpha, Subst Type)
instance Pretty Constraint where
pretty :: Constraint -> Sem r Doc
pretty = \case
CSub Type
ty1 Type
ty2 -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA (Int -> BFixity -> PA
PA Int
4 BFixity
In) (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Type -> Sem r Doc
forall t (r :: EffectRow).
(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
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Type
ty2)
CEq Type
ty1 Type
ty2 -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA (Int -> BFixity -> PA
PA Int
4 BFixity
In) (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Type -> Sem r Doc
forall t (r :: EffectRow).
(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
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Type
ty2)
CQual Qualifier
q Type
ty -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA (Int -> BFixity -> PA
PA Int
10 BFixity
InL) (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Qualifier -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Qualifier
q) 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
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Type
ty)
CAnd [Constraint
c] -> Constraint -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Constraint
c
CAnd (Constraint
c:[Constraint]
cs) -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA (Int -> BFixity -> PA
PA Int
3 BFixity
InR) (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Constraint -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Constraint
c) 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
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Constraint -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty ([Constraint] -> Constraint
CAnd [Constraint]
cs))
CAnd [] -> Sem r Doc
"True"
Constraint
CTrue -> Sem r Doc
"True"
COr [Constraint
c] -> Constraint -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Constraint
c
COr (Constraint
c:[Constraint]
cs) -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA (Int -> BFixity -> PA
PA Int
2 BFixity
InR) (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Constraint -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Constraint
c) 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
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Constraint -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty ([Constraint] -> Constraint
COr [Constraint]
cs))
COr [] -> Sem r Doc
"False"
CAll Bind [Name Type] Constraint
b -> Bind [Name Type] Constraint
-> (([Name Type], Constraint) -> Sem r Doc) -> Sem r Doc
forall (r :: EffectRow) p t c.
(Member LFresh r, Alpha p, Alpha t) =>
Bind p t -> ((p, t) -> Sem r c) -> Sem r c
lunbind Bind [Name Type] Constraint
b ((([Name Type], Constraint) -> Sem r Doc) -> Sem r Doc)
-> (([Name Type], Constraint) -> Sem r Doc) -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ \([Name Type]
xs, Constraint
c) ->
Sem r Doc
"∀" 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
forall (f :: * -> *). Monad f => f Doc -> [f Doc] -> f Doc
intercalate Sem r Doc
"," ((Name Type -> Sem r Doc) -> [Name Type] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty [Name Type]
xs) 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 (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Constraint -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Constraint
c
cAnd :: [Constraint] -> Constraint
cAnd :: [Constraint] -> Constraint
cAnd [Constraint]
cs = case (Constraint -> Bool) -> [Constraint] -> [Constraint]
forall a. (a -> Bool) -> [a] -> [a]
filter Constraint -> Bool
nontrivial [Constraint]
cs of
[] -> Constraint
CTrue
[Constraint
c] -> Constraint
c
[Constraint]
cs' -> [Constraint] -> Constraint
CAnd [Constraint]
cs'
where
nontrivial :: Constraint -> Bool
nontrivial Constraint
CTrue = Bool
False
nontrivial Constraint
_ = Bool
True
instance Semigroup Constraint where
Constraint
c1 <> :: Constraint -> Constraint -> Constraint
<> Constraint
c2 = [Constraint] -> Constraint
cAnd [Constraint
c1,Constraint
c2]
sconcat :: NonEmpty Constraint -> Constraint
sconcat = [Constraint] -> Constraint
cAnd ([Constraint] -> Constraint)
-> (NonEmpty Constraint -> [Constraint])
-> NonEmpty Constraint
-> Constraint
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty Constraint -> [Constraint]
forall a. NonEmpty a -> [a]
NE.toList
stimes :: b -> Constraint -> Constraint
stimes = b -> Constraint -> Constraint
forall b a. Integral b => b -> a -> a
stimesIdempotent
instance Monoid Constraint where
mempty :: Constraint
mempty = Constraint
CTrue
mappend :: Constraint -> Constraint -> Constraint
mappend = Constraint -> Constraint -> Constraint
forall a. Semigroup a => a -> a -> a
(<>)
mconcat :: [Constraint] -> Constraint
mconcat = [Constraint] -> Constraint
cAnd