From 456b38819dd1bdafdf2baaa59125ecf9910722ed Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Mon, 21 Nov 2011 22:40:44 -0800 Subject: Dafny: Added "type" declaration (syntax: "type X;"), which introduces an arbitrary type (like a global type parameter). In the future, a refined module may allow such types to be instantiated. --- Dafny/Compiler.cs | 5 +- Dafny/Dafny.atg | 17 +- Dafny/DafnyAst.cs | 22 +- Dafny/Parser.cs | 847 +++++++++++++++++++++++++++------------------------- Dafny/Printer.cs | 8 +- Dafny/Resolver.cs | 21 +- Dafny/Scanner.cs | 293 +++++++++--------- Dafny/Translator.cs | 8 +- 8 files changed, 648 insertions(+), 573 deletions(-) (limited to 'Dafny') diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs index d0e0cb0e..8e7f7631 100644 --- a/Dafny/Compiler.cs +++ b/Dafny/Compiler.cs @@ -74,7 +74,10 @@ namespace Microsoft.Dafny { } foreach (TopLevelDecl d in m.TopLevelDecls) { wr.WriteLine(); - if (d is DatatypeDecl) { + if (d is ArbitraryTypeDecl) { + var at = (ArbitraryTypeDecl)d; + Error("Arbitrary type ('{0}') cannot be compiled", at.Name); + } else if (d is DatatypeDecl) { DatatypeDecl dt = (DatatypeDecl)d; Indent(indent); wr.Write("public abstract class Base_{0}", dt.Name); diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg index 2eaaca7f..04b8d9fa 100644 --- a/Dafny/Dafny.atg +++ b/Dafny/Dafny.atg @@ -134,7 +134,7 @@ IGNORE cr + lf + tab /*------------------------------------------------------------------------*/ PRODUCTIONS Dafny -= (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; += (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at; Attributes attrs; IToken/*!*/ id; List theImports; List membersDefaultClass = new List(); ModuleDecl module; @@ -157,11 +157,13 @@ Dafny "{" (. module.BodyStartTok = t; .) { ClassDecl (. module.TopLevelDecls.Add(c); .) | DatatypeDecl (. module.TopLevelDecls.Add(dt); .) + | ArbitraryTypeDecl(. module.TopLevelDecls.Add(at); .) } "}" (. module.BodyEndTok = t; theModules.Add(module); .) - | ClassDecl (. defaultModule.TopLevelDecls.Add(c); .) - | DatatypeDecl (. defaultModule.TopLevelDecls.Add(dt); .) + | ClassDecl (. defaultModule.TopLevelDecls.Add(c); .) + | DatatypeDecl (. defaultModule.TopLevelDecls.Add(dt); .) + | ArbitraryTypeDecl (. defaultModule.TopLevelDecls.Add(at); .) | ClassMemberDecl } (. if (defaultModuleCreatedHere) { @@ -273,6 +275,15 @@ FieldDecl<.MemberModifiers mmod, List/*!*/ mm.> } ";" . +ArbitraryTypeDecl += (. IToken/*!*/ id; + Attributes attrs = null; + .) + "type" + { Attribute } + Ident (. at = new ArbitraryTypeDecl(id, id.val, module, attrs); .) + ";" + . CouplingInvDecl<.MemberModifiers mmod, List/*!*/ mm.> = (. Contract.Requires(cce.NonNullElements(mm)); Attributes attrs = null; diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs index 8272736c..83fa4645 100644 --- a/Dafny/DafnyAst.cs +++ b/Dafny/DafnyAst.cs @@ -169,7 +169,7 @@ namespace Microsoft.Dafny { return true; } else { UserDefinedType udt = this as UserDefinedType; - return udt != null && udt.ResolvedParam == null && !(udt.ResolvedClass is DatatypeDecl); + return udt != null && udt.ResolvedParam == null && udt.ResolvedClass is ClassDecl; } } } @@ -201,7 +201,6 @@ namespace Microsoft.Dafny { } public bool IsTypeParameter { get { - Contract.Ensures(!Contract.Result() || this is UserDefinedType && ((UserDefinedType)this).ResolvedParam != null); UserDefinedType ct = this as UserDefinedType; return ct != null && ct.ResolvedParam != null; } @@ -601,7 +600,6 @@ namespace Microsoft.Dafny { : base(tok, name, null) { Contract.Requires(tok != null); Contract.Requires(name != null); - } } @@ -653,7 +651,6 @@ namespace Microsoft.Dafny { Contract.Invariant(cce.NonNullElements(TypeArgs)); } - public TopLevelDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDecl/*!*/ module, List/*!*/ typeArgs, Attributes attributes) : base(tok, name, attributes) { Contract.Requires(tok != null); @@ -920,6 +917,23 @@ namespace Microsoft.Dafny { } } + public class ArbitraryTypeDecl : TopLevelDecl, TypeParameter.ParentType + { + public readonly TypeParameter TheType; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(TheType != null && Name == TheType.Name); + } + + public ArbitraryTypeDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDecl/*!*/ module, Attributes attributes) + : base(tok, name, module, new List(), attributes) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(module != null); + TheType = new TypeParameter(tok, name); + } + } + [ContractClass(typeof(IVariableContracts))] public interface IVariable { string/*!*/ Name { diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs index 583fcc61..d942582f 100644 --- a/Dafny/Parser.cs +++ b/Dafny/Parser.cs @@ -18,12 +18,12 @@ 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 = 105; const bool T = true; const bool x = false; const int minErrDist = 2; - + public Scanner/*!*/ scanner; public Errors/*!*/ errors; @@ -134,10 +134,10 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List= minErrDist) errors.SemErr(t, msg); errDist = 0; } - - public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { - Contract.Requires(tok != null); - Contract.Requires(msg != null); + + public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { + Contract.Requires(tok != null); + Contract.Requires(msg != null); errors.SemErr(tok, msg); } @@ -150,15 +150,15 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List theImports; List membersDefaultClass = new List(); ModuleDecl module; @@ -215,13 +215,16 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List/*!*/ mm, bool allowConstructors) { Contract.Requires(cce.NonNullElements(mm)); Method/*!*/ m; @@ -367,21 +386,21 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List/*!*/ typeArgs) { Contract.Requires(cce.NonNullElements(typeArgs)); IToken/*!*/ id; - Expect(23); + Expect(24); Ident(out id); typeArgs.Add(new TypeParameter(id, id.val)); while (la.kind == 19) { @@ -389,7 +408,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List/*!*/ mm) { @@ -430,8 +449,8 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List/*!*/ formals) { Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; string/*!*/ name; bool isGhost; - Expect(33); + Expect(34); if (StartOf(5)) { TypeIdentOptional(out id, out name, out ty, out isGhost); formals.Add(new Formal(id, name, ty, true, isGhost)); @@ -588,13 +607,13 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List/*!*/ gt; switch (la.kind) { - case 35: { + case 36: { Get(); tok = t; break; } - case 36: { + case 37: { Get(); tok = t; ty = new NatType(); break; } - case 37: { + case 38: { Get(); tok = t; ty = new IntType(); break; } - case 38: { + case 39: { Get(); tok = t; gt = new List(); GenericInstantiation(gt); @@ -702,7 +721,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List(); GenericInstantiation(gt); @@ -713,7 +732,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List(); GenericInstantiation(gt); @@ -724,17 +743,17 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List/*!*/ formals) { Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; bool isGhost; - Expect(33); + Expect(34); if (la.kind == 1 || la.kind == 11) { GIdentType(allowGhostKeyword, out id, out ty, out isGhost); formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); @@ -744,7 +763,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List/*!*/ req, List/*!*/ mod, List/*!*/ ens, @@ -752,7 +771,7 @@ List/*!*/ decreases) { 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; - if (la.kind == 28) { + if (la.kind == 29) { Get(); if (StartOf(6)) { FrameExpression(out fe); @@ -764,27 +783,27 @@ List/*!*/ decreases) { } } Expect(17); - } else if (la.kind == 29 || la.kind == 30 || la.kind == 31) { - if (la.kind == 29) { + } else if (la.kind == 30 || la.kind == 31 || la.kind == 32) { + if (la.kind == 30) { Get(); isFree = true; } - if (la.kind == 30) { + if (la.kind == 31) { Get(); Expression(out e); Expect(17); req.Add(new MaybeFreeExpression(e, isFree)); - } else if (la.kind == 31) { + } else if (la.kind == 32) { Get(); Expression(out e); Expect(17); ens.Add(new MaybeFreeExpression(e, isFree)); - } else SynErr(108); - } else if (la.kind == 32) { + } else SynErr(109); + } else if (la.kind == 33) { Get(); DecreasesList(decreases, false); Expect(17); - } else SynErr(109); + } else SynErr(110); } void BlockStmt(out Statement/*!*/ block, out IToken bodyStart, out IToken bodyEnd) { @@ -804,7 +823,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 == 45) { + if (la.kind == 46) { Get(); Ident(out id); fieldName = id.val; @@ -835,7 +854,7 @@ List/*!*/ decreases) { void GenericInstantiation(List/*!*/ gt) { Contract.Requires(cce.NonNullElements(gt)); Type/*!*/ ty; - Expect(23); + Expect(24); Type(out ty); gt.Add(ty); while (la.kind == 19) { @@ -843,7 +862,7 @@ List/*!*/ decreases) { Type(out ty); gt.Add(ty); } - Expect(24); + Expect(25); } void ReferenceType(out IToken/*!*/ tok, out Type/*!*/ ty) { @@ -851,7 +870,7 @@ List/*!*/ decreases) { tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/ List/*!*/ gt; - if (la.kind == 41) { + if (la.kind == 42) { Get(); tok = t; ty = new ObjectType(); } else if (la.kind == 3) { @@ -870,22 +889,22 @@ List/*!*/ decreases) { } else if (la.kind == 1) { Ident(out tok); gt = new List(); - if (la.kind == 23) { + if (la.kind == 24) { GenericInstantiation(gt); } ty = new UserDefinedType(tok, tok.val, gt); - } else SynErr(110); + } else SynErr(111); } void FunctionSpec(List/*!*/ reqs, List/*!*/ reads, List/*!*/ ens, List/*!*/ decreases) { Contract.Requires(cce.NonNullElements(reqs)); Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(cce.NonNullElements(decreases)); Expression/*!*/ e; FrameExpression/*!*/ fe; - if (la.kind == 30) { + if (la.kind == 31) { Get(); Expression(out e); Expect(17); reqs.Add(e); - } else if (la.kind == 43) { + } else if (la.kind == 44) { Get(); if (StartOf(8)) { PossiblyWildFrameExpression(out fe); @@ -897,16 +916,16 @@ List/*!*/ decreases) { } } Expect(17); - } else if (la.kind == 31) { + } else if (la.kind == 32) { Get(); Expression(out e); Expect(17); ens.Add(e); - } else if (la.kind == 32) { + } else if (la.kind == 33) { Get(); DecreasesList(decreases, false); Expect(17); - } else SynErr(111); + } else SynErr(112); } void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) { @@ -920,23 +939,23 @@ List/*!*/ decreases) { void PossiblyWildFrameExpression(out FrameExpression/*!*/ fe) { Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr; - if (la.kind == 44) { + if (la.kind == 45) { Get(); fe = new FrameExpression(new WildcardExpr(t), null); } else if (StartOf(6)) { FrameExpression(out fe); - } else SynErr(112); + } else SynErr(113); } void PossiblyWildExpression(out Expression/*!*/ e) { Contract.Ensures(Contract.ValueAtReturn(out e)!=null); e = dummyExpr; - if (la.kind == 44) { + if (la.kind == 45) { Get(); e = new WildcardExpr(t); } else if (StartOf(6)) { Expression(out e); - } else SynErr(113); + } else SynErr(114); } void Stmt(List/*!*/ ss) { @@ -957,19 +976,19 @@ List/*!*/ decreases) { BlockStmt(out s, out bodyStart, out bodyEnd); break; } - case 62: { + case 63: { AssertStmt(out s); break; } - case 63: { + case 64: { AssumeStmt(out s); break; } - case 64: { + case 65: { 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 34: case 90: case 91: case 92: case 93: case 94: case 95: case 96: { UpdateStmt(out s); break; } @@ -977,58 +996,58 @@ List/*!*/ decreases) { VarDeclStatement(out s); break; } - case 55: { + case 56: { IfStmt(out s); break; } - case 59: { + case 60: { WhileStmt(out s); break; } - case 61: { + case 62: { MatchStmt(out s); break; } - case 65: { + case 66: { ParallelStmt(out s); break; } - case 46: { + case 47: { Get(); x = t; Ident(out id); - Expect(22); + Expect(23); OneStmt(out s); s.Labels = new LabelNode(x, id.val, s.Labels); break; } - case 47: { + case 48: { Get(); x = t; breakCount = 1; label = null; if (la.kind == 1) { Ident(out id); label = id.val; - } else if (la.kind == 17 || la.kind == 47) { - while (la.kind == 47) { + } else if (la.kind == 17 || la.kind == 48) { + while (la.kind == 48) { Get(); breakCount++; } - } else SynErr(114); + } else SynErr(115); Expect(17); s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); break; } - case 48: { + case 49: { ReturnStmt(out s); break; } - default: SynErr(115); break; + default: SynErr(116); break; } } void AssertStmt(out Statement/*!*/ s) { Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e; - Expect(62); + Expect(63); x = t; Expression(out e); Expect(17); @@ -1037,7 +1056,7 @@ List/*!*/ decreases) { void AssumeStmt(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); @@ -1048,7 +1067,7 @@ List/*!*/ decreases) { Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Attributes.Argument/*!*/ arg; List args = new List(); - Expect(64); + Expect(65); x = t; AttributeArg(out arg); args.Add(arg); @@ -1073,14 +1092,14 @@ List/*!*/ decreases) { if (la.kind == 17) { Get(); rhss.Add(new ExprRhs(e)); - } else if (la.kind == 19 || la.kind == 49) { + } else if (la.kind == 19 || la.kind == 50) { lhss.Add(e); lhs0 = e; while (la.kind == 19) { Get(); Lhs(out e); lhss.Add(e); } - Expect(49); + Expect(50); x = t; Rhs(out r, lhs0); rhss.Add(r); @@ -1090,10 +1109,10 @@ List/*!*/ decreases) { rhss.Add(r); } Expect(17); - } else if (la.kind == 22) { + } else if (la.kind == 23) { Get(); SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); - } else SynErr(116); + } else SynErr(117); s = new UpdateStmt(x, lhss, rhss); } @@ -1117,7 +1136,7 @@ List/*!*/ decreases) { LocalIdentTypeOptional(out d, isGhost); lhss.Add(d); } - if (la.kind == 49) { + if (la.kind == 50) { Get(); assignTok = t; lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name); @@ -1156,26 +1175,26 @@ List/*!*/ decreases) { List alternatives; ifStmt = dummyStmt; // to please the compiler - Expect(55); + Expect(56); x = t; - if (la.kind == 33) { + if (la.kind == 34) { Guard(out guard); BlockStmt(out thn, out bodyStart, out bodyEnd); - if (la.kind == 56) { + if (la.kind == 57) { Get(); - if (la.kind == 55) { + if (la.kind == 56) { IfStmt(out s); els = s; } else if (la.kind == 7) { BlockStmt(out s, out bodyStart, out bodyEnd); els = s; - } else SynErr(117); + } else SynErr(118); } ifStmt = new IfStmt(x, guard, thn, els); } else if (la.kind == 7) { AlternativeBlock(out alternatives); ifStmt = new AlternativeStmt(x, alternatives); - } else SynErr(118); + } else SynErr(119); } void WhileStmt(out Statement/*!*/ stmt) { @@ -1189,9 +1208,9 @@ List/*!*/ decreases) { List alternatives; stmt = dummyStmt; // to please the compiler - Expect(59); + Expect(60); x = t; - if (la.kind == 33) { + if (la.kind == 34) { Guard(out guard); Contract.Assume(guard == null || cce.Owner.None(guard)); LoopSpec(out invariants, out decreases, out mod); @@ -1201,18 +1220,18 @@ List/*!*/ decreases) { LoopSpec(out invariants, out decreases, out mod); AlternativeBlock(out alternatives); stmt = new AlternativeLoopStmt(x, invariants, decreases, mod, alternatives); - } else SynErr(119); + } else SynErr(120); } void MatchStmt(out Statement/*!*/ s) { Contract.Ensures(Contract.ValueAtReturn(out s) != null); Token x; Expression/*!*/ e; MatchCaseStmt/*!*/ c; List cases = new List(); - Expect(61); + Expect(62); x = t; Expression(out e); Expect(7); - while (la.kind == 57) { + while (la.kind == 58) { CaseStatement(out c); cases.Add(c); } @@ -1232,19 +1251,19 @@ List/*!*/ decreases) { Statement/*!*/ block; IToken bodyStart, bodyEnd; - Expect(65); + Expect(66); x = t; - Expect(33); + Expect(34); QuantifierDomain(out bvars, out attrs, out range); if (range == null) { range = new LiteralExpr(x, true); } - Expect(34); - while (la.kind == 29 || la.kind == 31) { + Expect(35); + while (la.kind == 30 || la.kind == 32) { isFree = false; - if (la.kind == 29) { + if (la.kind == 30) { Get(); isFree = true; } - Expect(31); + Expect(32); Expression(out e); Expect(17); ens.Add(new MaybeFreeExpression(e, isFree)); @@ -1258,7 +1277,7 @@ List/*!*/ decreases) { List rhss = null; AssignmentRhs r; - Expect(48); + Expect(49); returnTok = t; if (StartOf(10)) { Rhs(out r, null); @@ -1281,27 +1300,27 @@ List/*!*/ decreases) { List args; r = null; // to please compiler - if (la.kind == 50) { + if (la.kind == 51) { Get(); newToken = t; TypeAndToken(out x, out ty); - if (la.kind == 51 || la.kind == 53) { - if (la.kind == 51) { + if (la.kind == 52 || la.kind == 54) { + if (la.kind == 52) { Get(); ee = new List(); Expressions(ee); - Expect(52); + Expect(53); UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true); } else { Get(); Ident(out x); - Expect(33); + Expect(34); args = new List(); if (StartOf(6)) { Expressions(args); } - Expect(34); + Expect(35); initCall = new CallStmt(x, new List(), receiverForInitCall, x.val, args); } @@ -1312,18 +1331,18 @@ List/*!*/ decreases) { r = new TypeRhs(newToken, ty, initCall); } - } else if (la.kind == 54) { + } else if (la.kind == 55) { Get(); x = t; Expression(out e); r = new ExprRhs(new UnaryExpr(x, UnaryExpr.Opcode.SetChoose, e)); - } else if (la.kind == 44) { + } else if (la.kind == 45) { Get(); r = new HavocRhs(t); } else if (StartOf(6)) { Expression(out e); r = new ExprRhs(e); - } else SynErr(120); + } else SynErr(121); } void Lhs(out Expression e) { @@ -1331,16 +1350,16 @@ List/*!*/ decreases) { if (la.kind == 1) { DottedIdentifiersAndFunction(out e); - while (la.kind == 51 || la.kind == 53) { + while (la.kind == 52 || la.kind == 54) { Suffix(ref e); } } else if (StartOf(11)) { ConstAtomExpression(out e); Suffix(ref e); - while (la.kind == 51 || la.kind == 53) { + while (la.kind == 52 || la.kind == 54) { Suffix(ref e); } - } else SynErr(121); + } else SynErr(122); } void Expressions(List/*!*/ args) { @@ -1356,15 +1375,15 @@ List/*!*/ decreases) { void Guard(out Expression e) { Expression/*!*/ ee; e = null; - Expect(33); - if (la.kind == 44) { + Expect(34); + if (la.kind == 45) { Get(); e = null; } else if (StartOf(6)) { Expression(out ee); e = ee; - } else SynErr(122); - Expect(34); + } else SynErr(123); + Expect(35); } void AlternativeBlock(out List alternatives) { @@ -1374,11 +1393,11 @@ List/*!*/ decreases) { List body; Expect(7); - while (la.kind == 57) { + while (la.kind == 58) { Get(); x = t; Expression(out e); - Expect(58); + Expect(59); body = new List(); while (StartOf(7)) { Stmt(body); @@ -1395,17 +1414,17 @@ List/*!*/ decreases) { mod = null; while (StartOf(12)) { - if (la.kind == 29 || la.kind == 60) { + if (la.kind == 30 || la.kind == 61) { isFree = false; - if (la.kind == 29) { + if (la.kind == 30) { Get(); isFree = true; } - Expect(60); + Expect(61); Expression(out e); invariants.Add(new MaybeFreeExpression(e, isFree)); Expect(17); - } else if (la.kind == 32) { + } else if (la.kind == 33) { Get(); DecreasesList(decreases, true); Expect(17); @@ -1433,10 +1452,10 @@ List/*!*/ decreases) { BoundVar/*!*/ bv; List body = new List(); - Expect(57); + Expect(58); x = t; Ident(out id); - if (la.kind == 33) { + if (la.kind == 34) { Get(); IdentTypeOptional(out bv); arguments.Add(bv); @@ -1445,9 +1464,9 @@ List/*!*/ decreases) { IdentTypeOptional(out bv); arguments.Add(bv); } - Expect(34); + Expect(35); } - Expect(58); + Expect(59); while (StartOf(7)) { Stmt(body); } @@ -1462,7 +1481,7 @@ List/*!*/ decreases) { } else if (StartOf(6)) { Expression(out e); arg = new Attributes.Argument(t, e); - } else SynErr(123); + } else SynErr(124); } void QuantifierDomain(out List bvars, out Attributes attrs, out Expression range) { @@ -1490,7 +1509,7 @@ List/*!*/ decreases) { 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); @@ -1501,7 +1520,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); @@ -1510,23 +1529,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(124); + } else SynErr(125); } void LogicalExpression(out Expression/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; RelationalExpression(out e0); if (StartOf(13)) { - 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); @@ -1537,7 +1556,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); @@ -1548,11 +1567,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(125); + } else SynErr(126); } void RelationalExpression(out Expression/*!*/ e) { @@ -1646,25 +1665,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(126); + } else SynErr(127); } void OrOp() { - if (la.kind == 72) { + if (la.kind == 73) { Get(); - } else if (la.kind == 73) { + } else if (la.kind == 74) { Get(); - } else SynErr(127); + } else SynErr(128); } 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 == 84 || la.kind == 85) { + while (la.kind == 85 || la.kind == 86) { AddOp(out x, out op); Factor(out e1); e0 = new BinaryExpr(x, op, e0, e1); @@ -1677,50 +1696,50 @@ List/*!*/ decreases) { IToken y; switch (la.kind) { - case 74: { + case 75: { Get(); x = t; op = BinaryExpr.Opcode.Eq; break; } - case 23: { + case 24: { Get(); x = t; op = BinaryExpr.Opcode.Lt; break; } - case 24: { + case 25: { Get(); 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 79: { + case 80: { Get(); x = t; op = BinaryExpr.Opcode.In; break; } - case 80: { + case 81: { Get(); x = t; y = Token.NoToken; - if (la.kind == 79) { + if (la.kind == 80) { Get(); y = t; } @@ -1735,29 +1754,29 @@ List/*!*/ decreases) { break; } - case 81: { + case 82: { Get(); x = t; op = BinaryExpr.Opcode.Neq; break; } - case 82: { + case 83: { Get(); x = t; op = BinaryExpr.Opcode.Le; break; } - case 83: { + case 84: { Get(); x = t; op = BinaryExpr.Opcode.Ge; break; } - default: SynErr(128); break; + default: SynErr(129); 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 == 44 || la.kind == 86 || la.kind == 87) { + while (la.kind == 45 || la.kind == 87 || la.kind == 88) { MulOp(out x, out op); UnaryExpression(out e1); e0 = new BinaryExpr(x, op, e0, e1); @@ -1766,82 +1785,82 @@ 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 == 84) { + if (la.kind == 85) { Get(); x = t; op = BinaryExpr.Opcode.Add; - } else if (la.kind == 85) { + } else if (la.kind == 86) { Get(); x = t; op = BinaryExpr.Opcode.Sub; - } else SynErr(129); + } else SynErr(130); } void UnaryExpression(out Expression/*!*/ e) { Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr; switch (la.kind) { - case 85: { + case 86: { Get(); x = t; UnaryExpression(out e); e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e); break; } - case 80: case 88: { + case 81: case 89: { NegOp(); x = t; UnaryExpression(out e); e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); break; } - case 18: case 38: case 55: case 61: case 62: case 63: case 98: case 99: case 100: case 101: { + case 18: case 39: case 56: case 62: case 63: case 64: case 99: case 100: case 101: case 102: { EndlessExpression(out e); break; } case 1: { DottedIdentifiersAndFunction(out e); - while (la.kind == 51 || la.kind == 53) { + while (la.kind == 52 || la.kind == 54) { Suffix(ref e); } break; } - case 7: case 51: { + case 7: case 52: { DisplayExpr(out e); break; } - case 39: { + case 40: { MultiSetExpr(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 34: case 90: case 91: case 92: case 93: case 94: case 95: case 96: { ConstAtomExpression(out e); - while (la.kind == 51 || la.kind == 53) { + while (la.kind == 52 || la.kind == 54) { Suffix(ref e); } break; } - default: SynErr(130); break; + default: SynErr(131); 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 == 44) { + if (la.kind == 45) { Get(); x = t; op = BinaryExpr.Opcode.Mul; - } else if (la.kind == 86) { + } else if (la.kind == 87) { Get(); x = t; op = BinaryExpr.Opcode.Div; - } else if (la.kind == 87) { + } else if (la.kind == 88) { Get(); x = t; op = BinaryExpr.Opcode.Mod; - } else SynErr(131); + } else SynErr(132); } void NegOp() { - if (la.kind == 80) { + if (la.kind == 81) { Get(); - } else if (la.kind == 88) { + } else if (la.kind == 89) { Get(); - } else SynErr(132); + } else SynErr(133); } void EndlessExpression(out Expression e) { @@ -1852,30 +1871,30 @@ List/*!*/ decreases) { List letVars; List letRHSs; switch (la.kind) { - case 55: { + case 56: { Get(); x = t; Expression(out e); - Expect(96); + Expect(97); Expression(out e0); - Expect(56); + Expect(57); Expression(out e1); e = new ITEExpr(x, e, e0, e1); break; } - case 61: { + case 62: { MatchExpression(out e); break; } - case 98: case 99: case 100: case 101: { + case 99: case 100: case 101: case 102: { QuantifierGuts(out e); break; } - case 38: { + case 39: { ComprehensionExpr(out e); break; } - case 62: { + case 63: { Get(); x = t; Expression(out e0); @@ -1884,7 +1903,7 @@ List/*!*/ decreases) { e = new AssertExpr(x, e0, e1); break; } - case 63: { + case 64: { Get(); x = t; Expression(out e0); @@ -1905,7 +1924,7 @@ List/*!*/ decreases) { IdentTypeOptional(out d); letVars.Add(d); } - Expect(49); + Expect(50); Expression(out e); letRHSs.Add(e); while (la.kind == 19) { @@ -1918,7 +1937,7 @@ List/*!*/ decreases) { e = new LetExpr(x, letVars, letRHSs, e); break; } - default: SynErr(133); break; + default: SynErr(134); break; } } @@ -1929,18 +1948,18 @@ List/*!*/ decreases) { Ident(out id); idents.Add(id); - while (la.kind == 53) { + while (la.kind == 54) { Get(); Ident(out id); idents.Add(id); } - if (la.kind == 33) { + if (la.kind == 34) { Get(); openParen = t; args = new List(); if (StartOf(6)) { Expressions(args); } - Expect(34); + Expect(35); } e = new IdentifierSequence(idents, openParen, args); } @@ -1951,37 +1970,37 @@ List/*!*/ decreases) { List multipleIndices = null; bool func = false; - if (la.kind == 53) { + if (la.kind == 54) { Get(); Ident(out id); - if (la.kind == 33) { + if (la.kind == 34) { Get(); args = new List(); func = true; if (StartOf(6)) { Expressions(args); } - Expect(34); + Expect(35); e = new FunctionCallExpr(id, id.val, e, args); } if (!func) { e = new FieldSelectExpr(id, e, id.val); } - } else if (la.kind == 51) { + } else if (la.kind == 52) { Get(); x = t; if (StartOf(6)) { Expression(out ee); e0 = ee; - if (la.kind == 97) { + if (la.kind == 98) { Get(); anyDots = true; if (StartOf(6)) { Expression(out ee); e1 = ee; } - } else if (la.kind == 49) { + } else if (la.kind == 50) { Get(); Expression(out ee); e1 = ee; - } else if (la.kind == 19 || la.kind == 52) { + } else if (la.kind == 19 || la.kind == 53) { while (la.kind == 19) { Get(); Expression(out ee); @@ -1992,15 +2011,15 @@ List/*!*/ decreases) { multipleIndices.Add(ee); } - } else SynErr(134); - } else if (la.kind == 97) { + } else SynErr(135); + } else if (la.kind == 98) { Get(); anyDots = true; if (StartOf(6)) { Expression(out ee); e1 = ee; } - } else SynErr(135); + } else SynErr(136); if (multipleIndices != null) { e = new MultiSelectExpr(x, e, multipleIndices); // make sure an array class with this dimensionality exists @@ -2023,8 +2042,8 @@ List/*!*/ decreases) { } } - Expect(52); - } else SynErr(136); + Expect(53); + } else SynErr(137); } void DisplayExpr(out Expression e) { @@ -2040,15 +2059,15 @@ List/*!*/ decreases) { } e = new SetDisplayExpr(x, elements); Expect(8); - } else if (la.kind == 51) { + } else if (la.kind == 52) { Get(); x = t; elements = new List(); if (StartOf(6)) { Expressions(elements); } e = new SeqDisplayExpr(x, elements); - Expect(52); - } else SynErr(137); + Expect(53); + } else SynErr(138); } void MultiSetExpr(out Expression e) { @@ -2056,7 +2075,7 @@ List/*!*/ decreases) { IToken/*!*/ x = null; List/*!*/ elements; e = dummyExpr; - Expect(39); + Expect(40); x = t; if (la.kind == 7) { Get(); @@ -2066,15 +2085,15 @@ List/*!*/ decreases) { } e = new MultiSetDisplayExpr(x, elements); Expect(8); - } else if (la.kind == 33) { + } else if (la.kind == 34) { Get(); x = t; elements = new List(); Expression(out e); e = new MultiSetFormingExpr(x, e); - Expect(34); + Expect(35); } else if (StartOf(15)) { SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses."); - } else SynErr(138); + } else SynErr(139); } void ConstAtomExpression(out Expression/*!*/ e) { @@ -2083,17 +2102,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; @@ -2103,35 +2122,35 @@ 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); - Expression(out e); Expect(34); + Expression(out e); + Expect(35); e = new FreshExpr(x, e); break; } - case 94: { + case 95: { Get(); x = t; - Expect(33); - Expression(out e); Expect(34); + Expression(out e); + Expect(35); e = new AllocatedExpr(x, e); break; } - case 95: { + case 96: { Get(); x = t; - Expect(33); - Expression(out e); Expect(34); + Expression(out e); + Expect(35); e = new OldExpr(x, e); break; } @@ -2143,15 +2162,15 @@ List/*!*/ decreases) { Expect(16); break; } - case 33: { + case 34: { Get(); x = t; Expression(out e); e = new ParensExpression(x, e); - Expect(34); + Expect(35); break; } - default: SynErr(139); break; + default: SynErr(140); break; } } @@ -2170,10 +2189,10 @@ List/*!*/ decreases) { Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; MatchCaseExpr/*!*/ c; List cases = new List(); - Expect(61); + Expect(62); x = t; Expression(out e); - while (la.kind == 57) { + while (la.kind == 58) { CaseExpression(out c); cases.Add(c); } @@ -2188,13 +2207,13 @@ List/*!*/ decreases) { Expression range; Expression/*!*/ body; - if (la.kind == 98 || la.kind == 99) { + if (la.kind == 99 || la.kind == 100) { Forall(); x = t; univ = true; - } else if (la.kind == 100 || la.kind == 101) { + } else if (la.kind == 101 || la.kind == 102) { Exists(); x = t; - } else SynErr(140); + } else SynErr(141); QuantifierDomain(out bvars, out attrs, out range); QSep(); Expression(out body); @@ -2214,7 +2233,7 @@ List/*!*/ decreases) { Expression/*!*/ range; Expression body = null; - Expect(38); + Expect(39); x = t; IdentTypeOptional(out bv); bvars.Add(bv); @@ -2225,7 +2244,7 @@ List/*!*/ decreases) { } Expect(16); Expression(out range); - if (la.kind == 102 || la.kind == 103) { + if (la.kind == 103 || la.kind == 104) { QSep(); Expression(out body); } @@ -2240,10 +2259,10 @@ List/*!*/ decreases) { BoundVar/*!*/ bv; Expression/*!*/ body; - Expect(57); + Expect(58); x = t; Ident(out id); - if (la.kind == 33) { + if (la.kind == 34) { Get(); IdentTypeOptional(out bv); arguments.Add(bv); @@ -2252,35 +2271,35 @@ List/*!*/ decreases) { IdentTypeOptional(out bv); arguments.Add(bv); } - Expect(34); + Expect(35); } - Expect(58); + Expect(59); Expression(out body); c = new MatchCaseExpr(x, id.val, arguments, body); } void Forall() { - if (la.kind == 98) { + if (la.kind == 99) { Get(); - } else if (la.kind == 99) { + } else if (la.kind == 100) { Get(); - } else SynErr(141); + } else SynErr(142); } void Exists() { - if (la.kind == 100) { + if (la.kind == 101) { Get(); - } else if (la.kind == 101) { + } else if (la.kind == 102) { Get(); - } else SynErr(142); + } else SynErr(143); } void QSep() { - if (la.kind == 102) { + if (la.kind == 103) { Get(); - } else if (la.kind == 103) { + } else if (la.kind == 104) { Get(); - } else SynErr(143); + } else SynErr(144); } void AttributeBody(ref Attributes attrs) { @@ -2288,7 +2307,7 @@ List/*!*/ decreases) { List aArgs = new List(); Attributes.Argument/*!*/ aArg; - Expect(22); + Expect(23); Expect(1); aName = t.val; if (StartOf(16)) { @@ -2307,31 +2326,31 @@ List/*!*/ decreases) { public void Parse() { la = new Token(); - la.val = ""; + la.val = ""; Get(); Dafny(); - Expect(0); + Expect(0); } - + 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,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,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,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, 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,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,T,T,x, x,x,x,T, x,x,x,x, 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,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,T,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, 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,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,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,T,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, 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,T,T,x, x,x,x,T, x,x,x,x, 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,T,T, x,x,x,x, T,x,x,x, x,x,T,T, x,x,T,T, x,x,x,x, x,T,T,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, 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,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,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,x,x, x,x,x,x, x,x,x,x, x,x,T,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,T, T,x,x,x, x,x,x,x, T,T,x,T, x,x,x,T, T,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,T,x,x, x,T,x,x, T,x,x,x, T,T,T,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, T,T,x,x, x,x,T,T, x,x}, - {x,T,T,x, T,x,x,T, x,x,x,x, 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,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,T,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, 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,T,x,x, x,T,T,T, T,T,T,x, x,x,T,x, T,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,T,T, T,T,x,x, x,x,T,x, 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,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,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,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,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,x,x,x, x,x,T,T, 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,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,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, 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,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,T, T,x,x,x, x,T,x,x, x,x,x,x, T,x,x,x, T,x,x,x, x,x,T,T, 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,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, 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,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,T, T,x,x,x, x,T,x,x, x,x,x,T, T,x,x,T, T,x,x,x, x,x,T,T, 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,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,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, 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,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, x,x,x,x, x,x,x,x, x,x,x,T, 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,T, T,x,x,x, x,x,x,x, T,T,x,T, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,T,T,x, x,x,T,x, x,T,x,x, x,T,T,T, x,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,T,T,x, x,x,x,T, T,x,x}, + {x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,x,x,x, x,x,T,T, 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,T,T,T, T,T,T,T, T,x,x,T, T,T,T,x, x,x,x} }; } // end Parser @@ -2340,18 +2359,20 @@ List/*!*/ decreases) { public class Errors { public int count = 0; // number of errors detected public System.IO.TextWriter/*!*/ errorStream = Console.Out; // error messages go to this stream - public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text - public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text - + public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text + public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text + public void SynErr(string filename, int line, int col, int n) { - SynErr(filename, line, col, GetSyntaxErrorString(n)); - } - public virtual void SynErr(string filename, int line, int col, string msg) { - Contract.Requires(msg != null); + SynErr(filename, line, col, GetSyntaxErrorString(n)); + } + + public virtual void SynErr(string filename, int line, int col, string/*!*/ msg) { + Contract.Requires(msg != null); errorStream.WriteLine(errMsgFormat, filename, line, col, msg); count++; - } - string GetSyntaxErrorString(int n) { + } + + string GetSyntaxErrorString(int n) { string s; switch (n) { case 0: s = "EOF expected"; break; @@ -2374,134 +2395,135 @@ public class Errors { case 17: s = "\";\" expected"; break; case 18: s = "\"var\" expected"; break; case 19: s = "\",\" expected"; break; - case 20: s = "\"replaces\" expected"; break; - case 21: s = "\"by\" expected"; break; - case 22: s = "\":\" expected"; break; - case 23: s = "\"<\" expected"; break; - case 24: s = "\">\" expected"; break; - case 25: s = "\"method\" expected"; break; - case 26: s = "\"constructor\" expected"; break; - case 27: s = "\"returns\" expected"; break; - case 28: s = "\"modifies\" expected"; break; - case 29: s = "\"free\" expected"; break; - case 30: s = "\"requires\" expected"; break; - case 31: s = "\"ensures\" expected"; break; - case 32: s = "\"decreases\" expected"; break; - case 33: s = "\"(\" expected"; break; - case 34: s = "\")\" expected"; break; - case 35: s = "\"bool\" expected"; break; - case 36: s = "\"nat\" expected"; break; - case 37: s = "\"int\" expected"; break; - case 38: s = "\"set\" expected"; 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 = "\"assert\" expected"; break; - case 63: s = "\"assume\" expected"; break; - case 64: s = "\"print\" expected"; break; - case 65: s = "\"parallel\" 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 = "\"!\" 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 = "\"\\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 MethodDecl"; break; - case 107: s = "invalid TypeAndToken"; break; - case 108: s = "invalid MethodSpec"; break; + case 20: s = "\"type\" expected"; break; + case 21: s = "\"replaces\" expected"; break; + case 22: s = "\"by\" expected"; break; + case 23: s = "\":\" expected"; break; + case 24: s = "\"<\" expected"; break; + case 25: s = "\">\" expected"; break; + case 26: s = "\"method\" expected"; break; + case 27: s = "\"constructor\" expected"; break; + case 28: s = "\"returns\" expected"; break; + case 29: s = "\"modifies\" expected"; break; + case 30: s = "\"free\" expected"; break; + case 31: s = "\"requires\" expected"; break; + case 32: s = "\"ensures\" expected"; break; + case 33: s = "\"decreases\" expected"; break; + case 34: s = "\"(\" expected"; break; + case 35: s = "\")\" expected"; break; + case 36: s = "\"bool\" expected"; break; + case 37: s = "\"nat\" expected"; break; + case 38: s = "\"int\" expected"; break; + case 39: s = "\"set\" expected"; break; + case 40: s = "\"multiset\" expected"; break; + case 41: s = "\"seq\" expected"; break; + case 42: s = "\"object\" expected"; break; + case 43: s = "\"function\" expected"; break; + case 44: s = "\"reads\" expected"; break; + case 45: s = "\"*\" expected"; break; + case 46: s = "\"`\" expected"; break; + case 47: s = "\"label\" expected"; break; + case 48: s = "\"break\" expected"; break; + case 49: s = "\"return\" expected"; break; + case 50: s = "\":=\" expected"; break; + case 51: s = "\"new\" expected"; break; + case 52: s = "\"[\" expected"; break; + case 53: s = "\"]\" expected"; break; + case 54: s = "\".\" expected"; break; + case 55: s = "\"choose\" expected"; break; + case 56: s = "\"if\" expected"; break; + case 57: s = "\"else\" expected"; break; + case 58: s = "\"case\" expected"; break; + case 59: s = "\"=>\" expected"; break; + case 60: s = "\"while\" expected"; break; + case 61: s = "\"invariant\" expected"; break; + case 62: s = "\"match\" expected"; break; + case 63: s = "\"assert\" expected"; break; + case 64: s = "\"assume\" expected"; break; + case 65: s = "\"print\" expected"; break; + case 66: s = "\"parallel\" 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 = "\"!\" expected"; break; + case 82: s = "\"\\u2260\" expected"; break; + case 83: s = "\"\\u2264\" expected"; break; + case 84: s = "\"\\u2265\" 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 = "\"then\" expected"; break; + case 98: s = "\"..\" expected"; break; + case 99: s = "\"forall\" expected"; break; + case 100: s = "\"\\u2200\" expected"; break; + case 101: s = "\"exists\" expected"; break; + case 102: s = "\"\\u2203\" expected"; break; + case 103: s = "\"::\" expected"; break; + case 104: s = "\"\\u2022\" expected"; break; + case 105: s = "??? expected"; break; + case 106: s = "invalid ClassMemberDecl"; break; + case 107: s = "invalid MethodDecl"; break; + case 108: s = "invalid TypeAndToken"; break; case 109: s = "invalid MethodSpec"; break; - case 110: s = "invalid ReferenceType"; break; - case 111: s = "invalid FunctionSpec"; break; - case 112: s = "invalid PossiblyWildFrameExpression"; break; - case 113: s = "invalid PossiblyWildExpression"; break; - case 114: s = "invalid OneStmt"; break; + case 110: s = "invalid MethodSpec"; break; + case 111: s = "invalid ReferenceType"; break; + case 112: s = "invalid FunctionSpec"; break; + case 113: s = "invalid PossiblyWildFrameExpression"; break; + case 114: s = "invalid PossiblyWildExpression"; break; case 115: s = "invalid OneStmt"; break; - case 116: s = "invalid UpdateStmt"; break; - case 117: s = "invalid IfStmt"; break; + case 116: s = "invalid OneStmt"; break; + case 117: s = "invalid UpdateStmt"; break; case 118: s = "invalid IfStmt"; break; - case 119: s = "invalid WhileStmt"; break; - case 120: s = "invalid Rhs"; break; - case 121: s = "invalid Lhs"; break; - case 122: s = "invalid Guard"; break; - case 123: s = "invalid AttributeArg"; break; - case 124: s = "invalid EquivOp"; break; - case 125: s = "invalid ImpliesOp"; break; - case 126: s = "invalid AndOp"; break; - case 127: s = "invalid OrOp"; break; - case 128: s = "invalid RelOp"; break; - case 129: s = "invalid AddOp"; break; - case 130: s = "invalid UnaryExpression"; break; - case 131: s = "invalid MulOp"; break; - case 132: s = "invalid NegOp"; break; - case 133: s = "invalid EndlessExpression"; break; - case 134: s = "invalid Suffix"; break; + case 119: s = "invalid IfStmt"; break; + case 120: s = "invalid WhileStmt"; break; + case 121: s = "invalid Rhs"; break; + case 122: s = "invalid Lhs"; break; + case 123: s = "invalid Guard"; break; + case 124: s = "invalid AttributeArg"; break; + case 125: s = "invalid EquivOp"; break; + case 126: s = "invalid ImpliesOp"; break; + case 127: s = "invalid AndOp"; break; + case 128: s = "invalid OrOp"; break; + case 129: s = "invalid RelOp"; break; + case 130: s = "invalid AddOp"; break; + case 131: s = "invalid UnaryExpression"; break; + case 132: s = "invalid MulOp"; break; + case 133: s = "invalid NegOp"; break; + case 134: s = "invalid EndlessExpression"; break; case 135: s = "invalid Suffix"; break; case 136: s = "invalid Suffix"; break; - case 137: s = "invalid DisplayExpr"; break; - case 138: s = "invalid MultiSetExpr"; break; - case 139: s = "invalid ConstAtomExpression"; break; - case 140: s = "invalid QuantifierGuts"; break; - case 141: s = "invalid Forall"; break; - case 142: s = "invalid Exists"; break; - case 143: s = "invalid QSep"; break; + case 137: s = "invalid Suffix"; break; + case 138: s = "invalid DisplayExpr"; break; + case 139: s = "invalid MultiSetExpr"; 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 QSep"; break; default: s = "error " + n; break; } - return s; + return s; } public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { // semantic errors @@ -2509,8 +2531,9 @@ public class Errors { Contract.Requires(msg != null); SemErr(tok.filename, tok.line, tok.col, msg); } + public virtual void SemErr(string filename, int line, int col, string/*!*/ msg) { - Contract.Requires(msg != null); + Contract.Requires(msg != null); errorStream.WriteLine(errMsgFormat, filename, line, col, msg); count++; } diff --git a/Dafny/Printer.cs b/Dafny/Printer.cs index 5b9ba1d6..9f012509 100644 --- a/Dafny/Printer.cs +++ b/Dafny/Printer.cs @@ -62,7 +62,13 @@ namespace Microsoft.Dafny { int i = 0; foreach (TopLevelDecl d in classes) { Contract.Assert(d != null); - if (d is DatatypeDecl) { + if (d is ArbitraryTypeDecl) { + var at = (ArbitraryTypeDecl)d; + if (i++ != 0) { wr.WriteLine(); } + Indent(indent); + PrintClassMethodHelper("type", at.Attributes, at.Name, new List()); + wr.WriteLine(";"); + } else if (d is DatatypeDecl) { if (i++ != 0) { wr.WriteLine(); } PrintDatatype((DatatypeDecl)d, indent); } else { diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs index 55c2f48b..f54c633b 100644 --- a/Dafny/Resolver.cs +++ b/Dafny/Resolver.cs @@ -195,7 +195,10 @@ namespace Microsoft.Dafny { classes.Add(d.Name, d); } - if (d is ClassDecl) { + if (d is ArbitraryTypeDecl) { + // nothing more to register + + } else if (d is ClassDecl) { ClassDecl cl = (ClassDecl)d; // register the names of the class members @@ -293,7 +296,9 @@ namespace Microsoft.Dafny { Contract.Assert(d != null); allTypeParameters.PushMarker(); ResolveTypeParameters(d.TypeArgs, true, d); - if (d is ClassDecl) { + if (d is ArbitraryTypeDecl) { + // nothing to do + } else if (d is ClassDecl) { ResolveClassMemberTypes((ClassDecl)d); } else { ResolveCtorTypes((DatatypeDecl)d, datatypeDependencies); @@ -309,7 +314,9 @@ namespace Microsoft.Dafny { Contract.Assert(d != null); allTypeParameters.PushMarker(); ResolveTypeParameters(d.TypeArgs, false, d); - if (d is ClassDecl) { + if (d is ArbitraryTypeDecl) { + // nothing to do + } else if (d is ClassDecl) { ResolveClassMemberBodies((ClassDecl)d); } else { DatatypeDecl dtd = (DatatypeDecl)d; @@ -872,10 +879,12 @@ namespace Microsoft.Dafny { TopLevelDecl d; if (!classes.TryGetValue(t.Name, out d)) { Error(t.tok, "Undeclared top-level type or type parameter: {0}", t.Name); - } else if (cce.NonNull(d).TypeArgs.Count == t.TypeArgs.Count) { - t.ResolvedClass = d; - } else { + } else if (d.TypeArgs.Count != t.TypeArgs.Count) { Error(t.tok, "Wrong number of type arguments ({0} instead of {1}) passed to class/datatype: {2}", t.TypeArgs.Count, d.TypeArgs.Count, t.Name); + } else if (d is ArbitraryTypeDecl) { + t.ResolvedParam = ((ArbitraryTypeDecl)d).TheType; // resolve as type parameter + } else { + t.ResolvedClass = d; } } diff --git a/Dafny/Scanner.cs b/Dafny/Scanner.cs index 1ab06974..0d1749d8 100644 --- a/Dafny/Scanner.cs +++ b/Dafny/Scanner.cs @@ -19,7 +19,7 @@ public class Buffer { // a) whole stream in buffer // b) part of stream in buffer // 2) non seekable stream (network, console) - + public const int EOF = 65535 + 1; // char.MaxValue + 1; const int MIN_BUFFER_LENGTH = 1024; // 1KB const int MAX_BUFFER_LENGTH = MIN_BUFFER_LENGTH * 64; // 64KB @@ -31,15 +31,17 @@ public class Buffer { Stream/*!*/ stream; // input stream (seekable) bool isUserStream; // was the stream opened by the user? -[ContractInvariantMethod] -void ObjectInvariant(){ - Contract.Invariant(buf != null); - Contract.Invariant(stream != null);} - [NotDelayed] - public Buffer (Stream/*!*/ s, bool isUserStream) :base() { + [ContractInvariantMethod] + void ObjectInvariant(){ + Contract.Invariant(buf != null); + Contract.Invariant(stream != null); + } + +// [NotDelayed] + public Buffer (Stream/*!*/ s, bool isUserStream) : base() { Contract.Requires(s != null); stream = s; this.isUserStream = isUserStream; - + int fl, bl; if (s.CanSeek) { fl = (int) s.Length; @@ -51,12 +53,12 @@ void ObjectInvariant(){ buf = new byte[(bl>0) ? bl : MIN_BUFFER_LENGTH]; fileLen = fl; bufLen = bl; - + if (fileLen > 0) Pos = 0; // setup buffer to position 0 (start) else bufPos = 0; // index 0 is already after the file, thus Pos = 0 is invalid if (bufLen == fileLen && s.CanSeek) Close(); } - + protected Buffer(Buffer/*!*/ b) { // called in UTF8Buffer constructor Contract.Requires(b != null); buf = b.buf; @@ -73,14 +75,14 @@ void ObjectInvariant(){ } ~Buffer() { Close(); } - + protected void Close() { if (!isUserStream && stream != null) { stream.Close(); //stream = null; } } - + public virtual int Read () { if (bufPos < bufLen) { return buf[bufPos++]; @@ -100,7 +102,7 @@ void ObjectInvariant(){ Pos = curPos; return ch; } - + public string/*!*/ GetString (int beg, int end) { Contract.Ensures(Contract.Result() != null); int len = 0; @@ -139,7 +141,7 @@ void ObjectInvariant(){ } } } - + // Read the next chunk of bytes from the stream, increases the buffer // if needed and updates the fields fileLen and bufLen. // Returns the number of bytes read. @@ -209,23 +211,24 @@ public class UTF8Buffer: Buffer { public class Scanner { const char EOL = '\n'; const int eofSym = 0; /* pdt */ - const int maxT = 104; - const int noSym = 104; - - -[ContractInvariantMethod] -void objectInvariant(){ - Contract.Invariant(buffer!=null); - Contract.Invariant(t != null); - Contract.Invariant(start != null); - Contract.Invariant(tokens != null); - Contract.Invariant(pt != null); - Contract.Invariant(tval != null); - Contract.Invariant(Filename != null); - Contract.Invariant(errorHandler != null); -} + const int maxT = 105; + const int noSym = 105; + + + [ContractInvariantMethod] + void objectInvariant(){ + Contract.Invariant(buffer!=null); + Contract.Invariant(t != null); + Contract.Invariant(start != null); + Contract.Invariant(tokens != null); + Contract.Invariant(pt != null); + Contract.Invariant(tval != null); + Contract.Invariant(Filename != null); + Contract.Invariant(errorHandler != null); + } + public Buffer/*!*/ buffer; // scanner buffer - + Token/*!*/ t; // current token int ch; // current input character int pos; // byte position of current character @@ -236,13 +239,13 @@ void objectInvariant(){ Token/*!*/ tokens; // list of tokens already peeked (first token is a dummy) Token/*!*/ pt; // current peek token - + char[]/*!*/ tval = new char[128]; // text of current token int tlen; // length of current token - + private string/*!*/ Filename; private Errors/*!*/ errorHandler; - + static Scanner() { start = new Hashtable(128); for (int i = 39; i <= 39; ++i) start[i] = 1; @@ -290,9 +293,9 @@ void objectInvariant(){ start[Buffer.EOF] = -1; } - - [NotDelayed] - public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) :base(){ + +// [NotDelayed] + public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) : base() { Contract.Requires(fileName != null); Contract.Requires(errorHandler != null); this.errorHandler = errorHandler; @@ -302,15 +305,14 @@ void objectInvariant(){ Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read); buffer = new Buffer(stream, false); Filename = fileName; - Init(); } catch (IOException) { throw new FatalError("Cannot open file " + fileName); } } - - [NotDelayed] - public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) :base(){ + +// [NotDelayed] + public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) : base() { Contract.Requires(s != null); Contract.Requires(errorHandler != null); Contract.Requires(fileName != null); @@ -319,10 +321,9 @@ void objectInvariant(){ buffer = new Buffer(s, true); this.errorHandler = errorHandler; this.Filename = fileName; - Init(); } - + void Init() { pos = -1; line = 1; col = 0; oldEols = 0; @@ -343,11 +344,11 @@ void objectInvariant(){ Contract.Ensures(Contract.Result() != null); int p = buffer.Pos; int ch = buffer.Read(); - // replace isolated '\r' by '\n' in order to make + // replace isolated '\r' by '\n' in order to make // eol handling uniform across Windows, Unix and Mac if (ch == '\r' && buffer.Peek() != '\n') ch = EOL; while (ch != EOL && ch != Buffer.EOF){ - ch = buffer.Read(); + ch = buffer.Read(); // replace isolated '\r' by '\n' in order to make // eol handling uniform across Windows, Unix and Mac if (ch == '\r' && buffer.Peek() != '\n') ch = EOL; @@ -358,7 +359,7 @@ void objectInvariant(){ } void NextCh() { - if (oldEols > 0) { ch = EOL; oldEols--; } + if (oldEols > 0) { ch = EOL; oldEols--; } else { // pos = buffer.Pos; // ch = buffer.Read(); col++; @@ -366,9 +367,9 @@ void objectInvariant(){ // // eol handling uniform across Windows, Unix and Mac // if (ch == '\r' && buffer.Peek() != '\n') ch = EOL; // if (ch == EOL) { line++; col = 0; } - + while (true) { - pos = buffer.Pos; + pos = buffer.Pos; ch = buffer.Read(); col++; // replace isolated '\r' by '\n' in order to make // eol handling uniform across Windows, Unix and Mac @@ -418,7 +419,7 @@ void objectInvariant(){ return; } - + } } @@ -495,51 +496,52 @@ void objectInvariant(){ case "unlimited": t.kind = 13; break; case "datatype": t.kind = 14; break; case "var": t.kind = 18; break; - case "replaces": t.kind = 20; break; - case "by": t.kind = 21; break; - case "method": t.kind = 25; break; - case "constructor": t.kind = 26; break; - case "returns": t.kind = 27; break; - case "modifies": t.kind = 28; break; - case "free": t.kind = 29; break; - case "requires": t.kind = 30; break; - case "ensures": t.kind = 31; break; - case "decreases": t.kind = 32; break; - case "bool": t.kind = 35; break; - case "nat": t.kind = 36; break; - case "int": t.kind = 37; break; - case "set": t.kind = 38; 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 "assert": t.kind = 62; break; - case "assume": t.kind = 63; break; - case "print": t.kind = 64; break; - case "parallel": t.kind = 65; break; - case "in": t.kind = 79; 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 "type": t.kind = 20; break; + case "replaces": t.kind = 21; break; + case "by": t.kind = 22; break; + case "method": t.kind = 26; break; + case "constructor": t.kind = 27; break; + case "returns": t.kind = 28; break; + case "modifies": t.kind = 29; break; + case "free": t.kind = 30; break; + case "requires": t.kind = 31; break; + case "ensures": t.kind = 32; break; + case "decreases": t.kind = 33; break; + case "bool": t.kind = 36; break; + case "nat": t.kind = 37; break; + case "int": t.kind = 38; break; + case "set": t.kind = 39; break; + case "multiset": t.kind = 40; break; + case "seq": t.kind = 41; break; + case "object": t.kind = 42; break; + case "function": t.kind = 43; break; + case "reads": t.kind = 44; break; + case "label": t.kind = 47; break; + case "break": t.kind = 48; break; + case "return": t.kind = 49; break; + case "new": t.kind = 51; break; + case "choose": t.kind = 55; break; + case "if": t.kind = 56; break; + case "else": t.kind = 57; break; + case "case": t.kind = 58; break; + case "while": t.kind = 60; break; + case "invariant": t.kind = 61; break; + case "match": t.kind = 62; break; + case "assert": t.kind = 63; break; + case "assume": t.kind = 64; break; + case "print": t.kind = 65; break; + case "parallel": t.kind = 66; break; + case "in": t.kind = 80; 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 "then": t.kind = 97; break; + case "forall": t.kind = 99; break; + case "exists": t.kind = 101; break; default: break; } } @@ -556,10 +558,13 @@ void objectInvariant(){ t.pos = pos; t.col = col; t.line = line; t.filename = this.Filename; int state; - if (start.ContainsKey(ch)) { state = (int) cce.NonNull( start[ch]); } + if (start.ContainsKey(ch)) { + Contract.Assert(start[ch] != null); + state = (int) start[ch]; + } else { state = 0; } tlen = 0; AddCh(); - + switch (state) { case -1: { t.kind = eofSym; break; } // NextCh already done case 0: { @@ -646,75 +651,75 @@ void objectInvariant(){ case 20: {t.kind = 19; break;} case 21: - {t.kind = 33; break;} - case 22: {t.kind = 34; break;} + case 22: + {t.kind = 35; break;} case 23: - {t.kind = 44; break;} - case 24: {t.kind = 45; break;} + case 24: + {t.kind = 46; break;} case 25: - {t.kind = 49; break;} + {t.kind = 50; break;} case 26: - {t.kind = 51; break;} - case 27: {t.kind = 52; break;} + case 27: + {t.kind = 53; break;} case 28: - {t.kind = 58; break;} + {t.kind = 59; 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: - {t.kind = 81; break;} - case 43: {t.kind = 82; break;} - case 44: + case 43: {t.kind = 83; break;} - case 45: + case 44: {t.kind = 84; break;} - case 46: + case 45: {t.kind = 85; break;} - case 47: + case 46: {t.kind = 86; break;} - case 48: + case 47: {t.kind = 87; break;} - case 49: + case 48: {t.kind = 88; break;} + case 49: + {t.kind = 89; break;} case 50: - {t.kind = 97; break;} + {t.kind = 98; break;} case 51: - {t.kind = 99; break;} + {t.kind = 100; break;} case 52: - {t.kind = 101; break;} - case 53: {t.kind = 102; break;} - case 54: + case 53: {t.kind = 103; break;} + case 54: + {t.kind = 104; break;} case 55: recEnd = pos; recKind = 15; if (ch == '>') {AddCh(); goto case 28;} @@ -725,48 +730,48 @@ void objectInvariant(){ if (ch == '|') {AddCh(); goto case 37;} else {t.kind = 16; break;} case 57: - recEnd = pos; recKind = 22; + recEnd = pos; recKind = 23; if (ch == '=') {AddCh(); goto case 25;} else if (ch == ':') {AddCh(); goto case 53;} - else {t.kind = 22; break;} + else {t.kind = 23; break;} case 58: - recEnd = pos; recKind = 23; + recEnd = pos; recKind = 24; if (ch == '=') {AddCh(); goto case 63;} - else {t.kind = 23; break;} + else {t.kind = 24; break;} case 59: - recEnd = pos; recKind = 24; + recEnd = pos; recKind = 25; if (ch == '=') {AddCh(); goto case 39;} - else {t.kind = 24; break;} + else {t.kind = 25; break;} case 60: - recEnd = pos; recKind = 53; + recEnd = pos; recKind = 54; if (ch == '.') {AddCh(); goto case 50;} - else {t.kind = 53; break;} + else {t.kind = 54; break;} case 61: - recEnd = pos; recKind = 80; + recEnd = pos; recKind = 81; if (ch == '=') {AddCh(); goto case 40;} else if (ch == '!') {AddCh(); goto case 41;} - else {t.kind = 80; break;} + else {t.kind = 81; break;} case 62: - 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 63: - 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); return t; } - + private void SetScannerBehindT() { buffer.Pos = t.pos; NextCh(); line = t.line; col = t.col; for (int i = 0; i < tlen; i++) NextCh(); } - + // get the next token (possibly a token already seen during peeking) public Token/*!*/ Scan () { Contract.Ensures(Contract.Result() != null); @@ -787,7 +792,7 @@ void objectInvariant(){ } pt = pt.next; } while (pt.kind > maxT); // skip pragmas - + return pt; } diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs index d1e41663..e0adcba3 100644 --- a/Dafny/Translator.cs +++ b/Dafny/Translator.cs @@ -302,7 +302,9 @@ namespace Microsoft.Dafny { } foreach (TopLevelDecl d in program.BuiltIns.SystemModule.TopLevelDecls) { - if (d is DatatypeDecl) { + if (d is ArbitraryTypeDecl) { + // nothing to do--this is treated just like a type parameter + } else if (d is DatatypeDecl) { AddDatatype((DatatypeDecl)d); } else { AddClassMembers((ClassDecl)d); @@ -310,7 +312,9 @@ namespace Microsoft.Dafny { } foreach (ModuleDecl m in program.Modules) { foreach (TopLevelDecl d in m.TopLevelDecls) { - if (d is DatatypeDecl) { + if (d is ArbitraryTypeDecl) { + // nothing to do--this is treated just like a type parameter + } else if (d is DatatypeDecl) { AddDatatype((DatatypeDecl)d); } else { AddClassMembers((ClassDecl)d); -- cgit v1.2.3