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,
)
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 (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)
    CAnd [c] -> pretty c
    -- Use rt for both, since we don't need to print parens for /\ at all
    CAnd (c : cs) -> withPA (PA 3 InR) $ rt (pretty c) <+> "/\\" <+> rt (pretty (CAnd cs))
    CAnd [] -> "True"
    CTrue -> "True"
    COr [c] -> pretty c
    COr (c : cs) -> withPA (PA 2 InR) $ lt (pretty c) <+> "\\/" <+> rt (pretty (COr cs))
    COr [] -> "False"
    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
  cs' -> CAnd cs'
 where
  nontrivial CTrue = False
  nontrivial _ = True

instance Semigroup Constraint where
  c1 <> c2 = cAnd [c1, c2]
  sconcat = cAnd . NE.toList
  stimes = stimesIdempotent

instance Monoid Constraint where
  mempty = CTrue
  mappend = (<>)
  mconcat = cAnd