diff options
| -rw-r--r-- | compiler/deSugar/Check.hs | 11 | ||||
| -rw-r--r-- | compiler/deSugar/DsMonad.hs | 2 | ||||
| -rw-r--r-- | compiler/deSugar/PmOracle.hs | 190 | ||||
| -rw-r--r-- | compiler/deSugar/PmPpr.hs | 36 | ||||
| -rw-r--r-- | compiler/deSugar/PmTypes.hs (renamed from compiler/deSugar/PmExpr.hs) | 287 | ||||
| -rw-r--r-- | compiler/deSugar/PmTypes.hs-boot (renamed from compiler/deSugar/PmOracle.hs-boot) | 2 | ||||
| -rw-r--r-- | compiler/ghc.cabal.in | 4 | ||||
| -rw-r--r-- | compiler/typecheck/TcRnTypes.hs | 2 |
8 files changed, 264 insertions, 270 deletions
diff --git a/compiler/deSugar/Check.hs b/compiler/deSugar/Check.hs index 3a1515d0cc..1c9493bbca 100644 --- a/compiler/deSugar/Check.hs +++ b/compiler/deSugar/Check.hs @@ -26,7 +26,7 @@ module Check ( import GhcPrelude -import PmExpr +import PmTypes import PmOracle import PmPpr import BasicTypes (Origin, isGenerated) @@ -817,7 +817,7 @@ below is the *right thing to do*: The case with literals is a bit different. a literal @l@ should be translated to @x (True <- x == from l)@. Since we want to have better warnings for overloaded literals as it is a very common feature, we treat them differently. -They are mainly covered in Note [Undecidable Equality for PmAltCons] in PmExpr. +They are mainly covered in Note [Undecidable Equality for PmAltCons] in PmTypes. 4. N+K Patterns & Pattern Synonyms ---------------------------------- @@ -949,7 +949,7 @@ additional features added to the coverage checker which are not described in the paper. This Note serves as a reference for these new features. * Value abstractions are severely simplified to the point where they are just - variables. The information about the PmExpr shape of a variable is encoded in + variables. The information about the shape of a variable is encoded in the oracle state 'Delta' instead. * Handling of uninhabited fields like `!Void`. See Note [Strict argument type constraints] in PmOracle. @@ -1397,9 +1397,6 @@ addPatTmCs ps xs k = do pv <- concat <$> translatePatVec fam_insts ps locallyExtendPmDelta (\delta -> addVarPatVecCt delta xs pv) k --- ---------------------------------------------------------------------------- --- * Converting between Value Abstractions, Patterns and PmExpr - -- | Add a constraint equating a variable to a 'PatVec'. Picks out the single -- 'PmPat' of arity 1 and equates x to it. Returns the original Delta if that -- fails. Otherwise it returns Nothing when the resulting Delta would be @@ -1422,7 +1419,7 @@ addVarPatVecCt delta (x:xs) (pat:pv) addVarPatVecCt delta [] pv = ASSERT( patVecArity pv == 0 ) pure (Just delta) addVarPatVecCt _ (_:_) [] = panic "More match vars than patterns" --- | Convert a pattern to a 'PmExpr' (will be either 'Nothing' if the pattern is +-- | Convert a pattern to a 'PmTypes' (will be either 'Nothing' if the pattern is -- a guard pattern, or 'Just' an expression in all other cases) by dropping the -- guards addVarPatCt :: Delta -> Id -> PmPat -> DsM (Maybe Delta) diff --git a/compiler/deSugar/DsMonad.hs b/compiler/deSugar/DsMonad.hs index d937b3b134..1bfa25324a 100644 --- a/compiler/deSugar/DsMonad.hs +++ b/compiler/deSugar/DsMonad.hs @@ -70,7 +70,7 @@ import BasicTypes ( Origin ) import DataCon import ConLike import TyCon -import {-# SOURCE #-} PmOracle +import PmTypes import Id import Module import Outputable diff --git a/compiler/deSugar/PmOracle.hs b/compiler/deSugar/PmOracle.hs index 93c4d1d959..f9abae481c 100644 --- a/compiler/deSugar/PmOracle.hs +++ b/compiler/deSugar/PmOracle.hs @@ -31,7 +31,7 @@ module PmOracle ( import GhcPrelude -import PmExpr +import PmTypes import DynFlags import Outputable @@ -77,7 +77,6 @@ import Control.Monad.Trans.State.Strict import Data.Bifunctor (second) import Data.Foldable (foldlM) import Data.List (find) -import Data.List.NonEmpty (NonEmpty (..)) import qualified Data.List.NonEmpty as NonEmpty import qualified Data.Semigroup as Semigroup @@ -100,22 +99,6 @@ mkPmId ty = getUniqueM >>= \unique -> ----------------------------------------------- -- * Caching possible matches of a COMPLETE set -type ConLikeSet = UniqDSet ConLike - --- | A data type caching the results of 'completeMatchConLikes' with support for --- deletion of contructors that were already matched on. -data PossibleMatches - = PM TyCon (NonEmpty ConLikeSet) - -- ^ Each ConLikeSet is a (subset of) the constructors in a COMPLETE pragma - -- 'NonEmpty' because the empty case would mean that the type has no COMPLETE - -- set at all, for which we have 'NoPM' - | NoPM - -- ^ No COMPLETE set for this type (yet). Think of overloaded literals. - -instance Outputable PossibleMatches where - ppr (PM _tc cs) = ppr (NonEmpty.toList cs) - ppr NoPM = text "<NoPM>" - initIM :: Type -> DsM (Maybe PossibleMatches) initIM ty = case splitTyConApp_maybe ty of Nothing -> pure Nothing @@ -235,26 +218,6 @@ equateTyVars ex_tvs1 ex_tvs2 -- * Pattern match oracle --- | Term and type constraints to accompany each value vector abstraction. --- For efficiency, we store the term oracle state instead of the term --- constraints. -data Delta = MkDelta { delta_ty_cs :: Bag EvVar -- Type oracle; things like a~Int - , delta_tm_cs :: TmState } -- Term oracle; things like x~Nothing - --- | An initial delta that is always satisfiable -initDelta :: Delta -initDelta = MkDelta emptyBag initTmState - -instance Outputable Delta where - ppr delta = vcat [ - -- intentionally formatted this way enable the dev to comment in only - -- the info she needs - ppr (delta_tm_cs delta), - ppr (pprEvVarWithType <$> delta_ty_cs delta) - --ppr (delta_ty_cs delta) - ] - - {- Note [Recovering from unsatisfiable pattern-matching constraints] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider the following code (see #12957 and #15450): @@ -603,68 +566,10 @@ tyIsSatisfiable recheck_complete_sets new_ty_cs = SC $ \delta -> do {- ********************************************************************* * * - SharedIdEnv DIdEnv with sharing * * ********************************************************************* -} --- | Either @Indirect x@, meaning the value is represented by that of @x@, or --- an @Entry@ containing containing the actual value it represents. -data Shared a - = Indirect Id - | Entry a - --- | A 'DIdEnv' in which entries can be shared by multiple 'Id's. --- Merge equivalence classes of two Ids by 'setIndirectSDIE' and set the entry --- of an Id with 'setEntrySDIE'. -newtype SharedDIdEnv a - = SDIE { unSDIE :: DIdEnv (Shared a) } - -emptySDIE :: SharedDIdEnv a -emptySDIE = SDIE emptyDVarEnv - -lookupReprAndEntrySDIE :: SharedDIdEnv a -> Id -> (Id, Maybe a) -lookupReprAndEntrySDIE sdie@(SDIE env) x = case lookupDVarEnv env x of - Nothing -> (x, Nothing) - Just (Indirect y) -> lookupReprAndEntrySDIE sdie y - Just (Entry a) -> (x, Just a) - --- | @lookupSDIE env x@ looks up an entry for @x@, looking through all --- 'Indirect's until it finds a shared 'Entry'. -lookupSDIE :: SharedDIdEnv a -> Id -> Maybe a -lookupSDIE sdie x = snd (lookupReprAndEntrySDIE sdie x) - --- | Check if two variables are part of the same equivalence class. -sameRepresentative :: SharedDIdEnv a -> Id -> Id -> Bool -sameRepresentative sdie x y = - fst (lookupReprAndEntrySDIE sdie x) == fst (lookupReprAndEntrySDIE sdie y) - --- | @setIndirectSDIE env x y@ sets @x@'s 'Entry' to @Indirect y@, thereby --- merging @x@'s equivalence class into @y@'s. This will discard all info on --- @x@! -setIndirectSDIE :: SharedDIdEnv a -> Id -> Id -> SharedDIdEnv a -setIndirectSDIE sdie@(SDIE env) x y = - SDIE $ extendDVarEnv env (fst (lookupReprAndEntrySDIE sdie x)) (Indirect y) - --- | @setEntrySDIE env x a@ sets the 'Entry' @x@ is associated with to @a@, --- thereby modifying its whole equivalence class. -setEntrySDIE :: SharedDIdEnv a -> Id -> a -> SharedDIdEnv a -setEntrySDIE sdie@(SDIE env) x a = - SDIE $ extendDVarEnv env (fst (lookupReprAndEntrySDIE sdie x)) (Entry a) - -traverseSharedIdEnv :: Applicative f => (a -> f b) -> SharedDIdEnv a -> f (SharedDIdEnv b) -traverseSharedIdEnv f = fmap (SDIE . listToUDFM) . traverse g . udfmToList . unSDIE - where - g (u, Indirect y) = pure (u,Indirect y) - g (u, Entry a) = (u,) . Entry <$> f a - -instance Outputable a => Outputable (Shared a) where - ppr (Indirect x) = ppr x - ppr (Entry a) = ppr a - -instance Outputable a => Outputable (SharedDIdEnv a) where - ppr (SDIE env) = ppr env - {- ********************************************************************* * * @@ -673,66 +578,6 @@ instance Outputable a => Outputable (SharedDIdEnv a) where * * ********************************************************************* -} --- | The term oracle state. Stores 'VarInfo' for encountered 'Id's. These --- entries are possibly shared when we figure out that two variables must be --- equal, thus represent the same set of values. --- --- See Note [TmState invariants]. -newtype TmState = TS (SharedDIdEnv VarInfo) - -- Deterministic so that we generate deterministic error messages - --- | Information about an 'Id'. Stores positive ('vi_pos') facts, like @x ~ Just 42@, --- and negative ('vi_neg') facts, like "x is not (:)". --- Also caches the type ('vi_ty'), the 'PossibleMatches' of a COMPLETE set --- ('vi_cache') and the number of times each variable was refined --- ('vi_n_refines'). --- --- Subject to Note [The Pos/Neg invariant]. -data VarInfo - = VI - { vi_ty :: !Type - -- ^ The type of the variable. Important for rejecting possible GADT - -- constructors or incompatible pattern synonyms (@Just42 :: Maybe Int@). - - , vi_pos :: [(PmAltCon, [Id])] - -- ^ Positive info: 'PmExprCon's it is (i.e. @x ~ [Just y, PatSyn z]@), all - -- at the same time (i.e. conjunctive). We need a list because of nested - -- pattern matches involving pattern synonym - -- case x of { Just y -> case x of PatSyn z -> ... } - -- However, no more than one RealDataCon in the list, otherwise contradiction - -- because of generativity. - - , vi_neg :: ![PmAltCon] - -- ^ Negative info: A list of 'PmAltCon's that it 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@. Is orthogonal to anything from 'vi_pos', - -- in the sense that 'eqPmAltCon' returns @PossiblyOverlap@ for any pairing - -- between 'vi_pos' and 'vi_neg'. - - -- See Note [Why record both positive and negative info?] - - , vi_cache :: !PossibleMatches - -- ^ A cache of the associated COMPLETE sets. At any time a superset of - -- possible constructors of each COMPLETE set. So, if it's not in here, we - -- can't possibly match on it. Complementary to 'vi_neg'. We still need it - -- to recognise completion of a COMPLETE set efficiently for large enums. - - , vi_n_refines :: !Int - -- ^ Purely for Check performance reasons. The number of times this - -- representative was refined ('refineToAltCon') in the Check's ConVar split. - -- Sadly, we can't store this info in the Check module, as it's tightly coupled - -- to the particular 'Delta' and also is per *representative*, not per - -- syntactic variable. Note that this number does not always correspond to the - -- length of solutions: 'addVarConCt' might add a solution without - -- incurring the potential exponential blowup by ConVar. - } - {- Note [The Pos/Neg invariant] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Invariant applying to each VarInfo: Whenever we have @(C, [y,z])@ in 'vi_pos', @@ -830,19 +675,6 @@ The "list" option is far simpler, but incurs some overhead in representation and warning messages (which can be alleviated by someone with enough dedication). -} --- | Not user-facing. -instance Outputable TmState where - ppr (TS state) = ppr state - --- | Not user-facing. -instance Outputable VarInfo where - ppr (VI ty pos neg cache n) - = braces (hcat (punctuate comma [ppr ty, ppr pos, ppr neg, ppr cache, ppr n])) - --- | Initial state of the oracle. -initTmState :: TmState -initTmState = TS emptySDIE - -- | A 'SatisfiabilityCheck' based on new term-level constraints. -- Returns a new 'Delta' if the new constraints are compatible with existing -- ones. @@ -1098,15 +930,15 @@ ensureInhabited delta vi = fmap (set_cache vi) <$> test (vi_cache vi) -- This wo -- impossible matches. ensureAllPossibleMatchesInhabited :: Delta -> DsM (Maybe Delta) ensureAllPossibleMatchesInhabited delta@MkDelta{ delta_tm_cs = TS env } - = runMaybeT (set_tm_cs_env delta <$> traverseSharedIdEnv go env) + = runMaybeT (set_tm_cs_env delta <$> traverseSDIE go env) where set_tm_cs_env delta env = delta{ delta_tm_cs = TS env } go vi = MaybeT (ensureInhabited delta vi) -- | @refineToAltCon delta x con arg_tys ex_tyvars@ instantiates @con@ at -- @arg_tys@ with fresh variables (equating existentials to @ex_tyvars@). --- It adds a new term equality equating @x@ is to the resulting 'PmExprCon' and --- new type equalities arising from GADT matches. +-- It adds a new term equality equating @x@ is to the resulting 'PmAltCon' app +-- and new type equalities arising from GADT matches. -- If successful, returns the new @delta@ and the fresh term variables, or -- @Nothing@ otherwise. refineToAltCon :: Delta -> Id -> PmAltCon -> [Type] -> [TyVar] -> DsM (Maybe (Delta, [Id])) @@ -1286,19 +1118,19 @@ addVarVarCt delta@MkDelta{ delta_tm_cs = TS env } (x, y) -- class, otherwise we might get cyclic substitutions. -- Cf. 'extendSubstAndSolve' and -- @testsuite/tests/pmcheck/should_compile/CyclicSubst.hs@. - | sameRepresentative env x y = pure delta - | otherwise = equate delta x y + | sameRepresentativeSDIE env x y = pure delta + | otherwise = equate delta x y -- | @equate ts@(TS env) x y@ merges the equivalence classes of @x@ and @y@ by -- adding an indirection to the environment. -- Makes sure that the positive and negative facts of @x@ and @y@ are -- compatible. --- Preconditions: @not (sameRepresentative env x y)@ +-- Preconditions: @not (sameRepresentativeSDIE env x y)@ -- -- See Note [TmState invariants]. equate :: Delta -> Id -> Id -> MaybeT DsM Delta equate delta@MkDelta{ delta_tm_cs = TS env } x y - = ASSERT( not (sameRepresentative env x y) ) + = ASSERT( not (sameRepresentativeSDIE env x y) ) case (lookupSDIE env x, lookupSDIE env y) of (Nothing, _) -> pure (delta{ delta_tm_cs = TS (setIndirectSDIE env x y) }) (_, Nothing) -> pure (delta{ delta_tm_cs = TS (setIndirectSDIE env y x) }) @@ -1323,9 +1155,9 @@ equate delta@MkDelta{ delta_tm_cs = TS env } x y -- go! pure delta_neg --- | @addVarConCt x alt args ts@ extends the substitution with a mapping @x: -> --- PmExprCon alt args@ if compatible with refutable shapes of @x@ and its --- solution, reject (@Nothing@) otherwise. +-- | @addVarConCt x alt args ts@ extends the substitution with a solution +-- @x :-> (alt, args)@ if compatible with refutable shapes of @x@ and its +-- other solutions, reject (@Nothing@) otherwise. -- -- See Note [TmState invariants]. addVarConCt :: Delta -> Id -> PmAltCon -> [Id] -> MaybeT DsM Delta diff --git a/compiler/deSugar/PmPpr.hs b/compiler/deSugar/PmPpr.hs index bee38ed46b..82e6d0f0a0 100644 --- a/compiler/deSugar/PmPpr.hs +++ b/compiler/deSugar/PmPpr.hs @@ -1,6 +1,6 @@ {-# LANGUAGE CPP, ViewPatterns #-} --- | Provides factilities for pretty-printing 'PmExpr's in a way approriate for +-- | Provides factilities for pretty-printing 'Delta's in a way appropriate for -- user facing pattern match warnings. module PmPpr ( pprUncovered @@ -22,7 +22,7 @@ import Util import Maybes import Data.List.NonEmpty (NonEmpty, nonEmpty, toList) -import PmExpr +import PmTypes import PmOracle -- | Pretty-print the guts of an uncovered value vector abstraction, i.e., its @@ -44,7 +44,7 @@ pprUncovered delta vas | otherwise = hang (fsep vec) 4 $ text "where" <+> vcat (map (pprRefutableShapes . snd) (udfmToList refuts)) where - ppr_action = mapM (pprPmExprVar 2) vas + ppr_action = mapM (pprPmVar 2) vas (vec, renamings) = runPmPpr delta ppr_action refuts = prettifyRefuts delta renamings @@ -128,16 +128,16 @@ checkRefuts x = do -- | Pretty print a variable, but remember to prettify the names of the variables -- that refer to neg-literals. The ones that cannot be shown are printed as -- underscores. -pprPmExprVar :: Int -> Id -> PmPprM SDoc -pprPmExprVar prec x = do +pprPmVar :: Int -> Id -> PmPprM SDoc +pprPmVar prec x = do delta <- ask case lookupSolution delta x of - Just (alt, args) -> pprPmExprCon prec alt args + Just (alt, args) -> pprPmAltCon prec alt args Nothing -> fromMaybe underscore <$> checkRefuts x -pprPmExprCon :: Int -> PmAltCon -> [Id] -> PmPprM SDoc -pprPmExprCon _prec (PmAltLit l) _ = pure (ppr l) -pprPmExprCon prec (PmAltConLike cl) args = do +pprPmAltCon :: Int -> PmAltCon -> [Id] -> PmPprM SDoc +pprPmAltCon _prec (PmAltLit l) _ = pure (ppr l) +pprPmAltCon prec (PmAltConLike cl) args = do delta <- ask pprConLike delta prec cl args @@ -146,24 +146,24 @@ pprConLike delta _prec cl args | Just pm_expr_list <- pmExprAsList delta (PmAltConLike cl) args = case pm_expr_list of NilTerminated list -> - brackets . fsep . punctuate comma <$> mapM (pprPmExprVar 0) list + brackets . fsep . punctuate comma <$> mapM (pprPmVar 0) list WcVarTerminated pref x -> - parens . fcat . punctuate colon <$> mapM (pprPmExprVar 0) (toList pref ++ [x]) + parens . fcat . punctuate colon <$> mapM (pprPmVar 0) (toList pref ++ [x]) pprConLike _delta _prec (RealDataCon con) args | isUnboxedTupleCon con , let hash_parens doc = text "(#" <+> doc <+> text "#)" - = hash_parens . fsep . punctuate comma <$> mapM (pprPmExprVar 0) args + = hash_parens . fsep . punctuate comma <$> mapM (pprPmVar 0) args | isTupleDataCon con - = parens . fsep . punctuate comma <$> mapM (pprPmExprVar 0) args + = parens . fsep . punctuate comma <$> mapM (pprPmVar 0) args pprConLike _delta prec cl args | conLikeIsInfix cl = case args of - [x, y] -> do x' <- pprPmExprVar 1 x - y' <- pprPmExprVar 1 y + [x, y] -> do x' <- pprPmVar 1 x + y' <- pprPmVar 1 y return (cparen (prec > 0) (x' <+> ppr cl <+> y')) -- can it be infix but have more than two arguments? - list -> pprPanic "pprPmExprCon:" (ppr list) + list -> pprPanic "pprConLike:" (ppr list) | null args = return (ppr cl) - | otherwise = do args' <- mapM (pprPmExprVar 2) args + | otherwise = do args' <- mapM (pprPmVar 2) args return (cparen (prec > 1) (fsep (ppr cl : args'))) -- | The result of 'pmExprAsList'. @@ -171,7 +171,7 @@ data PmExprList = NilTerminated [Id] | WcVarTerminated (NonEmpty Id) Id --- | Extract a list of 'PmExpr's out of a sequence of cons cells, optionally +-- | Extract a list of 'Id's out of a sequence of cons cells, optionally -- terminated by a wildcard variable instead of @[]@. Some examples: -- -- * @pmExprAsList (1:2:[]) == Just ('NilTerminated' [1,2])@, a regular, diff --git a/compiler/deSugar/PmExpr.hs b/compiler/deSugar/PmTypes.hs index f83c63e4fd..fc97f636a7 100644 --- a/compiler/deSugar/PmExpr.hs +++ b/compiler/deSugar/PmTypes.hs @@ -1,17 +1,35 @@ {- Author: George Karachalias <george.karachalias@cs.kuleuven.be> - -Haskell expressions (as used by the pattern matching checker) and utilities. + Sebastian Graf <sgraf1337@gmail.com> -} {-# LANGUAGE CPP #-} {-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE TupleSections #-} + +-- | Types used through-out pattern match checking. This module is mostly there +-- to be imported from "TcRnTypes". The exposed API is that of "PmOracle" and +-- "Check". +module PmTypes ( + -- * Representations for Literals and AltCons + PmLit(..), PmLitValue(..), PmAltCon(..), pmLitType, pmAltConType, + + -- ** Equality on 'PmAltCon's + PmEquality(..), eqPmAltCon, + + -- ** Operations on 'PmLit' + literalToPmLit, negatePmLit, overloadPmLit, + pmLitAsStringLit, coreExprAsPmLit, + + -- * Caching partially matched COMPLETE sets + ConLikeSet, PossibleMatches(..), -module PmExpr ( - PmLit(..), PmLitValue(..), PmAltCon(..), - pmAltConType, PmEquality(..), eqPmAltCon, - pmLitType, literalToPmLit, negatePmLit, overloadPmLit, - pmLitAsStringLit, coreExprAsPmLit + -- * A 'DIdEnv' where entries may be shared + Shared(..), SharedDIdEnv(..), emptySDIE, lookupSDIE, sameRepresentativeSDIE, + setIndirectSDIE, setEntrySDIE, traverseSDIE, + + -- * The pattern match oracle + VarInfo(..), TmState(..), Delta(..), initDelta, ) where #include "HsVersions.h" @@ -19,8 +37,13 @@ module PmExpr ( import GhcPrelude import Util +import Bag import FastString +import Var (EvVar) import Id +import VarEnv +import UniqDSet +import UniqDFM import Name import DataCon import ConLike @@ -34,22 +57,13 @@ import CoreUtils (exprType) import PrelNames import TysWiredIn import TysPrim +import TcRnTypes (pprEvVarWithType) import Numeric (fromRat) import Data.Foldable (find) +import qualified Data.List.NonEmpty as NonEmpty import Data.Ratio -{- -%************************************************************************ -%* * - Lifted Expressions -%* * -%************************************************************************ --} - --- ---------------------------------------------------------------------------- --- ** Types - -- | Literals (simple and overloaded ones) for pattern match checking. -- -- See Note [Undecidable Equality for PmAltCons] @@ -118,6 +132,39 @@ pmAltConType :: PmAltCon -> [Type] -> Type pmAltConType (PmAltLit lit) _arg_tys = ASSERT( null _arg_tys ) pmLitType lit pmAltConType (PmAltConLike con) arg_tys = conLikeResTy con arg_tys +instance Outputable PmLitValue where + ppr (PmLitInt i) = ppr i + ppr (PmLitRat r) = ppr (double (fromRat r)) -- good enough + ppr (PmLitChar c) = pprHsChar c + ppr (PmLitString s) = pprHsString s + ppr (PmLitOverInt n i) = minuses n (ppr i) + ppr (PmLitOverRat n r) = minuses n (ppr (double (fromRat r))) + ppr (PmLitOverString s) = pprHsString s + +-- Take care of negated literals +minuses :: Int -> SDoc -> SDoc +minuses n sdoc = iterate (\sdoc -> parens (char '-' <> sdoc)) sdoc !! n + +instance Outputable PmLit where + ppr (PmLit ty v) = ppr v <> suffix + where + -- Some ad-hoc hackery for displaying proper lit suffixes based on type + tbl = [ (intPrimTy, primIntSuffix) + , (int64PrimTy, primInt64Suffix) + , (wordPrimTy, primWordSuffix) + , (word64PrimTy, primWord64Suffix) + , (charPrimTy, primCharSuffix) + , (floatPrimTy, primFloatSuffix) + , (doublePrimTy, primDoubleSuffix) ] + suffix = fromMaybe empty (snd <$> find (eqType ty . fst) tbl) + +instance Outputable PmAltCon where + ppr (PmAltConLike cl) = ppr cl + ppr (PmAltLit l) = ppr l + +instance Outputable PmEquality where + ppr = text . show + -- | Undecidable equality for values represented by 'ConLike's. -- See Note [Undecidable Equality for PmAltCons]. -- 'PatSynCon's aren't enforced to be generative, so two syntactically different @@ -265,12 +312,6 @@ pmLitAsStringLit :: PmLit -> Maybe FastString pmLitAsStringLit (PmLit _ (PmLitString s)) = Just s pmLitAsStringLit _ = Nothing --- ---------------------------------------------------------------------------- --- ** Predicates on PmExpr - --- ----------------------------------------------------------------------- --- ** Lift source expressions (HsExpr Id) to PmExpr - coreExprAsPmLit :: CoreExpr -> Maybe PmLit -- coreExprAsPmLit e | pprTrace "coreExprAsPmLit" (ppr e) False = undefined coreExprAsPmLit (Tick _t e) = coreExprAsPmLit e @@ -322,43 +363,167 @@ coreExprAsPmLit e = case collectArgs e of | otherwise = False -{- -%************************************************************************ -%* * - Pretty printing -%* * -%************************************************************************ --} - -instance Outputable PmLitValue where - ppr (PmLitInt i) = ppr i - ppr (PmLitRat r) = ppr (double (fromRat r)) -- good enough - ppr (PmLitChar c) = pprHsChar c - ppr (PmLitString s) = pprHsString s - ppr (PmLitOverInt n i) = minuses n (ppr i) - ppr (PmLitOverRat n r) = minuses n (ppr (double (fromRat r))) - ppr (PmLitOverString s) = pprHsString s - --- Take care of negated literals -minuses :: Int -> SDoc -> SDoc -minuses n sdoc = iterate (\sdoc -> parens (char '-' <> sdoc)) sdoc !! n +type ConLikeSet = UniqDSet ConLike + +-- | A data type caching the results of 'completeMatchConLikes' with support for +-- deletion of contructors that were already matched on. +data PossibleMatches + = PM TyCon (NonEmpty.NonEmpty ConLikeSet) + -- ^ Each ConLikeSet is a (subset of) the constructors in a COMPLETE pragma + -- 'NonEmpty' because the empty case would mean that the type has no COMPLETE + -- set at all, for which we have 'NoPM' + | NoPM + -- ^ No COMPLETE set for this type (yet). Think of overloaded literals. + +instance Outputable PossibleMatches where + ppr (PM _tc cs) = ppr (NonEmpty.toList cs) + ppr NoPM = text "<NoPM>" + +-- | Either @Indirect x@, meaning the value is represented by that of @x@, or +-- an @Entry@ containing containing the actual value it represents. +data Shared a + = Indirect Id + | Entry a + +-- | A 'DIdEnv' in which entries can be shared by multiple 'Id's. +-- Merge equivalence classes of two Ids by 'setIndirectSDIE' and set the entry +-- of an Id with 'setEntrySDIE'. +newtype SharedDIdEnv a + = SDIE { unSDIE :: DIdEnv (Shared a) } + +emptySDIE :: SharedDIdEnv a +emptySDIE = SDIE emptyDVarEnv + +lookupReprAndEntrySDIE :: SharedDIdEnv a -> Id -> (Id, Maybe a) +lookupReprAndEntrySDIE sdie@(SDIE env) x = case lookupDVarEnv env x of + Nothing -> (x, Nothing) + Just (Indirect y) -> lookupReprAndEntrySDIE sdie y + Just (Entry a) -> (x, Just a) + +-- | @lookupSDIE env x@ looks up an entry for @x@, looking through all +-- 'Indirect's until it finds a shared 'Entry'. +lookupSDIE :: SharedDIdEnv a -> Id -> Maybe a +lookupSDIE sdie x = snd (lookupReprAndEntrySDIE sdie x) + +-- | Check if two variables are part of the same equivalence class. +sameRepresentativeSDIE :: SharedDIdEnv a -> Id -> Id -> Bool +sameRepresentativeSDIE sdie x y = + fst (lookupReprAndEntrySDIE sdie x) == fst (lookupReprAndEntrySDIE sdie y) + +-- | @setIndirectSDIE env x y@ sets @x@'s 'Entry' to @Indirect y@, thereby +-- merging @x@'s equivalence class into @y@'s. This will discard all info on +-- @x@! +setIndirectSDIE :: SharedDIdEnv a -> Id -> Id -> SharedDIdEnv a +setIndirectSDIE sdie@(SDIE env) x y = + SDIE $ extendDVarEnv env (fst (lookupReprAndEntrySDIE sdie x)) (Indirect y) + +-- | @setEntrySDIE env x a@ sets the 'Entry' @x@ is associated with to @a@, +-- thereby modifying its whole equivalence class. +setEntrySDIE :: SharedDIdEnv a -> Id -> a -> SharedDIdEnv a +setEntrySDIE sdie@(SDIE env) x a = + SDIE $ extendDVarEnv env (fst (lookupReprAndEntrySDIE sdie x)) (Entry a) + +traverseSDIE :: Applicative f => (a -> f b) -> SharedDIdEnv a -> f (SharedDIdEnv b) +traverseSDIE f = fmap (SDIE . listToUDFM) . traverse g . udfmToList . unSDIE + where + g (u, Indirect y) = pure (u,Indirect y) + g (u, Entry a) = (u,) . Entry <$> f a -instance Outputable PmLit where - ppr (PmLit ty v) = ppr v <> suffix - where - -- Some ad-hoc hackery for displaying proper lit suffixes based on type - tbl = [ (intPrimTy, primIntSuffix) - , (int64PrimTy, primInt64Suffix) - , (wordPrimTy, primWordSuffix) - , (word64PrimTy, primWord64Suffix) - , (charPrimTy, primCharSuffix) - , (floatPrimTy, primFloatSuffix) - , (doublePrimTy, primDoubleSuffix) ] - suffix = fromMaybe empty (snd <$> find (eqType ty . fst) tbl) +instance Outputable a => Outputable (Shared a) where + ppr (Indirect x) = ppr x + ppr (Entry a) = ppr a -instance Outputable PmAltCon where - ppr (PmAltConLike cl) = ppr cl - ppr (PmAltLit l) = ppr l +instance Outputable a => Outputable (SharedDIdEnv a) where + ppr (SDIE env) = ppr env -instance Outputable PmEquality where - ppr = text . show +-- | The term oracle state. Stores 'VarInfo' for encountered 'Id's. These +-- entries are possibly shared when we figure out that two variables must be +-- equal, thus represent the same set of values. +-- +-- See Note [TmState invariants]. +newtype TmState = TS (SharedDIdEnv VarInfo) + -- Deterministic so that we generate deterministic error messages + +-- | Information about an 'Id'. Stores positive ('vi_pos') facts, like @x ~ Just 42@, +-- and negative ('vi_neg') facts, like "x is not (:)". +-- Also caches the type ('vi_ty'), the 'PossibleMatches' of a COMPLETE set +-- ('vi_cache') and the number of times each variable was refined +-- ('vi_n_refines'). +-- +-- Subject to Note [The Pos/Neg invariant]. +data VarInfo + = VI + { vi_ty :: !Type + -- ^ The type of the variable. Important for rejecting possible GADT + -- constructors or incompatible pattern synonyms (@Just42 :: Maybe Int@). + + , vi_pos :: [(PmAltCon, [Id])] + -- ^ Positive info: 'PmAltCon' apps it is (i.e. @x ~ [Just y, PatSyn z]@), all + -- at the same time (i.e. conjunctive). We need a list because of nested + -- pattern matches involving pattern synonym + -- case x of { Just y -> case x of PatSyn z -> ... } + -- However, no more than one RealDataCon in the list, otherwise contradiction + -- because of generativity. + + , vi_neg :: ![PmAltCon] + -- ^ Negative info: A list of 'PmAltCon's that it 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@. Is orthogonal to anything from 'vi_pos', + -- in the sense that 'eqPmAltCon' returns @PossiblyOverlap@ for any pairing + -- between 'vi_pos' and 'vi_neg'. + + -- See Note [Why record both positive and negative info?] + + , vi_cache :: !PossibleMatches + -- ^ A cache of the associated COMPLETE sets. At any time a superset of + -- possible constructors of each COMPLETE set. So, if it's not in here, we + -- can't possibly match on it. Complementary to 'vi_neg'. We still need it + -- to recognise completion of a COMPLETE set efficiently for large enums. + + , vi_n_refines :: !Int + -- ^ Purely for Check performance reasons. The number of times this + -- representative was refined ('refineToAltCon') in the Check's ConVar split. + -- Sadly, we can't store this info in the Check module, as it's tightly coupled + -- to the particular 'Delta' and also is per *representative*, not per + -- syntactic variable. Note that this number does not always correspond to the + -- length of solutions: 'addVarConCt' might add a solution without + -- incurring the potential exponential blowup by ConVar. + } + +-- | Not user-facing. +instance Outputable TmState where + ppr (TS state) = ppr state + +-- | Not user-facing. +instance Outputable VarInfo where + ppr (VI ty pos neg cache n) + = braces (hcat (punctuate comma [ppr ty, ppr pos, ppr neg, ppr cache, ppr n])) + +-- | Initial state of the oracle. +initTmState :: TmState +initTmState = TS emptySDIE + +-- | Term and type constraints to accompany each value vector abstraction. +-- For efficiency, we store the term oracle state instead of the term +-- constraints. +data Delta = MkDelta { delta_ty_cs :: Bag EvVar -- Type oracle; things like a~Int + , delta_tm_cs :: TmState } -- Term oracle; things like x~Nothing + +-- | An initial delta that is always satisfiable +initDelta :: Delta +initDelta = MkDelta emptyBag initTmState + +instance Outputable Delta where + ppr delta = vcat [ + -- intentionally formatted this way enable the dev to comment in only + -- the info she needs + ppr (delta_tm_cs delta), + ppr (pprEvVarWithType <$> delta_ty_cs delta) + --ppr (delta_ty_cs delta) + ] diff --git a/compiler/deSugar/PmOracle.hs-boot b/compiler/deSugar/PmTypes.hs-boot index e099fe78a6..f6e3a7ec5b 100644 --- a/compiler/deSugar/PmOracle.hs-boot +++ b/compiler/deSugar/PmTypes.hs-boot @@ -1,4 +1,4 @@ -module PmOracle where +module PmTypes where import GhcPrelude () diff --git a/compiler/ghc.cabal.in b/compiler/ghc.cabal.in index 884006b487..fc5f581a4d 100644 --- a/compiler/ghc.cabal.in +++ b/compiler/ghc.cabal.in @@ -334,9 +334,9 @@ Library CoreStats MkCore PprCore - PmExpr - PmPpr PmOracle + PmPpr + PmTypes Check Coverage Desugar diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs index cd3bf5c1a5..fe7db11404 100644 --- a/compiler/typecheck/TcRnTypes.hs +++ b/compiler/typecheck/TcRnTypes.hs @@ -167,7 +167,7 @@ import TcType import Annotations import InstEnv import FamInstEnv -import {-# SOURCE #-} PmOracle (Delta) +import {-# SOURCE #-} PmTypes (Delta) import IOEnv import RdrName import Name |