Constraints.hs

{-# 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