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