{-
Author: George Karachalias <george.karachalias@cs.kuleuven.be>

Haskell expressions (as used by the pattern matching checker) and utilities.
-}

{-# LANGUAGE CPP #-}
{-# LANGUAGE ViewPatterns #-}

module PmExpr (
        PmExpr(..), PmLit(..), SimpleEq, ComplexEq, toComplex, eqPmLit,
        truePmExpr, falsePmExpr, isTruePmExpr, isFalsePmExpr, isNotPmExprOther,
        lhsExprToPmExpr, hsExprToPmExpr, substComplexEq, filterComplex,
        pprPmExprWithParens, runPmPprM
    ) where

#include "HsVersions.h"

import GhcPrelude

import BasicTypes (SourceText)
import FastString (FastString, unpackFS)
import HsSyn
import Id
import Name
import NameSet
import DataCon
import ConLike
import TcType (isStringTy)
import TysWiredIn
import Outputable
import Util
import SrcLoc

import Data.Maybe (mapMaybe)
import Data.List (groupBy, sortBy, nubBy)
import Control.Monad.Trans.State.Lazy

{-
%************************************************************************
%*                                                                      *
                         Lifted Expressions
%*                                                                      *
%************************************************************************
-}

{- Note [PmExprOther in PmExpr]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Since there is no plan to extend the (currently pretty naive) term oracle in
the near future, instead of playing with the verbose (HsExpr Id), we lift it to
PmExpr. All expressions the term oracle does not handle are wrapped by the
constructor PmExprOther. Note that we do not perform substitution in
PmExprOther. Because of this, we do not even print PmExprOther, since they may
refer to variables that are otherwise substituted away.
-}

-- ----------------------------------------------------------------------------
-- ** Types

-- | Lifted expressions for pattern match checking.
data PmExpr = PmExprVar   Name
            | PmExprCon   ConLike [PmExpr]
            | PmExprLit   PmLit
            | PmExprEq    PmExpr PmExpr  -- Syntactic equality
            | PmExprOther (HsExpr GhcTc)  -- Note [PmExprOther in PmExpr]


mkPmExprData :: DataCon -> [PmExpr] -> PmExpr
mkPmExprData :: DataCon -> [PmExpr] -> PmExpr
mkPmExprData dc :: DataCon
dc args :: [PmExpr]
args = ConLike -> [PmExpr] -> PmExpr
PmExprCon (DataCon -> ConLike
RealDataCon DataCon
dc) [PmExpr]
args

-- | Literals (simple and overloaded ones) for pattern match checking.
data PmLit = PmSLit (HsLit GhcTc)                               -- simple
           | PmOLit Bool {- is it negated? -} (HsOverLit GhcTc) -- overloaded

-- | Equality between literals for pattern match checking.
eqPmLit :: PmLit -> PmLit -> Bool
eqPmLit :: PmLit -> PmLit -> Bool
eqPmLit (PmSLit    l1 :: HsLit GhcTc
l1) (PmSLit    l2 :: HsLit GhcTc
l2) = HsLit GhcTc
l1 HsLit GhcTc -> HsLit GhcTc -> Bool
forall a. Eq a => a -> a -> Bool
== HsLit GhcTc
l2
eqPmLit (PmOLit b1 :: Bool
b1 l1 :: HsOverLit GhcTc
l1) (PmOLit b2 :: Bool
b2 l2 :: HsOverLit GhcTc
l2) = Bool
b1 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
b2 Bool -> Bool -> Bool
&& HsOverLit GhcTc
l1 HsOverLit GhcTc -> HsOverLit GhcTc -> Bool
forall a. Eq a => a -> a -> Bool
== HsOverLit GhcTc
l2
  -- See Note [Undecidable Equality for Overloaded Literals]
eqPmLit _              _              = Bool
False

{- Note [Undecidable Equality for Overloaded Literals]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Equality on overloaded literals is undecidable in the general case. Consider
the following example:

  instance Num Bool where
    ...
    fromInteger 0 = False -- C-like representation of booleans
    fromInteger _ = True

    f :: Bool -> ()
    f 1 = ()        -- Clause A
    f 2 = ()        -- Clause B

Clause B is redundant but to detect this, we should be able to solve the
constraint: False ~ (fromInteger 2 ~ fromInteger 1) which means that we
have to look through function `fromInteger`, whose implementation could
be anything. This poses difficulties for:

1. The expressive power of the check.
   We cannot expect a reasonable implementation of pattern matching to detect
   that fromInteger 2 ~ fromInteger 1 is True, unless we unfold function
   fromInteger. This puts termination at risk and is undecidable in the
   general case.

2. Performance.
   Having an unresolved constraint False ~ (fromInteger 2 ~ fromInteger 1)
   lying around could become expensive really fast. Ticket #11161 illustrates
   how heavy use of overloaded literals can generate plenty of those
   constraints, effectively undermining the term oracle's performance.

3. Error nessages/Warnings.
   What should our message for `f` above be? A reasonable approach would be
   to issue:

     Pattern matches are (potentially) redundant:
       f 2 = ...    under the assumption that 1 == 2

   but seems to complex and confusing for the user.

We choose to treat overloaded literals that look different as different. The
impact of this is the following:

  * Redundancy checking is rather conservative, since it cannot see that clause
    B above is redundant.

  * We have instant equality check for overloaded literals (we do not rely on
    the term oracle which is rather expensive, both in terms of performance and
    memory). This significantly improves the performance of functions `covered`
    `uncovered` and `divergent` in deSugar/Check.hs and effectively addresses
    #11161.

  * The warnings issued are simpler.

  * We do not play on the safe side, strictly speaking. The assumption that
    1 /= 2 makes the redundancy check more conservative but at the same time
    makes its dual (exhaustiveness check) unsafe. This we can live with, mainly
    for two reasons:
    1. At the moment we do not use the results of the check during compilation
       where this would be a disaster (could result in runtime errors even if
       our function was deemed exhaustive).
    2. Pattern matcing on literals can never be considered exhaustive unless we
       have a catch-all clause. Hence, this assumption affects mainly the
       appearance of the warnings and is, in practice safe.
-}

nubPmLit :: [PmLit] -> [PmLit]
nubPmLit :: [PmLit] -> [PmLit]
nubPmLit = (PmLit -> PmLit -> Bool) -> [PmLit] -> [PmLit]
forall a. (a -> a -> Bool) -> [a] -> [a]
nubBy PmLit -> PmLit -> Bool
eqPmLit

-- | Term equalities
type SimpleEq  = (Id, PmExpr) -- We always use this orientation
type ComplexEq = (PmExpr, PmExpr)

-- | Lift a `SimpleEq` to a `ComplexEq`
toComplex :: SimpleEq -> ComplexEq
toComplex :: SimpleEq -> ComplexEq
toComplex (x :: Id
x,e :: PmExpr
e) = (Name -> PmExpr
PmExprVar (Id -> Name
idName Id
x), PmExpr
e)

-- | Expression `True'
truePmExpr :: PmExpr
truePmExpr :: PmExpr
truePmExpr = DataCon -> [PmExpr] -> PmExpr
mkPmExprData DataCon
trueDataCon []

-- | Expression `False'
falsePmExpr :: PmExpr
falsePmExpr :: PmExpr
falsePmExpr = DataCon -> [PmExpr] -> PmExpr
mkPmExprData DataCon
falseDataCon []

-- ----------------------------------------------------------------------------
-- ** Predicates on PmExpr

-- | Check if an expression is lifted or not
isNotPmExprOther :: PmExpr -> Bool
isNotPmExprOther :: PmExpr -> Bool
isNotPmExprOther (PmExprOther _) = Bool
False
isNotPmExprOther _expr :: PmExpr
_expr           = Bool
True

-- | Check whether a literal is negated
isNegatedPmLit :: PmLit -> Bool
isNegatedPmLit :: PmLit -> Bool
isNegatedPmLit (PmOLit b :: Bool
b _) = Bool
b
isNegatedPmLit _other_lit :: PmLit
_other_lit   = Bool
False

-- | Check whether a PmExpr is syntactically equal to term `True'.
isTruePmExpr :: PmExpr -> Bool
isTruePmExpr :: PmExpr -> Bool
isTruePmExpr (PmExprCon c :: ConLike
c []) = ConLike
c ConLike -> ConLike -> Bool
forall a. Eq a => a -> a -> Bool
== DataCon -> ConLike
RealDataCon DataCon
trueDataCon
isTruePmExpr _other_expr :: PmExpr
_other_expr      = Bool
False

-- | Check whether a PmExpr is syntactically equal to term `False'.
isFalsePmExpr :: PmExpr -> Bool
isFalsePmExpr :: PmExpr -> Bool
isFalsePmExpr (PmExprCon c :: ConLike
c []) = ConLike
c ConLike -> ConLike -> Bool
forall a. Eq a => a -> a -> Bool
== DataCon -> ConLike
RealDataCon DataCon
falseDataCon
isFalsePmExpr _other_expr :: PmExpr
_other_expr      = Bool
False

-- | Check whether a PmExpr is syntactically e
isNilPmExpr :: PmExpr -> Bool
isNilPmExpr :: PmExpr -> Bool
isNilPmExpr (PmExprCon c :: ConLike
c _) = ConLike
c ConLike -> ConLike -> Bool
forall a. Eq a => a -> a -> Bool
== DataCon -> ConLike
RealDataCon DataCon
nilDataCon
isNilPmExpr _other_expr :: PmExpr
_other_expr     = Bool
False

-- | Check whether a PmExpr is syntactically equal to (x == y).
-- Since (==) is overloaded and can have an arbitrary implementation, we use
-- the PmExprEq constructor to represent only equalities with non-overloaded
-- literals where it coincides with a syntactic equality check.
isPmExprEq :: PmExpr -> Maybe (PmExpr, PmExpr)
isPmExprEq :: PmExpr -> Maybe ComplexEq
isPmExprEq (PmExprEq e1 :: PmExpr
e1 e2 :: PmExpr
e2) = ComplexEq -> Maybe ComplexEq
forall a. a -> Maybe a
Just (PmExpr
e1,PmExpr
e2)
isPmExprEq _other_expr :: PmExpr
_other_expr      = Maybe ComplexEq
forall a. Maybe a
Nothing

-- | Check if a DataCon is (:).
isConsDataCon :: DataCon -> Bool
isConsDataCon :: DataCon -> Bool
isConsDataCon con :: DataCon
con = DataCon
consDataCon DataCon -> DataCon -> Bool
forall a. Eq a => a -> a -> Bool
== DataCon
con

-- ----------------------------------------------------------------------------
-- ** Substitution in PmExpr

-- | We return a boolean along with the expression. Hence, if substitution was
-- a no-op, we know that the expression still cannot progress.
substPmExpr :: Name -> PmExpr -> PmExpr -> (PmExpr, Bool)
substPmExpr :: Name -> PmExpr -> PmExpr -> (PmExpr, Bool)
substPmExpr x :: Name
x e1 :: PmExpr
e1 e :: PmExpr
e =
  case PmExpr
e of
    PmExprVar z :: Name
z | Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
z    -> (PmExpr
e1, Bool
True)
                | Bool
otherwise -> (PmExpr
e, Bool
False)
    PmExprCon c :: ConLike
c ps :: [PmExpr]
ps -> let (ps' :: [PmExpr]
ps', bs :: [Bool]
bs) = (PmExpr -> (PmExpr, Bool)) -> [PmExpr] -> ([PmExpr], [Bool])
forall a b c. (a -> (b, c)) -> [a] -> ([b], [c])
mapAndUnzip (Name -> PmExpr -> PmExpr -> (PmExpr, Bool)
substPmExpr Name
x PmExpr
e1) [PmExpr]
ps
                      in  (ConLike -> [PmExpr] -> PmExpr
PmExprCon ConLike
c [PmExpr]
ps', [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Bool]
bs)
    PmExprEq ex :: PmExpr
ex ey :: PmExpr
ey -> let (ex' :: PmExpr
ex', bx :: Bool
bx) = Name -> PmExpr -> PmExpr -> (PmExpr, Bool)
substPmExpr Name
x PmExpr
e1 PmExpr
ex
                          (ey' :: PmExpr
ey', by :: Bool
by) = Name -> PmExpr -> PmExpr -> (PmExpr, Bool)
substPmExpr Name
x PmExpr
e1 PmExpr
ey
                      in  (PmExpr -> PmExpr -> PmExpr
PmExprEq PmExpr
ex' PmExpr
ey', Bool
bx Bool -> Bool -> Bool
|| Bool
by)
    _other_expr :: PmExpr
_other_expr    -> (PmExpr
e, Bool
False) -- The rest are terminals (We silently ignore
                                 -- Other). See Note [PmExprOther in PmExpr]

-- | Substitute in a complex equality. We return (Left eq) if the substitution
-- affected the equality or (Right eq) if nothing happened.
substComplexEq :: Name -> PmExpr -> ComplexEq -> Either ComplexEq ComplexEq
substComplexEq :: Name -> PmExpr -> ComplexEq -> Either ComplexEq ComplexEq
substComplexEq x :: Name
x e :: PmExpr
e (ex :: PmExpr
ex, ey :: PmExpr
ey)
  | Bool
bx Bool -> Bool -> Bool
|| Bool
by  = ComplexEq -> Either ComplexEq ComplexEq
forall a b. a -> Either a b
Left  (PmExpr
ex', PmExpr
ey')
  | Bool
otherwise = ComplexEq -> Either ComplexEq ComplexEq
forall a b. b -> Either a b
Right (PmExpr
ex', PmExpr
ey')
  where
    (ex' :: PmExpr
ex', bx :: Bool
bx) = Name -> PmExpr -> PmExpr -> (PmExpr, Bool)
substPmExpr Name
x PmExpr
e PmExpr
ex
    (ey' :: PmExpr
ey', by :: Bool
by) = Name -> PmExpr -> PmExpr -> (PmExpr, Bool)
substPmExpr Name
x PmExpr
e PmExpr
ey

-- -----------------------------------------------------------------------
-- ** Lift source expressions (HsExpr Id) to PmExpr

lhsExprToPmExpr :: LHsExpr GhcTc -> PmExpr
lhsExprToPmExpr :: LHsExpr GhcTc -> PmExpr
lhsExprToPmExpr (LHsExpr GhcTc -> Located (SrcSpanLess (LHsExpr GhcTc))
forall a. HasSrcSpan a => a -> Located (SrcSpanLess a)
dL->L _ e :: SrcSpanLess (LHsExpr GhcTc)
e) = HsExpr GhcTc -> PmExpr
hsExprToPmExpr SrcSpanLess (LHsExpr GhcTc)
HsExpr GhcTc
e

hsExprToPmExpr :: HsExpr GhcTc -> PmExpr

hsExprToPmExpr :: HsExpr GhcTc -> PmExpr
hsExprToPmExpr (HsVar        _ x :: Located (IdP GhcTc)
x) = Name -> PmExpr
PmExprVar (Id -> Name
idName (Located Id -> SrcSpanLess (Located Id)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc Located Id
Located (IdP GhcTc)
x))
hsExprToPmExpr (HsConLikeOut _ c :: ConLike
c) = Name -> PmExpr
PmExprVar (ConLike -> Name
conLikeName ConLike
c)

-- Desugar literal strings as a list of characters. For other literal values,
-- keep it as it is.
-- See `translatePat` in Check.hs (the `NPat` and `LitPat` case), and
-- Note [Translate Overloaded Literal for Exhaustiveness Checking].
hsExprToPmExpr (HsOverLit _ olit :: HsOverLit GhcTc
olit)
  | OverLit (OverLitTc False ty) (HsIsString src :: SourceText
src s :: FastString
s) _ <- HsOverLit GhcTc
olit, Type -> Bool
isStringTy Type
ty
  = SourceText -> FastString -> PmExpr
stringExprToList SourceText
src FastString
s
  | Bool
otherwise = PmLit -> PmExpr
PmExprLit (Bool -> HsOverLit GhcTc -> PmLit
PmOLit Bool
False HsOverLit GhcTc
olit)
hsExprToPmExpr (HsLit     _ lit :: HsLit GhcTc
lit)
  | HsString src :: XHsString GhcTc
src s :: FastString
s <- HsLit GhcTc
lit
  = SourceText -> FastString -> PmExpr
stringExprToList SourceText
XHsString GhcTc
src FastString
s
  | Bool
otherwise = PmLit -> PmExpr
PmExprLit (HsLit GhcTc -> PmLit
PmSLit HsLit GhcTc
lit)

hsExprToPmExpr e :: HsExpr GhcTc
e@(NegApp _ (LHsExpr GhcTc -> Located (SrcSpanLess (LHsExpr GhcTc))
forall a. HasSrcSpan a => a -> Located (SrcSpanLess a)
dL->L _ neg_expr :: SrcSpanLess (LHsExpr GhcTc)
neg_expr) _)
  | PmExprLit (PmOLit False olit :: HsOverLit GhcTc
olit) <- HsExpr GhcTc -> PmExpr
hsExprToPmExpr SrcSpanLess (LHsExpr GhcTc)
HsExpr GhcTc
neg_expr
    -- NB: DON'T simply @(NegApp (NegApp olit))@ as @x@. when extension
    -- @RebindableSyntax@ enabled, (-(-x)) may not equals to x.
  = PmLit -> PmExpr
PmExprLit (Bool -> HsOverLit GhcTc -> PmLit
PmOLit Bool
True HsOverLit GhcTc
olit)
  | Bool
otherwise = HsExpr GhcTc -> PmExpr
PmExprOther HsExpr GhcTc
e

hsExprToPmExpr (HsPar _ (LHsExpr GhcTc -> Located (SrcSpanLess (LHsExpr GhcTc))
forall a. HasSrcSpan a => a -> Located (SrcSpanLess a)
dL->L _ e :: SrcSpanLess (LHsExpr GhcTc)
e)) = HsExpr GhcTc -> PmExpr
hsExprToPmExpr SrcSpanLess (LHsExpr GhcTc)
HsExpr GhcTc
e

hsExprToPmExpr e :: HsExpr GhcTc
e@(ExplicitTuple _ ps :: [LHsTupArg GhcTc]
ps boxity :: Boxity
boxity)
  | (LHsTupArg GhcTc -> Bool) -> [LHsTupArg GhcTc] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all LHsTupArg GhcTc -> Bool
forall id. LHsTupArg id -> Bool
tupArgPresent [LHsTupArg GhcTc]
ps = DataCon -> [PmExpr] -> PmExpr
mkPmExprData DataCon
tuple_con [PmExpr]
tuple_args
  | Bool
otherwise            = HsExpr GhcTc -> PmExpr
PmExprOther HsExpr GhcTc
e
  where
    tuple_con :: DataCon
tuple_con  = Boxity -> Arity -> DataCon
tupleDataCon Boxity
boxity ([LHsTupArg GhcTc] -> Arity
forall (t :: * -> *) a. Foldable t => t a -> Arity
length [LHsTupArg GhcTc]
ps)
    tuple_args :: [PmExpr]
tuple_args = [ LHsExpr GhcTc -> PmExpr
lhsExprToPmExpr LHsExpr GhcTc
e | (LHsTupArg GhcTc -> Located (SrcSpanLess (LHsTupArg GhcTc))
forall a. HasSrcSpan a => a -> Located (SrcSpanLess a)
dL->L _ (Present _ e)) <- [LHsTupArg GhcTc]
ps ]

hsExprToPmExpr e :: HsExpr GhcTc
e@(ExplicitList _  mb_ol :: Maybe (SyntaxExpr GhcTc)
mb_ol elems :: [LHsExpr GhcTc]
elems)
  | Maybe (SyntaxExpr GhcTc)
Nothing <- Maybe (SyntaxExpr GhcTc)
mb_ol = (PmExpr -> PmExpr -> PmExpr) -> PmExpr -> [PmExpr] -> PmExpr
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr PmExpr -> PmExpr -> PmExpr
cons PmExpr
nil ((LHsExpr GhcTc -> PmExpr) -> [LHsExpr GhcTc] -> [PmExpr]
forall a b. (a -> b) -> [a] -> [b]
map LHsExpr GhcTc -> PmExpr
lhsExprToPmExpr [LHsExpr GhcTc]
elems)
  | Bool
otherwise        = HsExpr GhcTc -> PmExpr
PmExprOther HsExpr GhcTc
e {- overloaded list: No PmExprApp -}
  where
    cons :: PmExpr -> PmExpr -> PmExpr
cons x :: PmExpr
x xs :: PmExpr
xs = DataCon -> [PmExpr] -> PmExpr
mkPmExprData DataCon
consDataCon [PmExpr
x,PmExpr
xs]
    nil :: PmExpr
nil       = DataCon -> [PmExpr] -> PmExpr
mkPmExprData DataCon
nilDataCon  []

-- we want this but we would have to make everything monadic :/
-- ./compiler/deSugar/DsMonad.hs:397:dsLookupDataCon :: Name -> DsM DataCon
--
-- hsExprToPmExpr (RecordCon   c _ binds) = do
--   con  <- dsLookupDataCon (unLoc c)
--   args <- mapM lhsExprToPmExpr (hsRecFieldsArgs binds)
--   return (PmExprCon con args)
hsExprToPmExpr e :: HsExpr GhcTc
e@(RecordCon {}) = HsExpr GhcTc -> PmExpr
PmExprOther HsExpr GhcTc
e

hsExprToPmExpr (HsTick           _ _ e :: LHsExpr GhcTc
e) = LHsExpr GhcTc -> PmExpr
lhsExprToPmExpr LHsExpr GhcTc
e
hsExprToPmExpr (HsBinTick      _ _ _ e :: LHsExpr GhcTc
e) = LHsExpr GhcTc -> PmExpr
lhsExprToPmExpr LHsExpr GhcTc
e
hsExprToPmExpr (HsTickPragma _ _ _ _ e :: LHsExpr GhcTc
e) = LHsExpr GhcTc -> PmExpr
lhsExprToPmExpr LHsExpr GhcTc
e
hsExprToPmExpr (HsSCC          _ _ _ e :: LHsExpr GhcTc
e) = LHsExpr GhcTc -> PmExpr
lhsExprToPmExpr LHsExpr GhcTc
e
hsExprToPmExpr (HsCoreAnn      _ _ _ e :: LHsExpr GhcTc
e) = LHsExpr GhcTc -> PmExpr
lhsExprToPmExpr LHsExpr GhcTc
e
hsExprToPmExpr (ExprWithTySig    _ e :: LHsExpr GhcTc
e _) = LHsExpr GhcTc -> PmExpr
lhsExprToPmExpr LHsExpr GhcTc
e
hsExprToPmExpr (HsWrap           _ _ e :: HsExpr GhcTc
e) =  HsExpr GhcTc -> PmExpr
hsExprToPmExpr HsExpr GhcTc
e
hsExprToPmExpr e :: HsExpr GhcTc
e = HsExpr GhcTc -> PmExpr
PmExprOther HsExpr GhcTc
e -- the rest are not handled by the oracle

stringExprToList :: SourceText -> FastString -> PmExpr
stringExprToList :: SourceText -> FastString -> PmExpr
stringExprToList src :: SourceText
src s :: FastString
s = (PmExpr -> PmExpr -> PmExpr) -> PmExpr -> [PmExpr] -> PmExpr
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr PmExpr -> PmExpr -> PmExpr
cons PmExpr
nil ((Char -> PmExpr) -> [Char] -> [PmExpr]
forall a b. (a -> b) -> [a] -> [b]
map Char -> PmExpr
charToPmExpr (FastString -> [Char]
unpackFS FastString
s))
  where
    cons :: PmExpr -> PmExpr -> PmExpr
cons x :: PmExpr
x xs :: PmExpr
xs      = DataCon -> [PmExpr] -> PmExpr
mkPmExprData DataCon
consDataCon [PmExpr
x,PmExpr
xs]
    nil :: PmExpr
nil            = DataCon -> [PmExpr] -> PmExpr
mkPmExprData DataCon
nilDataCon  []
    charToPmExpr :: Char -> PmExpr
charToPmExpr c :: Char
c = PmLit -> PmExpr
PmExprLit (HsLit GhcTc -> PmLit
PmSLit (XHsChar GhcTc -> Char -> HsLit GhcTc
forall x. XHsChar x -> Char -> HsLit x
HsChar SourceText
XHsChar GhcTc
src Char
c))

{-
%************************************************************************
%*                                                                      *
                            Pretty printing
%*                                                                      *
%************************************************************************
-}

{- 1. Literals
~~~~~~~~~~~~~~
Starting with a function definition like:

    f :: Int -> Bool
    f 5 = True
    f 6 = True

The uncovered set looks like:
    { var |> False == (var == 5), False == (var == 6) }

Yet, we would like to print this nicely as follows:
   x , where x not one of {5,6}

Function `filterComplex' takes the set of residual constraints and packs
together the negative constraints that refer to the same variable so we can do
just this. Since these variables will be shown to the programmer, we also give
them better names (t1, t2, ..), hence the SDoc in PmNegLitCt.

2. Residual Constraints
~~~~~~~~~~~~~~~~~~~~~~~
Unhandled constraints that refer to HsExpr are typically ignored by the solver
(it does not even substitute in HsExpr so they are even printed as wildcards).
Additionally, the oracle returns a substitution if it succeeds so we apply this
substitution to the vectors before printing them out (see function `pprOne' in
Check.hs) to be more precice.
-}

-- -----------------------------------------------------------------------------
-- ** Transform residual constraints in appropriate form for pretty printing

type PmNegLitCt = (Name, (SDoc, [PmLit]))

filterComplex :: [ComplexEq] -> [PmNegLitCt]
filterComplex :: [ComplexEq] -> [PmNegLitCt]
filterComplex = (SDoc -> (Name, [PmLit]) -> PmNegLitCt)
-> [SDoc] -> [(Name, [PmLit])] -> [PmNegLitCt]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith SDoc -> (Name, [PmLit]) -> PmNegLitCt
forall a a b. a -> (a, b) -> (a, (a, b))
rename [SDoc]
nameList ([(Name, [PmLit])] -> [PmNegLitCt])
-> ([ComplexEq] -> [(Name, [PmLit])])
-> [ComplexEq]
-> [PmNegLitCt]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([(Name, PmLit)] -> (Name, [PmLit]))
-> [[(Name, PmLit)]] -> [(Name, [PmLit])]
forall a b. (a -> b) -> [a] -> [b]
map [(Name, PmLit)] -> (Name, [PmLit])
forall a. [(a, PmLit)] -> (a, [PmLit])
mkGroup
              ([[(Name, PmLit)]] -> [(Name, [PmLit])])
-> ([ComplexEq] -> [[(Name, PmLit)]])
-> [ComplexEq]
-> [(Name, [PmLit])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Name, PmLit) -> (Name, PmLit) -> Bool)
-> [(Name, PmLit)] -> [[(Name, PmLit)]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (Name, PmLit) -> (Name, PmLit) -> Bool
forall a b b. Eq a => (a, b) -> (a, b) -> Bool
name ([(Name, PmLit)] -> [[(Name, PmLit)]])
-> ([ComplexEq] -> [(Name, PmLit)])
-> [ComplexEq]
-> [[(Name, PmLit)]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Name, PmLit) -> (Name, PmLit) -> Ordering)
-> [(Name, PmLit)] -> [(Name, PmLit)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Name, PmLit) -> (Name, PmLit) -> Ordering
forall a b b. Ord a => (a, b) -> (a, b) -> Ordering
order ([(Name, PmLit)] -> [(Name, PmLit)])
-> ([ComplexEq] -> [(Name, PmLit)])
-> [ComplexEq]
-> [(Name, PmLit)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ComplexEq -> Maybe (Name, PmLit))
-> [ComplexEq] -> [(Name, PmLit)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ComplexEq -> Maybe (Name, PmLit)
isNegLitCs
  where
    order :: (a, b) -> (a, b) -> Ordering
order x :: (a, b)
x y :: (a, b)
y = a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ((a, b) -> a
forall a b. (a, b) -> a
fst (a, b)
x) ((a, b) -> a
forall a b. (a, b) -> a
fst (a, b)
y)
    name :: (a, b) -> (a, b) -> Bool
name  x :: (a, b)
x y :: (a, b)
y = (a, b) -> a
forall a b. (a, b) -> a
fst (a, b)
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== (a, b) -> a
forall a b. (a, b) -> a
fst (a, b)
y
    mkGroup :: [(a, PmLit)] -> (a, [PmLit])
mkGroup l :: [(a, PmLit)]
l = ((a, PmLit) -> a
forall a b. (a, b) -> a
fst ([(a, PmLit)] -> (a, PmLit)
forall a. [a] -> a
head [(a, PmLit)]
l), [PmLit] -> [PmLit]
nubPmLit ([PmLit] -> [PmLit]) -> [PmLit] -> [PmLit]
forall a b. (a -> b) -> a -> b
$ ((a, PmLit) -> PmLit) -> [(a, PmLit)] -> [PmLit]
forall a b. (a -> b) -> [a] -> [b]
map (a, PmLit) -> PmLit
forall a b. (a, b) -> b
snd [(a, PmLit)]
l)
    rename :: a -> (a, b) -> (a, (a, b))
rename new :: a
new (old :: a
old, lits :: b
lits) = (a
old, (a
new, b
lits))

    isNegLitCs :: ComplexEq -> Maybe (Name, PmLit)
isNegLitCs (e1 :: PmExpr
e1,e2 :: PmExpr
e2)
      | PmExpr -> Bool
isFalsePmExpr PmExpr
e1, Just (x :: PmExpr
x,y :: PmExpr
y) <- PmExpr -> Maybe ComplexEq
isPmExprEq PmExpr
e2 = PmExpr -> PmExpr -> Maybe (Name, PmLit)
isNegLitCs' PmExpr
x PmExpr
y
      | PmExpr -> Bool
isFalsePmExpr PmExpr
e2, Just (x :: PmExpr
x,y :: PmExpr
y) <- PmExpr -> Maybe ComplexEq
isPmExprEq PmExpr
e1 = PmExpr -> PmExpr -> Maybe (Name, PmLit)
isNegLitCs' PmExpr
x PmExpr
y
      | Bool
otherwise = Maybe (Name, PmLit)
forall a. Maybe a
Nothing

    isNegLitCs' :: PmExpr -> PmExpr -> Maybe (Name, PmLit)
isNegLitCs' (PmExprVar x :: Name
x) (PmExprLit l :: PmLit
l) = (Name, PmLit) -> Maybe (Name, PmLit)
forall a. a -> Maybe a
Just (Name
x, PmLit
l)
    isNegLitCs' (PmExprLit l :: PmLit
l) (PmExprVar x :: Name
x) = (Name, PmLit) -> Maybe (Name, PmLit)
forall a. a -> Maybe a
Just (Name
x, PmLit
l)
    isNegLitCs' _ _             = Maybe (Name, PmLit)
forall a. Maybe a
Nothing

    -- Try nice names p,q,r,s,t before using the (ugly) t_i
    nameList :: [SDoc]
    nameList :: [SDoc]
nameList = ([Char] -> SDoc) -> [[Char]] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map [Char] -> SDoc
text ["p","q","r","s","t"] [SDoc] -> [SDoc] -> [SDoc]
forall a. [a] -> [a] -> [a]
++
                 [ [Char] -> SDoc
text ('t'Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
:Arity -> [Char]
forall a. Show a => a -> [Char]
show Arity
u) | Arity
u <- [(0 :: Int)..] ]

-- ----------------------------------------------------------------------------

runPmPprM :: PmPprM a -> [PmNegLitCt] -> (a, [(SDoc,[PmLit])])
runPmPprM :: PmPprM a -> [PmNegLitCt] -> (a, [(SDoc, [PmLit])])
runPmPprM m :: PmPprM a
m lit_env :: [PmNegLitCt]
lit_env = (a
result, (PmNegLitCt -> Maybe (SDoc, [PmLit]))
-> [PmNegLitCt] -> [(SDoc, [PmLit])]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe PmNegLitCt -> Maybe (SDoc, [PmLit])
forall a b. (Name, (a, b)) -> Maybe (a, b)
is_used [PmNegLitCt]
lit_env)
  where
    (result :: a
result, (_lit_env :: [PmNegLitCt]
_lit_env, used :: NameSet
used)) = PmPprM a -> ([PmNegLitCt], NameSet) -> (a, ([PmNegLitCt], NameSet))
forall s a. State s a -> s -> (a, s)
runState PmPprM a
m ([PmNegLitCt]
lit_env, NameSet
emptyNameSet)

    is_used :: (Name, (a, b)) -> Maybe (a, b)
is_used (x :: Name
x,(name :: a
name, lits :: b
lits))
      | Name -> NameSet -> Bool
elemNameSet Name
x NameSet
used = (a, b) -> Maybe (a, b)
forall a. a -> Maybe a
Just (a
name, b
lits)
      | Bool
otherwise         = Maybe (a, b)
forall a. Maybe a
Nothing

type PmPprM a = State ([PmNegLitCt], NameSet) a
-- (the first part of the state is read only. make it a reader?)

addUsed :: Name -> PmPprM ()
addUsed :: Name -> PmPprM ()
addUsed x :: Name
x = (([PmNegLitCt], NameSet) -> ([PmNegLitCt], NameSet)) -> PmPprM ()
forall (m :: * -> *) s. Monad m => (s -> s) -> StateT s m ()
modify (\(negated :: [PmNegLitCt]
negated, used :: NameSet
used) -> ([PmNegLitCt]
negated, NameSet -> Name -> NameSet
extendNameSet NameSet
used Name
x))

checkNegation :: Name -> PmPprM (Maybe SDoc) -- the clean name if it is negated
checkNegation :: Name -> PmPprM (Maybe SDoc)
checkNegation x :: Name
x = do
  [PmNegLitCt]
negated <- (([PmNegLitCt], NameSet) -> [PmNegLitCt])
-> StateT ([PmNegLitCt], NameSet) Identity [PmNegLitCt]
forall (m :: * -> *) s a. Monad m => (s -> a) -> StateT s m a
gets ([PmNegLitCt], NameSet) -> [PmNegLitCt]
forall a b. (a, b) -> a
fst
  Maybe SDoc -> PmPprM (Maybe SDoc)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe SDoc -> PmPprM (Maybe SDoc))
-> Maybe SDoc -> PmPprM (Maybe SDoc)
forall a b. (a -> b) -> a -> b
$ case Name -> [PmNegLitCt] -> Maybe (SDoc, [PmLit])
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
x [PmNegLitCt]
negated of
    Just (new :: SDoc
new, _) -> SDoc -> Maybe SDoc
forall a. a -> Maybe a
Just SDoc
new
    Nothing       -> Maybe SDoc
forall a. Maybe a
Nothing

-- | Pretty print a pmexpr, but remember to prettify the names of the variables
-- that refer to neg-literals. The ones that cannot be shown are printed as
-- underscores.
pprPmExpr :: PmExpr -> PmPprM SDoc
pprPmExpr :: PmExpr -> PmPprM SDoc
pprPmExpr (PmExprVar x :: Name
x) = do
  Maybe SDoc
mb_name <- Name -> PmPprM (Maybe SDoc)
checkNegation Name
x
  case Maybe SDoc
mb_name of
    Just name :: SDoc
name -> Name -> PmPprM ()
addUsed Name
x PmPprM () -> PmPprM SDoc -> PmPprM SDoc
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SDoc -> PmPprM SDoc
forall (m :: * -> *) a. Monad m => a -> m a
return SDoc
name
    Nothing   -> SDoc -> PmPprM SDoc
