From 454909184e73582e425cad56a526956d91b88dcc Mon Sep 17 00:00:00 2001 From: qunyanm Date: Thu, 14 May 2015 15:44:39 -0700 Subject: Allow MatchExpr and MatchStmt to have nested patterns. Such as function last(xs: List): T requires xs != Nil { match xs case Cons(y, Nil) => y case Cons(y, Cons(z, zs)) => last(Cons(z, zs)) } And function minus(x: Nat, y: Nat): Nat { match (x, y) case (Zero, _) => Zero case (Suc(_), Zero) => x case (Suc(a), Suc(b)) => minus(a, b) } --- Source/Dafny/Printer.cs | 60 ++++++++++++++++++++++++------------------------- 1 file changed, 30 insertions(+), 30 deletions(-) (limited to 'Source/Dafny/Printer.cs') diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index bf42c71a..0259f12c 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -901,17 +901,7 @@ namespace Microsoft.Dafny { wr.WriteLine(); Indent(caseInd); wr.Write("case {0}", mc.Id); - if (mc.Arguments.Count != 0) { - string sep = "("; - foreach (BoundVar bv in mc.Arguments) { - wr.Write("{0}{1}", sep, bv.DisplayName); - if (bv.Type is NonProxyType) { - wr.Write(": {0}", bv.Type); - } - sep = ", "; - } - wr.Write(")"); - } + PrintMatchCaseArgument(mc); wr.Write(" =>"); foreach (Statement bs in mc.Body) { wr.WriteLine(); @@ -1199,17 +1189,7 @@ namespace Microsoft.Dafny { bool isLastCase = i == e.Cases.Count - 1; Indent(ind); wr.Write("case {0}", mc.Id); - if (mc.Arguments.Count != 0) { - string sep = "("; - foreach (BoundVar bv in mc.Arguments) { - wr.Write("{0}{1}", sep, bv.DisplayName); - if (bv.Type is NonProxyType) { - wr.Write(": {0}", bv.Type); - } - sep = ", "; - } - wr.Write(")"); - } + PrintMatchCaseArgument(mc); wr.WriteLine(" =>"); PrintExtendedExpr(mc.Body, ind + IndentAmount, isLastCase, isLastCase && (parensNeeded || endWithCloseParen)); i++; @@ -1246,6 +1226,33 @@ namespace Microsoft.Dafny { } } + public void PrintMatchCaseArgument(MatchCase mc) { + if (mc.Arguments != null) { + if (mc.Arguments.Count != 0) { + string sep = "("; + foreach (BoundVar bv in mc.Arguments) { + wr.Write("{0}{1}", sep, bv.DisplayName); + if (bv.Type is NonProxyType) { + wr.Write(": {0}", bv.Type); + } + sep = ", "; + } + wr.Write(")"); + } + } else { + Contract.Assert(mc.CasePatterns != null); + if (mc.CasePatterns.Count != 0) { + string sep = "("; + foreach (var cp in mc.CasePatterns) { + wr.Write(sep); + PrintCasePattern(cp); + sep = ", "; + } + wr.Write(")"); + } + } + } + public void PrintExpression(Expression expr, bool isFollowedBySemicolon) { Contract.Requires(expr != null); PrintExpr(expr, 0, false, true, isFollowedBySemicolon, -1); @@ -1859,14 +1866,7 @@ namespace Microsoft.Dafny { foreach (var mc in e.Cases) { bool isLastCase = i == e.Cases.Count - 1; wr.Write(" case {0}", mc.Id); - if (mc.Arguments.Count != 0) { - string sep = "("; - foreach (BoundVar bv in mc.Arguments) { - wr.Write("{0}{1}", sep, bv.DisplayName); - sep = ", "; - } - wr.Write(")"); - } + PrintMatchCaseArgument(mc); wr.Write(" => "); PrintExpression(mc.Body, isRightmost && isLastCase, !parensNeeded && isFollowedBySemicolon); i++; -- cgit v1.2.3 From 10a8896ae40fd918abbb8caa616ac6ee0876ac1d Mon Sep 17 00:00:00 2001 From: qunyanm Date: Fri, 29 May 2015 16:29:15 -0700 Subject: Add an infinite set collection type. --- Binaries/DafnyPrelude.bpl | 91 ++ Source/Dafny/Cloner.cs | 9 +- Source/Dafny/Dafny.atg | 42 +- Source/Dafny/DafnyAst.cs | 51 +- Source/Dafny/Parser.cs | 1852 +++++++++++++++++---------------- Source/Dafny/Printer.cs | 6 +- Source/Dafny/RefinementTransformer.cs | 3 +- Source/Dafny/Resolver.cs | 111 +- Source/Dafny/Rewriter.cs | 12 +- Source/Dafny/Scanner.cs | 300 +++--- Source/Dafny/Translator.cs | 160 ++- Source/DafnyExtension/TokenTagger.cs | 1 + Test/dafny0/ISets.dfy | 40 + Test/dafny0/ISets.dfy.expect | 2 + Util/Emacs/dafny-mode.el | 2 +- Util/latex/dafny.sty | 2 +- Util/vim/dafny.vim | 2 +- 17 files changed, 1508 insertions(+), 1178 deletions(-) create mode 100644 Test/dafny0/ISets.dfy create mode 100644 Test/dafny0/ISets.dfy.expect (limited to 'Source/Dafny/Printer.cs') diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 74bdb63e..5ee8b845 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -20,6 +20,7 @@ const unique TInt : Ty; const unique TNat : Ty; const unique TReal : Ty; function TSet(Ty) : Ty; +function TISet(Ty) : Ty; function TMultiSet(Ty) : Ty; function TSeq(Ty) : Ty; function TMap(Ty, Ty) : Ty; @@ -27,6 +28,8 @@ function TIMap(Ty, Ty) : Ty; function Inv0_TSet(Ty) : Ty; axiom (forall t: Ty :: { TSet(t) } Inv0_TSet(TSet(t)) == t); +function Inv0_TISet(Ty) : Ty; +axiom (forall t: Ty :: { TISet(t) } Inv0_TISet(TISet(t)) == t); function Inv0_TSeq(Ty) : Ty; axiom (forall t: Ty :: { TSeq(t) } Inv0_TSeq(TSeq(t)) == t); function Inv0_TMultiSet(Ty) : Ty; @@ -52,6 +55,7 @@ const unique TagInt : TyTag; const unique TagNat : TyTag; const unique TagReal : TyTag; const unique TagSet : TyTag; +const unique TagISet : TyTag; const unique TagMultiSet : TyTag; const unique TagSeq : TyTag; const unique TagMap : TyTag; @@ -64,6 +68,7 @@ axiom Tag(TInt) == TagInt; axiom Tag(TNat) == TagNat; axiom Tag(TReal) == TagReal; axiom (forall t: Ty :: { TSet(t) } Tag(TSet(t)) == TagSet); +axiom (forall t: Ty :: { TISet(t) } Tag(TISet(t)) == TagISet); axiom (forall t: Ty :: { TMultiSet(t) } Tag(TMultiSet(t)) == TagMultiSet); axiom (forall t: Ty :: { TSeq(t) } Tag(TSeq(t)) == TagSeq); axiom (forall t, u: Ty :: { TMap(t,u) } Tag(TMap(t,u)) == TagMap); @@ -137,6 +142,9 @@ axiom (forall bx : Box :: axiom (forall bx : Box, t : Ty :: { $IsBox(bx, TSet(t)) } ( $IsBox(bx, TSet(t)) ==> $Box($Unbox(bx) : Set Box) == bx && $Is($Unbox(bx) : Set Box, TSet(t)))); +axiom (forall bx : Box, t : Ty :: + { $IsBox(bx, TISet(t)) } + ( $IsBox(bx, TISet(t)) ==> $Box($Unbox(bx) : ISet Box) == bx && $Is($Unbox(bx) : ISet Box, TISet(t)))); axiom (forall bx : Box, t : Ty :: { $IsBox(bx, TMultiSet(t)) } ( $IsBox(bx, TMultiSet(t)) ==> $Box($Unbox(bx) : MultiSet Box) == bx && $Is($Unbox(bx) : MultiSet Box, TMultiSet(t)))); @@ -187,6 +195,10 @@ axiom (forall v: Set Box, t0: Ty :: { $Is(v, TSet(t0)) } $Is(v, TSet(t0)) <==> (forall bx: Box :: { v[bx] } v[bx] ==> $IsBox(bx, t0))); +axiom (forall v: ISet Box, t0: Ty :: { $Is(v, TISet(t0)) } + $Is(v, TISet(t0)) <==> + (forall bx: Box :: { v[bx] } + v[bx] ==> $IsBox(bx, t0))); axiom (forall v: MultiSet Box, t0: Ty :: { $Is(v, TMultiSet(t0)) } $Is(v, TMultiSet(t0)) <==> (forall bx: Box :: { v[bx] } @@ -202,6 +214,10 @@ axiom (forall v: Set Box, t0: Ty, h: Heap :: { $IsAlloc(v, TSet(t0), h) } $IsAlloc(v, TSet(t0), h) <==> (forall bx: Box :: { v[bx] } v[bx] ==> $IsAllocBox(bx, t0, h))); +axiom (forall v: ISet Box, t0: Ty, h: Heap :: { $IsAlloc(v, TISet(t0), h) } + $IsAlloc(v, TISet(t0), h) <==> + (forall bx: Box :: { v[bx] } + v[bx] ==> $IsAllocBox(bx, t0, h))); axiom (forall v: MultiSet Box, t0: Ty, h: Heap :: { $IsAlloc(v, TMultiSet(t0), h) } $IsAlloc(v, TMultiSet(t0), h) <==> (forall bx: Box :: { v[bx] } @@ -544,6 +560,81 @@ function Set#Disjoint(Set T, Set T): bool; axiom (forall a: Set T, b: Set T :: { Set#Disjoint(a,b) } Set#Disjoint(a,b) <==> (forall o: T :: {a[o]} {b[o]} !a[o] || !b[o])); +// --------------------------------------------------------------- +// -- Axiomatization of isets ------------------------------------- +// --------------------------------------------------------------- + +type ISet T = [T]bool; + +function ISet#Empty(): Set T; +axiom (forall o: T :: { ISet#Empty()[o] } !ISet#Empty()[o]); + +// the empty set could be of anything +//axiom (forall t: Ty :: { $Is(ISet#Empty() : [T]bool, TISet(t)) } $Is(ISet#Empty() : [T]bool, TISet(t))); + + +function ISet#UnionOne(ISet T, T): ISet T; +axiom (forall a: ISet T, x: T, o: T :: { ISet#UnionOne(a,x)[o] } + ISet#UnionOne(a,x)[o] <==> o == x || a[o]); +axiom (forall a: ISet T, x: T :: { ISet#UnionOne(a, x) } + ISet#UnionOne(a, x)[x]); +axiom (forall a: ISet T, x: T, y: T :: { ISet#UnionOne(a, x), a[y] } + a[y] ==> ISet#UnionOne(a, x)[y]); + +function ISet#Union(ISet T, ISet T): ISet T; +axiom (forall a: ISet T, b: ISet T, o: T :: { ISet#Union(a,b)[o] } + ISet#Union(a,b)[o] <==> a[o] || b[o]); +axiom (forall a, b: ISet T, y: T :: { ISet#Union(a, b), a[y] } + a[y] ==> ISet#Union(a, b)[y]); +axiom (forall a, b: Set T, y: T :: { ISet#Union(a, b), b[y] } + b[y] ==> ISet#Union(a, b)[y]); +axiom (forall a, b: ISet T :: { ISet#Union(a, b) } + ISet#Disjoint(a, b) ==> + ISet#Difference(ISet#Union(a, b), a) == b && + ISet#Difference(ISet#Union(a, b), b) == a); +// Follows from the general union axiom, but might be still worth including, because disjoint union is a common case: +// axiom (forall a, b: ISet T :: { ISet#Card(ISet#Union(a, b)) } +// ISet#Disjoint(a, b) ==> +// ISet#Card(ISet#Union(a, b)) == ISet#Card(a) + ISet#Card(b)); + +function ISet#Intersection(ISet T, ISet T): ISet T; +axiom (forall a: ISet T, b: ISet T, o: T :: { ISet#Intersection(a,b)[o] } + ISet#Intersection(a,b)[o] <==> a[o] && b[o]); + +axiom (forall a, b: ISet T :: { ISet#Union(ISet#Union(a, b), b) } + ISet#Union(ISet#Union(a, b), b) == ISet#Union(a, b)); +axiom (forall a, b: Set T :: { ISet#Union(a, ISet#Union(a, b)) } + ISet#Union(a, ISet#Union(a, b)) == ISet#Union(a, b)); +axiom (forall a, b: ISet T :: { ISet#Intersection(ISet#Intersection(a, b), b) } + ISet#Intersection(ISet#Intersection(a, b), b) == ISet#Intersection(a, b)); +axiom (forall a, b: ISet T :: { ISet#Intersection(a, ISet#Intersection(a, b)) } + ISet#Intersection(a, ISet#Intersection(a, b)) == ISet#Intersection(a, b)); + + +function ISet#Difference(ISet T, ISet T): ISet T; +axiom (forall a: ISet T, b: ISet T, o: T :: { ISet#Difference(a,b)[o] } + ISet#Difference(a,b)[o] <==> a[o] && !b[o]); +axiom (forall a, b: ISet T, y: T :: { ISet#Difference(a, b), b[y] } + b[y] ==> !ISet#Difference(a, b)[y] ); + +function ISet#Subset(ISet T, ISet T): bool; +axiom(forall a: ISet T, b: ISet T :: { ISet#Subset(a,b) } + ISet#Subset(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] ==> b[o])); +// axiom(forall a: ISet T, b: ISet T :: +// { ISet#Subset(a,b), ISet#Card(a), ISet#Card(b) } // very restrictive trigger +// ISet#Subset(a,b) ==> ISet#Card(a) <= ISet#Card(b)); + + +function ISet#Equal(ISet T, ISet T): bool; +axiom(forall a: ISet T, b: ISet T :: { ISet#Equal(a,b) } + ISet#Equal(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] <==> b[o])); +axiom(forall a: ISet T, b: ISet T :: { ISet#Equal(a,b) } // extensionality axiom for sets + ISet#Equal(a,b) ==> a == b); + +function ISet#Disjoint(ISet T, ISet T): bool; +axiom (forall a: ISet T, b: ISet T :: { ISet#Disjoint(a,b) } + ISet#Disjoint(a,b) <==> (forall o: T :: {a[o]} {b[o]} !a[o] || !b[o])); + // --------------------------------------------------------------- // -- Axiomatization of multisets -------------------------------- // --------------------------------------------------------------- diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index f729d411..9b7bb12e 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -160,7 +160,7 @@ namespace Microsoft.Dafny return t; } else if (t is SetType) { var tt = (SetType)t; - return new SetType(CloneType(tt.Arg)); + return new SetType(tt.Finite, CloneType(tt.Arg)); } else if (t is SeqType) { var tt = (SeqType)t; return new SeqType(CloneType(tt.Arg)); @@ -187,7 +187,7 @@ namespace Microsoft.Dafny return new InferredTypeProxy(); } else if (t is OperationTypeProxy) { var p = (OperationTypeProxy)t; - return new OperationTypeProxy(p.AllowInts, p.AllowReals, p.AllowChar, p.AllowSeq, p.AllowSetVarieties); + return new OperationTypeProxy(p.AllowInts, p.AllowReals, p.AllowChar, p.AllowSeq, p.AllowSetVarieties, p.AllowISet); } else if (t is ParamTypeProxy) { return new ParamTypeProxy(CloneTypeParam(((ParamTypeProxy)t).orig)); } else { @@ -277,7 +277,7 @@ namespace Microsoft.Dafny } else if (expr is DisplayExpression) { DisplayExpression e = (DisplayExpression)expr; if (expr is SetDisplayExpr) { - return new SetDisplayExpr(Tok(e.tok), e.Elements.ConvertAll(CloneExpr)); + return new SetDisplayExpr(Tok(e.tok), ((SetDisplayExpr)expr).Finite, e.Elements.ConvertAll(CloneExpr)); } else if (expr is MultiSetDisplayExpr) { return new MultiSetDisplayExpr(Tok(e.tok), e.Elements.ConvertAll(CloneExpr)); } else { @@ -384,7 +384,8 @@ namespace Microsoft.Dafny return new LambdaExpr(tk, l.OneShot, bvs, range, l.Reads.ConvertAll(CloneFrameExpr), term); } else { Contract.Assert(e is SetComprehension); - return new SetComprehension(tk, bvs, range, term, CloneAttributes(e.Attributes)); + var tt = (SetComprehension)e; + return new SetComprehension(tk, tt.Finite, bvs, range, term, CloneAttributes(e.Attributes)); } } else if (expr is WildcardExpr) { diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 16cc09eb..b2b40629 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -175,6 +175,9 @@ bool IsMapDisplay() { bool IsIMapDisplay() { return la.kind == _imap && scanner.Peek().kind == _lbracket; } +bool IsISetDisplay() { + return la.kind == _iset && scanner.Peek().kind == _lbrace; +} bool IsSuffix() { return la.kind == _dot || la.kind == _lbracket || la.kind == _openparen; @@ -334,6 +337,7 @@ bool IsType(ref IToken pt) { return true; case _arrayToken: case _set: + case _iset: case _multiset: case _seq: case _map: @@ -416,6 +420,7 @@ TOKENS object = "object". string = "string". set = "set". + iset = "iset". multiset = "multiset". seq = "seq". map = "map". @@ -754,7 +759,7 @@ NewtypeDecl "=" ( IF(IsIdentColonOrBar()) NoUSIdent - [ ":" Type ] (. if (baseType == null) { baseType = new OperationTypeProxy(true, true, false, false, false); } .) + [ ":" Type ] (. if (baseType == null) { baseType = new OperationTypeProxy(true, true, false, false, false, false); } .) "|" Expression (. td = new NewtypeDecl(theVerifyThisFile ? id : new IncludeToken(id), id.val, module, new BoundVar(bvId, bvId.val, baseType), wh, attrs); .) | Type (. td = new NewtypeDecl(theVerifyThisFile ? id : new IncludeToken(id), id.val, module, baseType, attrs); .) @@ -1139,7 +1144,13 @@ TypeAndToken [ GenericInstantiation ] (. if (gt.Count > 1) { SemErr("set type expects only one type argument"); } - ty = new SetType(gt.Count == 1 ? gt[0] : null); + ty = new SetType(true, gt.Count == 1 ? gt[0] : null); + .) + | "iset" (. tok = t; gt = new List(); .) + [ GenericInstantiation ] (. if (gt.Count > 1) { + SemErr("set type expects only one type argument"); + } + ty = new SetType(false, gt.Count == 1 ? gt[0] : null); .) | "multiset" (. tok = t; gt = new List(); .) [ GenericInstantiation ] (. if (gt.Count > 1) { @@ -2324,10 +2335,13 @@ UnaryExpression "imap" (. x = t; .) MapDisplayExpr { IF(IsSuffix()) Suffix } + | IF(IsISetDisplay()) /* this alternative must be checked before going into EndlessExpression, where there is another "iset" */ + "iset" (. x = t; .) + ISetDisplayExpr + { IF(IsSuffix()) Suffix } | IF(IsLambda(allowLambda)) LambdaExpression /* this is an endless expression */ | EndlessExpression - | NameSegment { IF(IsSuffix()) Suffix } | DisplayExpr @@ -2432,13 +2446,22 @@ ParensExpression } .) . +ISetDisplayExpr += (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); + List elements = new List();; + e = dummyExpr; + .) + "{" + [ Expressions ] (. e = new SetDisplayExpr(setToken, finite, elements);.) + "}" + . DisplayExpr = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken x; List elements; e = dummyExpr; .) ( "{" (. x = t; elements = new List(); .) - [ Expressions ] (. e = new SetDisplayExpr(x, elements);.) + [ Expressions ] (. e = new SetDisplayExpr(x, true, elements);.) "}" | "[" (. x = t; elements = new List(); .) [ Expressions ] (. e = new SeqDisplayExpr(x, elements); .) @@ -2503,7 +2526,10 @@ EndlessExpression "else" Expression (. e = new ITEExpr(x, e, e0, e1); .) | MatchExpression | QuantifierGuts - | SetComprehensionExpr + | "set" (. x = t; .) + SetComprehensionExpr + | "iset" (. x = t; .) + SetComprehensionExpr | StmtInExpr Expression (. e = new StmtExpr(s.Tok, s, e); .) | LetExpr @@ -2842,16 +2868,14 @@ QuantifierDomain<.out List bvars, out Attributes attrs, out Expression ] . -SetComprehensionExpr +SetComprehensionExpr = (. Contract.Ensures(Contract.ValueAtReturn(out q) != null); - IToken x = Token.NoToken; BoundVar bv; List bvars = new List(); Expression range; Expression body = null; Attributes attrs = null; .) - "set" (. x = t; .) IdentTypeOptional (. bvars.Add(bv); .) { "," IdentTypeOptional (. bvars.Add(bv); .) @@ -2863,7 +2887,7 @@ SetComprehensionExpr Expression ] (. if (body == null && bvars.Count != 1) { SemErr(t, "a set comprehension with more than one bound variable must have a term expression"); } - q = new SetComprehension(x, bvars, range, body, attrs); + q = new SetComprehension(setToken, finite, bvars, range, body, attrs); .) . Expressions<.List args.> diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index a94b9a1b..b8660f98 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -165,7 +165,7 @@ namespace Microsoft.Dafny { var argExprs = args.ConvertAll(a => (Expression)new IdentifierExpr(tok, a.Name) { Var = a, Type = a.Type }); var readsIS = new FunctionCallExpr(tok, "reads", new ImplicitThisExpr(tok), tok, argExprs) { - Type = new SetType(new ObjectType()), + Type = new SetType(true, new ObjectType()), }; var readsFrame = new List { new FrameExpression(tok, readsIS, null) }; var req = new Function(tok, "requires", false, false, true, @@ -174,7 +174,7 @@ namespace Microsoft.Dafny { new Specification(new List(), null), null, null, null); var reads = new Function(tok, "reads", false, false, true, - new List(), args, new SetType(new ObjectType()), + new List(), args, new SetType(true, new ObjectType()), new List(), readsFrame, new List(), new Specification(new List(), null), null, null, null); @@ -535,6 +535,12 @@ namespace Microsoft.Dafny { return t != null && !t.Finite; } } + public bool IsISetType { + get { + var t = NormalizeExpand() as SetType; + return t != null && !t.Finite; + } + } public NewtypeDecl AsNewtype { get { var udt = NormalizeExpand() as UserDefinedType; @@ -633,7 +639,7 @@ namespace Microsoft.Dafny { /// public bool IsOrdered { get { - return !IsTypeParameter && !IsCoDatatype && !IsArrowType && !IsIMapType; + return !IsTypeParameter && !IsCoDatatype && !IsArrowType && !IsIMapType && !IsISetType; } } @@ -859,17 +865,25 @@ namespace Microsoft.Dafny { } public class SetType : CollectionType { - public SetType(Type arg) : base(arg) { + private bool finite; + + public bool Finite { + get { return finite; } + set { finite = value; } } - public override string CollectionTypeName { get { return "set"; } } + + public SetType(bool finite, Type arg) : base(arg) { + this.finite = finite; + } + public override string CollectionTypeName { get { return finite ? "set" : "iset"; } } [Pure] public override bool Equals(Type that) { var t = that.NormalizeExpand() as SetType; - return t != null && Arg.Equals(t.Arg); + return t != null && Finite == t.Finite && Arg.Equals(t.Arg); } public override bool PossiblyEquals_W(Type that) { var t = that as SetType; - return t != null && Arg.PossiblyEquals(t.Arg); + return t != null && Finite == t.Finite && Arg.PossiblyEquals(t.Arg); } } @@ -1312,20 +1326,22 @@ namespace Microsoft.Dafny { /// /// This proxy stands for: - /// set(Arg) or multiset(Arg) or seq(Arg) or map(Arg, anyRange) or imap(Arg, anyRange) + /// set(Arg) or iset(Arg) or multiset(Arg) or seq(Arg) or map(Arg, anyRange) or imap(Arg, anyRange) /// public class CollectionTypeProxy : RestrictedTypeProxy { public readonly Type Arg; public readonly bool AllowIMap; + public readonly bool AllowISet; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(Arg != null); } - public CollectionTypeProxy(Type arg, bool allowIMap) { + public CollectionTypeProxy(Type arg, bool allowIMap, bool allowISet) { Contract.Requires(arg != null); Arg = arg; AllowIMap = allowIMap; + AllowISet = allowISet; } public override int OrderID { get { @@ -1338,6 +1354,7 @@ namespace Microsoft.Dafny { /// This proxy can stand for any numeric type. /// In addition, if AllowSeq, then it can stand for a seq. /// In addition, if AllowSetVarieties, it can stand for a set or multiset. + /// In addition, if AllowISet, then it can stand for a iset /// public class OperationTypeProxy : RestrictedTypeProxy { public readonly bool AllowInts; @@ -1345,13 +1362,14 @@ namespace Microsoft.Dafny { public readonly bool AllowChar; public readonly bool AllowSeq; public readonly bool AllowSetVarieties; + public readonly bool AllowISet; public bool JustInts { - get { return AllowInts && !AllowReals && !AllowChar && !AllowSeq && !AllowSetVarieties; } + get { return AllowInts && !AllowReals && !AllowChar && !AllowSeq && !AllowSetVarieties && !AllowISet; } } public bool JustReals { - get { return !AllowInts && AllowReals && !AllowChar && !AllowSeq && !AllowSetVarieties; } + get { return !AllowInts && AllowReals && !AllowChar && !AllowSeq && !AllowSetVarieties && !AllowISet; } } - public OperationTypeProxy(bool allowInts, bool allowReals, bool allowChar, bool allowSeq, bool allowSetVarieties) { + public OperationTypeProxy(bool allowInts, bool allowReals, bool allowChar, bool allowSeq, bool allowSetVarieties, bool allowISet) { Contract.Requires(allowInts || allowReals || allowChar || allowSeq || allowSetVarieties); // don't allow unsatisfiable constraint Contract.Requires(!(!allowInts && !allowReals && allowChar && !allowSeq && !allowSetVarieties)); // to constrain to just char, don't use a proxy AllowInts = allowInts; @@ -1359,6 +1377,7 @@ namespace Microsoft.Dafny { AllowChar = allowChar; AllowSeq = allowSeq; AllowSetVarieties = allowSetVarieties; + AllowISet = allowISet; } public override int OrderID { get { @@ -5691,10 +5710,12 @@ namespace Microsoft.Dafny { } public class SetDisplayExpr : DisplayExpression { - public SetDisplayExpr(IToken tok, List elements) + public bool Finite; + public SetDisplayExpr(IToken tok, bool finite, List elements) : base(tok, elements) { Contract.Requires(tok != null); Contract.Requires(cce.NonNullElements(elements)); + Finite = finite; } } @@ -6683,9 +6704,10 @@ namespace Microsoft.Dafny { public class SetComprehension : ComprehensionExpr { + public readonly bool Finite; public readonly bool TermIsImplicit; - public SetComprehension(IToken tok, List bvars, Expression range, Expression term, Attributes attrs) + public SetComprehension(IToken tok, bool finite, List bvars, Expression range, Expression term, Attributes attrs) : base(tok, bvars, range, term ?? new IdentifierExpr(tok, bvars[0].Name), attrs) { Contract.Requires(tok != null); Contract.Requires(cce.NonNullElements(bvars)); @@ -6693,6 +6715,7 @@ namespace Microsoft.Dafny { Contract.Requires(range != null); TermIsImplicit = term == null; + Finite = finite; } } public class MapComprehension : ComprehensionExpr diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 162e23a3..fa41877f 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -27,51 +27,52 @@ public class Parser { public const int _object = 11; public const int _string = 12; public const int _set = 13; - public const int _multiset = 14; - public const int _seq = 15; - public const int _map = 16; - public const int _imap = 17; - public const int _charToken = 18; - public const int _stringToken = 19; - public const int _colon = 20; - public const int _comma = 21; - public const int _verticalbar = 22; - public const int _doublecolon = 23; - public const int _bullet = 24; - public const int _dot = 25; - public const int _semi = 26; - public const int _darrow = 27; - public const int _arrow = 28; - public const int _assume = 29; - public const int _calc = 30; - public const int _case = 31; - public const int _then = 32; - public const int _else = 33; - public const int _decreases = 34; - public const int _invariant = 35; - public const int _function = 36; - public const int _predicate = 37; - public const int _inductive = 38; - public const int _lemma = 39; - public const int _copredicate = 40; - public const int _modifies = 41; - public const int _reads = 42; - public const int _requires = 43; - public const int _lbrace = 44; - public const int _rbrace = 45; - public const int _lbracket = 46; - public const int _rbracket = 47; - public const int _openparen = 48; - public const int _closeparen = 49; - public const int _openAngleBracket = 50; - public const int _closeAngleBracket = 51; - public const int _eq = 52; - public const int _neq = 53; - public const int _neqAlt = 54; - public const int _star = 55; - public const int _notIn = 56; - public const int _ellipsis = 57; - public const int maxT = 136; + public const int _iset = 14; + public const int _multiset = 15; + public const int _seq = 16; + public const int _map = 17; + public const int _imap = 18; + public const int _charToken = 19; + public const int _stringToken = 20; + public const int _colon = 21; + public const int _comma = 22; + public const int _verticalbar = 23; + public const int _doublecolon = 24; + public const int _bullet = 25; + public const int _dot = 26; + public const int _semi = 27; + public const int _darrow = 28; + public const int _arrow = 29; + public const int _assume = 30; + public const int _calc = 31; + public const int _case = 32; + public const int _then = 33; + public const int _else = 34; + public const int _decreases = 35; + public const int _invariant = 36; + public const int _function = 37; + public const int _predicate = 38; + public const int _inductive = 39; + public const int _lemma = 40; + public const int _copredicate = 41; + public const int _modifies = 42; + public const int _reads = 43; + public const int _requires = 44; + public const int _lbrace = 45; + public const int _rbrace = 46; + public const int _lbracket = 47; + public const int _rbracket = 48; + public const int _openparen = 49; + public const int _closeparen = 50; + public const int _openAngleBracket = 51; + public const int _closeAngleBracket = 52; + public const int _eq = 53; + public const int _neq = 54; + public const int _neqAlt = 55; + public const int _star = 56; + public const int _notIn = 57; + public const int _ellipsis = 58; + public const int maxT = 137; const bool _T = true; const bool _x = false; @@ -245,6 +246,9 @@ bool IsMapDisplay() { bool IsIMapDisplay() { return la.kind == _imap && scanner.Peek().kind == _lbracket; } +bool IsISetDisplay() { + return la.kind == _iset && scanner.Peek().kind == _lbrace; +} bool IsSuffix() { return la.kind == _dot || la.kind == _lbracket || la.kind == _openparen; @@ -404,6 +408,7 @@ bool IsType(ref IToken pt) { return true; case _arrayToken: case _set: + case _iset: case _multiset: case _seq: case _map: @@ -515,9 +520,9 @@ bool IsType(ref IToken pt) { TraitDecl/*!*/ trait; Contract.Assert(defaultModule != null); - while (la.kind == 58) { + while (la.kind == 59) { Get(); - Expect(19); + Expect(20); { string parsedFile = t.filename; bool isVerbatimString; @@ -535,42 +540,42 @@ bool IsType(ref IToken pt) { } while (StartOf(1)) { switch (la.kind) { - case 59: case 60: case 62: { + case 60: case 61: case 63: { SubModuleDecl(defaultModule, out submodule); defaultModule.TopLevelDecls.Add(submodule); break; } - case 67: { + case 68: { ClassDecl(defaultModule, out c); defaultModule.TopLevelDecls.Add(c); break; } - case 73: case 74: { + case 74: case 75: { DatatypeDecl(defaultModule, out dt); defaultModule.TopLevelDecls.Add(dt); break; } - case 76: { + case 77: { NewtypeDecl(defaultModule, out td); defaultModule.TopLevelDecls.Add(td); break; } - case 77: { + case 78: { OtherTypeDecl(defaultModule, out td); defaultModule.TopLevelDecls.Add(td); break; } - case 78: { + case 79: { IteratorDecl(defaultModule, out iter); defaultModule.TopLevelDecls.Add(iter); break; } - case 69: { + case 70: { TraitDecl(defaultModule, out trait); defaultModule.TopLevelDecls.Add(trait); break; } - case 36: case 37: case 38: case 39: case 40: case 70: case 71: case 72: case 75: case 81: case 82: case 83: case 84: { + case 37: case 38: case 39: case 40: case 41: case 71: case 72: case 73: case 76: case 82: case 83: case 84: case 85: { ClassMemberDecl(membersDefaultClass, false, !DafnyOptions.O.AllowGlobals); break; } @@ -603,94 +608,94 @@ bool IsType(ref IToken pt) { bool isAbstract = false; bool opened = false; - if (la.kind == 59 || la.kind == 60) { - if (la.kind == 59) { + if (la.kind == 60 || la.kind == 61) { + if (la.kind == 60) { Get(); isAbstract = true; } - Expect(60); - while (la.kind == 44) { + Expect(61); + while (la.kind == 45) { Attribute(ref attrs); } NoUSIdent(out id); - if (la.kind == 61) { + if (la.kind == 62) { Get(); QualifiedModuleName(out idRefined); } module = new ModuleDefinition(id, id.val, isAbstract, false, idRefined == null ? null : idRefined, parent, attrs, false); - Expect(44); + Expect(45); module.BodyStartTok = t; while (StartOf(1)) { switch (la.kind) { - case 59: case 60: case 62: { + case 60: case 61: case 63: { SubModuleDecl(module, out sm); module.TopLevelDecls.Add(sm); break; } - case 67: { + case 68: { ClassDecl(module, out c); module.TopLevelDecls.Add(c); break; } - case 69: { + case 70: { TraitDecl(module, out trait); module.TopLevelDecls.Add(trait); break; } - case 73: case 74: { + case 74: case 75: { DatatypeDecl(module, out dt); module.TopLevelDecls.Add(dt); break; } - case 76: { + case 77: { NewtypeDecl(module, out td); module.TopLevelDecls.Add(td); break; } - case 77: { + case 78: { OtherTypeDecl(module, out td); module.TopLevelDecls.Add(td); break; } - case 78: { + case 79: { IteratorDecl(module, out iter); module.TopLevelDecls.Add(iter); break; } - case 36: case 37: case 38: case 39: case 40: case 70: case 71: case 72: case 75: case 81: case 82: case 83: case 84: { + case 37: case 38: case 39: case 40: case 41: case 71: case 72: case 73: case 76: case 82: case 83: case 84: case 85: { ClassMemberDecl(namedModuleDefaultClassMembers, false, !DafnyOptions.O.AllowGlobals); break; } } } - Expect(45); + Expect(46); module.BodyEndTok = t; module.TopLevelDecls.Add(new DefaultClassDecl(module, namedModuleDefaultClassMembers)); submodule = new LiteralModuleDecl(module, parent); - } else if (la.kind == 62) { + } else if (la.kind == 63) { Get(); - if (la.kind == 63) { + if (la.kind == 64) { Get(); opened = true; } NoUSIdent(out id); - if (la.kind == 64 || la.kind == 65) { - if (la.kind == 64) { + if (la.kind == 65 || la.kind == 66) { + if (la.kind == 65) { Get(); QualifiedModuleName(out idPath); submodule = new AliasModuleDecl(idPath, id, parent, opened); } else { Get(); QualifiedModuleName(out idPath); - if (la.kind == 66) { + if (la.kind == 67) { Get(); QualifiedModuleName(out idAssignment); } submodule = new ModuleFacadeDecl(idPath, id, parent, idAssignment, opened); } } - if (la.kind == 26) { - while (!(la.kind == 0 || la.kind == 26)) {SynErr(137); Get();} + if (la.kind == 27) { + while (!(la.kind == 0 || la.kind == 27)) {SynErr(138); Get();} Get(); errors.Warning(t, "the semi-colon that used to terminate a sub-module declaration has been deprecated; in the new syntax, just leave off the semi-colon"); } @@ -700,7 +705,7 @@ bool IsType(ref IToken pt) { submodule = new AliasModuleDecl(idPath, id, parent, opened); } - } else SynErr(138); + } else SynErr(139); } void ClassDecl(ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c) { @@ -714,31 +719,31 @@ bool IsType(ref IToken pt) { List members = new List(); IToken bodyStart; - while (!(la.kind == 0 || la.kind == 67)) {SynErr(139); Get();} - Expect(67); - while (la.kind == 44) { + while (!(la.kind == 0 || la.kind == 68)) {SynErr(140); Get();} + Expect(68); + while (la.kind == 45) { Attribute(ref attrs); } NoUSIdent(out id); - if (la.kind == 50) { + if (la.kind == 51) { GenericParameters(typeArgs); } - if (la.kind == 68) { + if (la.kind == 69) { Get(); Type(out trait); traits.Add(trait); - while (la.kind == 21) { + while (la.kind == 22) { Get(); Type(out trait); traits.Add(trait); } } - Expect(44); + Expect(45); bodyStart = t; while (StartOf(2)) { ClassMemberDecl(members, true, false); } - Expect(45); + Expect(46); c = new ClassDecl(id, id.val, module, typeArgs, members, attrs, traits); c.BodyStartTok = bodyStart; c.BodyEndTok = t; @@ -755,29 +760,29 @@ bool IsType(ref IToken pt) { IToken bodyStart = Token.NoToken; // dummy assignment bool co = false; - while (!(la.kind == 0 || la.kind == 73 || la.kind == 74)) {SynErr(140); Get();} - if (la.kind == 73) { + while (!(la.kind == 0 || la.kind == 74 || la.kind == 75)) {SynErr(141); Get();} + if (la.kind == 74) { Get(); - } else if (la.kind == 74) { + } else if (la.kind == 75) { Get(); co = true; - } else SynErr(141); - while (la.kind == 44) { + } else SynErr(142); + while (la.kind == 45) { Attribute(ref attrs); } NoUSIdent(out id); - if (la.kind == 50) { + if (la.kind == 51) { GenericParameters(typeArgs); } - Expect(64); + Expect(65); bodyStart = t; DatatypeMemberDecl(ctors); - while (la.kind == 22) { + while (la.kind == 23) { Get(); DatatypeMemberDecl(ctors); } - if (la.kind == 26) { - while (!(la.kind == 0 || la.kind == 26)) {SynErr(142); Get();} + if (la.kind == 27) { + while (!(la.kind == 0 || la.kind == 27)) {SynErr(143); Get();} Get(); errors.Warning(t, "the semi-colon that used to terminate a (co)datatype declaration has been deprecated; in the new syntax, just leave off the semi-colon"); } @@ -798,26 +803,26 @@ bool IsType(ref IToken pt) { Type baseType = null; Expression wh; - Expect(76); - while (la.kind == 44) { + Expect(77); + while (la.kind == 45) { Attribute(ref attrs); } NoUSIdent(out id); - Expect(64); + Expect(65); if (IsIdentColonOrBar()) { NoUSIdent(out bvId); - if (la.kind == 20) { + if (la.kind == 21) { Get(); Type(out baseType); } - if (baseType == null) { baseType = new OperationTypeProxy(true, true, false, false, false); } - Expect(22); + if (baseType == null) { baseType = new OperationTypeProxy(true, true, false, false, false, false); } + Expect(23); Expression(out wh, false, true); td = new NewtypeDecl(theVerifyThisFile ? id : new IncludeToken(id), id.val, module, new BoundVar(bvId, bvId.val, baseType), wh, attrs); } else if (StartOf(3)) { Type(out baseType); td = new NewtypeDecl(theVerifyThisFile ? id : new IncludeToken(id), id.val, module, baseType, attrs); - } else SynErr(143); + } else SynErr(144); } void OtherTypeDecl(ModuleDefinition module, out TopLevelDecl td) { @@ -828,35 +833,35 @@ bool IsType(ref IToken pt) { td = null; Type ty; - Expect(77); - while (la.kind == 44) { + Expect(78); + while (la.kind == 45) { Attribute(ref attrs); } NoUSIdent(out id); - if (la.kind == 48) { + if (la.kind == 49) { Get(); - Expect(52); - Expect(49); + Expect(53); + Expect(50); eqSupport = TypeParameter.EqualitySupportValue.Required; - if (la.kind == 50) { + if (la.kind == 51) { GenericParameters(typeArgs); } } else if (StartOf(4)) { - if (la.kind == 50) { + if (la.kind == 51) { GenericParameters(typeArgs); } - if (la.kind == 64) { + if (la.kind == 65) { Get(); Type(out ty); td = new TypeSynonymDecl(id, id.val, typeArgs, module, ty, attrs); } - } else SynErr(144); + } else SynErr(145); if (td == null) { td = new OpaqueTypeDecl(id, id.val, module, eqSupport, typeArgs, attrs); } - if (la.kind == 26) { - while (!(la.kind == 0 || la.kind == 26)) {SynErr(145); Get();} + if (la.kind == 27) { + while (!(la.kind == 0 || la.kind == 27)) {SynErr(146); Get();} Get(); errors.Warning(t, "the semi-colon that used to terminate an opaque-type declaration has been deprecated; in the new syntax, just leave off the semi-colon"); } @@ -885,19 +890,19 @@ bool IsType(ref IToken pt) { IToken bodyStart = Token.NoToken; IToken bodyEnd = Token.NoToken; - while (!(la.kind == 0 || la.kind == 78)) {SynErr(146); Get();} - Expect(78); - while (la.kind == 44) { + while (!(la.kind == 0 || la.kind == 79)) {SynErr(147); Get();} + Expect(79); + while (la.kind == 45) { Attribute(ref attrs); } NoUSIdent(out id); - if (la.kind == 48 || la.kind == 50) { - if (la.kind == 50) { + if (la.kind == 49 || la.kind == 51) { + if (la.kind == 51) { GenericParameters(typeArgs); } Formals(true, true, ins); - if (la.kind == 79 || la.kind == 80) { - if (la.kind == 79) { + if (la.kind == 80 || la.kind == 81) { + if (la.kind == 80) { Get(); } else { Get(); @@ -905,14 +910,14 @@ bool IsType(ref IToken pt) { } Formals(false, true, outs); } - } else if (la.kind == 57) { + } else if (la.kind == 58) { Get(); signatureEllipsis = t; - } else SynErr(147); + } else SynErr(148); while (StartOf(5)) { IteratorSpec(reads, mod, decreases, req, ens, yieldReq, yieldEns, ref readsAttrs, ref modAttrs, ref decrAttrs); } - if (la.kind == 44) { + if (la.kind == 45) { BlockStmt(out body, out bodyStart, out bodyEnd); } iter = new IteratorDecl(id, id.val, module, typeArgs, ins, outs, @@ -935,21 +940,21 @@ bool IsType(ref IToken pt) { List members = new List(); IToken bodyStart; - while (!(la.kind == 0 || la.kind == 69)) {SynErr(148); Get();} - Expect(69); - while (la.kind == 44) { + while (!(la.kind == 0 || la.kind == 70)) {SynErr(149); Get();} + Expect(70); + while (la.kind == 45) { Attribute(ref attrs); } NoUSIdent(out id); - if (la.kind == 50) { + if (la.kind == 51) { GenericParameters(typeArgs); } - Expect(44); + Expect(45); bodyStart = t; while (StartOf(2)) { ClassMemberDecl(members, true, false); } - Expect(45); + Expect(46); trait = new TraitDecl(id, id.val, module, typeArgs, members, attrs); trait.BodyStartTok = bodyStart; trait.BodyEndTok = t; @@ -963,11 +968,11 @@ bool IsType(ref IToken pt) { MemberModifiers mmod = new MemberModifiers(); IToken staticToken = null, protectedToken = null; - while (la.kind == 70 || la.kind == 71 || la.kind == 72) { - if (la.kind == 70) { + while (la.kind == 71 || la.kind == 72 || la.kind == 73) { + if (la.kind == 71) { Get(); mmod.IsGhost = true; - } else if (la.kind == 71) { + } else if (la.kind == 72) { Get(); mmod.IsStatic = true; staticToken = t; } else { @@ -975,7 +980,7 @@ bool IsType(ref IToken pt) { mmod.IsProtected = true; protectedToken = t; } } - if (la.kind == 75) { + if (la.kind == 76) { if (moduleLevelDecl) { SemErr(la, "fields are not allowed to be declared at the module level; instead, wrap the field in a 'class' declaration"); mmod.IsStatic = false; @@ -1003,21 +1008,21 @@ bool IsType(ref IToken pt) { MethodDecl(mmod, allowConstructors, out m); mm.Add(m); - } else SynErr(149); + } else SynErr(150); } void Attribute(ref Attributes attrs) { string name; var args = new List(); - Expect(44); - Expect(20); + Expect(45); + Expect(21); Expect(1); name = t.val; if (StartOf(7)) { Expressions(args); } - Expect(45); + Expect(46); attrs = new Attributes(name, args, attrs); } @@ -1035,7 +1040,7 @@ bool IsType(ref IToken pt) { IToken id; ids = new List(); Ident(out id); ids.Add(id); - while (la.kind == 25) { + while (la.kind == 26) { Get(); Ident(out id); ids.Add(id); @@ -1053,29 +1058,29 @@ bool IsType(ref IToken pt) { IToken/*!*/ id; TypeParameter.EqualitySupportValue eqSupport; - Expect(50); + Expect(51); NoUSIdent(out id); eqSupport = TypeParameter.EqualitySupportValue.Unspecified; - if (la.kind == 48) { + if (la.kind == 49) { Get(); - Expect(52); - Expect(49); + Expect(53); + Expect(50); eqSupport = TypeParameter.EqualitySupportValue.Required; } typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); - while (la.kind == 21) { + while (la.kind == 22) { Get(); NoUSIdent(out id); eqSupport = TypeParameter.EqualitySupportValue.Unspecified; - if (la.kind == 48) { + if (la.kind == 49) { Get(); - Expect(52); - Expect(49); + Expect(53); + Expect(50); eqSupport = TypeParameter.EqualitySupportValue.Required; } typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); } - Expect(51); + Expect(52); } void Type(out Type ty) { @@ -1088,16 +1093,16 @@ bool IsType(ref IToken pt) { Attributes attrs = null; IToken/*!*/ id; Type/*!*/ ty; - while (!(la.kind == 0 || la.kind == 75)) {SynErr(150); Get();} - Expect(75); + while (!(la.kind == 0 || la.kind == 76)) {SynErr(151); Get();} + Expect(76); if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); } - while (la.kind == 44) { + while (la.kind == 45) { Attribute(ref attrs); } FIdentType(out id, out ty); mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); - while (la.kind == 21) { + while (la.kind == 22) { Get(); FIdentType(out id, out ty); mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); @@ -1124,111 +1129,111 @@ bool IsType(ref IToken pt) { IToken signatureEllipsis = null; bool missingOpenParen; - if (la.kind == 36) { + if (la.kind == 37) { Get(); - if (la.kind == 81) { + if (la.kind == 82) { Get(); isFunctionMethod = true; } if (mmod.IsGhost) { SemErr(t, "functions cannot be declared 'ghost' (they are ghost by default)"); } - while (la.kind == 44) { + while (la.kind == 45) { Attribute(ref attrs); } NoUSIdent(out id); - if (la.kind == 48 || la.kind == 50) { - if (la.kind == 50) { + if (la.kind == 49 || la.kind == 51) { + if (la.kind == 51) { GenericParameters(typeArgs); } Formals(true, isFunctionMethod, formals); - Expect(20); + Expect(21); Type(out returnType); - } else if (la.kind == 57) { + } else if (la.kind == 58) { Get(); signatureEllipsis = t; - } else SynErr(151); - } else if (la.kind == 37) { + } else SynErr(152); + } else if (la.kind == 38) { Get(); isPredicate = true; - if (la.kind == 81) { + if (la.kind == 82) { Get(); isFunctionMethod = true; } if (mmod.IsGhost) { SemErr(t, "predicates cannot be declared 'ghost' (they are ghost by default)"); } - while (la.kind == 44) { + while (la.kind == 45) { Attribute(ref attrs); } NoUSIdent(out id); if (StartOf(8)) { - if (la.kind == 50) { + if (la.kind == 51) { GenericParameters(typeArgs); } missingOpenParen = true; - if (la.kind == 48) { + if (la.kind == 49) { Formals(true, isFunctionMethod, formals); missingOpenParen = false; } if (missingOpenParen) { errors.Warning(t, "with the new support of higher-order functions in Dafny, parentheses-less predicates are no longer supported; in the new syntax, parentheses are required for the declaration and uses of predicates, even if the predicate takes no additional arguments"); } - if (la.kind == 20) { + if (la.kind == 21) { Get(); SemErr(t, "predicates do not have an explicitly declared return type; it is always bool"); } - } else if (la.kind == 57) { + } else if (la.kind == 58) { Get(); signatureEllipsis = t; - } else SynErr(152); - } else if (la.kind == 38) { + } else SynErr(153); + } else if (la.kind == 39) { Get(); - Expect(37); + Expect(38); isIndPredicate = true; if (mmod.IsGhost) { SemErr(t, "inductive predicates cannot be declared 'ghost' (they are ghost by default)"); } - while (la.kind == 44) { + while (la.kind == 45) { Attribute(ref attrs); } NoUSIdent(out id); - if (la.kind == 48 || la.kind == 50) { - if (la.kind == 50) { + if (la.kind == 49 || la.kind == 51) { + if (la.kind == 51) { GenericParameters(typeArgs); } Formals(true, isFunctionMethod, formals); - if (la.kind == 20) { + if (la.kind == 21) { Get(); SemErr(t, "inductive predicates do not have an explicitly declared return type; it is always bool"); } - } else if (la.kind == 57) { + } else if (la.kind == 58) { Get(); signatureEllipsis = t; - } else SynErr(153); - } else if (la.kind == 40) { + } else SynErr(154); + } else if (la.kind == 41) { Get(); isCoPredicate = true; if (mmod.IsGhost) { SemErr(t, "copredicates cannot be declared 'ghost' (they are ghost by default)"); } - while (la.kind == 44) { + while (la.kind == 45) { Attribute(ref attrs); } NoUSIdent(out id); - if (la.kind == 48 || la.kind == 50) { - if (la.kind == 50) { + if (la.kind == 49 || la.kind == 51) { + if (la.kind == 51) { GenericParameters(typeArgs); } Formals(true, isFunctionMethod, formals); - if (la.kind == 20) { + if (la.kind == 21) { Get(); SemErr(t, "copredicates do not have an explicitly declared return type; it is always bool"); } - } else if (la.kind == 57) { + } else if (la.kind == 58) { Get(); signatureEllipsis = t; - } else SynErr(154); - } else SynErr(155); + } else SynErr(155); + } else SynErr(156); decreases = isIndPredicate || isCoPredicate ? null : new List(); while (StartOf(9)) { FunctionSpec(reqs, reads, ens, decreases); } - if (la.kind == 44) { + if (la.kind == 45) { FunctionBody(out body, out bodyStart, out bodyEnd); } if (DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom") && !Attributes.Contains(attrs, "imported")) { @@ -1282,36 +1287,36 @@ bool IsType(ref IToken pt) { IToken bodyStart = Token.NoToken; IToken bodyEnd = Token.NoToken; - while (!(StartOf(10))) {SynErr(156); Get();} + while (!(StartOf(10))) {SynErr(157); Get();} switch (la.kind) { - case 81: { + case 82: { Get(); break; } - case 39: { + case 40: { Get(); isLemma = true; break; } - case 82: { + case 83: { Get(); isCoLemma = true; break; } - case 83: { + case 84: { Get(); isCoLemma = true; errors.Warning(t, "the 'comethod' keyword has been deprecated; it has been renamed to 'colemma'"); break; } - case 38: { + case 39: { Get(); - Expect(39); + Expect(40); isIndLemma = true; break; } - case 84: { + case 85: { Get(); if (allowConstructor) { isConstructor = true; @@ -1321,7 +1326,7 @@ bool IsType(ref IToken pt) { break; } - default: SynErr(157); break; + default: SynErr(158); break; } keywordToken = t; if (isLemma) { @@ -1345,7 +1350,7 @@ bool IsType(ref IToken pt) { } } - while (la.kind == 44) { + while (la.kind == 45) { Attribute(ref attrs); } if (la.kind == 1) { @@ -1359,24 +1364,24 @@ bool IsType(ref IToken pt) { } } - if (la.kind == 48 || la.kind == 50) { - if (la.kind == 50) { + if (la.kind == 49 || la.kind == 51) { + if (la.kind == 51) { GenericParameters(typeArgs); } Formals(true, !mmod.IsGhost, ins); - if (la.kind == 80) { + if (la.kind == 81) { Get(); if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); } Formals(false, !mmod.IsGhost, outs); } - } else if (la.kind == 57) { + } else if (la.kind == 58) { Get(); signatureEllipsis = t; - } else SynErr(158); + } else SynErr(159); while (StartOf(11)) { MethodSpec(req, mod, ens, dec, ref decAttrs, ref modAttrs); } - if (la.kind == 44) { + if (la.kind == 45) { BlockStmt(out body, out bodyStart, out bodyEnd); } if (DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom") && !Attributes.Contains(attrs, "imported") && !Attributes.Contains(attrs, "decl") && theVerifyThisFile) { @@ -1411,11 +1416,11 @@ bool IsType(ref IToken pt) { IToken/*!*/ id; List formals = new List(); - while (la.kind == 44) { + while (la.kind == 45) { Attribute(ref attrs); } NoUSIdent(out id); - if (la.kind == 48) { + if (la.kind == 49) { FormalsOptionalIds(formals); } ctors.Add(new DatatypeCtor(id, id.val, formals, attrs)); @@ -1423,17 +1428,17 @@ bool IsType(ref IToken pt) { void FormalsOptionalIds(List/*!*/ formals) { Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; string/*!*/ name; bool isGhost; - Expect(48); + Expect(49); if (StartOf(12)) { TypeIdentOptional(out id, out name, out ty, out isGhost); formals.Add(new Formal(id, name, ty, true, isGhost)); - while (la.kind == 21) { + while (la.kind == 22) { Get(); TypeIdentOptional(out id, out name, out ty, out isGhost); formals.Add(new Formal(id, name, ty, true, isGhost)); } } - Expect(49); + Expect(50); } void FIdentType(out IToken/*!*/ id, out Type/*!*/ ty) { @@ -1445,14 +1450,14 @@ bool IsType(ref IToken pt) { } else if (la.kind == 2) { Get(); id = t; - } else SynErr(159); - Expect(20); + } else SynErr(160); + Expect(21); Type(out ty); } void OldSemi() { - if (la.kind == 26) { - while (!(la.kind == 0 || la.kind == 26)) {SynErr(160); Get();} + if (la.kind == 27) { + while (!(la.kind == 0 || la.kind == 27)) {SynErr(161); Get();} Get(); } } @@ -1461,7 +1466,7 @@ bool IsType(ref IToken pt) { Expression e0; IToken endTok; EquivExpression(out e, allowSemi, allowLambda); if (SemiFollowsCall(allowSemi, e)) { - Expect(26); + Expect(27); endTok = t; Expression(out e0, allowSemi, allowLambda); e = new StmtExpr(e.tok, @@ -1475,7 +1480,7 @@ bool IsType(ref IToken pt) { Contract.Ensures(Contract.ValueAtReturn(out id)!=null); Contract.Ensures(Contract.ValueAtReturn(out ty)!=null); isGhost = false; - if (la.kind == 70) { + if (la.kind == 71) { Get(); if (allowGhostKeyword) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); } } @@ -1485,7 +1490,7 @@ bool IsType(ref IToken pt) { void IdentType(out IToken/*!*/ id, out Type/*!*/ ty, bool allowWildcardId) { Contract.Ensures(Contract.ValueAtReturn(out id) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null); WildIdent(out id, allowWildcardId); - Expect(20); + Expect(21); Type(out ty); } @@ -1501,7 +1506,7 @@ bool IsType(ref IToken pt) { IToken id; Type ty; Type optType = null; WildIdent(out id, true); - if (la.kind == 20) { + if (la.kind == 21) { Get(); Type(out ty); optType = ty; @@ -1514,7 +1519,7 @@ bool IsType(ref IToken pt) { IToken id; Type ty; Type optType = null; WildIdent(out id, true); - if (la.kind == 20) { + if (la.kind == 21) { Get(); Type(out ty); optType = ty; @@ -1527,13 +1532,13 @@ bool IsType(ref IToken pt) { Contract.Ensures(Contract.ValueAtReturn(out ty)!=null); Contract.Ensures(Contract.ValueAtReturn(out identName)!=null); string name = null; id = Token.NoToken; ty = new BoolType()/*dummy*/; isGhost = false; - if (la.kind == 70) { + if (la.kind == 71) { Get(); isGhost = true; } if (StartOf(3)) { TypeAndToken(out id, out ty); - if (la.kind == 20) { + if (la.kind == 21) { Get(); UserDefinedType udt = ty as UserDefinedType; if (udt != null && udt.TypeArgs.Count == 0) { @@ -1547,9 +1552,9 @@ bool IsType(ref IToken pt) { } else if (la.kind == 2) { Get(); id = t; name = id.val; - Expect(20); + Expect(21); Type(out ty); - } else SynErr(161); + } else SynErr(162); if (name != null) { identName = name; } else { @@ -1597,20 +1602,33 @@ bool IsType(ref IToken pt) { case 13: { Get(); tok = t; gt = new List(); - if (la.kind == 50) { + if (la.kind == 51) { GenericInstantiation(gt); } if (gt.Count > 1) { SemErr("set type expects only one type argument"); } - ty = new SetType(gt.Count == 1 ? gt[0] : null); + ty = new SetType(true, gt.Count == 1 ? gt[0] : null); break; } case 14: { Get(); tok = t; gt = new List(); - if (la.kind == 50) { + if (la.kind == 51) { + GenericInstantiation(gt); + } + if (gt.Count > 1) { + SemErr("set type expects only one type argument"); + } + ty = new SetType(false, gt.Count == 1 ? gt[0] : null); + + break; + } + case 15: { + Get(); + tok = t; gt = new List(); + if (la.kind == 51) { GenericInstantiation(gt); } if (gt.Count > 1) { @@ -1620,10 +1638,10 @@ bool IsType(ref IToken pt) { break; } - case 15: { + case 16: { Get(); tok = t; gt = new List(); - if (la.kind == 50) { + if (la.kind == 51) { GenericInstantiation(gt); } if (gt.Count > 1) { @@ -1638,10 +1656,10 @@ bool IsType(ref IToken pt) { tok = t; ty = new UserDefinedType(tok, tok.val, null); break; } - case 16: { + case 17: { Get(); tok = t; gt = new List(); - if (la.kind == 50) { + if (la.kind == 51) { GenericInstantiation(gt); } if (gt.Count == 0) { @@ -1655,10 +1673,10 @@ bool IsType(ref IToken pt) { break; } - case 17: { + case 18: { Get(); tok = t; gt = new List(); - if (la.kind == 50) { + if (la.kind == 51) { GenericInstantiation(gt); } if (gt.Count == 0) { @@ -1675,7 +1693,7 @@ bool IsType(ref IToken pt) { case 5: { Get(); tok = t; gt = null; - if (la.kind == 50) { + if (la.kind == 51) { gt = new List(); GenericInstantiation(gt); } @@ -1684,19 +1702,19 @@ bool IsType(ref IToken pt) { break; } - case 48: { + case 49: { Get(); tok = t; tupleArgTypes = new List(); if (StartOf(3)) { Type(out ty); tupleArgTypes.Add(ty); - while (la.kind == 21) { + while (la.kind == 22) { Get(); Type(out ty); tupleArgTypes.Add(ty); } } - Expect(49); + Expect(50); if (tupleArgTypes.Count == 1) { // just return the type 'ty' } else { @@ -1711,11 +1729,11 @@ bool IsType(ref IToken pt) { Expression e; tok = t; NameSegmentForTypeName(out e); tok = t; - while (la.kind == 25) { + while (la.kind == 26) { Get(); Expect(1); tok = t; List typeArgs = null; - if (la.kind == 50) { + if (la.kind == 51) { typeArgs = new List(); GenericInstantiation(typeArgs); } @@ -1724,9 +1742,9 @@ bool IsType(ref IToken pt) { ty = new UserDefinedType(e.tok, e); break; } - default: SynErr(162); break; + default: SynErr(163); break; } - if (la.kind == 28) { + if (la.kind == 29) { Type t2; Get(); tok = t; @@ -1744,17 +1762,17 @@ bool IsType(ref IToken pt) { void Formals(bool incoming, bool allowGhostKeyword, List formals) { Contract.Requires(cce.NonNullElements(formals)); IToken id; Type ty; bool isGhost; - Expect(48); - if (la.kind == 1 || la.kind == 70) { + Expect(49); + if (la.kind == 1 || la.kind == 71) { GIdentType(allowGhostKeyword, out id, out ty, out isGhost); formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); - while (la.kind == 21) { + while (la.kind == 22) { Get(); GIdentType(allowGhostKeyword, out id, out ty, out isGhost); formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); } } - Expect(49); + Expect(50); } void IteratorSpec(List/*!*/ reads, List/*!*/ mod, List decreases, @@ -1763,45 +1781,45 @@ List/*!*/ yieldReq, List/*!* ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; bool isYield = false; Attributes ensAttrs = null; - while (!(StartOf(13))) {SynErr(163); Get();} - if (la.kind == 42) { + while (!(StartOf(13))) {SynErr(164); Get();} + if (la.kind == 43) { Get(); while (IsAttribute()) { Attribute(ref readsAttrs); } FrameExpression(out fe, false, false); reads.Add(fe); - while (la.kind == 21) { + while (la.kind == 22) { Get(); FrameExpression(out fe, false, false); reads.Add(fe); } OldSemi(); - } else if (la.kind == 41) { + } else if (la.kind == 42) { Get(); while (IsAttribute()) { Attribute(ref modAttrs); } FrameExpression(out fe, false, false); mod.Add(fe); - while (la.kind == 21) { + while (la.kind == 22) { Get(); FrameExpression(out fe, false, false); mod.Add(fe); } OldSemi(); } else if (StartOf(14)) { - if (la.kind == 85) { + if (la.kind == 86) { Get(); isFree = true; errors.Warning(t, "the 'free' keyword is soon to be deprecated"); } - if (la.kind == 87) { + if (la.kind == 88) { Get(); isYield = true; } - if (la.kind == 43) { + if (la.kind == 44) { Get(); Expression(out e, false, false); OldSemi(); @@ -1811,7 +1829,7 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { req.Add(new MaybeFreeExpression(e, isFree)); } - } else if (la.kind == 86) { + } else if (la.kind == 87) { Get(); while (IsAttribute()) { Attribute(ref ensAttrs); @@ -1824,27 +1842,27 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); } - } else SynErr(164); - } else if (la.kind == 34) { + } else SynErr(165); + } else if (la.kind == 35) { Get(); while (IsAttribute()) { Attribute(ref decrAttrs); } DecreasesList(decreases, false, false); OldSemi(); - } else SynErr(165); + } else SynErr(166); } void BlockStmt(out BlockStmt/*!*/ block, out IToken bodyStart, out IToken bodyEnd) { Contract.Ensures(Contract.ValueAtReturn(out block) != null); List body = new List(); - Expect(44); + Expect(45); bodyStart = t; while (StartOf(15)) { Stmt(body); } - Expect(45); + Expect(46); bodyEnd = t; block = new BlockStmt(bodyStart, bodyEnd, body); } @@ -1854,33 +1872,33 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Requires(cce.NonNullElements(req)); Contract.Requires(cce.NonNullElements(mod)); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(cce.NonNullElements(decreases)); Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; Attributes ensAttrs = null; - while (!(StartOf(16))) {SynErr(166); Get();} - if (la.kind == 41) { + while (!(StartOf(16))) {SynErr(167); Get();} + if (la.kind == 42) { Get(); while (IsAttribute()) { Attribute(ref modAttrs); } FrameExpression(out fe, false, false); mod.Add(fe); - while (la.kind == 21) { + while (la.kind == 22) { Get(); FrameExpression(out fe, false, false); mod.Add(fe); } OldSemi(); - } else if (la.kind == 43 || la.kind == 85 || la.kind == 86) { - if (la.kind == 85) { + } else if (la.kind == 44 || la.kind == 86 || la.kind == 87) { + if (la.kind == 86) { Get(); isFree = true; errors.Warning(t, "the 'free' keyword is soon to be deprecated"); } - if (la.kind == 43) { + if (la.kind == 44) { Get(); Expression(out e, false, false); OldSemi(); req.Add(new MaybeFreeExpression(e, isFree)); - } else if (la.kind == 86) { + } else if (la.kind == 87) { Get(); while (IsAttribute()) { Attribute(ref ensAttrs); @@ -1888,15 +1906,15 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out e, false, false); OldSemi(); ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); - } else SynErr(167); - } else if (la.kind == 34) { + } else SynErr(168); + } else if (la.kind == 35) { Get(); while (IsAttribute()) { Attribute(ref decAttrs); } DecreasesList(decreases, true, false); OldSemi(); - } else SynErr(168); + } else SynErr(169); } void FrameExpression(out FrameExpression fe, bool allowSemi, bool allowLambda) { @@ -1909,18 +1927,18 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (StartOf(7)) { Expression(out e, allowSemi, allowLambda); feTok = e.tok; - if (la.kind == 88) { + if (la.kind == 89) { Get(); Ident(out id); fieldName = id.val; feTok = id; } fe = new FrameExpression(feTok, e, fieldName); - } else if (la.kind == 88) { + } else if (la.kind == 89) { Get(); Ident(out id); fieldName = id.val; fe = new FrameExpression(id, new ImplicitThisExpr(id), fieldName); - } else SynErr(169); + } else SynErr(170); } void DecreasesList(List decreases, bool allowWildcard, bool allowLambda) { @@ -1932,7 +1950,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo decreases.Add(e); } - while (la.kind == 21) { + while (la.kind == 22) { Get(); PossiblyWildExpression(out e, allowLambda); if (!allowWildcard && e is WildcardExpr) { @@ -1946,15 +1964,15 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void GenericInstantiation(List/*!*/ gt) { Contract.Requires(cce.NonNullElements(gt)); Type/*!*/ ty; - Expect(50); + Expect(51); Type(out ty); gt.Add(ty); - while (la.kind == 21) { + while (la.kind == 22) { Get(); Type(out ty); gt.Add(ty); } - Expect(51); + Expect(52); } void NameSegmentForTypeName(out Expression e) { @@ -1962,7 +1980,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List typeArgs = null; Ident(out id); - if (la.kind == 50) { + if (la.kind == 51) { typeArgs = new List(); GenericInstantiation(typeArgs); } @@ -1975,28 +1993,28 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(decreases == null || cce.NonNullElements(decreases)); Expression/*!*/ e; FrameExpression/*!*/ fe; - while (!(StartOf(17))) {SynErr(170); Get();} - if (la.kind == 43) { + while (!(StartOf(17))) {SynErr(171); Get();} + if (la.kind == 44) { Get(); Expression(out e, false, false); OldSemi(); reqs.Add(e); - } else if (la.kind == 42) { + } else if (la.kind == 43) { Get(); PossiblyWildFrameExpression(out fe, false); reads.Add(fe); - while (la.kind == 21) { + while (la.kind == 22) { Get(); PossiblyWildFrameExpression(out fe, false); reads.Add(fe); } OldSemi(); - } else if (la.kind == 86) { + } else if (la.kind == 87) { Get(); Expression(out e, false, false); OldSemi(); ens.Add(e); - } else if (la.kind == 34) { + } else if (la.kind == 35) { Get(); if (decreases == null) { SemErr(t, "'decreases' clauses are meaningless for copredicates, so they are not allowed"); @@ -2005,37 +2023,37 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo DecreasesList(decreases, false, false); OldSemi(); - } else SynErr(171); + } else SynErr(172); } void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) { Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr; - Expect(44); + Expect(45); bodyStart = t; Expression(out e, true, true); - Expect(45); + Expect(46); bodyEnd = t; } void PossiblyWildFrameExpression(out FrameExpression fe, bool allowSemi) { Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr; - if (la.kind == 55) { + if (la.kind == 56) { Get(); fe = new FrameExpression(t, new WildcardExpr(t), null); } else if (StartOf(18)) { FrameExpression(out fe, allowSemi, false); - } else SynErr(172); + } else SynErr(173); } void PossiblyWildExpression(out Expression e, bool allowLambda) { Contract.Ensures(Contract.ValueAtReturn(out e)!=null); e = dummyExpr; - if (la.kind == 55) { + if (la.kind == 56) { Get(); e = new WildcardExpr(t); } else if (StartOf(7)) { Expression(out e, false, allowLambda); - } else SynErr(173); + } else SynErr(174); } void Stmt(List/*!*/ ss) { @@ -2052,92 +2070,92 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken bodyStart, bodyEnd; int breakCount; - while (!(StartOf(19))) {SynErr(174); Get();} + while (!(StartOf(19))) {SynErr(175); Get();} switch (la.kind) { - case 44: { + case 45: { BlockStmt(out bs, out bodyStart, out bodyEnd); s = bs; break; } - case 99: { + case 100: { AssertStmt(out s); break; } - case 29: { + case 30: { AssumeStmt(out s); break; } - case 100: { + case 101: { PrintStmt(out s); break; } - case 1: case 2: case 3: case 4: case 8: case 10: case 18: case 19: case 22: case 48: case 129: case 130: case 131: case 132: case 133: case 134: { + case 1: case 2: case 3: case 4: case 8: case 10: case 19: case 20: case 23: case 49: case 130: case 131: case 132: case 133: case 134: case 135: { UpdateStmt(out s); break; } - case 70: case 75: { + case 71: case 76: { VarDeclStatement(out s); break; } - case 96: { + case 97: { IfStmt(out s); break; } - case 97: { + case 98: { WhileStmt(out s); break; } - case 98: { + case 99: { MatchStmt(out s); break; } - case 101: case 102: { + case 102: case 103: { ForallStmt(out s); break; } - case 30: { + case 31: { CalcStmt(out s); break; } - case 103: { + case 104: { ModifyStmt(out s); break; } - case 89: { + case 90: { Get(); x = t; NoUSIdent(out id); - Expect(20); + Expect(21); OneStmt(out s); s.Labels = new LList