{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE OverloadedStrings #-}

-----------------------------------------------------------------------------

-----------------------------------------------------------------------------

-- |
-- Module      :  Disco.Typecheck.Constraints
-- Copyright   :  disco team and contributors
-- Maintainer  :  byorgey@gmail.com
--
-- SPDX-License-Identifier: BSD-3-Clause
--
-- Constraints generated by type inference & checking.
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

-- | Constraints are generated as a result of type inference and checking.
--   These constraints are accumulated during the inference and checking phase
--   and are subsequently solved by the constraint solver.
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
    -- Use rt for both, since we don't need to print parens for /\ at all
    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

-- A helper function for creating a single constraint from a list of constraints.
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