Commit 8a506104 authored by Georgios Karachalias's avatar Georgios Karachalias

Major Overhaul of Pattern Match Checking (Fixes #595)

This patch adresses several problems concerned with exhaustiveness and
redundancy checking of pattern matching. The list of improvements includes:

* Making the check type-aware (handles GADTs, Type Families, DataKinds, etc.).
  This fixes #4139, #3927, #8970 and other related tickets.

* Making the check laziness-aware. Cases that are overlapped but affect
  evaluation are issued now with "Patterns have inaccessible right hand side".
  Additionally, "Patterns are overlapped" is now replaced by "Patterns are
  redundant".

* Improved messages for literals. This addresses tickets #5724, #2204, etc.

* Improved reasoning concerning cases where simple and overloaded
  patterns are matched (See #322).

* Substantially improved reasoning for pattern guards. Addresses #3078.

* OverloadedLists extension does not break exhaustiveness checking anymore
  (addresses #9951). Note that in general this cannot be handled but if we know
  that an argument has type '[a]', we treat it as a list since, the instance of
  'IsList' gives the identity for both 'fromList' and 'toList'. If the type is
  not clear or is not the list type, then the check cannot do much still. I am
  a bit concerned about OverlappingInstances though, since one may override the
  '[a]' instance with e.g. an '[Int]' instance that is not the identity.

* Improved reasoning for nested pattern matching (partial solution). Now we
  propagate type and (some) term constraints deeper when checking, so we can
  detect more inconsistencies. For example, this is needed for #4139.

I am still not satisfied with several things but I would like to address at
least the following before the next release:
    Term constraints are too many and not printed for non-exhaustive matches
(with the exception of literals). This sometimes results in two identical (in
appearance) uncovered warnings. Unless we actually show their difference, I
would like to have a single warning.
parent d25f3c07
......@@ -15,13 +15,15 @@ module UniqSupply (
mkSplitUniqSupply,
splitUniqSupply, listSplitUniqSupply,
splitUniqSupply3, splitUniqSupply4,
-- * Unique supply monad and its abstraction
UniqSM, MonadUnique(..),
UniqSM, MonadUnique(..), liftUs,
-- ** Operations on the monad
initUs, initUs_,
lazyThenUs, lazyMapUs,
getUniqueSupplyM3,
-- * Set supply strategy
initUniqSupply
......@@ -97,6 +99,22 @@ uniqFromSupply (MkSplitUniqSupply n _ _) = mkUniqueGrimily n
uniqsFromSupply (MkSplitUniqSupply n _ s2) = mkUniqueGrimily n : uniqsFromSupply s2
takeUniqFromSupply (MkSplitUniqSupply n s1 _) = (mkUniqueGrimily n, s1)
-- | Build three 'UniqSupply' from a single one,
-- each of which can supply its own unique
splitUniqSupply3 :: UniqSupply -> (UniqSupply, UniqSupply, UniqSupply)
splitUniqSupply3 us = (us1, us2, us3)
where
(us1, us') = splitUniqSupply us
(us2, us3) = splitUniqSupply us'
-- | Build four 'UniqSupply' from a single one,
-- each of which can supply its own unique
splitUniqSupply4 :: UniqSupply -> (UniqSupply, UniqSupply, UniqSupply, UniqSupply)
splitUniqSupply4 us = (us1, us2, us3, us4)
where
(us1, us2, us') = splitUniqSupply3 us
(us3, us4) = splitUniqSupply us'
{-
************************************************************************
* *
......@@ -185,6 +203,12 @@ instance MonadUnique UniqSM where
getUniqueM = getUniqueUs
getUniquesM = getUniquesUs
getUniqueSupplyM3 :: MonadUnique m => m (UniqSupply, UniqSupply, UniqSupply)
getUniqueSupplyM3 = liftM3 (,,) getUniqueSupplyM getUniqueSupplyM getUniqueSupplyM
liftUs :: MonadUnique m => UniqSM a -> m a
liftUs m = getUniqueSupplyM >>= return . flip initUs_ m
getUniqueUs :: UniqSM Unique
getUniqueUs = USM (\us -> case takeUniqFromSupply us of
(u,us') -> (# u, us' #))
......
This diff is collapsed.
......@@ -130,7 +130,7 @@ dsHsBind dflags
dsHsBind dflags
(FunBind { fun_id = L _ fun, fun_matches = matches
, fun_co_fn = co_fn, fun_tick = tick })
= do { (args, body) <- matchWrapper (FunRhs (idName fun)) matches
= do { (args, body) <- matchWrapper (FunRhs (idName fun)) Nothing matches
; let body' = mkOptTickBox tick body
; rhs <- dsHsWrapper co_fn (mkLams args body')
; let core_binds@(id,_) = makeCorePair dflags fun False 0 rhs
......@@ -169,7 +169,9 @@ dsHsBind dflags
, abe_mono = local, abe_prags = prags } <- export
, not (xopt Opt_Strict dflags) -- handle strict binds
, not (anyBag (isBangedPatBind . unLoc) binds) -- in the next case
= do { (_, bind_prs) <- ds_lhs_binds binds
= -- push type constraints deeper for pattern match check
addDictsDs (toTcTypeBag (listToBag dicts)) $
do { (_, bind_prs) <- ds_lhs_binds binds
; let core_bind = Rec bind_prs
; ds_binds <- dsTcEvBinds_s ev_binds
; rhs <- dsHsWrapper wrap $ -- Usually the identity
......@@ -191,7 +193,9 @@ dsHsBind dflags
, abs_exports = exports, abs_ev_binds = ev_binds
, abs_binds = binds })
-- See Note [Desugaring AbsBinds]
= do { (local_force_vars, bind_prs) <- ds_lhs_binds binds
= -- push type constraints deeper for pattern match check
addDictsDs (toTcTypeBag (listToBag dicts)) $
do { (local_force_vars, bind_prs) <- ds_lhs_binds binds
; let core_bind = Rec [ makeCorePair dflags (add_inline lcl_id) False 0 rhs
| (lcl_id, rhs) <- bind_prs ]
-- Monomorphic recursion possible, hence Rec
......
......@@ -150,7 +150,7 @@ dsUnliftedBind (FunBind { fun_id = L _ fun
, fun_tick = tick }) body
-- Can't be a bang pattern (that looks like a PatBind)
-- so must be simply unboxed
= do { (args, rhs) <- matchWrapper (FunRhs (idName fun)) matches
= do { (args, rhs) <- matchWrapper (FunRhs (idName fun)) Nothing matches
; MASSERT( null args ) -- Functions aren't lifted
; MASSERT( isIdHsWrapper co_fn )
; let rhs' = mkOptTickBox tick rhs
......@@ -215,11 +215,11 @@ dsExpr (NegApp expr neg_expr)
= App <$> dsExpr neg_expr <*> dsLExpr expr
dsExpr (HsLam a_Match)
= uncurry mkLams <$> matchWrapper LambdaExpr a_Match
= uncurry mkLams <$> matchWrapper LambdaExpr Nothing a_Match
dsExpr (HsLamCase arg matches)
= do { arg_var <- newSysLocalDs arg
; ([discrim_var], matching_code) <- matchWrapper CaseAlt matches
; ([discrim_var], matching_code) <- matchWrapper CaseAlt Nothing matches
; return $ Lam arg_var $ bindNonRec discrim_var (Var arg_var) matching_code }
dsExpr e@(HsApp fun arg)
......@@ -319,7 +319,7 @@ dsExpr (HsCoreAnn _ _ expr)
dsExpr (HsCase discrim matches)
= do { core_discrim <- dsLExpr discrim
; ([discrim_var], matching_code) <- matchWrapper CaseAlt matches
; ([discrim_var], matching_code) <- matchWrapper CaseAlt (Just discrim) matches
; return (bindNonRec discrim_var core_discrim matching_code) }
-- Pepe: The binds are in scope in the body but NOT in the binding group
......@@ -576,11 +576,11 @@ dsExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = fields
-- constructor aguments.
; alts <- mapM (mk_alt upd_fld_env) cons_to_upd
; ([discrim_var], matching_code)
<- matchWrapper RecUpd (MG { mg_alts = noLoc alts
, mg_arg_tys = [in_ty]
, mg_res_ty = out_ty, mg_origin = FromSource })
-- FromSource is not strictly right, but we
-- want incomplete pattern-match warnings
<- matchWrapper RecUpd Nothing (MG { mg_alts = noLoc alts
, mg_arg_tys = [in_ty]
, mg_res_ty = out_ty, mg_origin = FromSource })
-- FromSource is not strictly right, but we
-- want incomplete pattern-match warnings
; return (add_field_binds field_binds' $
bindNonRec discrim_var record_expr' matching_code) }
......
......@@ -8,7 +8,7 @@ Matching guarded right-hand-sides (GRHSs)
{-# LANGUAGE CPP #-}
module DsGRHSs ( dsGuarded, dsGRHSs, dsGRHS ) where
module DsGRHSs ( dsGuarded, dsGRHSs, dsGRHS, isTrueLHsExpr ) where
#include "HsVersions.h"
......
......@@ -11,7 +11,7 @@
module DsMonad (
DsM, mapM, mapAndUnzipM,
initDs, initDsTc, fixDs,
initDs, initDsTc, initTcDsForSolver, fixDs,
foldlM, foldrM, whenGOptM, unsetGOptM, unsetWOptM,
Applicative(..),(<$>),
......@@ -31,6 +31,9 @@ module DsMonad (
DsMetaEnv, DsMetaVal(..), dsGetMetaEnv, dsLookupMetaEnv, dsExtendMetaEnv,
-- Getting and setting EvVars and term constraints in local environment
getDictsDs, addDictsDs, getTmCsDs, addTmCsDs,
-- Warnings
DsWarning, warnDs, failWithDs, discardWarningsDs,
......@@ -54,6 +57,7 @@ import HscTypes
import Bag
import DataCon
import TyCon
import PmExpr
import Id
import Module
import Outputable
......@@ -66,6 +70,7 @@ import DynFlags
import ErrUtils
import FastString
import Maybes
import Var (EvVar)
import GHC.Fingerprint
import Data.IORef
......@@ -227,12 +232,36 @@ initDsTc thing_inside
; setEnvs ds_envs thing_inside
}
initTcDsForSolver :: TcM a -> DsM (Messages, Maybe a)
-- Spin up a TcM context so that we can run the constraint solver
-- Returns any error messages generated by the constraint solver
-- and (Just res) if no error happened; Nothing if an errror happened
--
-- Simon says: I'm not very happy about this. We spin up a complete TcM monad
-- only to immediately refine it to a TcS monad.
-- Better perhaps to make TcS into its own monad, rather than building on TcS
-- But that may in turn interact with plugins
initTcDsForSolver thing_inside
= do { (gbl, lcl) <- getEnvs
; hsc_env <- getTopEnv
; let DsGblEnv { ds_mod = mod
, ds_fam_inst_env = fam_inst_env } = gbl
DsLclEnv { dsl_loc = loc } = lcl
; liftIO $ initTc hsc_env HsSrcFile False mod loc $
updGblEnv (\tc_gbl -> tc_gbl { tcg_fam_inst_env = fam_inst_env }) $
thing_inside }
mkDsEnvs :: DynFlags -> Module -> GlobalRdrEnv -> TypeEnv -> FamInstEnv
-> IORef Messages -> IORef [(Fingerprint, (Id, CoreExpr))]
-> (DsGblEnv, DsLclEnv)
mkDsEnvs dflags mod rdr_env type_env fam_inst_env msg_var static_binds_var
= let if_genv = IfGblEnv { if_rec_types = Just (mod, return type_env) }
if_lenv = mkIfLclEnv mod (ptext (sLit "GHC error in desugarer lookup in") <+> ppr mod)
real_span = realSrcLocSpan (mkRealSrcLoc (moduleNameFS (moduleName mod)) 1 1)
gbl_env = DsGblEnv { ds_mod = mod
, ds_fam_inst_env = fam_inst_env
, ds_if_env = (if_genv, if_lenv)
......@@ -242,8 +271,10 @@ mkDsEnvs dflags mod rdr_env type_env fam_inst_env msg_var static_binds_var
, ds_parr_bi = panic "DsMonad: uninitialised ds_parr_bi"
, ds_static_binds = static_binds_var
}
lcl_env = DsLclEnv { dsl_meta = emptyNameEnv
, dsl_loc = noSrcSpan
lcl_env = DsLclEnv { dsl_meta = emptyNameEnv
, dsl_loc = real_span
, dsl_dicts = emptyBag
, dsl_tm_cs = emptyBag
}
in (gbl_env, lcl_env)
......@@ -305,11 +336,34 @@ the @SrcSpan@ being carried around.
getGhcModeDs :: DsM GhcMode
getGhcModeDs = getDynFlags >>= return . ghcMode
-- | Get in-scope type constraints (pm check)
getDictsDs :: DsM (Bag EvVar)
getDictsDs = do { env <- getLclEnv; return (dsl_dicts env) }
-- | Add in-scope type constraints (pm check)
addDictsDs :: Bag EvVar -> DsM a -> DsM a
addDictsDs ev_vars
= updLclEnv (\env -> env { dsl_dicts = unionBags ev_vars (dsl_dicts env) })
-- | Get in-scope term constraints (pm check)
getTmCsDs :: DsM (Bag SimpleEq)
getTmCsDs = do { env <- getLclEnv; return (dsl_tm_cs env) }
-- | Add in-scope term constraints (pm check)
addTmCsDs :: Bag SimpleEq -> DsM a -> DsM a
addTmCsDs tm_cs
= updLclEnv (\env -> env { dsl_tm_cs = unionBags tm_cs (dsl_tm_cs env) })
getSrcSpanDs :: DsM SrcSpan
getSrcSpanDs = do { env <- getLclEnv; return (dsl_loc env) }
getSrcSpanDs = do { env <- getLclEnv
; return (RealSrcSpan (dsl_loc env)) }
putSrcSpanDs :: SrcSpan -> DsM a -> DsM a
putSrcSpanDs new_loc thing_inside = updLclEnv (\ env -> env {dsl_loc = new_loc}) thing_inside
putSrcSpanDs (UnhelpfulSpan {}) thing_inside
= thing_inside
putSrcSpanDs (RealSrcSpan real_span) thing_inside
= updLclEnv (\ env -> env {dsl_loc = real_span}) thing_inside
warnDs :: SDoc -> DsM ()
warnDs warn = do { env <- getGblEnv
; loc <- getSrcSpanDs
......
......@@ -35,6 +35,7 @@ import PatSyn
import MatchCon
import MatchLit
import Type
import TcType ( toTcTypeBag )
import TyCon( isNewTyCon )
import TysWiredIn
import ListSetOps
......@@ -44,132 +45,10 @@ import Util
import Name
import Outputable
import BasicTypes ( isGenerated )
import FastString
import Control.Monad( when )
import Control.Monad( unless )
import qualified Data.Map as Map
{-
This function is a wrapper of @match@, it must be called from all the parts where
it was called match, but only substitutes the first call, ....
if the associated flags are declared, warnings will be issued.
It can not be called matchWrapper because this name already exists :-(
JJCQ 30-Nov-1997
-}
matchCheck :: DsMatchContext
-> [Id] -- Vars rep'ing the exprs we're matching with
-> Type -- Type of the case expression
-> [EquationInfo] -- Info about patterns, etc. (type synonym below)
-> DsM MatchResult -- Desugared result!
matchCheck ctx vars ty qs
= do { dflags <- getDynFlags
; matchCheck_really dflags ctx vars ty qs }
matchCheck_really :: DynFlags
-> DsMatchContext
-> [Id]
-> Type
-> [EquationInfo]
-> DsM MatchResult
matchCheck_really dflags ctx@(DsMatchContext hs_ctx _) vars ty qs
= do { when shadow (dsShadowWarn ctx eqns_shadow)
; when incomplete (dsIncompleteWarn ctx pats)
; match vars ty qs }
where
(pats, eqns_shadow) = check qs
incomplete = incomplete_flag hs_ctx && notNull pats
shadow = wopt Opt_WarnOverlappingPatterns dflags
&& notNull eqns_shadow
incomplete_flag :: HsMatchContext id -> Bool
incomplete_flag (FunRhs {}) = wopt Opt_WarnIncompletePatterns dflags
incomplete_flag CaseAlt = wopt Opt_WarnIncompletePatterns dflags
incomplete_flag IfAlt = False
incomplete_flag LambdaExpr = wopt Opt_WarnIncompleteUniPatterns dflags
incomplete_flag PatBindRhs = wopt Opt_WarnIncompleteUniPatterns dflags
incomplete_flag ProcExpr = wopt Opt_WarnIncompleteUniPatterns dflags
incomplete_flag RecUpd = wopt Opt_WarnIncompletePatternsRecUpd dflags
incomplete_flag ThPatSplice = False
incomplete_flag PatSyn = False
incomplete_flag ThPatQuote = False
incomplete_flag (StmtCtxt {}) = False -- Don't warn about incomplete patterns
-- in list comprehensions, pattern guards
-- etc. They are often *supposed* to be
-- incomplete
{-
This variable shows the maximum number of lines of output generated for warnings.
It will limit the number of patterns/equations displayed to@ maximum_output@.
(ToDo: add command-line option?)
-}
maximum_output :: Int
maximum_output = 4
-- The next two functions create the warning message.
dsShadowWarn :: DsMatchContext -> [EquationInfo] -> DsM ()
dsShadowWarn ctx@(DsMatchContext kind loc) qs
= putSrcSpanDs loc (warnDs warn)
where
warn | qs `lengthExceeds` maximum_output
= pp_context ctx (ptext (sLit "are overlapped"))
(\ f -> vcat (map (ppr_eqn f kind) (take maximum_output qs)) $$
ptext (sLit "..."))
| otherwise
= pp_context ctx (ptext (sLit "are overlapped"))
(\ f -> vcat $ map (ppr_eqn f kind) qs)
dsIncompleteWarn :: DsMatchContext -> [ExhaustivePat] -> DsM ()
dsIncompleteWarn ctx@(DsMatchContext kind loc) pats
= putSrcSpanDs loc (warnDs warn)
where
warn = pp_context ctx (ptext (sLit "are non-exhaustive"))
(\_ -> hang (ptext (sLit "Patterns not matched:"))
4 ((vcat $ map (ppr_incomplete_pats kind)
(take maximum_output pats))
$$ dots))
dots | pats `lengthExceeds` maximum_output = ptext (sLit "...")
| otherwise = empty
pp_context :: DsMatchContext -> SDoc -> ((SDoc -> SDoc) -> SDoc) -> SDoc
pp_context (DsMatchContext kind _loc) msg rest_of_msg_fun
= vcat [ptext (sLit "Pattern match(es)") <+> msg,
sep [ptext (sLit "In") <+> ppr_match <> char ':', nest 4 (rest_of_msg_fun pref)]]
where
(ppr_match, pref)
= case kind of
FunRhs fun -> (pprMatchContext kind, \ pp -> ppr fun <+> pp)
_ -> (pprMatchContext kind, \ pp -> pp)
ppr_pats :: Outputable a => [a] -> SDoc
ppr_pats pats = sep (map ppr pats)
ppr_shadow_pats :: HsMatchContext Name -> [Pat Id] -> SDoc
ppr_shadow_pats kind pats
= sep [ppr_pats pats, matchSeparator kind, ptext (sLit "...")]
ppr_incomplete_pats :: HsMatchContext Name -> ExhaustivePat -> SDoc
ppr_incomplete_pats _ (pats,[]) = ppr_pats pats
ppr_incomplete_pats _ (pats,constraints) =
sep [ppr_pats pats, ptext (sLit "with"),
sep (map ppr_constraint constraints)]
ppr_constraint :: (Name,[HsLit]) -> SDoc
ppr_constraint (var,pats) = sep [ppr var, ptext (sLit "`notElem`"), ppr pats]
ppr_eqn :: (SDoc -> SDoc) -> HsMatchContext Name -> EquationInfo -> SDoc
ppr_eqn prefixF kind eqn = prefixF (ppr_shadow_pats kind (eqn_pats eqn))
{-
************************************************************************
* *
......@@ -764,6 +643,7 @@ Call @match@ with all of this information!
-}
matchWrapper :: HsMatchContext Name -- For shadowing warning messages
-> Maybe (LHsExpr Id) -- The scrutinee, if we check a case expr
-> MatchGroup Id (LHsExpr Id) -- Matches being desugared
-> DsM ([Id], CoreExpr) -- Results
......@@ -791,22 +671,38 @@ one pattern, and match simply only accepts one pattern.
JJQC 30-Nov-1997
-}
matchWrapper ctxt (MG { mg_alts = L _ matches
, mg_arg_tys = arg_tys
, mg_res_ty = rhs_ty
, mg_origin = origin })
= do { eqns_info <- mapM mk_eqn_info matches
matchWrapper ctxt mb_scr (MG { mg_alts = L _ matches
, mg_arg_tys = arg_tys
, mg_res_ty = rhs_ty
, mg_origin = origin })
= do { dflags <- getDynFlags
; locn <- getSrcSpanDs
; new_vars <- case matches of
[] -> mapM newSysLocalDs arg_tys
(m:_) -> selectMatchVars (map unLoc (hsLMatchPats m))
; eqns_info <- mapM (mk_eqn_info new_vars) matches
-- pattern match check warnings
; unless (isGenerated origin) $
-- See Note [Type and Term Equality Propagation]
addTmCsDs (genCaseTmCs1 mb_scr new_vars) $
dsPmWarn dflags (DsMatchContext ctxt locn) $
checkMatches new_vars matches
; result_expr <- handleWarnings $
matchEquations ctxt new_vars eqns_info rhs_ty
; return (new_vars, result_expr) }
where
mk_eqn_info (L _ (Match _ pats _ grhss))
mk_eqn_info vars (L _ (Match _ pats _ grhss))
= do { dflags <- getDynFlags
; let upats = map (strictify dflags) pats
; match_result <- dsGRHSs ctxt upats grhss rhs_ty
dicts = toTcTypeBag (collectEvVarsPats upats) -- Only TcTyVars
; tm_cs <- genCaseTmCs2 mb_scr upats vars
; match_result <- addDictsDs dicts $ -- See Note [Type and Term Equality Propagation]
addTmCsDs tm_cs $ -- See Note [Type and Term Equality Propagation]
dsGRHSs ctxt upats grhss rhs_ty
; return (EqnInfo { eqn_pats = upats, eqn_rhs = match_result}) }
strictify dflags pat =
......@@ -822,11 +718,9 @@ matchEquations :: HsMatchContext Name
-> [Id] -> [EquationInfo] -> Type
-> DsM CoreExpr
matchEquations ctxt vars eqns_info rhs_ty
= do { locn <- getSrcSpanDs
; let ds_ctxt = DsMatchContext ctxt locn
error_doc = matchContextErrString ctxt
= do { let error_doc = matchContextErrString ctxt
; match_result <- matchCheck ds_ctxt vars rhs_ty eqns_info
; match_result <- match vars rhs_ty eqns_info
; fail_expr <- mkErrorAppDs pAT_ERROR_ID rhs_ty error_doc
; extractMatchResult match_result fail_expr }
......@@ -864,10 +758,14 @@ matchSinglePat :: CoreExpr -> HsMatchContext Name -> LPat Id
-- Used for things like [ e | pat <- stuff ], where
-- incomplete patterns are just fine
matchSinglePat (Var var) ctx (L _ pat) ty match_result
= do { locn <- getSrcSpanDs
; matchCheck (DsMatchContext ctx locn)
[var] ty
[EqnInfo { eqn_pats = [pat], eqn_rhs = match_result }] }
= do { dflags <- getDynFlags
; locn <- getSrcSpanDs
-- pattern match check warnings
; dsPmWarn dflags (DsMatchContext ctx locn) (checkSingle var pat)
; match [var] ty
[EqnInfo { eqn_pats = [pat], eqn_rhs = match_result }] }
matchSinglePat scrut hs_ctx pat ty match_result
= do { var <- selectSimpleMatchVarL pat
......
......@@ -13,6 +13,7 @@ match :: [Id]
matchWrapper
:: HsMatchContext Name
-> Maybe (LHsExpr Id)
-> MatchGroup Id (LHsExpr Id)
-> DsM ([Id], CoreExpr)
......
{-
Author: George Karachalias <george.karachalias@cs.kuleuven.be>
Haskell expressions (as used by the pattern matching checker) and utilities.
-}
{-# LANGUAGE CPP #-}
module PmExpr (
PmExpr(..), PmLit(..), SimpleEq, ComplexEq, eqPmLit,
truePmExpr, falsePmExpr, isTruePmExpr, isFalsePmExpr, isNotPmExprOther,
lhsExprToPmExpr, hsExprToPmExpr, substComplexEq, filterComplex,
pprPmExprWithParens, runPmPprM
) where
#include "HsVersions.h"
import HsSyn
import Id
import DataCon
import TysWiredIn
import Outputable
import Util
import SrcLoc
import FastString -- sLit
import VarSet
import Data.Functor ((<$>))
import Data.Maybe (mapMaybe)
import Data.List (groupBy, sortBy)
import Control.Monad.Trans.State.Lazy
{-
%************************************************************************
%* *
Lifted Expressions
%* *
%************************************************************************
-}
{- Note [PmExprOther in PmExpr]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Since there is no plan to extend the (currently pretty naive) term oracle in
the near future, instead of playing with the verbose (HsExpr Id), we lift it to
PmExpr. All expressions the term oracle does not handle are wrapped by the
constructor PmExprOther. Note that we do not perform substitution in
PmExprOther. Because of this, we do not even print PmExprOther, since they may
refer to variables that are otherwise substituted away.
-}
-- ----------------------------------------------------------------------------
-- ** Types
-- | Lifted expressions for pattern match checking.
data PmExpr = PmExprVar Id
| PmExprCon DataCon [PmExpr]
| PmExprLit PmLit
| PmExprEq PmExpr PmExpr -- Syntactic equality
| PmExprOther (HsExpr Id) -- Note [PmExprOther in PmExpr]
-- | Literals (simple and overloaded ones) for pattern match checking.
data PmLit = PmSLit HsLit -- simple
| PmOLit Bool {- is it negated? -} (HsOverLit Id) -- overloaded
-- | PmLit equality. If both literals are overloaded, the equality check may be
-- inconclusive. Since an overloaded PmLit represents a function application
-- (e.g. fromInteger 5), if two literals look the same they are the same but
-- if they don't, whether they are depends on the implementation of the
-- from-function.
eqPmLit :: PmLit -> PmLit -> Maybe Bool
eqPmLit (PmSLit l1) (PmSLit l2 ) = Just (l1 == l2)
eqPmLit (PmOLit b1 l1) (PmOLit b2 l2) = if res then Just True else Nothing
where res = b1 == b2 && l1 == l2
eqPmLit _ _ = Just False -- this should not even happen I think
nubPmLit :: [PmLit] -> [PmLit]
nubPmLit [] = []
nubPmLit [x] = [x]
nubPmLit (x:xs) = x : nubPmLit (filter (neqPmLit x) xs)
where neqPmLit l1 l2 = case eqPmLit l1 l2 of
Just True -> False
Just False -> True
Nothing -> True
-- | Term equalities
type SimpleEq = (Id, PmExpr) -- We always use this orientation
type ComplexEq = (PmExpr, PmExpr)
-- | Expression `True'
truePmExpr :: PmExpr
truePmExpr = PmExprCon trueDataCon []
-- | Expression `False'
falsePmExpr :: PmExpr
falsePmExpr = PmExprCon falseDataCon []
-- ----------------------------------------------------------------------------