{-# 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
(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
      -- Use rt for both, since we don't need to print parens for /\ at all
    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

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