{-# 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
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. 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
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' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Constraint -> m (Constraint, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Constraint -> m (Constraint, Perm AnyName)
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
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' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
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
Alpha, Subst Type)
instance Pretty Constraint where
pretty :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Constraint -> Sem r (Doc ann)
pretty = \case
CSub Type
ty1 Type
ty2 -> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA (Int -> BFixity -> PA
PA Int
4 BFixity
In) forall a b. (a -> b) -> a -> b
$ forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Type
ty1) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"<:" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Type
ty2)
CEq Type
ty1 Type
ty2 -> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA (Int -> BFixity -> PA
PA Int
4 BFixity
In) forall a b. (a -> b) -> a -> b
$ forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Type
ty1) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"=" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Type
ty2)
CQual Qualifier
q Type
ty -> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA (Int -> BFixity -> PA
PA Int
10 BFixity
InL) forall a b. (a -> b) -> a -> b
$ forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Qualifier
q) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Type
ty)
CAnd [Constraint
c] -> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Constraint
c
CAnd (Constraint
c : [Constraint]
cs) -> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA (Int -> BFixity -> PA
PA Int
3 BFixity
InR) forall a b. (a -> b) -> a -> b
$ forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Constraint
c) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"/\\" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty ([Constraint] -> Constraint
CAnd [Constraint]
cs))
CAnd [] -> Sem r (Doc ann)
"True"
Constraint
CTrue -> Sem r (Doc ann)
"True"
COr [Constraint
c] -> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Constraint
c
COr (Constraint
c : [Constraint]
cs) -> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA (Int -> BFixity -> PA
PA Int
2 BFixity
InR) forall a b. (a -> b) -> a -> b
$ forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Constraint
c) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"\\/" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty ([Constraint] -> Constraint
COr [Constraint]
cs))
COr [] -> Sem r (Doc ann)
"False"
CAll Bind [Name Type] Constraint
b -> 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 forall a b. (a -> b) -> a -> b
$ \([Name Type]
xs, Constraint
c) ->
Sem r (Doc ann)
"∀" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (f :: * -> *) ann.
Monad f =>
f (Doc ann) -> [f (Doc ann)] -> f (Doc ann)
intercalate Sem r (Doc ann)
"," (forall a b. (a -> b) -> [a] -> [b]
map forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty [Name Type]
xs) forall a. Semigroup a => a -> a -> a
<> Sem r (Doc ann)
"." forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Constraint
c
cAnd :: [Constraint] -> Constraint
cAnd :: [Constraint] -> Constraint
cAnd [Constraint]
cs = case 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NonEmpty a -> [a]
NE.toList
stimes :: forall b. Integral b => b -> Constraint -> Constraint
stimes = forall b a. Integral b => b -> a -> a
stimesIdempotent
instance Monoid Constraint where
mempty :: Constraint
mempty = Constraint
CTrue
mappend :: Constraint -> Constraint -> Constraint
mappend = forall a. Semigroup a => a -> a -> a
(<>)
mconcat :: [Constraint] -> Constraint
mconcat = [Constraint] -> Constraint
cAnd