From 1ef4a8b7e58c8de43dee6a10249a585eed1929f6 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 8 Sep 2011 09:10:30 -0700 Subject: Dafny: fixed parsing bug with "!in" Dafny: fixed translation bug with missing match cases (where the constructor has some parameters) Dafny: fixed translation bug where the program had forward references to members of a datatype --- Dafny/Dafny.atg | 20 ++- Dafny/Parser.cs | 344 +++++++++++++++++++++++++++------------------------- Dafny/Scanner.cs | 226 +++++++++++++++++----------------- Dafny/Translator.cs | 42 ++++--- 4 files changed, 334 insertions(+), 298 deletions(-) (limited to 'Dafny') diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg index 028d6826..77eb3dbf 100644 --- a/Dafny/Dafny.atg +++ b/Dafny/Dafny.atg @@ -1059,7 +1059,10 @@ RelationalExpression .) . RelOp -= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/; .) += (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); + x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/; + IToken y; + .) ( "==" (. x = t; op = BinaryExpr.Opcode.Eq; .) | "<" (. x = t; op = BinaryExpr.Opcode.Lt; .) | ">" (. x = t; op = BinaryExpr.Opcode.Gt; .) @@ -1068,7 +1071,20 @@ RelOp | "!=" (. x = t; op = BinaryExpr.Opcode.Neq; .) | "!!" (. x = t; op = BinaryExpr.Opcode.Disjoint; .) | "in" (. x = t; op = BinaryExpr.Opcode.In; .) - | "!in" (. x = t; op = BinaryExpr.Opcode.NotIn; .) + | /* The next operator is "!in", but Coco evidently parses "!in" even when it is a prefix of, say, "!initialized". + * The reason for this seems to be that the first character of "!in" is not a letter. So, here is the workaround: + */ + "!" (. x = t; y = Token.NoToken; .) + [ "in" (. y = t; .) + ] (. if (y == Token.NoToken) { + SemErr(x, "invalid RelOp"); + } else if (y.pos != x.pos + 1) { + SemErr(x, "invalid RelOp (perhaps you intended \"!in\" with no intervening whitespace?)"); + } else { + x.val = "!in"; + op = BinaryExpr.Opcode.NotIn; + } + .) | '\u2260' (. x = t; op = BinaryExpr.Opcode.Neq; .) | '\u2264' (. x = t; op = BinaryExpr.Opcode.Le; .) | '\u2265' (. x = t; op = BinaryExpr.Opcode.Ge; .) diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs index 109422ad..ed0e285b 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 = 105; + public const int maxT = 104; 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; @@ -375,7 +375,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List/*!*/ typeArgs) { @@ -490,7 +490,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List/*!*/ decreases) { Expression(out e); Expect(17); ens.Add(new MaybeFreeExpression(e, isFree)); - } else SynErr(109); + } else SynErr(108); } else if (la.kind == 32) { Get(); DecreasesList(decreases, false); Expect(17); - } else SynErr(110); + } else SynErr(109); } void BlockStmt(out Statement/*!*/ block, out IToken bodyStart, out IToken bodyEnd) { @@ -874,7 +874,7 @@ List/*!*/ decreases) { GenericInstantiation(gt); } ty = new UserDefinedType(tok, tok.val, gt); - } else SynErr(111); + } else SynErr(110); } void FunctionSpec(List/*!*/ reqs, List/*!*/ reads, List/*!*/ ens, List/*!*/ decreases) { @@ -906,7 +906,7 @@ List/*!*/ decreases) { Get(); DecreasesList(decreases, false); Expect(17); - } else SynErr(112); + } else SynErr(111); } void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) { @@ -925,7 +925,7 @@ List/*!*/ decreases) { fe = new FrameExpression(new WildcardExpr(t), null); } else if (StartOf(6)) { FrameExpression(out fe); - } else SynErr(113); + } else SynErr(112); } void PossiblyWildExpression(out Expression/*!*/ e) { @@ -936,7 +936,7 @@ List/*!*/ decreases) { e = new WildcardExpr(t); } else if (StartOf(6)) { Expression(out e); - } else SynErr(114); + } else SynErr(113); } void Stmt(List/*!*/ ss) { @@ -969,7 +969,7 @@ List/*!*/ decreases) { PrintStmt(out s); break; } - case 1: case 2: case 16: case 33: case 90: case 91: case 92: case 93: case 94: case 95: case 96: { + case 1: case 2: case 16: case 33: case 89: case 90: case 91: case 92: case 93: case 94: case 95: { UpdateStmt(out s); break; } @@ -1013,7 +1013,7 @@ List/*!*/ decreases) { Get(); breakCount++; } - } else SynErr(115); + } else SynErr(114); Expect(17); s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); break; @@ -1022,7 +1022,7 @@ List/*!*/ decreases) { ReturnStmt(out s); break; } - default: SynErr(116); break; + default: SynErr(115); break; } } @@ -1093,7 +1093,7 @@ List/*!*/ decreases) { } else if (la.kind == 22) { Get(); SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); - } else SynErr(117); + } else SynErr(116); s = new UpdateStmt(x, lhss, rhss); } @@ -1166,13 +1166,13 @@ List/*!*/ decreases) { } else if (la.kind == 7) { BlockStmt(out s, out bodyStart, out bodyEnd); els = s; - } else SynErr(118); + } else SynErr(117); } ifStmt = new IfStmt(x, guard, thn, els); } else if (la.kind == 7) { AlternativeBlock(out alternatives); ifStmt = new AlternativeStmt(x, alternatives); - } else SynErr(119); + } else SynErr(118); } void WhileStmt(out Statement/*!*/ stmt) { @@ -1198,7 +1198,7 @@ List/*!*/ decreases) { LoopSpec(out invariants, out decreases, out mod); AlternativeBlock(out alternatives); stmt = new AlternativeLoopStmt(x, invariants, decreases, mod, alternatives); - } else SynErr(120); + } else SynErr(119); } void MatchStmt(out Statement/*!*/ s) { @@ -1335,7 +1335,7 @@ List/*!*/ decreases) { } else if (StartOf(6)) { Expression(out e); r = new ExprRhs(e); - } else SynErr(121); + } else SynErr(120); } void Lhs(out Expression e) { @@ -1352,7 +1352,7 @@ List/*!*/ decreases) { while (la.kind == 51 || la.kind == 53) { Suffix(ref e); } - } else SynErr(122); + } else SynErr(121); } void Expressions(List/*!*/ args) { @@ -1375,7 +1375,7 @@ List/*!*/ decreases) { } else if (StartOf(6)) { Expression(out ee); e = ee; - } else SynErr(123); + } else SynErr(122); Expect(34); } @@ -1473,7 +1473,7 @@ List/*!*/ decreases) { } else if (StartOf(6)) { Expression(out e); arg = new Attributes.Argument(e); - } else SynErr(124); + } else SynErr(123); } void EquivExpression(out Expression/*!*/ e0) { @@ -1503,7 +1503,7 @@ List/*!*/ decreases) { Get(); } else if (la.kind == 68) { Get(); - } else SynErr(125); + } else SynErr(124); } void LogicalExpression(out Expression/*!*/ e0) { @@ -1541,7 +1541,7 @@ List/*!*/ decreases) { Get(); } else if (la.kind == 70) { Get(); - } else SynErr(126); + } else SynErr(125); } void RelationalExpression(out Expression/*!*/ e) { @@ -1639,7 +1639,7 @@ List/*!*/ decreases) { Get(); } else if (la.kind == 72) { Get(); - } else SynErr(127); + } else SynErr(126); } void OrOp() { @@ -1647,7 +1647,7 @@ List/*!*/ decreases) { Get(); } else if (la.kind == 74) { Get(); - } else SynErr(128); + } else SynErr(127); } void Term(out Expression/*!*/ e0) { @@ -1661,7 +1661,10 @@ List/*!*/ decreases) { } void RelOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) { - Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/; + Contract.Ensures(Contract.ValueAtReturn(out x) != null); + x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/; + IToken y; + switch (la.kind) { case 75: { Get(); @@ -1705,7 +1708,20 @@ List/*!*/ decreases) { } case 80: { Get(); - x = t; op = BinaryExpr.Opcode.NotIn; + x = t; y = Token.NoToken; + if (la.kind == 63) { + Get(); + y = t; + } + if (y == Token.NoToken) { + SemErr(x, "invalid RelOp"); + } else if (y.pos != x.pos + 1) { + SemErr(x, "invalid RelOp (perhaps you intended \"!in\" with no intervening whitespace?)"); + } else { + x.val = "!in"; + op = BinaryExpr.Opcode.NotIn; + } + break; } case 81: { @@ -1723,7 +1739,7 @@ List/*!*/ decreases) { x = t; op = BinaryExpr.Opcode.Ge; break; } - default: SynErr(129); break; + default: SynErr(128); break; } } @@ -1745,7 +1761,7 @@ List/*!*/ decreases) { } else if (la.kind == 85) { Get(); x = t; op = BinaryExpr.Opcode.Sub; - } else SynErr(130); + } else SynErr(129); } void UnaryExpression(out Expression/*!*/ e) { @@ -1758,14 +1774,14 @@ List/*!*/ decreases) { e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e); break; } - case 88: case 89: { + case 80: case 88: { NegOp(); x = t; UnaryExpression(out e); e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); break; } - case 38: case 55: case 61: case 99: case 100: case 101: case 102: { + case 38: case 55: case 61: case 98: case 99: case 100: case 101: { EndlessExpression(out e); break; } @@ -1784,14 +1800,14 @@ List/*!*/ decreases) { MultiSetExpr(out e); break; } - case 2: case 16: case 33: case 90: case 91: case 92: case 93: case 94: case 95: case 96: { + case 2: case 16: case 33: case 89: case 90: case 91: case 92: case 93: case 94: case 95: { ConstAtomExpression(out e); while (la.kind == 51 || la.kind == 53) { Suffix(ref e); } break; } - default: SynErr(131); break; + default: SynErr(130); break; } } @@ -1806,15 +1822,15 @@ List/*!*/ decreases) { } else if (la.kind == 87) { Get(); x = t; op = BinaryExpr.Opcode.Mod; - } else SynErr(132); + } else SynErr(131); } void NegOp() { - if (la.kind == 88) { + if (la.kind == 80) { Get(); - } else if (la.kind == 89) { + } else if (la.kind == 88) { Get(); - } else SynErr(133); + } else SynErr(132); } void EndlessExpression(out Expression e) { @@ -1826,7 +1842,7 @@ List/*!*/ decreases) { Get(); x = t; Expression(out e); - Expect(97); + Expect(96); Expression(out e0); Expect(56); Expression(out e1); @@ -1837,7 +1853,7 @@ List/*!*/ decreases) { QuantifierGuts(out e); } else if (la.kind == 38) { ComprehensionExpr(out e); - } else SynErr(134); + } else SynErr(133); } void DottedIdentifiersAndFunction(out Expression e) { @@ -1888,7 +1904,7 @@ List/*!*/ decreases) { if (StartOf(6)) { Expression(out ee); e0 = ee; - if (la.kind == 98) { + if (la.kind == 97) { Get(); anyDots = true; if (StartOf(6)) { @@ -1910,15 +1926,15 @@ List/*!*/ decreases) { multipleIndices.Add(ee); } - } else SynErr(135); - } else if (la.kind == 98) { + } else SynErr(134); + } else if (la.kind == 97) { Get(); anyDots = true; if (StartOf(6)) { Expression(out ee); e1 = ee; } - } else SynErr(136); + } else SynErr(135); if (multipleIndices != null) { e = new MultiSelectExpr(x, e, multipleIndices); // make sure an array class with this dimensionality exists @@ -1942,7 +1958,7 @@ List/*!*/ decreases) { } Expect(52); - } else SynErr(137); + } else SynErr(136); } void DisplayExpr(out Expression e) { @@ -1966,7 +1982,7 @@ List/*!*/ decreases) { } e = new SeqDisplayExpr(x, elements); Expect(52); - } else SynErr(138); + } else SynErr(137); } void MultiSetExpr(out Expression e) { @@ -1992,7 +2008,7 @@ List/*!*/ decreases) { Expect(34); } else if (StartOf(16)) { SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses."); - } else SynErr(139); + } else SynErr(138); } void ConstAtomExpression(out Expression/*!*/ e) { @@ -2001,17 +2017,17 @@ List/*!*/ decreases) { e = dummyExpr; switch (la.kind) { - case 90: { + case 89: { Get(); e = new LiteralExpr(t, false); break; } - case 91: { + case 90: { Get(); e = new LiteralExpr(t, true); break; } - case 92: { + case 91: { Get(); e = new LiteralExpr(t); break; @@ -2021,12 +2037,12 @@ List/*!*/ decreases) { e = new LiteralExpr(t, n); break; } - case 93: { + case 92: { Get(); e = new ThisExpr(t); break; } - case 94: { + case 93: { Get(); x = t; Expect(33); @@ -2035,7 +2051,7 @@ List/*!*/ decreases) { e = new FreshExpr(x, e); break; } - case 95: { + case 94: { Get(); x = t; Expect(33); @@ -2044,7 +2060,7 @@ List/*!*/ decreases) { e = new AllocatedExpr(x, e); break; } - case 96: { + case 95: { Get(); x = t; Expect(33); @@ -2069,7 +2085,7 @@ List/*!*/ decreases) { Expect(34); break; } - default: SynErr(140); break; + default: SynErr(139); break; } } @@ -2108,13 +2124,13 @@ List/*!*/ decreases) { Expression range = null; Expression/*!*/ body; - if (la.kind == 99 || la.kind == 100) { + if (la.kind == 98 || la.kind == 99) { Forall(); x = t; univ = true; - } else if (la.kind == 101 || la.kind == 102) { + } else if (la.kind == 100 || la.kind == 101) { Exists(); x = t; - } else SynErr(141); + } else SynErr(140); IdentTypeOptional(out bv); bvars.Add(bv); while (la.kind == 19) { @@ -2158,7 +2174,7 @@ List/*!*/ decreases) { } Expect(16); Expression(out range); - if (la.kind == 103 || la.kind == 104) { + if (la.kind == 102 || la.kind == 103) { QSep(); Expression(out body); } @@ -2192,19 +2208,19 @@ List/*!*/ decreases) { } void Forall() { - if (la.kind == 99) { + if (la.kind == 98) { Get(); - } else if (la.kind == 100) { + } else if (la.kind == 99) { Get(); - } else SynErr(142); + } else SynErr(141); } void Exists() { - if (la.kind == 101) { + if (la.kind == 100) { Get(); - } else if (la.kind == 102) { + } else if (la.kind == 101) { Get(); - } else SynErr(143); + } else SynErr(142); } void AttributeOrTrigger(ref Attributes attrs, ref Triggers trigs) { @@ -2217,16 +2233,16 @@ List/*!*/ decreases) { es = new List(); Expressions(es); trigs = new Triggers(es, trigs); - } else SynErr(144); + } else SynErr(143); Expect(8); } void QSep() { - if (la.kind == 103) { + if (la.kind == 102) { Get(); - } else if (la.kind == 104) { + } else if (la.kind == 103) { Get(); - } else SynErr(145); + } else SynErr(144); } void AttributeBody(ref Attributes attrs) { @@ -2253,32 +2269,32 @@ 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, x,T,x,x, x,T,T,T, T,T,T,x, x,x,T,x, T,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x}, - {x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,T,x, T,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x}, - {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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}, - {x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x}, - {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, T,x,x,T, T,T,T,x, x,x,x}, - {x,T,T,x, x,x,x,T, x,x,x,T, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,T, x,x,x,T, x,T,T,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x}, - {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, T,x,x,T, T,T,T,x, x,x,x}, - {x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x}, - {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,T,T, x,x,T,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, T,x,x,T, T,T,T,x, x,x,x}, - {x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,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,T, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x}, - {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,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,T, x,x,x,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, 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,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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, T,x,x,T, T,T,T,x, x,x,x} + {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, + {x,x,x,x, x,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,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,x,x, 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,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x}, + {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,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,x,x, 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,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,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, + {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,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,T, x,x,x,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,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,x,x, 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 @@ -2287,18 +2303,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; @@ -2381,7 +2399,7 @@ public class Errors { case 77: s = "\">=\" expected"; break; case 78: s = "\"!=\" expected"; break; case 79: s = "\"!!\" expected"; break; - case 80: 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; @@ -2389,68 +2407,67 @@ public class Errors { 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 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 109: s = "invalid MethodSpec"; 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 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 115: s = "invalid OneStmt"; break; - case 116: s = "invalid OneStmt"; break; - case 117: s = "invalid UpdateStmt"; break; + case 116: s = "invalid UpdateStmt"; break; + case 117: s = "invalid IfStmt"; break; case 118: s = "invalid IfStmt"; 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 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 135: s = "invalid Suffix"; break; case 136: s = "invalid Suffix"; 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 AttributeOrTrigger"; break; - case 145: s = "invalid QSep"; 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 AttributeOrTrigger"; 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 @@ -2458,8 +2475,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/Scanner.cs b/Dafny/Scanner.cs index 5014ec39..b23cdb25 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 = 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); -} + 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); + } + 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; @@ -256,43 +259,43 @@ void objectInvariant(){ start[97] = 10; start[123] = 17; start[125] = 18; - start[61] = 57; - start[124] = 58; + start[61] = 55; + start[124] = 56; start[59] = 19; start[44] = 20; - start[58] = 59; - start[60] = 60; - start[62] = 61; + start[58] = 57; + start[60] = 58; + start[62] = 59; start[40] = 21; start[41] = 22; start[42] = 23; start[96] = 24; start[91] = 26; start[93] = 27; - start[46] = 62; + start[46] = 60; start[8660] = 31; start[8658] = 33; start[38] = 34; start[8743] = 36; start[8744] = 38; - start[33] = 63; - start[8800] = 44; - start[8804] = 45; - start[8805] = 46; - start[43] = 47; - start[45] = 48; - start[47] = 49; - start[37] = 50; - start[172] = 51; - start[8704] = 53; - start[8707] = 54; - start[8226] = 56; + start[33] = 61; + start[8800] = 42; + start[8804] = 43; + start[8805] = 44; + start[43] = 45; + start[45] = 46; + start[47] = 47; + start[37] = 48; + start[172] = 49; + start[8704] = 51; + start[8707] = 52; + start[8226] = 54; 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; } - + } } @@ -530,16 +531,16 @@ void objectInvariant(){ case "assert": t.kind = 64; break; case "assume": t.kind = 65; break; case "print": t.kind = 66; break; - case "false": t.kind = 90; break; - case "true": t.kind = 91; break; - case "null": t.kind = 92; break; - case "this": t.kind = 93; break; - case "fresh": t.kind = 94; break; - case "allocated": t.kind = 95; break; - case "old": t.kind = 96; break; - case "then": t.kind = 97; break; - case "forall": t.kind = 99; break; - case "exists": t.kind = 101; 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; default: break; } } @@ -556,10 +557,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: { @@ -690,73 +694,67 @@ void objectInvariant(){ case 41: {t.kind = 79; break;} case 42: - if (ch == 'n') {AddCh(); goto case 43;} - else {goto case 0;} + {t.kind = 81; break;} case 43: - {t.kind = 80; break;} + {t.kind = 82; break;} case 44: - {t.kind = 81; break;} + {t.kind = 83; break;} case 45: - {t.kind = 82; break;} + {t.kind = 84; break;} case 46: - {t.kind = 83; break;} + {t.kind = 85; break;} case 47: - {t.kind = 84; break;} + {t.kind = 86; break;} case 48: - {t.kind = 85; break;} + {t.kind = 87; break;} case 49: - {t.kind = 86; break;} + {t.kind = 88; break;} case 50: - {t.kind = 87; break;} + {t.kind = 97; break;} case 51: - {t.kind = 89; break;} + {t.kind = 99; break;} case 52: - {t.kind = 98; break;} + {t.kind = 101; break;} case 53: - {t.kind = 100; break;} - case 54: {t.kind = 102; break;} - case 55: + case 54: {t.kind = 103; break;} - case 56: - {t.kind = 104; break;} - case 57: + case 55: recEnd = pos; recKind = 15; if (ch == '>') {AddCh(); goto case 28;} - else if (ch == '=') {AddCh(); goto case 64;} + else if (ch == '=') {AddCh(); goto case 62;} else {t.kind = 15; break;} - case 58: + case 56: recEnd = pos; recKind = 16; if (ch == '|') {AddCh(); goto case 37;} else {t.kind = 16; break;} - case 59: + case 57: recEnd = pos; recKind = 22; if (ch == '=') {AddCh(); goto case 25;} - else if (ch == ':') {AddCh(); goto case 55;} + else if (ch == ':') {AddCh(); goto case 53;} else {t.kind = 22; break;} - case 60: + case 58: recEnd = pos; recKind = 23; - if (ch == '=') {AddCh(); goto case 65;} + if (ch == '=') {AddCh(); goto case 63;} else {t.kind = 23; break;} - case 61: + case 59: recEnd = pos; recKind = 24; if (ch == '=') {AddCh(); goto case 39;} else {t.kind = 24; break;} - case 62: + case 60: recEnd = pos; recKind = 53; - if (ch == '.') {AddCh(); goto case 52;} + if (ch == '.') {AddCh(); goto case 50;} else {t.kind = 53; break;} - case 63: - recEnd = pos; recKind = 88; + case 61: + recEnd = pos; recKind = 80; if (ch == '=') {AddCh(); goto case 40;} else if (ch == '!') {AddCh(); goto case 41;} - else if (ch == 'i') {AddCh(); goto case 42;} - else {t.kind = 88; break;} - case 64: + else {t.kind = 80; break;} + case 62: recEnd = pos; recKind = 75; if (ch == '>') {AddCh(); goto case 32;} else {t.kind = 75; break;} - case 65: + case 63: recEnd = pos; recKind = 76; if (ch == '=') {AddCh(); goto case 29;} else {t.kind = 76; break;} @@ -765,14 +763,14 @@ void objectInvariant(){ 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); @@ -793,7 +791,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 998eeb3a..0c5be389 100644 --- a/Dafny/Translator.cs +++ b/Dafny/Translator.cs @@ -362,17 +362,13 @@ namespace Microsoft.Dafny { if (bvs.Length != 0) { q = new Bpl.ExistsExpr(ctor.tok, bvs, q); } - var queryFunctionName = string.Format("{0}.{1}?", ctor.EnclosingDatatype.Name, ctor.Name); - q = Bpl.Expr.Imp(FunctionCall(ctor.tok, queryFunctionName, Bpl.Type.Bool, dId), q); + q = Bpl.Expr.Imp(FunctionCall(ctor.tok, ctor.QueryField.FullName, Bpl.Type.Bool, dId), q); q = new Bpl.ForallExpr(ctor.tok, new VariableSeq(dBv), q); sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q)); - // Add: function dt.ctor?(d: DatatypeType): bool { DatatypeCtorId(d) == ##dt.ctor } - var d = new Bpl.Formal(ctor.tok, new Bpl.TypedIdent(ctor.tok, "d", predef.DatatypeType), true); - var res = new Bpl.Formal(ctor.tok, new Bpl.TypedIdent(ctor.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false); - fn = new Bpl.Function(ctor.tok, queryFunctionName, new VariableSeq(d), res); - fieldFunctions.Add(ctor.QueryField, fn); - lhs = FunctionCall(ctor.tok, BuiltinFunction.DatatypeCtorId, null, new Bpl.IdentifierExpr(ctor.tok, d.Name, predef.DatatypeType)); + // Add: function dt.ctor?(this: DatatypeType): bool { DatatypeCtorId(this) == ##dt.ctor } + fn = GetReadonlyField(ctor.QueryField); + lhs = FunctionCall(ctor.tok, BuiltinFunction.DatatypeCtorId, null, new Bpl.IdentifierExpr(ctor.tok, fn.InParams[0].Name, predef.DatatypeType)); fn.Body = Bpl.Expr.Eq(lhs, new Bpl.IdentifierExpr(ctor.tok, cid)); // this uses the "cid" defined for the previous axiom sink.TopLevelDeclarations.Add(fn); @@ -405,14 +401,16 @@ namespace Microsoft.Dafny { i = 0; foreach (Formal arg in ctor.Formals) { // function ##dt.ctor#i(DatatypeType) returns (Ti); - argTypes = new Bpl.VariableSeq(); - argTypes.Add(new Bpl.Formal(ctor.tok, new Bpl.TypedIdent(ctor.tok, Bpl.TypedIdent.NoName, predef.DatatypeType), true)); - resType = new Bpl.Formal(arg.tok, new Bpl.TypedIdent(arg.tok, Bpl.TypedIdent.NoName, TrType(arg.Type)), false); - string nm = arg.HasName ? string.Format("{0}.{1}", ctor.EnclosingDatatype.Name, arg.Name) : "#" + ctor.FullName + "#" + i; - fn = new Bpl.Function(ctor.tok, nm, argTypes, resType); var sf = ctor.Destructors[i]; if (sf != null) { - fieldFunctions.Add(sf, fn); + fn = GetReadonlyField(sf); + } else { + Contract.Assert(!arg.HasName); + argTypes = new Bpl.VariableSeq(); + argTypes.Add(new Bpl.Formal(ctor.tok, new Bpl.TypedIdent(ctor.tok, Bpl.TypedIdent.NoName, predef.DatatypeType), true)); + resType = new Bpl.Formal(arg.tok, new Bpl.TypedIdent(arg.tok, Bpl.TypedIdent.NoName, TrType(arg.Type)), false); + string nm = "#" + ctor.FullName + "#" + i; + fn = new Bpl.Function(ctor.tok, nm, argTypes, resType); } sink.TopLevelDeclarations.Add(fn); // axiom (forall params :: ##dt.ctor#i(#dt.ctor(params)) == params_i); @@ -1453,13 +1451,19 @@ namespace Microsoft.Dafny { Contract.Requires(predef != null); Contract.Ensures(Contract.Result() != null); - VariableSeq bvars; - List args; - CreateBoundVariables(ctor.Formals, out bvars, out args); - locals.AddRange(bvars); + // create local variables for the formals + var args = new ExprSeq(); + foreach (Formal arg in ctor.Formals) { + Contract.Assert(arg != null); + var nm = string.Format("a{0}#{1}", args.Length, otherTmpVarCount); + otherTmpVarCount++; + Bpl.Variable bv = new Bpl.LocalVariable(arg.tok, new Bpl.TypedIdent(arg.tok, nm, TrType(arg.Type))); + locals.Add(bv); + args.Add(new Bpl.IdentifierExpr(arg.tok, bv)); + } Bpl.IdentifierExpr id = new Bpl.IdentifierExpr(tok, ctor.FullName, predef.DatatypeType); - return new Bpl.NAryExpr(tok, new Bpl.FunctionCall(id), new ExprSeq(args.ToArray())); + return new Bpl.NAryExpr(tok, new Bpl.FunctionCall(id), args); } Bpl.Expr IsTotal(Expression expr, ExpressionTranslator etran) { -- cgit v1.2.3