Skip to content

Commit

Permalink
Fix compilation of superset operations (dafny-lang#1368)
Browse files Browse the repository at this point in the history
  • Loading branch information
sorawee authored Aug 23, 2021
1 parent 7f31201 commit 6a6158b
Show file tree
Hide file tree
Showing 3 changed files with 21 additions and 0 deletions.
1 change: 1 addition & 0 deletions Source/Dafny/Compiler.cs
Original file line number Diff line number Diff line change
Expand Up @@ -1070,6 +1070,7 @@ protected virtual void CompileBinOp(BinaryExpr.ResolvedOpcode op,
e1, e0, tok, resultType,
out opString, out preOpString, out postOpString, out callString, out staticCallString, out reverseArguments, out truncateResult, out convertE1_to_int,
errorWr);
reverseArguments = !reverseArguments;
} else if (negatedOp != BinaryExpr.ResolvedOpcode.Add) { // remember from above that Add stands for "there is no negated op"
CompileBinOp(negatedOp,
e0, e1, tok, resultType,
Expand Down
4 changes: 4 additions & 0 deletions Test/comp/Collections.dfy
Original file line number Diff line number Diff line change
Expand Up @@ -36,6 +36,8 @@ method Sets() {
print " disjoint: ", a !! b, " ", b !! c, "\n";
print " subset: ", a <= b, " ", b <= c, " ", c <= c, "\n";
print " proper subset: ", a < b, " ", b < c, " ", c < c, "\n";
print " superset: ", a >= b, " ", b >= a, " ", c >= c, "\n";
print " proper superset: ", a > b, " ", b > a, " ", c > c, "\n";
print " membership: ", 17 in a, " ", 17 in b, " ", 17 in c, "\n";

var cl := new Class;
Expand Down Expand Up @@ -75,6 +77,8 @@ method MultiSets() {
print " disjoint: ", a !! b, " ", b !! c, "\n";
print " subset: ", a <= b, " ", b <= c, " ", c <= c, "\n";
print " proper subset: ", a < b, " ", b < c, " ", c < c, "\n";
print " superset: ", a >= b, " ", b >= a, " ", c >= c, "\n";
print " proper superset: ", a > b, " ", b > a, " ", c > c, "\n";
print " membership: ", 17 in a, " ", 17 in b, " ", 17 in c, "\n";
print " update: ", a[17 := 2], " ", b[17 := 2], " ", c[17 := 2], "\n";
print " multiplicity: ", a[17], " ", b[17], " ", c[17], "\n";
Expand Down
16 changes: 16 additions & 0 deletions Test/comp/Collections.dfy.expect
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,8 @@ Sets: {} {17, 82} {12, 17}
disjoint: true false
subset: true false true
proper subset: true false false
superset: false true true
proper superset: false true false
membership: false true true
eq covariance: 1 true true
false true
Expand All @@ -23,6 +25,8 @@ Multisets: multiset{} multiset{17, 17, 82, 82} multiset{12, 17}
disjoint: true false
subset: true false true
proper subset: true false false
superset: false true true
proper superset: false true false
membership: false true true
update: multiset{17, 17} multiset{17, 17, 82, 82} multiset{12, 17, 17}
multiplicity: 0 2 1
Expand Down Expand Up @@ -125,6 +129,8 @@ Sets: {} {17, 82} {12, 17}
disjoint: true false
subset: true false true
proper subset: true false false
superset: false true true
proper superset: false true false
membership: false true true
eq covariance: 1 true true
false true
Expand All @@ -138,6 +144,8 @@ Multisets: multiset{} multiset{17, 17, 82, 82} multiset{12, 17}
disjoint: true false
subset: true false true
proper subset: true false false
superset: false true true
proper superset: false true false
membership: false true true
update: multiset{17, 17} multiset{17, 17, 82, 82} multiset{12, 17, 17}
multiplicity: 0 2 1
Expand Down Expand Up @@ -240,6 +248,8 @@ Sets: {} {17, 82} {12, 17}
disjoint: true false
subset: true false true
proper subset: true false false
superset: false true true
proper superset: false true false
membership: false true true
eq covariance: 1 true true
false true
Expand All @@ -253,6 +263,8 @@ Multisets: multiset{} multiset{17, 17, 82, 82} multiset{12, 17}
disjoint: true false
subset: true false true
proper subset: true false false
superset: false true true
proper superset: false true false
membership: false true true
update: multiset{17, 17} multiset{17, 17, 82, 82} multiset{12, 17, 17}
multiplicity: 0 2 1
Expand Down Expand Up @@ -355,6 +367,8 @@ Sets: {} {17, 82} {17, 12}
disjoint: true false
subset: true false true
proper subset: true false false
superset: false true true
proper superset: false true false
membership: false true true
eq covariance: 1 true true
false true
Expand All @@ -368,6 +382,8 @@ Multisets: multiset{} multiset{17, 17, 82, 82} multiset{17, 12}
disjoint: true false
subset: true false true
proper subset: true false false
superset: false true true
proper superset: false true false
membership: false true true
update: multiset{17, 17} multiset{17, 17, 82, 82} multiset{17, 17, 12}
multiplicity: 0 2 1
Expand Down

0 comments on commit 6a6158b

Please sign in to comment.