diff options
| author | Sebastian Graf <sebastian.graf@kit.edu> | 2019-05-20 17:14:28 +0200 |
|---|---|---|
| committer | Sebastian Graf <sgraf1337@gmail.com> | 2019-05-21 05:20:23 -0400 |
| commit | edf6087f6c79c12ba4518231492c7d42fc6cc0f0 (patch) | |
| tree | e7a4c6f50e2fd1a9af25c3408ce67e23f51d0e69 | |
| parent | b46efa2bbf86cf0673d0d6dfd5c40b2b0db5f9ff (diff) | |
| download | haskell-wip/pmcheck-eqs.tar.gz | |
Make TmOracle reduce nullary constructor equalitieswip/pmcheck-eqs
Previously, `simplifyEqExpr` would just give up on constructor
applications when no argument to either constructor was simplified.
That's unfortunate as all arguments might be equal anyway! A special
case of this is nullary constructors. Currently, the TmOracle would fail
to solve a term equality `False ~ (True = True)` because it can't make
any progress on any of `True`s arguments.
Instead we now try to properly simplify the term equality even when no
simplification of constructor arguments was achieved.
| -rw-r--r-- | compiler/deSugar/TmOracle.hs | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/compiler/deSugar/TmOracle.hs b/compiler/deSugar/TmOracle.hs index 87e5f0a268..ebe59f9d77 100644 --- a/compiler/deSugar/TmOracle.hs +++ b/compiler/deSugar/TmOracle.hs @@ -208,10 +208,9 @@ simplifyEqExpr e1 e2 = case (e1, e2) of (ts2', bs2) = mapAndUnzip simplifyPmExpr ts2 (tss, _bss) = zipWithAndUnzip simplifyEqExpr ts1' ts2' worst_case = PmExprEq (PmExprCon c1 ts1') (PmExprCon c2 ts2') - in if | not (or bs1 || or bs2) -> (worst_case, False) -- no progress - | all isTruePmExpr tss -> (truePmExpr, True) + in if | all isTruePmExpr tss -> (truePmExpr, True) | any isFalsePmExpr tss -> (falsePmExpr, True) - | otherwise -> (worst_case, False) + | otherwise -> (worst_case, or bs1 || or bs2) | otherwise -> (falsePmExpr, True) -- We cannot do anything about the rest.. |