Skip to content
Snippets Groups Projects
Commit d20ed249 authored by Sebastian Graf's avatar Sebastian Graf
Browse files

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.
parent a5fdd185
No related branches found
No related tags found
No related merge requests found
Pipeline #5853 canceled
......@@ -210,7 +210,7 @@ simplifyEqExpr e1 e2 = case (e1, e2) of
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)
| any isFalsePmExpr tss -> (falsePmExpr, True)
| otherwise -> (worst_case, or bs1 || or bs2)
| otherwise -> (worst_case, False)
| otherwise -> (falsePmExpr, True)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment