Haskell symbolic update rule #1662
Conversation
| @@ -410,6 +410,9 @@ module MAP-KORE-SYMBOLIC [kore,symbolic] | |||
|
|
|||
| rule #Ceil(@M:Map [@K:KItem]) => {(@K in_keys(@M)) #Equals true} #And #Ceil(@M) #And #Ceil(@K) [anywhere, simplification] | |||
|
|
|||
| rule (K |-> _ M:Map) [ K <- V ] => (K |-> V M:Map) [simplification] | |||
| rule (M:Map) [ K <- V ] => (K |-> V M:Map) [simplification] | |||
There was a problem hiding this comment.
| rule (M:Map) [ K <- V ] => (K |-> V M:Map) [simplification] | |
| rule (M:Map) [ K <- V ] => (K |-> V M:Map) requires notBool( K in_keys M ) [simplification] |
| <k> | ||
| assignment ( (MAP:Map X:MyId |-> 1) [ Y:MyId <- 2 ] [ Z:MyId <- 3 ] ) => | ||
| assignmentResult ( MAP Z |-> 3 ) | ||
| </k> requires Y ==K X andBool Z ==K Y andBool Z ==K X |
There was a problem hiding this comment.
This is redundant. Did gen-tests.sh generate the spec this way?
| </k> requires Y ==K X andBool Z ==K Y andBool Z ==K X | |
| </k> requires Y ==K X andBool Z ==K Y |
There was a problem hiding this comment.
@ttuegel Yes. https://github.com/kframework/k/blob/master/k-distribution/tests/regression-new/map-symbolic-tests/assignment-17-spec.k#L9
The only thing I did with this tests was taking the part from the .out file and put it as the rhs.
| assignment ( (MAP:Map X:MyId |-> 1) [ Y:MyId <- 2 ] [ Z:MyId <- 3 ] ) => | ||
| assignmentResult ( MAP Z |-> 3 ) | ||
| </k> | ||
| requires Y ==K X andBool Z ==K Y andBool Z ==K X andBool notBool X in_keys(MAP) |
There was a problem hiding this comment.
This is redundant; it is implied by the left-hand side of the claim:
| requires Y ==K X andBool Z ==K Y andBool Z ==K X andBool notBool X in_keys(MAP) | |
| requires Y ==K X andBool Z ==K Y andBool Z ==K X |
|
|
||
| claim | ||
| <k> | ||
| assignment ( (MAP:Map X:MyId |-> 1) [ Y:MyId <- 2 ] [ Z:MyId <- 3 ] ) => |
There was a problem hiding this comment.
This claim doesn't test anything.
There was a problem hiding this comment.
To provide some context, these tests were written how they were (with invalid RHSs), so that we would get the actual output of the backend (rather than having the backend try to prove that the RHS actually is semantically equal to the resulting final state). That way we could make sure that both (i) the simplifications we want were happenning, and (ii) the simplifications we don't want were not happenning.
This was to not trust the java backend map equality checks basically, but I think it makes sense to update the tests for the haskell backend because we trust it's routines more.
| module ASSIGNMENT-21-SPEC | ||
| imports MAP-TESTS | ||
|
|
||
| claim |
There was a problem hiding this comment.
This claim doesn't test anything.
| module ASSIGNMENT-22-SPEC | ||
| imports MAP-TESTS | ||
|
|
||
| claim |
There was a problem hiding this comment.
This claim doesn't test anything.
| module ASSIGNMENT-24-SPEC | ||
| imports MAP-TESTS | ||
|
|
||
| claim |
There was a problem hiding this comment.
This claim doesn't test anything.
| module ASSIGNMENT-25-SPEC | ||
| imports MAP-TESTS | ||
|
|
||
| claim |
There was a problem hiding this comment.
This claim doesn't test anything.
|
@andreiburdusa I pushed some changes to this branch. I think you are right that the output from proving each spec should be |
|
I didn't add |
|
@andreiburdusa We should update those tests to use existentially-quantified variables: |
There was a problem hiding this comment.
This looks OK to me. @ana-pantilie please merge this into your pull request and proceed with fixing the right-hand sides of claims, as we discussed.
| //Symbolic in_keys | ||
| rule K in_keys(M [ K <- undef ]) => false [simplification] |
There was a problem hiding this comment.
| //Symbolic in_keys | |
| rule K in_keys(M [ K <- undef ]) => false [simplification] | |
| // Symbolic in_keys | |
| rule K in_keys(M [ K <- undef ]) => false [simplification] |
|
This was merged into #1661. |
Fixes runtimeverification/haskell-backend#2248