[Git][ghc/ghc][wip/pmcheck-ncon] Add `PmNCons` to `Check` for correct warnings in the presence of `COMPLETE` groups
Sebastian Graf
gitlab at gitlab.haskell.org
Thu Jun 6 13:03:34 UTC 2019
Sebastian Graf pushed to branch wip/pmcheck-ncon at Glasgow Haskell Compiler / GHC
Commits:
236c0cfb by Sebastian Graf at 2019-06-06T13:03:03Z
Add `PmNCons` to `Check` 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.
The introduction of an `PmNCons` variant in `PmPat` fixes this: 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 in `PmNCons`.
After all clauses have been processed this way, we filter out any value
vector abstractions from the uncovered set involving `PmNCons` whose set
of covered constructors completely overlap a `COMPLETE` set.
- - - - -
20 changed files:
- compiler/basicTypes/NameEnv.hs
- compiler/deSugar/Check.hs
- compiler/deSugar/DsMonad.hs
- compiler/deSugar/PmExpr.hs
- compiler/deSugar/PmPpr.hs
- compiler/deSugar/TmOracle.hs
- compiler/typecheck/TcRnTypes.hs
- compiler/utils/Binary.hs
- compiler/utils/ListSetOps.hs
- docs/users_guide/glasgow_exts.rst
- + testsuite/tests/perf/compiler/ManyAlternatives.hs
- + testsuite/tests/pmcheck/complete_sigs/T13363a.hs
- + testsuite/tests/pmcheck/complete_sigs/T13363a.stderr
- + testsuite/tests/pmcheck/complete_sigs/T13363b.hs
- + testsuite/tests/pmcheck/complete_sigs/T13363b.stderr
- testsuite/tests/pmcheck/complete_sigs/all.T
- testsuite/tests/pmcheck/should_compile/all.T
- + testsuite/tests/pmcheck/should_compile/pmc008.hs
- + testsuite/tests/pmcheck/should_compile/pmc009.hs
- + testsuite/tests/pmcheck/should_compile/pmc010.hs
Changes:
=====================================
compiler/basicTypes/NameEnv.hs
=====================================
@@ -27,7 +27,7 @@ module NameEnv (
lookupDNameEnv,
delFromDNameEnv,
mapDNameEnv,
- alterDNameEnv,
+ alterDNameEnv, extendDNameEnv_C,
-- ** Dependency analysis
depAnal
) where
@@ -156,3 +156,6 @@ mapDNameEnv = mapUDFM
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
=====================================
compiler/deSugar/Check.hs
=====================================
@@ -24,6 +24,7 @@ module Check (
import GhcPrelude
+import PmExpr
import TmOracle
import PmPpr
import Unify( tcMatchTy )
@@ -56,20 +57,19 @@ import TyCoRep
import Type
import UniqSupply
import DsUtils (isTrueLHsExpr)
-import Maybes (expectJust)
+import Maybes (MaybeT (..), expectJust)
import qualified GHC.LanguageExtensions as LangExt
-import Data.List (find)
+import Data.List (find, (\\))
import Data.Maybe (catMaybes, isJust, fromMaybe)
-import Control.Monad (forM, when, forM_, zipWithM, filterM)
+import Control.Monad (forM, when, guard, forM_, zipWithM, filterM)
+import Control.Monad.Trans.Class (lift)
import Coercion
import TcEvidence
import TcSimplify (tcNormalise)
import IOEnv
import qualified Data.Semigroup as Semi
-import ListT (ListT(..), fold, select)
-
{-
This module checks pattern matches for:
\begin{enumerate}
@@ -92,72 +92,23 @@ The algorithm is based on the paper:
%************************************************************************
-}
--- We use the non-determinism monad to apply the algorithm to several
--- possible sets of constructors. Users can specify complete sets of
--- constructors by using COMPLETE pragmas.
--- The algorithm only picks out constructor
--- sets deep in the bowels which makes a simpler `mapM` more difficult to
--- implement. The non-determinism is only used in one place, see the ConVar
--- case in `pmCheckHd`.
-
-type PmM a = ListT DsM a
-
-liftD :: DsM a -> PmM a
-liftD m = ListT $ \sk fk -> m >>= \a -> sk a fk
+type PmM = DsM
--- Pick the first match complete covered match or otherwise the "best" match.
--- The best match is the one with the least uncovered clauses, ties broken
--- by the number of inaccessible clauses followed by number of redundant
--- clauses.
---
--- This is specified in the
--- "Disambiguating between multiple ``COMPLETE`` pragmas" section of the
--- users' guide. If you update the implementation of this function, make sure
--- to update that section of the users' guide as well.
-getResult :: PmM PmResult -> DsM PmResult
-getResult ls
- = do { res <- fold ls goM (pure Nothing)
- ; case res of
- Nothing -> panic "getResult is empty"
- Just a -> return a }
- where
- goM :: PmResult -> DsM (Maybe PmResult) -> DsM (Maybe PmResult)
- goM mpm dpm = do { pmr <- dpm
- ; return $ Just $ go pmr mpm }
-
- -- Careful not to force unecessary results
- go :: Maybe PmResult -> PmResult -> PmResult
- go Nothing rs = rs
- go (Just old@(PmResult prov rs (UncoveredPatterns us) is)) new
- | null us && null rs && null is = old
- | otherwise =
- let PmResult prov' rs' (UncoveredPatterns us') is' = new
- in case compareLength us us'
- `mappend` (compareLength is is')
- `mappend` (compareLength rs rs')
- `mappend` (compare prov prov') of
- GT -> new
- EQ -> new
- LT -> old
- go (Just (PmResult _ _ (TypeOfUncovered _) _)) _new
- = panic "getResult: No inhabitation candidates"
-
-data PatTy = PAT | VA -- Used only as a kind, to index PmPat
+-- | Used only as a kind, to index PmPat
+data PatTy = PAT | VA
-- The *arity* of a PatVec [p1,..,pn] is
-- the number of p1..pn that are not Guards
data PmPat :: PatTy -> * where
+ -- | For the arguments' meaning see 'HsPat.ConPatOut'.
PmCon :: { pm_con_con :: ConLike
, pm_con_arg_tys :: [Type]
, pm_con_tvs :: [TyVar]
- , pm_con_dicts :: [EvVar]
, pm_con_args :: [PmPat t] } -> PmPat t
- -- For PmCon arguments' meaning see @ConPatOut@ in hsSyn/HsPat.hs
PmVar :: { pm_var_id :: Id } -> PmPat t
- PmLit :: { pm_lit_lit :: PmLit } -> PmPat t -- See Note [Literals in PmPat]
- PmNLit :: { pm_lit_id :: Id
- , pm_lit_not :: [PmLit] } -> PmPat 'VA
+ -- | See Note [Literals in PmPat]
+ PmLit :: { pm_lit_lit :: PmLit } -> PmPat t
PmGrd :: { pm_grd_pv :: PatVec
, pm_grd_expr :: PmExpr } -> PmPat 'PAT
-- | A fake guard pattern (True <- _) used to represent cases we cannot handle.
@@ -200,8 +151,7 @@ data Covered = Covered | NotCovered
deriving Show
instance Outputable Covered where
- ppr (Covered) = text "Covered"
- ppr (NotCovered) = text "NotCovered"
+ ppr = text . show
-- Like the or monoid for booleans
-- Covered = True, Uncovered = False
@@ -218,8 +168,7 @@ data Diverged = Diverged | NotDiverged
deriving Show
instance Outputable Diverged where
- ppr Diverged = text "Diverged"
- ppr NotDiverged = text "NotDiverged"
+ ppr = text . show
instance Semi.Semigroup Diverged where
Diverged <> _ = Diverged
@@ -230,51 +179,26 @@ instance Monoid Diverged where
mempty = NotDiverged
mappend = (Semi.<>)
--- | When we learned that a given match group is complete
-data Provenance =
- FromBuiltin -- ^ From the original definition of the type
- -- constructor.
- | FromComplete -- ^ From a user-provided @COMPLETE@ pragma
- deriving (Show, Eq, Ord)
-
-instance Outputable Provenance where
- ppr = text . show
-
-instance Semi.Semigroup Provenance where
- FromComplete <> _ = FromComplete
- _ <> FromComplete = FromComplete
- _ <> _ = FromBuiltin
-
-instance Monoid Provenance where
- mempty = FromBuiltin
- mappend = (Semi.<>)
-
data PartialResult = PartialResult {
- presultProvenance :: Provenance
- -- keep track of provenance because we don't want
- -- to warn about redundant matches if the result
- -- is contaminated with a COMPLETE pragma
- , presultCovered :: Covered
+ presultCovered :: Covered
, presultUncovered :: Uncovered
, presultDivergent :: Diverged }
instance Outputable PartialResult where
- ppr (PartialResult prov c vsa d)
- = text "PartialResult" <+> ppr prov <+> ppr c
- <+> ppr d <+> ppr vsa
+ ppr (PartialResult c vsa d)
+ = text "PartialResult" <+> ppr c <+> ppr d <+> ppr vsa
instance Semi.Semigroup PartialResult where
- (PartialResult prov1 cs1 vsa1 ds1)
- <> (PartialResult prov2 cs2 vsa2 ds2)
- = PartialResult (prov1 Semi.<> prov2)
- (cs1 Semi.<> cs2)
+ (PartialResult cs1 vsa1 ds1)
+ <> (PartialResult cs2 vsa2 ds2)
+ = PartialResult (cs1 Semi.<> cs2)
(vsa1 Semi.<> vsa2)
(ds1 Semi.<> ds2)
instance Monoid PartialResult where
- mempty = PartialResult mempty mempty [] mempty
+ mempty = PartialResult mempty [] mempty
mappend = (Semi.<>)
-- newtype ChoiceOf a = ChoiceOf [a]
@@ -292,15 +216,13 @@ instance Monoid PartialResult where
--
data PmResult =
PmResult {
- pmresultProvenance :: Provenance
- , pmresultRedundant :: [Located [LPat GhcTc]]
+ pmresultRedundant :: [Located [LPat GhcTc]]
, pmresultUncovered :: UncoveredCandidates
, pmresultInaccessible :: [Located [LPat GhcTc]] }
instance Outputable PmResult where
ppr pmr = hang (text "PmResult") 2 $ vcat
- [ text "pmresultProvenance" <+> ppr (pmresultProvenance pmr)
- , text "pmresultRedundant" <+> ppr (pmresultRedundant pmr)
+ [ text "pmresultRedundant" <+> ppr (pmresultRedundant pmr)
, text "pmresultUncovered" <+> ppr (pmresultUncovered pmr)
, text "pmresultInaccessible" <+> ppr (pmresultInaccessible pmr)
]
@@ -325,11 +247,11 @@ instance Outputable UncoveredCandidates where
-- | The empty pattern check result
emptyPmResult :: PmResult
-emptyPmResult = PmResult FromBuiltin [] (UncoveredPatterns []) []
+emptyPmResult = PmResult [] (UncoveredPatterns []) []
-- | Non-exhaustive empty case with unknown/trivial inhabitants
uncoveredWithTy :: Type -> PmResult
-uncoveredWithTy ty = PmResult FromBuiltin [] (TypeOfUncovered ty) []
+uncoveredWithTy ty = PmResult [] (TypeOfUncovered ty) []
{-
%************************************************************************
@@ -342,8 +264,8 @@ uncoveredWithTy ty = PmResult FromBuiltin [] (TypeOfUncovered ty) []
-- | Check a single pattern binding (let)
checkSingle :: DynFlags -> DsMatchContext -> Id -> Pat GhcTc -> DsM ()
checkSingle dflags ctxt@(DsMatchContext _ locn) var p = do
- tracePmD "checkSingle" (vcat [ppr ctxt, ppr var, ppr p])
- mb_pm_res <- tryM (getResult (checkSingle' locn var p))
+ tracePm "checkSingle" (vcat [ppr ctxt, ppr var, ppr p])
+ mb_pm_res <- tryM (checkSingle' locn var p)
case mb_pm_res of
Left _ -> warnPmIters dflags ctxt
Right res -> dsPmWarn dflags ctxt res
@@ -351,25 +273,25 @@ checkSingle dflags ctxt@(DsMatchContext _ locn) var p = do
-- | Check a single pattern binding (let)
checkSingle' :: SrcSpan -> Id -> Pat GhcTc -> PmM PmResult
checkSingle' locn var p = do
- liftD resetPmIterDs -- set the iter-no to zero
- fam_insts <- liftD dsGetFamInstEnvs
- clause <- liftD $ translatePat fam_insts p
+ resetPmIterDs -- set the iter-no to zero
+ fam_insts <- dsGetFamInstEnvs
+ clause <- translatePat fam_insts p
missing <- mkInitialUncovered [var]
tracePm "checkSingle': missing" (vcat (map pprValVecDebug missing))
-- no guards
- PartialResult prov cs us ds <- runMany (pmcheckI clause []) missing
- let us' = UncoveredPatterns us
+ PartialResult cs us ds <- runMany (pmcheckI clause []) missing
+ us' <- UncoveredPatterns <$> normaliseUncovered us
return $ case (cs,ds) of
- (Covered, _ ) -> PmResult prov [] us' [] -- useful
- (NotCovered, NotDiverged) -> PmResult prov m us' [] -- redundant
- (NotCovered, Diverged ) -> PmResult prov [] us' m -- inaccessible rhs
+ (Covered, _ ) -> PmResult [] us' [] -- useful
+ (NotCovered, NotDiverged) -> PmResult m us' [] -- redundant
+ (NotCovered, Diverged ) -> PmResult [] us' m -- inaccessible rhs
where m = [cL locn [cL locn p]]
-- | Exhaustive for guard matches, is used for guards in pattern bindings and
-- in @MultiIf@ expressions.
checkGuardMatches :: HsMatchContext Name -- Match context
-> GRHSs GhcTc (LHsExpr GhcTc) -- Guarded RHSs
- -> DsM ()
+ -> PmM ()
checkGuardMatches hs_ctx guards@(GRHSs _ grhss _) = do
dflags <- getDynFlags
let combinedLoc = foldl1 combineSrcSpans (map getLoc grhss)
@@ -384,14 +306,14 @@ checkGuardMatches _ (XGRHSs _) = panic "checkGuardMatches"
-- | Check a matchgroup (case, functions, etc.)
checkMatches :: DynFlags -> DsMatchContext
- -> [Id] -> [LMatch GhcTc (LHsExpr GhcTc)] -> DsM ()
+ -> [Id] -> [LMatch GhcTc (LHsExpr GhcTc)] -> PmM ()
checkMatches dflags ctxt vars matches = do
- tracePmD "checkMatches" (hang (vcat [ppr ctxt
+ tracePm "checkMatches" (hang (vcat [ppr ctxt
, ppr vars
, text "Matches:"])
2
(vcat (map ppr matches)))
- mb_pm_res <- tryM $ getResult $ case matches of
+ mb_pm_res <- tryM $ case matches of
-- Check EmptyCase separately
-- See Note [Checking EmptyCase Expressions]
[] | [var] <- vars -> checkEmptyCase' var
@@ -406,38 +328,36 @@ checkMatches' :: [Id] -> [LMatch GhcTc (LHsExpr GhcTc)] -> PmM PmResult
checkMatches' vars matches
| null matches = panic "checkMatches': EmptyCase"
| otherwise = do
- liftD resetPmIterDs -- set the iter-no to zero
+ resetPmIterDs -- set the iter-no to zero
missing <- mkInitialUncovered vars
tracePm "checkMatches': missing" (vcat (map pprValVecDebug missing))
- (prov, rs,us,ds) <- go matches missing
+ (rs,us,ds) <- go matches missing
+ us' <- normaliseUncovered us
return $ PmResult {
- pmresultProvenance = prov
- , pmresultRedundant = map hsLMatchToLPats rs
- , pmresultUncovered = UncoveredPatterns us
+ pmresultRedundant = map hsLMatchToLPats rs
+ , pmresultUncovered = UncoveredPatterns us'
, pmresultInaccessible = map hsLMatchToLPats ds }
where
go :: [LMatch GhcTc (LHsExpr GhcTc)] -> Uncovered
- -> PmM (Provenance
- , [LMatch GhcTc (LHsExpr GhcTc)]
+ -> PmM ( [LMatch GhcTc (LHsExpr GhcTc)]
, Uncovered
, [LMatch GhcTc (LHsExpr GhcTc)])
- go [] missing = return (mempty, [], missing, [])
+ go [] missing = return ([], missing, [])
go (m:ms) missing = do
tracePm "checkMatches': go" (ppr m $$ ppr missing)
- fam_insts <- liftD dsGetFamInstEnvs
- (clause, guards) <- liftD $ translateMatch fam_insts m
- r@(PartialResult prov cs missing' ds)
+ fam_insts <- dsGetFamInstEnvs
+ (clause, guards) <- translateMatch fam_insts m
+ r@(PartialResult cs missing' ds)
<- runMany (pmcheckI clause guards) missing
tracePm "checkMatches': go: res" (ppr r)
- (ms_prov, rs, final_u, is) <- go ms missing'
- let final_prov = prov `mappend` ms_prov
+ (rs, final_u, is) <- go ms missing'
return $ case (cs, ds) of
-- useful
- (Covered, _ ) -> (final_prov, rs, final_u, is)
+ (Covered, _ ) -> (rs, final_u, is)
-- redundant
- (NotCovered, NotDiverged) -> (final_prov, m:rs, final_u,is)
+ (NotCovered, NotDiverged) -> (m:rs, final_u,is)
-- inaccessible
- (NotCovered, Diverged ) -> (final_prov, rs, final_u, m:is)
+ (NotCovered, Diverged ) -> (rs, final_u, m:is)
hsLMatchToLPats :: LMatch id body -> Located [LPat id]
hsLMatchToLPats (dL->L l (Match { m_pats = pats })) = cL l pats
@@ -465,7 +385,7 @@ checkEmptyCase' var = do
pure $ fmap (ValVec [va]) mb_sat
return $ if null missing_m
then emptyPmResult
- else PmResult FromBuiltin [] (UncoveredPatterns missing_m) []
+ else PmResult [] (UncoveredPatterns missing_m) []
-- | Returns 'True' if the argument 'Type' is a fully saturated application of
-- a closed type constructor.
@@ -516,7 +436,7 @@ pmTopNormaliseType_maybe :: FamInstEnvs -> Bag EvVar -> Type
-- is a type family with a variable result kind. I (Richard E) can't think
-- of a way to cause trouble here, though.
pmTopNormaliseType_maybe env ty_cs typ
- = do (_, mb_typ') <- liftD $ initTcDsForSolver $ tcNormalise ty_cs typ
+ = do (_, mb_typ') <- initTcDsForSolver $ tcNormalise ty_cs typ
-- Before proceeding, we chuck typ into the constraint solver, in case
-- solving for given equalities may reduce typ some. See
-- "Wrinkle: local equalities" in
@@ -579,8 +499,8 @@ pmTopNormaliseType_maybe env ty_cs typ
-- for why this is done.)
pmInitialTmTyCs :: PmM Delta
pmInitialTmTyCs = do
- ty_cs <- liftD getDictsDs
- tm_cs <- bagToList <$> liftD getTmCsDs
+ ty_cs <- getDictsDs
+ tm_cs <- bagToList <$> getTmCsDs
sat_ty <- tyOracle ty_cs
let initTyCs = if sat_ty then ty_cs else emptyBag
initTmState = fromMaybe initialTmState (tmOracle initialTmState tm_cs)
@@ -628,7 +548,7 @@ that we expect.
pmIsSatisfiable
:: Delta -- ^ The ambient term and type constraints
-- (known to be satisfiable).
- -> TmEq -- ^ The new term constraint.
+ -> TmVarCt -- ^ The new term constraint.
-> Bag EvVar -- ^ The new type constraints.
-> [Type] -- ^ The strict argument types.
-> PmM (Maybe Delta)
@@ -654,7 +574,7 @@ pmIsSatisfiable amb_cs new_tm_c new_ty_cs strict_arg_tys = do
tmTyCsAreSatisfiable
:: Delta -- ^ The ambient term and type constraints
-- (known to be satisfiable).
- -> TmEq -- ^ The new term constraint.
+ -> TmVarCt -- ^ The new term constraint.
-> Bag EvVar -- ^ The new type constraints.
-> PmM (Maybe Delta)
-- ^ @'Just' delta@ if the constraints (@delta@) are
@@ -671,12 +591,61 @@ tmTyCsAreSatisfiable
, delta_tm_cs = term_cs }
_unsat -> Nothing
+-- | This weeds out patterns with 'PmVar's where at least one COMPLETE set is
+-- rendered vacuous by equality constraints.
+--
+-- This is quite costly due to the many oracle queries, so we only call this
+-- on the final uncovered set.
+normaliseUncovered :: Uncovered -> PmM Uncovered
+normaliseUncovered us = do
+ let valvec_inhabited p (ValVec vva delta) = runMaybeT $ do
+ vva' <- traverse (valabs_inhabited p delta) vva
+ pure (ValVec vva' delta)
+ valabs_inhabited p delta v = case v :: ValAbs of
+ pm at PmCon{ pm_con_args = args } -> do
+ args' <- traverse (valabs_inhabited p delta) args
+ pure pm { pm_con_args = args' }
+ PmVar x
+ | let (ty, ncons) = lookupRefutableAltCons x (delta_tm_cs delta)
+ , cls@(cl:_) <- [ cl | PmAltConLike cl <- ncons ]
+ -> do
+ grps <- lift (allCompleteMatches cl ty)
+ var_inh p delta x cls grps
+ _ -> pure v
+ var_inh p delta x ncons grps = do
+ let grp_inh = filterM (p delta x) . (\\ ncons)
+ incomplete_grps <- traverse grp_inh grps
+ -- If all cons of any COMPLETE set are matched, the ValVec is vacuous.
+ guard (all notNull incomplete_grps)
+ -- If there's a unique singleton incomplete group, turn it into a
+ -- `PmCon` for better readability of warning messages.
+ case incomplete_grps of
+ [[con]] -> do
+ -- We don't want to simplify to a `PmCon` (which won't normalise any
+ -- further) when @p@ is just the @cheap_inh_test at . Thus, we have to
+ -- assert satisfiability here, even if @actual_inh_test@ already did
+ -- so.
+ ic <- MaybeT $ mkOneSatisfiableConFull delta x con
+ pure (ic_val_abs ic)
+ _ -> pure (PmVar x)
+
+ -- We'll first do a cheap sweep without consulting the oracles
+ let cheap_inh_test _ _ _ = pure True
+ us1 <- mapMaybeM (valvec_inhabited cheap_inh_test) us
+ -- Then we'll do another pass trying to weed out the rest with (in)equalities
+ let actual_inh_test delta x con = do
+ lift (tracePm "nrm" (ppr con <+> ppr x <+> ppr (delta_tm_cs delta)))
+ isJust <$> lift (mkOneSatisfiableConFull delta x con)
+ us2 <- mapMaybeM (valvec_inhabited actual_inh_test) us1
+ tracePm "normaliseUncovered" (vcat (map pprValVecDebug us2))
+ pure us2
+
-- | Implements two performance optimizations, as described in the
-- \"Strict argument type constraints\" section of
-- @Note [Extensions to GADTs Meet Their Match]@.
checkAllNonVoid :: RecTcChecker -> Delta -> [Type] -> PmM Bool
checkAllNonVoid rec_ts amb_cs strict_arg_tys = do
- fam_insts <- liftD dsGetFamInstEnvs
+ fam_insts <- dsGetFamInstEnvs
let definitely_inhabited =
definitelyInhabitedType fam_insts (delta_ty_cs amb_cs)
tys_to_check <- filterOutM definitely_inhabited strict_arg_tys
@@ -833,7 +802,7 @@ equalities (such as i ~ Int) that may be in scope.
inhabitationCandidates :: Bag EvVar -> Type
-> PmM (Either Type (TyCon, [InhabitationCandidate]))
inhabitationCandidates ty_cs ty = do
- fam_insts <- liftD dsGetFamInstEnvs
+ fam_insts <- dsGetFamInstEnvs
mb_norm_res <- pmTopNormaliseType_maybe fam_insts ty_cs ty
case mb_norm_res of
Just (src_ty, dcs, core_ty) -> alts_to_check src_ty core_ty dcs
@@ -847,7 +816,7 @@ inhabitationCandidates ty_cs ty = do
-- PmCon empty, since we know that they are not gonna be used. Is the
-- right-thing-to-do to actually create them, even if they are never used?
build_tm :: ValAbs -> [DataCon] -> ValAbs
- build_tm = foldr (\dc e -> PmCon (RealDataCon dc) [] [] [] [e])
+ build_tm = foldr (\dc e -> PmCon (RealDataCon dc) [] [] [e])
-- Inhabitation candidates, using the result of pmTopNormaliseType_maybe
alts_to_check :: Type -> Type -> [DataCon]
@@ -857,7 +826,7 @@ inhabitationCandidates ty_cs ty = do
| tc `elem` trivially_inhabited
-> case dcs of
[] -> return (Left src_ty)
- (_:_) -> do var <- liftD $ mkPmId core_ty
+ (_:_) -> do var <- mkPmId core_ty
let va = build_tm (PmVar var) dcs
return $ Right (tc, [InhabitationCandidate
{ ic_val_abs = va, ic_tm_ct = mkIdEq var
@@ -867,7 +836,7 @@ inhabitationCandidates ty_cs ty = do
-- Don't consider abstract tycons since we don't know what their
-- constructors are, which makes the results of coverage checking
-- them extremely misleading.
- -> liftD $ do
+ -> do
var <- mkPmId core_ty -- it would be wrong to unify x
alts <- mapM (mkOneConFull var . RealDataCon) (tyConDataCons tc)
return $ Right
@@ -925,7 +894,7 @@ nullaryConPattern :: ConLike -> Pattern
-- Nullary data constructor and nullary type constructor
nullaryConPattern con =
PmCon { pm_con_con = con, pm_con_arg_tys = []
- , pm_con_tvs = [], pm_con_dicts = [], pm_con_args = [] }
+ , pm_con_tvs = [], pm_con_args = [] }
{-# INLINE nullaryConPattern #-}
truePattern :: Pattern
@@ -933,7 +902,7 @@ truePattern = nullaryConPattern (RealDataCon trueDataCon)
{-# INLINE truePattern #-}
-- | Generate a `canFail` pattern vector of a specific type
-mkCanFailPmPat :: Type -> DsM PatVec
+mkCanFailPmPat :: Type -> PmM PatVec
mkCanFailPmPat ty = do
var <- mkPmVar ty
return [var, PmFake]
@@ -942,21 +911,20 @@ vanillaConPattern :: ConLike -> [Type] -> PatVec -> Pattern
-- ADT constructor pattern => no existentials, no local constraints
vanillaConPattern con arg_tys args =
PmCon { pm_con_con = con, pm_con_arg_tys = arg_tys
- , pm_con_tvs = [], pm_con_dicts = [], pm_con_args = args }
+ , pm_con_tvs = [], pm_con_args = args }
{-# INLINE vanillaConPattern #-}
-- | Create an empty list pattern of a given type
nilPattern :: Type -> Pattern
nilPattern ty =
PmCon { pm_con_con = RealDataCon nilDataCon, pm_con_arg_tys = [ty]
- , pm_con_tvs = [], pm_con_dicts = []
- , pm_con_args = [] }
+ , pm_con_tvs = [], pm_con_args = [] }
{-# INLINE nilPattern #-}
mkListPatVec :: Type -> PatVec -> PatVec -> PatVec
mkListPatVec ty xs ys = [PmCon { pm_con_con = RealDataCon consDataCon
, pm_con_arg_tys = [ty]
- , pm_con_tvs = [], pm_con_dicts = []
+ , pm_con_tvs = []
, pm_con_args = xs++ys }]
{-# INLINE mkListPatVec #-}
@@ -968,7 +936,7 @@ mkLitPattern lit = PmLit { pm_lit_lit = PmSLit lit }
-- -----------------------------------------------------------------------
-- * Transform (Pat Id) into of (PmPat Id)
-translatePat :: FamInstEnvs -> Pat GhcTc -> DsM PatVec
+translatePat :: FamInstEnvs -> Pat GhcTc -> PmM PatVec
translatePat fam_insts pat = case pat of
WildPat ty -> mkPmVars [ty]
VarPat _ id -> return [PmVar (unLoc id)]
@@ -1047,17 +1015,16 @@ translatePat fam_insts pat = case pat of
ConPatOut { pat_con = (dL->L _ con)
, pat_arg_tys = arg_tys
, pat_tvs = ex_tvs
- , pat_dicts = dicts
, pat_args = ps } -> do
- groups <- allCompleteMatches con arg_tys
+ let ty = conLikeResTy con arg_tys
+ groups <- allCompleteMatches con ty
case groups of
- [] -> mkCanFailPmPat (conLikeResTy con arg_tys)
+ [] -> mkCanFailPmPat ty
_ -> do
args <- translateConPatVec fam_insts arg_tys ex_tvs con ps
return [PmCon { pm_con_con = con
, pm_con_arg_tys = arg_tys
, pm_con_tvs = ex_tvs
- , pm_con_dicts = dicts
, pm_con_args = args }]
-- See Note [Translate Overloaded Literal for Exhaustiveness Checking]
@@ -1185,12 +1152,12 @@ from translation in pattern matcher.
-- | Translate a list of patterns (Note: each pattern is translated
-- to a pattern vector but we do not concatenate the results).
-translatePatVec :: FamInstEnvs -> [Pat GhcTc] -> DsM [PatVec]
+translatePatVec :: FamInstEnvs -> [Pat GhcTc] -> PmM [PatVec]
translatePatVec fam_insts pats = mapM (translatePat fam_insts) pats
-- | Translate a constructor pattern
translateConPatVec :: FamInstEnvs -> [Type] -> [TyVar]
- -> ConLike -> HsConPatDetails GhcTc -> DsM PatVec
+ -> ConLike -> HsConPatDetails GhcTc -> PmM PatVec
translateConPatVec fam_insts _univ_tys _ex_tvs _ (PrefixCon ps)
= concat <$> translatePatVec fam_insts (map unLoc ps)
translateConPatVec fam_insts _univ_tys _ex_tvs _ (InfixCon p1 p2)
@@ -1246,11 +1213,12 @@ translateConPatVec fam_insts univ_tys ex_tvs c (RecCon (HsRecFields fs _))
-- Translate a single match
translateMatch :: FamInstEnvs -> LMatch GhcTc (LHsExpr GhcTc)
- -> DsM (PatVec,[PatVec])
+ -> PmM (PatVec,[PatVec])
translateMatch fam_insts (dL->L _ (Match { m_pats = lpats, m_grhss = grhss })) =
do
pats' <- concat <$> translatePatVec fam_insts pats
guards' <- mapM (translateGuards fam_insts) guards
+ -- tracePm "translateMatch" (vcat [ppr pats, ppr pats', ppr guards, ppr guards'])
return (pats', guards')
where
extractGuards :: LGRHS GhcTc (LHsExpr GhcTc) -> [GuardStmt GhcTc]
@@ -1265,11 +1233,11 @@ translateMatch _ _ = panic "translateMatch"
-- * Transform source guards (GuardStmt Id) to PmPats (Pattern)
-- | Translate a list of guard statements to a pattern vector
-translateGuards :: FamInstEnvs -> [GuardStmt GhcTc] -> DsM PatVec
+translateGuards :: FamInstEnvs -> [GuardStmt GhcTc] -> PmM PatVec
translateGuards fam_insts guards = do
all_guards <- concat <$> mapM (translateGuard fam_insts) guards
let
- shouldKeep :: Pattern -> DsM Bool
+ shouldKeep :: Pattern -> PmM Bool
shouldKeep p
| PmVar {} <- p = pure True
| PmCon {} <- p = (&&)
@@ -1294,7 +1262,7 @@ translateGuards fam_insts guards = do
pure (PmFake : kept)
-- | Check whether a pattern can fail to match
-cantFailPattern :: Pattern -> DsM Bool
+cantFailPattern :: Pattern -> PmM Bool
cantFailPattern PmVar {} = pure True
cantFailPattern PmCon { pm_con_con = c, pm_con_arg_tys = tys, pm_con_args = ps}
= (&&) <$> singleMatchConstructor c tys <*> allM cantFailPattern ps
@@ -1302,7 +1270,7 @@ cantFailPattern (PmGrd pv _e) = allM cantFailPattern pv
cantFailPattern _ = pure False
-- | Translate a guard statement to Pattern
-translateGuard :: FamInstEnvs -> GuardStmt GhcTc -> DsM PatVec
+translateGuard :: FamInstEnvs -> GuardStmt GhcTc -> PmM PatVec
translateGuard fam_insts guard = case guard of
BodyStmt _ e _ _ -> translateBoolGuard e
LetStmt _ binds -> translateLet (unLoc binds)
@@ -1315,18 +1283,18 @@ translateGuard fam_insts guard = case guard of
XStmtLR {} -> panic "translateGuard RecStmt"
-- | Translate let-bindings
-translateLet :: HsLocalBinds GhcTc -> DsM PatVec
+translateLet :: HsLocalBinds GhcTc -> PmM PatVec
translateLet _binds = return []
-- | Translate a pattern guard
-translateBind :: FamInstEnvs -> LPat GhcTc -> LHsExpr GhcTc -> DsM PatVec
+translateBind :: FamInstEnvs -> LPat GhcTc -> LHsExpr GhcTc -> PmM PatVec
translateBind fam_insts (dL->L _ p) e = do
ps <- translatePat fam_insts p
g <- mkGuard ps (unLoc e)
return [g]
-- | Translate a boolean guard
-translateBoolGuard :: LHsExpr GhcTc -> DsM PatVec
+translateBoolGuard :: LHsExpr GhcTc -> PmM PatVec
translateBoolGuard e
| isJust (isTrueLHsExpr e) = return []
-- The formal thing to do would be to generate (True <- True)
@@ -1427,10 +1395,17 @@ efficiently, which gave rise to #11276. The original approach translated
pat |> co ===> x (pat <- (e |> co))
-Instead, we now check whether the coercion is a hole or if it is just refl, in
-which case we can drop it. Unfortunately, data families generate useful
-coercions so guards are still generated in these cases and checking data
-families is not really efficient.
+Why did we do this seemingly unnecessary expansion in the first place?
+The reason is that the type of @pat |> co@ (which is the type of the value
+abstraction we match against) might be different than that of @pat at . Data
+instances such as @Sing (a :: Bool)@ are a good example of this: If we would
+just drop the coercion, we'd get a type error when matching @pat@ against its
+value abstraction, with the result being that pmIsSatisfiable decides that every
+possible data constructor fitting @pat@ is rejected as uninhabitated, leading to
+a lot of false warnings.
+
+But we can check whether the coercion is a hole or if it is just refl, in
+which case we can drop it.
%************************************************************************
%* *
@@ -1449,7 +1424,6 @@ pmPatType (PmCon { pm_con_con = con, pm_con_arg_tys = tys })
= conLikeResTy con tys
pmPatType (PmVar { pm_var_id = x }) = idType x
pmPatType (PmLit { pm_lit_lit = l }) = pmLitType l
-pmPatType (PmNLit { pm_lit_id = x }) = idType x
pmPatType (PmGrd { pm_grd_pv = pv })
= ASSERT(patVecArity pv == 1) (pmPatType p)
where Just p = find ((==1) . patternArity) pv
@@ -1464,7 +1438,7 @@ pmPatType PmFake = pmPatType truePattern
data InhabitationCandidate =
InhabitationCandidate
{ ic_val_abs :: ValAbs
- , ic_tm_ct :: TmEq
+ , ic_tm_ct :: TmVarCt
, ic_ty_cs :: Bag EvVar
, ic_strict_arg_tys :: [Type]
}
@@ -1477,10 +1451,13 @@ checker adheres to. Since the paper's publication, there have been some
additional features added to the coverage checker which are not described in
the paper. This Note serves as a reference for these new features.
------
--- Strict argument type constraints
------
+* Handling of uninhabited fields like `!Void`.
+ See Note [Strict argument type constraints]
+* Efficient handling of literal splitting, large enumerations and accurate
+ redundancy warnings for `COMPLETE` groups. See Note [PmNLit and PmNCon]
+Note [Strict argument type constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In the ConVar case of clause processing, each conlike K traditionally
generates two different forms of constraints:
@@ -1600,8 +1577,43 @@ intuition formal, we say that a type is definitely inhabitable (DI) if:
1. C has no equality constraints (since they might be unsatisfiable)
2. C has no strict argument types (since they might be uninhabitable)
-It's relatively cheap to cheap if a type is DI, so before we call `nonVoid`
+It's relatively cheap to check if a type is DI, so before we call `nonVoid`
on a list of strict argument types, we filter out all of the DI ones.
+
+Note [PmNLit and PmNCon]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+TLDR:
+* 'PmNLit' is an efficient encoding of literals we already matched on.
+ Important for checking redundancy without blowing up the term oracle.
+* 'PmNCon' is an efficient encoding of all constructors we already matched on.
+ Important for proper redundancy and completeness checks while being more
+ efficient than the `ConVar` split in GADTs Meet Their Match.
+
+GADTs Meet Their Match handled literals by desugaring to guard expressions,
+effectively encoding the knowledge in the term oracle. As it turned out, this
+doesn't scale (#11303, cf. Note [Literals in PmPat]), so we adopted an approach
+that encodes negative information about literals as a 'PmNLit', which encodes
+literal values the carried variable may no longer take on.
+
+The counterpart for constructor values is 'PmNCon', where we associate
+with a variable the topmost 'ConLike's it surely can't be. This is in contrast
+to GADTs Meet Their Match, where instead the `ConVar` case would split the value
+vector abstraction on all possible constructors from a `COMPLETE` group.
+In fact, we used to do just that, but committing to a particular `COMPLETE`
+group in `ConVar`, even nondeterministically, led to misleading redundancy
+warnings (#13363).
+Apart from that, splitting on huge enumerations in the presence of a catch-all
+case is a huge waste of resources.
+
+Note that since we have pattern guards, the term oracle must also be able to
+cope with negative equations involving literals and constructors, cf.
+Note [Refutable shapes] in TmOracle. Since we don't want to put too much strain
+on the term oracle with repeated coverage checks against all `COMPLETE` groups,
+we only do so once at the end in 'normaliseUncovered'.
+
+Peter Sestoft was probably the first to describe positive and negative
+information about terms in this manner in ML Pattern Match Compilation and
+Partial Evaluation.
-}
instance Outputable InhabitationCandidate where
@@ -1616,7 +1628,7 @@ instance Outputable InhabitationCandidate where
-- | Generate an 'InhabitationCandidate' for a given conlike (generate
-- fresh variables of the appropriate type for arguments)
-mkOneConFull :: Id -> ConLike -> DsM InhabitationCandidate
+mkOneConFull :: Id -> ConLike -> PmM InhabitationCandidate
-- * x :: T tys, where T is an algebraic data type
-- NB: in the case of a data family, T is the *representation* TyCon
-- e.g. data instance T (a,b) = T1 a b
@@ -1656,52 +1668,54 @@ mkOneConFull x con = do
let con_abs = PmCon { pm_con_con = con
, pm_con_arg_tys = tc_args
, pm_con_tvs = ex_tvs'
- , pm_con_dicts = evvars
, pm_con_args = arguments }
strict_arg_tys = filterByList arg_is_banged arg_tys'
return $ InhabitationCandidate
{ ic_val_abs = con_abs
- , ic_tm_ct = (x, vaToPmExpr con_abs)
+ , ic_tm_ct = TVC x (vaToPmExpr con_abs)
, ic_ty_cs = listToBag evvars
, ic_strict_arg_tys = strict_arg_tys
}
+-- | 'mkOneConFull' and immediately check whether the resulting
+-- 'InhabitationCandidat' @ic@ is inhabited by consulting 'pmIsSatisfiable'.
+-- Return @Just ic@ if it is.
+mkOneSatisfiableConFull :: Delta -> Id -> ConLike -> PmM (Maybe InhabitationCandidate)
+mkOneSatisfiableConFull delta x con = do
+ ic <- mkOneConFull x con
+ (ic <$) <$> pmIsSatisfiable delta (ic_tm_ct ic) (ic_ty_cs ic) (ic_strict_arg_tys ic)
+
-- ----------------------------------------------------------------------------
-- * More smart constructors and fresh variable generation
-- | Create a guard pattern
-mkGuard :: PatVec -> HsExpr GhcTc -> DsM Pattern
+mkGuard :: PatVec -> HsExpr GhcTc -> PmM Pattern
mkGuard pv e = do
res <- allM cantFailPattern pv
let expr = hsExprToPmExpr e
- tracePmD "mkGuard" (vcat [ppr pv, ppr e, ppr res, ppr expr])
+ tracePm "mkGuard" (vcat [ppr pv, ppr e, ppr res, ppr expr])
if | res -> pure (PmGrd pv expr)
| PmExprOther {} <- expr -> pure PmFake
| otherwise -> pure (PmGrd pv expr)
--- | Create a term equality of the form: `(x ~ lit)`
-mkPosEq :: Id -> PmLit -> TmEq
-mkPosEq x l = (x, PmExprLit l)
-{-# INLINE mkPosEq #-}
-
-- | Create a term equality of the form: `(x ~ x)`
-- (always discharged by the term oracle)
-mkIdEq :: Id -> TmEq
-mkIdEq x = (x, PmExprVar (idName x))
+mkIdEq :: Id -> TmVarCt
+mkIdEq x = TVC x (PmExprVar (idName x))
{-# INLINE mkIdEq #-}
-- | Generate a variable pattern of a given type
-mkPmVar :: Type -> DsM (PmPat p)
+mkPmVar :: Type -> PmM (PmPat p)
mkPmVar ty = PmVar <$> mkPmId ty
{-# INLINE mkPmVar #-}
-- | Generate many variable patterns, given a list of types
-mkPmVars :: [Type] -> DsM PatVec
+mkPmVars :: [Type] -> PmM PatVec
mkPmVars tys = mapM mkPmVar tys
{-# INLINE mkPmVars #-}
-- | Generate a fresh `Id` of a given type
-mkPmId :: Type -> DsM Id
+mkPmId :: Type -> PmM Id
mkPmId ty = getUniqueM >>= \unique ->
let occname = mkVarOccFS $ fsLit "$pm"
name = mkInternalName unique occname noSrcSpan
@@ -1710,7 +1724,7 @@ mkPmId ty = getUniqueM >>= \unique ->
-- | Generate a fresh term variable of a given and return it in two forms:
-- * A variable pattern
-- * A variable expression
-mkPmId2Forms :: Type -> DsM (Pattern, LHsExpr GhcTc)
+mkPmId2Forms :: Type -> PmM (Pattern, LHsExpr GhcTc)
mkPmId2Forms ty = do
x <- mkPmId ty
return (PmVar x, noLoc (HsVar noExt (noLoc x)))
@@ -1721,10 +1735,9 @@ mkPmId2Forms ty = do
-- | Convert a value abstraction an expression
vaToPmExpr :: ValAbs -> PmExpr
vaToPmExpr (PmCon { pm_con_con = c, pm_con_args = ps })
- = PmExprCon c (map vaToPmExpr ps)
+ = PmExprCon (PmAltConLike c) (map vaToPmExpr ps)
vaToPmExpr (PmVar { pm_var_id = x }) = PmExprVar (idName x)
-vaToPmExpr (PmLit { pm_lit_lit = l }) = PmExprLit l
-vaToPmExpr (PmNLit { pm_lit_id = x }) = PmExprVar (idName x)
+vaToPmExpr (PmLit { pm_lit_lit = l }) = mkPmExprLit l
-- | Convert a pattern vector to a list of value abstractions by dropping the
-- guards (See Note [Translating As Patterns])
@@ -1738,20 +1751,18 @@ coercePmPat :: Pattern -> [ValAbs]
coercePmPat (PmVar { pm_var_id = x }) = [PmVar { pm_var_id = x }]
coercePmPat (PmLit { pm_lit_lit = l }) = [PmLit { pm_lit_lit = l }]
coercePmPat (PmCon { pm_con_con = con, pm_con_arg_tys = arg_tys
- , pm_con_tvs = tvs, pm_con_dicts = dicts
- , pm_con_args = args })
+ , pm_con_tvs = tvs, pm_con_args = args })
= [PmCon { pm_con_con = con, pm_con_arg_tys = arg_tys
- , pm_con_tvs = tvs, pm_con_dicts = dicts
- , pm_con_args = coercePatVec args }]
+ , pm_con_tvs = tvs, pm_con_args = coercePatVec args }]
coercePmPat (PmGrd {}) = [] -- drop the guards
coercePmPat PmFake = [] -- drop the guards
-- | Check whether a 'ConLike' has the /single match/ property, i.e. whether
-- it is the only possible match in the given context. See also
-- 'allCompleteMatches' and Note [Single match constructors].
-singleMatchConstructor :: ConLike -> [Type] -> DsM Bool
+singleMatchConstructor :: ConLike -> [Type] -> PmM Bool
singleMatchConstructor cl tys =
- any (isSingleton . snd) <$> allCompleteMatches cl tys
+ any isSingleton <$> allCompleteMatches cl (conLikeResTy cl tys)
{-
Note [Single match constructors]
@@ -1786,20 +1797,17 @@ translation step. See #15753 for why this yields surprising results.
-- 2. From `COMPLETE` pragmas which have the same type as the result
-- type constructor. Note that we only use `COMPLETE` pragmas
-- *all* of whose pattern types match. See #14135
-allCompleteMatches :: ConLike -> [Type] -> DsM [(Provenance, [ConLike])]
-allCompleteMatches cl tys = do
+allCompleteMatches :: ConLike -> Type -> DsM [[ConLike]]
+allCompleteMatches cl ty = do
let fam = case cl of
RealDataCon dc ->
- [(FromBuiltin, map RealDataCon (tyConDataCons (dataConTyCon dc)))]
+ [map RealDataCon (tyConDataCons (dataConTyCon dc))]
PatSynCon _ -> []
- ty = conLikeResTy cl tys
pragmas <- case splitTyConApp_maybe ty of
Just (tc, _) -> dsGetCompleteMatches tc
Nothing -> return []
- let fams cm = (FromComplete,) <$>
- mapM dsLookupConLike (completeMatchConLikes cm)
- from_pragma <- filter (\(_,m) -> isValidCompleteMatch ty m) <$>
- mapM fams pragmas
+ let fams cm = mapM dsLookupConLike (completeMatchConLikes cm)
+ from_pragma <- filter (isValidCompleteMatch ty) <$> mapM fams pragmas
let final_groups = fam ++ from_pragma
return final_groups
where
@@ -1891,8 +1899,7 @@ nameType name ty = do
-- | Check whether a set of type constraints is satisfiable.
tyOracle :: Bag EvVar -> PmM Bool
tyOracle evs
- = liftD $
- do { ((_warns, errs), res) <- initTcDsForSolver $ tcCheckSatisfiability evs
+ = do { ((_warns, errs), res) <- initTcDsForSolver $ tcCheckSatisfiability evs
; case res of
Just sat -> return sat
Nothing -> pprPanic "tyOracle" (vcat $ pprErrMsgBagWithLoc errs) }
@@ -1974,7 +1981,7 @@ mkInitialUncovered vars = do
-- limit is not exceeded and call `pmcheck`
pmcheckI :: PatVec -> [PatVec] -> ValVec -> PmM PartialResult
pmcheckI ps guards vva = do
- n <- liftD incrCheckPmIterDs
+ n <- incrCheckPmIterDs
tracePm "pmCheck" (ppr n <> colon <+> pprPatVec ps
$$ hang (text "guards:") 2 (vcat (map pprPatVec guards))
$$ pprValVecDebug vva)
@@ -1986,7 +1993,7 @@ pmcheckI ps guards vva = do
-- | Increase the counter for elapsed algorithm iterations, check that the
-- limit is not exceeded and call `pmcheckGuards`
pmcheckGuardsI :: [PatVec] -> ValVec -> PmM PartialResult
-pmcheckGuardsI gvs vva = liftD incrCheckPmIterDs >> pmcheckGuards gvs vva
+pmcheckGuardsI gvs vva = incrCheckPmIterDs >> pmcheckGuards gvs vva
{-# INLINE pmcheckGuardsI #-}
-- | Increase the counter for elapsed algorithm iterations, check that the
@@ -1994,7 +2001,7 @@ pmcheckGuardsI gvs vva = liftD incrCheckPmIterDs >> pmcheckGuards gvs vva
pmcheckHdI :: Pattern -> PatVec -> [PatVec] -> ValAbs -> ValVec
-> PmM PartialResult
pmcheckHdI p ps guards va vva = do
- n <- liftD incrCheckPmIterDs
+ n <- incrCheckPmIterDs
tracePm "pmCheckHdI" (ppr n <> colon <+> pprPmPatDebug p
$$ pprPatVec ps
$$ hang (text "guards:") 2 (vcat (map pprPatVec guards))
@@ -2024,10 +2031,12 @@ pmcheck (PmFake : ps) guards vva =
pmcheck (p : ps) guards (ValVec vas delta)
| PmGrd { pm_grd_pv = pv, pm_grd_expr = e } <- p
= do
- y <- liftD $ mkPmId (pmPatType p)
+ tracePm "PmGrd: pmPatType" (hcat [ppr p, ppr (pmPatType p)])
+ y <- mkPmId (pmPatType p)
let tm_state = extendSubst y e (delta_tm_cs delta)
delta' = delta { delta_tm_cs = tm_state }
- utail <$> pmcheckI (pv ++ ps) guards (ValVec (PmVar y : vas) delta')
+ pr <- pmcheckI (pv ++ ps) guards (ValVec (PmVar y : vas) delta')
+ pure $ utail pr
pmcheck [] _ (ValVec (_:_) _) = panic "pmcheck: nil-cons"
pmcheck (_:_) _ (ValVec [] _) = panic "pmcheck: cons-nil"
@@ -2039,10 +2048,9 @@ pmcheck (p:ps) guards (ValVec (va:vva) delta)
pmcheckGuards :: [PatVec] -> ValVec -> PmM PartialResult
pmcheckGuards [] vva = return (usimple [vva])
pmcheckGuards (gv:gvs) vva = do
- (PartialResult prov1 cs vsa ds) <- pmcheckI gv [] vva
- (PartialResult prov2 css vsas dss) <- runMany (pmcheckGuardsI gvs) vsa
- return $ PartialResult (prov1 `mappend` prov2)
- (cs `mappend` css)
+ (PartialResult cs vsa ds) <- pmcheckI gv [] vva
+ (PartialResult css vsas dss) <- runMany (pmcheckGuardsI gvs) vsa
+ return $ PartialResult (cs `mappend` css)
vsas
(ds `mappend` dss)
@@ -2054,7 +2062,7 @@ pmcheckHd :: Pattern -> PatVec -> [PatVec] -> ValAbs -> ValVec
-- Var
pmcheckHd (PmVar x) ps guards va (ValVec vva delta)
- | Just tm_state <- solveOneEq (delta_tm_cs delta) (x, vaToPmExpr va)
+ | Just tm_state <- solveOneEq (delta_tm_cs delta) (TVC x (vaToPmExpr va))
= ucon va <$> pmcheckI ps guards (ValVec vva (delta {delta_tm_cs = tm_state}))
| otherwise = return mempty
@@ -2077,72 +2085,52 @@ pmcheckHd ( p@(PmCon { pm_con_con = c1, pm_con_tvs = ex_tvs1
| otherwise = Just <$> to_evvar tv1 tv2
evvars <- (listToBag . catMaybes) <$>
ASSERT(ex_tvs1 `equalLength` ex_tvs2)
- liftD (zipWithM mb_to_evvar ex_tvs1 ex_tvs2)
+ (zipWithM mb_to_evvar ex_tvs1 ex_tvs2)
let delta' = delta { delta_ty_cs = evvars `unionBags` delta_ty_cs delta }
- kcon c1 (pm_con_arg_tys p) (pm_con_tvs p) (pm_con_dicts p)
+ kcon c1 (pm_con_arg_tys p) (pm_con_tvs p)
<$> pmcheckI (args1 ++ ps) guards (ValVec (args2 ++ vva) delta')
-- LitLit
-pmcheckHd (PmLit l1) ps guards (va@(PmLit l2)) vva =
- case eqPmLit l1 l2 of
- True -> ucon va <$> pmcheckI ps guards vva
- False -> return $ ucon va (usimple [vva])
+pmcheckHd (PmLit l1) ps guards (va@(PmLit l2)) vva
+ | l1 == l2 = ucon va <$> pmcheckI ps guards vva
+ | otherwise = return $ ucon va (usimple [vva])
-- ConVar
-pmcheckHd (p@(PmCon { pm_con_con = con, pm_con_arg_tys = tys }))
- ps guards
- (PmVar x) (ValVec vva delta) = do
- (prov, complete_match) <- select =<< liftD (allCompleteMatches con tys)
-
- cons_cs <- mapM (liftD . mkOneConFull x) complete_match
-
- inst_vsa <- flip mapMaybeM cons_cs $
- \InhabitationCandidate{ ic_val_abs = va, ic_tm_ct = tm_ct
- , ic_ty_cs = ty_cs
- , ic_strict_arg_tys = strict_arg_tys } -> do
- mb_sat <- pmIsSatisfiable delta tm_ct ty_cs strict_arg_tys
- pure $ fmap (ValVec (va:vva)) mb_sat
-
- set_provenance prov .
- force_if (canDiverge (idName x) (delta_tm_cs delta)) <$>
- runMany (pmcheckI (p:ps) guards) inst_vsa
+pmcheckHd p at PmCon{} ps guards (PmVar x) vva@(ValVec vas delta) = do
+ -- Split the value vector into two value vectors: One representing the current
+ -- constructor, the other representing everything but the current constructor
+ -- (and the already known impossible constructors).
+ let con = pm_con_con p
+
+ -- For the value vector of the current constructor, we directly recurse into
+ -- checking the the current case, so we get back a PartialResult
+ ic <- mkOneConFull x con
+ mb_delta' <- pmIsSatisfiable delta (ic_tm_ct ic) (ic_ty_cs ic) (ic_strict_arg_tys ic)
+ pr_pos <- case mb_delta' of
+ Nothing -> pure mempty
+ Just delta' -> do
+ tracePm "success" (ppr (delta_tm_cs delta))
+ pmcheckHdI p ps guards (ic_val_abs ic) (ValVec vas delta')
+
+ let pr_neg = mkUnmatched x (PmAltConLike con) vva
+ tracePm "ConVar" (vcat [ppr p, ppr x, ppr pr_pos, ppr pr_neg])
+
+ -- Combine both into a single PartialResult
+ let pr = mkUnion pr_pos pr_neg
+ pure (forceIfCanDiverge x (delta_tm_cs delta) pr)
-- LitVar
-pmcheckHd (p@(PmLit l)) ps guards (PmVar x) (ValVec vva delta)
- = force_if (canDiverge (idName x) (delta_tm_cs delta)) <$>
- mkUnion non_matched <$>
- case solveOneEq (delta_tm_cs delta) (mkPosEq x l) of
- Just tm_state -> pmcheckHdI p ps guards (PmLit l) $
- ValVec vva (delta {delta_tm_cs = tm_state})
- Nothing -> return mempty
- where
- -- See Note [Refutable shapes] in TmOracle
- us | Just tm_state <- addSolveRefutableAltCon (delta_tm_cs delta) x (PmAltLit l)
- = [ValVec (PmNLit x [l] : vva) (delta { delta_tm_cs = tm_state })]
- | otherwise = []
+pmcheckHd p@(PmLit l) ps guards (PmVar x) vva@(ValVec vas delta) = do
+ pr_pos <- case solveOneEq (delta_tm_cs delta) (TVC x (mkPmExprLit l)) of
+ Nothing -> pure mempty
+ Just tms -> pmcheckHdI p ps guards (PmLit l) vva'
+ where
+ vva'= ValVec vas (delta { delta_tm_cs = tms })
- non_matched = usimple us
-
--- LitNLit
-pmcheckHd (p@(PmLit l)) ps guards
- (PmNLit { pm_lit_id = x, pm_lit_not = lits }) (ValVec vva delta)
- | all (not . eqPmLit l) lits
- , Just tm_state <- solveOneEq (delta_tm_cs delta) (mkPosEq x l)
- -- Both guards check the same so it would be sufficient to have only
- -- the second one. Nevertheless, it is much cheaper to check whether
- -- the literal is in the list so we check it first, to avoid calling
- -- the term oracle (`solveOneEq`) if possible
- = mkUnion non_matched <$>
- pmcheckHdI p ps guards (PmLit l)
- (ValVec vva (delta { delta_tm_cs = tm_state }))
- | otherwise = return non_matched
- where
- -- See Note [Refutable shapes] in TmOracle
- us | Just tm_state <- addSolveRefutableAltCon (delta_tm_cs delta) x (PmAltLit l)
- = [ValVec (PmNLit x (l:lits) : vva) (delta { delta_tm_cs = tm_state })]
- | otherwise = []
+ let pr_neg = mkUnmatched x (PmAltLit l) vva
- non_matched = usimple us
+ let pr = mkUnion pr_pos pr_neg
+ pure (forceIfCanDiverge x (delta_tm_cs delta) pr)
-- ----------------------------------------------------------------------------
-- The following three can happen only in cases like #322 where constructors
@@ -2153,7 +2141,7 @@ pmcheckHd (p@(PmLit l)) ps guards
-- LitCon
pmcheckHd p at PmLit{} ps guards va at PmCon{} (ValVec vva delta)
- = do y <- liftD $ mkPmId (pmPatType va)
+ = do y <- mkPmId (pmPatType va)
-- Analogous to the ConVar case, we have to case split the value
-- abstraction on possible literals. We do so by introducing a fresh
-- variable that is equated to the constructor. LitVar will then take
@@ -2164,18 +2152,14 @@ pmcheckHd p at PmLit{} ps guards va at PmCon{} (ValVec vva delta)
-- ConLit
pmcheckHd p at PmCon{} ps guards (PmLit l) (ValVec vva delta)
- = do y <- liftD $ mkPmId (pmPatType p)
+ = do y <- mkPmId (pmPatType p)
-- This desugars to the ConVar case by introducing a fresh variable that
-- is equated to the literal via a constraint. ConVar will then properly
-- case split on all possible constructors.
- let tm_state = extendSubst y (PmExprLit l) (delta_tm_cs delta)
+ let tm_state = extendSubst y (mkPmExprLit l) (delta_tm_cs delta)
delta' = delta { delta_tm_cs = tm_state }
pmcheckHdI p ps guards (PmVar y) (ValVec vva delta')
--- ConNLit
-pmcheckHd (p@(PmCon {})) ps guards (PmNLit { pm_lit_id = x }) vva
- = pmcheckHdI p ps guards (PmVar x) vva
-
-- Impossible: handled by pmcheck
pmcheckHd PmFake _ _ _ _ = panic "pmcheckHd: Fake"
pmcheckHd (PmGrd {}) _ _ _ _ = panic "pmcheckHd: Guard"
@@ -2323,9 +2307,8 @@ ucon va = updateVsa upd
-- value vector abstractions of length `(a+n)`, pass the first `n` value
-- abstractions to the constructor (Hence, the resulting value vector
-- abstractions will have length `n+1`)
-kcon :: ConLike -> [Type] -> [TyVar] -> [EvVar]
- -> PartialResult -> PartialResult
-kcon con arg_tys ex_tvs dicts
+kcon :: ConLike -> [Type] -> [TyVar] -> PartialResult -> PartialResult
+kcon con arg_tys ex_tvs
= let n = conLikeArity con
upd vsa =
[ ValVec (va:vva) delta
@@ -2334,7 +2317,6 @@ kcon con arg_tys ex_tvs dicts
, let va = PmCon { pm_con_con = con
, pm_con_arg_tys = arg_tys
, pm_con_tvs = ex_tvs
- , pm_con_dicts = dicts
, pm_con_args = args } ]
in updateVsa upd
@@ -2354,13 +2336,19 @@ mkCons vva = updateVsa (vva:)
forces :: PartialResult -> PartialResult
forces pres = pres { presultDivergent = Diverged }
--- | Set the divergent set to non-empty if the flag is `True`
-force_if :: Bool -> PartialResult -> PartialResult
-force_if True pres = forces pres
-force_if False pres = pres
+-- | Set the divergent set to non-empty if the variable has not been forced yet
+forceIfCanDiverge :: Id -> TmState -> PartialResult -> PartialResult
+forceIfCanDiverge x tms
+ | canDiverge (idName x) tms = forces
+ | otherwise = id
-set_provenance :: Provenance -> PartialResult -> PartialResult
-set_provenance prov pr = pr { presultProvenance = prov }
+mkUnmatched :: Id -> PmAltCon -> ValVec -> PartialResult
+mkUnmatched x nalt (ValVec vva delta) = usimple us
+ where
+ -- See Note [Refutable shapes] in TmOracle
+ us | Just tms <- tryAddRefutableAltCon (delta_tm_cs delta) x nalt
+ = [ValVec (PmVar x : vva) (delta { delta_tm_cs = tms })]
+ | otherwise = []
-- ----------------------------------------------------------------------------
-- * Propagation of term constraints inwards when checking nested matches
@@ -2369,7 +2357,7 @@ set_provenance prov pr = pr { presultProvenance = prov }
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When checking a match it would be great to have all type and term information
available so we can get more precise results. For this reason we have functions
-`addDictsDs' and `addTmCsDs' in PmMonad that store in the environment type and
+`addDictsDs' and `addTmCsDs' in DsMonad that store in the environment type and
term constraints (respectively) as we go deeper.
The type constraints we propagate inwards are collected by `collectEvVarsPats'
@@ -2403,22 +2391,22 @@ these constraints.
genCaseTmCs2 :: Maybe (LHsExpr GhcTc) -- Scrutinee
-> [Pat GhcTc] -- LHS (should have length 1)
-> [Id] -- MatchVars (should have length 1)
- -> DsM (Bag TmEq)
+ -> DsM (Bag TmVarCt)
genCaseTmCs2 Nothing _ _ = return emptyBag
genCaseTmCs2 (Just scr) [p] [var] = do
fam_insts <- dsGetFamInstEnvs
[e] <- map vaToPmExpr . coercePatVec <$> translatePat fam_insts p
let scr_e = lhsExprToPmExpr scr
- return $ listToBag [(var, e), (var, scr_e)]
+ return $ listToBag [(TVC var e), (TVC var scr_e)]
genCaseTmCs2 _ _ _ = panic "genCaseTmCs2: HsCase"
-- | Generate a simple equality when checking a case expression:
-- case x of { matches }
-- When checking matches we record that (x ~ y) where y is the initial
-- uncovered. All matches will have to satisfy this equality.
-genCaseTmCs1 :: Maybe (LHsExpr GhcTc) -> [Id] -> Bag TmEq
+genCaseTmCs1 :: Maybe (LHsExpr GhcTc) -> [Id] -> Bag TmVarCt
genCaseTmCs1 Nothing _ = emptyBag
-genCaseTmCs1 (Just scr) [var] = unitBag (var, lhsExprToPmExpr scr)
+genCaseTmCs1 (Just scr) [var] = unitBag (TVC var (lhsExprToPmExpr scr))
genCaseTmCs1 _ _ = panic "genCaseTmCs1: HsCase"
{- Note [Literals in PmPat]
@@ -2486,15 +2474,15 @@ instance Outputable ValVec where
-- | Apply a term substitution to a value vector abstraction. All VAs are
-- transformed to PmExpr (used only before pretty printing).
-substInValAbs :: PmVarEnv -> [ValAbs] -> [PmExpr]
+substInValAbs :: TmVarCtEnv -> [ValAbs] -> [PmExpr]
substInValAbs subst = map (exprDeepLookup subst . vaToPmExpr)
-- | Issue all the warnings (coverage, exhaustiveness, inaccessibility)
dsPmWarn :: DynFlags -> DsMatchContext -> PmResult -> DsM ()
dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result
= when (flag_i || flag_u) $ do
- let exists_r = flag_i && notNull redundant && onlyBuiltin
- exists_i = flag_i && notNull inaccessible && onlyBuiltin && not is_rec_upd
+ let exists_r = flag_i && notNull redundant
+ exists_i = flag_i && notNull inaccessible && not is_rec_upd
exists_u = flag_u && (case uncovered of
TypeOfUncovered _ -> True
UncoveredPatterns u -> notNull u)
@@ -2511,8 +2499,7 @@ dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result
UncoveredPatterns candidates -> pprEqns candidates
where
PmResult
- { pmresultProvenance = prov
- , pmresultRedundant = redundant
+ { pmresultRedundant = redundant
, pmresultUncovered = uncovered
, pmresultInaccessible = inaccessible } = pm_result
@@ -2523,8 +2510,6 @@ dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result
is_rec_upd = case kind of { RecUpd -> True; _ -> False }
-- See Note [Inaccessible warnings for record updates]
- onlyBuiltin = prov == FromBuiltin
-
maxPatterns = maxUncoveredPatterns dflags
-- Print a single clause (for redundant/with-inaccessible-rhs)
@@ -2637,11 +2622,7 @@ pprPats kind pats
-- Debugging Infrastructre
tracePm :: String -> SDoc -> PmM ()
-tracePm herald doc = liftD $ tracePmD herald doc
-
-
-tracePmD :: String -> SDoc -> DsM ()
-tracePmD herald doc = do
+tracePm herald doc = do
dflags <- getDynFlags
printer <- mkPrintUnqualifiedDs
liftIO $ dumpIfSet_dyn_printer printer dflags
@@ -2649,11 +2630,10 @@ tracePmD herald doc = do
pprPmPatDebug :: PmPat a -> SDoc
-pprPmPatDebug (PmCon cc _arg_tys _con_tvs _con_dicts con_args)
+pprPmPatDebug (PmCon cc _arg_tys _con_tvs con_args)
= hsep [text "PmCon", ppr cc, hsep (map pprPmPatDebug con_args)]
pprPmPatDebug (PmVar vid) = text "PmVar" <+> ppr vid
pprPmPatDebug (PmLit li) = text "PmLit" <+> ppr li
-pprPmPatDebug (PmNLit i nl) = text "PmNLit" <+> ppr i <+> ppr nl
pprPmPatDebug (PmGrd pv ge) = text "PmGrd" <+> hsep (map pprPmPatDebug pv)
<+> ppr ge
pprPmPatDebug PmFake = text "PmFake"
@@ -2671,5 +2651,5 @@ pprValAbs ps = hang (text "ValAbs:") 2
pprValVecDebug :: ValVec -> SDoc
pprValVecDebug (ValVec vas _d) = text "ValVec" <+>
parens (pprValAbs vas)
- -- <not a haddock> $$ ppr (delta_tm_cs _d)
+ $$ ppr (delta_tm_cs _d)
-- <not a haddock> $$ ppr (delta_ty_cs _d)
=====================================
compiler/deSugar/DsMonad.hs
=====================================
@@ -396,11 +396,11 @@ addDictsDs ev_vars
= updLclEnv (\env -> env { dsl_dicts = unionBags ev_vars (dsl_dicts env) })
-- | Get in-scope term constraints (pm check)
-getTmCsDs :: DsM (Bag TmEq)
+getTmCsDs :: DsM (Bag TmVarCt)
getTmCsDs = do { env <- getLclEnv; return (dsl_tm_cs env) }
-- | Add in-scope term constraints (pm check)
-addTmCsDs :: Bag TmEq -> DsM a -> DsM a
+addTmCsDs :: Bag TmVarCt -> DsM a -> DsM a
addTmCsDs tm_cs
= updLclEnv (\env -> env { dsl_tm_cs = unionBags tm_cs (dsl_tm_cs env) })
=====================================
compiler/deSugar/PmExpr.hs
=====================================
@@ -9,14 +9,15 @@ Haskell expressions (as used by the pattern matching checker) and utilities.
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module PmExpr (
- PmExpr(..), PmLit(..), PmAltCon(..), TmEq,
- eqPmLit, isNotPmExprOther, lhsExprToPmExpr, hsExprToPmExpr
+ PmExpr(..), PmLit(..), PmAltCon(..), TmVarCt(..), isNotPmExprOther,
+ lhsExprToPmExpr, hsExprToPmExpr, mkPmExprLit, pmExprAsList
) where
#include "HsVersions.h"
import GhcPrelude
+import Util
import BasicTypes (SourceText)
import FastString (FastString, unpackFS)
import HsSyn
@@ -53,34 +54,29 @@ 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 Overloaded Literals]
data PmLit = PmSLit (HsLit GhcTc) -- simple
| PmOLit Bool {- is it negated? -} (HsOverLit GhcTc) -- overloaded
+ deriving Eq
--- | 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.
+-- | 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
+ deriving Eq
-instance Eq PmAltCon where
- PmAltLit l1 == PmAltLit l2 = eqPmLit l1 l2
+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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -148,8 +144,11 @@ impact of this is the following:
appearance of the warnings and is, in practice safe.
-}
--- | Term equalities
-type TmEq = (Id, PmExpr)
+-- | A term constraint. @TVC x e@ encodes that @x@ is equal to @e at .
+data TmVarCt = TVC !Id !PmExpr
+
+instance Outputable TmVarCt where
+ ppr (TVC x e) = ppr x <+> char '~' <+> ppr e
-- ----------------------------------------------------------------------------
-- ** Predicates on PmExpr
@@ -189,17 +188,17 @@ hsExprToPmExpr (HsVar _ x) = PmExprVar (idName (unLoc x))
hsExprToPmExpr (HsOverLit _ olit)
| OverLit (OverLitTc False ty) (HsIsString src s) _ <- olit, isStringTy ty
= stringExprToList src s
- | otherwise = PmExprLit (PmOLit False olit)
+ | 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 at . when extension
-- @RebindableSyntax@ enabled, (-(-x)) may not equals to x.
- = PmExprLit (PmOLit True olit)
+ = PmExprCon (PmAltLit (PmOLit False olit)) []
| otherwise = PmExprOther e
hsExprToPmExpr (HsPar _ (dL->L _ e)) = hsExprToPmExpr e
@@ -246,7 +245,22 @@ 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
+
+-- | Extract a list of 'PmExpr's out of a sequence of cons cells.
+pmExprAsList :: PmExpr -> Maybe [PmExpr]
+pmExprAsList (pmExprToDataConApp -> Just (c, es))
+ | c == nilDataCon
+ = ASSERT( null es ) Just []
+ | c == consDataCon
+ = ASSERT( length es == 2 ) (es !! 0 :) <$> pmExprAsList (es !! 1)
+pmExprAsList _
+ = Nothing
{-
%************************************************************************
@@ -260,18 +274,18 @@ 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 _ (pmExprAsList -> Just list)
+ = brackets $ fsep $ punctuate comma $ map ppr list
+ 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) (hcat (ppr cl:map (go 1) args))
=====================================
compiler/deSugar/PmPpr.hs
=====================================
@@ -21,8 +21,8 @@ import TysWiredIn
import Outputable
import Control.Monad.Trans.State.Strict
import Maybes
-import Util
+import PmExpr
import TmOracle
-- | Pretty-print the guts of an uncovered value vector abstraction, i.e., its
@@ -35,6 +35,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 +48,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 +94,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, (_ty, lits)) = (old, (new, lits))
-- 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 +132,33 @@ 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 list <- pmExprAsList (PmExprCon (PmAltConLike cl) args)
+ = brackets . fsep . punctuate comma <$> mapM pprPmExpr list
+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 +174,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
=====================================
compiler/deSugar/TmOracle.hs
=====================================
@@ -5,20 +5,16 @@ Author: George Karachalias <george.karachalias at 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(..), TmEq, PmVarEnv, PmRefutEnv,
- eqPmLit, isNotPmExprOther, lhsExprToPmExpr, hsExprToPmExpr,
-
-- the term oracle
- tmOracle, TmState, initialTmState, wrapUpTmState, solveOneEq,
- extendSubst, canDiverge, isRigid,
- addSolveRefutableAltCon, lookupRefutableAltCons,
+ tmOracle, TmVarCtEnv, PmRefutEnv, TmState, initialTmState,
+ wrapUpTmState, solveOneEq, extendSubst, canDiverge, isRigid,
+ tryAddRefutableAltCon, lookupRefutableAltCons,
-- misc.
exprDeepLookup, pmLitType
@@ -33,16 +29,16 @@ import PmExpr
import Util
import Id
import Name
+import NameEnv
+import UniqFM
+import UniqDFM
import Type
import HsLit
import TcHsSyn
import MonadUtils
-import ListSetOps (insertNoDup, unionLists)
+import ListSetOps (unionLists)
import Maybes
import Outputable
-import NameEnv
-import UniqFM
-import UniqDFM
{-
%************************************************************************
@@ -52,25 +48,29 @@ import UniqDFM
%************************************************************************
-}
--- | The type of substitutions.
-type PmVarEnv = NameEnv PmExpr
+-- | Pretty much a @['TmVarCt']@ association list where the domain is 'Name'
+-- instead of 'Id'. This is the type of 'tm_pos', where we store solutions for
+-- rigid pattern match variables.
+type TmVarCtEnv = NameEnv PmExpr
-- | An environment assigning shapes to variables that immediately lead to a
-- refutation. So, if this maps @x :-> [Just]@, then trying to solve a
--- 'TmEq' like @x ~ Just False@ immediately leads to a contradiction.
+-- 'TmVarCt' like @x ~ Just False@ immediately leads to a contradiction.
+-- Additionally, this stores the 'Type' from which to draw 'ConLike's from.
+--
-- Determinism is important since we use this for warning messages in
--- 'PmPpr.pprUncovered'. We don't do the same for 'PmVarEnv', so that is a plain
+-- 'PmPpr.pprUncovered'. We don't do the same for 'TmVarCtEnv', so that is a plain
-- 'NameEnv'.
--
-- See also Note [Refutable shapes] in TmOracle.
-type PmRefutEnv = DNameEnv [PmAltCon]
+type PmRefutEnv = DNameEnv (Type, [PmAltCon])
-- | The state of the term oracle. Tracks all term-level facts of the form "x is
-- @True@" ('tm_pos') and "x is not @5@" ('tm_neg').
--
-- Subject to Note [The Pos/Neg invariant].
data TmState = TmS
- { tm_pos :: !PmVarEnv
+ { tm_pos :: !TmVarCtEnv
-- ^ A substitution with solutions we extend with every step and return as a
-- result. The substitution is in /triangular form/: It might map @x@ to @y@
-- where @y@ itself occurs in the domain of 'tm_pos', rendering lookup
@@ -78,12 +78,20 @@ data TmState = TmS
-- along a chain of var-to-var mappings until we find the solution but has the
-- advantage that when we update the solution for @y@ above, we automatically
-- update the solution for @x@ in a union-find-like fashion.
- , tm_neg :: !PmRefutEnv
+ -- Invariant: Only maps to other variables ('PmExprVar') or to WHNFs
+ -- ('PmExprCon'). Ergo, never maps to a 'PmExprOther'.
+ , tm_neg :: !PmRefutEnv
-- ^ Maps each variable @x@ to a list of 'PmAltCon's that @x@ definitely
- -- cannot match. Example, @x :-> [3, 4]@ means that @x@ cannot match a literal
- -- 3 or 4. Should we later solve @x@ to a variable @y@
- -- ('extendSubstAndSolve'), we merge the refutable shapes of @x@ into those of
- -- @y at . See also Note [The Pos/Neg invariant].
+ -- cannot match. Example, assuming
+ --
+ -- @
+ -- data T = Leaf Int | Branch T T | Node Int T
+ -- @
+ --
+ -- then @x :-> [Leaf, Node]@ means that @x@ cannot match a @Leaf@ or @Node@,
+ -- and hence can only match @Branch at . Should we later solve @x@ to a variable
+ -- @y@ ('extendSubstAndSolve'), we merge the refutable shapes of @x@ into
+ -- those of @y at . See also Note [The Pos/Neg invariant].
}
{- Note [The Pos/Neg invariant]
@@ -92,7 +100,7 @@ Invariant: In any 'TmState', The domains of 'tm_pos' and 'tm_neg' are disjoint.
For example, it would make no sense to say both
tm_pos = [...x :-> 3 ...]
- tm_neg = [...x :-> [3,42]... ]
+ tm_neg = [...x :-> [4,42]... ]
The positive information is strictly more informative than the negative.
Suppose we are adding the (positive) fact @x :-> e@ to 'tm_pos'. Then we must
@@ -109,7 +117,7 @@ instance Outputable TmState where
pos = map pos_eq (nonDetUFMToList (tm_pos state))
neg = map neg_eq (udfmToList (tm_neg state))
pos_eq (l, r) = ppr l <+> char '~' <+> ppr r
- neg_eq (l, r) = ppr l <+> char '≁' <+> ppr r
+ neg_eq (l, r) = ppr l <+> text "/~" <+> ppr r
-- | Initial state of the oracle.
initialTmState :: TmState
@@ -117,13 +125,13 @@ initialTmState = TmS emptyNameEnv emptyDNameEnv
-- | Wrap up the term oracle's state once solving is complete. Return the
-- flattened 'tm_pos' and 'tm_neg'.
-wrapUpTmState :: TmState -> (PmVarEnv, PmRefutEnv)
+wrapUpTmState :: TmState -> (TmVarCtEnv, PmRefutEnv)
wrapUpTmState solver_state
- = (flattenPmVarEnv (tm_pos solver_state), tm_neg solver_state)
+ = (flattenTmVarCtEnv (tm_pos solver_state), tm_neg solver_state)
-- | Flatten the triangular subsitution.
-flattenPmVarEnv :: PmVarEnv -> PmVarEnv
-flattenPmVarEnv env = mapNameEnv (exprDeepLookup env) env
+flattenTmVarCtEnv :: TmVarCtEnv -> TmVarCtEnv
+flattenTmVarCtEnv env = mapNameEnv (exprDeepLookup env) env
-- | Check whether a constraint (x ~ BOT) can succeed,
-- given the resulting state of the term oracle.
@@ -144,21 +152,23 @@ canDiverge x TmS{ tm_pos = pos, tm_neg = neg }
-- | Check whether the equality @x ~ e@ leads to a refutation. Make sure that
-- @x@ and @e@ are completely substituted before!
isRefutable :: Name -> PmExpr -> PmRefutEnv -> Bool
-isRefutable x e env
- = fromMaybe False $ elem <$> exprToAlt e <*> lookupDNameEnv env x
+isRefutable x e env = fromMaybe False $ do
+ alt <- exprToAlt e
+ (_, nalts) <- lookupDNameEnv env x
+ pure (elem alt nalts)
-- | Solve an equality (top-level).
-solveOneEq :: TmState -> TmEq -> Maybe TmState
-solveOneEq solver_env (x, e) = unify solver_env (PmExprVar (idName x), e)
+solveOneEq :: TmState -> TmVarCt -> Maybe TmState
+solveOneEq solver_env (TVC x e) = unify solver_env (PmExprVar (idName x), e)
exprToAlt :: PmExpr -> Maybe PmAltCon
-exprToAlt (PmExprLit l) = Just (PmAltLit l)
-exprToAlt _ = Nothing
+exprToAlt (PmExprCon c _) = Just c
+exprToAlt _ = Nothing
-- | Record that a particular 'Id' can't take the shape of a 'PmAltCon' in the
-- 'TmState' and return @Nothing@ if that leads to a contradiction.
-addSolveRefutableAltCon :: TmState -> Id -> PmAltCon -> Maybe TmState
-addSolveRefutableAltCon original at TmS{ tm_pos = pos, tm_neg = neg } x nalt
+tryAddRefutableAltCon :: TmState -> Id -> PmAltCon -> Maybe TmState
+tryAddRefutableAltCon original at TmS{ tm_pos = pos, tm_neg = neg } x nalt
= case exprToAlt e of
-- We have to take care to preserve Note [The Pos/Neg invariant]
Nothing -> Just extended -- Not solved yet
@@ -168,20 +178,24 @@ addSolveRefutableAltCon original at TmS{ tm_pos = pos, tm_neg = neg } x nalt
where -- refutation redundant
(y, e) = varDeepLookup pos (idName x)
extended = original { tm_neg = neg' }
- neg' = alterDNameEnv (delNulls (insertNoDup nalt)) neg y
+ neg' = extendDNameEnv_C combineRefutEntries neg y (idType x, [nalt])
--- | When updating 'tm_neg', we want to delete any 'null' entries. This adapter
--- intends to provide a suitable interface for 'alterDNameEnv'.
-delNulls :: ([a] -> [a]) -> Maybe [a] -> Maybe [a]
-delNulls f mb_entry
- | ret@(_:_) <- f (fromMaybe [] mb_entry) = Just ret
- | otherwise = Nothing
+-- | Combines two entries in a 'PmRefutEnv' by merging the set of refutable
+-- 'PmAltCon's.
+combineRefutEntries :: (Type, [PmAltCon]) -> (Type, [PmAltCon]) -> (Type, [PmAltCon])
+combineRefutEntries (old_ty, old_nalts) (new_ty, new_nalts)
+ = ASSERT( eqType old_ty new_ty ) (old_ty, unionLists old_nalts new_nalts)
-- | Return all 'PmAltCon' shapes that are impossible for 'Id' to take, i.e.
-- would immediately lead to a refutation by the term oracle.
-lookupRefutableAltCons :: Id -> TmState -> [PmAltCon]
-lookupRefutableAltCons x TmS { tm_neg = neg }
- = fromMaybe [] (lookupDNameEnv neg (idName x))
+--
+-- Precondition: The queried Id 'isFlexible'.
+lookupRefutableAltCons :: Id -> TmState -> (Type, [PmAltCon])
+lookupRefutableAltCons x _tms at TmS{ tm_pos = pos, tm_neg = neg }
+ = ASSERT( not (isSolution _e) )
+ fromMaybe (idType x, []) (lookupDNameEnv neg y)
+ where
+ (y, _e) = varDeepLookup pos (idName x)
-- | Is the given variable /rigid/ (i.e., we have a solution for it) or
-- /flexible/ (i.e., no solution)? Returns the solution if /rigid/. A
@@ -193,6 +207,11 @@ isRigid TmS{ tm_pos = pos } x = lookupNameEnv pos x
isFlexible :: TmState -> Name -> Bool
isFlexible tms = isNothing . isRigid tms
+-- | Is this a solution for a variable, i.e., something in WHNF?
+isSolution :: PmExpr -> Bool
+isSolution PmExprCon{} = True
+isSolution _ = False
+
-- | Try to unify two 'PmExpr's and record the gained knowledge in the
-- 'TmState'.
--
@@ -205,12 +224,8 @@ unify tms eq@(e1, e2) = case eq of
(PmExprOther _,_) -> boring
(_,PmExprOther _) -> boring
- (PmExprLit l1, PmExprLit l2) -> case eqPmLit l1 l2 of
- -- See Note [Undecidable Equality for Overloaded Literals]
- True -> boring
- False -> unsat
-
(PmExprCon c1 ts1, PmExprCon c2 ts2)
+ -- See Note [Undecidable Equality for Overloaded Literals]
| c1 == c2 -> foldlM unify tms (zip ts1 ts2)
| otherwise -> unsat
@@ -224,42 +239,46 @@ unify tms eq@(e1, e2) = case eq of
| Just e1' <- isRigid tms x -> unify tms (e1', e2)
(_, PmExprVar y)
| Just e2' <- isRigid tms y -> unify tms (e1, e2')
- (PmExprVar x, _) -> extendSubstAndSolve x e2 tms
- (_, PmExprVar y) -> extendSubstAndSolve y e1 tms
-
- _ -> WARN( True, text "unify: Catch all" <+> ppr eq)
- boring -- I HATE CATCH-ALLS
+ (PmExprVar x, PmExprVar y) -> Just (equate x y tms)
+ (PmExprVar x, _) -> trySolve x e2 tms
+ (_, PmExprVar y) -> trySolve y e1 tms
where
boring = Just tms
unsat = Nothing
+-- | Merges the equivalence classes of @x@ and @y@ by extending the substitution
+-- with @x :-> y at .
+-- Preconditions: @x /= y@ and both @x@ and @y@ are flexible (cf.
+-- 'isFlexible'/'isRigid').
+equate :: Name -> Name -> TmState -> TmState
+equate x y tms at TmS{ tm_pos = pos, tm_neg = neg }
+ = ASSERT( x /= y )
+ ASSERT( isFlexible tms x )
+ ASSERT( isFlexible tms y )
+ tms'
+ where
+ pos' = extendNameEnv pos x (PmExprVar y)
+ -- Be careful to uphold Note [The Pos/Neg invariant] by merging the refuts
+ -- of x into those of y
+ neg' = case lookupDNameEnv neg x of
+ Nothing -> neg
+ Just entry -> extendDNameEnv_C combineRefutEntries neg y entry
+ `delFromDNameEnv` x
+ tms' = TmS { tm_pos = pos', tm_neg = neg' }
+
-- | Extend the substitution with a mapping @x: -> e@ if compatible with
-- refutable shapes of @x@ and its solution, reject (@Nothing@) otherwise.
--
--- Precondition: @a@ is flexible (cf. 'isFlexible'/'isRigid').
--- Precondition: @e@ is not @y@, where @y@ is in the equivalence class
--- represented by @x at .
-extendSubstAndSolve :: Name -> PmExpr -> TmState -> Maybe TmState
-extendSubstAndSolve x e _tms at TmS{ tm_pos = pos, tm_neg = neg }
+-- Precondition: @x@ is flexible (cf. 'isFlexible'/'isRigid').
+-- Precondition: @e@ is a solution, i.e., 'PmExprCon' (cf. 'isSolution').
+trySolve:: Name -> PmExpr -> TmState -> Maybe TmState
+trySolve x e _tms at TmS{ tm_pos = pos, tm_neg = neg }
| ASSERT( isFlexible _tms x )
- ASSERT( _assert_is_not_cyclic )
- isRefutable x e' neg -- NB: e', the newly flattened solution for @x@
+ ASSERT( isSolution e )
+ isRefutable x e neg
= Nothing
| otherwise
- = Just (TmS new_pos new_neg)
- where
- new_pos = extendNameEnv pos x e
- (y, e') = varDeepLookup new_pos x
- -- Be careful to uphold Note [The Pos/Neg invariant] by adjusting 'tm_neg'
- neg' | x == y = neg
- | otherwise = case lookupDNameEnv neg x of
- Nothing -> neg
- Just nalts ->
- alterDNameEnv (delNulls (unionLists nalts)) neg y
- new_neg = delFromDNameEnv neg' x
- _assert_is_not_cyclic = case e of
- PmExprVar z -> fst (varDeepLookup pos z) /= x
- _ -> True
+ = Just (TmS (extendNameEnv pos x e) (delFromDNameEnv neg x))
-- | When we know that a variable is fresh, we do not actually have to
-- check whether anything changes, we know that nothing does. Hence,
@@ -278,7 +297,7 @@ extendSubst y e solver_state at TmS{ tm_pos = pos }
-- representative in the triangular substitution @env@ and the completely
-- substituted expression. The latter may just be the representative wrapped
-- with 'PmExprVar' if we haven't found a solution for it yet.
-varDeepLookup :: PmVarEnv -> Name -> (Name, PmExpr)
+varDeepLookup :: TmVarCtEnv -> Name -> (Name, PmExpr)
varDeepLookup env x = case lookupNameEnv env x of
Just (PmExprVar y) -> varDeepLookup env y
Just e -> (x, exprDeepLookup env e) -- go deeper
@@ -286,13 +305,13 @@ varDeepLookup env x = case lookupNameEnv env x of
{-# INLINE varDeepLookup #-}
-- | Apply an (un-flattened) substitution to an expression.
-exprDeepLookup :: PmVarEnv -> PmExpr -> PmExpr
+exprDeepLookup :: TmVarCtEnv -> PmExpr -> PmExpr
exprDeepLookup env (PmExprVar x) = snd (varDeepLookup env x)
exprDeepLookup env (PmExprCon c es) = PmExprCon c (map (exprDeepLookup env) es)
-exprDeepLookup _ other_expr = other_expr -- PmExprLit, PmExprOther
+exprDeepLookup _ e at PmExprOther{} = e
-- | External interface to the term oracle.
-tmOracle :: TmState -> [TmEq] -> Maybe TmState
+tmOracle :: TmState -> [TmVarCt] -> Maybe TmState
tmOracle tm_state eqs = foldlM solveOneEq tm_state eqs
-- | Type of a PmLit
@@ -340,9 +359,17 @@ second clause and report the clause as redundant. After the third clause, the
set of such *refutable* literals is again extended to `[0, 1]`.
In general, we want to store a set of refutable shapes (`PmAltCon`) for each
-variable. That's the purpose of the `PmRefutEnv`. `addSolveRefutableAltCon` will
-add such a refutable mapping to the `PmRefutEnv` in the term oracles state and
-check if causes any immediate contradiction. Whenever we record a solution in
-the substitution via `extendSubstAndSolve`, the refutable environment is checked
-for any matching refutable `PmAltCon`.
+variable. That's the purpose of the `PmRefutEnv`. This extends to
+`ConLike`s, where all value arguments are universally quantified implicitly.
+So, if the `PmRefutEnv` contains an entry for `x` with `Just [Bool]`, then this
+corresponds to the fact that `forall y. x ≁ Just @Bool y`.
+
+`tryAddRefutableAltCon` will add such a refutable mapping to the `PmRefutEnv`
+in the term oracles state and check if it causes any immediate contradiction.
+Whenever we record a solution in the substitution via `extendSubstAndSolve`, the
+refutable environment is checked for any matching refutable `PmAltCon`.
+
+Note that `PmAltConLike` carries a list of type arguments. This purely for the
+purpose of being able to reconstruct all other constructors of the matching
+group the `ConLike` is part of through calling `allCompleteMatches` in Check.
-}
=====================================
compiler/typecheck/TcRnTypes.hs
=====================================
@@ -391,7 +391,7 @@ data DsLclEnv = DsLclEnv {
-- These two fields are augmented as we walk inwards,
-- through each patttern match in turn
dsl_dicts :: Bag EvVar, -- Constraints from GADT pattern-matching
- dsl_tm_cs :: Bag TmEq, -- Constraints form term-level pattern matching
+ dsl_tm_cs :: Bag TmVarCt, -- Constraints form term-level pattern matching
dsl_pm_iter :: IORef Int -- Number of iterations for pmcheck so far
-- We fail if this gets too big
=====================================
compiler/utils/Binary.hs
=====================================
@@ -724,7 +724,6 @@ putTypeRep bh (Fun arg res) = do
put_ bh (3 :: Word8)
putTypeRep bh arg
putTypeRep bh res
-putTypeRep _ _ = fail "Binary.putTypeRep: Impossible"
getSomeTypeRep :: BinHandle -> IO SomeTypeRep
getSomeTypeRep bh = do
=====================================
compiler/utils/ListSetOps.hs
=====================================
@@ -14,7 +14,7 @@ module ListSetOps (
Assoc, assoc, assocMaybe, assocUsing, assocDefault, assocDefaultUsing,
-- Duplicate handling
- hasNoDups, removeDups, findDupsEq, insertNoDup,
+ hasNoDups, removeDups, findDupsEq,
equivClasses,
-- Indexing
@@ -169,10 +169,3 @@ findDupsEq _ [] = []
findDupsEq eq (x:xs) | null eq_xs = findDupsEq eq xs
| otherwise = (x :| eq_xs) : findDupsEq eq neq_xs
where (eq_xs, neq_xs) = partition (eq x) xs
-
--- | \( O(n) \). @'insertNoDup' x xs@ treats @xs@ as a set, inserting @x@ only
--- when an equal element couldn't be found in @xs at .
-insertNoDup :: (Eq a) => a -> [a] -> [a]
-insertNoDup x set
- | elem x set = set
- | otherwise = x:set
=====================================
docs/users_guide/glasgow_exts.rst
=====================================
@@ -15420,49 +15420,6 @@ the user must provide a type signature. ::
foo :: [a] -> Int
foo T = 5
-.. _multiple-complete-pragmas:
-
-Disambiguating between multiple ``COMPLETE`` pragmas
-----------------------------------------------------
-
-What should happen if there are multiple ``COMPLETE`` sets that apply to a
-single set of patterns? Consider this example: ::
-
- data T = MkT1 | MkT2 | MkT2Internal
- {-# COMPLETE MkT1, MkT2 #-}
- {-# COMPLETE MkT1, MkT2Internal #-}
-
- f :: T -> Bool
- f MkT1 = True
- f MkT2 = False
-
-Which ``COMPLETE`` pragma should be used when checking the coverage of the
-patterns in ``f``? If we pick the ``COMPLETE`` set that covers ``MkT1`` and
-``MkT2``, then ``f`` is exhaustive, but if we pick the other ``COMPLETE`` set
-that covers ``MkT1`` and ``MkT2Internal``, then ``f`` is *not* exhaustive,
-since it fails to match ``MkT2Internal``. An intuitive way to solve this
-dilemma is to recognize that picking the former ``COMPLETE`` set produces the
-fewest number of uncovered pattern clauses, and thus is the better choice.
-
-GHC disambiguates between multiple ``COMPLETE`` sets based on this rationale.
-To make things more formal, when the pattern-match checker requests a set of
-constructors for some data type constructor ``T``, the checker returns:
-
-* The original set of data constructors for ``T``
-* Any ``COMPLETE`` sets of type ``T``
-
-GHC then checks for pattern coverage using each of these sets. If any of these
-sets passes the pattern coverage checker with no warnings, then we are done. If
-each set produces at least one warning, then GHC must pick one of the sets of
-warnings depending on how good the results are. The results are prioritized in
-this order:
-
-1. Fewest uncovered clauses
-2. Fewest redundant clauses
-3. Fewest inaccessible clauses
-4. Whether the match comes from the original set of data constructors or from a
- ``COMPLETE`` pragma (prioritizing the former over the latter)
-
.. _overlap-pragma:
``OVERLAPPING``, ``OVERLAPPABLE``, ``OVERLAPS``, and ``INCOHERENT`` pragmas
=====================================
testsuite/tests/perf/compiler/ManyAlternatives.hs
=====================================
@@ -0,0 +1,2005 @@
+module ManyAlternatives where
+
+data A1000 = A0
+ | A0001
+ | A0002
+ | A0003
+ | A0004
+ | A0005
+ | A0006
+ | A0007
+ | A0008
+ | A0009
+ | A0010
+ | A0011
+ | A0012
+ | A0013
+ | A0014
+ | A0015
+ | A0016
+ | A0017
+ | A0018
+ | A0019
+ | A0020
+ | A0021
+ | A0022
+ | A0023
+ | A0024
+ | A0025
+ | A0026
+ | A0027
+ | A0028
+ | A0029
+ | A0030
+ | A0031
+ | A0032
+ | A0033
+ | A0034
+ | A0035
+ | A0036
+ | A0037
+ | A0038
+ | A0039
+ | A0040
+ | A0041
+ | A0042
+ | A0043
+ | A0044
+ | A0045
+ | A0046
+ | A0047
+ | A0048
+ | A0049
+ | A0050
+ | A0051
+ | A0052
+ | A0053
+ | A0054
+ | A0055
+ | A0056
+ | A0057
+ | A0058
+ | A0059
+ | A0060
+ | A0061
+ | A0062
+ | A0063
+ | A0064
+ | A0065
+ | A0066
+ | A0067
+ | A0068
+ | A0069
+ | A0070
+ | A0071
+ | A0072
+ | A0073
+ | A0074
+ | A0075
+ | A0076
+ | A0077
+ | A0078
+ | A0079
+ | A0080
+ | A0081
+ | A0082
+ | A0083
+ | A0084
+ | A0085
+ | A0086
+ | A0087
+ | A0088
+ | A0089
+ | A0090
+ | A0091
+ | A0092
+ | A0093
+ | A0094
+ | A0095
+ | A0096
+ | A0097
+ | A0098
+ | A0099
+ | A0100
+ | A0101
+ | A0102
+ | A0103
+ | A0104
+ | A0105
+ | A0106
+ | A0107
+ | A0108
+ | A0109
+ | A0110
+ | A0111
+ | A0112
+ | A0113
+ | A0114
+ | A0115
+ | A0116
+ | A0117
+ | A0118
+ | A0119
+ | A0120
+ | A0121
+ | A0122
+ | A0123
+ | A0124
+ | A0125
+ | A0126
+ | A0127
+ | A0128
+ | A0129
+ | A0130
+ | A0131
+ | A0132
+ | A0133
+ | A0134
+ | A0135
+ | A0136
+ | A0137
+ | A0138
+ | A0139
+ | A0140
+ | A0141
+ | A0142
+ | A0143
+ | A0144
+ | A0145
+ | A0146
+ | A0147
+ | A0148
+ | A0149
+ | A0150
+ | A0151
+ | A0152
+ | A0153
+ | A0154
+ | A0155
+ | A0156
+ | A0157
+ | A0158
+ | A0159
+ | A0160
+ | A0161
+ | A0162
+ | A0163
+ | A0164
+ | A0165
+ | A0166
+ | A0167
+ | A0168
+ | A0169
+ | A0170
+ | A0171
+ | A0172
+ | A0173
+ | A0174
+ | A0175
+ | A0176
+ | A0177
+ | A0178
+ | A0179
+ | A0180
+ | A0181
+ | A0182
+ | A0183
+ | A0184
+ | A0185
+ | A0186
+ | A0187
+ | A0188
+ | A0189
+ | A0190
+ | A0191
+ | A0192
+ | A0193
+ | A0194
+ | A0195
+ | A0196
+ | A0197
+ | A0198
+ | A0199
+ | A0200
+ | A0201
+ | A0202
+ | A0203
+ | A0204
+ | A0205
+ | A0206
+ | A0207
+ | A0208
+ | A0209
+ | A0210
+ | A0211
+ | A0212
+ | A0213
+ | A0214
+ | A0215
+ | A0216
+ | A0217
+ | A0218
+ | A0219
+ | A0220
+ | A0221
+ | A0222
+ | A0223
+ | A0224
+ | A0225
+ | A0226
+ | A0227
+ | A0228
+ | A0229
+ | A0230
+ | A0231
+ | A0232
+ | A0233
+ | A0234
+ | A0235
+ | A0236
+ | A0237
+ | A0238
+ | A0239
+ | A0240
+ | A0241
+ | A0242
+ | A0243
+ | A0244
+ | A0245
+ | A0246
+ | A0247
+ | A0248
+ | A0249
+ | A0250
+ | A0251
+ | A0252
+ | A0253
+ | A0254
+ | A0255
+ | A0256
+ | A0257
+ | A0258
+ | A0259
+ | A0260
+ | A0261
+ | A0262
+ | A0263
+ | A0264
+ | A0265
+ | A0266
+ | A0267
+ | A0268
+ | A0269
+ | A0270
+ | A0271
+ | A0272
+ | A0273
+ | A0274
+ | A0275
+ | A0276
+ | A0277
+ | A0278
+ | A0279
+ | A0280
+ | A0281
+ | A0282
+ | A0283
+ | A0284
+ | A0285
+ | A0286
+ | A0287
+ | A0288
+ | A0289
+ | A0290
+ | A0291
+ | A0292
+ | A0293
+ | A0294
+ | A0295
+ | A0296
+ | A0297
+ | A0298
+ | A0299
+ | A0300
+ | A0301
+ | A0302
+ | A0303
+ | A0304
+ | A0305
+ | A0306
+ | A0307
+ | A0308
+ | A0309
+ | A0310
+ | A0311
+ | A0312
+ | A0313
+ | A0314
+ | A0315
+ | A0316
+ | A0317
+ | A0318
+ | A0319
+ | A0320
+ | A0321
+ | A0322
+ | A0323
+ | A0324
+ | A0325
+ | A0326
+ | A0327
+ | A0328
+ | A0329
+ | A0330
+ | A0331
+ | A0332
+ | A0333
+ | A0334
+ | A0335
+ | A0336
+ | A0337
+ | A0338
+ | A0339
+ | A0340
+ | A0341
+ | A0342
+ | A0343
+ | A0344
+ | A0345
+ | A0346
+ | A0347
+ | A0348
+ | A0349
+ | A0350
+ | A0351
+ | A0352
+ | A0353
+ | A0354
+ | A0355
+ | A0356
+ | A0357
+ | A0358
+ | A0359
+ | A0360
+ | A0361
+ | A0362
+ | A0363
+ | A0364
+ | A0365
+ | A0366
+ | A0367
+ | A0368
+ | A0369
+ | A0370
+ | A0371
+ | A0372
+ | A0373
+ | A0374
+ | A0375
+ | A0376
+ | A0377
+ | A0378
+ | A0379
+ | A0380
+ | A0381
+ | A0382
+ | A0383
+ | A0384
+ | A0385
+ | A0386
+ | A0387
+ | A0388
+ | A0389
+ | A0390
+ | A0391
+ | A0392
+ | A0393
+ | A0394
+ | A0395
+ | A0396
+ | A0397
+ | A0398
+ | A0399
+ | A0400
+ | A0401
+ | A0402
+ | A0403
+ | A0404
+ | A0405
+ | A0406
+ | A0407
+ | A0408
+ | A0409
+ | A0410
+ | A0411
+ | A0412
+ | A0413
+ | A0414
+ | A0415
+ | A0416
+ | A0417
+ | A0418
+ | A0419
+ | A0420
+ | A0421
+ | A0422
+ | A0423
+ | A0424
+ | A0425
+ | A0426
+ | A0427
+ | A0428
+ | A0429
+ | A0430
+ | A0431
+ | A0432
+ | A0433
+ | A0434
+ | A0435
+ | A0436
+ | A0437
+ | A0438
+ | A0439
+ | A0440
+ | A0441
+ | A0442
+ | A0443
+ | A0444
+ | A0445
+ | A0446
+ | A0447
+ | A0448
+ | A0449
+ | A0450
+ | A0451
+ | A0452
+ | A0453
+ | A0454
+ | A0455
+ | A0456
+ | A0457
+ | A0458
+ | A0459
+ | A0460
+ | A0461
+ | A0462
+ | A0463
+ | A0464
+ | A0465
+ | A0466
+ | A0467
+ | A0468
+ | A0469
+ | A0470
+ | A0471
+ | A0472
+ | A0473
+ | A0474
+ | A0475
+ | A0476
+ | A0477
+ | A0478
+ | A0479
+ | A0480
+ | A0481
+ | A0482
+ | A0483
+ | A0484
+ | A0485
+ | A0486
+ | A0487
+ | A0488
+ | A0489
+ | A0490
+ | A0491
+ | A0492
+ | A0493
+ | A0494
+ | A0495
+ | A0496
+ | A0497
+ | A0498
+ | A0499
+ | A0500
+ | A0501
+ | A0502
+ | A0503
+ | A0504
+ | A0505
+ | A0506
+ | A0507
+ | A0508
+ | A0509
+ | A0510
+ | A0511
+ | A0512
+ | A0513
+ | A0514
+ | A0515
+ | A0516
+ | A0517
+ | A0518
+ | A0519
+ | A0520
+ | A0521
+ | A0522
+ | A0523
+ | A0524
+ | A0525
+ | A0526
+ | A0527
+ | A0528
+ | A0529
+ | A0530
+ | A0531
+ | A0532
+ | A0533
+ | A0534
+ | A0535
+ | A0536
+ | A0537
+ | A0538
+ | A0539
+ | A0540
+ | A0541
+ | A0542
+ | A0543
+ | A0544
+ | A0545
+ | A0546
+ | A0547
+ | A0548
+ | A0549
+ | A0550
+ | A0551
+ | A0552
+ | A0553
+ | A0554
+ | A0555
+ | A0556
+ | A0557
+ | A0558
+ | A0559
+ | A0560
+ | A0561
+ | A0562
+ | A0563
+ | A0564
+ | A0565
+ | A0566
+ | A0567
+ | A0568
+ | A0569
+ | A0570
+ | A0571
+ | A0572
+ | A0573
+ | A0574
+ | A0575
+ | A0576
+ | A0577
+ | A0578
+ | A0579
+ | A0580
+ | A0581
+ | A0582
+ | A0583
+ | A0584
+ | A0585
+ | A0586
+ | A0587
+ | A0588
+ | A0589
+ | A0590
+ | A0591
+ | A0592
+ | A0593
+ | A0594
+ | A0595
+ | A0596
+ | A0597
+ | A0598
+ | A0599
+ | A0600
+ | A0601
+ | A0602
+ | A0603
+ | A0604
+ | A0605
+ | A0606
+ | A0607
+ | A0608
+ | A0609
+ | A0610
+ | A0611
+ | A0612
+ | A0613
+ | A0614
+ | A0615
+ | A0616
+ | A0617
+ | A0618
+ | A0619
+ | A0620
+ | A0621
+ | A0622
+ | A0623
+ | A0624
+ | A0625
+ | A0626
+ | A0627
+ | A0628
+ | A0629
+ | A0630
+ | A0631
+ | A0632
+ | A0633
+ | A0634
+ | A0635
+ | A0636
+ | A0637
+ | A0638
+ | A0639
+ | A0640
+ | A0641
+ | A0642
+ | A0643
+ | A0644
+ | A0645
+ | A0646
+ | A0647
+ | A0648
+ | A0649
+ | A0650
+ | A0651
+ | A0652
+ | A0653
+ | A0654
+ | A0655
+ | A0656
+ | A0657
+ | A0658
+ | A0659
+ | A0660
+ | A0661
+ | A0662
+ | A0663
+ | A0664
+ | A0665
+ | A0666
+ | A0667
+ | A0668
+ | A0669
+ | A0670
+ | A0671
+ | A0672
+ | A0673
+ | A0674
+ | A0675
+ | A0676
+ | A0677
+ | A0678
+ | A0679
+ | A0680
+ | A0681
+ | A0682
+ | A0683
+ | A0684
+ | A0685
+ | A0686
+ | A0687
+ | A0688
+ | A0689
+ | A0690
+ | A0691
+ | A0692
+ | A0693
+ | A0694
+ | A0695
+ | A0696
+ | A0697
+ | A0698
+ | A0699
+ | A0700
+ | A0701
+ | A0702
+ | A0703
+ | A0704
+ | A0705
+ | A0706
+ | A0707
+ | A0708
+ | A0709
+ | A0710
+ | A0711
+ | A0712
+ | A0713
+ | A0714
+ | A0715
+ | A0716
+ | A0717
+ | A0718
+ | A0719
+ | A0720
+ | A0721
+ | A0722
+ | A0723
+ | A0724
+ | A0725
+ | A0726
+ | A0727
+ | A0728
+ | A0729
+ | A0730
+ | A0731
+ | A0732
+ | A0733
+ | A0734
+ | A0735
+ | A0736
+ | A0737
+ | A0738
+ | A0739
+ | A0740
+ | A0741
+ | A0742
+ | A0743
+ | A0744
+ | A0745
+ | A0746
+ | A0747
+ | A0748
+ | A0749
+ | A0750
+ | A0751
+ | A0752
+ | A0753
+ | A0754
+ | A0755
+ | A0756
+ | A0757
+ | A0758
+ | A0759
+ | A0760
+ | A0761
+ | A0762
+ | A0763
+ | A0764
+ | A0765
+ | A0766
+ | A0767
+ | A0768
+ | A0769
+ | A0770
+ | A0771
+ | A0772
+ | A0773
+ | A0774
+ | A0775
+ | A0776
+ | A0777
+ | A0778
+ | A0779
+ | A0780
+ | A0781
+ | A0782
+ | A0783
+ | A0784
+ | A0785
+ | A0786
+ | A0787
+ | A0788
+ | A0789
+ | A0790
+ | A0791
+ | A0792
+ | A0793
+ | A0794
+ | A0795
+ | A0796
+ | A0797
+ | A0798
+ | A0799
+ | A0800
+ | A0801
+ | A0802
+ | A0803
+ | A0804
+ | A0805
+ | A0806
+ | A0807
+ | A0808
+ | A0809
+ | A0810
+ | A0811
+ | A0812
+ | A0813
+ | A0814
+ | A0815
+ | A0816
+ | A0817
+ | A0818
+ | A0819
+ | A0820
+ | A0821
+ | A0822
+ | A0823
+ | A0824
+ | A0825
+ | A0826
+ | A0827
+ | A0828
+ | A0829
+ | A0830
+ | A0831
+ | A0832
+ | A0833
+ | A0834
+ | A0835
+ | A0836
+ | A0837
+ | A0838
+ | A0839
+ | A0840
+ | A0841
+ | A0842
+ | A0843
+ | A0844
+ | A0845
+ | A0846
+ | A0847
+ | A0848
+ | A0849
+ | A0850
+ | A0851
+ | A0852
+ | A0853
+ | A0854
+ | A0855
+ | A0856
+ | A0857
+ | A0858
+ | A0859
+ | A0860
+ | A0861
+ | A0862
+ | A0863
+ | A0864
+ | A0865
+ | A0866
+ | A0867
+ | A0868
+ | A0869
+ | A0870
+ | A0871
+ | A0872
+ | A0873
+ | A0874
+ | A0875
+ | A0876
+ | A0877
+ | A0878
+ | A0879
+ | A0880
+ | A0881
+ | A0882
+ | A0883
+ | A0884
+ | A0885
+ | A0886
+ | A0887
+ | A0888
+ | A0889
+ | A0890
+ | A0891
+ | A0892
+ | A0893
+ | A0894
+ | A0895
+ | A0896
+ | A0897
+ | A0898
+ | A0899
+ | A0900
+ | A0901
+ | A0902
+ | A0903
+ | A0904
+ | A0905
+ | A0906
+ | A0907
+ | A0908
+ | A0909
+ | A0910
+ | A0911
+ | A0912
+ | A0913
+ | A0914
+ | A0915
+ | A0916
+ | A0917
+ | A0918
+ | A0919
+ | A0920
+ | A0921
+ | A0922
+ | A0923
+ | A0924
+ | A0925
+ | A0926
+ | A0927
+ | A0928
+ | A0929
+ | A0930
+ | A0931
+ | A0932
+ | A0933
+ | A0934
+ | A0935
+ | A0936
+ | A0937
+ | A0938
+ | A0939
+ | A0940
+ | A0941
+ | A0942
+ | A0943
+ | A0944
+ | A0945
+ | A0946
+ | A0947
+ | A0948
+ | A0949
+ | A0950
+ | A0951
+ | A0952
+ | A0953
+ | A0954
+ | A0955
+ | A0956
+ | A0957
+ | A0958
+ | A0959
+ | A0960
+ | A0961
+ | A0962
+ | A0963
+ | A0964
+ | A0965
+ | A0966
+ | A0967
+ | A0968
+ | A0969
+ | A0970
+ | A0971
+ | A0972
+ | A0973
+ | A0974
+ | A0975
+ | A0976
+ | A0977
+ | A0978
+ | A0979
+ | A0980
+ | A0981
+ | A0982
+ | A0983
+ | A0984
+ | A0985
+ | A0986
+ | A0987
+ | A0988
+ | A0989
+ | A0990
+ | A0991
+ | A0992
+ | A0993
+ | A0994
+ | A0995
+ | A0996
+ | A0997
+ | A0998
+ | A0999
+ | A1000
+
+f :: A1000 -> Int
+f A0001 = 1990001
+f A0002 = 1990002
+f A0003 = 1990003
+f A0004 = 1990004
+f A0005 = 1990005
+f A0006 = 1990006
+f A0007 = 1990007
+f A0008 = 1990008
+f A0009 = 1990009
+f A0010 = 1990010
+f A0011 = 1990011
+f A0012 = 1990012
+f A0013 = 1990013
+f A0014 = 1990014
+f A0015 = 1990015
+f A0016 = 1990016
+f A0017 = 1990017
+f A0018 = 1990018
+f A0019 = 1990019
+f A0020 = 1990020
+f A0021 = 1990021
+f A0022 = 1990022
+f A0023 = 1990023
+f A0024 = 1990024
+f A0025 = 1990025
+f A0026 = 1990026
+f A0027 = 1990027
+f A0028 = 1990028
+f A0029 = 1990029
+f A0030 = 1990030
+f A0031 = 1990031
+f A0032 = 1990032
+f A0033 = 1990033
+f A0034 = 1990034
+f A0035 = 1990035
+f A0036 = 1990036
+f A0037 = 1990037
+f A0038 = 1990038
+f A0039 = 1990039
+f A0040 = 1990040
+f A0041 = 1990041
+f A0042 = 1990042
+f A0043 = 1990043
+f A0044 = 1990044
+f A0045 = 1990045
+f A0046 = 1990046
+f A0047 = 1990047
+f A0048 = 1990048
+f A0049 = 1990049
+f A0050 = 1990050
+f A0051 = 1990051
+f A0052 = 1990052
+f A0053 = 1990053
+f A0054 = 1990054
+f A0055 = 1990055
+f A0056 = 1990056
+f A0057 = 1990057
+f A0058 = 1990058
+f A0059 = 1990059
+f A0060 = 1990060
+f A0061 = 1990061
+f A0062 = 1990062
+f A0063 = 1990063
+f A0064 = 1990064
+f A0065 = 1990065
+f A0066 = 1990066
+f A0067 = 1990067
+f A0068 = 1990068
+f A0069 = 1990069
+f A0070 = 1990070
+f A0071 = 1990071
+f A0072 = 1990072
+f A0073 = 1990073
+f A0074 = 1990074
+f A0075 = 1990075
+f A0076 = 1990076
+f A0077 = 1990077
+f A0078 = 1990078
+f A0079 = 1990079
+f A0080 = 1990080
+f A0081 = 1990081
+f A0082 = 1990082
+f A0083 = 1990083
+f A0084 = 1990084
+f A0085 = 1990085
+f A0086 = 1990086
+f A0087 = 1990087
+f A0088 = 1990088
+f A0089 = 1990089
+f A0090 = 1990090
+f A0091 = 1990091
+f A0092 = 1990092
+f A0093 = 1990093
+f A0094 = 1990094
+f A0095 = 1990095
+f A0096 = 1990096
+f A0097 = 1990097
+f A0098 = 1990098
+f A0099 = 1990099
+f A0100 = 1990100
+f A0101 = 1990101
+f A0102 = 1990102
+f A0103 = 1990103
+f A0104 = 1990104
+f A0105 = 1990105
+f A0106 = 1990106
+f A0107 = 1990107
+f A0108 = 1990108
+f A0109 = 1990109
+f A0110 = 1990110
+f A0111 = 1990111
+f A0112 = 1990112
+f A0113 = 1990113
+f A0114 = 1990114
+f A0115 = 1990115
+f A0116 = 1990116
+f A0117 = 1990117
+f A0118 = 1990118
+f A0119 = 1990119
+f A0120 = 1990120
+f A0121 = 1990121
+f A0122 = 1990122
+f A0123 = 1990123
+f A0124 = 1990124
+f A0125 = 1990125
+f A0126 = 1990126
+f A0127 = 1990127
+f A0128 = 1990128
+f A0129 = 1990129
+f A0130 = 1990130
+f A0131 = 1990131
+f A0132 = 1990132
+f A0133 = 1990133
+f A0134 = 1990134
+f A0135 = 1990135
+f A0136 = 1990136
+f A0137 = 1990137
+f A0138 = 1990138
+f A0139 = 1990139
+f A0140 = 1990140
+f A0141 = 1990141
+f A0142 = 1990142
+f A0143 = 1990143
+f A0144 = 1990144
+f A0145 = 1990145
+f A0146 = 1990146
+f A0147 = 1990147
+f A0148 = 1990148
+f A0149 = 1990149
+f A0150 = 1990150
+f A0151 = 1990151
+f A0152 = 1990152
+f A0153 = 1990153
+f A0154 = 1990154
+f A0155 = 1990155
+f A0156 = 1990156
+f A0157 = 1990157
+f A0158 = 1990158
+f A0159 = 1990159
+f A0160 = 1990160
+f A0161 = 1990161
+f A0162 = 1990162
+f A0163 = 1990163
+f A0164 = 1990164
+f A0165 = 1990165
+f A0166 = 1990166
+f A0167 = 1990167
+f A0168 = 1990168
+f A0169 = 1990169
+f A0170 = 1990170
+f A0171 = 1990171
+f A0172 = 1990172
+f A0173 = 1990173
+f A0174 = 1990174
+f A0175 = 1990175
+f A0176 = 1990176
+f A0177 = 1990177
+f A0178 = 1990178
+f A0179 = 1990179
+f A0180 = 1990180
+f A0181 = 1990181
+f A0182 = 1990182
+f A0183 = 1990183
+f A0184 = 1990184
+f A0185 = 1990185
+f A0186 = 1990186
+f A0187 = 1990187
+f A0188 = 1990188
+f A0189 = 1990189
+f A0190 = 1990190
+f A0191 = 1990191
+f A0192 = 1990192
+f A0193 = 1990193
+f A0194 = 1990194
+f A0195 = 1990195
+f A0196 = 1990196
+f A0197 = 1990197
+f A0198 = 1990198
+f A0199 = 1990199
+f A0200 = 1990200
+f A0201 = 1990201
+f A0202 = 1990202
+f A0203 = 1990203
+f A0204 = 1990204
+f A0205 = 1990205
+f A0206 = 1990206
+f A0207 = 1990207
+f A0208 = 1990208
+f A0209 = 1990209
+f A0210 = 1990210
+f A0211 = 1990211
+f A0212 = 1990212
+f A0213 = 1990213
+f A0214 = 1990214
+f A0215 = 1990215
+f A0216 = 1990216
+f A0217 = 1990217
+f A0218 = 1990218
+f A0219 = 1990219
+f A0220 = 1990220
+f A0221 = 1990221
+f A0222 = 1990222
+f A0223 = 1990223
+f A0224 = 1990224
+f A0225 = 1990225
+f A0226 = 1990226
+f A0227 = 1990227
+f A0228 = 1990228
+f A0229 = 1990229
+f A0230 = 1990230
+f A0231 = 1990231
+f A0232 = 1990232
+f A0233 = 1990233
+f A0234 = 1990234
+f A0235 = 1990235
+f A0236 = 1990236
+f A0237 = 1990237
+f A0238 = 1990238
+f A0239 = 1990239
+f A0240 = 1990240
+f A0241 = 1990241
+f A0242 = 1990242
+f A0243 = 1990243
+f A0244 = 1990244
+f A0245 = 1990245
+f A0246 = 1990246
+f A0247 = 1990247
+f A0248 = 1990248
+f A0249 = 1990249
+f A0250 = 1990250
+f A0251 = 1990251
+f A0252 = 1990252
+f A0253 = 1990253
+f A0254 = 1990254
+f A0255 = 1990255
+f A0256 = 1990256
+f A0257 = 1990257
+f A0258 = 1990258
+f A0259 = 1990259
+f A0260 = 1990260
+f A0261 = 1990261
+f A0262 = 1990262
+f A0263 = 1990263
+f A0264 = 1990264
+f A0265 = 1990265
+f A0266 = 1990266
+f A0267 = 1990267
+f A0268 = 1990268
+f A0269 = 1990269
+f A0270 = 1990270
+f A0271 = 1990271
+f A0272 = 1990272
+f A0273 = 1990273
+f A0274 = 1990274
+f A0275 = 1990275
+f A0276 = 1990276
+f A0277 = 1990277
+f A0278 = 1990278
+f A0279 = 1990279
+f A0280 = 1990280
+f A0281 = 1990281
+f A0282 = 1990282
+f A0283 = 1990283
+f A0284 = 1990284
+f A0285 = 1990285
+f A0286 = 1990286
+f A0287 = 1990287
+f A0288 = 1990288
+f A0289 = 1990289
+f A0290 = 1990290
+f A0291 = 1990291
+f A0292 = 1990292
+f A0293 = 1990293
+f A0294 = 1990294
+f A0295 = 1990295
+f A0296 = 1990296
+f A0297 = 1990297
+f A0298 = 1990298
+f A0299 = 1990299
+f A0300 = 1990300
+f A0301 = 1990301
+f A0302 = 1990302
+f A0303 = 1990303
+f A0304 = 1990304
+f A0305 = 1990305
+f A0306 = 1990306
+f A0307 = 1990307
+f A0308 = 1990308
+f A0309 = 1990309
+f A0310 = 1990310
+f A0311 = 1990311
+f A0312 = 1990312
+f A0313 = 1990313
+f A0314 = 1990314
+f A0315 = 1990315
+f A0316 = 1990316
+f A0317 = 1990317
+f A0318 = 1990318
+f A0319 = 1990319
+f A0320 = 1990320
+f A0321 = 1990321
+f A0322 = 1990322
+f A0323 = 1990323
+f A0324 = 1990324
+f A0325 = 1990325
+f A0326 = 1990326
+f A0327 = 1990327
+f A0328 = 1990328
+f A0329 = 1990329
+f A0330 = 1990330
+f A0331 = 1990331
+f A0332 = 1990332
+f A0333 = 1990333
+f A0334 = 1990334
+f A0335 = 1990335
+f A0336 = 1990336
+f A0337 = 1990337
+f A0338 = 1990338
+f A0339 = 1990339
+f A0340 = 1990340
+f A0341 = 1990341
+f A0342 = 1990342
+f A0343 = 1990343
+f A0344 = 1990344
+f A0345 = 1990345
+f A0346 = 1990346
+f A0347 = 1990347
+f A0348 = 1990348
+f A0349 = 1990349
+f A0350 = 1990350
+f A0351 = 1990351
+f A0352 = 1990352
+f A0353 = 1990353
+f A0354 = 1990354
+f A0355 = 1990355
+f A0356 = 1990356
+f A0357 = 1990357
+f A0358 = 1990358
+f A0359 = 1990359
+f A0360 = 1990360
+f A0361 = 1990361
+f A0362 = 1990362
+f A0363 = 1990363
+f A0364 = 1990364
+f A0365 = 1990365
+f A0366 = 1990366
+f A0367 = 1990367
+f A0368 = 1990368
+f A0369 = 1990369
+f A0370 = 1990370
+f A0371 = 1990371
+f A0372 = 1990372
+f A0373 = 1990373
+f A0374 = 1990374
+f A0375 = 1990375
+f A0376 = 1990376
+f A0377 = 1990377
+f A0378 = 1990378
+f A0379 = 1990379
+f A0380 = 1990380
+f A0381 = 1990381
+f A0382 = 1990382
+f A0383 = 1990383
+f A0384 = 1990384
+f A0385 = 1990385
+f A0386 = 1990386
+f A0387 = 1990387
+f A0388 = 1990388
+f A0389 = 1990389
+f A0390 = 1990390
+f A0391 = 1990391
+f A0392 = 1990392
+f A0393 = 1990393
+f A0394 = 1990394
+f A0395 = 1990395
+f A0396 = 1990396
+f A0397 = 1990397
+f A0398 = 1990398
+f A0399 = 1990399
+f A0400 = 1990400
+f A0401 = 1990401
+f A0402 = 1990402
+f A0403 = 1990403
+f A0404 = 1990404
+f A0405 = 1990405
+f A0406 = 1990406
+f A0407 = 1990407
+f A0408 = 1990408
+f A0409 = 1990409
+f A0410 = 1990410
+f A0411 = 1990411
+f A0412 = 1990412
+f A0413 = 1990413
+f A0414 = 1990414
+f A0415 = 1990415
+f A0416 = 1990416
+f A0417 = 1990417
+f A0418 = 1990418
+f A0419 = 1990419
+f A0420 = 1990420
+f A0421 = 1990421
+f A0422 = 1990422
+f A0423 = 1990423
+f A0424 = 1990424
+f A0425 = 1990425
+f A0426 = 1990426
+f A0427 = 1990427
+f A0428 = 1990428
+f A0429 = 1990429
+f A0430 = 1990430
+f A0431 = 1990431
+f A0432 = 1990432
+f A0433 = 1990433
+f A0434 = 1990434
+f A0435 = 1990435
+f A0436 = 1990436
+f A0437 = 1990437
+f A0438 = 1990438
+f A0439 = 1990439
+f A0440 = 1990440
+f A0441 = 1990441
+f A0442 = 1990442
+f A0443 = 1990443
+f A0444 = 1990444
+f A0445 = 1990445
+f A0446 = 1990446
+f A0447 = 1990447
+f A0448 = 1990448
+f A0449 = 1990449
+f A0450 = 1990450
+f A0451 = 1990451
+f A0452 = 1990452
+f A0453 = 1990453
+f A0454 = 1990454
+f A0455 = 1990455
+f A0456 = 1990456
+f A0457 = 1990457
+f A0458 = 1990458
+f A0459 = 1990459
+f A0460 = 1990460
+f A0461 = 1990461
+f A0462 = 1990462
+f A0463 = 1990463
+f A0464 = 1990464
+f A0465 = 1990465
+f A0466 = 1990466
+f A0467 = 1990467
+f A0468 = 1990468
+f A0469 = 1990469
+f A0470 = 1990470
+f A0471 = 1990471
+f A0472 = 1990472
+f A0473 = 1990473
+f A0474 = 1990474
+f A0475 = 1990475
+f A0476 = 1990476
+f A0477 = 1990477
+f A0478 = 1990478
+f A0479 = 1990479
+f A0480 = 1990480
+f A0481 = 1990481
+f A0482 = 1990482
+f A0483 = 1990483
+f A0484 = 1990484
+f A0485 = 1990485
+f A0486 = 1990486
+f A0487 = 1990487
+f A0488 = 1990488
+f A0489 = 1990489
+f A0490 = 1990490
+f A0491 = 1990491
+f A0492 = 1990492
+f A0493 = 1990493
+f A0494 = 1990494
+f A0495 = 1990495
+f A0496 = 1990496
+f A0497 = 1990497
+f A0498 = 1990498
+f A0499 = 1990499
+f A0500 = 1990500
+f A0501 = 1990501
+f A0502 = 1990502
+f A0503 = 1990503
+f A0504 = 1990504
+f A0505 = 1990505
+f A0506 = 1990506
+f A0507 = 1990507
+f A0508 = 1990508
+f A0509 = 1990509
+f A0510 = 1990510
+f A0511 = 1990511
+f A0512 = 1990512
+f A0513 = 1990513
+f A0514 = 1990514
+f A0515 = 1990515
+f A0516 = 1990516
+f A0517 = 1990517
+f A0518 = 1990518
+f A0519 = 1990519
+f A0520 = 1990520
+f A0521 = 1990521
+f A0522 = 1990522
+f A0523 = 1990523
+f A0524 = 1990524
+f A0525 = 1990525
+f A0526 = 1990526
+f A0527 = 1990527
+f A0528 = 1990528
+f A0529 = 1990529
+f A0530 = 1990530
+f A0531 = 1990531
+f A0532 = 1990532
+f A0533 = 1990533
+f A0534 = 1990534
+f A0535 = 1990535
+f A0536 = 1990536
+f A0537 = 1990537
+f A0538 = 1990538
+f A0539 = 1990539
+f A0540 = 1990540
+f A0541 = 1990541
+f A0542 = 1990542
+f A0543 = 1990543
+f A0544 = 1990544
+f A0545 = 1990545
+f A0546 = 1990546
+f A0547 = 1990547
+f A0548 = 1990548
+f A0549 = 1990549
+f A0550 = 1990550
+f A0551 = 1990551
+f A0552 = 1990552
+f A0553 = 1990553
+f A0554 = 1990554
+f A0555 = 1990555
+f A0556 = 1990556
+f A0557 = 1990557
+f A0558 = 1990558
+f A0559 = 1990559
+f A0560 = 1990560
+f A0561 = 1990561
+f A0562 = 1990562
+f A0563 = 1990563
+f A0564 = 1990564
+f A0565 = 1990565
+f A0566 = 1990566
+f A0567 = 1990567
+f A0568 = 1990568
+f A0569 = 1990569
+f A0570 = 1990570
+f A0571 = 1990571
+f A0572 = 1990572
+f A0573 = 1990573
+f A0574 = 1990574
+f A0575 = 1990575
+f A0576 = 1990576
+f A0577 = 1990577
+f A0578 = 1990578
+f A0579 = 1990579
+f A0580 = 1990580
+f A0581 = 1990581
+f A0582 = 1990582
+f A0583 = 1990583
+f A0584 = 1990584
+f A0585 = 1990585
+f A0586 = 1990586
+f A0587 = 1990587
+f A0588 = 1990588
+f A0589 = 1990589
+f A0590 = 1990590
+f A0591 = 1990591
+f A0592 = 1990592
+f A0593 = 1990593
+f A0594 = 1990594
+f A0595 = 1990595
+f A0596 = 1990596
+f A0597 = 1990597
+f A0598 = 1990598
+f A0599 = 1990599
+f A0600 = 1990600
+f A0601 = 1990601
+f A0602 = 1990602
+f A0603 = 1990603
+f A0604 = 1990604
+f A0605 = 1990605
+f A0606 = 1990606
+f A0607 = 1990607
+f A0608 = 1990608
+f A0609 = 1990609
+f A0610 = 1990610
+f A0611 = 1990611
+f A0612 = 1990612
+f A0613 = 1990613
+f A0614 = 1990614
+f A0615 = 1990615
+f A0616 = 1990616
+f A0617 = 1990617
+f A0618 = 1990618
+f A0619 = 1990619
+f A0620 = 1990620
+f A0621 = 1990621
+f A0622 = 1990622
+f A0623 = 1990623
+f A0624 = 1990624
+f A0625 = 1990625
+f A0626 = 1990626
+f A0627 = 1990627
+f A0628 = 1990628
+f A0629 = 1990629
+f A0630 = 1990630
+f A0631 = 1990631
+f A0632 = 1990632
+f A0633 = 1990633
+f A0634 = 1990634
+f A0635 = 1990635
+f A0636 = 1990636
+f A0637 = 1990637
+f A0638 = 1990638
+f A0639 = 1990639
+f A0640 = 1990640
+f A0641 = 1990641
+f A0642 = 1990642
+f A0643 = 1990643
+f A0644 = 1990644
+f A0645 = 1990645
+f A0646 = 1990646
+f A0647 = 1990647
+f A0648 = 1990648
+f A0649 = 1990649
+f A0650 = 1990650
+f A0651 = 1990651
+f A0652 = 1990652
+f A0653 = 1990653
+f A0654 = 1990654
+f A0655 = 1990655
+f A0656 = 1990656
+f A0657 = 1990657
+f A0658 = 1990658
+f A0659 = 1990659
+f A0660 = 1990660
+f A0661 = 1990661
+f A0662 = 1990662
+f A0663 = 1990663
+f A0664 = 1990664
+f A0665 = 1990665
+f A0666 = 1990666
+f A0667 = 1990667
+f A0668 = 1990668
+f A0669 = 1990669
+f A0670 = 1990670
+f A0671 = 1990671
+f A0672 = 1990672
+f A0673 = 1990673
+f A0674 = 1990674
+f A0675 = 1990675
+f A0676 = 1990676
+f A0677 = 1990677
+f A0678 = 1990678
+f A0679 = 1990679
+f A0680 = 1990680
+f A0681 = 1990681
+f A0682 = 1990682
+f A0683 = 1990683
+f A0684 = 1990684
+f A0685 = 1990685
+f A0686 = 1990686
+f A0687 = 1990687
+f A0688 = 1990688
+f A0689 = 1990689
+f A0690 = 1990690
+f A0691 = 1990691
+f A0692 = 1990692
+f A0693 = 1990693
+f A0694 = 1990694
+f A0695 = 1990695
+f A0696 = 1990696
+f A0697 = 1990697
+f A0698 = 1990698
+f A0699 = 1990699
+f A0700 = 1990700
+f A0701 = 1990701
+f A0702 = 1990702
+f A0703 = 1990703
+f A0704 = 1990704
+f A0705 = 1990705
+f A0706 = 1990706
+f A0707 = 1990707
+f A0708 = 1990708
+f A0709 = 1990709
+f A0710 = 1990710
+f A0711 = 1990711
+f A0712 = 1990712
+f A0713 = 1990713
+f A0714 = 1990714
+f A0715 = 1990715
+f A0716 = 1990716
+f A0717 = 1990717
+f A0718 = 1990718
+f A0719 = 1990719
+f A0720 = 1990720
+f A0721 = 1990721
+f A0722 = 1990722
+f A0723 = 1990723
+f A0724 = 1990724
+f A0725 = 1990725
+f A0726 = 1990726
+f A0727 = 1990727
+f A0728 = 1990728
+f A0729 = 1990729
+f A0730 = 1990730
+f A0731 = 1990731
+f A0732 = 1990732
+f A0733 = 1990733
+f A0734 = 1990734
+f A0735 = 1990735
+f A0736 = 1990736
+f A0737 = 1990737
+f A0738 = 1990738
+f A0739 = 1990739
+f A0740 = 1990740
+f A0741 = 1990741
+f A0742 = 1990742
+f A0743 = 1990743
+f A0744 = 1990744
+f A0745 = 1990745
+f A0746 = 1990746
+f A0747 = 1990747
+f A0748 = 1990748
+f A0749 = 1990749
+f A0750 = 1990750
+f A0751 = 1990751
+f A0752 = 1990752
+f A0753 = 1990753
+f A0754 = 1990754
+f A0755 = 1990755
+f A0756 = 1990756
+f A0757 = 1990757
+f A0758 = 1990758
+f A0759 = 1990759
+f A0760 = 1990760
+f A0761 = 1990761
+f A0762 = 1990762
+f A0763 = 1990763
+f A0764 = 1990764
+f A0765 = 1990765
+f A0766 = 1990766
+f A0767 = 1990767
+f A0768 = 1990768
+f A0769 = 1990769
+f A0770 = 1990770
+f A0771 = 1990771
+f A0772 = 1990772
+f A0773 = 1990773
+f A0774 = 1990774
+f A0775 = 1990775
+f A0776 = 1990776
+f A0777 = 1990777
+f A0778 = 1990778
+f A0779 = 1990779
+f A0780 = 1990780
+f A0781 = 1990781
+f A0782 = 1990782
+f A0783 = 1990783
+f A0784 = 1990784
+f A0785 = 1990785
+f A0786 = 1990786
+f A0787 = 1990787
+f A0788 = 1990788
+f A0789 = 1990789
+f A0790 = 1990790
+f A0791 = 1990791
+f A0792 = 1990792
+f A0793 = 1990793
+f A0794 = 1990794
+f A0795 = 1990795
+f A0796 = 1990796
+f A0797 = 1990797
+f A0798 = 1990798
+f A0799 = 1990799
+f A0800 = 1990800
+f A0801 = 1990801
+f A0802 = 1990802
+f A0803 = 1990803
+f A0804 = 1990804
+f A0805 = 1990805
+f A0806 = 1990806
+f A0807 = 1990807
+f A0808 = 1990808
+f A0809 = 1990809
+f A0810 = 1990810
+f A0811 = 1990811
+f A0812 = 1990812
+f A0813 = 1990813
+f A0814 = 1990814
+f A0815 = 1990815
+f A0816 = 1990816
+f A0817 = 1990817
+f A0818 = 1990818
+f A0819 = 1990819
+f A0820 = 1990820
+f A0821 = 1990821
+f A0822 = 1990822
+f A0823 = 1990823
+f A0824 = 1990824
+f A0825 = 1990825
+f A0826 = 1990826
+f A0827 = 1990827
+f A0828 = 1990828
+f A0829 = 1990829
+f A0830 = 1990830
+f A0831 = 1990831
+f A0832 = 1990832
+f A0833 = 1990833
+f A0834 = 1990834
+f A0835 = 1990835
+f A0836 = 1990836
+f A0837 = 1990837
+f A0838 = 1990838
+f A0839 = 1990839
+f A0840 = 1990840
+f A0841 = 1990841
+f A0842 = 1990842
+f A0843 = 1990843
+f A0844 = 1990844
+f A0845 = 1990845
+f A0846 = 1990846
+f A0847 = 1990847
+f A0848 = 1990848
+f A0849 = 1990849
+f A0850 = 1990850
+f A0851 = 1990851
+f A0852 = 1990852
+f A0853 = 1990853
+f A0854 = 1990854
+f A0855 = 1990855
+f A0856 = 1990856
+f A0857 = 1990857
+f A0858 = 1990858
+f A0859 = 1990859
+f A0860 = 1990860
+f A0861 = 1990861
+f A0862 = 1990862
+f A0863 = 1990863
+f A0864 = 1990864
+f A0865 = 1990865
+f A0866 = 1990866
+f A0867 = 1990867
+f A0868 = 1990868
+f A0869 = 1990869
+f A0870 = 1990870
+f A0871 = 1990871
+f A0872 = 1990872
+f A0873 = 1990873
+f A0874 = 1990874
+f A0875 = 1990875
+f A0876 = 1990876
+f A0877 = 1990877
+f A0878 = 1990878
+f A0879 = 1990879
+f A0880 = 1990880
+f A0881 = 1990881
+f A0882 = 1990882
+f A0883 = 1990883
+f A0884 = 1990884
+f A0885 = 1990885
+f A0886 = 1990886
+f A0887 = 1990887
+f A0888 = 1990888
+f A0889 = 1990889
+f A0890 = 1990890
+f A0891 = 1990891
+f A0892 = 1990892
+f A0893 = 1990893
+f A0894 = 1990894
+f A0895 = 1990895
+f A0896 = 1990896
+f A0897 = 1990897
+f A0898 = 1990898
+f A0899 = 1990899
+f A0900 = 1990900
+f A0901 = 1990901
+f A0902 = 1990902
+f A0903 = 1990903
+f A0904 = 1990904
+f A0905 = 1990905
+f A0906 = 1990906
+f A0907 = 1990907
+f A0908 = 1990908
+f A0909 = 1990909
+f A0910 = 1990910
+f A0911 = 1990911
+f A0912 = 1990912
+f A0913 = 1990913
+f A0914 = 1990914
+f A0915 = 1990915
+f A0916 = 1990916
+f A0917 = 1990917
+f A0918 = 1990918
+f A0919 = 1990919
+f A0920 = 1990920
+f A0921 = 1990921
+f A0922 = 1990922
+f A0923 = 1990923
+f A0924 = 1990924
+f A0925 = 1990925
+f A0926 = 1990926
+f A0927 = 1990927
+f A0928 = 1990928
+f A0929 = 1990929
+f A0930 = 1990930
+f A0931 = 1990931
+f A0932 = 1990932
+f A0933 = 1990933
+f A0934 = 1990934
+f A0935 = 1990935
+f A0936 = 1990936
+f A0937 = 1990937
+f A0938 = 1990938
+f A0939 = 1990939
+f A0940 = 1990940
+f A0941 = 1990941
+f A0942 = 1990942
+f A0943 = 1990943
+f A0944 = 1990944
+f A0945 = 1990945
+f A0946 = 1990946
+f A0947 = 1990947
+f A0948 = 1990948
+f A0949 = 1990949
+f A0950 = 1990950
+f A0951 = 1990951
+f A0952 = 1990952
+f A0953 = 1990953
+f A0954 = 1990954
+f A0955 = 1990955
+f A0956 = 1990956
+f A0957 = 1990957
+f A0958 = 1990958
+f A0959 = 1990959
+f A0960 = 1990960
+f A0961 = 1990961
+f A0962 = 1990962
+f A0963 = 1990963
+f A0964 = 1990964
+f A0965 = 1990965
+f A0966 = 1990966
+f A0967 = 1990967
+f A0968 = 1990968
+f A0969 = 1990969
+f A0970 = 1990970
+f A0971 = 1990971
+f A0972 = 1990972
+f A0973 = 1990973
+f A0974 = 1990974
+f A0975 = 1990975
+f A0976 = 1990976
+f A0977 = 1990977
+f A0978 = 1990978
+f A0979 = 1990979
+f A0980 = 1990980
+f A0981 = 1990981
+f A0982 = 1990982
+f A0983 = 1990983
+f A0984 = 1990984
+f A0985 = 1990985
+f A0986 = 1990986
+f A0987 = 1990987
+f A0988 = 1990988
+f A0989 = 1990989
+f A0990 = 1990990
+f A0991 = 1990991
+f A0992 = 1990992
+f A0993 = 1990993
+f A0994 = 1990994
+f A0995 = 1990995
+f A0996 = 1990996
+f A0997 = 1990997
+f A0998 = 1990998
+f A0999 = 1990999
+f A1000 = 1991000
=====================================
testsuite/tests/pmcheck/complete_sigs/T13363a.hs
=====================================
@@ -0,0 +1,15 @@
+{-# LANGUAGE PatternSynonyms #-}
+
+module Lib where
+
+data Boolean = F | T
+ deriving Eq
+
+pattern TooGoodToBeTrue :: Boolean
+pattern TooGoodToBeTrue = T
+{-# COMPLETE F, TooGoodToBeTrue #-}
+
+catchAll :: Boolean -> Int
+catchAll F = 0
+catchAll TooGoodToBeTrue = 1
+catchAll _ = error "impossible"
=====================================
testsuite/tests/pmcheck/complete_sigs/T13363a.stderr
=====================================
@@ -0,0 +1,7 @@
+
+testsuite/tests/pmcheck/complete_sigs/T13363a.hs:15:1: warning: [-Woverlapping-patterns]
+ Pattern match is redundant
+ In an equation for `catchAll': catchAll _ = ...
+ |
+14 | catchAll _ = error "impossible"
+ | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
=====================================
testsuite/tests/pmcheck/complete_sigs/T13363b.hs
=====================================
@@ -0,0 +1,16 @@
+{-# LANGUAGE PatternSynonyms #-}
+
+module Lib where
+
+data T = A | B | C
+ deriving Eq
+
+pattern BC :: T
+pattern BC = C
+
+{-# COMPLETE A, BC #-}
+
+f A = 1
+f B = 2
+f BC = 3
+f _ = error "impossible"
=====================================
testsuite/tests/pmcheck/complete_sigs/T13363b.stderr
=====================================
@@ -0,0 +1,7 @@
+
+testsuite/tests/pmcheck/complete_sigs/T13363b.hs:16:1: warning: [-Woverlapping-patterns]
+ Pattern match is redundant
+ In an equation for `f': f _ = ...
+ |
+16 | f _ = error "impossible"
+ | ^^^^^^^^^^^^^^^^^^^^^^^^^
=====================================
testsuite/tests/pmcheck/complete_sigs/all.T
=====================================
@@ -14,4 +14,6 @@ test('completesig13', normal, compile, [''])
test('completesig14', normal, compile, [''])
test('completesig15', normal, compile_fail, [''])
test('T14059a', normal, compile, [''])
-test('T14253', expect_broken(14253), compile, [''])
+test('T14253', normal, compile, [''])
+test('T13363a', normal, compile, ['-Wall'])
+test('T13363b', normal, compile, ['-Wall'])
=====================================
testsuite/tests/pmcheck/should_compile/all.T
=====================================
@@ -92,6 +92,12 @@ test('pmc006', [], compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('pmc007', [], compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('pmc008', [], compile,
+ ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('pmc009', [], compile,
+ ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('pmc010', [], compile,
+ ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T11245', [], compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T12949', [], compile, ['-fwarn-overlapping-patterns'])
=====================================
testsuite/tests/pmcheck/should_compile/pmc008.hs
=====================================
@@ -0,0 +1,9 @@
+{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-overlapping-patterns #-}
+
+module PMC008 where
+
+-- complete match, but because of the guard, the information that `x` is not
+-- `Just` has to flow through the term oracle.
+foo :: Maybe Int -> Int
+foo x | Just y <- x = y
+foo Nothing = 43
=====================================
testsuite/tests/pmcheck/should_compile/pmc009.hs
=====================================
@@ -0,0 +1,7 @@
+module Lib where
+
+data D = A | B
+
+f :: D -> D -> D
+f A A = A
+f B B = B
=====================================
testsuite/tests/pmcheck/should_compile/pmc010.hs
=====================================
@@ -0,0 +1,9 @@
+module Lib where
+
+data D = A | B | C | D
+
+f :: D -> D -> D
+f A A = A
+f B B = B
+f C C = C
+f D D = D
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/commit/236c0cfb3ab952dc6af6a71f8fce5bd8f2030d4b
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/commit/236c0cfb3ab952dc6af6a71f8fce5bd8f2030d4b
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20190606/226bdac4/attachment-0001.html>
More information about the ghc-commits
mailing list