From edf6087f6c79c12ba4518231492c7d42fc6cc0f0 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Mon, 20 May 2019 17:14:28 +0200 Subject: Make TmOracle reduce nullary constructor equalities 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. --- compiler/deSugar/TmOracle.hs | 5 ++--- 1 file 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.. -- cgit v1.2.1