diff options
Diffstat (limited to 'compiler/deSugar/PmExpr.hs')
| -rw-r--r-- | compiler/deSugar/PmExpr.hs | 450 |
1 files changed, 267 insertions, 183 deletions
diff --git a/compiler/deSugar/PmExpr.hs b/compiler/deSugar/PmExpr.hs index 3697dd8cc1..f83c63e4fd 100644 --- a/compiler/deSugar/PmExpr.hs +++ b/compiler/deSugar/PmExpr.hs @@ -6,29 +6,38 @@ Haskell expressions (as used by the pattern matching checker) and utilities. {-# LANGUAGE CPP #-} {-# LANGUAGE ViewPatterns #-} -{-# LANGUAGE GeneralizedNewtypeDeriving #-} module PmExpr ( - PmExpr(..), PmLit(..), PmAltCon(..), TmVarCt(..), - eqPmLit, isNotPmExprOther, lhsExprToPmExpr, hsExprToPmExpr + PmLit(..), PmLitValue(..), PmAltCon(..), + pmAltConType, PmEquality(..), eqPmAltCon, + pmLitType, literalToPmLit, negatePmLit, overloadPmLit, + pmLitAsStringLit, coreExprAsPmLit ) where #include "HsVersions.h" import GhcPrelude -import BasicTypes (SourceText) -import FastString (FastString, unpackFS) -import HsSyn +import Util +import FastString import Id import Name import DataCon import ConLike -import TcEvidence (isErasableHsWrapper) -import TcType (isStringTy) -import TysWiredIn import Outputable -import SrcLoc +import Maybes +import Type +import TyCon +import Literal +import CoreSyn +import CoreUtils (exprType) +import PrelNames +import TysWiredIn +import TysPrim + +import Numeric (fromRat) +import Data.Foldable (find) +import Data.Ratio {- %************************************************************************ @@ -38,52 +47,135 @@ import SrcLoc %************************************************************************ -} -{- 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 - | 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. -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. -- --- See Note [Refutable shapes] in TmOracle. Really similar to 'CoreSyn.AltCon'. -newtype PmAltCon = PmAltLit PmLit - deriving Outputable - +-- See Note [Undecidable Equality for PmAltCons] +data PmLit = PmLit + { pm_lit_ty :: Type + , pm_lit_val :: PmLitValue } + +data PmLitValue + = PmLitInt Integer + | PmLitRat Rational + | PmLitChar Char + -- We won't actually see PmLitString in the oracle since we desugar strings to + -- lists + | PmLitString FastString + | PmLitOverInt Int {- How often Negated? -} Integer + | PmLitOverRat Int {- How often Negated? -} Rational + | PmLitOverString FastString + +-- | Undecidable semantic equality result. +-- See Note [Undecidable Equality for PmAltCons] +data PmEquality + = Equal + | Disjoint + | PossiblyOverlap + deriving (Eq, Show) + +-- | When 'PmEquality' can be decided. @True <=> Equal@, @False <=> Disjoint@. +decEquality :: Bool -> PmEquality +decEquality True = Equal +decEquality False = Disjoint + +-- | 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 +eqPmLit :: PmLit -> PmLit -> PmEquality +eqPmLit (PmLit t1 v1) (PmLit t2 v2) + -- no haddock | pprTrace "eqPmLit" (ppr t1 <+> ppr v1 $$ ppr t2 <+> ppr v2) False = undefined + | not (t1 `eqType` t2) = Disjoint + | otherwise = go v1 v2 + where + go (PmLitInt i1) (PmLitInt i2) = decEquality (i1 == i2) + go (PmLitRat r1) (PmLitRat r2) = decEquality (r1 == r2) + go (PmLitChar c1) (PmLitChar c2) = decEquality (c1 == c2) + go (PmLitString s1) (PmLitString s2) = decEquality (s1 == s2) + go (PmLitOverInt n1 i1) (PmLitOverInt n2 i2) + | n1 == n2 && i1 == i2 = Equal + go (PmLitOverRat n1 r1) (PmLitOverRat n2 r2) + | n1 == n2 && r1 == r2 = Equal + go (PmLitOverString s1) (PmLitOverString s2) + | s1 == s2 = Equal + go _ _ = PossiblyOverlap + +-- | Syntactic equality. +instance Eq PmLit where + a == b = eqPmLit a b == Equal + +-- | Type of a 'PmLit' +pmLitType :: PmLit -> Type +pmLitType (PmLit ty _) = ty + +-- | Type of a 'PmAltCon' +pmAltConType :: PmAltCon -> [Type] -> Type +pmAltConType (PmAltLit lit) _arg_tys = ASSERT( null _arg_tys ) pmLitType lit +pmAltConType (PmAltConLike con) arg_tys = conLikeResTy con arg_tys + +-- | 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 +eqConLike :: ConLike -> ConLike -> PmEquality +eqConLike (RealDataCon dc1) (RealDataCon dc2) = decEquality (dc1 == dc2) +eqConLike (PatSynCon psc1) (PatSynCon psc2) + | psc1 == psc2 + = Equal +eqConLike _ _ = PossiblyOverlap + +-- | Represents the head of a match against a 'ConLike' or literal. +-- Really similar to 'CoreSyn.AltCon'. +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 'eqPmLit' and 'eqConLike', 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 +-- +-- Examples (omitting some constructor wrapping): +-- +-- * @eqPmAltCon (LitInt 42) (LitInt 1) == Just False@: Lit equality is +-- decidable +-- * @eqPmAltCon (DataCon A) (DataCon B) == Just False@: DataCon equality is +-- decidable +-- * @eqPmAltCon (LitOverInt 42) (LitOverInt 1) == Nothing@: OverLit equality +-- is undecidable +-- * @eqPmAltCon (PatSyn PA) (PatSyn PB) == Nothing@: PatSyn equality is +-- undecidable +-- * @eqPmAltCon (DataCon I#) (LitInt 1) == Nothing@: DataCon to Lit +-- comparisons are undecidable without reasoning about the wrapped @Int#@ +-- * @eqPmAltCon (LitOverInt 1) (LitOverInt 1) == Just True@: We assume +-- reflexivity for overloaded literals +-- * @eqPmAltCon (PatSyn PA) (PatSyn PA) == Just True@: We assume reflexivity +-- for Pattern Synonyms +eqPmAltCon :: PmAltCon -> PmAltCon -> PmEquality +eqPmAltCon (PmAltConLike cl1) (PmAltConLike cl2) = eqConLike cl1 cl2 +eqPmAltCon (PmAltLit l1) (PmAltLit l2) = eqPmLit l1 l2 +eqPmAltCon _ _ = PossiblyOverlap + +-- | Syntactic equality. instance Eq PmAltCon where - PmAltLit l1 == PmAltLit l2 = eqPmLit l1 l2 + a == b = eqPmAltCon a b == Equal -{- 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 +188,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 +208,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 'eqPmAltCons'. 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,120 +227,100 @@ 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 assume F a ~ F a, though. -} --- | A term constraint. @TVC x e@ encodes that @x@ is equal to @e@. -data TmVarCt = TVC !Id !PmExpr +literalToPmLit :: Type -> Literal -> Maybe PmLit +literalToPmLit ty l = PmLit ty <$> go l + where + go (LitChar c) = Just (PmLitChar c) + go (LitFloat r) = Just (PmLitRat r) + go (LitDouble r) = Just (PmLitRat r) + go (LitString s) = Just (PmLitString (mkFastStringByteString s)) + go (LitNumber _ i _) = Just (PmLitInt i) + go _ = Nothing + +negatePmLit :: PmLit -> Maybe PmLit +negatePmLit (PmLit ty v) = PmLit ty <$> go v + where + go (PmLitInt i) = Just (PmLitInt (-i)) + go (PmLitRat r) = Just (PmLitRat (-r)) + go (PmLitOverInt n i) = Just (PmLitOverInt (n+1) i) + go (PmLitOverRat n r) = Just (PmLitOverRat (n+1) r) + go _ = Nothing + +overloadPmLit :: Type -> PmLit -> Maybe PmLit +overloadPmLit ty (PmLit _ v) = PmLit ty <$> go v + where + go (PmLitInt i) = Just (PmLitOverInt 0 i) + go (PmLitRat r) = Just (PmLitOverRat 0 r) + go (PmLitString s) + | ty `eqType` stringTy = Just v + | otherwise = Just (PmLitOverString s) + go _ = Nothing -instance Outputable TmVarCt where - ppr (TVC x e) = ppr x <+> char '~' <+> ppr e +pmLitAsStringLit :: PmLit -> Maybe FastString +pmLitAsStringLit (PmLit _ (PmLitString s)) = Just s +pmLitAsStringLit _ = Nothing -- ---------------------------------------------------------------------------- -- ** Predicates on PmExpr --- | Check if an expression is lifted or not -isNotPmExprOther :: PmExpr -> Bool -isNotPmExprOther (PmExprOther _) = False -isNotPmExprOther _expr = True - -- ----------------------------------------------------------------------- -- ** Lift source expressions (HsExpr Id) to PmExpr -lhsExprToPmExpr :: LHsExpr GhcTc -> PmExpr -lhsExprToPmExpr (dL->L _ e) = hsExprToPmExpr e - -hsExprToPmExpr :: HsExpr GhcTc -> PmExpr - --- Translating HsVar to flexible meta variables in the unification problem is --- morally wrong, but it does the right thing for now. --- In contrast to the situation in pattern matches, HsVars in expression syntax --- are object language variables, most similar to rigid variables with an --- unknown solution. The correct way would be to handle them through PmExprOther --- and identify syntactically equal occurrences by the same rigid meta variable, --- but we can't compare the wrapped HsExpr for equality. Hence we are stuck with --- this hack. -hsExprToPmExpr (HsVar _ x) = PmExprVar (idName (unLoc x)) - --- Translating HsConLikeOut to a flexible meta variable is misleading. --- For an example why, consider `consAreRigid` in --- `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]. -hsExprToPmExpr (HsOverLit _ olit) - | OverLit (OverLitTc False ty) (HsIsString src s) _ <- olit, isStringTy ty - = stringExprToList src s - | otherwise = PmExprLit (PmOLit False olit) -hsExprToPmExpr (HsLit _ lit) - | HsString src s <- lit - = stringExprToList src s - | otherwise = PmExprLit (PmSLit lit) - -hsExprToPmExpr e@(NegApp _ (dL->L _ neg_expr) _) - | PmExprLit (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) - | otherwise = PmExprOther e - -hsExprToPmExpr (HsPar _ (dL->L _ e)) = hsExprToPmExpr e - -hsExprToPmExpr e@(ExplicitTuple _ ps boxity) - | all tupArgPresent ps = mkPmExprData tuple_con tuple_args - | otherwise = PmExprOther e - where - tuple_con = tupleDataCon boxity (length ps) - tuple_args = [ lhsExprToPmExpr e | (dL->L _ (Present _ e)) <- ps ] - -hsExprToPmExpr e@(ExplicitList _ mb_ol elems) - | Nothing <- mb_ol = foldr cons nil (map lhsExprToPmExpr elems) - | otherwise = PmExprOther e {- overloaded list: No PmExprApp -} - where - cons x xs = mkPmExprData consDataCon [x,xs] - nil = mkPmExprData 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@(RecordCon {}) = PmExprOther e - -hsExprToPmExpr (HsTick _ _ e) = lhsExprToPmExpr e -hsExprToPmExpr (HsBinTick _ _ _ e) = lhsExprToPmExpr e -hsExprToPmExpr (HsTickPragma _ _ _ _ e) = lhsExprToPmExpr e -hsExprToPmExpr (HsSCC _ _ _ e) = lhsExprToPmExpr e -hsExprToPmExpr (HsCoreAnn _ _ _ e) = lhsExprToPmExpr e -hsExprToPmExpr (ExprWithTySig _ e _) = lhsExprToPmExpr e -hsExprToPmExpr (HsWrap _ w e) - -- A dictionary application spoils e and we have no choice but to return an - -- PmExprOther. Same thing for other stuff that can't erased in the - -- compilation process. Otherwise this bites in - -- teststuite/tests/pmcheck/should_compile/PmExprVars.hs. - | isErasableHsWrapper w = hsExprToPmExpr e -hsExprToPmExpr e = PmExprOther e -- the rest are not handled by the oracle - -stringExprToList :: SourceText -> FastString -> PmExpr -stringExprToList src s = foldr cons nil (map charToPmExpr (unpackFS s)) +coreExprAsPmLit :: CoreExpr -> Maybe PmLit +-- coreExprAsPmLit e | pprTrace "coreExprAsPmLit" (ppr e) False = undefined +coreExprAsPmLit (Tick _t e) = coreExprAsPmLit e +coreExprAsPmLit (Lit l) = literalToPmLit (literalType l) l +coreExprAsPmLit e = case collectArgs e of + (Var x, [Lit l]) + | Just dc <- isDataConWorkId_maybe x + , dc `elem` [intDataCon, wordDataCon, charDataCon, floatDataCon, doubleDataCon] + -> literalToPmLit (exprType e) l + (Var x, [_ty, Lit n, Lit d]) + | Just dc <- isDataConWorkId_maybe x + , dataConName dc == ratioDataConName + -- HACK: just assume we have a literal double. This case only occurs for + -- overloaded lits anyway, so we immediately override type information + -> literalToPmLit (exprType e) (mkLitDouble (litValue n % litValue d)) + (Var x, args) + -- Take care of -XRebindableSyntax. The last argument should be the (only) + -- integer literal, otherwise we can't really do much about it. + | [Lit l] <- dropWhile (not . is_lit) args + -- getOccFS because of -XRebindableSyntax + , getOccFS (idName x) == getOccFS fromIntegerName + -> literalToPmLit (literalType l) l >>= overloadPmLit (exprType e) + (Var x, args) + -- Similar to fromInteger case + | [r] <- dropWhile (not . is_ratio) args + , getOccFS (idName x) == getOccFS fromRationalName + -> coreExprAsPmLit r >>= overloadPmLit (exprType e) + (Var x, [Type _ty, _dict, s]) + | idName x == fromStringName + -- NB: Calls coreExprAsPmLit and then overloadPmLit, so that we return PmLitOverStrings + -> coreExprAsPmLit s >>= overloadPmLit (exprType e) + -- These last two cases handle String literals + (Var x, [Type ty]) + | Just dc <- isDataConWorkId_maybe x + , dc == nilDataCon + , ty `eqType` charTy + -> literalToPmLit stringTy (mkLitString "") + (Var x, [Lit l]) + | idName x `elem` [unpackCStringName, unpackCStringUtf8Name] + -> literalToPmLit stringTy l + _ -> Nothing where - cons x xs = mkPmExprData consDataCon [x,xs] - nil = mkPmExprData nilDataCon [] - charToPmExpr c = PmExprLit (PmSLit (HsChar src c)) + is_lit Lit{} = True + is_lit _ = False + is_ratio (Type _) = False + is_ratio r + | Just (tc, _) <- splitTyConApp_maybe (exprType r) + = tyConName tc == ratioTyConName + | otherwise + = False {- %************************************************************************ @@ -259,22 +330,35 @@ stringExprToList src s = foldr cons nil (map charToPmExpr (unpackFS s)) %************************************************************************ -} -instance Outputable PmLit where - ppr (PmSLit l) = pmPprHsLit l - ppr (PmOLit neg l) = (if neg then char '-' else empty) <> ppr l +instance Outputable PmLitValue where + ppr (PmLitInt i) = ppr i + ppr (PmLitRat r) = ppr (double (fromRat r)) -- good enough + ppr (PmLitChar c) = pprHsChar c + ppr (PmLitString s) = pprHsString s + ppr (PmLitOverInt n i) = minuses n (ppr i) + ppr (PmLitOverRat n r) = minuses n (ppr (double (fromRat r))) + ppr (PmLitOverString s) = pprHsString s + +-- Take care of negated literals +minuses :: Int -> SDoc -> SDoc +minuses n sdoc = iterate (\sdoc -> parens (char '-' <> sdoc)) sdoc !! n -instance Outputable PmExpr where - ppr = go (0 :: Int) +instance Outputable PmLit where + ppr (PmLit ty v) = ppr v <> suffix 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 prec (PmExprCon cl args) - = cparen (null args || prec > 0) (hcat (ppr cl:map (go 1) args)) + -- Some ad-hoc hackery for displaying proper lit suffixes based on type + tbl = [ (intPrimTy, primIntSuffix) + , (int64PrimTy, primInt64Suffix) + , (wordPrimTy, primWordSuffix) + , (word64PrimTy, primWord64Suffix) + , (charPrimTy, primCharSuffix) + , (floatPrimTy, primFloatSuffix) + , (doublePrimTy, primDoubleSuffix) ] + suffix = fromMaybe empty (snd <$> find (eqType ty . fst) tbl) + +instance Outputable PmAltCon where + ppr (PmAltConLike cl) = ppr cl + ppr (PmAltLit l) = ppr l + +instance Outputable PmEquality where + ppr = text . show |