Change the representation of reachability claims, part 2 #2025
Conversation
The specs are restated so that the right-hand side does not unify with the initial left-hand side.
This reverts commit 6d605fcd8e90549253aae40309bcdb51e6172c9b.
kore/src/Kore/Step/ClaimPattern.hs
Outdated
| instance From OnePathRule Attribute.Trusted where | ||
| from = Attribute.trusted . attributes . getOnePathRule | ||
|
|
||
| instance From OnePathRule (TermLike VariableName) where |
There was a problem hiding this comment.
It's the entire claim as a term-like. This is related to the From rule (TermLike VariableName) constraint used when logging (we need this otherwise we wouldn't be able to print the rule in the log). I think that discussion got lost amidst everything else. The first thing that came to mind was to use a newtype over TermLike VariableName so that it's clearer this is the whole rule represented as a term. What do you think?
There was a problem hiding this comment.
Yes, we could have something like
newtype AxiomPattern = AxiomPattern (TermLike VariableName)
kore/src/Kore/Step/ClaimPattern.hs
Outdated
| { left = | ||
| Pattern.mapVariables resetConfigVariable left | ||
| , right = | ||
| Pattern.mapVariables resetConfigVariable <$> right |
There was a problem hiding this comment.
Should this be MultiOr.map instead of fmap?
There was a problem hiding this comment.
That's right. Thanks for spotting this!
There was a problem hiding this comment.
Is it safe to remove the Functor instance of that type yet?
There was a problem hiding this comment.
There are still places where it's used. I was thinking it would be cleaner to do this as another task.
There was a problem hiding this comment.
Sounds good! I can take care of that; there were several clean-up items that I wanted to do, that should be postponed until #2080 is merged.
…tion-of-claims-part2
3 participants
Part of #1278
After #2007
Reviewer checklist
stack test --coveragestack haddock