Create a Kore.Reachability context #2141
Conversation
The data type does not represent the state of the entire proof, but only the state of a single claim.
There are three types which represent reachability logic claims (AllPathClaim, OnePathClaim, and SomeClaim) so it did not make sense to call out SomeClaim as _the_ ReachabilityClaim. The prefix Some- matches the typical naming convention of collecting multiple subtypes in a sum type.
ttuegel
force-pushed
the
refactor--reachability
branch
from
97cc67b to
58911fd
Compare
|
|
||
| {- | Sum type to distinguish rewrite axioms (used for stepping) | ||
| from function axioms (used for functional simplification). | ||
| --} |
There was a problem hiding this comment.
Should this comment be updated?
There was a problem hiding this comment.
In fact, I think this type can go away entirely, so this pull request will be held up a little longer while I try to do that. Actually, removing the type isn't so hard, but there are some tests which should be salvaged.
There was a problem hiding this comment.
I added my clean-up commits. Feel free to revert them if you think there's something wrong about them.
-
There used to be two test modules for verifying one path and all path claims, and another module for their sum type. This used to make sense because the verifying functions were polymorphic and we could test the functions with the specific claim type directly. Sometime in the past, these functions were changed to take the sum type. I removed the two modules, and added any tests which were missing to
Prove.hs. I also enabled a couple of tests for claims with disjunctions on the RHS. -
I moved a test module from
Test.Kore.StrategiestoTest.Kore.Reachabilityso that the directory hierarchy is similar to the one in project.
Co-authored-by: ana-pantilie <45069775+ana-pantilie@users.noreply.github.com>
ttuegel
force-pushed
the
refactor--reachability
branch
from
694399c to
3b33fd0
Compare
3 participants
This is part 1 of my clean-up after #2080. It collects most of the things related to reachability logic under the
Kore.Reachabilitytree, in an effort to establish a Bounded Context.Reviewer checklist
stack test --coveragestack haddock