Infer that the right-hand side of claims is defined #2136
Conversation
kore/src/Kore/Step/Rule/Simplify.hs
Outdated
| lhs' = simplified { Pattern.substitution = mempty } | ||
| rhs = ClaimPattern.right claimPattern | ||
| simplifiedLhs <- simplify lhs | ||
| simplifiedRhs <- OrPattern.filterOr <$> traverse simplify rhs |
There was a problem hiding this comment.
@ana-pantilie Aren't we already simplify the right-hand side of the claim somewhere else?
There was a problem hiding this comment.
Yes, in the simplify transition of the strategy: https://github.com/kframework/kore/blob/c28200738e0a5e8c2b9aaf6a6046b996f68082e3/kore/src/Kore/Strategies/Goal.hs#L838
kore/src/Kore/Step/Rule/Simplify.hs
Outdated
| simplifiedRhs <- OrPattern.filterOr <$> traverse simplify rhs | ||
| let substitution = | ||
| Pattern.substitution simplifiedLhs | ||
| <> foldMap Pattern.substitution (MultiOr.getMultiOr simplifiedRhs) |
There was a problem hiding this comment.
We cannot add the substitution from the right-hand side to the global substitution. We can't apply it to the left-hand side, and it isn't right to drop it from the right-hand side (below) either.
There was a problem hiding this comment.
Initially I didn't do that, but I tried it out of other ideas
| \ceil{SortGeneratedTopCell{}, SortGeneratedTopCell{}}( | ||
| /* Fn Spa */ | ||
| Lbl'-LT-'generatedTop'-GT-'{}( |
There was a problem hiding this comment.
I know this hasn't been simplified because Lbl'-LT-'generatedTop'-GT-'{} is a functional constructor.
kore/src/Kore/Step/Rule/Simplify.hs
Outdated
| let simplifiedRhs = OrPattern.filterOr (OrPattern.map Pattern.requireDefined rhs) | ||
| let substitution = Pattern.substitution simplifiedLhs | ||
| lhs' = simplifiedLhs { Pattern.substitution = mempty } | ||
| claimPattern | ||
| { ClaimPattern.left = lhs' | ||
| , ClaimPattern.right = simplifiedRhs |
There was a problem hiding this comment.
This code will only be called once, at start-up. Please move it to Kore.Reachability.Claim.simplify', where we infer that the left-hand side of the claim is defined, and where we simplify both sides of the claim. The \ceil patterns must be simplified under the same conditions as the rest of the right-hand side.
Fixes #2110
Reviewer checklist
stack test --coveragestack haddock