forall (m :: * -> *) a. Monad m => a -> m a
return SDoc
underscore

pprPmExpr (PmExprCon con :: ConLike
con args :: [PmExpr]
args) = ConLike -> [PmExpr] -> PmPprM SDoc
pprPmExprCon ConLike
con [PmExpr]
args
pprPmExpr (PmExprLit l :: PmLit
l)        = SDoc -> PmPprM SDoc
forall (m :: * -> *) a. Monad m => a -> m a
return (PmLit -> SDoc
forall a. Outputable a => a -> SDoc
ppr PmLit
l)
pprPmExpr (PmExprEq _ _)       = SDoc -> PmPprM SDoc
forall (m :: * -> *) a. Monad m => a -> m a
return SDoc
underscore -- don't show
pprPmExpr (PmExprOther _)      = SDoc -> PmPprM SDoc
forall (m :: * -> *) a. Monad m => a -> m a
return SDoc
underscore -- don't show

needsParens :: PmExpr -> Bool
needsParens :: PmExpr -> Bool
needsParens (PmExprVar   {}) = Bool
False
needsParens (PmExprLit    l :: PmLit
l) = PmLit -> Bool
isNegatedPmLit PmLit
l
needsParens (PmExprEq    {}) = Bool
False -- will become a wildcard
needsParens (PmExprOther {}) = Bool
False -- will become a wildcard
needsParens (PmExprCon (RealDataCon c :: DataCon
c) es :: [PmExpr]
es)
  | DataCon -> Bool
isTupleDataCon DataCon
c
  Bool -> Bool -> Bool
|| DataCon -> Bool
isConsDataCon DataCon
c Bool -> Bool -> Bool
|| [PmExpr] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PmExpr]
es = Bool
False
  | Bool
otherwise                   = Bool
True
needsParens (PmExprCon (PatSynCon _) es :: [PmExpr]
es) = Bool -> Bool
not ([PmExpr] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PmExpr]
es)

pprPmExprWithParens :: PmExpr -> PmPprM SDoc
pprPmExprWithParens :: PmExpr -> PmPprM SDoc
pprPmExprWithParens expr :: PmExpr
expr
  | PmExpr -> Bool
needsParens PmExpr
expr = SDoc -> SDoc
parens (SDoc -> SDoc) -> PmPprM SDoc -> PmPprM SDoc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PmExpr -> PmPprM SDoc
pprPmExpr PmExpr
expr
  | Bool
otherwise        =            PmExpr -> PmPprM SDoc
pprPmExpr PmExpr
expr

pprPmExprCon :: ConLike -> [PmExpr] -> PmPprM SDoc
pprPmExprCon :: ConLike -> [PmExpr] -> PmPprM SDoc
pprPmExprCon (RealDataCon con :: DataCon
con) args :: [PmExpr]
args
  | DataCon -> Bool
