From 4525fe31770419570d9ddd7a9e1faa836720b353 Mon Sep 17 00:00:00 2001 From: tabarbe Date: Wed, 4 Aug 2010 22:28:39 +0000 Subject: Dafny: Made line endings consistent --- Source/Dafny/Dafny.atg | 12 +- Source/Dafny/Parser.cs | 508 +++++++++++++++++++------------------- Source/Dafny/Scanner.cs | 72 +++--- Source/Dafny/Translator.cs | 2 +- Source/DafnyDriver/DafnyDriver.cs | 2 +- 5 files changed, 298 insertions(+), 298 deletions(-) (limited to 'Source') diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 538a2865..85cf64fe 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -211,7 +211,7 @@ ClassDecl } "}" (. if (optionalId == null) - c = new ClassDecl(id, id.val, module, typeArgs, members, attrs); + c = new ClassDecl(id, id.val, module, typeArgs, members, attrs); else c = new ClassRefinementDecl(id, id.val, module, typeArgs, members, attrs, optionalId); .) @@ -306,7 +306,7 @@ CouplingInvDecl<.MemberModifiers mmod, List/*!*/ mm.> "by" Expression ";" - (. mm.Add(new CouplingInvariant(ids, e, attrs)); + (. mm.Add(new CouplingInvariant(ids, e, attrs)); parseVarScope.PopMarker(); .) . @@ -368,7 +368,7 @@ TypeIdentOptional/*!*/ typeArgs.> -= (. Contract.Requires(cce.NonNullElements(typeArgs)); += (. Contract.Requires(cce.NonNullElements(typeArgs)); IToken/*!*/ id; .) "<" Ident (. typeArgs.Add(new TypeParameter(id, id.val)); .) @@ -415,7 +415,7 @@ MethodDecl if (isRefinement) m = new MethodRefinement(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs); else - m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs); + m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs); .) . @@ -553,7 +553,7 @@ FunctionDecl . FunctionSpec<.List/*!*/ reqs, List/*!*/ reads, List/*!*/ decreases.> -= (. Contract.Requires(cce.NonNullElements(reqs)); Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(cce.NonNullElements(decreases)); += (. Contract.Requires(cce.NonNullElements(reqs)); Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(cce.NonNullElements(decreases)); Expression/*!*/ e; FrameExpression/*!*/ fe; .) ( "requires" Expression ";" (. reqs.Add(e); .) | "reads" [ PossiblyWildFrameExpression (. reads.Add(fe); .) @@ -1105,7 +1105,7 @@ NegOp = "!" | '\u00ac'. ConstAtomExpression = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x, dtName, id; BigInteger n; List/*!*/ elements; - e = dummyExpr; + e = dummyExpr; .) ( "false" (. e = new LiteralExpr(t, false); .) | "true" (. e = new LiteralExpr(t, true); .) diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 7f03fcf2..ec029451 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -213,7 +213,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List(); + attrs = null; theImports = new List(); while (la.kind == 6) { Attribute(ref attrs); } @@ -222,25 +222,25 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List/*!*/ ids) { - IToken/*!*/ id; + IToken/*!*/ id; Ident(out id); - ids.Add(id.val); + ids.Add(id.val); while (la.kind == 16) { Get(); Ident(out id); - ids.Add(id.val); + ids.Add(id.val); } } @@ -306,7 +306,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List/*!*/ mm) { @@ -353,38 +353,38 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List/*!*/ typeArgs) { - Contract.Requires(cce.NonNullElements(typeArgs)); - IToken/*!*/ id; + Contract.Requires(cce.NonNullElements(typeArgs)); + IToken/*!*/ id; Expect(20); Ident(out id); - typeArgs.Add(new TypeParameter(id, id.val)); + typeArgs.Add(new TypeParameter(id, id.val)); while (la.kind == 16) { Get(); Ident(out id); - typeArgs.Add(new TypeParameter(id, id.val)); + typeArgs.Add(new TypeParameter(id, id.val)); } Expect(21); } @@ -402,11 +402,11 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List/*!*/ formals) { - Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; string/*!*/ name; bool isGhost; + Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; string/*!*/ name; bool isGhost; Expect(29); if (StartOf(6)) { TypeIdentOptional(out id, out name, out ty, out isGhost); - formals.Add(new Formal(id, name, ty, true, isGhost)); parseVarScope.Push(name, name); + formals.Add(new Formal(id, name, ty, true, isGhost)); parseVarScope.Push(name, name); while (la.kind == 16) { Get(); TypeIdentOptional(out id, out name, out ty, out isGhost); - formals.Add(new Formal(id, name, ty, true, isGhost)); parseVarScope.Push(name, name); + formals.Add(new Formal(id, name, ty, true, isGhost)); parseVarScope.Push(name, name); } } Expect(30); @@ -597,13 +597,13 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List(); + tok = t; gt = new List(); GenericInstantiation(gt); if (gt.Count != 1) { SemErr("set type expects exactly one type argument"); @@ -687,7 +687,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List(); + tok = t; gt = new List(); GenericInstantiation(gt); if (gt.Count != 1) { SemErr("seq type expects exactly one type argument"); @@ -700,15 +700,15 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List/*!*/ formals) { - Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; bool isGhost; + Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; bool isGhost; Expect(29); if (la.kind == 1 || la.kind == 10) { GIdentType(allowGhosts, out id, out ty, out isGhost); - formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); parseVarScope.Push(id.val, id.val); + formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); parseVarScope.Push(id.val, id.val); while (la.kind == 16) { Get(); GIdentType(allowGhosts, out id, out ty, out isGhost); - formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); parseVarScope.Push(id.val, id.val); + formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); parseVarScope.Push(id.val, id.val); } } Expect(30); @@ -723,29 +723,29 @@ List/*!*/ decreases) { Get(); if (StartOf(8)) { FrameExpression(out fe); - mod.Add(fe); + mod.Add(fe); while (la.kind == 16) { Get(); FrameExpression(out fe); - mod.Add(fe); + mod.Add(fe); } } Expect(14); } else if (la.kind == 25 || la.kind == 26 || la.kind == 27) { if (la.kind == 25) { Get(); - isFree = true; + isFree = true; } if (la.kind == 26) { Get(); Expression(out e); Expect(14); - req.Add(new MaybeFreeExpression(e, isFree)); + req.Add(new MaybeFreeExpression(e, isFree)); } else if (la.kind == 27) { Get(); Expression(out e); Expect(14); - ens.Add(new MaybeFreeExpression(e, isFree)); + ens.Add(new MaybeFreeExpression(e, isFree)); } else SynErr(110); } else if (la.kind == 28) { Get(); @@ -759,48 +759,48 @@ List/*!*/ decreases) { List body = new List(); Statement/*!*/ s; - parseVarScope.PushMarker(); + parseVarScope.PushMarker(); Expect(6); - x = t; + x = t; while (StartOf(9)) { Stmt(body); } Expect(7); - block = new BlockStmt(x, body); - parseVarScope.PopMarker(); + block = new BlockStmt(x, body); + parseVarScope.PopMarker(); } void FrameExpression(out FrameExpression/*!*/ fe) { - Contract.Ensures(Contract.ValueAtReturn(out fe) != null); Expression/*!*/ e; IToken/*!*/ id; string fieldName = null; + Contract.Ensures(Contract.ValueAtReturn(out fe) != null); Expression/*!*/ e; IToken/*!*/ id; string fieldName = null; Expression(out e); if (la.kind == 40) { Get(); Ident(out id); - fieldName = id.val; + fieldName = id.val; } - fe = new FrameExpression(e, fieldName); + fe = new FrameExpression(e, fieldName); } void Expressions(List/*!*/ args) { - Contract.Requires(cce.NonNullElements(args)); Expression/*!*/ e; + Contract.Requires(cce.NonNullElements(args)); Expression/*!*/ e; Expression(out e); - args.Add(e); + args.Add(e); while (la.kind == 16) { Get(); Expression(out e); - args.Add(e); + args.Add(e); } } void GenericInstantiation(List/*!*/ gt) { - Contract.Requires(cce.NonNullElements(gt)); Type/*!*/ ty; + Contract.Requires(cce.NonNullElements(gt)); Type/*!*/ ty; Expect(20); Type(out ty); - gt.Add(ty); + gt.Add(ty); while (la.kind == 16) { Get(); Type(out ty); - gt.Add(ty); + gt.Add(ty); } Expect(21); } @@ -812,10 +812,10 @@ List/*!*/ decreases) { if (la.kind == 35) { Get(); - tok = t; ty = new ObjectType(); + tok = t; ty = new ObjectType(); } else if (la.kind == 36) { Get(); - tok = t; gt = new List(); + tok = t; gt = new List(); GenericInstantiation(gt); if (gt.Count != 1) { SemErr("array type expects exactly one type argument"); @@ -824,31 +824,31 @@ List/*!*/ decreases) { } else if (la.kind == 1) { Ident(out tok); - gt = new List(); + gt = new List(); if (la.kind == 20) { GenericInstantiation(gt); } - ty = new UserDefinedType(tok, tok.val, gt); + ty = new UserDefinedType(tok, tok.val, gt); } else SynErr(112); } void FunctionSpec(List/*!*/ reqs, List/*!*/ reads, List/*!*/ decreases) { - Contract.Requires(cce.NonNullElements(reqs)); Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(cce.NonNullElements(decreases)); - Expression/*!*/ e; FrameExpression/*!*/ fe; + Contract.Requires(cce.NonNullElements(reqs)); Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(cce.NonNullElements(decreases)); + Expression/*!*/ e; FrameExpression/*!*/ fe; if (la.kind == 26) { Get(); Expression(out e); Expect(14); - reqs.Add(e); + reqs.Add(e); } else if (la.kind == 38) { Get(); if (StartOf(10)) { PossiblyWildFrameExpression(out fe); - reads.Add(fe); + reads.Add(fe); while (la.kind == 16) { Get(); PossiblyWildFrameExpression(out fe); - reads.Add(fe); + reads.Add(fe); } } Expect(14); @@ -860,7 +860,7 @@ List/*!*/ decreases) { } void FunctionBody(out Expression/*!*/ e) { - Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr; + Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr; Expect(6); if (la.kind == 41) { MatchExpression(out e); @@ -871,10 +871,10 @@ List/*!*/ decreases) { } void PossiblyWildFrameExpression(out FrameExpression/*!*/ fe) { - Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr; + Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr; if (la.kind == 39) { Get(); - fe = new FrameExpression(new WildcardExpr(t), null); + fe = new FrameExpression(new WildcardExpr(t), null); } else if (StartOf(8)) { FrameExpression(out fe); } else SynErr(115); @@ -882,10 +882,10 @@ List/*!*/ decreases) { void PossiblyWildExpression(out Expression/*!*/ e) { Contract.Ensures(Contract.ValueAtReturn(out e)!=null); - e = dummyExpr; + e = dummyExpr; if (la.kind == 39) { Get(); - e = new WildcardExpr(t); + e = new WildcardExpr(t); } else if (StartOf(8)) { Expression(out e); } else SynErr(116); @@ -896,13 +896,13 @@ List/*!*/ decreases) { List cases = new List(); Expect(41); - x = t; + x = t; Expression(out e); while (la.kind == 42) { CaseExpression(out c); - cases.Add(c); + cases.Add(c); } - e = new MatchExpr(x, e, cases); + e = new MatchExpr(x, e, cases); } void CaseExpression(out MatchCaseExpr/*!*/ c) { @@ -911,36 +911,36 @@ List/*!*/ decreases) { Expression/*!*/ body; Expect(42); - x = t; parseVarScope.PushMarker(); + x = t; parseVarScope.PushMarker(); Ident(out id); if (la.kind == 29) { Get(); Ident(out arg); arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy())); - parseVarScope.Push(arg.val, arg.val); + parseVarScope.Push(arg.val, arg.val); while (la.kind == 16) { Get(); Ident(out arg); arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy())); - parseVarScope.Push(arg.val, arg.val); + parseVarScope.Push(arg.val, arg.val); } Expect(30); } Expect(43); Expression(out body); c = new MatchCaseExpr(x, id.val, arguments, body); - parseVarScope.PopMarker(); + parseVarScope.PopMarker(); } void Stmt(List/*!*/ ss) { - Contract.Requires(cce.NonNullElements(ss)); Statement/*!*/ s; + Contract.Requires(cce.NonNullElements(ss)); Statement/*!*/ s; while (la.kind == 6) { BlockStmt(out s); - ss.Add(s); + ss.Add(s); } if (StartOf(11)) { OneStmt(out s); - ss.Add(s); + ss.Add(s); } else if (la.kind == 10 || la.kind == 15) { VarDeclStmts(ss); } else SynErr(117); @@ -997,28 +997,28 @@ List/*!*/ decreases) { } case 44: { Get(); - x = t; + x = t; Ident(out id); Expect(19); - s = new LabelStmt(x, id.val); + s = new LabelStmt(x, id.val); break; } case 45: { Get(); - x = t; + x = t; if (la.kind == 1) { Ident(out id); - label = id.val; + label = id.val; } Expect(14); - s = new BreakStmt(x, label); + s = new BreakStmt(x, label); break; } case 46: { Get(); - x = t; + x = t; Expect(14); - s = new ReturnStmt(x); + s = new ReturnStmt(x); break; } default: SynErr(118); break; @@ -1026,47 +1026,47 @@ List/*!*/ decreases) { } void VarDeclStmts(List/*!*/ ss) { - Contract.Requires(cce.NonNullElements(ss)); VarDecl/*!*/ d; bool isGhost = false; + Contract.Requires(cce.NonNullElements(ss)); VarDecl/*!*/ d; bool isGhost = false; if (la.kind == 10) { Get(); - isGhost = true; + isGhost = true; } Expect(15); IdentTypeRhs(out d, isGhost); - ss.Add(d); parseVarScope.Push(d.Name, d.Name); + ss.Add(d); parseVarScope.Push(d.Name, d.Name); while (la.kind == 16) { Get(); IdentTypeRhs(out d, isGhost); - ss.Add(d); parseVarScope.Push(d.Name, d.Name); + ss.Add(d); parseVarScope.Push(d.Name, d.Name); } Expect(14); } void AssertStmt(out Statement/*!*/ s) { - Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e; + Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e; Expect(60); - x = t; + x = t; Expression(out e); Expect(14); - s = new AssertStmt(x, e); + s = new AssertStmt(x, e); } void AssumeStmt(out Statement/*!*/ s) { - Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e; + Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e; Expect(61); - x = t; + x = t; Expression(out e); Expect(14); - s = new AssumeStmt(x, e); + s = new AssumeStmt(x, e); } void UseStmt(out Statement/*!*/ s) { - Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e; + Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e; Expect(62); - x = t; + x = t; Expression(out e); Expect(14); - s = new UseStmt(x, e); + s = new UseStmt(x, e); } void PrintStmt(out Statement/*!*/ s) { @@ -1074,16 +1074,16 @@ List/*!*/ decreases) { List args = new List(); Expect(63); - x = t; + x = t; AttributeArg(out arg); - args.Add(arg); + args.Add(arg); while (la.kind == 16) { Get(); AttributeArg(out arg); - args.Add(arg); + args.Add(arg); } Expect(14); - s = new PrintStmt(x, args); + s = new PrintStmt(x, args); } void AssignStmt(out Statement/*!*/ s) { @@ -1095,7 +1095,7 @@ List/*!*/ decreases) { LhsExpr(out lhs); Expect(47); - x = t; + x = t; AssignRhs(out rhs, out ty); if (ty == null) { Contract.Assert(rhs != null); @@ -1110,12 +1110,12 @@ List/*!*/ decreases) { } void HavocStmt(out Statement/*!*/ s) { - Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ lhs; + Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ lhs; Expect(51); - x = t; + x = t; LhsExpr(out lhs); Expect(14); - s = new AssignStmt(x, lhs); + s = new AssignStmt(x, lhs); } void CallStmt(out Statement/*!*/ s) { @@ -1125,7 +1125,7 @@ List/*!*/ decreases) { List newVars = new List(); Expect(56); - x = t; + x = t; CallStmtSubExpr(out e); if (la.kind == 16 || la.kind == 47) { if (la.kind == 16) { @@ -1140,11 +1140,11 @@ List/*!*/ decreases) { } Ident(out id); - RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars); + RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars); while (la.kind == 16) { Get(); Ident(out id); - RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars); + RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars); } Expect(47); CallStmtSubExpr(out e); @@ -1181,20 +1181,20 @@ List/*!*/ decreases) { Statement els = null; Expect(52); - x = t; + x = t; Guard(out guard); BlockStmt(out thn); if (la.kind == 53) { Get(); if (la.kind == 52) { IfStmt(out s); - els = s; + els = s; } else if (la.kind == 6) { BlockStmt(out s); - els = s; + els = s; } else SynErr(119); } - ifStmt = new IfStmt(x, guard, thn, els); + ifStmt = new IfStmt(x, guard, thn, els); } void WhileStmt(out Statement/*!*/ stmt) { @@ -1206,50 +1206,50 @@ List/*!*/ decreases) { Statement/*!*/ body; Expect(54); - x = t; + x = t; Guard(out guard); - Contract.Assume(guard == null || cce.Owner.None(guard)); + Contract.Assume(guard == null || cce.Owner.None(guard)); while (la.kind == 25 || la.kind == 28 || la.kind == 55) { if (la.kind == 25 || la.kind == 55) { - isFree = false; + isFree = false; if (la.kind == 25) { Get(); - isFree = true; + isFree = true; } Expect(55); Expression(out e); - invariants.Add(new MaybeFreeExpression(e, isFree)); + invariants.Add(new MaybeFreeExpression(e, isFree)); Expect(14); } else { Get(); PossiblyWildExpression(out e); - decreases.Add(e); + decreases.Add(e); while (la.kind == 16) { Get(); PossiblyWildExpression(out e); - decreases.Add(e); + decreases.Add(e); } Expect(14); } } BlockStmt(out body); - stmt = new WhileStmt(x, guard, invariants, decreases, body); + stmt = new WhileStmt(x, guard, invariants, decreases, body); } void MatchStmt(out Statement/*!*/ s) { Contract.Ensures(Contract.ValueAtReturn(out s) != null); Token x; Expression/*!*/ e; MatchCaseStmt/*!*/ c; - List cases = new List(); + List cases = new List(); Expect(41); - x = t; + x = t; Expression(out e); Expect(6); while (la.kind == 42) { CaseStatement(out c); - cases.Add(c); + cases.Add(c); } Expect(7); - s = new MatchStmt(x, e, cases); + s = new MatchStmt(x, e, cases); } void ForeachStmt(out Statement/*!*/ s) { @@ -1260,7 +1260,7 @@ List/*!*/ decreases) { List bodyPrefix = new List(); AssignStmt bodyAssign = null; - parseVarScope.PushMarker(); + parseVarScope.PushMarker(); Expect(57); x = t; range = new LiteralExpr(x, true); @@ -1274,7 +1274,7 @@ List/*!*/ decreases) { } Expect(58); Expression(out collection); - parseVarScope.Push(boundVar.val, boundVar.val); + parseVarScope.Push(boundVar.val, boundVar.val); if (la.kind == 59) { Get(); Expression(out range); @@ -1307,7 +1307,7 @@ List/*!*/ decreases) { s = dummyStmt; // some error occurred in parsing the bodyAssign } - parseVarScope.PopMarker(); + parseVarScope.PopMarker(); } void LhsExpr(out Expression/*!*/ e) { @@ -1322,22 +1322,22 @@ List/*!*/ decreases) { if (la.kind == 48) { Get(); TypeAndToken(out x, out tt); - ty = tt; + ty = tt; if (la.kind == 49) { Get(); Expression(out ee); Expect(50); - e = ee; + e = ee; } } else if (StartOf(8)) { Expression(out ee); - e = ee; + e = ee; } else SynErr(121); if (e == null && ty == null) { e = dummyExpr; } } void SelectExpression(out Expression/*!*/ e) { - Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ id; e = dummyExpr; + Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ id; e = dummyExpr; if (la.kind == 1) { IdentOrFuncExpression(out e); } else if (la.kind == 29 || la.kind == 95 || la.kind == 96) { @@ -1357,7 +1357,7 @@ List/*!*/ decreases) { if (la.kind == 19) { Get(); Type(out ty); - optionalType = ty; + optionalType = ty; } if (la.kind == 47) { Get(); @@ -1379,14 +1379,14 @@ List/*!*/ decreases) { } void Guard(out Expression e) { - Expression/*!*/ ee; e = null; + Expression/*!*/ ee; e = null; Expect(29); if (la.kind == 39) { Get(); - e = null; + e = null; } else if (StartOf(8)) { Expression(out ee); - e = ee; + e = ee; } else SynErr(123); Expect(30); } @@ -1398,33 +1398,33 @@ List/*!*/ decreases) { List body = new List(); Expect(42); - x = t; parseVarScope.PushMarker(); + x = t; parseVarScope.PushMarker(); Ident(out id); if (la.kind == 29) { Get(); Ident(out arg); arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy())); - parseVarScope.Push(arg.val, arg.val); + parseVarScope.Push(arg.val, arg.val); while (la.kind == 16) { Get(); Ident(out arg); arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy())); - parseVarScope.Push(arg.val, arg.val); + parseVarScope.Push(arg.val, arg.val); } Expect(30); } Expect(43); - parseVarScope.PushMarker(); + parseVarScope.PushMarker(); while (StartOf(9)) { Stmt(body); } - parseVarScope.PopMarker(); - c = new MatchCaseStmt(x, id.val, arguments, body); - parseVarScope.PopMarker(); + parseVarScope.PopMarker(); + c = new MatchCaseStmt(x, id.val, arguments, body); + parseVarScope.PopMarker(); } void CallStmtSubExpr(out Expression/*!*/ e) { - Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr; + Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr; if (la.kind == 1) { IdentOrFuncExpression(out e); } else if (la.kind == 29 || la.kind == 95 || la.kind == 96) { @@ -1437,35 +1437,35 @@ List/*!*/ decreases) { } void AttributeArg(out Attributes.Argument/*!*/ arg) { - Contract.Ensures(Contract.ValueAtReturn(out arg) != null); Expression/*!*/ e; arg = dummyAttrArg; + Contract.Ensures(Contract.ValueAtReturn(out arg) != null); Expression/*!*/ e; arg = dummyAttrArg; if (la.kind == 3) { Get(); - arg = new Attributes.Argument(t.val.Substring(1, t.val.Length-2)); + arg = new Attributes.Argument(t.val.Substring(1, t.val.Length-2)); } else if (StartOf(8)) { Expression(out e); - arg = new Attributes.Argument(e); + arg = new Attributes.Argument(e); } else SynErr(125); } void EquivExpression(out Expression/*!*/ e0) { - Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; + Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; ImpliesExpression(out e0); while (la.kind == 65 || la.kind == 66) { EquivOp(); - x = t; + x = t; ImpliesExpression(out e1); - e0 = new BinaryExpr(x, BinaryExpr.Opcode.Iff, e0, e1); + e0 = new BinaryExpr(x, BinaryExpr.Opcode.Iff, e0, e1); } } void ImpliesExpression(out Expression/*!*/ e0) { - Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; + Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; LogicalExpression(out e0); if (la.kind == 67 || la.kind == 68) { ImpliesOp(); - x = t; + x = t; ImpliesExpression(out e1); - e0 = new BinaryExpr(x, BinaryExpr.Opcode.Imp, e0, e1); + e0 = new BinaryExpr(x, BinaryExpr.Opcode.Imp, e0, e1); } } @@ -1478,30 +1478,30 @@ List/*!*/ decreases) { } void LogicalExpression(out Expression/*!*/ e0) { - Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; + Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; RelationalExpression(out e0); if (StartOf(13)) { if (la.kind == 69 || la.kind == 70) { AndOp(); - x = t; + x = t; RelationalExpression(out e1); - e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); + e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); while (la.kind == 69 || la.kind == 70) { AndOp(); - x = t; + x = t; RelationalExpression(out e1); - e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); + e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); } } else { OrOp(); - x = t; + x = t; RelationalExpression(out e1); - e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); + e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); while (la.kind == 71 || la.kind == 72) { OrOp(); - x = t; + x = t; RelationalExpression(out e1); - e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); + e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); } } } @@ -1516,12 +1516,12 @@ List/*!*/ decreases) { } void RelationalExpression(out Expression/*!*/ e0) { - Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op; + Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op; Term(out e0); if (StartOf(14)) { RelOp(out x, out op); Term(out e1); - e0 = new BinaryExpr(x, op, e0, e1); + e0 = new BinaryExpr(x, op, e0, e1); } } @@ -1542,76 +1542,76 @@ List/*!*/ decreases) { } void Term(out Expression/*!*/ e0) { - Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op; + Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op; Factor(out e0); while (la.kind == 82 || la.kind == 83) { AddOp(out x, out op); Factor(out e1); - e0 = new BinaryExpr(x, op, e0, e1); + e0 = new BinaryExpr(x, op, e0, e1); } } 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)*/; switch (la.kind) { case 73: { Get(); - x = t; op = BinaryExpr.Opcode.Eq; + x = t; op = BinaryExpr.Opcode.Eq; break; } case 20: { Get(); - x = t; op = BinaryExpr.Opcode.Lt; + x = t; op = BinaryExpr.Opcode.Lt; break; } case 21: { Get(); - x = t; op = BinaryExpr.Opcode.Gt; + x = t; op = BinaryExpr.Opcode.Gt; break; } case 74: { Get(); - x = t; op = BinaryExpr.Opcode.Le; + x = t; op = BinaryExpr.Opcode.Le; break; } case 75: { Get(); - x = t; op = BinaryExpr.Opcode.Ge; + x = t; op = BinaryExpr.Opcode.Ge; break; } case 76: { Get(); - x = t; op = BinaryExpr.Opcode.Neq; + x = t; op = BinaryExpr.Opcode.Neq; break; } case 77: { Get(); - x = t; op = BinaryExpr.Opcode.Disjoint; + x = t; op = BinaryExpr.Opcode.Disjoint; break; } case 58: { Get(); - x = t; op = BinaryExpr.Opcode.In; + x = t; op = BinaryExpr.Opcode.In; break; } case 78: { Get(); - x = t; op = BinaryExpr.Opcode.NotIn; + x = t; op = BinaryExpr.Opcode.NotIn; break; } case 79: { Get(); - x = t; op = BinaryExpr.Opcode.Neq; + x = t; op = BinaryExpr.Opcode.Neq; break; } case 80: { Get(); - x = t; op = BinaryExpr.Opcode.Le; + x = t; op = BinaryExpr.Opcode.Le; break; } case 81: { Get(); - x = t; op = BinaryExpr.Opcode.Ge; + x = t; op = BinaryExpr.Opcode.Ge; break; } default: SynErr(130); break; @@ -1619,38 +1619,38 @@ List/*!*/ decreases) { } void Factor(out Expression/*!*/ e0) { - Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op; + Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op; UnaryExpression(out e0); while (la.kind == 39 || la.kind == 84 || la.kind == 85) { MulOp(out x, out op); UnaryExpression(out e1); - e0 = new BinaryExpr(x, op, e0, e1); + e0 = new BinaryExpr(x, op, e0, e1); } } void AddOp(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)*/; if (la.kind == 82) { Get(); - x = t; op = BinaryExpr.Opcode.Add; + x = t; op = BinaryExpr.Opcode.Add; } else if (la.kind == 83) { Get(); - x = t; op = BinaryExpr.Opcode.Sub; + x = t; op = BinaryExpr.Opcode.Sub; } else SynErr(131); } void UnaryExpression(out Expression/*!*/ e) { - Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr; + Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr; if (la.kind == 83) { Get(); - x = t; + x = t; UnaryExpression(out e); - e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e); + e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e); } else if (la.kind == 86 || la.kind == 87) { NegOp(); - x = t; + x = t; UnaryExpression(out e); - e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); + e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); } else if (StartOf(12)) { SelectExpression(out e); } else if (StartOf(15)) { @@ -1659,16 +1659,16 @@ List/*!*/ decreases) { } void MulOp(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)*/; if (la.kind == 39) { Get(); - x = t; op = BinaryExpr.Opcode.Mul; + x = t; op = BinaryExpr.Opcode.Mul; } else if (la.kind == 84) { Get(); - x = t; op = BinaryExpr.Opcode.Div; + x = t; op = BinaryExpr.Opcode.Div; } else if (la.kind == 85) { Get(); - x = t; op = BinaryExpr.Opcode.Mod; + x = t; op = BinaryExpr.Opcode.Mod; } else SynErr(133); } @@ -1682,36 +1682,36 @@ List/*!*/ decreases) { void ConstAtomExpression(out Expression/*!*/ e) { Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x, dtName, id; BigInteger n; List/*!*/ elements; - e = dummyExpr; + e = dummyExpr; switch (la.kind) { case 88: { Get(); - e = new LiteralExpr(t, false); + e = new LiteralExpr(t, false); break; } case 89: { Get(); - e = new LiteralExpr(t, true); + e = new LiteralExpr(t, true); break; } case 90: { Get(); - e = new LiteralExpr(t); + e = new LiteralExpr(t); break; } case 2: { Nat(out n); - e = new LiteralExpr(t, n); + e = new LiteralExpr(t, n); break; } case 91: { Get(); - x = t; + x = t; Ident(out dtName); Expect(92); Ident(out id); - elements = new List(); + elements = new List(); if (la.kind == 29) { Get(); if (StartOf(8)) { @@ -1719,43 +1719,43 @@ List/*!*/ decreases) { } Expect(30); } - e = new DatatypeValue(t, dtName.val, id.val, elements); + e = new DatatypeValue(t, dtName.val, id.val, elements); break; } case 93: { Get(); - x = t; + x = t; Expect(29); Expression(out e); Expect(30); - e = new FreshExpr(x, e); + e = new FreshExpr(x, e); break; } case 59: { Get(); - x = t; + x = t; Expression(out e); - e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e); + e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e); Expect(59); break; } case 6: { Get(); - x = t; elements = new List(); + x = t; elements = new List(); if (StartOf(8)) { Expressions(elements); } - e = new SetDisplayExpr(x, elements); + e = new SetDisplayExpr(x, elements); Expect(7); break; } case 49: { Get(); - x = t; elements = new List(); + x = t; elements = new List(); if (StartOf(8)) { Expressions(elements); } - e = new SeqDisplayExpr(x, elements); + e = new SeqDisplayExpr(x, elements); Expect(50); break; } @@ -1775,16 +1775,16 @@ List/*!*/ decreases) { } void IdentOrFuncExpression(out Expression/*!*/ e) { - Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ id; e = dummyExpr; List/*!*/ args; + Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ id; e = dummyExpr; List/*!*/ args; Ident(out id); if (la.kind == 29) { Get(); - args = new List(); + args = new List(); if (StartOf(8)) { Expressions(args); } Expect(30); - e = new FunctionCallExpr(id, id.val, new ImplicitThisExpr(id), args); + e = new FunctionCallExpr(id, id.val, new ImplicitThisExpr(id), args); } if (e == dummyExpr) { if (parseVarScope.Find(id.val) != null) { @@ -1797,17 +1797,17 @@ List/*!*/ decreases) { } void ObjectExpression(out Expression/*!*/ e) { - Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr; + Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr; if (la.kind == 95) { Get(); - e = new ThisExpr(t); + e = new ThisExpr(t); } else if (la.kind == 96) { Get(); - x = t; + x = t; Expect(29); Expression(out e); Expect(30); - e = new OldExpr(x, e); + e = new OldExpr(x, e); } else if (la.kind == 29) { Get(); if (StartOf(16)) { @@ -1829,38 +1829,38 @@ List/*!*/ decreases) { Ident(out id); if (la.kind == 29) { Get(); - args = new List(); func = true; + args = new List(); func = true; if (StartOf(8)) { Expressions(args); } Expect(30); - e = new FunctionCallExpr(id, id.val, e, args); + e = new FunctionCallExpr(id, id.val, e, args); } if (!func) { e = new FieldSelectExpr(id, e, id.val); } } else if (la.kind == 49) { Get(); - x = t; + x = t; if (StartOf(8)) { Expression(out ee); - e0 = ee; + e0 = ee; if (la.kind == 47 || la.kind == 94) { if (la.kind == 94) { Get(); - anyDots = true; + anyDots = true; if (StartOf(8)) { Expression(out ee); - e1 = ee; + e1 = ee; } } else { Get(); Expression(out ee); - e1 = ee; + e1 = ee; } } } else if (la.kind == 94) { Get(); Expression(out ee); - anyDots = true; e1 = ee; + anyDots = true; e1 = ee; } else SynErr(138); if (!anyDots && e0 == null) { /* a parsing error occurred */ @@ -1894,18 +1894,18 @@ List/*!*/ decreases) { if (la.kind == 97 || la.kind == 98) { Forall(); - x = t; univ = true; + x = t; univ = true; } else if (la.kind == 99 || la.kind == 100) { Exists(); - x = t; + x = t; } else SynErr(140); - parseVarScope.PushMarker(); + parseVarScope.PushMarker(); IdentTypeOptional(out bv); - bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name); + bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name); while (la.kind == 16) { Get(); IdentTypeOptional(out bv); - bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name); + bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name); } while (la.kind == 6) { AttributeOrTrigger(ref attrs, ref trigs); @@ -1944,9 +1944,9 @@ List/*!*/ decreases) { if (la.kind == 19) { AttributeBody(ref attrs); } else if (StartOf(8)) { - es = new List(); + es = new List(); Expressions(es); - trigs = new Triggers(es, trigs); + trigs = new Triggers(es, trigs); } else SynErr(143); Expect(7); } @@ -1966,17 +1966,17 @@ List/*!*/ decreases) { Expect(19); Expect(1); - aName = t.val; + aName = t.val; if (StartOf(17)) { AttributeArg(out aArg); - aArgs.Add(aArg); + aArgs.Add(aArg); while (la.kind == 16) { Get(); AttributeArg(out aArg); - aArgs.Add(aArg); + aArgs.Add(aArg); } } - attrs = new Attributes(aName, aArgs, attrs); + attrs = new Attributes(aName, aArgs, attrs); } diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs index e45ad610..b9f36a87 100644 --- a/Source/Dafny/Scanner.cs +++ b/Source/Dafny/Scanner.cs @@ -253,40 +253,40 @@ void objectInvariant(){ for (int i = 97; i <= 122; ++i) start[i] = 1; for (int i = 48; i <= 57; ++i) start[i] = 2; for (int i = 34; i <= 34; ++i) start[i] = 3; - start[123] = 5; - start[125] = 6; - start[59] = 7; - start[44] = 8; - start[58] = 46; - start[60] = 47; - start[62] = 48; - start[40] = 9; - start[41] = 10; - start[42] = 11; - start[96] = 12; - start[61] = 49; - start[91] = 15; - start[93] = 16; - start[124] = 50; - start[8660] = 19; - start[8658] = 21; - start[38] = 22; - start[8743] = 24; - start[8744] = 26; - start[33] = 51; - start[8800] = 32; - start[8804] = 33; - start[8805] = 34; - start[43] = 35; - start[45] = 36; - start[47] = 37; - start[37] = 38; - start[172] = 39; - start[35] = 40; - start[46] = 52; - start[8704] = 42; - start[8707] = 43; - start[8226] = 45; + start[123] = 5; + start[125] = 6; + start[59] = 7; + start[44] = 8; + start[58] = 46; + start[60] = 47; + start[62] = 48; + start[40] = 9; + start[41] = 10; + start[42] = 11; + start[96] = 12; + start[61] = 49; + start[91] = 15; + start[93] = 16; + start[124] = 50; + start[8660] = 19; + start[8658] = 21; + start[38] = 22; + start[8743] = 24; + start[8744] = 26; + start[33] = 51; + start[8800] = 32; + start[8804] = 33; + start[8805] = 34; + start[43] = 35; + start[45] = 36; + start[47] = 37; + start[37] = 38; + start[172] = 39; + start[35] = 40; + start[46] = 52; + start[8704] = 42; + start[8707] = 43; + start[8226] = 45; start[Buffer.EOF] = -1; } @@ -374,7 +374,7 @@ void objectInvariant(){ // eol handling uniform across Windows, Unix and Mac if (ch == '\r' && buffer.Peek() != '\n') ch = EOL; if (ch == EOL) { - line++; col = 0; + line++; col = 0; } else if (ch == '#' && col == 1) { int prLine = line; int prColumn = 0; @@ -552,7 +552,7 @@ void objectInvariant(){ int recKind = noSym; int recEnd = pos; t = new Token(); - t.pos = pos; t.col = col; t.line = line; + 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]); } diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 1fe9fcb7..d9f499fa 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -2059,7 +2059,7 @@ void ObjectInvariant() private readonly Dictionary subst; public NominalSubstituter(Dictionary subst) :base(){ Contract.Requires(cce.NonNullElements(subst)); - this.subst = subst; + this.subst = subst; } [ContractInvariantMethod] diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index 5f0416cc..18f8b1c5 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -708,7 +708,7 @@ void ObjectInvariant() if (b.tok == null) { Console.WriteLine(" "); } else { - // for ErrorTrace == 1 restrict the output; + // for ErrorTrace == 1 restrict the output; // do not print tokens with -17:-4 as their location because they have been // introduced in the translation and do not give any useful feedback to the user if (!(CommandLineOptions.Clo.ErrorTrace == 1 && b.tok.line == -17 && b.tok.col == -4)) { -- cgit v1.2.3