content: {-# 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,
    cOr,
  )
  where
  
  import Data.List.NonEmpty (NonEmpty (..))
  import qualified Data.List.NonEmpty as NE
  import Data.Semigroup
  import Disco.Effects.LFresh
  import Disco.Pretty hiding ((<>))
  import Disco.Syntax.Operators (BFixity (In, InL, InR))
  import Disco.Types
  import Disco.Types.Rules
  import GHC.Generics (Generic)
  import Unbound.Generics.LocallyNameless hiding (lunbind)
  
  -- | 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 :: NonEmpty Constraint -> Constraint
    CTrue :: Constraint
    COr :: NonEmpty Constraint -> Constraint
    CAll :: Bind [Name Type] Constraint -> Constraint
    deriving (Show, Generic, Alpha, Subst Type)
  
  instance Pretty Constraint where
    pretty = \case
      CSub ty1 ty2 -> withPA (PA 4 In) $ lt (pretty ty1) <+> "<:" <+> rt (pretty ty2)
      CEq ty1 ty2 -> withPA (PA 4 In) $ lt (pretty ty1) <+> "=" <+> rt (pretty ty2)
      CQual q ty -> withPA (PA 10 InL) $ lt (pretty q) <+> rt (pretty ty)
      -- Use rt for everything, since we don't need to print parens for /\ at all
      CAnd cs -> withPA (PA 3 InR) $ foldr1 (\a b -> a <+> "/\\" <+> b) (NE.map (rt . pretty) cs)
      CTrue -> "True"
      COr cs -> withPA (PA 2 InR) $ foldr1 (\a b -> lt a <+> "\\/" <+> rt b) (NE.map pretty cs)
      CAll b -> lunbind b $ \(xs, c) ->
        "∀" <+> intercalate "," (map pretty xs) <> "." <+> pretty c
  
  -- A helper function for creating a single constraint from a list of constraints.
  cAnd :: [Constraint] -> Constraint
  cAnd cs = case filter nontrivial cs of
    [] -> CTrue
    [c] -> c
    (c : cs') -> CAnd (c :| cs')
   where
    nontrivial CTrue = False
    nontrivial _ = True
  
  cOr :: [Constraint] -> Constraint
  cOr [] = error "Empty list of constraints in cOr"
  cOr [c] = c
  cOr (c : cs) = COr (c :| cs)
  
  instance Semigroup Constraint where
    c1 <> c2 = cAnd [c1, c2]
    sconcat = cAnd . NE.toList
    stimes = stimesIdempotent
  
  instance Monoid Constraint where
    mempty = CTrue
    mappend = (<>)
    mconcat = cAnd
  