summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Jason Koenig <unknown>2011-07-11 15:33:45 -0700
committerGravatar Jason Koenig <unknown>2011-07-11 15:33:45 -0700
commitf72015819c90a23b150b1d70147eb51c51e2d5ed (patch)
treea07b8d9094f028d5ea071e46dbaf818b5bb8d5fe
parentd5bf8e1275ae1cc79ddb7048d2015160bdf2bddc (diff)
Partial implementation of multisets.
Diffstat
-rw-r--r--Binaries/DafnyPrelude.bpl103
-rw-r--r--Source/Dafny/Dafny.atg15
-rw-r--r--Source/Dafny/DafnyAst.cs41
-rw-r--r--Source/Dafny/Parser.cs670
-rw-r--r--Source/Dafny/Printer.cs5
-rw-r--r--Source/Dafny/Resolver.cs50
-rw-r--r--Source/Dafny/Scanner.cs144
-rw-r--r--Source/Dafny/Translator.cs214
8 files changed, 821 insertions, 421 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index dc152185..1a8bb027 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -84,6 +84,109 @@ function Set#Choose<T>(Set T, TickType): T;
axiom (forall<T> a: Set T, tick: TickType :: { Set#Choose(a, tick) }
a != Set#Empty() ==> a[Set#Choose(a, tick)]);
+
+// ---------------------------------------------------------------
+// -- Axiomatization of multisets --------------------------------
+// ---------------------------------------------------------------
+
+function Math#min(a: int, b: int): int;
+axiom (forall a: int, b: int :: { Math#min(a, b) } a <= b <==> Math#min(a, b) == a);
+axiom (forall a: int, b: int :: { Math#min(a, b) } b <= a <==> Math#min(a, b) == b);
+axiom (forall a: int, b: int :: { Math#min(a, b) } Math#min(a, b) == a || Math#min(a, b) == b);
+
+function Math#clip(a: int): int;
+axiom (forall a: int :: { Math#clip(a) } 0 <= a ==> Math#clip(a) == a);
+axiom (forall a: int :: { Math#clip(a) } a < 0 ==> Math#clip(a) == 0);
+
+type MultiSet T = [T]int;
+
+// ints are non-negative
+axiom (forall<T> o: T, ms: MultiSet T :: { ms[o] } 0 <= ms[o] );
+
+function MultiSet#Empty<T>(): MultiSet T;
+axiom (forall<T> o: T :: { MultiSet#Empty()[o] } MultiSet#Empty()[o] == 0);
+
+function MultiSet#Singleton<T>(T): MultiSet T;
+axiom (forall<T> r: T :: { MultiSet#Singleton(r) } MultiSet#Singleton(r)[r] == 1);
+axiom (forall<T> r: T, o: T :: { MultiSet#Singleton(r)[o] } (MultiSet#Singleton(r)[o] == 1 <==> r == o) &&
+ (MultiSet#Singleton(r)[o] == 0 <==> r != o));
+
+function MultiSet#UnionOne<T>(MultiSet T, T): MultiSet T;
+// pure containment axiom (in the original multiset or is the added element)
+axiom (forall<T> a: MultiSet T, x: T, o: T :: { MultiSet#UnionOne(a,x)[o] }
+ 0 < MultiSet#UnionOne(a,x)[o] <==> o == x || 0 < a[o]);
+// union-ing increases count by one
+axiom (forall<T> a: MultiSet T, x: T :: { MultiSet#UnionOne(a, x) }
+ MultiSet#UnionOne(a, x)[x] == a[x] + 1);
+// non-decreasing
+axiom (forall<T> a: MultiSet T, x: T, y: T :: { MultiSet#UnionOne(a, x), a[y] }
+ 0 < a[y] ==> 0 < MultiSet#UnionOne(a, x)[y]);
+// other elements unchanged
+axiom (forall<T> a: MultiSet T, x: T, y: T :: { MultiSet#UnionOne(a, x), a[y] }
+ x != y ==> a[y] == MultiSet#UnionOne(a, x)[y]);
+
+function MultiSet#Union<T>(MultiSet T, MultiSet T): MultiSet T;
+// union-ing is the sum of the contents
+axiom (forall<T> a: MultiSet T, b: MultiSet T, o: T :: { MultiSet#Union(a,b)[o] }
+ MultiSet#Union(a,b)[o] == a[o] + b[o]);
+
+// two containment axioms
+axiom (forall<T> a, b: MultiSet T, y: T :: { MultiSet#Union(a, b), a[y] }
+ 0 < a[y] ==> 0 < MultiSet#Union(a, b)[y]);
+axiom (forall<T> a, b: MultiSet T, y: T :: { MultiSet#Union(a, b), b[y] }
+ 0 < b[y] ==> 0 < MultiSet#Union(a, b)[y]);
+
+// symmetry axiom
+axiom (forall<T> a, b: MultiSet T :: { MultiSet#Union(a, b) }
+ MultiSet#Disjoint(a, b) ==>
+ MultiSet#Difference(MultiSet#Union(a, b), a) == b &&
+ MultiSet#Difference(MultiSet#Union(a, b), b) == a);
+
+function MultiSet#Intersection<T>(MultiSet T, MultiSet T): MultiSet T;
+axiom (forall<T> a: MultiSet T, b: MultiSet T, o: T :: { MultiSet#Intersection(a,b)[o] }
+ MultiSet#Intersection(a,b)[o] == Math#min(a[o], b[o]));
+
+// left and right pseudo-idempotence
+axiom (forall<T> a, b: MultiSet T :: { MultiSet#Intersection(MultiSet#Intersection(a, b), b) }
+ MultiSet#Intersection(MultiSet#Intersection(a, b), b) == MultiSet#Intersection(a, b));
+axiom (forall<T> a, b: MultiSet T :: { MultiSet#Intersection(a, MultiSet#Intersection(a, b)) }
+ MultiSet#Intersection(a, MultiSet#Intersection(a, b)) == MultiSet#Intersection(a, b));
+
+// multiset difference, a - b. clip() makes it positive.
+function MultiSet#Difference<T>(MultiSet T, MultiSet T): MultiSet T;
+axiom (forall<T> a: MultiSet T, b: MultiSet T, o: T :: { MultiSet#Difference(a,b)[o] }
+ MultiSet#Difference(a,b)[o] == Math#clip(a[o] - b[o]));
+axiom (forall<T> a, b: MultiSet T, y: T :: { MultiSet#Difference(a, b), b[y], a[y] }
+ a[y] <= b[y] ==> MultiSet#Difference(a, b)[y] == 0 );
+
+// multiset subset means a must have at most as many of each element as b
+function MultiSet#Subset<T>(MultiSet T, MultiSet T): bool;
+axiom(forall<T> a: MultiSet T, b: MultiSet T :: { MultiSet#Subset(a,b) }
+ MultiSet#Subset(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] <= b[o]));
+
+function MultiSet#Equal<T>(MultiSet T, MultiSet T): bool;
+axiom(forall<T> a: MultiSet T, b: MultiSet T :: { MultiSet#Equal(a,b) }
+ MultiSet#Equal(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] == b[o]));
+// extensionality axiom for multisets
+axiom(forall<T> a: MultiSet T, b: MultiSet T :: { MultiSet#Equal(a,b) }
+ MultiSet#Equal(a,b) ==> a == b);
+
+function MultiSet#Disjoint<T>(MultiSet T, MultiSet T): bool;
+axiom (forall<T> a: MultiSet T, b: MultiSet T :: { MultiSet#Disjoint(a,b) }
+ MultiSet#Disjoint(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] == 0 || b[o] == 0));
+
+// conversion to a multiset. each element in the original set has duplicity 1.
+function MultiSet#FromSet<T>(Set T): MultiSet T;
+axiom (forall<T> s: Set T, a: T :: { MultiSet#FromSet(s)[a] }
+ MultiSet#FromSet(s)[a] == 0 <==> !s[a] &&
+ MultiSet#FromSet(s)[a] == 1 <==> s[a]);
+
+// avoiding this for now.
+//function Set#Choose<T>(Set T, TickType): T;
+//axiom (forall<T> a: Set T, tick: TickType :: { Set#Choose(a, tick) }
+// a != Set#Empty() ==> a[Set#Choose(a, tick)]);
+
+
// ---------------------------------------------------------------
// -- Axiomatization of sequences --------------------------------
// ---------------------------------------------------------------
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index f6e40722..3f6c64b8 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -518,6 +518,12 @@ TypeAndToken<out IToken/*!*/ tok, out Type/*!*/ ty>
}
ty = new SetType(gt[0]);
.)
+ | "multiset" (. tok = t; gt = new List<Type/*!*/>(); .)
+ GenericInstantiation<gt> (. if (gt.Count != 1) {
+ SemErr("multiset type expects exactly one type argument");
+ }
+ ty = new MultiSetType(gt[0]);
+ .)
| "seq" (. tok = t; gt = new List<Type/*!*/>(); .)
GenericInstantiation<gt> (. if (gt.Count != 1) {
@@ -1251,11 +1257,14 @@ ConstAtomExpression<out Expression/*!*/ e>
DisplayExpr<out Expression e>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
- IToken/*!*/ x; List<Expression/*!*/>/*!*/ elements;
+ IToken/*!*/ x = null; List<Expression/*!*/>/*!*/ elements;
e = dummyExpr;
+ bool isMulti = false;
.)
- ( "{" (. x = t; elements = new List<Expression/*!*/>(); .)
- [ Expressions<elements> ] (. e = new SetDisplayExpr(x, elements); .)
+ ( [ "multi" (. x = t; isMulti = true; .) ]
+ "{" (. if (!isMulti) x = t; elements = new List<Expression/*!*/>(); .)
+ [ Expressions<elements> ] (. if (isMulti) e = new MultiSetDisplayExpr(x, elements);
+ else e = new SetDisplayExpr(x, elements);.)
"}"
| "[" (. x = t; elements = new List<Expression/*!*/>(); .)
[ Expressions<elements> ] (. e = new SeqDisplayExpr(x, elements); .)
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 4868be10..cf1a8630 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -256,7 +256,7 @@ namespace Microsoft.Dafny {
this.Arg = arg;
}
}
-
+
public class SetType : CollectionType {
public SetType(Type arg) : base(arg) {
Contract.Requires(arg != null);
@@ -269,6 +269,19 @@ namespace Microsoft.Dafny {
}
}
+ public class MultiSetType : CollectionType
+ {
+ public MultiSetType(Type arg) : base(arg) {
+ Contract.Requires(arg != null);
+ }
+ [Pure]
+ public override string ToString() {
+ Contract.Ensures(Contract.Result<string>() != null);
+ Contract.Assume(cce.IsPeerConsistent(Arg));
+ return "multiset<" + base.Arg + ">";
+ }
+ }
+
public class SeqType : CollectionType {
public SeqType(Type arg) : base(arg) {
Contract.Requires(arg != null);
@@ -487,9 +500,9 @@ namespace Microsoft.Dafny {
/// <summary>
/// This proxy stands for either:
- /// int or set or seq
+ /// int or set or multiset or seq
/// if AllowSeq, or:
- /// int or set
+ /// int or set or multiset
/// if !AllowSeq.
/// </summary>
public class OperationTypeProxy : RestrictedTypeProxy {
@@ -2062,7 +2075,7 @@ namespace Microsoft.Dafny {
get { return Elements; }
}
}
-
+
public class SetDisplayExpr : DisplayExpression {
public SetDisplayExpr(IToken tok, List<Expression/*!*/>/*!*/ elements)
: base(tok, elements) {
@@ -2071,6 +2084,13 @@ namespace Microsoft.Dafny {
}
}
+ public class MultiSetDisplayExpr : DisplayExpression {
+ public MultiSetDisplayExpr(IToken tok, List<Expression/*!*/>/*!*/ elements) : base(tok, elements) {
+ Contract.Requires(tok != null);
+ Contract.Requires(cce.NonNullElements(elements));
+ }
+ }
+
public class SeqDisplayExpr : DisplayExpression {
public SeqDisplayExpr(IToken tok, List<Expression/*!*/>/*!*/ elements)
: base(tok, elements) {
@@ -2378,6 +2398,19 @@ namespace Microsoft.Dafny {
Union,
Intersection,
SetDifference,
+ // multi-sets
+ MultiSetEq,
+ MultiSetNeq,
+ MultiSubset,
+ MultiSuperset,
+ ProperMultiSubset,
+ ProperMultiSuperset,
+ MultiSetDisjoint,
+ InMultiSet,
+ NotInMultiSet,
+ MultiSetUnion,
+ MultiSetIntersection,
+ MultiSetDifference,
// sequences
SeqEq,
SeqNeq,
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index e12ab7e3..091d9f5d 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -20,7 +20,7 @@ public class Parser {
public const int _digits = 2;
public const int _arrayToken = 3;
public const int _string = 4;
- public const int maxT = 104;
+ public const int maxT = 106;
const bool T = true;
const bool x = false;
@@ -379,7 +379,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
}
if (la.kind == 18) {
FieldDecl(mmod, mm);
- } else if (la.kind == 41) {
+ } else if (la.kind == 42) {
FunctionDecl(mmod, out f);
mm.Add(f);
} else if (la.kind == 10 || la.kind == 25 || la.kind == 26) {
@@ -387,7 +387,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
mm.Add(m);
} else if (la.kind == 20) {
CouplingInvDecl(mmod, mm);
- } else SynErr(105);
+ } else SynErr(107);
}
void GenericParameters(List<TypeParameter/*!*/>/*!*/ typeArgs) {
@@ -442,7 +442,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
- Expect(41);
+ Expect(42);
if (la.kind == 25) {
Get();
isFunctionMethod = true;
@@ -470,7 +470,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
}
FunctionBody(out bb, out bodyStart, out bodyEnd);
body = bb;
- } else SynErr(106);
+ } else SynErr(108);
f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, returnType, reqs, reads, ens, decreases, body, attrs);
f.BodyStartTok = bodyStart;
f.BodyEndTok = bodyEnd;
@@ -502,7 +502,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
} else if (la.kind == 10) {
Get();
isRefinement = true;
- } else SynErr(107);
+ } else SynErr(109);
if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); }
if (isConstructor) {
if (mmod.IsGhost) {
@@ -537,7 +537,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
}
BlockStmt(out bb, out bodyStart, out bodyEnd);
body = (BlockStmt)bb;
- } else SynErr(108);
+ } else SynErr(110);
if (isRefinement)
m = new MethodRefinement(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
else if (isConstructor)
@@ -724,17 +724,28 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
tok = t; gt = new List<Type/*!*/>();
GenericInstantiation(gt);
if (gt.Count != 1) {
+ SemErr("multiset type expects exactly one type argument");
+ }
+ ty = new MultiSetType(gt[0]);
+
+ break;
+ }
+ case 40: {
+ Get();
+ tok = t; gt = new List<Type/*!*/>();
+ GenericInstantiation(gt);
+ if (gt.Count != 1) {
SemErr("seq type expects exactly one type argument");
}
ty = new SeqType(gt[0]);
break;
}
- case 1: case 3: case 40: {
+ case 1: case 3: case 41: {
ReferenceType(out tok, out ty);
break;
}
- default: SynErr(109); break;
+ default: SynErr(111); break;
}
}
@@ -785,12 +796,12 @@ List<Expression/*!*/>/*!*/ decreases) {
Expression(out e);
Expect(17);
ens.Add(new MaybeFreeExpression(e, isFree));
- } else SynErr(110);
+ } else SynErr(112);
} else if (la.kind == 32) {
Get();
DecreasesList(decreases, false);
Expect(17);
- } else SynErr(111);
+ } else SynErr(113);
}
void BlockStmt(out Statement/*!*/ block, out IToken bodyStart, out IToken bodyEnd) {
@@ -810,7 +821,7 @@ List<Expression/*!*/>/*!*/ decreases) {
void FrameExpression(out FrameExpression/*!*/ fe) {
Contract.Ensures(Contract.ValueAtReturn(out fe) != null); Expression/*!*/ e; IToken/*!*/ id; string fieldName = null;
Expression(out e);
- if (la.kind == 44) {
+ if (la.kind == 45) {
Get();
Ident(out id);
fieldName = id.val;
@@ -857,7 +868,7 @@ List<Expression/*!*/>/*!*/ decreases) {
tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
List<Type/*!*/>/*!*/ gt;
- if (la.kind == 40) {
+ if (la.kind == 41) {
Get();
tok = t; ty = new ObjectType();
} else if (la.kind == 3) {
@@ -880,7 +891,7 @@ List<Expression/*!*/>/*!*/ decreases) {
GenericInstantiation(gt);
}
ty = new UserDefinedType(tok, tok.val, gt);
- } else SynErr(112);
+ } else SynErr(114);
}
void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/>/*!*/ decreases) {
@@ -891,7 +902,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Expression(out e);
Expect(17);
reqs.Add(e);
- } else if (la.kind == 42) {
+ } else if (la.kind == 43) {
Get();
if (StartOf(10)) {
PossiblyWildFrameExpression(out fe);
@@ -912,7 +923,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
DecreasesList(decreases, false);
Expect(17);
- } else SynErr(113);
+ } else SynErr(115);
}
void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) {
@@ -926,23 +937,23 @@ List<Expression/*!*/>/*!*/ decreases) {
void PossiblyWildFrameExpression(out FrameExpression/*!*/ fe) {
Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr;
- if (la.kind == 43) {
+ if (la.kind == 44) {
Get();
fe = new FrameExpression(new WildcardExpr(t), null);
} else if (StartOf(8)) {
FrameExpression(out fe);
- } else SynErr(114);
+ } else SynErr(116);
}
void PossiblyWildExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e)!=null);
e = dummyExpr;
- if (la.kind == 43) {
+ if (la.kind == 44) {
Get();
e = new WildcardExpr(t);
} else if (StartOf(8)) {
Expression(out e);
- } else SynErr(115);
+ } else SynErr(117);
}
void Stmt(List<Statement/*!*/>/*!*/ ss) {
@@ -963,19 +974,19 @@ List<Expression/*!*/>/*!*/ decreases) {
BlockStmt(out s, out bodyStart, out bodyEnd);
break;
}
- case 63: {
+ case 64: {
AssertStmt(out s);
break;
}
- case 64: {
+ case 65: {
AssumeStmt(out s);
break;
}
- case 65: {
+ case 66: {
PrintStmt(out s);
break;
}
- case 1: case 2: case 16: case 33: case 89: case 90: case 91: case 92: case 93: case 94: case 95: {
+ case 1: case 2: case 16: case 33: case 90: case 91: case 92: case 93: case 94: case 95: case 96: {
UpdateStmt(out s);
break;
}
@@ -983,23 +994,23 @@ List<Expression/*!*/>/*!*/ decreases) {
VarDeclStatement(out s);
break;
}
- case 54: {
+ case 55: {
IfStmt(out s);
break;
}
- case 58: {
+ case 59: {
WhileStmt(out s);
break;
}
- case 60: {
+ case 61: {
MatchStmt(out s);
break;
}
- case 61: {
+ case 62: {
ForeachStmt(out s);
break;
}
- case 45: {
+ case 46: {
Get();
x = t;
Ident(out id);
@@ -1008,33 +1019,33 @@ List<Expression/*!*/>/*!*/ decreases) {
s.Labels = new LabelNode(x, id.val, s.Labels);
break;
}
- case 46: {
+ case 47: {
Get();
x = t; breakCount = 1; label = null;
if (la.kind == 1) {
Ident(out id);
label = id.val;
- } else if (la.kind == 17 || la.kind == 46) {
- while (la.kind == 46) {
+ } else if (la.kind == 17 || la.kind == 47) {
+ while (la.kind == 47) {
Get();
breakCount++;
}
- } else SynErr(116);
+ } else SynErr(118);
Expect(17);
s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount);
break;
}
- case 47: {
+ case 48: {
ReturnStmt(out s);
break;
}
- default: SynErr(117); break;
+ default: SynErr(119); break;
}
}
void AssertStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e;
- Expect(63);
+ Expect(64);
x = t;
Expression(out e);
Expect(17);
@@ -1043,7 +1054,7 @@ List<Expression/*!*/>/*!*/ decreases) {
void AssumeStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e;
- Expect(64);
+ Expect(65);
x = t;
Expression(out e);
Expect(17);
@@ -1054,7 +1065,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Attributes.Argument/*!*/ arg;
List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();
- Expect(65);
+ Expect(66);
x = t;
AttributeArg(out arg);
args.Add(arg);
@@ -1079,14 +1090,14 @@ List<Expression/*!*/>/*!*/ decreases) {
if (la.kind == 17) {
Get();
rhss.Add(new ExprRhs(e));
- } else if (la.kind == 19 || la.kind == 48) {
+ } else if (la.kind == 19 || la.kind == 49) {
lhss.Add(e); lhs0 = e;
while (la.kind == 19) {
Get();
Lhs(out e);
lhss.Add(e);
}
- Expect(48);
+ Expect(49);
x = t;
Rhs(out r, lhs0);
rhss.Add(r);
@@ -1099,7 +1110,7 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (la.kind == 22) {
Get();
SemErr(t, "invalid statement (did you forget the 'label' keyword?)");
- } else SynErr(118);
+ } else SynErr(120);
s = new UpdateStmt(x, lhss, rhss);
}
@@ -1123,7 +1134,7 @@ List<Expression/*!*/>/*!*/ decreases) {
LocalIdentTypeOptional(out d, isGhost);
lhss.Add(d);
}
- if (la.kind == 48) {
+ if (la.kind == 49) {
Get();
assignTok = t; lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name);
Rhs(out r, lhs0);
@@ -1159,26 +1170,26 @@ List<Expression/*!*/>/*!*/ decreases) {
List<GuardedAlternative> alternatives;
ifStmt = dummyStmt; // to please the compiler
- Expect(54);
+ Expect(55);
x = t;
if (la.kind == 33) {
Guard(out guard);
BlockStmt(out thn, out bodyStart, out bodyEnd);
- if (la.kind == 55) {
+ if (la.kind == 56) {
Get();
- if (la.kind == 54) {
+ if (la.kind == 55) {
IfStmt(out s);
els = s;
} else if (la.kind == 7) {
BlockStmt(out s, out bodyStart, out bodyEnd);
els = s;
- } else SynErr(119);
+ } else SynErr(121);
}
ifStmt = new IfStmt(x, guard, thn, els);
} else if (la.kind == 7) {
AlternativeBlock(out alternatives);
ifStmt = new AlternativeStmt(x, alternatives);
- } else SynErr(120);
+ } else SynErr(122);
}
void WhileStmt(out Statement/*!*/ stmt) {
@@ -1192,7 +1203,7 @@ List<Expression/*!*/>/*!*/ decreases) {
List<GuardedAlternative> alternatives;
stmt = dummyStmt; // to please the compiler
- Expect(58);
+ Expect(59);
x = t;
if (la.kind == 33) {
Guard(out guard);
@@ -1204,18 +1215,18 @@ List<Expression/*!*/>/*!*/ decreases) {
LoopSpec(out invariants, out decreases, out mod);
AlternativeBlock(out alternatives);
stmt = new AlternativeLoopStmt(x, invariants, decreases, mod, alternatives);
- } else SynErr(121);
+ } else SynErr(123);
}
void MatchStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null);
Token x; Expression/*!*/ e; MatchCaseStmt/*!*/ c;
List<MatchCaseStmt/*!*/> cases = new List<MatchCaseStmt/*!*/>();
- Expect(60);
+ Expect(61);
x = t;
Expression(out e);
Expect(7);
- while (la.kind == 56) {
+ while (la.kind == 57) {
CaseStatement(out c);
cases.Add(c);
}
@@ -1232,7 +1243,7 @@ List<Expression/*!*/>/*!*/ decreases) {
List<PredicateStmt/*!*/> bodyPrefix = new List<PredicateStmt/*!*/>();
Statement bodyAssign = null;
- Expect(61);
+ Expect(62);
x = t;
range = new LiteralExpr(x, true);
ty = new InferredTypeProxy();
@@ -1243,7 +1254,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
Type(out ty);
}
- Expect(62);
+ Expect(63);
Expression(out collection);
if (la.kind == 16) {
Get();
@@ -1251,8 +1262,8 @@ List<Expression/*!*/>/*!*/ decreases) {
}
Expect(34);
Expect(7);
- while (la.kind == 63 || la.kind == 64) {
- if (la.kind == 63) {
+ while (la.kind == 64 || la.kind == 65) {
+ if (la.kind == 64) {
AssertStmt(out s);
if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); }
} else {
@@ -1276,7 +1287,7 @@ List<Expression/*!*/>/*!*/ decreases) {
List<AssignmentRhs> rhss = null;
AssignmentRhs r;
- Expect(47);
+ Expect(48);
returnTok = t;
if (StartOf(12)) {
Rhs(out r, null);
@@ -1299,16 +1310,16 @@ List<Expression/*!*/>/*!*/ decreases) {
List<Expression> args;
r = null; // to please compiler
- if (la.kind == 49) {
+ if (la.kind == 50) {
Get();
newToken = t;
TypeAndToken(out x, out ty);
- if (la.kind == 50 || la.kind == 52) {
- if (la.kind == 50) {
+ if (la.kind == 51 || la.kind == 53) {
+ if (la.kind == 51) {
Get();
ee = new List<Expression>();
Expressions(ee);
- Expect(51);
+ Expect(52);
UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true);
} else {
@@ -1330,18 +1341,18 @@ List<Expression/*!*/>/*!*/ decreases) {
r = new TypeRhs(newToken, ty, initCall);
}
- } else if (la.kind == 53) {
+ } else if (la.kind == 54) {
Get();
x = t;
Expression(out e);
r = new ExprRhs(new UnaryExpr(x, UnaryExpr.Opcode.SetChoose, e));
- } else if (la.kind == 43) {
+ } else if (la.kind == 44) {
Get();
r = new HavocRhs(t);
} else if (StartOf(8)) {
Expression(out e);
r = new ExprRhs(e);
- } else SynErr(122);
+ } else SynErr(124);
}
void Lhs(out Expression e) {
@@ -1349,16 +1360,16 @@ List<Expression/*!*/>/*!*/ decreases) {
if (la.kind == 1) {
DottedIdentifiersAndFunction(out e);
- while (la.kind == 50 || la.kind == 52) {
+ while (la.kind == 51 || la.kind == 53) {
Suffix(ref e);
}
} else if (StartOf(13)) {
ConstAtomExpression(out e);
Suffix(ref e);
- while (la.kind == 50 || la.kind == 52) {
+ while (la.kind == 51 || la.kind == 53) {
Suffix(ref e);
}
- } else SynErr(123);
+ } else SynErr(125);
}
void Expressions(List<Expression/*!*/>/*!*/ args) {
@@ -1375,13 +1386,13 @@ List<Expression/*!*/>/*!*/ decreases) {
void Guard(out Expression e) {
Expression/*!*/ ee; e = null;
Expect(33);
- if (la.kind == 43) {
+ if (la.kind == 44) {
Get();
e = null;
} else if (StartOf(8)) {
Expression(out ee);
e = ee;
- } else SynErr(124);
+ } else SynErr(126);
Expect(34);
}
@@ -1392,11 +1403,11 @@ List<Expression/*!*/>/*!*/ decreases) {
List<Statement> body;
Expect(7);
- while (la.kind == 56) {
+ while (la.kind == 57) {
Get();
x = t;
Expression(out e);
- Expect(57);
+ Expect(58);
body = new List<Statement>();
while (StartOf(9)) {
Stmt(body);
@@ -1413,13 +1424,13 @@ List<Expression/*!*/>/*!*/ decreases) {
mod = null;
while (StartOf(14)) {
- if (la.kind == 29 || la.kind == 59) {
+ if (la.kind == 29 || la.kind == 60) {
isFree = false;
if (la.kind == 29) {
Get();
isFree = true;
}
- Expect(59);
+ Expect(60);
Expression(out e);
invariants.Add(new MaybeFreeExpression(e, isFree));
Expect(17);
@@ -1450,7 +1461,7 @@ List<Expression/*!*/>/*!*/ decreases) {
List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();
List<Statement/*!*/> body = new List<Statement/*!*/>();
- Expect(56);
+ Expect(57);
x = t;
Ident(out id);
if (la.kind == 33) {
@@ -1464,7 +1475,7 @@ List<Expression/*!*/>/*!*/ decreases) {
}
Expect(34);
}
- Expect(57);
+ Expect(58);
while (StartOf(9)) {
Stmt(body);
}
@@ -1479,13 +1490,13 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (StartOf(8)) {
Expression(out e);
arg = new Attributes.Argument(e);
- } else SynErr(125);
+ } else SynErr(127);
}
void EquivExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
ImpliesExpression(out e0);
- while (la.kind == 66 || la.kind == 67) {
+ while (la.kind == 67 || la.kind == 68) {
EquivOp();
x = t;
ImpliesExpression(out e1);
@@ -1496,7 +1507,7 @@ List<Expression/*!*/>/*!*/ decreases) {
void ImpliesExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
LogicalExpression(out e0);
- if (la.kind == 68 || la.kind == 69) {
+ if (la.kind == 69 || la.kind == 70) {
ImpliesOp();
x = t;
ImpliesExpression(out e1);
@@ -1505,23 +1516,23 @@ List<Expression/*!*/>/*!*/ decreases) {
}
void EquivOp() {
- if (la.kind == 66) {
+ if (la.kind == 67) {
Get();
- } else if (la.kind == 67) {
+ } else if (la.kind == 68) {
Get();
- } else SynErr(126);
+ } else SynErr(128);
}
void LogicalExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
RelationalExpression(out e0);
if (StartOf(15)) {
- if (la.kind == 70 || la.kind == 71) {
+ if (la.kind == 71 || la.kind == 72) {
AndOp();
x = t;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1);
- while (la.kind == 70 || la.kind == 71) {
+ while (la.kind == 71 || la.kind == 72) {
AndOp();
x = t;
RelationalExpression(out e1);
@@ -1532,7 +1543,7 @@ List<Expression/*!*/>/*!*/ decreases) {
x = t;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1);
- while (la.kind == 72 || la.kind == 73) {
+ while (la.kind == 73 || la.kind == 74) {
OrOp();
x = t;
RelationalExpression(out e1);
@@ -1543,11 +1554,11 @@ List<Expression/*!*/>/*!*/ decreases) {
}
void ImpliesOp() {
- if (la.kind == 68) {
+ if (la.kind == 69) {
Get();
- } else if (la.kind == 69) {
+ } else if (la.kind == 70) {
Get();
- } else SynErr(127);
+ } else SynErr(129);
}
void RelationalExpression(out Expression/*!*/ e) {
@@ -1570,7 +1581,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Term(out e1);
e = new BinaryExpr(x, op, e0, e1);
if (op == BinaryExpr.Opcode.Disjoint)
- acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, e0, e1); // accumulate first two operands.
+ acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, e0, e1); // accumulate first two operands.
while (StartOf(16)) {
if (chain == null) {
@@ -1603,36 +1614,35 @@ List<Expression/*!*/>/*!*/ decreases) {
break;
case BinaryExpr.Opcode.Neq:
if (hasSeenNeq) { SemErr(x, "a chain cannot have more than one != operator"); }
- if (kind != 0 && kind != 1 && kind != 2) { SemErr(x, "this operator cannot continue this chain"); }
- hasSeenNeq = true; break;
- case BinaryExpr.Opcode.Lt:
- case BinaryExpr.Opcode.Le:
- if (kind == 0) { kind = 1; }
- else if (kind != 1) { SemErr(x, "this operator chain cannot continue with an ascending operator"); }
- break;
- case BinaryExpr.Opcode.Gt:
- case BinaryExpr.Opcode.Ge:
- if (kind == 0) { kind = 2; }
- else if (kind != 2) { SemErr(x, "this operator chain cannot continue with a descending operator"); }
- break;
- case BinaryExpr.Opcode.Disjoint:
- if (kind != 4) { SemErr(x, "can only chain disjoint (!!) with itself."); kind = 3; }
- break;
- default:
- SemErr(x, "this operator cannot be part of a chain");
- kind = 3; break;
- }
-
+ if (kind != 0 && kind != 1 && kind != 2) { SemErr(x, "this operator cannot continue this chain"); }
+ hasSeenNeq = true; break;
+ case BinaryExpr.Opcode.Lt:
+ case BinaryExpr.Opcode.Le:
+ if (kind == 0) { kind = 1; }
+ else if (kind != 1) { SemErr(x, "this operator chain cannot continue with an ascending operator"); }
+ break;
+ case BinaryExpr.Opcode.Gt:
+ case BinaryExpr.Opcode.Ge:
+ if (kind == 0) { kind = 2; }
+ else if (kind != 2) { SemErr(x, "this operator chain cannot continue with a descending operator"); }
+ break;
+ case BinaryExpr.Opcode.Disjoint:
+ if (kind != 4) { SemErr(x, "can only chain disjoint (!!) with itself."); kind = 3; }
+ break;
+ default:
+ SemErr(x, "this operator cannot be part of a chain");
+ kind = 3; break;
+ }
+
Term(out e1);
ops.Add(op); chain.Add(e1);
- if (op == BinaryExpr.Opcode.Disjoint)
- {
+ if (op == BinaryExpr.Opcode.Disjoint) {
e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, acc, e1));
- acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, acc, e1); //e0 has already been added.
- }
- else
- e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, e0, e1));
-
+ acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, acc, e1); //e0 has already been added.
+ }
+ else
+ e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, e0, e1));
+
}
}
if (chain != null) {
@@ -1642,25 +1652,25 @@ List<Expression/*!*/>/*!*/ decreases) {
}
void AndOp() {
- if (la.kind == 70) {
+ if (la.kind == 71) {
Get();
- } else if (la.kind == 71) {
+ } else if (la.kind == 72) {
Get();
- } else SynErr(128);
+ } else SynErr(130);
}
void OrOp() {
- if (la.kind == 72) {
+ if (la.kind == 73) {
Get();
- } else if (la.kind == 73) {
+ } else if (la.kind == 74) {
Get();
- } else SynErr(129);
+ } else SynErr(131);
}
void Term(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
Factor(out e0);
- while (la.kind == 83 || la.kind == 84) {
+ while (la.kind == 84 || la.kind == 85) {
AddOp(out x, out op);
Factor(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1670,7 +1680,7 @@ List<Expression/*!*/>/*!*/ decreases) {
void RelOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
switch (la.kind) {
- case 74: {
+ case 75: {
Get();
x = t; op = BinaryExpr.Opcode.Eq;
break;
@@ -1685,59 +1695,59 @@ List<Expression/*!*/>/*!*/ decreases) {
x = t; op = BinaryExpr.Opcode.Gt;
break;
}
- case 75: {
+ case 76: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 76: {
+ case 77: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- case 77: {
+ case 78: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
break;
}
- case 78: {
+ case 79: {
Get();
x = t; op = BinaryExpr.Opcode.Disjoint;
break;
}
- case 62: {
+ case 63: {
Get();
x = t; op = BinaryExpr.Opcode.In;
break;
}
- case 79: {
+ case 80: {
Get();
x = t; op = BinaryExpr.Opcode.NotIn;
break;
}
- case 80: {
+ case 81: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
break;
}
- case 81: {
+ case 82: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 82: {
+ case 83: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- default: SynErr(130); break;
+ default: SynErr(132); break;
}
}
void Factor(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
UnaryExpression(out e0);
- while (la.kind == 43 || la.kind == 85 || la.kind == 86) {
+ while (la.kind == 44 || la.kind == 86 || la.kind == 87) {
MulOp(out x, out op);
UnaryExpression(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1746,78 +1756,78 @@ List<Expression/*!*/>/*!*/ decreases) {
void AddOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryExpr.Opcode.Add/*(dummy)*/;
- if (la.kind == 83) {
+ if (la.kind == 84) {
Get();
x = t; op = BinaryExpr.Opcode.Add;
- } else if (la.kind == 84) {
+ } else if (la.kind == 85) {
Get();
x = t; op = BinaryExpr.Opcode.Sub;
- } else SynErr(131);
+ } else SynErr(133);
}
void UnaryExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr;
switch (la.kind) {
- case 84: {
+ case 85: {
Get();
x = t;
UnaryExpression(out e);
e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e);
break;
}
- case 87: case 88: {
+ case 88: case 89: {
NegOp();
x = t;
UnaryExpression(out e);
e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e);
break;
}
- case 38: case 54: case 60: case 98: case 99: case 100: case 101: {
+ case 38: case 55: case 61: case 100: case 101: case 102: case 103: {
EndlessExpression(out e);
break;
}
case 1: {
DottedIdentifiersAndFunction(out e);
- while (la.kind == 50 || la.kind == 52) {
+ while (la.kind == 51 || la.kind == 53) {
Suffix(ref e);
}
break;
}
- case 7: case 50: {
+ case 7: case 51: case 97: {
DisplayExpr(out e);
break;
}
- case 2: case 16: case 33: case 89: case 90: case 91: case 92: case 93: case 94: case 95: {
+ case 2: case 16: case 33: case 90: case 91: case 92: case 93: case 94: case 95: case 96: {
ConstAtomExpression(out e);
- while (la.kind == 50 || la.kind == 52) {
+ while (la.kind == 51 || la.kind == 53) {
Suffix(ref e);
}
break;
}
- default: SynErr(132); break;
+ default: SynErr(134); break;
}
}
void MulOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
- if (la.kind == 43) {
+ if (la.kind == 44) {
Get();
x = t; op = BinaryExpr.Opcode.Mul;
- } else if (la.kind == 85) {
+ } else if (la.kind == 86) {
Get();
x = t; op = BinaryExpr.Opcode.Div;
- } else if (la.kind == 86) {
+ } else if (la.kind == 87) {
Get();
x = t; op = BinaryExpr.Opcode.Mod;
- } else SynErr(133);
+ } else SynErr(135);
}
void NegOp() {
- if (la.kind == 87) {
+ if (la.kind == 88) {
Get();
- } else if (la.kind == 88) {
+ } else if (la.kind == 89) {
Get();
- } else SynErr(134);
+ } else SynErr(136);
}
void EndlessExpression(out Expression e) {
@@ -1825,22 +1835,22 @@ List<Expression/*!*/>/*!*/ decreases) {
Expression e0, e1;
e = dummyExpr;
- if (la.kind == 54) {
+ if (la.kind == 55) {
Get();
x = t;
Expression(out e);
- Expect(96);
+ Expect(98);
Expression(out e0);
- Expect(55);
+ Expect(56);
Expression(out e1);
e = new ITEExpr(x, e, e0, e1);
- } else if (la.kind == 60) {
+ } else if (la.kind == 61) {
MatchExpression(out e);
} else if (StartOf(17)) {
QuantifierGuts(out e);
} else if (la.kind == 38) {
ComprehensionExpr(out e);
- } else SynErr(135);
+ } else SynErr(137);
}
void DottedIdentifiersAndFunction(out Expression e) {
@@ -1850,7 +1860,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Ident(out id);
idents.Add(id);
- while (la.kind == 52) {
+ while (la.kind == 53) {
Get();
Ident(out id);
idents.Add(id);
@@ -1872,7 +1882,7 @@ List<Expression/*!*/>/*!*/ decreases) {
List<Expression> multipleIndices = null;
bool func = false;
- if (la.kind == 52) {
+ if (la.kind == 53) {
Get();
Ident(out id);
if (la.kind == 33) {
@@ -1885,24 +1895,24 @@ List<Expression/*!*/>/*!*/ decreases) {
e = new FunctionCallExpr(id, id.val, e, args);
}
if (!func) { e = new FieldSelectExpr(id, e, id.val); }
- } else if (la.kind == 50) {
+ } else if (la.kind == 51) {
Get();
x = t;
if (StartOf(8)) {
Expression(out ee);
e0 = ee;
- if (la.kind == 97) {
+ if (la.kind == 99) {
Get();
anyDots = true;
if (StartOf(8)) {
Expression(out ee);
e1 = ee;
}
- } else if (la.kind == 48) {
+ } else if (la.kind == 49) {
Get();
Expression(out ee);
e1 = ee;
- } else if (la.kind == 19 || la.kind == 51) {
+ } else if (la.kind == 19 || la.kind == 52) {
while (la.kind == 19) {
Get();
Expression(out ee);
@@ -1913,12 +1923,12 @@ List<Expression/*!*/>/*!*/ decreases) {
multipleIndices.Add(ee);
}
- } else SynErr(136);
- } else if (la.kind == 97) {
+ } else SynErr(138);
+ } else if (la.kind == 99) {
Get();
Expression(out ee);
anyDots = true; e1 = ee;
- } else SynErr(137);
+ } else SynErr(139);
if (multipleIndices != null) {
e = new MultiSelectExpr(x, e, multipleIndices);
// make sure an array class with this dimensionality exists
@@ -1941,32 +1951,38 @@ List<Expression/*!*/>/*!*/ decreases) {
}
}
- Expect(51);
- } else SynErr(138);
+ Expect(52);
+ } else SynErr(140);
}
void DisplayExpr(out Expression e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null);
- IToken/*!*/ x; List<Expression/*!*/>/*!*/ elements;
+ IToken/*!*/ x = null; List<Expression/*!*/>/*!*/ elements;
e = dummyExpr;
+ bool isMulti = false;
- if (la.kind == 7) {
- Get();
- x = t; elements = new List<Expression/*!*/>();
+ if (la.kind == 7 || la.kind == 97) {
+ if (la.kind == 97) {
+ Get();
+ x = t; isMulti = true;
+ }
+ Expect(7);
+ if (!isMulti) x = t; elements = new List<Expression/*!*/>();
if (StartOf(8)) {
Expressions(elements);
}
- e = new SetDisplayExpr(x, elements);
+ if (isMulti) e = new MultiSetDisplayExpr(x, elements);
+ else e = new SetDisplayExpr(x, elements);
Expect(8);
- } else if (la.kind == 50) {
+ } else if (la.kind == 51) {
Get();
x = t; elements = new List<Expression/*!*/>();
if (StartOf(8)) {
Expressions(elements);
}
e = new SeqDisplayExpr(x, elements);
- Expect(51);
- } else SynErr(139);
+ Expect(52);
+ } else SynErr(141);
}
void ConstAtomExpression(out Expression/*!*/ e) {
@@ -1975,17 +1991,17 @@ List<Expression/*!*/>/*!*/ decreases) {
e = dummyExpr;
switch (la.kind) {
- case 89: {
+ case 90: {
Get();
e = new LiteralExpr(t, false);
break;
}
- case 90: {
+ case 91: {
Get();
e = new LiteralExpr(t, true);
break;
}
- case 91: {
+ case 92: {
Get();
e = new LiteralExpr(t);
break;
@@ -1995,12 +2011,12 @@ List<Expression/*!*/>/*!*/ decreases) {
e = new LiteralExpr(t, n);
break;
}
- case 92: {
+ case 93: {
Get();
e = new ThisExpr(t);
break;
}
- case 93: {
+ case 94: {
Get();
x = t;
Expect(33);
@@ -2009,7 +2025,7 @@ List<Expression/*!*/>/*!*/ decreases) {
e = new FreshExpr(x, e);
break;
}
- case 94: {
+ case 95: {
Get();
x = t;
Expect(33);
@@ -2018,7 +2034,7 @@ List<Expression/*!*/>/*!*/ decreases) {
e = new AllocatedExpr(x, e);
break;
}
- case 95: {
+ case 96: {
Get();
x = t;
Expect(33);
@@ -2043,7 +2059,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Expect(34);
break;
}
- default: SynErr(140); break;
+ default: SynErr(142); break;
}
}
@@ -2062,10 +2078,10 @@ List<Expression/*!*/>/*!*/ decreases) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; MatchCaseExpr/*!*/ c;
List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();
- Expect(60);
+ Expect(61);
x = t;
Expression(out e);
- while (la.kind == 56) {
+ while (la.kind == 57) {
CaseExpression(out c);
cases.Add(c);
}
@@ -2082,13 +2098,13 @@ List<Expression/*!*/>/*!*/ decreases) {
Expression range = null;
Expression/*!*/ body;
- if (la.kind == 98 || la.kind == 99) {
+ if (la.kind == 100 || la.kind == 101) {
Forall();
x = t; univ = true;
- } else if (la.kind == 100 || la.kind == 101) {
+ } else if (la.kind == 102 || la.kind == 103) {
Exists();
x = t;
- } else SynErr(141);
+ } else SynErr(143);
IdentTypeOptional(out bv);
bvars.Add(bv);
while (la.kind == 19) {
@@ -2132,7 +2148,7 @@ List<Expression/*!*/>/*!*/ decreases) {
}
Expect(16);
Expression(out range);
- if (la.kind == 102 || la.kind == 103) {
+ if (la.kind == 104 || la.kind == 105) {
QSep();
Expression(out body);
}
@@ -2146,7 +2162,7 @@ List<Expression/*!*/>/*!*/ decreases) {
List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();
Expression/*!*/ body;
- Expect(56);
+ Expect(57);
x = t;
Ident(out id);
if (la.kind == 33) {
@@ -2160,25 +2176,25 @@ List<Expression/*!*/>/*!*/ decreases) {
}
Expect(34);
}
- Expect(57);
+ Expect(58);
Expression(out body);
c = new MatchCaseExpr(x, id.val, arguments, body);
}
void Forall() {
- if (la.kind == 98) {
+ if (la.kind == 100) {
Get();
- } else if (la.kind == 99) {
+ } else if (la.kind == 101) {
Get();
- } else SynErr(142);
+ } else SynErr(144);
}
void Exists() {
- if (la.kind == 100) {
+ if (la.kind == 102) {
Get();
- } else if (la.kind == 101) {
+ } else if (la.kind == 103) {
Get();
- } else SynErr(143);
+ } else SynErr(145);
}
void AttributeOrTrigger(ref Attributes attrs, ref Triggers trigs) {
@@ -2191,16 +2207,16 @@ List<Expression/*!*/>/*!*/ decreases) {
es = new List<Expression/*!*/>();
Expressions(es);
trigs = new Triggers(es, trigs);
- } else SynErr(144);
+ } else SynErr(146);
Expect(8);
}
void QSep() {
- if (la.kind == 102) {
+ if (la.kind == 104) {
Get();
- } else if (la.kind == 103) {
+ } else if (la.kind == 105) {
Get();
- } else SynErr(145);
+ } else SynErr(147);
}
void AttributeBody(ref Attributes attrs) {
@@ -2235,25 +2251,25 @@ List<Expression/*!*/>/*!*/ decreases) {
}
static readonly bool[,]/*!*/ set = {
- {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,T,x,x, x,T,T,T, T,T,T,x, x,x,T,x, T,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,T,x, T,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,T,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
- {x,T,T,x, x,x,x,T, x,x,x,T, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,T,x, x,x,T,x, T,T,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},
- {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,x,x,T, x,x,x,x, x,x,T,x, x,x,T,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
- {x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,x,x,T, x,x,x,x, x,T,T,x, x,T,T,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
- {x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x},
- {x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,T,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x}
+ {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,x,x,x, x,T,x,x, x,T,T,T, T,T,T,x, x,x,T,x, T,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,T,x, T,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x},
+ {x,T,T,x, x,x,x,T, x,x,x,T, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,T, x,x,x,T, x,T,T,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x},
+ {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,x,x,x, T,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x},
+ {x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,x,x,x, T,x,x,x, x,x,T,T, x,x,T,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x},
+ {x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x},
+ {x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x}
};
} // end Parser
@@ -2317,113 +2333,115 @@ public class Errors {
case 36: s = "\"nat\" expected"; break;
case 37: s = "\"int\" expected"; break;
case 38: s = "\"set\" expected"; break;
- case 39: s = "\"seq\" expected"; break;
- case 40: s = "\"object\" expected"; break;
- case 41: s = "\"function\" expected"; break;
- case 42: s = "\"reads\" expected"; break;
- case 43: s = "\"*\" expected"; break;
- case 44: s = "\"`\" expected"; break;
- case 45: s = "\"label\" expected"; break;
- case 46: s = "\"break\" expected"; break;
- case 47: s = "\"return\" expected"; break;
- case 48: s = "\":=\" expected"; break;
- case 49: s = "\"new\" expected"; break;
- case 50: s = "\"[\" expected"; break;
- case 51: s = "\"]\" expected"; break;
- case 52: s = "\".\" expected"; break;
- case 53: s = "\"choose\" expected"; break;
- case 54: s = "\"if\" expected"; break;
- case 55: s = "\"else\" expected"; break;
- case 56: s = "\"case\" expected"; break;
- case 57: s = "\"=>\" expected"; break;
- case 58: s = "\"while\" expected"; break;
- case 59: s = "\"invariant\" expected"; break;
- case 60: s = "\"match\" expected"; break;
- case 61: s = "\"foreach\" expected"; break;
- case 62: s = "\"in\" expected"; break;
- case 63: s = "\"assert\" expected"; break;
- case 64: s = "\"assume\" expected"; break;
- case 65: s = "\"print\" expected"; break;
- case 66: s = "\"<==>\" expected"; break;
- case 67: s = "\"\\u21d4\" expected"; break;
- case 68: s = "\"==>\" expected"; break;
- case 69: s = "\"\\u21d2\" expected"; break;
- case 70: s = "\"&&\" expected"; break;
- case 71: s = "\"\\u2227\" expected"; break;
- case 72: s = "\"||\" expected"; break;
- case 73: s = "\"\\u2228\" expected"; break;
- case 74: s = "\"==\" expected"; break;
- case 75: s = "\"<=\" expected"; break;
- case 76: s = "\">=\" expected"; break;
- case 77: s = "\"!=\" expected"; break;
- case 78: s = "\"!!\" expected"; break;
- case 79: s = "\"!in\" expected"; break;
- case 80: s = "\"\\u2260\" expected"; break;
- case 81: s = "\"\\u2264\" expected"; break;
- case 82: s = "\"\\u2265\" expected"; break;
- case 83: s = "\"+\" expected"; break;
- case 84: s = "\"-\" expected"; break;
- case 85: s = "\"/\" expected"; break;
- case 86: s = "\"%\" expected"; break;
- case 87: s = "\"!\" expected"; break;
- case 88: s = "\"\\u00ac\" expected"; break;
- case 89: s = "\"false\" expected"; break;
- case 90: s = "\"true\" expected"; break;
- case 91: s = "\"null\" expected"; break;
- case 92: s = "\"this\" expected"; break;
- case 93: s = "\"fresh\" expected"; break;
- case 94: s = "\"allocated\" expected"; break;
- case 95: s = "\"old\" expected"; break;
- case 96: s = "\"then\" expected"; break;
- case 97: s = "\"..\" expected"; break;
- case 98: s = "\"forall\" expected"; break;
- case 99: s = "\"\\u2200\" expected"; break;
- case 100: s = "\"exists\" expected"; break;
- case 101: s = "\"\\u2203\" expected"; break;
- case 102: s = "\"::\" expected"; break;
- case 103: s = "\"\\u2022\" expected"; break;
- case 104: s = "??? expected"; break;
- case 105: s = "invalid ClassMemberDecl"; break;
- case 106: s = "invalid FunctionDecl"; break;
- case 107: s = "invalid MethodDecl"; break;
- case 108: s = "invalid MethodDecl"; break;
- case 109: s = "invalid TypeAndToken"; break;
- case 110: s = "invalid MethodSpec"; break;
- case 111: s = "invalid MethodSpec"; break;
- case 112: s = "invalid ReferenceType"; break;
- case 113: s = "invalid FunctionSpec"; break;
- case 114: s = "invalid PossiblyWildFrameExpression"; break;
- case 115: s = "invalid PossiblyWildExpression"; break;
- case 116: s = "invalid OneStmt"; break;
- case 117: s = "invalid OneStmt"; break;
- case 118: s = "invalid UpdateStmt"; break;
- case 119: s = "invalid IfStmt"; break;
- case 120: s = "invalid IfStmt"; break;
- case 121: s = "invalid WhileStmt"; break;
- case 122: s = "invalid Rhs"; break;
- case 123: s = "invalid Lhs"; break;
- case 124: s = "invalid Guard"; break;
- case 125: s = "invalid AttributeArg"; break;
- case 126: s = "invalid EquivOp"; break;
- case 127: s = "invalid ImpliesOp"; break;
- case 128: s = "invalid AndOp"; break;
- case 129: s = "invalid OrOp"; break;
- case 130: s = "invalid RelOp"; break;
- case 131: s = "invalid AddOp"; break;
- case 132: s = "invalid UnaryExpression"; break;
- case 133: s = "invalid MulOp"; break;
- case 134: s = "invalid NegOp"; break;
- case 135: s = "invalid EndlessExpression"; break;
- case 136: s = "invalid Suffix"; break;
- case 137: s = "invalid Suffix"; break;
+ case 39: s = "\"multiset\" expected"; break;
+ case 40: s = "\"seq\" expected"; break;
+ case 41: s = "\"object\" expected"; break;
+ case 42: s = "\"function\" expected"; break;
+ case 43: s = "\"reads\" expected"; break;
+ case 44: s = "\"*\" expected"; break;
+ case 45: s = "\"`\" expected"; break;
+ case 46: s = "\"label\" expected"; break;
+ case 47: s = "\"break\" expected"; break;
+ case 48: s = "\"return\" expected"; break;
+ case 49: s = "\":=\" expected"; break;
+ case 50: s = "\"new\" expected"; break;
+ case 51: s = "\"[\" expected"; break;
+ case 52: s = "\"]\" expected"; break;
+ case 53: s = "\".\" expected"; break;
+ case 54: s = "\"choose\" expected"; break;
+ case 55: s = "\"if\" expected"; break;
+ case 56: s = "\"else\" expected"; break;
+ case 57: s = "\"case\" expected"; break;
+ case 58: s = "\"=>\" expected"; break;
+ case 59: s = "\"while\" expected"; break;
+ case 60: s = "\"invariant\" expected"; break;
+ case 61: s = "\"match\" expected"; break;
+ case 62: s = "\"foreach\" expected"; break;
+ case 63: s = "\"in\" expected"; break;
+ case 64: s = "\"assert\" expected"; break;
+ case 65: s = "\"assume\" expected"; break;
+ case 66: s = "\"print\" expected"; break;
+ case 67: s = "\"<==>\" expected"; break;
+ case 68: s = "\"\\u21d4\" expected"; break;
+ case 69: s = "\"==>\" expected"; break;
+ case 70: s = "\"\\u21d2\" expected"; break;
+ case 71: s = "\"&&\" expected"; break;
+ case 72: s = "\"\\u2227\" expected"; break;
+ case 73: s = "\"||\" expected"; break;
+ case 74: s = "\"\\u2228\" expected"; break;
+ case 75: s = "\"==\" expected"; break;
+ case 76: s = "\"<=\" expected"; break;
+ case 77: s = "\">=\" expected"; break;
+ case 78: s = "\"!=\" expected"; break;
+ case 79: s = "\"!!\" expected"; break;
+ case 80: s = "\"!in\" expected"; break;
+ case 81: s = "\"\\u2260\" expected"; break;
+ case 82: s = "\"\\u2264\" expected"; break;
+ case 83: s = "\"\\u2265\" expected"; break;
+ case 84: s = "\"+\" expected"; break;
+ case 85: s = "\"-\" expected"; break;
+ case 86: s = "\"/\" expected"; break;
+ case 87: s = "\"%\" expected"; break;
+ case 88: s = "\"!\" expected"; break;
+ case 89: s = "\"\\u00ac\" expected"; break;
+ case 90: s = "\"false\" expected"; break;
+ case 91: s = "\"true\" expected"; break;
+ case 92: s = "\"null\" expected"; break;
+ case 93: s = "\"this\" expected"; break;
+ case 94: s = "\"fresh\" expected"; break;
+ case 95: s = "\"allocated\" expected"; break;
+ case 96: s = "\"old\" expected"; break;
+ case 97: s = "\"multi\" expected"; break;
+ case 98: s = "\"then\" expected"; break;
+ case 99: s = "\"..\" expected"; break;
+ case 100: s = "\"forall\" expected"; break;
+ case 101: s = "\"\\u2200\" expected"; break;
+ case 102: s = "\"exists\" expected"; break;
+ case 103: s = "\"\\u2203\" expected"; break;
+ case 104: s = "\"::\" expected"; break;
+ case 105: s = "\"\\u2022\" expected"; break;
+ case 106: s = "??? expected"; break;
+ case 107: s = "invalid ClassMemberDecl"; break;
+ case 108: s = "invalid FunctionDecl"; break;
+ case 109: s = "invalid MethodDecl"; break;
+ case 110: s = "invalid MethodDecl"; break;
+ case 111: s = "invalid TypeAndToken"; break;
+ case 112: s = "invalid MethodSpec"; break;
+ case 113: s = "invalid MethodSpec"; break;
+ case 114: s = "invalid ReferenceType"; break;
+ case 115: s = "invalid FunctionSpec"; break;
+ case 116: s = "invalid PossiblyWildFrameExpression"; break;
+ case 117: s = "invalid PossiblyWildExpression"; break;
+ case 118: s = "invalid OneStmt"; break;
+ case 119: s = "invalid OneStmt"; break;
+ case 120: s = "invalid UpdateStmt"; break;
+ case 121: s = "invalid IfStmt"; break;
+ case 122: s = "invalid IfStmt"; break;
+ case 123: s = "invalid WhileStmt"; break;
+ case 124: s = "invalid Rhs"; break;
+ case 125: s = "invalid Lhs"; break;
+ case 126: s = "invalid Guard"; break;
+ case 127: s = "invalid AttributeArg"; break;
+ case 128: s = "invalid EquivOp"; break;
+ case 129: s = "invalid ImpliesOp"; break;
+ case 130: s = "invalid AndOp"; break;
+ case 131: s = "invalid OrOp"; break;
+ case 132: s = "invalid RelOp"; break;
+ case 133: s = "invalid AddOp"; break;
+ case 134: s = "invalid UnaryExpression"; break;
+ case 135: s = "invalid MulOp"; break;
+ case 136: s = "invalid NegOp"; break;
+ case 137: s = "invalid EndlessExpression"; break;
case 138: s = "invalid Suffix"; break;
- case 139: s = "invalid DisplayExpr"; break;
- case 140: s = "invalid ConstAtomExpression"; break;
- case 141: s = "invalid QuantifierGuts"; break;
- case 142: s = "invalid Forall"; break;
- case 143: s = "invalid Exists"; break;
- case 144: s = "invalid AttributeOrTrigger"; break;
- case 145: s = "invalid QSep"; break;
+ case 139: s = "invalid Suffix"; break;
+ case 140: s = "invalid Suffix"; break;
+ case 141: s = "invalid DisplayExpr"; break;
+ case 142: s = "invalid ConstAtomExpression"; break;
+ case 143: s = "invalid QuantifierGuts"; break;
+ case 144: s = "invalid Forall"; break;
+ case 145: s = "invalid Exists"; break;
+ case 146: s = "invalid AttributeOrTrigger"; break;
+ case 147: s = "invalid QSep"; break;
default: s = "error " + n; break;
}
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index e49ce6e9..1bdc057e 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -788,9 +788,10 @@ namespace Microsoft.Dafny {
} else if (expr is DisplayExpression) {
DisplayExpression e = (DisplayExpression)expr;
- wr.Write(e is SetDisplayExpr ? "{" : "[");
+ if (e is MultiSetDisplayExpr) wr.Write("multi");
+ wr.Write(e is SetDisplayExpr || e is MultiSetDisplayExpr ? "{" : "[");
PrintExpressionList(e.Elements);
- wr.Write(e is SetDisplayExpr ? "}" : "]");
+ wr.Write(e is SetDisplayExpr || e is MultiSetDisplayExpr ? "}" : "]");
} else if (expr is FieldSelectExpr) {
FieldSelectExpr e = (FieldSelectExpr)expr;
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 197a603e..19a0da05 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -897,6 +897,8 @@ namespace Microsoft.Dafny {
return b is ObjectType;
} else if (a is SetType) {
return b is SetType && UnifyTypes(((SetType)a).Arg, ((SetType)b).Arg);
+ } else if (a is MultiSetType) {
+ return b is MultiSetType && UnifyTypes(((MultiSetType)a).Arg, ((MultiSetType)b).Arg);
} else if (a is SeqType) {
return b is SeqType && UnifyTypes(((SeqType)a).Arg, ((SeqType)b).Arg);
} else if (a is UserDefinedType) {
@@ -994,7 +996,7 @@ namespace Microsoft.Dafny {
} else if (proxy is OperationTypeProxy) {
OperationTypeProxy opProxy = (OperationTypeProxy)proxy;
- if (t is IntType || t is SetType || (opProxy.AllowSeq && t is SeqType)) {
+ if (t is IntType || t is SetType || t is MultiSetType || (opProxy.AllowSeq && t is SeqType)) {
// this is the expected case
} else {
return false;
@@ -2097,6 +2099,8 @@ namespace Microsoft.Dafny {
return type;
} else if (type is SetType) {
return new SetType(arg);
+ } else if (type is MultiSetType) {
+ return new MultiSetType(arg);
} else if (type is SeqType) {
return new SeqType(arg);
} else {
@@ -2301,6 +2305,8 @@ namespace Microsoft.Dafny {
}
if (expr is SetDisplayExpr) {
expr.Type = new SetType(elementType);
+ } else if (expr is MultiSetDisplayExpr) {
+ expr.Type = new MultiSetType(elementType);
} else {
expr.Type = new SeqType(elementType);
}
@@ -2477,12 +2483,13 @@ namespace Microsoft.Dafny {
break;
case BinaryExpr.Opcode.Disjoint:
- if (!UnifyTypes(e.E0.Type, new SetType(new InferredTypeProxy()))) {
- Error(expr, "arguments must be of a set type (got {0})", e.E0.Type);
- }
+ // TODO: the error messages are backwards from what (ideally) they should be. this is necessary because UnifyTypes can't backtrack.
if (!UnifyTypes(e.E0.Type, e.E1.Type)) {
Error(expr, "arguments must have the same type (got {0} and {1})", e.E0.Type, e.E1.Type);
}
+ if (!UnifyTypes(e.E0.Type, new SetType(new InferredTypeProxy())) && !UnifyTypes(e.E0.Type, new MultiSetType(new InferredTypeProxy()))) {
+ Error(expr, "arguments must be of a [multi]set type (got {0})", e.E0.Type);
+ }
expr.Type = Type.Bool;
break;
@@ -3137,6 +3144,12 @@ namespace Microsoft.Dafny {
goto CHECK_NEXT_BOUND_VARIABLE;
}
break;
+ case BinaryExpr.ResolvedOpcode.InMultiSet:
+ if (whereIsBv == 0) {
+ bounds.Add(new QuantifierExpr.SetBoundedPool(e1));
+ goto CHECK_NEXT_BOUND_VARIABLE;
+ }
+ break;
case BinaryExpr.ResolvedOpcode.InSeq:
if (whereIsBv == 0) {
bounds.Add(new QuantifierExpr.SeqBoundedPool(e1));
@@ -3553,6 +3566,8 @@ namespace Microsoft.Dafny {
case BinaryExpr.Opcode.Eq:
if (operandType is SetType) {
return BinaryExpr.ResolvedOpcode.SetEq;
+ } else if (operandType is MultiSetType) {
+ return BinaryExpr.ResolvedOpcode.MultiSetEq;
} else if (operandType is SeqType) {
return BinaryExpr.ResolvedOpcode.SeqEq;
} else {
@@ -3561,17 +3576,26 @@ namespace Microsoft.Dafny {
case BinaryExpr.Opcode.Neq:
if (operandType is SetType) {
return BinaryExpr.ResolvedOpcode.SetNeq;
+ } else if (operandType is MultiSetType) {
+ return BinaryExpr.ResolvedOpcode.MultiSetNeq;
} else if (operandType is SeqType) {
return BinaryExpr.ResolvedOpcode.SeqNeq;
} else {
return BinaryExpr.ResolvedOpcode.NeqCommon;
}
- case BinaryExpr.Opcode.Disjoint: return BinaryExpr.ResolvedOpcode.Disjoint;
+ case BinaryExpr.Opcode.Disjoint:
+ if (operandType is MultiSetType) {
+ return BinaryExpr.ResolvedOpcode.MultiSetDisjoint;
+ } else {
+ return BinaryExpr.ResolvedOpcode.Disjoint;
+ }
case BinaryExpr.Opcode.Lt:
if (operandType.IsDatatype) {
return BinaryExpr.ResolvedOpcode.RankLt;
} else if (operandType is SetType) {
return BinaryExpr.ResolvedOpcode.ProperSubset;
+ } else if (operandType is MultiSetType) {
+ return BinaryExpr.ResolvedOpcode.ProperMultiSubset;
} else if (operandType is SeqType) {
return BinaryExpr.ResolvedOpcode.ProperPrefix;
} else {
@@ -3580,6 +3604,8 @@ namespace Microsoft.Dafny {
case BinaryExpr.Opcode.Le:
if (operandType is SetType) {
return BinaryExpr.ResolvedOpcode.Subset;
+ } else if (operandType is MultiSetType) {
+ return BinaryExpr.ResolvedOpcode.MultiSubset;
} else if (operandType is SeqType) {
return BinaryExpr.ResolvedOpcode.Prefix;
} else {
@@ -3588,6 +3614,8 @@ namespace Microsoft.Dafny {
case BinaryExpr.Opcode.Add:
if (operandType is SetType) {
return BinaryExpr.ResolvedOpcode.Union;
+ } else if (operandType is MultiSetType) {
+ return BinaryExpr.ResolvedOpcode.MultiSetUnion;
} else if (operandType is SeqType) {
return BinaryExpr.ResolvedOpcode.Concat;
} else {
@@ -3596,12 +3624,16 @@ namespace Microsoft.Dafny {
case BinaryExpr.Opcode.Sub:
if (operandType is SetType) {
return BinaryExpr.ResolvedOpcode.SetDifference;
+ } else if (operandType is MultiSetType) {
+ return BinaryExpr.ResolvedOpcode.MultiSetDifference;
} else {
return BinaryExpr.ResolvedOpcode.Sub;
}
case BinaryExpr.Opcode.Mul:
if (operandType is SetType) {
return BinaryExpr.ResolvedOpcode.Intersection;
+ } else if (operandType is MultiSetType) {
+ return BinaryExpr.ResolvedOpcode.MultiSetIntersection;
} else {
return BinaryExpr.ResolvedOpcode.Mul;
}
@@ -3610,24 +3642,32 @@ namespace Microsoft.Dafny {
return BinaryExpr.ResolvedOpcode.RankGt;
} else if (operandType is SetType) {
return BinaryExpr.ResolvedOpcode.ProperSuperset;
+ } else if (operandType is MultiSetType) {
+ return BinaryExpr.ResolvedOpcode.ProperMultiSuperset;
} else {
return BinaryExpr.ResolvedOpcode.Gt;
}
case BinaryExpr.Opcode.Ge:
if (operandType is SetType) {
return BinaryExpr.ResolvedOpcode.Superset;
+ } else if (operandType is MultiSetType) {
+ return BinaryExpr.ResolvedOpcode.MultiSuperset;
} else {
return BinaryExpr.ResolvedOpcode.Ge;
}
case BinaryExpr.Opcode.In:
if (operandType is SetType) {
return BinaryExpr.ResolvedOpcode.InSet;
+ } else if (operandType is MultiSetType) {
+ return BinaryExpr.ResolvedOpcode.InMultiSet;
} else {
return BinaryExpr.ResolvedOpcode.InSeq;
}
case BinaryExpr.Opcode.NotIn:
if (operandType is SetType) {
return BinaryExpr.ResolvedOpcode.NotInSet;
+ } else if (operandType is MultiSetType) {
+ return BinaryExpr.ResolvedOpcode.NotInMultiSet;
} else {
return BinaryExpr.ResolvedOpcode.NotInSeq;
}
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index 81f556c8..a1fd9851 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/Dafny/Scanner.cs
@@ -211,8 +211,8 @@ public class UTF8Buffer: Buffer {
public class Scanner {
const char EOL = '\n';
const int eofSym = 0; /* pdt */
- const int maxT = 104;
- const int noSym = 104;
+ const int maxT = 106;
+ const int noSym = 106;
[ContractInvariantMethod]
@@ -510,36 +510,38 @@ public class Scanner {
case "nat": t.kind = 36; break;
case "int": t.kind = 37; break;
case "set": t.kind = 38; break;
- case "seq": t.kind = 39; break;
- case "object": t.kind = 40; break;
- case "function": t.kind = 41; break;
- case "reads": t.kind = 42; break;
- case "label": t.kind = 45; break;
- case "break": t.kind = 46; break;
- case "return": t.kind = 47; break;
- case "new": t.kind = 49; break;
- case "choose": t.kind = 53; break;
- case "if": t.kind = 54; break;
- case "else": t.kind = 55; break;
- case "case": t.kind = 56; break;
- case "while": t.kind = 58; break;
- case "invariant": t.kind = 59; break;
- case "match": t.kind = 60; break;
- case "foreach": t.kind = 61; break;
- case "in": t.kind = 62; break;
- case "assert": t.kind = 63; break;
- case "assume": t.kind = 64; break;
- case "print": t.kind = 65; break;
- case "false": t.kind = 89; break;
- case "true": t.kind = 90; break;
- case "null": t.kind = 91; break;
- case "this": t.kind = 92; break;
- case "fresh": t.kind = 93; break;
- case "allocated": t.kind = 94; break;
- case "old": t.kind = 95; break;
- case "then": t.kind = 96; break;
- case "forall": t.kind = 98; break;
- case "exists": t.kind = 100; break;
+ case "multiset": t.kind = 39; break;
+ case "seq": t.kind = 40; break;
+ case "object": t.kind = 41; break;
+ case "function": t.kind = 42; break;
+ case "reads": t.kind = 43; break;
+ case "label": t.kind = 46; break;
+ case "break": t.kind = 47; break;
+ case "return": t.kind = 48; break;
+ case "new": t.kind = 50; break;
+ case "choose": t.kind = 54; break;
+ case "if": t.kind = 55; break;
+ case "else": t.kind = 56; break;
+ case "case": t.kind = 57; break;
+ case "while": t.kind = 59; break;
+ case "invariant": t.kind = 60; break;
+ case "match": t.kind = 61; break;
+ case "foreach": t.kind = 62; break;
+ case "in": t.kind = 63; break;
+ case "assert": t.kind = 64; break;
+ case "assume": t.kind = 65; break;
+ case "print": t.kind = 66; break;
+ case "false": t.kind = 90; break;
+ case "true": t.kind = 91; break;
+ case "null": t.kind = 92; break;
+ case "this": t.kind = 93; break;
+ case "fresh": t.kind = 94; break;
+ case "allocated": t.kind = 95; break;
+ case "old": t.kind = 96; break;
+ case "multi": t.kind = 97; break;
+ case "then": t.kind = 98; break;
+ case "forall": t.kind = 100; break;
+ case "exists": t.kind = 102; break;
default: break;
}
}
@@ -653,76 +655,76 @@ public class Scanner {
case 22:
{t.kind = 34; break;}
case 23:
- {t.kind = 43; break;}
- case 24:
{t.kind = 44; break;}
+ case 24:
+ {t.kind = 45; break;}
case 25:
- {t.kind = 48; break;}
+ {t.kind = 49; break;}
case 26:
- {t.kind = 50; break;}
- case 27:
{t.kind = 51; break;}
+ case 27:
+ {t.kind = 52; break;}
case 28:
- {t.kind = 57; break;}
+ {t.kind = 58; break;}
case 29:
if (ch == '>') {AddCh(); goto case 30;}
else {goto case 0;}
case 30:
- {t.kind = 66; break;}
- case 31:
{t.kind = 67; break;}
- case 32:
+ case 31:
{t.kind = 68; break;}
- case 33:
+ case 32:
{t.kind = 69; break;}
+ case 33:
+ {t.kind = 70; break;}
case 34:
if (ch == '&') {AddCh(); goto case 35;}
else {goto case 0;}
case 35:
- {t.kind = 70; break;}
- case 36:
{t.kind = 71; break;}
- case 37:
+ case 36:
{t.kind = 72; break;}
- case 38:
+ case 37:
{t.kind = 73; break;}
+ case 38:
+ {t.kind = 74; break;}
case 39:
- {t.kind = 76; break;}
- case 40:
{t.kind = 77; break;}
- case 41:
+ case 40:
{t.kind = 78; break;}
+ case 41:
+ {t.kind = 79; break;}
case 42:
if (ch == 'n') {AddCh(); goto case 43;}
else {goto case 0;}
case 43:
- {t.kind = 79; break;}
- case 44:
{t.kind = 80; break;}
- case 45:
+ case 44:
{t.kind = 81; break;}
- case 46:
+ case 45:
{t.kind = 82; break;}
- case 47:
+ case 46:
{t.kind = 83; break;}
- case 48:
+ case 47:
{t.kind = 84; break;}
- case 49:
+ case 48:
{t.kind = 85; break;}
- case 50:
+ case 49:
{t.kind = 86; break;}
+ case 50:
+ {t.kind = 87; break;}
case 51:
- {t.kind = 88; break;}
+ {t.kind = 89; break;}
case 52:
- {t.kind = 97; break;}
- case 53:
{t.kind = 99; break;}
- case 54:
+ case 53:
{t.kind = 101; break;}
+ case 54:
+ {t.kind = 103; break;}
case 55:
- {t.kind = 102; break;}
+ {t.kind = 104; break;}
case 56:
- {t.kind = 103; break;}
+ {t.kind = 105; break;}
case 57:
recEnd = pos; recKind = 15;
if (ch == '>') {AddCh(); goto case 28;}
@@ -746,23 +748,23 @@ public class Scanner {
if (ch == '=') {AddCh(); goto case 39;}
else {t.kind = 24; break;}
case 62:
- recEnd = pos; recKind = 52;
+ recEnd = pos; recKind = 53;
if (ch == '.') {AddCh(); goto case 52;}
- else {t.kind = 52; break;}
+ else {t.kind = 53; break;}
case 63:
- recEnd = pos; recKind = 87;
+ recEnd = pos; recKind = 88;
if (ch == '=') {AddCh(); goto case 40;}
else if (ch == '!') {AddCh(); goto case 41;}
else if (ch == 'i') {AddCh(); goto case 42;}
- else {t.kind = 87; break;}
+ else {t.kind = 88; break;}
case 64:
- recEnd = pos; recKind = 74;
+ recEnd = pos; recKind = 75;
if (ch == '>') {AddCh(); goto case 32;}
- else {t.kind = 74; break;}
+ else {t.kind = 75; break;}
case 65:
- recEnd = pos; recKind = 75;
+ recEnd = pos; recKind = 76;
if (ch == '=') {AddCh(); goto case 29;}
- else {t.kind = 75; break;}
+ else {t.kind = 76; break;}
}
t.val = new String(tval, 0, tlen);
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index d1c77122..be18b658 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -43,6 +43,7 @@ namespace Microsoft.Dafny {
public readonly Bpl.Type BoxType;
public readonly Bpl.Type TickType;
private readonly Bpl.TypeSynonymDecl setTypeCtor;
+ private readonly Bpl.TypeSynonymDecl multiSetTypeCtor;
private readonly Bpl.TypeCtorDecl seqTypeCtor;
readonly Bpl.TypeCtorDecl fieldName;
public readonly Bpl.Type HeapType;
@@ -58,6 +59,7 @@ namespace Microsoft.Dafny {
Contract.Invariant(BoxType != null);
Contract.Invariant(TickType != null);
Contract.Invariant(setTypeCtor != null);
+ Contract.Invariant(multiSetTypeCtor != null);
Contract.Invariant(seqTypeCtor != null);
Contract.Invariant(fieldName != null);
Contract.Invariant(HeapType != null);
@@ -78,6 +80,14 @@ namespace Microsoft.Dafny {
return new Bpl.TypeSynonymAnnotation(Token.NoToken, setTypeCtor, new Bpl.TypeSeq(ty));
}
+ public Bpl.Type MultiSetType(IToken tok, Bpl.Type ty) {
+ Contract.Requires(tok != null);
+ Contract.Requires(ty != null);
+ Contract.Ensures(Contract.Result<Bpl.Type>() != null);
+
+ return new Bpl.TypeSynonymAnnotation(Token.NoToken, multiSetTypeCtor, new Bpl.TypeSeq(ty));
+ }
+
public Bpl.Type SeqType(IToken tok, Bpl.Type ty) {
Contract.Requires(tok != null);
Contract.Requires(ty != null);
@@ -101,7 +111,7 @@ namespace Microsoft.Dafny {
}
public PredefinedDecls(Bpl.TypeCtorDecl refType, Bpl.TypeCtorDecl boxType, Bpl.TypeCtorDecl tickType,
- Bpl.TypeSynonymDecl setTypeCtor, Bpl.TypeCtorDecl seqTypeCtor, Bpl.TypeCtorDecl fieldNameType,
+ Bpl.TypeSynonymDecl setTypeCtor, Bpl.TypeSynonymDecl multiSetTypeCtor, Bpl.TypeCtorDecl seqTypeCtor, Bpl.TypeCtorDecl fieldNameType,
Bpl.GlobalVariable heap, Bpl.TypeCtorDecl classNameType,
Bpl.TypeCtorDecl datatypeType, Bpl.TypeCtorDecl dtCtorId,
Bpl.Constant allocField) {
@@ -110,6 +120,7 @@ namespace Microsoft.Dafny {
Contract.Requires(boxType != null);
Contract.Requires(tickType != null);
Contract.Requires(setTypeCtor != null);
+ Contract.Requires(multiSetTypeCtor != null);
Contract.Requires(seqTypeCtor != null);
Contract.Requires(fieldNameType != null);
Contract.Requires(heap != null);
@@ -124,6 +135,7 @@ namespace Microsoft.Dafny {
this.BoxType = new Bpl.CtorType(Token.NoToken, boxType, new Bpl.TypeSeq());
this.TickType = new Bpl.CtorType(Token.NoToken, tickType, new Bpl.TypeSeq());
this.setTypeCtor = setTypeCtor;
+ this.multiSetTypeCtor = multiSetTypeCtor;
this.seqTypeCtor = seqTypeCtor;
this.fieldName = fieldNameType;
this.HeapType = heap.TypedIdent.Type;
@@ -142,9 +154,10 @@ namespace Microsoft.Dafny {
Console.WriteLine("Error: resolution errors encountered in Dafny prelude");
return null;
}
-
+
Bpl.TypeCtorDecl refType = null;
Bpl.TypeSynonymDecl setTypeCtor = null;
+ Bpl.TypeSynonymDecl multiSetTypeCtor = null;
Bpl.TypeCtorDecl seqTypeCtor = null;
Bpl.TypeCtorDecl fieldNameType = null;
Bpl.TypeCtorDecl classNameType = null;
@@ -179,6 +192,9 @@ namespace Microsoft.Dafny {
if (dt.Name == "Set") {
setTypeCtor = dt;
}
+ if (dt.Name == "MultiSet") {
+ multiSetTypeCtor = dt;
+ }
} else if (d is Bpl.Constant) {
Bpl.Constant c = (Bpl.Constant)d;
if (c.Name == "alloc") {
@@ -195,6 +211,8 @@ namespace Microsoft.Dafny {
Console.WriteLine("Error: Dafny prelude is missing declaration of type Seq");
} else if (setTypeCtor == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type Set");
+ } else if (multiSetTypeCtor == null) {
+ Console.WriteLine("Error: Dafny prelude is missing declaration of type MultiSet");
} else if (fieldNameType == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type Field");
} else if (classNameType == null) {
@@ -215,7 +233,7 @@ namespace Microsoft.Dafny {
Console.WriteLine("Error: Dafny prelude is missing declaration of constant alloc");
} else {
return new PredefinedDecls(refType, boxType, tickType,
- setTypeCtor, seqTypeCtor, fieldNameType, heap, classNameType, datatypeType, dtCtorId,
+ setTypeCtor, multiSetTypeCtor, seqTypeCtor, fieldNameType, heap, classNameType, datatypeType, dtCtorId,
allocField);
}
return null;
@@ -435,6 +453,20 @@ namespace Microsoft.Dafny {
rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, rhs);
q = new Bpl.ForallExpr(ctor.tok, bvs, Bpl.Expr.Imp(ante, Bpl.Expr.Lt(lhs, rhs)));
sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q));
+ } else if (arg.Type is MultiSetType) {
+ // axiom (forall params, d: Datatype :: 0 < arg[d] ==> DtRank(d) < DtRank(#dt.ctor(params)));
+ // that is:
+ // axiom (forall params, d: Datatype :: 0 < arg[Box(d)] ==> DtRank(d) < DtRank(#dt.ctor(params)));
+ CreateBoundVariables(ctor.Formals, out bvs, out args);
+ Bpl.Variable dVar = new Bpl.BoundVariable(arg.tok, new Bpl.TypedIdent(arg.tok, "d", predef.DatatypeType));
+ bvs.Add(dVar);
+ Bpl.IdentifierExpr ie = new Bpl.IdentifierExpr(arg.tok, dVar);
+ Bpl.Expr ante = Bpl.Expr.Gt(Bpl.Expr.SelectTok(arg.tok, args[i], FunctionCall(arg.tok, BuiltinFunction.Box, null, ie)), Bpl.Expr.Literal(0));
+ lhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, ie);
+ Bpl.Expr rhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);
+ rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, rhs);
+ q = new Bpl.ForallExpr(ctor.tok, bvs, Bpl.Expr.Imp(ante, Bpl.Expr.Lt(lhs, rhs)));
+ sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q));
}
i++;
}
@@ -2355,7 +2387,7 @@ namespace Microsoft.Dafny {
if (a == null) {
return null;
}
- Bpl.Expr t = new Bpl.IdentifierExpr(tok, ct is SetType ? "class.set" : "class.seq", predef.ClassNameType);
+ Bpl.Expr t = new Bpl.IdentifierExpr(tok, ct is SetType ? "class.set" : "class.seq", predef.ClassNameType); // ^^^ todo: this needs to talk about multisets too.
return FunctionCall(tok, BuiltinFunction.TypeTuple, null, t, a);
} else {
UserDefinedType ct = (UserDefinedType)type;
@@ -2891,6 +2923,8 @@ namespace Microsoft.Dafny {
return predef.DatatypeType;
} else if (type is SetType) {
return predef.SetType(Token.NoToken, predef.BoxType);
+ } else if (type is MultiSetType) {
+ return predef.MultiSetType(Token.NoToken, predef.BoxType);
} else if (type is SeqType) {
return predef.SeqType(Token.NoToken, predef.BoxType);
} else {
@@ -3194,6 +3228,10 @@ namespace Microsoft.Dafny {
Bpl.Expr oInS;
if (s.Collection.Type is SetType) {
oInS = etran.TrInSet(stmt.Tok, o, s.Collection, ((SetType)s.Collection.Type).Arg);
+ } else if (s.Collection.Type is MultiSetType) {
+ // should not be reached.
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
} else {
Bpl.BoundVariable iVar = new Bpl.BoundVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, "$i", Bpl.Type.Int));
Bpl.IdentifierExpr i = new Bpl.IdentifierExpr(stmt.Tok, iVar);
@@ -4016,7 +4054,22 @@ namespace Microsoft.Dafny {
Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(xSubT));
return new Bpl.ForallExpr(tok, new Bpl.VariableSeq(tVar), tr, Bpl.Expr.Imp(xSubT, wh));
}
-
+
+ } else if (type is MultiSetType) {
+ MultiSetType st = (MultiSetType)type;
+ // (forall t: BoxType :: { x[t] } 0 < x[t] ==> Unbox(t)-has-the-expected-type)
+ Bpl.BoundVariable tVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$t#" + otherTmpVarCount, predef.BoxType));
+ otherTmpVarCount++;
+ Bpl.Expr t = new Bpl.IdentifierExpr(tok, tVar);
+ Bpl.Expr xSubT = Bpl.Expr.Gt(Bpl.Expr.SelectTok(tok, x, t), Bpl.Expr.Literal(0));
+ Bpl.Expr unboxT = ExpressionTranslator.ModeledAsBoxType(st.Arg) ? t : FunctionCall(tok, BuiltinFunction.Unbox, TrType(st.Arg), t);
+
+ Bpl.Expr wh = GetWhereClause(tok, unboxT, st.Arg, etran);
+ if (wh != null) {
+ Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(xSubT));
+ return new Bpl.ForallExpr(tok, new Bpl.VariableSeq(tVar), tr, Bpl.Expr.Imp(xSubT, wh));
+ }
+
} else if (type is SeqType) {
SeqType st = (SeqType)type;
// (forall i: int :: { Seq#Index(x,i) }
@@ -4607,7 +4660,7 @@ namespace Microsoft.Dafny {
} else if (expr is BoogieWrapper) {
var e = (BoogieWrapper)expr;
return e.Expr;
-
+
} else if (expr is SetDisplayExpr) {
SetDisplayExpr e = (SetDisplayExpr)expr;
Bpl.Expr s = translator.FunctionCall(expr.tok, BuiltinFunction.SetEmpty, predef.BoxType);
@@ -4616,7 +4669,16 @@ namespace Microsoft.Dafny {
s = translator.FunctionCall(expr.tok, BuiltinFunction.SetUnionOne, predef.BoxType, s, ss);
}
return s;
-
+
+ } else if (expr is MultiSetDisplayExpr) { //^^^ todo: add multiset to BuiltinFunction
+ MultiSetDisplayExpr e = (MultiSetDisplayExpr)expr;
+ Bpl.Expr s = translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetEmpty, predef.BoxType);
+ foreach (Expression ee in e.Elements) {
+ Bpl.Expr ss = BoxIfNecessary(expr.tok, TrExpr(ee), cce.NonNull(ee.Type));
+ s = translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetUnionOne, predef.BoxType, s, ss);
+ }
+ return s;
+
} else if (expr is SeqDisplayExpr) {
SeqDisplayExpr e = (SeqDisplayExpr)expr;
Bpl.Expr s = translator.FunctionCall(expr.tok, BuiltinFunction.SeqEmpty, predef.BoxType);
@@ -4798,6 +4860,11 @@ namespace Microsoft.Dafny {
} else if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.NotInSet) {
Bpl.Expr arg = TrInSet(expr.tok, e0, e.E1, cce.NonNull(e.E0.Type)); // let TrInSet translate e.E1
return Bpl.Expr.Unary(expr.tok, UnaryOperator.Opcode.Not, arg);
+ } else if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.InMultiSet) {
+ return TrInMultiSet(expr.tok, e0, e.E1, cce.NonNull(e.E0.Type)); // let TrInMultiSet translate e.E1
+ } else if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.NotInMultiSet) {
+ Bpl.Expr arg = TrInMultiSet(expr.tok, e0, e.E1, cce.NonNull(e.E0.Type)); // let TrInMultiSet translate e.E1
+ return Bpl.Expr.Unary(expr.tok, UnaryOperator.Opcode.Not, arg);
}
Bpl.Expr e1 = TrExpr(e.E1);
BinaryOperator.Opcode bOpcode;
@@ -4840,7 +4907,9 @@ namespace Microsoft.Dafny {
case BinaryExpr.ResolvedOpcode.SetNeq:
return Bpl.Expr.Unary(expr.tok, UnaryOperator.Opcode.Not, translator.FunctionCall(expr.tok, BuiltinFunction.SetEqual, null, e0, e1));
case BinaryExpr.ResolvedOpcode.ProperSubset:
- return ProperSubset(expr.tok, e0, e1);
+ return Bpl.Expr.Binary(expr.tok, BinaryOperator.Opcode.And,
+ translator.FunctionCall(expr.tok, BuiltinFunction.SetSubset, null, e0, e1),
+ Bpl.Expr.Not(translator.FunctionCall(expr.tok, BuiltinFunction.SetEqual, null, e0, e1)));
case BinaryExpr.ResolvedOpcode.Subset:
return translator.FunctionCall(expr.tok, BuiltinFunction.SetSubset, null, e0, e1);
case BinaryExpr.ResolvedOpcode.Superset:
@@ -4853,12 +4922,43 @@ namespace Microsoft.Dafny {
return translator.FunctionCall(expr.tok, BuiltinFunction.SetDisjoint, null, e0, e1);
case BinaryExpr.ResolvedOpcode.InSet:
Contract.Assert(false); throw new cce.UnreachableException(); // this case handled above
+ case BinaryExpr.ResolvedOpcode.NotInSet:
+ Contract.Assert(false); throw new cce.UnreachableException(); // this case handled above
case BinaryExpr.ResolvedOpcode.Union:
return translator.FunctionCall(expr.tok, BuiltinFunction.SetUnion, translator.TrType(cce.NonNull((SetType)expr.Type).Arg), e0, e1);
case BinaryExpr.ResolvedOpcode.Intersection:
return translator.FunctionCall(expr.tok, BuiltinFunction.SetIntersection, translator.TrType(cce.NonNull((SetType)expr.Type).Arg), e0, e1);
case BinaryExpr.ResolvedOpcode.SetDifference:
return translator.FunctionCall(expr.tok, BuiltinFunction.SetDifference, translator.TrType(cce.NonNull((SetType)expr.Type).Arg), e0, e1);
+
+ case BinaryExpr.ResolvedOpcode.MultiSetEq:
+ return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetEqual, null, e0, e1);
+ case BinaryExpr.ResolvedOpcode.MultiSetNeq:
+ return Bpl.Expr.Unary(expr.tok, UnaryOperator.Opcode.Not, translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetEqual, null, e0, e1));
+ case BinaryExpr.ResolvedOpcode.ProperMultiSubset:
+ return Bpl.Expr.Binary(expr.tok, BinaryOperator.Opcode.And,
+ translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetSubset, null, e0, e1),
+ Bpl.Expr.Not(translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetEqual, null, e0, e1)));
+ case BinaryExpr.ResolvedOpcode.MultiSubset:
+ return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetSubset, null, e0, e1);
+ case BinaryExpr.ResolvedOpcode.MultiSuperset:
+ return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetSubset, null, e1, e0);
+ case BinaryExpr.ResolvedOpcode.ProperMultiSuperset:
+ return Bpl.Expr.Binary(expr.tok, BinaryOperator.Opcode.And,
+ translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetSubset, null, e1, e0),
+ Bpl.Expr.Not(translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetEqual, null, e0, e1)));
+ case BinaryExpr.ResolvedOpcode.MultiSetDisjoint:
+ return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetDisjoint, null, e0, e1);
+ case BinaryExpr.ResolvedOpcode.InMultiSet:
+ Contract.Assert(false); throw new cce.UnreachableException(); // this case handled above
+ case BinaryExpr.ResolvedOpcode.NotInMultiSet:
+ Contract.Assert(false); throw new cce.UnreachableException(); // this case handled above
+ case BinaryExpr.ResolvedOpcode.MultiSetUnion:
+ return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetUnion, translator.TrType(cce.NonNull((MultiSetType)expr.Type).Arg), e0, e1);
+ case BinaryExpr.ResolvedOpcode.MultiSetIntersection:
+ return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetIntersection, translator.TrType(cce.NonNull((MultiSetType)expr.Type).Arg), e0, e1);
+ case BinaryExpr.ResolvedOpcode.MultiSetDifference:
+ return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetDifference, translator.TrType(cce.NonNull((MultiSetType)expr.Type).Arg), e0, e1);
case BinaryExpr.ResolvedOpcode.SeqEq:
return translator.FunctionCall(expr.tok, BuiltinFunction.SeqEqual, null, e0, e1);
@@ -5173,7 +5273,49 @@ namespace Microsoft.Dafny {
}
return Bpl.Expr.SelectTok(tok, TrExpr(s), BoxIfNecessary(tok, elmt, elmtType));
}
-
+
+ /// <summary>
+ /// Translate like 0 < s[Box(elmt)], but try to avoid as many set functions as possible in the
+ /// translation, because such functions can mess up triggering.
+ /// </summary>
+ public Bpl.Expr TrInMultiSet(IToken tok, Bpl.Expr elmt, Expression s, Type elmtType) {
+ Contract.Requires(tok != null);
+ Contract.Requires(elmt != null);
+ Contract.Requires(s != null);
+ Contract.Requires(elmtType != null);
+
+ Contract.Ensures(Contract.Result<Bpl.Expr>() != null);
+
+ if (s is BinaryExpr) {
+ BinaryExpr bin = (BinaryExpr)s;
+ switch (bin.ResolvedOp) {
+ case BinaryExpr.ResolvedOpcode.MultiSetUnion:
+ return Bpl.Expr.Or(TrInMultiSet(tok, elmt, bin.E0, elmtType), TrInMultiSet(tok, elmt, bin.E1, elmtType));
+ case BinaryExpr.ResolvedOpcode.MultiSetIntersection:
+ return Bpl.Expr.And(TrInMultiSet(tok, elmt, bin.E0, elmtType), TrInMultiSet(tok, elmt, bin.E1, elmtType));
+ default:
+ break;
+ }
+ } else if (s is MultiSetDisplayExpr) {
+ MultiSetDisplayExpr disp = (MultiSetDisplayExpr)s;
+ Bpl.Expr disjunction = null;
+ foreach (Expression a in disp.Elements) {
+ Bpl.Expr disjunct = Bpl.Expr.Eq(elmt, TrExpr(a));
+ if (disjunction == null) {
+ disjunction = disjunct;
+ } else {
+ disjunction = Bpl.Expr.Or(disjunction, disjunct);
+ }
+ }
+ if (disjunction == null) {
+ return Bpl.Expr.False;
+ } else {
+ return disjunction;
+ }
+ }
+ return Bpl.Expr.Gt(Bpl.Expr.SelectTok(tok, TrExpr(s), BoxIfNecessary(tok, elmt, elmtType)), Bpl.Expr.Literal(0));
+ }
+
Bpl.QKeyValue TrAttributes(Attributes attrs) {
Bpl.QKeyValue kv = null;
while (attrs != null) {
@@ -5301,7 +5443,16 @@ namespace Microsoft.Dafny {
SetSubset,
SetDisjoint,
SetChoose,
-
+
+ MultiSetEmpty,
+ MultiSetUnionOne,
+ MultiSetUnion,
+ MultiSetIntersection,
+ MultiSetDifference,
+ MultiSetEqual,
+ MultiSetSubset,
+ MultiSetDisjoint,
+
SeqLength,
SeqEmpty,
SeqBuild,
@@ -5387,6 +5538,47 @@ namespace Microsoft.Dafny {
Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "Set#Choose", typeInstantiation, args);
+
+ case BuiltinFunction.MultiSetEmpty: {
+ Contract.Assert(args.Length == 0);
+ Contract.Assert(typeInstantiation != null);
+ Bpl.Type resultType = predef.MultiSetType(tok, typeInstantiation);
+ return Bpl.Expr.CoerceType(tok, FunctionCall(tok, "MultiSet#Empty", resultType, args), resultType);
+ }
+ case BuiltinFunction.MultiSetUnionOne:
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation != null);
+ return FunctionCall(tok, "MultiSet#UnionOne", predef.MultiSetType(tok, typeInstantiation), args);
+ case BuiltinFunction.MultiSetUnion:
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation != null);
+ return FunctionCall(tok, "MultiSet#Union", predef.MultiSetType(tok, typeInstantiation), args);
+ case BuiltinFunction.MultiSetIntersection:
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation != null);
+ return FunctionCall(tok, "MultiSet#Intersection", predef.MultiSetType(tok, typeInstantiation), args);
+ case BuiltinFunction.MultiSetDifference:
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation != null);
+ return FunctionCall(tok, "MultiSet#Difference", predef.MultiSetType(tok, typeInstantiation), args);
+ case BuiltinFunction.MultiSetEqual:
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation == null);
+ return FunctionCall(tok, "MultiSet#Equal", Bpl.Type.Bool, args);
+ case BuiltinFunction.MultiSetSubset:
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation == null);
+ return FunctionCall(tok, "MultiSet#Subset", Bpl.Type.Bool, args);
+ case BuiltinFunction.MultiSetDisjoint:
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation == null);
+ return FunctionCall(tok, "MultiSet#Disjoint", Bpl.Type.Bool, args);
+ // avoiding this for now
+ /*case BuiltinFunction.SetChoose:
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation != null);
+ return FunctionCall(tok, "Set#Choose", typeInstantiation, args);*/
+
case BuiltinFunction.SeqLength:
Contract.Assert(args.Length == 1);
Contract.Assert(typeInstantiation == null);
@@ -6033,6 +6225,8 @@ namespace Microsoft.Dafny {
if (newElements != e.Elements) {
if (expr is SetDisplayExpr) {
newExpr = new SetDisplayExpr(expr.tok, newElements);
+ } else if (expr is MultiSetDisplayExpr) {
+ newExpr = new MultiSetDisplayExpr(expr.tok, newElements);
} else {
newExpr = new SeqDisplayExpr(expr.tok, newElements);
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 13:08:31 +0000