{-# LANGUAGE DeriveFunctor       #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ViewPatterns        #-}

{-
Author: George Karachalias <george.karachalias@cs.kuleuven.be>
        Sebastian Graf <sgraf1337@gmail.com>
-}

-- | Types used through-out pattern match checking. This module is mostly there
-- to be imported from "GHC.HsToCore.Types". The exposed API is that of
-- "GHC.HsToCore.Pmc".
--
-- These types model the paper
-- [Lower Your Guards: A Compositional Pattern-Match Coverage Checker"](https://dl.acm.org/doi/abs/10.1145/3408989).
module GHC.HsToCore.Pmc.Types (
        -- * LYG syntax

        -- ** Guard language
        SrcInfo(..), PmGrd(..), GrdVec(..),

        -- ** Guard tree language
        PmMatchGroup(..), PmMatch(..), PmGRHSs(..), PmGRHS(..), PmPatBind(..), PmEmptyCase(..),

        -- * Coverage Checking types
        RedSets (..), Precision (..), CheckResult (..),

        -- * Pre and post coverage checking synonyms
        Pre, Post,

        -- * Normalised refinement types
        module GHC.HsToCore.Pmc.Solver.Types

    ) where

import GHC.Prelude

import GHC.HsToCore.Pmc.Solver.Types

import GHC.Data.OrdList
import GHC.Types.Id
import GHC.Types.Var (EvVar)
import GHC.Types.SrcLoc
import GHC.Utils.Outputable
import GHC.Core.Type
import GHC.Core

import Data.List.NonEmpty ( NonEmpty(..) )
import qualified Data.List.NonEmpty as NE
import qualified Data.Semigroup as Semi

--
-- * Guard language
--

-- | A very simple language for pattern guards. Let bindings, bang patterns,
-- and matching variables against flat constructor patterns.
-- The LYG guard language.
data PmGrd
  = -- | @PmCon x K dicts args@ corresponds to a @K dicts args <- x@ guard.
    -- The @args@ are bound in this construct, the @x@ is just a use.
    -- For the arguments' meaning see 'GHC.Hs.Pat.ConPatOut'.
    PmCon {
      PmGrd -> Id
pm_id          :: !Id,
      PmGrd -> PmAltCon
pm_con_con     :: !PmAltCon,
      PmGrd -> [Id]
pm_con_tvs     :: ![TyVar],
      PmGrd -> [Id]
pm_con_dicts   :: ![EvVar],
      PmGrd -> [Id]
pm_con_args    :: ![Id]
    }

    -- | @PmBang x@ corresponds to a @seq x True@ guard.
    -- If the extra 'SrcInfo' is present, the bang guard came from a source
    -- bang pattern, in which case we might want to report it as redundant.
    -- See Note [Dead bang patterns] in GHC.HsToCore.Pmc.Check.
  | PmBang {
      pm_id   :: !Id,
      PmGrd -> Maybe SrcInfo
_pm_loc :: !(Maybe SrcInfo)
    }

    -- | @PmLet x expr@ corresponds to a @let x = expr@ guard. This actually
    -- /binds/ @x@.
  | PmLet {
      pm_id        :: !Id,
      PmGrd -> CoreExpr
_pm_let_expr :: !CoreExpr
    }

-- | Should not be user-facing.
instance Outputable PmGrd where
  ppr :: PmGrd -> SDoc
ppr (PmCon Id
x PmAltCon
alt [Id]
_tvs [Id]
_con_dicts [Id]
con_args)
    = [SDoc] -> SDoc
hsep [PmAltCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr PmAltCon
alt, [SDoc] -> SDoc
hsep ((Id -> SDoc) -> [Id] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Id]
con_args), String -> SDoc
text String
"<-", Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
x]
  ppr (PmBang Id
x Maybe SrcInfo
_loc) = Char -> SDoc
char Char
'!' SDoc -> SDoc -> SDoc
<> Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
x
  ppr (PmLet Id
x CoreExpr
expr) = [SDoc] -> SDoc
hsep [String -> SDoc
text String
"let", Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
x, String -> SDoc
text String
"=", CoreExpr -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreExpr
expr]

--
-- * Guard tree language
--

-- | Means by which we identify a source construct for later pretty-printing in
-- a warning message. 'SDoc' for the equation to show, 'Located' for the
-- location.
newtype SrcInfo = SrcInfo (Located SDoc)

-- | A sequence of 'PmGrd's.
newtype GrdVec = GrdVec [PmGrd]

-- | A guard tree denoting 'MatchGroup'.
newtype PmMatchGroup p = PmMatchGroup (NonEmpty (PmMatch p))

-- | A guard tree denoting 'Match': A payload describing the pats and a bunch of
-- GRHS.
data PmMatch p = PmMatch { forall p. PmMatch p -> p
pm_pats :: !p, forall p. PmMatch p -> PmGRHSs p
pm_grhss :: !(PmGRHSs p) }

-- | A guard tree denoting 'GRHSs': A bunch of 'PmLet' guards for local
-- bindings from the 'GRHSs's @where@ clauses and the actual list of 'GRHS'.
-- See Note [Long-distance information for HsLocalBinds] in
-- "GHC.HsToCore.Pmc.Desugar".
data PmGRHSs p = PmGRHSs { forall p. PmGRHSs p -> p
pgs_lcls :: !p, forall p. PmGRHSs p -> NonEmpty (PmGRHS p)
pgs_grhss :: !(NonEmpty (PmGRHS p))}

-- | A guard tree denoting 'GRHS': A payload describing the grds and a 'SrcInfo'
-- useful for printing out in warnings messages.
data PmGRHS p = PmGRHS { forall p. PmGRHS p -> p
pg_grds :: !p, forall p. PmGRHS p -> SrcInfo
pg_rhs :: !SrcInfo }

-- | A guard tree denoting an -XEmptyCase.
newtype PmEmptyCase = PmEmptyCase { PmEmptyCase -> Id
pe_var :: Id }

-- | A guard tree denoting a pattern binding.
newtype PmPatBind p =
  -- just reuse GrdGRHS and pretend its @SrcInfo@ is info on the /pattern/,
  -- rather than on the pattern bindings.
  PmPatBind (PmGRHS p)

instance Outputable SrcInfo where
  ppr :: SrcInfo -> SDoc
ppr (SrcInfo (L (RealSrcSpan RealSrcSpan
rss Maybe BufSpan
_) SDoc
_)) = Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr (RealSrcSpan -> Int
srcSpanStartLine RealSrcSpan
rss)
  ppr (SrcInfo (L SrcSpan
s                   SDoc
_)) = SrcSpan -> SDoc
forall a. Outputable a => a -> SDoc
ppr SrcSpan
s

-- | Format LYG guards as @| True <- x, let x = 42, !z@
instance Outputable GrdVec where
  ppr :: GrdVec -> SDoc
ppr (GrdVec [])     = SDoc
empty
  ppr (GrdVec (PmGrd
g:[PmGrd]
gs)) = [SDoc] -> SDoc
fsep (Char -> SDoc
char Char
'|' SDoc -> SDoc -> SDoc
<+> PmGrd -> SDoc
forall a. Outputable a => a -> SDoc
ppr PmGrd
g SDoc -> [SDoc] -> [SDoc]
forall a. a -> [a] -> [a]
: (PmGrd -> SDoc) -> [PmGrd] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map ((SDoc
comma SDoc -> SDoc -> SDoc
<+>) (SDoc -> SDoc) -> (PmGrd -> SDoc) -> PmGrd -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PmGrd -> SDoc
forall a. Outputable a => a -> SDoc
ppr) [PmGrd]
gs)

-- | Format a LYG sequence (e.g. 'Match'es of a 'MatchGroup' or 'GRHSs') as
-- @{ <first alt>; ...; <last alt> }@
pprLygSequence :: Outputable a => NonEmpty a -> SDoc
pprLygSequence :: forall a. Outputable a => NonEmpty a -> SDoc
pprLygSequence (NonEmpty a -> [a]
forall a. NonEmpty a -> [a]
NE.toList -> [a]
as) =
  SDoc -> SDoc
braces (SDoc
space SDoc -> SDoc -> SDoc
<> [SDoc] -> SDoc
fsep (SDoc -> [SDoc] -> [SDoc]
punctuate SDoc
semi ((a -> SDoc) -> [a] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map a -> SDoc
forall a. Outputable a => a -> SDoc
ppr [a]
as)) SDoc -> SDoc -> SDoc
<> SDoc
space)

instance Outputable p => Outputable (PmMatchGroup p) where
  ppr :: PmMatchGroup p -> SDoc
ppr (PmMatchGroup NonEmpty (PmMatch p)
matches) = NonEmpty (PmMatch p) -> SDoc
forall a. Outputable a => NonEmpty a -> SDoc
pprLygSequence NonEmpty (PmMatch p)
matches

instance Outputable p => Outputable (PmMatch p) where
  ppr :: PmMatch p -> SDoc
ppr (PmMatch { pm_pats :: forall p. PmMatch p -> p
pm_pats = p
grds, pm_grhss :: forall p. PmMatch p -> PmGRHSs p
pm_grhss = PmGRHSs p
grhss }) =
    p -> SDoc
forall a. Outputable a => a -> SDoc
ppr p
grds SDoc -> SDoc -> SDoc
<+> PmGRHSs p -> SDoc
forall a. Outputable a => a -> SDoc
ppr PmGRHSs p
grhss

instance Outputable p => Outputable (PmGRHSs p) where
  ppr :: PmGRHSs p -> SDoc
ppr (PmGRHSs { pgs_lcls :: forall p. PmGRHSs p -> p
pgs_lcls = p
_lcls, pgs_grhss :: forall p. PmGRHSs p -> NonEmpty (PmGRHS p)
pgs_grhss = NonEmpty (PmGRHS p)
grhss }) =
    NonEmpty (PmGRHS p) -> SDoc
forall a. Outputable a => a -> SDoc
ppr NonEmpty (PmGRHS p)
grhss

instance Outputable p => Outputable (PmGRHS p) where
  ppr :: PmGRHS p -> SDoc
ppr (PmGRHS { pg_grds :: forall p. PmGRHS p -> p
pg_grds = p
grds, pg_rhs :: forall p. PmGRHS p -> SrcInfo
pg_rhs = SrcInfo
rhs }) =
    p -> SDoc
forall a. Outputable a => a -> SDoc
ppr p
grds SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"->" SDoc -> SDoc -> SDoc
<+> SrcInfo -> SDoc
forall a. Outputable a => a -> SDoc
ppr SrcInfo
rhs

instance Outputable p => Outputable (PmPatBind p) where
  ppr :: PmPatBind p -> SDoc
ppr (PmPatBind PmGRHS { pg_grds :: forall p. PmGRHS p -> p
pg_grds = p
grds, pg_rhs :: forall p. PmGRHS p -> SrcInfo
pg_rhs = SrcInfo
bind }) =
    SrcInfo -> SDoc
forall a. Outputable a => a -> SDoc
ppr SrcInfo
bind SDoc -> SDoc -> SDoc
<+> p -> SDoc
forall a. Outputable a => a -> SDoc
ppr p
grds SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"=" SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"..."

instance Outputable PmEmptyCase where
  ppr :: PmEmptyCase -> SDoc
ppr (PmEmptyCase { pe_var :: PmEmptyCase -> Id
pe_var = Id
var }) =
    String -> SDoc
text String
"<empty case on " SDoc -> SDoc -> SDoc
<> Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
var SDoc -> SDoc -> SDoc
<> String -> SDoc
text String
">"

data Precision = Approximate | Precise
  deriving (Precision -> Precision -> Bool
(Precision -> Precision -> Bool)
-> (Precision -> Precision -> Bool) -> Eq Precision
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Precision -> Precision -> Bool
== :: Precision -> Precision -> Bool
$c/= :: Precision -> Precision -> Bool
/= :: Precision -> Precision -> Bool
Eq, Int -> Precision -> ShowS
[Precision] -> ShowS
Precision -> String
(Int -> Precision -> ShowS)
-> (Precision -> String)
-> ([Precision] -> ShowS)
-> Show Precision
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Precision -> ShowS
showsPrec :: Int -> Precision -> ShowS
$cshow :: Precision -> String
show :: Precision -> String
$cshowList :: [Precision] -> ShowS
showList :: [Precision] -> ShowS
Show)

instance Outputable Precision where
  ppr :: Precision -> SDoc
ppr = String -> SDoc
text (String -> SDoc) -> (Precision -> String) -> Precision -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Precision -> String
forall a. Show a => a -> String
show

instance Semi.Semigroup Precision where
  Precision
Precise <> :: Precision -> Precision -> Precision
<> Precision
Precise = Precision
Precise
  Precision
_       <> Precision
_       = Precision
Approximate

instance Monoid Precision where
  mempty :: Precision
mempty = Precision
Precise
  mappend :: Precision -> Precision -> Precision
mappend = Precision -> Precision -> Precision
forall a. Semigroup a => a -> a -> a
(Semi.<>)

-- | Redundancy sets, used to determine redundancy of RHSs and bang patterns
-- (later digested into a 'CIRB').
data RedSets
  = RedSets
  { RedSets -> Nablas
rs_cov :: !Nablas
  -- ^ The /Covered/ set; the set of values reaching a particular program
  -- point.
  , RedSets -> Nablas
rs_div :: !Nablas
  -- ^ The /Diverging/ set; empty if no match can lead to divergence.
  --   If it wasn't empty, we have to turn redundancy warnings into
  --   inaccessibility warnings for any subclauses.
  , RedSets -> OrdList (Nablas, SrcInfo)
rs_bangs :: !(OrdList (Nablas, SrcInfo))
  -- ^ If any of the 'Nablas' is empty, the corresponding 'SrcInfo' pin-points
  -- a bang pattern in source that is redundant. See Note [Dead bang patterns].
  }

instance Outputable RedSets where
  ppr :: RedSets -> SDoc
ppr RedSets { rs_cov :: RedSets -> Nablas
rs_cov = Nablas
_cov, rs_div :: RedSets -> Nablas
rs_div = Nablas
_div, rs_bangs :: RedSets -> OrdList (Nablas, SrcInfo)
rs_bangs = OrdList (Nablas, SrcInfo)
_bangs }
    -- It's useful to change this definition for different verbosity levels in
    -- printf-debugging
    = SDoc
empty

-- | Pattern-match coverage check result
data CheckResult a
  = CheckResult
  { forall a. CheckResult a -> a
cr_ret :: !a
  -- ^ A hole for redundancy info and covered sets.
  , forall a. CheckResult a -> Nablas
cr_uncov   :: !Nablas
  -- ^ The set of uncovered values falling out at the bottom.
  --   (for -Wincomplete-patterns, but also important state for the algorithm)
  , forall a. CheckResult a -> Precision
cr_approx  :: !Precision
  -- ^ A flag saying whether we ran into the 'maxPmCheckModels' limit for the
  -- purpose of suggesting to crank it up in the warning message. Writer state.
  } deriving (forall a b. (a -> b) -> CheckResult a -> CheckResult b)
-> (forall a b. a -> CheckResult b -> CheckResult a)
-> Functor CheckResult
forall a b. a -> CheckResult b -> CheckResult a
forall a b. (a -> b) -> CheckResult a -> CheckResult b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> CheckResult a -> CheckResult b
fmap :: forall a b. (a -> b) -> CheckResult a -> CheckResult b
$c<$ :: forall a b. a -> CheckResult b -> CheckResult a
<$ :: forall a b. a -> CheckResult b -> CheckResult a
Functor

instance Outputable a => Outputable (CheckResult a) where
  ppr :: CheckResult a -> SDoc
ppr (CheckResult a
c Nablas
unc Precision
pc)
    = String -> SDoc
text String
"CheckResult" SDoc -> SDoc -> SDoc
<+> Precision -> SDoc
ppr_precision Precision
pc SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
braces ([SDoc] -> SDoc
fsep
        [ String -> a -> SDoc
forall {a}. Outputable a => String -> a -> SDoc
field String
"ret" a
c SDoc -> SDoc -> SDoc
<> SDoc
comma
        , String -> Nablas -> SDoc
forall {a}. Outputable a => String -> a -> SDoc
field String
"uncov" Nablas
unc])
    where
      ppr_precision :: Precision -> SDoc
ppr_precision Precision
Precise     = SDoc
empty
      ppr_precision Precision
Approximate = String -> SDoc
text String
"(Approximate)"
      field :: String -> a -> SDoc
field String
name a
value = String -> SDoc
text String
name SDoc -> SDoc -> SDoc
<+> SDoc
equals SDoc -> SDoc -> SDoc
<+> a -> SDoc
forall a. Outputable a => a -> SDoc
ppr a
value

--
-- * Pre and post coverage checking synonyms
--

-- | Used as tree payload pre-checking. The LYG guards to check.
type Pre = GrdVec

-- | Used as tree payload post-checking. The redundancy info we elaborated.
type Post = RedSets