isTupleDataCon DataCon
con = [SDoc] -> SDoc
mkTuple ([SDoc] -> SDoc)
-> StateT ([PmNegLitCt], NameSet) Identity [SDoc] -> PmPprM SDoc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (PmExpr -> PmPprM SDoc)
-> [PmExpr] -> StateT ([PmNegLitCt], NameSet) Identity [SDoc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM PmExpr -> PmPprM SDoc
pprPmExpr [PmExpr]
args
  | DataCon -> Bool
isConsDataCon DataCon
con  = PmPprM SDoc
pretty_list
  where
    mkTuple :: [SDoc] -> SDoc
    mkTuple :: [SDoc] -> SDoc
mkTuple = SDoc -> SDoc
parens     (SDoc -> SDoc) -> ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SDoc] -> SDoc
fsep ([SDoc] -> SDoc) -> ([SDoc] -> [SDoc]) -> [SDoc] -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> [SDoc] -> [SDoc]
punctuate SDoc
comma

    -- lazily, to be used in the list case only
    pretty_list :: PmPprM SDoc
    pretty_list :: PmPprM SDoc
pretty_list = case PmExpr -> Bool
isNilPmExpr ([PmExpr] -> PmExpr
forall a. [a] -> a
last [PmExpr]
list) of
      True  -> SDoc -> SDoc
