Commit 3534f4c7 authored by Sebastian Graf's avatar Sebastian Graf
Browse files

Encode refutable `ConLike`s in `TmOracle` for correct warnings in the presence of `COMPLETE` groups

Previously, we had an elaborate mechanism for selecting the warnings to
generate in the presence of different `COMPLETE` matching groups that,
albeit finely-tuned, produced wrong results from an end user's
perspective in some cases (#13363).

The underlying issue is that at the point where the `ConVar` case has to
commit to a particular `COMPLETE` group, there's not enough information
to do so and the status quo was to just enumerate all possible complete
sets nondeterministically.  The `getResult` function would then pick the
outcome according to metrics defined in accordance to the user's guide.
But crucially, it lacked knowledge about the order in which affected
clauses appear, leading to the surprising behavior in #13363.

In !1010 we taught the term oracle to reason about literal values a
variable can certainly not take on. This MR extends that idea to
`ConLike`s and thereby fixes #13363: Instead of committing to a
particular `COMPLETE` group in the `ConVar` case, we now split off the
matching constructor incrementally and record the newly covered case as
a refutable shape in the term oracle.  After all clauses have been
processed this way, we filter out any value vector abstractions from the
uncovered set involving variables whose set of covered constructors
completely overlap a `COMPLETE` set.
parent d2e290d3
Pipeline #8211 failed with stages
in 153 minutes and 37 seconds
......@@ -27,7 +27,7 @@ module NameEnv (
lookupDNameEnv,
delFromDNameEnv,
mapDNameEnv,
alterDNameEnv,
adjustDNameEnv, alterDNameEnv, extendDNameEnv_C,
-- ** Dependency analysis
depAnal
) where
......@@ -154,5 +154,11 @@ delFromDNameEnv = delFromUDFM
mapDNameEnv :: (a -> b) -> DNameEnv a -> DNameEnv b
mapDNameEnv = mapUDFM
adjustDNameEnv :: (a -> a) -> DNameEnv a -> Name -> DNameEnv a
adjustDNameEnv = adjustUDFM
alterDNameEnv :: (Maybe a -> Maybe a) -> DNameEnv a -> Name -> DNameEnv a
alterDNameEnv = alterUDFM
extendDNameEnv_C :: (a -> a -> a) -> DNameEnv a -> Name -> a -> DNameEnv a
extendDNameEnv_C = addToUDFM_C
This diff is collapsed.
......@@ -9,15 +9,17 @@ Haskell expressions (as used by the pattern matching checker) and utilities.
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module PmExpr (
PmExpr(..), PmLit(..), PmAltCon(..), TmVarCt(..),
eqPmLit, isNotPmExprOther, lhsExprToPmExpr, hsExprToPmExpr
PmExpr(..), PmLit(..), PmAltCon(..), TmVarCt(..), pmLitType,
isNotPmExprOther, hsOverLitAsHsLit, lhsExprToPmExpr, hsExprToPmExpr,
mkPmExprLit, decEqPmAltCon, PmExprList(..), pmExprAsList
) where
#include "HsVersions.h"
import GhcPrelude
import BasicTypes (SourceText)
import Util
import BasicTypes (SourceText, IntegralLit(..), negateIntegralLit)
import FastString (FastString, unpackFS)
import HsSyn
import Id
......@@ -25,10 +27,12 @@ import Name
import DataCon
import ConLike
import TcEvidence (isErasableHsWrapper)
import TcType (isStringTy)
import TcType (Type, eqType, isStringTy, isIntTy, isIntegerTy, isWordTy)
import TcHsSyn (hsLitType)
import TysWiredIn
import Outputable
import SrcLoc
import Data.List.NonEmpty (NonEmpty, nonEmpty, toList)
{-
%************************************************************************
......@@ -53,37 +57,86 @@ refer to variables that are otherwise substituted away.
-- | Lifted expressions for pattern match checking.
data PmExpr = PmExprVar Name
| PmExprCon ConLike [PmExpr]
| PmExprLit PmLit
| PmExprCon PmAltCon [PmExpr]
| PmExprOther (HsExpr GhcTc) -- Note [PmExprOther in PmExpr]
mkPmExprData :: DataCon -> [PmExpr] -> PmExpr
mkPmExprData dc args = PmExprCon (RealDataCon dc) args
-- | Literals (simple and overloaded ones) for pattern match checking.
--
-- See Note [Undecidable Equality for PmAltCons]
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 (PmSLit l1) (PmSLit l2) = l1 == l2
eqPmLit (PmOLit b1 l1) (PmOLit b2 l2) = b1 == b2 && l1 == l2
-- See Note [Undecidable Equality for Overloaded Literals]
eqPmLit _ _ = False
-- | Represents a match against a literal. We mostly use it to to encode shapes
-- for a variable that immediately lead to a refutation.
-- | Undecidable equality for values represented by 'PmLit's.
-- See Note [Undecidable Equality for PmAltCons]
--
-- * @Just True@ ==> Surely equal
-- * @Just False@ ==> Surely different (non-overlapping, even!)
-- * @Nothing@ ==> Equality relation undecidable
decEqPmLit :: PmLit -> PmLit -> Maybe Bool
decEqPmLit (PmSLit l1) (PmSLit l2) = Just (l1 == l2)
decEqPmLit (PmOLit b1 l1) (PmOLit b2 l2)
| b1 == b2, l1 == l2
= Just True
decEqPmLit _ _ = Nothing
-- | Syntactic equality.
instance Eq PmLit where
a == b = decEqPmLit a b == Just True
-- | Type of a PmLit
pmLitType :: PmLit -> Type
pmLitType (PmSLit lit) = hsLitType lit
pmLitType (PmOLit _ lit) = overLitType lit
-- | Undecidable equality for values represented by 'ConLike's.
-- See Note [Undecidable Equality for PmAltCons].
-- 'PatSynCon's aren't enforced to be generative, so two syntactically different
-- 'PatSynCon's might match the exact same values. Without looking into and
-- reasoning about the pattern synonym's definition, we can't decide if their
-- sets of matched values is different.
--
-- * @Just True@ ==> Surely equal
-- * @Just False@ ==> Surely different (non-overlapping, even!)
-- * @Nothing@ ==> Equality relation undecidable
decEqConLike :: ConLike -> ConLike -> Maybe Bool
decEqConLike (RealDataCon dc1) (RealDataCon dc2) = Just (dc1 == dc2)
decEqConLike (PatSynCon psc1) (PatSynCon psc2)
| psc1 == psc2
= Just True
decEqConLike _ _ = Nothing
-- | Represents a match against a 'ConLike' or literal. We mostly use it to
-- to encode shapes for a variable that immediately lead to a refutation.
--
-- See Note [Refutable shapes] in TmOracle. Really similar to 'CoreSyn.AltCon'.
newtype PmAltCon = PmAltLit PmLit
deriving Outputable
data PmAltCon = PmAltConLike ConLike
| PmAltLit PmLit
-- | We can't in general decide whether two 'PmAltCon's match the same set of
-- values. In addition to the reasons in 'decEqPmLit' and 'decEqConLike', a
-- 'PmAltConLike' might or might not represent the same value as a 'PmAltLit'.
-- See Note [Undecidable Equality for PmAltCons].
--
-- * @Just True@ ==> Surely equal
-- * @Just False@ ==> Surely different (non-overlapping, even!)
-- * @Nothing@ ==> Equality relation undecidable
decEqPmAltCon :: PmAltCon -> PmAltCon -> Maybe Bool
decEqPmAltCon (PmAltConLike cl1) (PmAltConLike cl2) = decEqConLike cl1 cl2
decEqPmAltCon (PmAltLit l1) (PmAltLit l2) = decEqPmLit l1 l2
decEqPmAltCon _ _ = Nothing
-- | Syntactic equality.
instance Eq PmAltCon where
PmAltLit l1 == PmAltLit l2 = eqPmLit l1 l2
a == b = decEqPmAltCon a b == Just True
mkPmExprData :: DataCon -> [PmExpr] -> PmExpr
mkPmExprData dc args = PmExprCon (PmAltConLike (RealDataCon dc)) args
mkPmExprLit :: PmLit -> PmExpr
mkPmExprLit l = PmExprCon (PmAltLit l) []
{- Note [Undecidable Equality for Overloaded Literals]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
{- Note [Undecidable Equality for PmAltCons]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Equality on overloaded literals is undecidable in the general case. Consider
the following example:
......@@ -96,25 +149,19 @@ the following example:
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
Clause B is redundant but to detect this, we must decide the constraint:
@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
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
2. Error messages/Warnings.
What should our message for @f@ above be? A reasonable approach would be
to issue:
Pattern matches are (potentially) redundant:
......@@ -122,8 +169,13 @@ be anything. This poses difficulties for:
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:
We choose to equate only obviously equal overloaded literals, in all other cases
we signal undecidability by returning Nothing from 'decEqPmAltCons'. We do
better for non-overloaded literals, because we know their fromInteger/fromString
implementation is actually injective, allowing us to simplify the constraint
@fromInteger 1 ~ fromInteger 2@ to @1 ~ 2@, which is trivially unsatisfiable.
The impact of this treatment of overloaded literals is the following:
* Redundancy checking is rather conservative, since it cannot see that clause
B above is redundant.
......@@ -136,16 +188,9 @@ impact of this is the following:
* 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.
Similar reasoning applies to pattern synonyms: In contrast to data constructors,
which are generative, constraints like F a ~ G b for two different pattern
synonyms F and G aren't immediately unsatisfiable. We know F a ~ F a, though.
-}
-- | A term constraint. @TVC x e@ encodes that @x@ is equal to @e@.
......@@ -165,6 +210,96 @@ isNotPmExprOther _expr = True
-- -----------------------------------------------------------------------
-- ** Lift source expressions (HsExpr Id) to PmExpr
-- | Mimics 'MatchLit.tidyNPat', but solely for purposes of better pattern match
-- warnings. See Note [Translate Overloaded Literals for Exhaustiveness Checking]
hsOverLitAsHsLit :: HsOverLit GhcTc -> Bool -> Type -> Maybe (HsLit GhcTc)
hsOverLitAsHsLit (OverLit (OverLitTc False ty) val _) negated outer_ty
| types_equal, isStringTy ty, HsIsString src s <- val, not negated
= Just (HsString src s)
| types_equal, isIntTy ty, HsIntegral i <- val
= Just (HsInt noExtField (apply_negation i))
| types_equal, isWordTy ty, HsIntegral i <- val
, let ni = apply_negation i
-- this is a type error... But as long as we do this consistently, this
-- shouldn't be a problem. The proper solution would be to return a HsExpr,
-- but that would require non-trivial boilerplate at the two call sites.
= Just (HsWordPrim (il_text ni) (il_value ni))
| types_equal, isIntegerTy ty, HsIntegral i <- val
, let ni = apply_negation i
= Just (HsInteger (il_text ni) (il_value ni) ty)
where
types_equal = eqType outer_ty ty
apply_negation
| negated = negateIntegralLit
| otherwise = id
hsOverLitAsHsLit _ _ _ = Nothing
{- Note [Translate Overloaded Literals for Exhaustiveness Checking]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Due to Note [Undecidable Equality for PmAltCons], the exhaustiveness checker can
do a much better job for primitive literals than for overloaded literals. So,
ideally, we'd run exhaustiveness checks /after/ we had translated part of the
overloaded literals ('HsOverLit') to their primitive counterpart ('HsLit') by
use of 'MatchLit.tidyNPat'. But since that is not the case, we have to mimic its
logic in 'translateNPat'.
But that only concerns patterns! We surely have to make sure to translate
expressions in a similar way in 'hsExprToPmExpr'. Thus, both 'translateNPat' and
'hsExprToPmExpr' call out to 'hsOverLitAsHsLit'.
Before #14546, the translations in 'hsExprToPmExpr' and 'translateNPat' were out
of sync, so the resulting comparisons between 'PmSLit' and 'PmOLit' could never
return True. But the fix in #14546 translated many occurrences where we could
have 'PmSLit's into 'PmOLit's, resulting in a loss of precision due to
Note [Undecidable Equality for PmAltCons].
Now, we translate the literal value to match and the literal patterns
consistently and try to turn them into plain literals as often as possible:
* For integral literals, we parse both the integral literal value and
the patterns as HsInt/HsWordPrim/HsInteger. For example:
case 0::Int of
0 -> putStrLn "A"
1 -> putStrLn "B"
_ -> putStrLn "C"
Note that we can decide now that the last two clauses are redundant.
* For string literals, we parse the string literals as HsString. When
OverloadedStrings is enabled and applicable for the data type, it will be
turned into a HsOverLit HsIsString. For example:
case "foo" of
"foo" -> putStrLn "A"
"bar" -> putStrLn "B"
"baz" -> putStrLn "C"
Even in the presence of -XOverloadedStrings, if @"foo" :: String@, the
overloaded string and its patterns will be turned into a list of character
literals, while for any other data type that satisfies 'IsString', this will
turn into the respective 'PmOLit'.
The desugaring of actual Strings to lists is so that we catch the redundant
pattern in following case:
case "foo" of
('f':_) -> putStrLn "A"
"bar" -> putStrLn "B"
For overloaded strings, we can still capture the exhaustiveness of pattern
"foo" and the redundancy of pattern "bar" and "baz" in the following code:
{-# LANGUAGE OverloadedStrings #-}
data D = ...
instance IsString D where ...
main = do
case "foo" :: D of
"foo" -> putStrLn "A"
"bar" -> putStrLn "B"
"baz" -> putStrLn "C"
-}
lhsExprToPmExpr :: LHsExpr GhcTc -> PmExpr
lhsExprToPmExpr (dL->L _ e) = hsExprToPmExpr e
......@@ -185,24 +320,22 @@ hsExprToPmExpr (HsVar _ x) = PmExprVar (idName (unLoc x))
-- `testsuite/tests/pmcheck/should_compile/PmExprVars.hs`.
-- hsExprToPmExpr (HsConLikeOut _ c) = PmExprVar (conLikeName 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].
-- See Note [Translate Overloaded Literals for Exhaustiveness Checking]
hsExprToPmExpr (HsOverLit _ olit)
| OverLit (OverLitTc False ty) (HsIsString src s) _ <- olit, isStringTy ty
= stringExprToList src s
| otherwise = PmExprLit (PmOLit False olit)
| Just lit <- hsOverLitAsHsLit olit False (overLitType olit)
= hsExprToPmExpr (HsLit noExtField lit)
| otherwise
= PmExprCon (PmAltLit (PmOLit False olit)) []
hsExprToPmExpr (HsLit _ lit)
| HsString src s <- lit
= stringExprToList src s
| otherwise = PmExprLit (PmSLit lit)
| otherwise = PmExprCon (PmAltLit (PmSLit lit)) []
hsExprToPmExpr e@(NegApp _ (dL->L _ neg_expr) _)
| PmExprLit (PmOLit False olit) <- hsExprToPmExpr neg_expr
| PmExprCon (PmAltLit (PmOLit False olit)) _ <- hsExprToPmExpr neg_expr
-- NB: DON'T simply @(NegApp (NegApp olit))@ as @x@. when extension
-- @RebindableSyntax@ enabled, (-(-x)) may not equals to x.
= PmExprLit (PmOLit True olit)
= PmExprCon (PmAltLit (PmOLit True olit)) []
| otherwise = PmExprOther e
hsExprToPmExpr (HsPar _ (dL->L _ e)) = hsExprToPmExpr e
......@@ -249,7 +382,40 @@ stringExprToList src s = foldr cons nil (map charToPmExpr (unpackFS s))
where
cons x xs = mkPmExprData consDataCon [x,xs]
nil = mkPmExprData nilDataCon []
charToPmExpr c = PmExprLit (PmSLit (HsChar src c))
charToPmExpr c = PmExprCon (PmAltLit (PmSLit (HsChar src c))) []
-- | Return @Just@ a 'DataCon' application or @Nothing@, otherwise.
pmExprToDataConApp :: PmExpr -> Maybe (DataCon, [PmExpr])
pmExprToDataConApp (PmExprCon (PmAltConLike (RealDataCon c)) es) = Just (c, es)
pmExprToDataConApp _ = Nothing
-- | The result of 'pmExprAsList'.
data PmExprList
= NilTerminated [PmExpr]
| WcVarTerminated (NonEmpty PmExpr) Name
-- | Extract a list of 'PmExpr's out of a sequence of cons cells, optionally
-- terminated by a wildcard variable instead of @[]@. Some examples:
--
-- * @pmExprAsList (1:2:[]) == Just ('NilTerminated' [1,2])@, a regular,
-- @[]@-terminated list. Should be pretty-printed as @[1,2]@.
-- * @pmExprAsList (1:2:x) == Just ('WcVarTerminated' [1,2] x)@, a list prefix
-- ending in a wildcard variable x (of list type). Should be pretty-printed as
-- (1:2:_).
-- * @pmExprAsList [] == Just ('NilTerminated' [])@
pmExprAsList :: PmExpr -> Maybe PmExprList
pmExprAsList = go []
where
go rev_pref (PmExprVar x)
| Just pref <- nonEmpty (reverse rev_pref)
= Just (WcVarTerminated pref x)
go rev_pref (pmExprToDataConApp -> Just (c, es))
| c == nilDataCon
= ASSERT( null es ) Just (NilTerminated (reverse rev_pref))
| c == consDataCon
= ASSERT( length es == 2 ) go (es !! 0 : rev_pref) (es !! 1)
go _ _
= Nothing
{-
%************************************************************************
......@@ -263,18 +429,32 @@ instance Outputable PmLit where
ppr (PmSLit l) = pmPprHsLit l
ppr (PmOLit neg l) = (if neg then char '-' else empty) <> ppr l
instance Outputable PmAltCon where
ppr (PmAltConLike cl) = ppr cl
ppr (PmAltLit l) = ppr l
instance Outputable PmExpr where
ppr = go (0 :: Int)
where
go _ (PmExprLit l) = ppr l
go _ (PmExprVar v) = ppr v
go _ (PmExprOther e) = angleBrackets (ppr e)
go _ (PmExprCon (RealDataCon dc) args)
| isTupleDataCon dc = parens $ comma_sep $ map ppr args
| dc == consDataCon = brackets $ comma_sep $ map ppr (list_cells args)
where
comma_sep = fsep . punctuate comma
list_cells (hd:tl) = hd : list_cells tl
list_cells _ = []
go _ (PmExprVar v) = ppr v
go _ (PmExprOther e) = angleBrackets (ppr e)
go _ (pmExprAsList -> Just pm_expr_list) = case pm_expr_list of
NilTerminated list
| Just lits <- as_string list
-> doubleQuotes $ hcat $ map ppr lits
| otherwise
-> brackets $ fsep $ punctuate comma $ map ppr list
WcVarTerminated pref x
| Just lits <- as_string (toList pref)
-> hcat [doubleQuotes $ hcat $ map ppr lits, text "++", ppr x]
| otherwise
-> parens $ fcat $ punctuate colon $ map ppr (toList pref) ++ [ppr x]
go _ (pmExprToDataConApp -> Just (dc, args))
| isTupleDataCon dc = parens $ fsep $ punctuate comma $ map ppr args
go prec (PmExprCon cl args)
= cparen (null args || prec > 0) (hcat (ppr cl:map (go 1) args))
= cparen (notNull args && prec > 0) (hsep (ppr cl:map (go 1) args))
as_string = traverse as_char_lit
as_char_lit (PmExprCon (PmAltLit lit) [])
| isStringTy (pmLitType lit) = Just lit
as_char_lit _ = Nothing
module PmExpr where
import GhcPrelude ()
data TmVarCt
......@@ -21,8 +21,9 @@ import TysWiredIn
import Outputable
import Control.Monad.Trans.State.Strict
import Maybes
import Util
import Data.List.NonEmpty (toList)
import PmExpr
import TmOracle
-- | Pretty-print the guts of an uncovered value vector abstraction, i.e., its
......@@ -35,6 +36,9 @@ import TmOracle
-- where p is not one of {3, 4}
-- q is not one of {0, 5}
-- @
--
-- When the set of refutable shapes contains more than 3 elements, the
-- additional elements are indicated by "...".
pprUncovered :: ([PmExpr], PmRefutEnv) -> SDoc
pprUncovered (expr_vec, refuts)
| null cs = fsep vec -- there are no literal constraints
......@@ -45,12 +49,17 @@ pprUncovered (expr_vec, refuts)
(vec,cs) = runPmPpr sdoc_vec (prettifyRefuts refuts)
-- | Output refutable shapes of a variable in the form of @var is not one of {2,
-- Nothing, 3}@.
-- Nothing, 3}@. Will never print more than 3 refutable shapes, the tail is
-- indicated by an ellipsis.
pprRefutableShapes :: (SDoc,[PmAltCon]) -> SDoc
pprRefutableShapes (var, alts)
= var <+> text "is not one of" <+> braces (pprWithCommas ppr_alt alts)
= var <+> text "is not one of" <+> format_alts alts
where
ppr_alt (PmAltLit lit) = ppr lit
format_alts = braces . fsep . punctuate comma . shorten . map ppr_alt
shorten (a:b:c:_:_) = a:b:c:[text "..."]
shorten xs = xs
ppr_alt (PmAltConLike cl) = ppr cl
ppr_alt (PmAltLit lit) = ppr lit
{- 1. Literals
~~~~~~~~~~~~~~
......@@ -86,7 +95,7 @@ type PrettyPmRefutEnv = DNameEnv (SDoc, [PmAltCon])
prettifyRefuts :: PmRefutEnv -> PrettyPmRefutEnv
prettifyRefuts = listToUDFM . zipWith rename nameList . udfmToList
where
rename new (old, lits) = (old, (new, lits))
rename new (old, ncons) = (old, (new, ncons))
-- Try nice names p,q,r,s,t before using the (ugly) t_i
nameList :: [SDoc]
nameList = map text ["p","q","r","s","t"] ++
......@@ -124,48 +133,37 @@ pprPmExpr (PmExprVar x) = do
Just name -> addUsed x >> return name
Nothing -> return underscore
pprPmExpr (PmExprCon con args) = pprPmExprCon con args
pprPmExpr (PmExprLit l) = return (ppr l)
pprPmExpr (PmExprOther _) = return underscore -- don't show
needsParens :: PmExpr -> Bool
needsParens (PmExprVar {}) = False
needsParens (PmExprLit l) = isNegatedPmLit l
needsParens (PmExprOther {}) = False -- will become a wildcard
needsParens (PmExprCon (RealDataCon c) es)
| isTupleDataCon c
|| isConsDataCon c || null es = False
| otherwise = True
needsParens (PmExprCon (PatSynCon _) es) = not (null es)
needsParens (PmExprVar {}) = False
needsParens (PmExprOther {}) = False -- will become a wildcard
needsParens (PmExprCon (PmAltLit l) _) = isNegatedPmLit l
needsParens (PmExprCon (PmAltConLike (RealDataCon c)) _)
| isTupleDataCon c || isConsDataCon c = False
needsParens (PmExprCon _ es) = not (null es)
pprPmExprWithParens :: PmExpr -> PmPprM SDoc
pprPmExprWithParens expr
| needsParens expr = parens <$> pprPmExpr expr
| otherwise = pprPmExpr expr
pprPmExprCon :: ConLike -> [PmExpr] -> PmPprM SDoc
pprPmExprCon (RealDataCon con) args
| isTupleDataCon con = mkTuple <$> mapM pprPmExpr args
| isConsDataCon con = pretty_list
where
mkTuple :: [SDoc] -> SDoc
mkTuple = parens . fsep . punctuate comma
-- lazily, to be used in the list case only
pretty_list :: PmPprM SDoc
pretty_list = case isNilPmExpr (last list) of
True -> brackets . fsep . punctuate comma <$> mapM pprPmExpr (init list)
False -> parens . hcat . punctuate colon <$> mapM pprPmExpr list
list = list_elements args
list_elements [x,y]
| PmExprCon c es <- y, RealDataCon nilDataCon == c
= ASSERT(null es) [x,y]
| PmExprCon c es <- y, RealDataCon consDataCon == c
= x : list_elements es
| otherwise = [x,y]
list_elements list = pprPanic "list_elements:" (ppr list)
pprPmExprCon cl args
pprPmExprCon :: PmAltCon -> [PmExpr] -> PmPprM SDoc
pprPmExprCon (PmAltConLike cl) args = pprConLike cl args
pprPmExprCon (PmAltLit l) _ = pure (ppr l)
pprConLike :: ConLike -> [PmExpr] -> PmPprM SDoc
pprConLike cl args
| Just pm_expr_list <- pmExprAsList (PmExprCon (PmAltConLike cl) args)
= case pm_expr_list of
NilTerminated list ->
brackets . fsep . punctuate comma <$> mapM pprPmExpr list
WcVarTerminated pref x ->
parens . fcat . punctuate colon <$> mapM pprPmExpr (toList pref ++ [PmExprVar x])
pprConLike (RealDataCon con) args
| isTupleDataCon con
= parens . fsep . punctuate comma <$> mapM pprPmExpr args
pprConLike cl args
| conLikeIsInfix cl = case args of
[x, y] -> do x' <- pprPmExprWithParens x
y' <- pprPmExprWithParens y
......@@ -181,11 +179,6 @@ isNegatedPmLit :: PmLit -> Bool
isNegatedPmLit (PmOLit b _) = b
isNegatedPmLit _other_lit = False
-- | Check whether a PmExpr is syntactically e
isNilPmExpr :: PmExpr -> Bool
isNilPmExpr (PmExprCon c _) = c == RealDataCon nilDataCon
isNilPmExpr _other_expr = False
-- | Check if a DataCon is (:).
isConsDataCon :: DataCon -> Bool
isConsDataCon con = consDataCon == con
......@@ -5,23 +5,19 @@ Author: George Karachalias <george.karachalias@cs.kuleuven.be>
{-# LANGUAGE CPP, MultiWayIf #-}
-- | The term equality oracle. The main export of the module are the functions
-- 'tmOracle', 'solveOneEq' and 'addSolveRefutableAltCon'.
-- 'tmOracle', 'solveOneEq' and 'tryAddRefutableAltCon'.
--
-- If you are looking for an oracle that can solve type-level constraints, look
-- at 'TcSimplify.tcCheckSatisfiability'.
module TmOracle (
-- re-exported from PmExpr
PmExpr(..), PmLit(..), PmAltCon(..), TmVarCt(..), TmVarCtEnv,
PmRefutEnv, eqPmLit, isNotPmExprOther, lhsExprToPmExpr, hsExprToPmExpr,
-- the term oracle
tmOracle, TmState, initialTmState, wrapUpTmState, solveOneEq,
extendSubst, canDiverge, isRigid,