From f72015819c90a23b150b1d70147eb51c51e2d5ed Mon Sep 17 00:00:00 2001 From: Jason Koenig Date: Mon, 11 Jul 2011 15:33:45 -0700 Subject: Partial implementation of multisets. --- Binaries/DafnyPrelude.bpl | 103 +++++++ Source/Dafny/Dafny.atg | 15 +- Source/Dafny/DafnyAst.cs | 41 ++- Source/Dafny/Parser.cs | 670 +++++++++++++++++++++++---------------------- Source/Dafny/Printer.cs | 5 +- Source/Dafny/Resolver.cs | 50 +++- Source/Dafny/Scanner.cs | 144 +++++----- Source/Dafny/Translator.cs | 214 ++++++++++++++- 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(Set T, TickType): T; axiom (forall 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 o: T, ms: MultiSet T :: { ms[o] } 0 <= ms[o] ); + +function MultiSet#Empty(): MultiSet T; +axiom (forall o: T :: { MultiSet#Empty()[o] } MultiSet#Empty()[o] == 0); + +function MultiSet#Singleton(T): MultiSet T; +axiom (forall r: T :: { MultiSet#Singleton(r) } MultiSet#Singleton(r)[r] == 1); +axiom (forall 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(MultiSet T, T): MultiSet T; +// pure containment axiom (in the original multiset or is the added element) +axiom (forall 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 a: MultiSet T, x: T :: { MultiSet#UnionOne(a, x) } + MultiSet#UnionOne(a, x)[x] == a[x] + 1); +// non-decreasing +axiom (forall 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 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(MultiSet T, MultiSet T): MultiSet T; +// union-ing is the sum of the contents +axiom (forall 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 a, b: MultiSet T, y: T :: { MultiSet#Union(a, b), a[y] } + 0 < a[y] ==> 0 < MultiSet#Union(a, b)[y]); +axiom (forall 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 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(MultiSet T, MultiSet T): MultiSet T; +axiom (forall 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 a, b: MultiSet T :: { MultiSet#Intersection(MultiSet#Intersection(a, b), b) } + MultiSet#Intersection(MultiSet#Intersection(a, b), b) == MultiSet#Intersection(a, b)); +axiom (forall 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(MultiSet T, MultiSet T): MultiSet T; +axiom (forall 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 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(MultiSet T, MultiSet T): bool; +axiom(forall 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(MultiSet T, MultiSet T): bool; +axiom(forall 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 a: MultiSet T, b: MultiSet T :: { MultiSet#Equal(a,b) } + MultiSet#Equal(a,b) ==> a == b); + +function MultiSet#Disjoint(MultiSet T, MultiSet T): bool; +axiom (forall 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(Set T): MultiSet T; +axiom (forall 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(Set T, TickType): T; +//axiom (forall 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 } ty = new SetType(gt[0]); .) + | "multiset" (. tok = t; gt = new List(); .) + GenericInstantiation (. if (gt.Count != 1) { + SemErr("multiset type expects exactly one type argument"); + } + ty = new MultiSetType(gt[0]); + .) | "seq" (. tok = t; gt = new List(); .) GenericInstantiation (. if (gt.Count != 1) { @@ -1251,11 +1257,14 @@ ConstAtomExpression DisplayExpr = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); - IToken/*!*/ x; List/*!*/ elements; + IToken/*!*/ x = null; List/*!*/ elements; e = dummyExpr; + bool isMulti = false; .) - ( "{" (. x = t; elements = new List(); .) - [ Expressions ] (. e = new SetDisplayExpr(x, elements); .) + ( [ "multi" (. x = t; isMulti = true; .) ] + "{" (. if (!isMulti) x = t; elements = new List(); .) + [ Expressions ] (. if (isMulti) e = new MultiSetDisplayExpr(x, elements); + else e = new SetDisplayExpr(x, elements);.) "}" | "[" (. x = t; elements = new List(); .) [ Expressions ] (. 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() != 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 { /// /// 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. /// public class OperationTypeProxy : RestrictedTypeProxy { @@ -2062,7 +2075,7 @@ namespace Microsoft.Dafny { get { return Elements; } } } - + public class SetDisplayExpr : DisplayExpression { public SetDisplayExpr(IToken tok, List/*!*/ elements) : base(tok, elements) { @@ -2071,6 +2084,13 @@ namespace Microsoft.Dafny { } } + public class MultiSetDisplayExpr : DisplayExpression { + public MultiSetDisplayExpr(IToken tok, List/*!*/ elements) : base(tok, elements) { + Contract.Requires(tok != null); + Contract.Requires(cce.NonNullElements(elements)); + } + } + public class SeqDisplayExpr : DisplayExpression { public SeqDisplayExpr(IToken tok, List/*!*/ 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/*!*/ typeArgs) { @@ -442,7 +442,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List(); + 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(); GenericInstantiation(gt); @@ -730,11 +741,11 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List/*!*/ 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/*!*/ 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/*!*/ decreases) { tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/ List/*!*/ 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/*!*/ decreases) { GenericInstantiation(gt); } ty = new UserDefinedType(tok, tok.val, gt); - } else SynErr(112); + } else SynErr(114); } void FunctionSpec(List/*!*/ reqs, List/*!*/ reads, List/*!*/ ens, List/*!*/ decreases) { @@ -891,7 +902,7 @@ List/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ ss) { @@ -963,19 +974,19 @@ List/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ decreases) { Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Attributes.Argument/*!*/ arg; List args = new List(); - Expect(65); + Expect(66); x = t; AttributeArg(out arg); args.Add(arg); @@ -1079,14 +1090,14 @@ List/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ decreases) { List 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/*!*/ decreases) { List 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/*!*/ 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 cases = new List(); - 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/*!*/ decreases) { List bodyPrefix = new List(); Statement bodyAssign = null; - Expect(61); + Expect(62); x = t; range = new LiteralExpr(x, true); ty = new InferredTypeProxy(); @@ -1243,7 +1254,7 @@ List/*!*/ decreases) { Get(); Type(out ty); } - Expect(62); + Expect(63); Expression(out collection); if (la.kind == 16) { Get(); @@ -1251,8 +1262,8 @@ List/*!*/ 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/*!*/ decreases) { List rhss = null; AssignmentRhs r; - Expect(47); + Expect(48); returnTok = t; if (StartOf(12)) { Rhs(out r, null); @@ -1299,16 +1310,16 @@ List/*!*/ decreases) { List 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(); Expressions(ee); - Expect(51); + Expect(52); UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true); } else { @@ -1330,18 +1341,18 @@ List/*!*/ 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/*!*/ 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/*!*/ args) { @@ -1375,13 +1386,13 @@ List/*!*/ 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/*!*/ decreases) { List body; Expect(7); - while (la.kind == 56) { + while (la.kind == 57) { Get(); x = t; Expression(out e); - Expect(57); + Expect(58); body = new List(); while (StartOf(9)) { Stmt(body); @@ -1413,13 +1424,13 @@ List/*!*/ 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/*!*/ decreases) { List arguments = new List(); List body = new List(); - Expect(56); + Expect(57); x = t; Ident(out id); if (la.kind == 33) { @@ -1464,7 +1475,7 @@ List/*!*/ decreases) { } Expect(34); } - Expect(57); + Expect(58); while (StartOf(9)) { Stmt(body); } @@ -1479,13 +1490,13 @@ List/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ decreases) { List 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ elements; + IToken/*!*/ x = null; List/*!*/ elements; e = dummyExpr; + bool isMulti = false; - if (la.kind == 7) { - Get(); - x = t; elements = new List(); + 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(); 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(); 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/*!*/ 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/*!*/ 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/*!*/ decreases) { e = new FreshExpr(x, e); break; } - case 94: { + case 95: { Get(); x = t; Expect(33); @@ -2018,7 +2034,7 @@ List/*!*/ decreases) { e = new AllocatedExpr(x, e); break; } - case 95: { + case 96: { Get(); x = t; Expect(33); @@ -2043,7 +2059,7 @@ List/*!*/ decreases) { Expect(34); break; } - default: SynErr(140); break; + default: SynErr(142); break; } } @@ -2062,10 +2078,10 @@ List/*!*/ decreases) { Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; MatchCaseExpr/*!*/ c; List cases = new List(); - 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/*!*/ 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/*!*/ 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/*!*/ decreases) { List arguments = new List(); Expression/*!*/ body; - Expect(56); + Expect(57); x = t; Ident(out id); if (la.kind == 33) { @@ -2160,25 +2176,25 @@ List/*!*/ 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/*!*/ decreases) { es = new List(); 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/*!*/ 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() != 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)); } - + + /// + /// 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. + /// + 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() != 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); } -- cgit v1.2.3