brackets (SDoc -> SDoc) -> ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SDoc] -> SDoc
fsep ([SDoc] -> SDoc) -> ([SDoc] -> [SDoc]) -> [SDoc] -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> [SDoc] -> [SDoc]
punctuate SDoc
comma ([SDoc] -> SDoc)
-> StateT ([PmNegLitCt], NameSet) Identity [SDoc] -> PmPprM SDoc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (PmExpr -> PmPprM SDoc)
-> [PmExpr] -> StateT ([PmNegLitCt], NameSet) Identity [SDoc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM PmExpr -> PmPprM SDoc
pprPmExpr ([PmExpr] -> [PmExpr]
forall a. [a] -> [a]
init [PmExpr]
list)
      False -> SDoc -> SDoc
parens   (SDoc -> SDoc) -> ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SDoc] -> SDoc
hcat ([SDoc] -> SDoc) -> ([SDoc] -> [SDoc]) -> [SDoc] -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> [SDoc] -> [SDoc]
punctuate SDoc
colon ([SDoc] -> SDoc)
-> StateT ([PmNegLitCt], NameSet) Identity [SDoc] -> PmPprM SDoc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (PmExpr -> PmPprM SDoc)
-> [PmExpr] -> StateT ([PmNegLitCt], NameSet) Identity [SDoc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM PmExpr -> PmPprM SDoc
pprPmExpr [PmExpr]
list

    list :: [PmExpr]
list = [PmExpr] -> [PmExpr]
list_elements [PmExpr]
args

    list_elements :: [PmExpr] -> [PmExpr]
list_elements [x :: PmExpr
x,y :: PmExpr
y]
      | PmExprCon c :: ConLike
c es :: [PmExpr]
es <- PmExpr
y,  DataCon -> ConLike
RealDataCon DataCon
nilDataCon ConLike -> ConLike -> Bool
forall a. Eq a => a -> a -> Bool
== ConLike
c
          = ASSERT(null es) [x,y]
      | PmExprCon c :: ConLike
c es :: [PmExpr]
es <- PmExpr
y, DataCon -> ConLike
RealDataCon DataCon
consDataCon ConLike -> ConLike -> Bool
forall a. Eq a => a -> a -> Bool
== ConLike
c
          = PmExpr
x PmExpr -> [PmExpr] -> [PmExpr]
forall a. a -> [a] -> [a]
: [PmExpr] -> [PmExpr]
list_elements [PmExpr]
es
      | Bool
otherwise = [PmExpr
x,PmExpr
y]
    list_elements list :: [PmExpr]
list  = [Char] -> SDoc -> [PmExpr]
forall a. HasCallStack => [Char] -> SDoc -> a
pprPanic "list_elements:" ([PmExpr] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [PmExpr]
list)
pprPmExprCon cl :: ConLike
cl args :: [PmExpr]
args
  | ConLike -> Bool
conLikeIsInfix ConLike
cl = case [PmExpr]
args of
      [x :: PmExpr
x, y :: PmExpr
y] -> do SDoc
x' <- PmExpr -> PmPprM SDoc
pprPmExprWithParens PmExpr
x
                   SDoc
y' <- PmExpr -> PmPprM SDoc
pprPmExprWithParens PmExpr
y
                   SDoc -> PmPprM SDoc
forall (m :: * -> *) a. Monad m => a -> m a
return (SDoc
x' SDoc -> SDoc -> SDoc
<+> ConLike -> SDoc
forall a. Outputable a => a -> SDoc
ppr ConLike
cl SDoc -> SDoc -> SDoc
<+> SDoc
y')
      -- can it be infix but have more than two arguments?
      list :: [PmExpr]
list   -> [Char] -> SDoc -> PmPprM SDoc
forall a. HasCallStack => [Char] -> SDoc -> a
pprPanic "pprPmExprCon:" ([PmExpr] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [PmExpr]
list)
  | [PmExpr] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PmExpr]
args = SDoc -> PmPprM SDoc
forall (m :: * -> *) a. Monad m => a -> m a
return (ConLike -> SDoc
forall a. Outputable a => a -> SDoc
ppr ConLike
cl)
  | Bool
otherwise = do [SDoc]
args' <- (PmExpr -> PmPprM SDoc)
-> [PmExpr] -> StateT ([PmNegLitCt], NameSet) Identity [SDoc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM PmExpr -> PmPprM SDoc
pprPmExprWithParens [PmExpr]
args
                   SDoc -> PmPprM SDoc
forall (m :: * -> *) a. Monad m => a -> m a
return ([SDoc] -> SDoc
fsep (ConLike -> SDoc
forall a. Outputable a => a -> SDoc
ppr ConLike
cl SDoc -> [SDoc] -> [SDoc]
forall a. a -> [a] -> [a]
: [SDoc]
args'))

instance Outputable PmLit where
  ppr :: PmLit -> SDoc
ppr (PmSLit     l :: HsLit GhcTc
l) = HsLit GhcTc -> SDoc
forall (x :: Pass). HsLit (GhcPass x) -> SDoc
pmPprHsLit HsLit GhcTc
l
  ppr (PmOLit neg :: Bool
neg l :: HsOverLit GhcTc
l) = (if Bool
neg then Char -> SDoc
char '-' else SDoc
empty) SDoc -> SDoc -> SDoc
<> HsOverLit GhcTc -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsOverLit GhcTc
l

-- not really useful for pmexprs per se
instance Outputable PmExpr where
  ppr :: PmExpr -> SDoc
ppr e :: PmExpr
e = (SDoc, [(SDoc, [PmLit])]) -> SDoc
forall a b. (a, b) -> a
fst ((SDoc, [(SDoc, [PmLit])]) -> SDoc)
-> (SDoc, [(SDoc, [PmLit])]) -> SDoc
forall a b. (a -> b) -> a -> b
$ PmPprM SDoc -> [PmNegLitCt] -> (SDoc, [(SDoc, [PmLit])])
forall a. PmPprM a -> [PmNegLitCt] -> (a, [(SDoc, [PmLit])])
runPmPprM (PmExpr -> PmPprM SDoc
pprPmExpr PmExpr
e) []