Commit ae4398d6 authored by Georgios Karachalias's avatar Georgios Karachalias
Browse files

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!).
parent 40fc3536
......@@ -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
......
......@@ -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) []
......@@ -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)
isLit