diff options
author | George Karachalias <george.karachalias@gmail.com> | 2015-12-04 07:11:55 +0100 |
---|---|---|
committer | George Karachalias <george.karachalias@gmail.com> | 2015-12-04 07:11:55 +0100 |
commit | ae4398d64655b43606386dddb01637bbfcf0171e (patch) | |
tree | 3ae903b249547366a6ad8531b7d773238ac1a74a /compiler | |
parent | 40fc353650d44472203153b04302a3614a0552eb (diff) | |
download | haskell-ae4398d64655b43606386dddb01637bbfcf0171e.tar.gz |
Improve performance for PM check on literals (Fixes #11160 and #11161)
Two changes:
1. Instead of generating constraints of the form (x ~ e) (as we do in
the paper), generate constraints of the form (e ~ e). The term oracle
(`tmOracle` in deSugar/TmOracle.hs) is not really efficient and in the
presence of many (x ~ e) constraints behaves quadratically. For
literals, constraints of the form (False ~ (x ~ lit)) are pretty common,
so if we start with { y ~ False, y ~ (x ~ lit) } we end up givng to the
solver (a) twice as many constraints as we need and (b) half of them
trigger the solver's weakness. This fixes #11160.
2. Treat two overloaded literals that look different as different. This
is not entirely correct but it is what both the previous and the current
check did. I had the ambitious plan to do the *right thing* (equality
between overloaded literals is undecidable in the general case) and just
use this assumption when issuing the warnings. It seems to generate much
more constraints than I expected (breaks #11161) so I just do it
immediately now instead of generating everything and filtering
afterwards.
Even if it is not (strictly speaking) correct, we have the following:
* Gives the "expected" warnings (the ones Ocaml or the previous
algorithm would give) and,
* Most importantly, it is safe. Unless a catch-all clause exists, a
match against literals is always non-exhaustive. So, effectively
this affects only what is shown to the user (and, evidently,
performance!).
Diffstat (limited to 'compiler')
-rw-r--r-- | compiler/deSugar/Check.hs | 128 | ||||
-rw-r--r-- | compiler/deSugar/PmExpr.hs | 24 | ||||
-rw-r--r-- | compiler/deSugar/TmOracle.hs | 247 |
3 files changed, 70 insertions, 329 deletions
diff --git a/compiler/deSugar/Check.hs b/compiler/deSugar/Check.hs index 382112c951..55dcfc224e 100644 --- a/compiler/deSugar/Check.hs +++ b/compiler/deSugar/Check.hs @@ -71,7 +71,7 @@ The algorithm used is described in the paper: type PmM a = DsM a -data PmConstraint = TmConstraint Id PmExpr -- ^ Term equalities: x ~ e +data PmConstraint = TmConstraint PmExpr PmExpr -- ^ Term equalities: e ~ e | TyConstraint [EvVar] -- ^ Type equalities | BtConstraint Id -- ^ Strictness constraints: x ~ _|_ @@ -174,10 +174,12 @@ checkMatches vars matches initial_uncovered :: [Id] -> DsM ValSetAbs initial_uncovered vars = do ty_cs <- TyConstraint . bagToList <$> getDictsDs - tm_cs <- map (uncurry TmConstraint) . bagToList <$> getTmCsDs + tm_cs <- map simpleToTmCs . bagToList <$> getTmCsDs let vsa = map (VA . PmVar) vars return $ mkConstraint (ty_cs:tm_cs) (foldr Cons Singleton vsa) - + where + simpleToTmCs :: (Id, PmExpr) -> PmConstraint + simpleToTmCs (x,e) = TmConstraint (PmExprVar x) e {- %************************************************************************ %* * @@ -670,8 +672,8 @@ mkOneConFull x usupply con = (con_abs, constraints) , pm_con_args = arguments } constraints -- term and type constraints - | null evvars = [ TmConstraint x (pmPatToPmExpr con_abs) ] - | otherwise = [ TmConstraint x (pmPatToPmExpr con_abs) + | null evvars = [ TmConstraint (PmExprVar x) (pmPatToPmExpr con_abs) ] + | otherwise = [ TmConstraint (PmExprVar x) (pmPatToPmExpr con_abs) , TyConstraint evvars ] mkConVars :: UniqSupply -> [Type] -> [ValAbs] -- ys, fresh with the given type @@ -818,14 +820,14 @@ nameType name usupply ty = newEvVar idname ty idname = mkInternalName unique occname noSrcSpan -- | Partition the constraints to type cs, term cs and forced variables -splitConstraints :: [PmConstraint] -> ([EvVar], [(Id, PmExpr)], Maybe Id) +splitConstraints :: [PmConstraint] -> ([EvVar], [(PmExpr, PmExpr)], Maybe Id) splitConstraints [] = ([],[],Nothing) splitConstraints (c : rest) = case c of - TyConstraint cs -> (cs ++ ty_cs, tm_cs, bot_cs) - TmConstraint x e -> (ty_cs, (x,e):tm_cs, bot_cs) - BtConstraint cs -> ASSERT (isNothing bot_cs) -- NB: Only one x ~ _|_ - (ty_cs, tm_cs, Just cs) + TyConstraint cs -> (cs ++ ty_cs, tm_cs, bot_cs) + TmConstraint e1 e2 -> (ty_cs, (e1,e2):tm_cs, bot_cs) + BtConstraint cs -> ASSERT (isNothing bot_cs) -- NB: Only one x ~ _|_ + (ty_cs, tm_cs, Just cs) where (ty_cs, tm_cs, bot_cs) = splitConstraints rest @@ -883,20 +885,14 @@ pruneVSABound n v = go n init_cs emptylist v vecs1 <- go n all_cs vec vsa1 vecs2 <- go (n - length vecs1) all_cs vec vsa2 return (vecs1 ++ vecs2) - Singleton -> - -- Have another go at the term oracle state, for strange - -- equalities between overloaded literals. See - -- Note [Undecidable Equality on Overloaded Literals] in TmOracle - if containsEqLits tm_env - then return [] -- not on the safe side - else do - -- TODO: Provide an incremental interface for the type oracle - sat <- tyOracle (listToBag ty_cs) - return $ case sat of - True -> let (residual_eqs, subst) = wrapUpTmState tm_env - vector = substInValVecAbs subst (toList vec) - in [(vector, residual_eqs)] - False -> [] + Singleton -> do + -- TODO: Provide an incremental interface for the type oracle + sat <- tyOracle (listToBag ty_cs) + return $ case sat of + True -> let (residual_eqs, subst) = wrapUpTmState tm_env + vector = substInValVecAbs subst (toList vec) + in [(vector, residual_eqs)] + False -> [] Constraint cs vsa -> case splitConstraints cs of (new_ty_cs, new_tm_cs, new_bot_ct) -> @@ -1000,7 +996,7 @@ pmTraverse us gvsa rec (p:ps) vsa = PmGuard pv e -> let (us1, us2) = splitUniqSupply us y = mkPmId us1 (patternType p) - cs = [TmConstraint y e] + cs = [TmConstraint (PmExprVar y) e] in mkConstraint cs $ tailVSA $ pmTraverse us2 gvsa rec (pv++ps) (VA (PmVar y) `mkCons` vsa) @@ -1023,16 +1019,12 @@ cMatcher, uMatcher, dMatcher :: PmMatcher -- CVar cMatcher us gvsa (PmVar x) ps va vsa = VA va `mkCons` (cs `mkConstraint` covered us gvsa ps vsa) - where cs = [TmConstraint x (pmPatToPmExpr va)] + where cs = [TmConstraint (PmExprVar x) (pmPatToPmExpr va)] -- CLitCon cMatcher us gvsa (PmLit l) ps (va@(PmCon {})) vsa - = VA va `mkCons` (cs `mkConstraint` covered us2 gvsa ps vsa) - where - (us1, us2) = splitUniqSupply us - y = mkPmId us1 (pmPatType va) - cs = [ TmConstraint y (PmExprLit l) - , TmConstraint y (pmPatToPmExpr va) ] + = VA va `mkCons` (cs `mkConstraint` covered us gvsa ps vsa) + where cs = [ TmConstraint (PmExprLit l) (pmPatToPmExpr va) ] -- CConLit cMatcher us gvsa (p@(PmCon {})) ps (PmLit l) vsa @@ -1041,7 +1033,7 @@ cMatcher us gvsa (p@(PmCon {})) ps (PmLit l) vsa (us1, us2, us3) = splitUniqSupply3 us y = mkPmId us1 (pmPatType p) (con_abs, all_cs) = mkOneConFull y us2 (pm_con_con p) - cs = TmConstraint y (PmExprLit l) : all_cs + cs = TmConstraint (PmExprVar y) (PmExprLit l) : all_cs -- CConCon cMatcher us gvsa (p@(PmCon { pm_con_con = c1, pm_con_args = args1 })) ps @@ -1055,15 +1047,8 @@ cMatcher us gvsa (p@(PmCon { pm_con_con = c1, pm_con_args = args1 })) ps -- CLitLit cMatcher us gvsa (PmLit l1) ps (va@(PmLit l2)) vsa = case eqPmLit l1 l2 of - Just True -> VA va `mkCons` covered us gvsa ps vsa -- match - Just False -> Empty -- mismatch - Nothing -> VA va `mkCons` (cs `mkConstraint` covered us2 gvsa ps vsa) - -- See Note [Undecidable Equality on Overloaded Literals] in TmOracle - where - (us1, us2) = splitUniqSupply us - y = mkPmId us1 (pmPatType va) - cs = [ TmConstraint y (PmExprLit l1) - , TmConstraint y (PmExprLit l2) ] + True -> VA va `mkCons` covered us gvsa ps vsa -- match + False -> Empty -- mismatch -- CConVar cMatcher us gvsa (p@(PmCon { pm_con_con = con })) ps (PmVar x) vsa @@ -1077,7 +1062,7 @@ cMatcher us gvsa (p@(PmLit l)) ps (PmVar x) vsa = cMatcher us gvsa p ps lit_abs (mkConstraint cs vsa) where lit_abs = PmLit l - cs = [TmConstraint x (PmExprLit l)] + cs = [TmConstraint (PmExprVar x) (PmExprLit l)] -- uMatcher -- ---------------------------------------------------------------------------- @@ -1085,7 +1070,7 @@ cMatcher us gvsa (p@(PmLit l)) ps (PmVar x) vsa -- UVar uMatcher us gvsa (PmVar x) ps va vsa = VA va `mkCons` (cs `mkConstraint` uncovered us gvsa ps vsa) - where cs = [TmConstraint x (pmPatToPmExpr va)] + where cs = [TmConstraint (PmExprVar x) (pmPatToPmExpr va)] -- ULitCon uMatcher us gvsa (PmLit l) ps (va@(PmCon {})) vsa @@ -1093,7 +1078,7 @@ uMatcher us gvsa (PmLit l) ps (va@(PmCon {})) vsa where (us1, us2) = splitUniqSupply us y = mkPmId us1 (pmPatType va) - cs = [TmConstraint y (PmExprLit l)] + cs = [TmConstraint (PmExprVar y) (PmExprLit l)] -- UConLit uMatcher us gvsa (p@(PmCon {})) ps (PmLit l) vsa @@ -1101,7 +1086,7 @@ uMatcher us gvsa (p@(PmCon {})) ps (PmLit l) vsa where (us1, us2) = splitUniqSupply us y = mkPmId us1 (pmPatType p) - cs = [TmConstraint y (PmExprLit l)] + cs = [TmConstraint (PmExprVar y) (PmExprLit l)] -- UConCon uMatcher us gvsa ( p@(PmCon { pm_con_con = c1, pm_con_args = args1 })) ps @@ -1115,20 +1100,8 @@ uMatcher us gvsa ( p@(PmCon { pm_con_con = c1, pm_con_args = args1 })) ps -- ULitLit uMatcher us gvsa (PmLit l1) ps (va@(PmLit l2)) vsa = case eqPmLit l1 l2 of - Just True -> VA va `mkCons` uncovered us gvsa ps vsa -- match - Just False -> VA va `mkCons` vsa -- mismatch - Nothing -> mkUnion (VA va `mkCons` - (match_cs `mkConstraint` uncovered us3 gvsa ps vsa)) - (non_match_cs `mkConstraint` (VA va `mkCons` vsa)) - -- See Note [Undecidable Equality on Overloaded Literals] in TmOracle - where - (us1, us2, us3) = splitUniqSupply3 us - y = mkPmId us1 (pmPatType va) - z = mkPmId us2 boolTy - match_cs = [ TmConstraint y (PmExprLit l1) - , TmConstraint y (PmExprLit l2) ] - non_match_cs = [ TmConstraint z falsePmExpr - , TmConstraint z (PmExprEq (PmExprLit l1) (PmExprLit l2))] + True -> VA va `mkCons` uncovered us gvsa ps vsa -- match + False -> VA va `mkCons` vsa -- mismatch -- UConVar uMatcher us gvsa (p@(PmCon { pm_con_con = con })) ps (PmVar x) vsa @@ -1145,14 +1118,12 @@ uMatcher us gvsa (p@(PmCon { pm_con_con = con })) ps (PmVar x) vsa -- ULitVar uMatcher us gvsa (p@(PmLit l)) ps (PmVar x) vsa - = mkUnion (uMatcher us2 gvsa p ps (PmLit l) (mkConstraint match_cs vsa)) + = mkUnion (uMatcher us gvsa p ps (PmLit l) (mkConstraint match_cs vsa)) (non_match_cs `mkConstraint` (VA (PmVar x) `mkCons` vsa)) where - (us1, us2) = splitUniqSupply us - y = mkPmId us1 (pmPatType p) - match_cs = [ TmConstraint x (PmExprLit l)] - non_match_cs = [ TmConstraint y falsePmExpr - , TmConstraint y (PmExprEq (PmExprVar x) (PmExprLit l)) ] + match_cs = [ TmConstraint (PmExprVar x) (PmExprLit l)] + non_match_cs = [ TmConstraint falsePmExpr + (PmExprEq (PmExprVar x) (PmExprLit l)) ] -- dMatcher -- ---------------------------------------------------------------------------- @@ -1160,16 +1131,12 @@ uMatcher us gvsa (p@(PmLit l)) ps (PmVar x) vsa -- DVar dMatcher us gvsa (PmVar x) ps va vsa = VA va `mkCons` (cs `mkConstraint` divergent us gvsa ps vsa) - where cs = [TmConstraint x (pmPatToPmExpr va)] + where cs = [TmConstraint (PmExprVar x) (pmPatToPmExpr va)] -- DLitCon dMatcher us gvsa (PmLit l) ps (va@(PmCon {})) vsa - = VA va `mkCons` (cs `mkConstraint` divergent us2 gvsa ps vsa) - where - (us1, us2) = splitUniqSupply us - y = mkPmId us1 (pmPatType va) - cs = [ TmConstraint y (PmExprLit l) - , TmConstraint y (pmPatToPmExpr va) ] + = VA va `mkCons` (cs `mkConstraint` divergent us gvsa ps vsa) + where cs = [ TmConstraint (PmExprLit l) (pmPatToPmExpr va) ] -- DConLit dMatcher us gvsa (p@(PmCon { pm_con_con = con })) ps (PmLit l) vsa @@ -1178,7 +1145,7 @@ dMatcher us gvsa (p@(PmCon { pm_con_con = con })) ps (PmLit l) vsa (us1, us2, us3) = splitUniqSupply3 us y = mkPmId us1 (pmPatType p) (con_abs, all_cs) = mkOneConFull y us2 con - cs = TmConstraint y (PmExprLit l) : all_cs + cs = TmConstraint (PmExprVar y) (PmExprLit l) : all_cs -- DConCon dMatcher us gvsa (p@(PmCon { pm_con_con = c1, pm_con_args = args1 })) ps @@ -1192,15 +1159,8 @@ dMatcher us gvsa (p@(PmCon { pm_con_con = c1, pm_con_args = args1 })) ps -- DLitLit dMatcher us gvsa (PmLit l1) ps (va@(PmLit l2)) vsa = case eqPmLit l1 l2 of - Just True -> VA va `mkCons` divergent us gvsa ps vsa -- we know: match - Just False -> Empty -- we know: no match - Nothing -> VA va `mkCons` (cs `mkConstraint` divergent us2 gvsa ps vsa) - -- See Note [Undecidable Equality on Overloaded Literals] in TmOracle - where - (us1, us2) = splitUniqSupply us - y = mkPmId us1 (pmPatType va) - cs = [ TmConstraint y (PmExprLit l1) - , TmConstraint y (PmExprLit l2) ] + True -> VA va `mkCons` divergent us gvsa ps vsa -- match + False -> Empty -- mismatch -- DConVar dMatcher us gvsa (p@(PmCon { pm_con_con = con })) ps (PmVar x) vsa @@ -1215,7 +1175,7 @@ dMatcher us gvsa (PmLit l) ps (PmVar x) vsa = mkUnion (VA (PmVar x) `mkCons` mkConstraint [BtConstraint x] vsa) (dMatcher us gvsa (PmLit l) ps (PmLit l) (mkConstraint cs vsa)) where - cs = [TmConstraint x (PmExprLit l)] + cs = [TmConstraint (PmExprVar x) (PmExprLit l)] -- ---------------------------------------------------------------------------- -- * Propagation of term constraints inwards when checking nested matches diff --git a/compiler/deSugar/PmExpr.hs b/compiler/deSugar/PmExpr.hs index c28e95d90d..f426bb4d19 100644 --- a/compiler/deSugar/PmExpr.hs +++ b/compiler/deSugar/PmExpr.hs @@ -27,7 +27,7 @@ import VarSet import Data.Functor ((<$>)) import Data.Maybe (mapMaybe) -import Data.List (groupBy, sortBy) +import Data.List (groupBy, sortBy, nubBy) import Control.Monad.Trans.State.Lazy {- @@ -66,21 +66,16 @@ data PmLit = PmSLit HsLit -- simple -- 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 +-- from-function. Yet, for the purposes of the check, we check syntactically +-- only (it is safe anyway, since literals always need a catch-all to be +-- considered to be exhaustive). +eqPmLit :: PmLit -> PmLit -> Bool +eqPmLit (PmSLit l1) (PmSLit l2) = l1 == l2 +eqPmLit (PmOLit b1 l1) (PmOLit b2 l2) = b1 == b2 && l1 == l2 +eqPmLit _ _ = False 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 +nubPmLit = nubBy eqPmLit -- | Term equalities type SimpleEq = (Id, PmExpr) -- We always use this orientation @@ -374,4 +369,3 @@ instance Outputable PmLit where -- not really useful for pmexprs per se instance Outputable PmExpr where ppr e = fst $ runPmPprM (pprPmExpr e) [] - diff --git a/compiler/deSugar/TmOracle.hs b/compiler/deSugar/TmOracle.hs index 8babc2ebdc..3731f801d3 100644 --- a/compiler/deSugar/TmOracle.hs +++ b/compiler/deSugar/TmOracle.hs @@ -14,7 +14,7 @@ module TmOracle ( pprPmExprWithParens, lhsExprToPmExpr, hsExprToPmExpr, -- the term oracle - tmOracle, TmState, initialTmState, containsEqLits, + tmOracle, TmState, initialTmState, -- misc. exprDeepLookup, pmLitType, flattenPmVarEnv @@ -91,12 +91,12 @@ type TmState = ([ComplexEq], TmOracleEnv) initialTmState :: TmState initialTmState = ([], (False, Map.empty)) --- | Solve a simple equality. -solveSimpleEq :: TmState -> SimpleEq -> Maybe TmState -solveSimpleEq solver_env@(_,(_,env)) simple +-- | Solve a complex equality (top-level). +solveOneEq :: TmState -> ComplexEq -> Maybe TmState +solveOneEq solver_env@(_,(_,env)) complex = solveComplexEq solver_env -- do the actual *merging* with existing state - $ simplifyComplexEq -- simplify as much as you can - $ applySubstSimpleEq env simple -- replace everything we already know + $ simplifyComplexEq -- simplify as much as you can + $ applySubstComplexEq env complex -- replace everything we already know -- | Solve a complex equality. solveComplexEq :: TmState -> ComplexEq -> Maybe TmState @@ -106,9 +106,8 @@ solveComplexEq solver_state@(standby, (unhandled, env)) eq@(e1, e2) = case eq of (_,PmExprOther _) -> Just (standby, (True, env)) (PmExprLit l1, PmExprLit l2) -> case eqPmLit l1 l2 of - Just True -> Just solver_state -- we are sure: equal - Just False -> Nothing -- we are sure: not equal - Nothing -> Just (eq:standby, (unhandled, env)) -- no clue + True -> Just solver_state + False -> Nothing (PmExprCon c1 ts1, PmExprCon c2 ts2) | c1 == c2 -> foldlM solveComplexEq solver_state (zip ts1 ts2) @@ -166,9 +165,8 @@ simplifyEqExpr e1 e2 = case (e1, e2) of -- Literals (PmExprLit l1, PmExprLit l2) -> case eqPmLit l1 l2 of - Just True -> (truePmExpr, True) - Just False -> (falsePmExpr, True) - Nothing -> (original, False) + True -> (truePmExpr, True) + False -> (falsePmExpr, True) -- Can potentially be simplified (PmExprEq {}, _) -> case (simplifyPmExpr e1, simplifyPmExpr e2) of @@ -199,18 +197,18 @@ simplifyEqExpr e1 e2 = case (e1, e2) of where original = PmExprEq e1 e2 -- reconstruct equality --- | Apply an (un-flattened) substitution on a simple equality. -applySubstSimpleEq :: PmVarEnv -> SimpleEq -> ComplexEq -applySubstSimpleEq env (x, e) = (varDeepLookup env x, exprDeepLookup env e) +-- | Apply an (un-flattened) substitution to a simple equality. +applySubstComplexEq :: PmVarEnv -> ComplexEq -> ComplexEq +applySubstComplexEq env (e1,e2) = (exprDeepLookup env e1, exprDeepLookup env e2) --- | Apply an (un-flattened) substitution on a variable. +-- | Apply an (un-flattened) substitution to a variable. varDeepLookup :: PmVarEnv -> Id -> PmExpr varDeepLookup env x | Just e <- Map.lookup x env = exprDeepLookup env e -- go deeper | otherwise = PmExprVar x -- terminal {-# INLINE varDeepLookup #-} --- | Apply an (un-flattened) substitution on an expression. +-- | Apply an (un-flattened) substitution to an expression. exprDeepLookup :: PmVarEnv -> PmExpr -> PmExpr exprDeepLookup env (PmExprVar x) = varDeepLookup env x exprDeepLookup env (PmExprCon c es) = PmExprCon c (map (exprDeepLookup env) es) @@ -219,8 +217,8 @@ exprDeepLookup env (PmExprEq e1 e2) = PmExprEq (exprDeepLookup env e1) exprDeepLookup _ other_expr = other_expr -- PmExprLit, PmExprOther -- | External interface to the term oracle. -tmOracle :: TmState -> [SimpleEq] -> Maybe TmState -tmOracle tm_state eqs = foldlM solveSimpleEq tm_state eqs +tmOracle :: TmState -> [ComplexEq] -> Maybe TmState +tmOracle tm_state eqs = foldlM solveOneEq tm_state eqs -- | Type of a PmLit pmLitType :: PmLit -> Type -- should be in PmExpr but gives cyclic imports :( @@ -241,215 +239,4 @@ is the following: truePmExpr, falsePmExpr or (e1' ~ e2') in case it is uncertain. Note that it is not e but rather e', since it may perform some simplifications deeper. - -Note [Undecidable Equality on Overloaded Literals] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Overloaded literals do not offer equality like constructors do. A literal @lit@ -is used to actually represent @from lit@. For example, we can have the -following: - - instance Num Bool where - ... - fromInteger 0 = False - fromInteger _ = True - - g :: Bool -> Bool - g 4 = ... -- clause A - g 2 = ... -- clause B - -Both clauses A and B will match argunent @True@ so we have an overlap. Yet, we -cannot detect this unless we unfold the @fromInteger@ function. So @eqPmLit@ -from deSugar/PmExpr.hs returns @Nothing@ in this case. This complexes things a -lot. Consider the following (similar to test ds022 in deSugar/should_compile): - - f l1 l2 = ... -- clause A - f l3 l4 = ... -- clause B - f l1 l2 = ... -- clause C - -Assuming that the @from@ function is side-effect-free (and total), clauses C -and D are redundant, independently of the implementation of @from@: - - l1 == l2 ===> from l1 == from l2 - l1 /= l2 =/=> from l1 /= from l2 - -Now consider what we should generate for @f@ (covered and uncovered only): - -U0 = { [x y |> {}] } - -Clause A: l1 l2 -------------------------------------------------------------------------------- -CA = { [l1 l2 |> { x ~ l1, y ~ l2 }] } - -UA = { [x y |> { False ~ (x ~ l1) }] - , [l1 y |> { x ~ l1, False ~ (y ~ l2) }] } - -Clause B: l3 l4 -------------------------------------------------------------------------------- - -CB = { [l3 l4 |> { False ~ (x ~ l1), x ~ l3, y ~ l4}] - ..reduces to: False ~ (l3 ~ l1), y ~ l4 - - , [l1 l4 |> { x ~ l1, False ~ (y ~ l2), l3 ~ z, z ~ l1, y ~ l4}] } - ..reduces to: x ~ l1, False ~ (l4 ~ l2), l1 ~ l3 - -UB = { [x y |> { False ~ (x ~ l1), False ~ (x ~ l3) }] - , [l3 y |> { False ~ (x ~ l1), x ~ l3, False ~ (y ~ l4) }] - ..reduces to: False ~ (l1 ~ l3), False ~ (y ~ l4) - , [l1 y |> { x ~ l1, False ~ (y ~ l2), False ~ (l1 ~ l3) }] - , [l1 y |> { x ~ l1, False ~ (y ~ l2), l1 ~ l3, False ~ (y ~ l4) }] } - -Clause C: l1 l2 -------------------------------------------------------------------------------- - -CC = { [l1 l2 |> { False ~ (x ~ l1), False ~ (x ~ l3), x ~ l1, y ~ l2 }] - ..reduces to: False ~ (l1 ~ l1), False ~ (l1 ~ l3), x ~ l1 - False ~ True, False ~ (l1 ~ l3), x ~ l1 - INCONSISTENT - , [l3 l2 |> { False ~ (l1 ~ l3), False ~ (y ~ l4), l1 ~ l3, y ~ l2 }] - ..reduces to: False ~ (l1 ~ l3), False ~ (l2 ~ l4), l1 ~ l3 - , [l1 l2 |> { x ~ l1, False ~ (y ~ l2), False ~ (l1 ~ l3), y ~ l2 }] - ..reduces to: x ~ l1, False ~ (l2 ~ l2), False ~ (l1 ~ l3) - x ~ l1, False ~ True, False ~ (l1 ~ l3) - INCONSISTENT - , [l1 l2 |> { x ~ l1,False ~ (y ~ l2),l1 ~ l3,False ~ (y ~ l4),y ~ l2 }] } - ..reduces to: x ~ l1, False ~ (l2 ~ l2), l1 ~ l3, False ~ (l2 ~ l4) - x ~ l1, False ~ True, l1 ~ l3, False ~ (l2 ~ l4) - INCONSISTENT -------------------------------------------------------------------------------- - -PROBLEM 1: -~~~~~~~~~~ -Now the first problem shows itself: Our basic unification-based term oracle -cannot detect that constraint: - - False ~ (l1 ~ l3), False ~ (l2 ~ l4), l1 ~ l3 - -is inconsistent. That's what function @tryLitEqs@ (in comments) tries to do: -use the equality l1 ~ l3 to replace False ~ (l1 ~ l3) with False ~ (l1 ~ l1) -and expose the inconsistency. - -PROBLEM 2: -~~~~~~~~~~ -Let's turn back to UB and assume we had only clauses A and B. UB is as follows: - - UB = { [x y |> { False ~ (x ~ l1), False ~ (x ~ l3) }] - , [l3 y |> { False ~ (l1 ~ l3), False ~ (y ~ l4) }] - , [l1 y |> { x ~ l1, False ~ (y ~ l2), False ~ (l1 ~ l3) }] - , [l1 y |> { x ~ l1, False ~ (y ~ l2), l1 ~ l3, False ~ (y ~ l4) }] } - -So we would get: - - Pattern match(es) are non-exhaustive - In an equation for f: - Patterns not matched: - x y where x not one of {l1, l3} - l3 y where y not one of {l4} - l1 y where y not one of {l2} - l1 y where y not one of {l2, l4} -- (*) - -What about the last warning? It holds UNDER THE ASSUMPTION that l1 == l2. It is -quite unintuitive for the user so at the moment we drop such cases (see -function @pruneVSABound@ in deSugar/Check.hs). I (gkaracha) would prefer to -issue a warning like: - - Pattern match(es) are non-exhaustive - In an equation for f: - Patterns not matched: - ... - l1 y where y not one of {l2, l4} - under the assumption that l1 ~ l3 - -It may be more complex but I would prefer to play on the safe side and (safely) -issue all warnings and leave it up to the user to decide whether the assumption -holds or not. - -At the moment, we use @containsEqLits@ and consider all constraints that -include literal equalities inconsistent. We could achieve the same by replacing -this clause of @eqPmLit@: - - eqPmLit (PmOLit b1 l1) (PmOLit b2 l2) - | b1 == b2 && l1 == l2 = Just True - | otherwise = Nothing - -with this: - - eqPmLit (PmOLit b1 l1) (PmOLit b2 l2) - | b1 == b2 && l1 == l2 = Just True - | otherwise = Just False - -which approximates on the unsafe side. Hopefully, literals always need a -catch-all case to be considered exhaustive so in practice it makes small -difference. I hate this but it gives the warnings the users are used to. -} - -{- Not Enabled at the moment - --- | Check whether overloaded literal constraints exist in the state and if --- they can be used to detect further inconsistencies. -tryLitEqs :: TmState -> Maybe Bool -tryLitEqs tm_state@(stb,_) = do - ans <- exploitLitEqs (Just tm_state) - -- Three possible results: - -- Nothing : Inconsistency found. - -- Just True : Literal constraints exist but no inconsistency found. - -- Just False : There are no literal constraints in the state. - return (isJust $ exists isLitEq_mb stb) - --- | Exploit overloaded literal constraints --- @lit1 ~ lit2@ to improve the term oracle's expressivity. -exploitLitEqs :: Maybe TmState -> Maybe TmState -exploitLitEqs tm_state = case tm_state of - -- The oracle did not find any inconsistency. Try and exploit - -- residual literal equalities for a more precise result. - Just st@(standby, (unhandled, env)) -> - case exists isLitEq_mb standby of - -- Such an equality exists. This means that we are under the assumption - -- that two overloaded literals reduce to the same value (for all we know - -- they do). Replace the one with the other in the rest residual - -- constraints and run the solver once more, looking for an inconsistency. - Just ((l1, l2), rest) -> - let new_env = Map.map (replaceLit l1 l2) env - new_stb = map (replaceLitSimplifyComplexEq l1 l2) rest - in exploitLitEqs - (foldlM solveComplexEq ([], (unhandled, new_env)) new_stb) - -- We don't have anything. Just return what you had.. - Nothing -> Just st - -- The oracle has already found an inconsistency. - -- No need to search further. - Nothing -> Nothing - where - replaceLitSimplifyComplexEq :: PmLit -> PmLit -> ComplexEq -> ComplexEq - replaceLitSimplifyComplexEq l1 l2 (e1,e2) = - simplifyComplexEq (replaceLit l1 l2 e1, replaceLit l1 l2 e2) - --- | Replace a literal with another in an expression --- See Note [Undecidable Equality on Overloaded Literals] -replaceLit :: PmLit -> PmLit -> PmExpr -> PmExpr -replaceLit l1 l2 e = case e of - PmExprVar {} -> e - PmExprCon c es -> PmExprCon c (map (replaceLit l1 l2) es) - PmExprLit l -> case eqPmLit l l1 of - Just True -> PmExprLit l2 - Just False -> e - Nothing -> e - PmExprEq e1 e2 -> PmExprEq (replaceLit l1 l2 e1) (replaceLit l1 l2 e2) - PmExprOther {} -> e -- do nothing --} - --- | Check whether the term oracle state --- contains any equalities between literals. -containsEqLits :: TmState -> Bool -containsEqLits (stb, _) = isJust (exists isLitEq_mb stb) - -exists :: (a -> Maybe b) -> [a] -> Maybe (b, [a]) -exists _ [] = Nothing -exists p (x:xs) = case p x of - Just y -> Just (y, xs) - Nothing -> do - (y, ys) <- exists p xs - return (y, x:ys) - --- | Check whether a complex equality refers to literals only -isLitEq_mb :: ComplexEq -> Maybe (PmLit, PmLit) -isLitEq_mb (PmExprLit l1, PmExprLit l2) = Just (l1, l2) -isLitEq_mb _other_eq = Nothing |