diff options
| -rw-r--r-- | Dafny/Dafny.atg | 314 | ||||
| -rw-r--r-- | Dafny/DafnyAst.ssc | 149 | ||||
| -rw-r--r-- | Dafny/DafnyMain.ssc | 3 | ||||
| -rw-r--r-- | Dafny/Makefile | 7 | ||||
| -rw-r--r-- | Dafny/Parser.ssc | 1248 | ||||
| -rw-r--r-- | Dafny/Resolver.ssc | 7 | ||||
| -rw-r--r-- | Dafny/Scanner.ssc | 902 | ||||
| -rw-r--r-- | Dafny/Translator.ssc | 115 | ||||
| -rw-r--r-- | Dafny/parser.frame | 103 | ||||
| -rw-r--r-- | Dafny/scanner.frame | 170 | ||||
| -rw-r--r-- | DafnyDriver/DafnyDriver.ssc | 6 |
11 files changed, 1528 insertions, 1496 deletions
diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg index 7affe087..ca02d3cf 100644 --- a/Dafny/Dafny.atg +++ b/Dafny/Dafny.atg @@ -12,6 +12,8 @@ using System.Collections.Generic;
using System.Numerics;
using Microsoft.Boogie;
+using System.IO;
+using System.Text;
COMPILER Dafny
@@ -64,15 +66,14 @@ private static Expression! ConvertToLocal(Expression! e) /// Note: first initialize the Scanner.
///</summary>
public static int Parse (string! filename, List<ModuleDecl!>! modules) /* throws System.IO.IOException */ {
+ string s;
if (filename == "stdin.dfy") {
- BoogiePL.Buffer.Fill(System.Console.In);
- Scanner.Init(filename);
- return Parse(modules);
+ s = Microsoft.Boogie.ParserHelper.Fill(System.Console.In, new List<string!>());
+ return Parse(s, modules);
} else {
using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {
- BoogiePL.Buffer.Fill(reader);
- Scanner.Init(filename);
- return Parse(modules);
+ s = Microsoft.Boogie.ParserHelper.Fill(reader, new List<string!>());
+ return Parse(s, filename, modules);
}
}
}
@@ -83,12 +84,17 @@ public static int Parse (string! filename, List<ModuleDecl!>! modules) /* throws /// Returns the number of parsing errors encountered.
/// Note: first initialize the Scanner.
///</summary>
-public static int Parse (List<ModuleDecl!>! modules) {
+public static int Parse (string! s, string! filename, List<ModuleDecl!>! modules) {
List<ModuleDecl!> oldModules = theModules;
theModules = modules;
- Parse();
+ byte[]! buffer = (!) UTF8Encoding.Default.GetBytes(s);
+ MemoryStream ms = new MemoryStream(buffer,false);
+ Errors errors = new Errors();
+ Scanner scanner = new Scanner(ms, errors, filename);
+ Parser parser = new Parser(scanner, errors);
+ parser.Parse();
theModules = oldModules;
- return Errors.count;
+ return parser.errors.count;
}
/*--------------------------------------------------------------------------*/
@@ -126,7 +132,7 @@ PRODUCTIONS Dafny
= (. ClassDecl! c; DatatypeDecl! dt;
- Attributes attrs; Token! id; List<string!> theImports;
+ Attributes attrs; IToken! id; List<string!> theImports;
List<MemberDecl!> membersDefaultClass = new List<MemberDecl!>();
ModuleDecl module;
@@ -174,7 +180,7 @@ Dafny .
ClassDecl<ModuleDecl! module, out ClassDecl! c>
-= (. Token! id;
+= (. IToken! id;
Attributes attrs = null;
List<TypeParameter!> typeArgs = new List<TypeParameter!>();
List<MemberDecl!> members = new List<MemberDecl!>();
@@ -189,7 +195,7 @@ ClassDecl<ModuleDecl! module, out ClassDecl! c> "}" (. c = new ClassDecl(id, id.val, module, typeArgs, members, attrs); .)
.
-ClassMemberDecl<List<MemberDecl!\>! mm>
+ClassMemberDecl<.List<MemberDecl!>! mm.>
= (. Method! m;
Function! f;
MemberModifiers mmod = new MemberModifiers();
@@ -205,7 +211,7 @@ ClassMemberDecl<List<MemberDecl!\>! mm> .
DatatypeDecl<ModuleDecl! module, out DatatypeDecl! dt>
-= (. Token! id;
+= (. IToken! id;
Attributes attrs = null;
List<TypeParameter!> typeArgs = new List<TypeParameter!>();
List<DatatypeCtor!> ctors = new List<DatatypeCtor!>();
@@ -220,9 +226,9 @@ DatatypeDecl<ModuleDecl! module, out DatatypeDecl! dt> "}" (. dt = new DatatypeDecl(id, id.val, module, typeArgs, ctors, attrs); .)
.
-DatatypeMemberDecl<List<DatatypeCtor!\>! ctors>
+DatatypeMemberDecl<.List<DatatypeCtor!>! ctors.>
= (. Attributes attrs = null;
- Token! id;
+ IToken! id;
List<TypeParameter!> typeArgs = new List<TypeParameter!>();
List<Formal!> formals = new List<Formal!>();
.)
@@ -237,13 +243,13 @@ DatatypeMemberDecl<List<DatatypeCtor!\>! ctors> ";"
.
-FieldDecl<MemberModifiers mmod, List<MemberDecl!\>! mm>
+FieldDecl<.MemberModifiers mmod, List<MemberDecl!>! mm.>
= (. Attributes attrs = null;
- Token! id; Type! ty;
+ IToken! id; Type! ty;
.)
"var"
- (. if (mmod.IsUnlimited) { SemErr(token, "fields cannot be declared 'unlimited'"); }
- if (mmod.IsStatic) { SemErr(token, "fields cannot be declared 'static'"); }
+ (. if (mmod.IsUnlimited) { SemErr(t, "fields cannot be declared 'unlimited'"); }
+ if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }
.)
{ Attribute<ref attrs> }
IdentType<out id, out ty> (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .)
@@ -252,22 +258,22 @@ FieldDecl<MemberModifiers mmod, List<MemberDecl!\>! mm> ";"
.
-GIdentType<bool allowGhost, out Token! id, out Type! ty, out bool isGhost>
+GIdentType<bool allowGhost, out IToken! id, out Type! ty, out bool isGhost>
/* isGhost always returns as false if allowGhost is false */
= (. isGhost = false; .)
- [ "ghost" (. if (allowGhost) { isGhost = true; } else { SemErr(token, "formal cannot be declared 'ghost' in this context"); } .)
+ [ "ghost" (. if (allowGhost) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); } .)
]
IdentType<out id, out ty>
.
-IdentType<out Token! id, out Type! ty>
+IdentType<out IToken! id, out Type! ty>
= Ident<out id>
":"
Type<out ty>
.
IdentTypeOptional<out BoundVar! var>
-= (. Token! id; Type! ty; Type optType = null;
+= (. IToken! id; Type! ty; Type optType = null;
.)
Ident<out id>
[ ":" Type<out ty> (. optType = ty; .)
@@ -275,7 +281,7 @@ IdentTypeOptional<out BoundVar! var> (. var = new BoundVar(id, id.val, optType == null ? new InferredTypeProxy() : optType); .)
.
-TypeIdentOptional<out Token! id, out string! identName, out Type! ty, out bool isGhost>
+TypeIdentOptional<out IToken! id, out string! identName, out Type! ty, out bool isGhost>
= (. string name = null; isGhost = false; .)
[ "ghost" (. isGhost = true; .)
]
@@ -301,8 +307,8 @@ TypeIdentOptional<out Token! id, out string! identName, out Type! ty, out bool i /*------------------------------------------------------------------------*/
-GenericParameters<List<TypeParameter!\>! typeArgs>
-= (. Token! id; .)
+GenericParameters<.List<TypeParameter!>! typeArgs.>
+= (. IToken! id; .)
"<"
Ident<out id> (. typeArgs.Add(new TypeParameter(id, id.val)); .)
{ "," Ident<out id> (. typeArgs.Add(new TypeParameter(id, id.val)); .)
@@ -313,7 +319,7 @@ GenericParameters<List<TypeParameter!\>! typeArgs> /*------------------------------------------------------------------------*/
MethodDecl<MemberModifiers mmod, out Method! m>
-= (. Token! id;
+= (. IToken! id;
Attributes attrs = null;
List<TypeParameter!>! typeArgs = new List<TypeParameter!>();
List<Formal!> ins = new List<Formal!>();
@@ -325,7 +331,7 @@ MethodDecl<MemberModifiers mmod, out Method! m> Statement! bb; BlockStmt body = null;
.)
"method"
- (. if (mmod.IsUnlimited) { SemErr(token, "methods cannot be declared 'unlimited'"); }
+ (. if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); }
.)
{ Attribute<ref attrs> }
Ident<out id>
@@ -345,8 +351,8 @@ MethodDecl<MemberModifiers mmod, out Method! m> .)
.
-MethodSpec<List<MaybeFreeExpression!\>! req, List<FrameExpression!\>! mod, List<MaybeFreeExpression!\>! ens,
- List<Expression!\>! decreases>
+MethodSpec<.List<MaybeFreeExpression!>! req, List<FrameExpression!>! mod, List<MaybeFreeExpression!>! ens,
+ List<Expression!>! decreases.>
= (. Expression! e; FrameExpression! fe; bool isFree = false;
.)
( "modifies" [ FrameExpression<out fe> (. mod.Add(fe); .)
@@ -362,8 +368,8 @@ MethodSpec<List<MaybeFreeExpression!\>! req, List<FrameExpression!\>! mod, List< )
.
-Formals<bool incoming, bool allowGhosts, List<Formal!\>! formals>
-= (. Token! id; Type! ty; bool isGhost; .)
+Formals<.bool incoming, bool allowGhosts, List<Formal!>! formals.>
+= (. IToken! id; Type! ty; bool isGhost; .)
"("
[
GIdentType<allowGhosts, out id, out ty, out isGhost> (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); parseVarScope.Push(id.val, id.val); .)
@@ -373,8 +379,8 @@ Formals<bool incoming, bool allowGhosts, List<Formal!\>! formals> ")"
.
-FormalsOptionalIds<List<Formal!\>! formals>
-= (. Token! id; Type! ty; string! name; bool isGhost; .)
+FormalsOptionalIds<.List<Formal!>! formals.>
+= (. IToken! id; Type! ty; string! name; bool isGhost; .)
"("
[
TypeIdentOptional<out id, out name, out ty, out isGhost> (. formals.Add(new Formal(id, name, ty, true, isGhost)); parseVarScope.Push(name, name); .)
@@ -387,24 +393,24 @@ FormalsOptionalIds<List<Formal!\>! formals> /*------------------------------------------------------------------------*/
Type<out Type! ty>
-= (. Token! tok; .)
+= (. IToken! tok; .)
TypeAndToken<out tok, out ty>
.
-TypeAndToken<out Token! tok, out Type! ty>
+TypeAndToken<out IToken! tok, out Type! ty>
= (. tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
List<Type!>! gt;
.)
- ( "bool" (. tok = token; .)
- | "int" (. tok = token; ty = new IntType(); .)
- | "set" (. tok = token; gt = new List<Type!>(); .)
+ ( "bool" (. tok = t; .)
+ | "int" (. tok = t; ty = new IntType(); .)
+ | "set" (. tok = t; gt = new List<Type!>(); .)
GenericInstantiation<gt> (. if (gt.Count != 1) {
SemErr("set type expects exactly one type argument");
}
ty = new SetType(gt[0]);
.)
- | "seq" (. tok = token; gt = new List<Type!>(); .)
+ | "seq" (. tok = t; gt = new List<Type!>(); .)
GenericInstantiation<gt> (. if (gt.Count != 1) {
SemErr("seq type expects exactly one type argument");
}
@@ -414,12 +420,12 @@ TypeAndToken<out Token! tok, out Type! ty> )
.
-ReferenceType<out Token! tok, out Type! ty>
+ReferenceType<out IToken! tok, out Type! ty>
= (. tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
List<Type!>! gt;
.)
- ( "object" (. tok = token; ty = new ObjectType(); .)
- | "array" (. tok = token; gt = new List<Type!>(); .)
+ ( "object" (. tok = t; ty = new ObjectType(); .)
+ | "array" (. tok = t; gt = new List<Type!>(); .)
GenericInstantiation<gt> (. if (gt.Count != 1) {
SemErr("array type expects exactly one type argument");
}
@@ -430,7 +436,7 @@ ReferenceType<out Token! tok, out Type! ty> )
.
-GenericInstantiation<List<Type!\>! gt>
+GenericInstantiation<.List<Type!>! gt.>
= (. Type! ty; .)
"<"
Type<out ty> (. gt.Add(ty); .)
@@ -443,7 +449,7 @@ GenericInstantiation<List<Type!\>! gt> FunctionDecl<MemberModifiers mmod, out Function! f>
= (. Attributes attrs = null;
- Token! id;
+ IToken! id;
List<TypeParameter!> typeArgs = new List<TypeParameter!>();
List<Formal!> formals = new List<Formal!>();
Type! returnType;
@@ -456,7 +462,7 @@ FunctionDecl<MemberModifiers mmod, out Function! f> "function"
[ "method" (. isFunctionMethod = true; .)
]
- (. if (mmod.IsGhost) { SemErr(token, "functions cannot be declared 'ghost' (they are ghost by default)"); }
+ (. if (mmod.IsGhost) { SemErr(t, "functions cannot be declared 'ghost' (they are ghost by default)"); }
.)
{ Attribute<ref attrs> }
Ident<out id>
@@ -475,7 +481,7 @@ FunctionDecl<MemberModifiers mmod, out Function! f> .)
.
-FunctionSpec<List<Expression!\>! reqs, List<FrameExpression!\>! reads, List<Expression!\>! decreases>
+FunctionSpec<.List<Expression!>! reqs, List<FrameExpression!>! reads, List<Expression!>! decreases.>
= (. Expression! e; FrameExpression! fe; .)
( "requires" Expression<out e> ";" (. reqs.Add(e); .)
| "reads" [ PossiblyWildFrameExpression<out fe> (. reads.Add(fe); .)
@@ -491,7 +497,7 @@ PossiblyWildExpression<out Expression! e> /* A decreases clause on a loop asks that no termination check be performed.
* Use of this feature is sound only with respect to partial correctness.
*/
- ( "*" (. e = new WildcardExpr(token); .)
+ ( "*" (. e = new WildcardExpr(t); .)
| Expression<out e>
)
.
@@ -504,13 +510,13 @@ PossiblyWildFrameExpression<out FrameExpression! fe> * any use of the function. Nevertheless, as an experimental feature, the
* language allows it (and it is sound).
*/
- ( "*" (. fe = new FrameExpression(new WildcardExpr(token), null); .)
+ ( "*" (. fe = new FrameExpression(new WildcardExpr(t), null); .)
| FrameExpression<out fe>
)
.
FrameExpression<out FrameExpression! fe>
-= (. Expression! e; Token! id; string fieldName = null; .)
+= (. Expression! e; IToken! id; string fieldName = null; .)
Expression<out e>
[ "`" Ident<out id> (. fieldName = id.val; .)
]
@@ -527,10 +533,10 @@ FunctionBody<out Expression! e> .
MatchExpression<out Expression! e>
-= (. Token! x; MatchCaseExpr! c;
+= (. IToken! x; MatchCaseExpr! c;
List<MatchCaseExpr!> cases = new List<MatchCaseExpr!>();
.)
- "match" (. x = token; .)
+ "match" (. x = t; .)
Expression<out e>
{ CaseExpression<out c> (. cases.Add(c); .)
}
@@ -538,11 +544,11 @@ MatchExpression<out Expression! e> .
CaseExpression<out MatchCaseExpr! c>
-= (. Token! x, id, arg;
+= (. IToken! x, id, arg;
List<BoundVar!> arguments = new List<BoundVar!>();
Expression! body;
.)
- "case" (. x = token; parseVarScope.PushMarker(); .)
+ "case" (. x = t; parseVarScope.PushMarker(); .)
Ident<out id>
[ "("
Ident<out arg> (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
@@ -559,19 +565,19 @@ CaseExpression<out MatchCaseExpr! c> /*------------------------------------------------------------------------*/
BlockStmt<out Statement! block>
-= (. Token! x;
+= (. IToken! x;
List<Statement!> body = new List<Statement!>();
Statement! s;
.)
(. parseVarScope.PushMarker(); .)
- "{" (. x = token; .)
+ "{" (. x = t; .)
{ Stmt<body>
}
"}" (. block = new BlockStmt(x, body); .)
(. parseVarScope.PopMarker(); .)
.
-Stmt<List<Statement!\>! ss>
+Stmt<.List<Statement!>! ss.>
= (. Statement! s; .)
/* By first reading a sequence of block statements, we avoid problems in the generated parser, despite
the ambiguity in the grammar. See Note in ConstAtomExpression production.
@@ -584,7 +590,7 @@ Stmt<List<Statement!\>! ss> .
OneStmt<out Statement! s>
-= (. Token! x; Token! id; string label = null;
+= (. IToken! x; IToken! id; string label = null;
s = dummyStmt; /* to please the compiler */
.)
/* This list does not contain BlockStmt, see comment above in Stmt production. */
@@ -599,25 +605,25 @@ OneStmt<out Statement! s> | WhileStmt<out s>
| MatchStmt<out s>
| ForeachStmt<out s>
- | "label" (. x = token; .)
+ | "label" (. x = t; .)
Ident<out id> ":" (. s = new LabelStmt(x, id.val); .)
- | "break" (. x = token; .)
+ | "break" (. x = t; .)
[ Ident<out id> (. label = id.val; .)
] ";" (. s = new BreakStmt(x, label); .)
- | "return" (. x = token; .)
+ | "return" (. x = t; .)
";" (. s = new ReturnStmt(x); .)
)
.
AssignStmt<out Statement! s>
-= (. Token! x;
+= (. IToken! x;
Expression! lhs;
Expression rhs;
Type ty;
s = dummyStmt;
.)
LhsExpr<out lhs>
- ":=" (. x = token; .)
+ ":=" (. x = t; .)
AssignRhs<out rhs, out ty> (. if (ty == null) {
assert rhs != null;
s = new AssignStmt(x, lhs, rhs);
@@ -632,7 +638,7 @@ AssignStmt<out Statement! s> AssignRhs<out Expression e, out Type ty>
/* ensures e != null || ty != null; */
-= (. Token! x; Expression! ee; Type! tt;
+= (. IToken! x; Expression! ee; Type! tt;
e = null; ty = null;
.)
( "new" TypeAndToken<out x, out tt> (. ty = tt; .)
@@ -643,8 +649,8 @@ AssignRhs<out Expression e, out Type ty> .
HavocStmt<out Statement! s>
-= (. Token! x; Expression! lhs; .)
- "havoc" (. x = token; .)
+= (. IToken! x; Expression! lhs; .)
+ "havoc" (. x = t; .)
LhsExpr<out lhs> ";" (. s = new AssignStmt(x, lhs); .)
.
@@ -652,7 +658,7 @@ LhsExpr<out Expression! e> = SelectExpression<out e>
.
-VarDeclStmts<List<Statement!\>! ss>
+VarDeclStmts<.List<Statement!>! ss.>
= (. VarDecl! d; bool isGhost = false; .)
[ "ghost" (. isGhost = true; .)
]
@@ -664,7 +670,7 @@ VarDeclStmts<List<Statement!\>! ss> .
IdentTypeRhs<out VarDecl! d, bool isGhost>
-= (. Token! id; Type! ty; Expression! e;
+= (. IToken! id; Type! ty; Expression! e;
Expression rhs = null; Type newType = null;
Type optionalType = null; DeterminedAssignmentRhs optionalRhs = null;
.)
@@ -690,13 +696,13 @@ IdentTypeRhs<out VarDecl! d, bool isGhost> .
IfStmt<out Statement! ifStmt>
-= (. Token! x;
+= (. IToken! x;
Expression guard;
Statement! thn;
Statement! s;
Statement els = null;
.)
- "if" (. x = token; .)
+ "if" (. x = t; .)
Guard<out guard>
BlockStmt<out thn>
[ "else"
@@ -708,14 +714,14 @@ IfStmt<out Statement! ifStmt> .
WhileStmt<out Statement! stmt>
-= (. Token! x;
+= (. IToken! x;
Expression guard;
bool isFree; Expression! e;
List<MaybeFreeExpression!> invariants = new List<MaybeFreeExpression!>();
List<Expression!> decreases = new List<Expression!>();
Statement! body;
.)
- "while" (. x = token; .)
+ "while" (. x = t; .)
Guard<out guard> (. assume guard == null || Owner.None(guard); .)
{ (. isFree = false; .)
[ "free" (. isFree = true; .)
@@ -744,7 +750,7 @@ Guard<out Expression e> /* null represents demonic-choice */ MatchStmt<out Statement! s>
= (. Token x; Expression! e; MatchCaseStmt! c;
List<MatchCaseStmt!> cases = new List<MatchCaseStmt!>(); .)
- "match" (. x = token; .)
+ "match" (. x = t; .)
Expression<out e>
"{"
{ CaseStatement<out c> (. cases.Add(c); .)
@@ -754,11 +760,11 @@ MatchStmt<out Statement! s> .
CaseStatement<out MatchCaseStmt! c>
-= (. Token! x, id, arg;
+= (. IToken! x, id, arg;
List<BoundVar!> arguments = new List<BoundVar!>();
List<Statement!> body = new List<Statement!>();
.)
- "case" (. x = token; parseVarScope.PushMarker(); .)
+ "case" (. x = t; parseVarScope.PushMarker(); .)
Ident<out id>
[ "("
Ident<out arg> (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
@@ -776,12 +782,12 @@ CaseStatement<out MatchCaseStmt! c> .
CallStmt<out Statement! s>
-= (. Token! x, id;
+= (. IToken! x, id;
Expression! e;
List<IdentifierExpr!> lhs = new List<IdentifierExpr!>();
List<AutoVarDecl!> newVars = new List<AutoVarDecl!>();
.)
- "call" (. x = token; .)
+ "call" (. x = t; .)
CallStmtSubExpr<out e>
[ "," /* call a,b,c,... := ... */
@@ -829,7 +835,7 @@ CallStmt<out Statement! s> /*------------------------------------------------------------------------*/
ForeachStmt<out Statement! s>
-= (. Token! x, boundVar;
+= (. IToken! x, boundVar;
Type! ty;
Expression! collection;
Expression! range;
@@ -837,7 +843,7 @@ ForeachStmt<out Statement! s> AssignStmt bodyAssign = null;
.)
(. parseVarScope.PushMarker(); .)
- "foreach" (. x = token;
+ "foreach" (. x = t;
range = new LiteralExpr(x, true);
ty = new InferredTypeProxy();
.)
@@ -865,28 +871,28 @@ ForeachStmt<out Statement! s> .
AssertStmt<out Statement! s>
-= (. Token! x; Expression! e; .)
- "assert" (. x = token; .)
+= (. IToken! x; Expression! e; .)
+ "assert" (. x = t; .)
Expression<out e> ";" (. s = new AssertStmt(x, e); .)
.
AssumeStmt<out Statement! s>
-= (. Token! x; Expression! e; .)
- "assume" (. x = token; .)
+= (. IToken! x; Expression! e; .)
+ "assume" (. x = t; .)
Expression<out e> ";" (. s = new AssumeStmt(x, e); .)
.
UseStmt<out Statement! s>
-= (. Token! x; Expression! e; .)
- "use" (. x = token; .)
+= (. IToken! x; Expression! e; .)
+ "use" (. x = t; .)
Expression<out e> ";" (. s = new UseStmt(x, e); .)
.
PrintStmt<out Statement! s>
-= (. Token! x; Attributes.Argument! arg;
+= (. IToken! x; Attributes.Argument! arg;
List<Attributes.Argument!> args = new List<Attributes.Argument!>();
.)
- "print" (. x = token; .)
+ "print" (. x = t; .)
AttributeArg<out arg> (. args.Add(arg); .)
{ "," AttributeArg<out arg> (. args.Add(arg); .)
}
@@ -895,10 +901,10 @@ PrintStmt<out Statement! s> /*------------------------------------------------------------------------*/
Expression<out Expression! e>
-= (. Token! x; Expression! e0; Expression! e1 = dummyExpr;
+= (. IToken! x; Expression! e0; Expression! e1 = dummyExpr;
e = dummyExpr;
.)
- ( "if" (. x = token; .)
+ ( "if" (. x = t; .)
Expression<out e>
"then" Expression<out e0>
"else" Expression<out e1> (. e = new ITEExpr(x, e, e0, e1); .)
@@ -908,9 +914,9 @@ Expression<out Expression! e> /*------------------------------------------------------------------------*/
EquivExpression<out Expression! e0>
-= (. Token! x; Expression! e1; .)
+= (. IToken! x; Expression! e1; .)
ImpliesExpression<out e0>
- { EquivOp (. x = token; .)
+ { EquivOp (. x = t; .)
ImpliesExpression<out e1> (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Iff, e0, e1); .)
}
.
@@ -919,9 +925,9 @@ EquivOp = "<==>" | '\u21d4'. /*------------------------------------------------------------------------*/
ImpliesExpression<out Expression! e0>
-= (. Token! x; Expression! e1; .)
+= (. IToken! x; Expression! e1; .)
LogicalExpression<out e0>
- [ ImpliesOp (. x = token; .)
+ [ ImpliesOp (. x = t; .)
ImpliesExpression<out e1> (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Imp, e0, e1); .)
]
.
@@ -930,16 +936,16 @@ ImpliesOp = "==>" | '\u21d2'. /*------------------------------------------------------------------------*/
LogicalExpression<out Expression! e0>
-= (. Token! x; Expression! e1; .)
+= (. IToken! x; Expression! e1; .)
RelationalExpression<out e0>
- [ AndOp (. x = token; .)
+ [ AndOp (. x = t; .)
RelationalExpression<out e1> (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); .)
- { AndOp (. x = token; .)
+ { AndOp (. x = t; .)
RelationalExpression<out e1> (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); .)
}
- | OrOp (. x = token; .)
+ | OrOp (. x = t; .)
RelationalExpression<out e1> (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); .)
- { OrOp (. x = token; .)
+ { OrOp (. x = t; .)
RelationalExpression<out e1> (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); .)
}
]
@@ -950,69 +956,69 @@ OrOp = "||" | '\u2228'. /*------------------------------------------------------------------------*/
RelationalExpression<out Expression! e0>
-= (. Token! x; Expression! e1; BinaryExpr.Opcode op; .)
+= (. IToken! x; Expression! e1; BinaryExpr.Opcode op; .)
Term<out e0>
[ RelOp<out x, out op>
Term<out e1> (. e0 = new BinaryExpr(x, op, e0, e1); .)
]
.
-RelOp<out Token! x, out BinaryExpr.Opcode op>
+RelOp<out IToken! x, out BinaryExpr.Opcode op>
= (. x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/; .)
- ( "==" (. x = token; op = BinaryExpr.Opcode.Eq; .)
- | "<" (. x = token; op = BinaryExpr.Opcode.Lt; .)
- | ">" (. x = token; op = BinaryExpr.Opcode.Gt; .)
- | "<=" (. x = token; op = BinaryExpr.Opcode.Le; .)
- | ">=" (. x = token; op = BinaryExpr.Opcode.Ge; .)
- | "!=" (. x = token; op = BinaryExpr.Opcode.Neq; .)
- | "!!" (. x = token; op = BinaryExpr.Opcode.Disjoint; .)
- | "in" (. x = token; op = BinaryExpr.Opcode.In; .)
- | "!in" (. x = token; op = BinaryExpr.Opcode.NotIn; .)
- | '\u2260' (. x = token; op = BinaryExpr.Opcode.Neq; .)
- | '\u2264' (. x = token; op = BinaryExpr.Opcode.Le; .)
- | '\u2265' (. x = token; op = BinaryExpr.Opcode.Ge; .)
+ ( "==" (. x = t; op = BinaryExpr.Opcode.Eq; .)
+ | "<" (. x = t; op = BinaryExpr.Opcode.Lt; .)
+ | ">" (. x = t; op = BinaryExpr.Opcode.Gt; .)
+ | "<=" (. x = t; op = BinaryExpr.Opcode.Le; .)
+ | ">=" (. x = t; op = BinaryExpr.Opcode.Ge; .)
+ | "!=" (. 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; .)
+ | '\u2260' (. x = t; op = BinaryExpr.Opcode.Neq; .)
+ | '\u2264' (. x = t; op = BinaryExpr.Opcode.Le; .)
+ | '\u2265' (. x = t; op = BinaryExpr.Opcode.Ge; .)
)
.
/*------------------------------------------------------------------------*/
Term<out Expression! e0>
-= (. Token! x; Expression! e1; BinaryExpr.Opcode op; .)
+= (. IToken! x; Expression! e1; BinaryExpr.Opcode op; .)
Factor<out e0>
{ AddOp<out x, out op>
Factor<out e1> (. e0 = new BinaryExpr(x, op, e0, e1); .)
}
.
-AddOp<out Token! x, out BinaryExpr.Opcode op>
+AddOp<out IToken! x, out BinaryExpr.Opcode op>
= (. x = Token.NoToken; op=BinaryExpr.Opcode.Add/*(dummy)*/; .)
- ( "+" (. x = token; op = BinaryExpr.Opcode.Add; .)
- | "-" (. x = token; op = BinaryExpr.Opcode.Sub; .)
+ ( "+" (. x = t; op = BinaryExpr.Opcode.Add; .)
+ | "-" (. x = t; op = BinaryExpr.Opcode.Sub; .)
)
.
/*------------------------------------------------------------------------*/
Factor<out Expression! e0>
-= (. Token! x; Expression! e1; BinaryExpr.Opcode op; .)
+= (. IToken! x; Expression! e1; BinaryExpr.Opcode op; .)
UnaryExpression<out e0>
{ MulOp<out x, out op>
UnaryExpression<out e1> (. e0 = new BinaryExpr(x, op, e0, e1); .)
}
.
-MulOp<out Token! x, out BinaryExpr.Opcode op>
+MulOp<out IToken! x, out BinaryExpr.Opcode op>
= (. x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/; .)
- ( "*" (. x = token; op = BinaryExpr.Opcode.Mul; .)
- | "/" (. x = token; op = BinaryExpr.Opcode.Div; .)
- | "%" (. x = token; op = BinaryExpr.Opcode.Mod; .)
+ ( "*" (. x = t; op = BinaryExpr.Opcode.Mul; .)
+ | "/" (. x = t; op = BinaryExpr.Opcode.Div; .)
+ | "%" (. x = t; op = BinaryExpr.Opcode.Mod; .)
)
.
/*------------------------------------------------------------------------*/
UnaryExpression<out Expression! e>
-= (. Token! x; e = dummyExpr; .)
- ( "-" (. x = token; .)
+= (. IToken! x; e = dummyExpr; .)
+ ( "-" (. x = t; .)
UnaryExpression<out e> (. e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e); .)
- | NegOp (. x = token; .)
+ | NegOp (. x = t; .)
UnaryExpression<out e> (. e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); .)
| SelectExpression<out e>
| ConstAtomExpression<out e>
@@ -1022,29 +1028,29 @@ UnaryExpression<out Expression! e> NegOp = "!" | '\u00ac'.
ConstAtomExpression<out Expression! e>
-= (. Token! x, dtName, id; BigInteger n; List<Expression!>! elements;
+= (. IToken! x, dtName, id; BigInteger n; List<Expression!>! elements;
e = dummyExpr;
.)
- ( "false" (. e = new LiteralExpr(token, false); .)
- | "true" (. e = new LiteralExpr(token, true); .)
- | "null" (. e = new LiteralExpr(token); .)
- | Nat<out n> (. e = new LiteralExpr(token, n); .)
- | "#" (. x = token; .)
+ ( "false" (. e = new LiteralExpr(t, false); .)
+ | "true" (. e = new LiteralExpr(t, true); .)
+ | "null" (. e = new LiteralExpr(t); .)
+ | Nat<out n> (. e = new LiteralExpr(t, n); .)
+ | "#" (. x = t; .)
Ident<out dtName>
"."
Ident<out id> (. elements = new List<Expression!>(); .)
[ "("
[ Expressions<elements> ]
- ")" ] (. e = new DatatypeValue(token, dtName.val, id.val, elements); .)
- | "fresh" (. x = token; .)
+ ")" ] (. e = new DatatypeValue(t, dtName.val, id.val, elements); .)
+ | "fresh" (. x = t; .)
"(" Expression<out e> ")" (. e = new FreshExpr(x, e); .)
- | "|" (. x = token; .)
+ | "|" (. x = t; .)
Expression<out e> (. e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e); .)
"|"
- | "{" (. x = token; elements = new List<Expression!>(); .)
+ | "{" (. x = t; elements = new List<Expression!>(); .)
[ Expressions<elements> ] (. e = new SetDisplayExpr(x, elements); .)
"}"
- | "[" (. x = token; elements = new List<Expression!>(); .)
+ | "[" (. x = t; elements = new List<Expression!>(); .)
[ Expressions<elements> ] (. e = new SeqDisplayExpr(x, elements); .)
"]"
)
@@ -1067,7 +1073,7 @@ CallStmtSubExpr<out Expression! e> .
SelectExpression<out Expression! e>
-= (. Token! id; e = dummyExpr; .)
+= (. IToken! id; e = dummyExpr; .)
( IdentOrFuncExpression<out e>
| ObjectExpression<out e>
)
@@ -1075,7 +1081,7 @@ SelectExpression<out Expression! e> .
IdentOrFuncExpression<out Expression! e>
-= (. Token! id; e = dummyExpr; List<Expression!>! args; .)
+= (. IToken! id; e = dummyExpr; List<Expression!>! args; .)
Ident<out id>
[ "(" (. args = new List<Expression!>(); .)
[ Expressions<args> ]
@@ -1091,7 +1097,7 @@ IdentOrFuncExpression<out Expression! e> .
SelectOrCallSuffix<ref Expression! e>
-= (. Token! id, x; List<Expression!>! args;
+= (. IToken! id, x; List<Expression!>! args;
Expression e0 = null; Expression e1 = null; Expression! ee; bool anyDots = false;
bool func = false;
.)
@@ -1102,7 +1108,7 @@ SelectOrCallSuffix<ref Expression! e> ")" (. e = new FunctionCallExpr(id, id.val, e, args); .)
] (. if (!func) { e = new FieldSelectExpr(id, e, id.val); } .)
- | "[" (. x = token; .)
+ | "[" (. x = t; .)
( Expression<out ee> (. e0 = ee; .)
[ ".." (. anyDots = true; .)
[ Expression<out ee> (. e1 = ee; .)
@@ -1136,9 +1142,9 @@ SelectOrCallSuffix<ref Expression! e> parsed here. The expression returned is never an lvalue.
*/
ObjectExpression<out Expression! e>
-= (. Token! x; e = dummyExpr; .)
- ( "this" (. e = new ThisExpr(token); .)
- | "old" (. x = token; .)
+= (. IToken! x; e = dummyExpr; .)
+ ( "this" (. e = new ThisExpr(t); .)
+ | "old" (. x = t; .)
"("
Expression<out e>
")" (. e = new OldExpr(x, e); .)
@@ -1152,17 +1158,17 @@ ObjectExpression<out Expression! e> /*------------------------------------------------------------------------*/
QuantifierGuts<out Expression! q>
-= (. Token! x = Token.NoToken;
+= (. IToken! x = Token.NoToken;
bool univ = false;
BoundVar! bv;
List<BoundVar!> bvars = new List<BoundVar!>();
- Token! tok; Expr! e; ExprSeq! es;
+ IToken! tok; Expr! e; ExprSeq! es;
Attributes attrs = null;
Triggers trigs = null;
Expression! body;
.)
- ( Forall (. x = token; univ = true; .)
- | Exists (. x = token; .)
+ ( Forall (. x = t; univ = true; .)
+ | Exists (. x = t; .)
)
(. parseVarScope.PushMarker(); .)
IdentTypeOptional<out bv> (. bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name); .)
@@ -1185,7 +1191,7 @@ Forall = "forall" | '\u2200'. Exists = "exists" | '\u2203'.
QSep = "::" | '\u2022'.
-Expressions<List<Expression!\>! args>
+Expressions<.List<Expression!>! args.>
= (. Expression! e; .)
Expression<out e> (. args.Add(e); .)
{ "," Expression<out e> (. args.Add(e); .)
@@ -1205,7 +1211,7 @@ AttributeBody<ref Attributes attrs> List<Attributes.Argument!> aArgs = new List<Attributes.Argument!>();
Attributes.Argument! aArg;
.)
- ":" ident (. aName = token.val; .)
+ ":" ident (. aName = t.val; .)
[ AttributeArg<out aArg> (. aArgs.Add(aArg); .)
{ "," AttributeArg<out aArg> (. aArgs.Add(aArg); .)
}
@@ -1214,7 +1220,7 @@ AttributeBody<ref Attributes attrs> AttributeArg<out Attributes.Argument! arg>
= (. Expression! e; arg = dummyAttrArg; .)
- ( string (. arg = new Attributes.Argument(token.val.Substring(1, token.val.Length-2)); .)
+ ( string (. arg = new Attributes.Argument(t.val.Substring(1, t.val.Length-2)); .)
| Expression<out e> (. arg = new Attributes.Argument(e); .)
)
.
@@ -1232,23 +1238,23 @@ AttributeOrTrigger<ref Attributes attrs, ref Triggers trigs> /*------------------------------------------------------------------------*/
-Idents<List<string!\>! ids>
-= (. Token! id; .)
+Idents<.List<string!>! ids.>
+= (. IToken! id; .)
Ident<out id> (. ids.Add(id.val); .)
{ "," Ident<out id> (. ids.Add(id.val); .)
}
.
-Ident<out Token! x>
+Ident<out IToken! x>
=
- ident (. x = token; .)
+ ident (. x = t; .)
.
Nat<out BigInteger n>
=
digits
(. try {
- n = BigInteger.Parse(token.val);
+ n = BigInteger.Parse(t.val);
} catch (System.FormatException) {
SemErr("incorrectly formatted number");
n = BigInteger.Zero;
diff --git a/Dafny/DafnyAst.ssc b/Dafny/DafnyAst.ssc index a8a93067..1d9dfd1c 100644 --- a/Dafny/DafnyAst.ssc +++ b/Dafny/DafnyAst.ssc @@ -7,6 +7,7 @@ using System; using System.Collections.Generic;
using Microsoft.Contracts;
using System.Numerics;
+using Microsoft.Boogie;
namespace Microsoft.Dafny
{
@@ -148,14 +149,14 @@ namespace Microsoft.Dafny }
public class UserDefinedType : Type {
- public readonly Token! tok;
+ public readonly IToken! tok;
public readonly string! Name;
[Rep] public readonly List<Type!>! TypeArgs;
public TopLevelDecl ResolvedClass; // filled in by resolution, if Name denotes a class/datatype and TypeArgs match the type parameters of that class/datatype
public TypeParameter ResolvedParam; // filled in by resolution, if Name denotes an enclosing type parameter and TypeArgs is the empty list
- public static UserDefinedType! ArrayType(Token! tok, Type! arg) {
+ public static UserDefinedType! ArrayType(IToken! tok, Type! arg) {
List<Type!> typeArgs = new List<Type!>();
typeArgs.Add(arg);
UserDefinedType udt = new UserDefinedType(tok, "array", typeArgs);
@@ -171,7 +172,7 @@ namespace Microsoft.Dafny }
- public UserDefinedType(Token! tok, string! name, [Captured] List<Type!>! typeArgs) {
+ public UserDefinedType(IToken! tok, string! name, [Captured] List<Type!>! typeArgs) {
this.tok = tok;
this.Name = name;
this.TypeArgs = typeArgs;
@@ -180,7 +181,7 @@ namespace Microsoft.Dafny /// <summary>
/// This constructor constructs a resolved class type
/// </summary>
- public UserDefinedType(Token! tok, string! name, TopLevelDecl! cd, [Captured] List<Type!>! typeArgs) {
+ public UserDefinedType(IToken! tok, string! name, TopLevelDecl! cd, [Captured] List<Type!>! typeArgs) {
this.tok = tok;
this.Name = name;
this.TypeArgs = typeArgs;
@@ -190,7 +191,7 @@ namespace Microsoft.Dafny /// <summary>
/// This constructor constructs a resolved type parameter
/// </summary>
- public UserDefinedType(Token! tok, string! name, TypeParameter! tp) {
+ public UserDefinedType(IToken! tok, string! name, TypeParameter! tp) {
this.tok = tok;
this.Name = name;
this.TypeArgs = new List<Type!>();
@@ -350,11 +351,11 @@ namespace Microsoft.Dafny // ------------------------------------------------------------------------------------------------------
public abstract class Declaration {
- public Token! tok;
+ public IToken! tok;
public readonly string! Name;
public readonly Attributes Attributes;
- public Declaration(Token! tok, string! name, Attributes attributes) {
+ public Declaration(IToken! tok, string! name, Attributes attributes) {
this.tok = tok;
this.Name = name;
this.Attributes = attributes;
@@ -386,7 +387,7 @@ namespace Microsoft.Dafny parent = value;
}
}
- public TypeParameter(Token! tok, string! name) {
+ public TypeParameter(IToken! tok, string! name) {
base(tok, name, null);
}
}
@@ -396,7 +397,7 @@ namespace Microsoft.Dafny public readonly List<TopLevelDecl!>! TopLevelDecls = new List<TopLevelDecl!>(); // filled in by the parser; readonly after that
public readonly Graph<MemberDecl!>! CallGraph = new Graph<MemberDecl!>(); // filled in during resolution
public int Height; // height in the topological sorting of modules; filled in during resolution
- public ModuleDecl(Token! tok, string! name, [Captured] List<string!>! imports, Attributes attributes) {
+ public ModuleDecl(IToken! tok, string! name, [Captured] List<string!>! imports, Attributes attributes) {
Imports = imports;
base(tok, name, attributes);
}
@@ -418,7 +419,7 @@ namespace Microsoft.Dafny public readonly ModuleDecl! Module;
public readonly List<TypeParameter!>! TypeArgs;
- public TopLevelDecl(Token! tok, string! name, ModuleDecl! module, List<TypeParameter!>! typeArgs, Attributes attributes) {
+ public TopLevelDecl(IToken! tok, string! name, ModuleDecl! module, List<TypeParameter!>! typeArgs, Attributes attributes) {
Module = module;
TypeArgs = typeArgs;
base(tok, name, attributes);
@@ -428,7 +429,7 @@ namespace Microsoft.Dafny public class ClassDecl : TopLevelDecl {
public readonly List<MemberDecl!>! Members;
- public ClassDecl(Token! tok, string! name, ModuleDecl! module, List<TypeParameter!>! typeArgs, [Captured] List<MemberDecl!>! members, Attributes attributes) {
+ public ClassDecl(IToken! tok, string! name, ModuleDecl! module, List<TypeParameter!>! typeArgs, [Captured] List<MemberDecl!>! members, Attributes attributes) {
Members = members;
base(tok, name, module, typeArgs, attributes);
}
@@ -450,7 +451,7 @@ namespace Microsoft.Dafny public readonly List<DatatypeCtor!>! Ctors;
public DatatypeCtor DefaultCtor; // set during resolution
- public DatatypeDecl(Token! tok, string! name, ModuleDecl! module, List<TypeParameter!>! typeArgs, [Captured] List<DatatypeCtor!>! ctors, Attributes attributes) {
+ public DatatypeDecl(IToken! tok, string! name, ModuleDecl! module, List<TypeParameter!>! typeArgs, [Captured] List<DatatypeCtor!>! ctors, Attributes attributes) {
Ctors = ctors;
base(tok, name, module, typeArgs, attributes);
}
@@ -462,7 +463,7 @@ namespace Microsoft.Dafny // Todo: One could imagine having a precondition on datatype constructors
public DatatypeDecl EnclosingDatatype; // filled in during resolution
- public DatatypeCtor(Token! tok, string! name, [Captured] List<TypeParameter!>! typeArgs, [Captured] List<Formal!>! formals,
+ public DatatypeCtor(IToken! tok, string! name, [Captured] List<TypeParameter!>! typeArgs, [Captured] List<Formal!>! formals,
Attributes attributes) {
this.TypeArgs = typeArgs;
this.Formals = formals;
@@ -481,7 +482,7 @@ namespace Microsoft.Dafny public abstract class MemberDecl : Declaration {
public ClassDecl EnclosingClass; // filled in during resolution
- public MemberDecl(Token! tok, string! name, Attributes attributes) {
+ public MemberDecl(IToken! tok, string! name, Attributes attributes) {
base(tok, name, attributes);
}
/// <summary>
@@ -500,7 +501,7 @@ namespace Microsoft.Dafny public readonly bool IsGhost;
public readonly Type! Type;
- public Field(Token! tok, string! name, bool isGhost, Type! type, Attributes attributes) {
+ public Field(IToken! tok, string! name, bool isGhost, Type! type, Attributes attributes) {
IsGhost = isGhost;
Type = type;
base(tok, name, attributes);
@@ -516,7 +517,7 @@ namespace Microsoft.Dafny }
public abstract class NonglobalVariable : IVariable {
- public readonly Token! tok;
+ public readonly IToken! tok;
readonly string! name;
public string! Name { get { return name; } }
readonly int varId = varIdCount++;
@@ -544,7 +545,7 @@ namespace Microsoft.Dafny set { isGhost = value; }
}
- public NonglobalVariable(Token! tok, string! name, Type! type, bool isGhost) {
+ public NonglobalVariable(IToken! tok, string! name, Type! type, bool isGhost) {
this.tok = tok;
this.name = name;
this.type = type;
@@ -558,7 +559,7 @@ namespace Microsoft.Dafny public readonly bool InParam; // true to in-parameter, false for out-parameter
public override bool IsMutable { get { return !InParam; } }
- public Formal(Token! tok, string! name, Type! type, bool inParam, bool isGhost) {
+ public Formal(IToken! tok, string! name, Type! type, bool inParam, bool isGhost) {
InParam = inParam;
base(tok, name, type, isGhost);
}
@@ -567,7 +568,7 @@ namespace Microsoft.Dafny public class BoundVar : NonglobalVariable {
public override bool IsMutable { get { return false; } }
- public BoundVar(Token! tok, string! name, Type! type) {
+ public BoundVar(IToken! tok, string! name, Type! type) {
base(tok, name, type, false);
}
}
@@ -585,7 +586,7 @@ namespace Microsoft.Dafny public readonly List<Expression!>! Decreases;
public readonly Expression Body; // an extended expression
- public Function(Token! tok, string! name, bool isStatic, bool isGhost, bool isUnlimited, [Captured] List<TypeParameter!>! typeArgs, [Captured] List<Formal!>! formals, Type! resultType,
+ public Function(IToken! tok, string! name, bool isStatic, bool isGhost, bool isUnlimited, [Captured] List<TypeParameter!>! typeArgs, [Captured] List<Formal!>! formals, Type! resultType,
List<Expression!>! req, List<FrameExpression!>! reads, List<Expression!>! decreases, Expression body, Attributes attributes) {
this.IsStatic = isStatic;
this.IsGhost = isGhost;
@@ -613,7 +614,7 @@ namespace Microsoft.Dafny public readonly List<Expression!>! Decreases;
public readonly BlockStmt Body;
- public Method(Token! tok, string! name,
+ public Method(IToken! tok, string! name,
bool isStatic, bool isGhost,
[Captured] List<TypeParameter!>! typeArgs,
[Captured] List<Formal!>! ins, [Captured] List<Formal!>! outs,
@@ -638,9 +639,9 @@ namespace Microsoft.Dafny // ------------------------------------------------------------------------------------------------------
public abstract class Statement {
- public readonly Token! Tok;
+ public readonly IToken! Tok;
public bool IsGhost; // filled in by resolution
- public Statement(Token! tok) {
+ public Statement(IToken! tok) {
this.Tok = tok;
}
}
@@ -648,7 +649,7 @@ namespace Microsoft.Dafny public abstract class PredicateStmt : Statement {
[Peer] public readonly Expression! Expr;
[Captured]
- public PredicateStmt(Token! tok, Expression! expr)
+ public PredicateStmt(IToken! tok, Expression! expr)
ensures Owner.Same(this, expr);
{
base(tok);
@@ -659,7 +660,7 @@ namespace Microsoft.Dafny public class AssertStmt : PredicateStmt {
[Captured]
- public AssertStmt(Token! tok, Expression! expr)
+ public AssertStmt(IToken! tok, Expression! expr)
ensures Owner.Same(this, expr);
{
base(tok, expr);
@@ -668,7 +669,7 @@ namespace Microsoft.Dafny public class AssumeStmt : PredicateStmt {
[Captured]
- public AssumeStmt(Token! tok, Expression! expr)
+ public AssumeStmt(IToken! tok, Expression! expr)
ensures Owner.Same(this, expr);
{
base(tok, expr);
@@ -677,7 +678,7 @@ namespace Microsoft.Dafny public class UseStmt : PredicateStmt {
[Captured]
- public UseStmt(Token! tok, Expression! expr)
+ public UseStmt(IToken! tok, Expression! expr)
ensures Owner.Same(this, expr);
{
base(tok, expr);
@@ -715,7 +716,7 @@ namespace Microsoft.Dafny public class PrintStmt : Statement {
public readonly List<Attributes.Argument!>! Args;
- public PrintStmt(Token! tok, List<Attributes.Argument!>! args)
+ public PrintStmt(IToken! tok, List<Attributes.Argument!>! args)
{
base(tok);
Args = args;
@@ -724,7 +725,7 @@ namespace Microsoft.Dafny public class LabelStmt : Statement {
public readonly string! Label;
- public LabelStmt(Token! tok, string! label) {
+ public LabelStmt(IToken! tok, string! label) {
this.Label = label;
base(tok);
}
@@ -734,14 +735,14 @@ namespace Microsoft.Dafny public readonly string TargetLabel;
public Statement TargetStmt; // filled in during resolution
- public BreakStmt(Token! tok, string targetLabel) {
+ public BreakStmt(IToken! tok, string targetLabel) {
this.TargetLabel = targetLabel;
base(tok);
}
}
public class ReturnStmt : Statement {
- public ReturnStmt(Token! tok) {
+ public ReturnStmt(IToken! tok) {
base(tok);
}
}
@@ -779,22 +780,22 @@ namespace Microsoft.Dafny public class AssignStmt : Statement {
public readonly Expression! Lhs;
public readonly AssignmentRhs! Rhs;
- public AssignStmt(Token! tok, Expression! lhs, Expression! rhs) { // ordinary assignment statement
+ public AssignStmt(IToken! tok, Expression! lhs, Expression! rhs) { // ordinary assignment statement
this.Lhs = lhs;
this.Rhs = new ExprRhs(rhs);
base(tok);
}
- public AssignStmt(Token! tok, Expression! lhs, Type! type) { // alloc statement
+ public AssignStmt(IToken! tok, Expression! lhs, Type! type) { // alloc statement
this.Lhs = lhs;
this.Rhs = new TypeRhs(type);
base(tok);
}
- public AssignStmt(Token! tok, Expression! lhs, Type! type, Expression! arraySize) { // array alloc statement
+ public AssignStmt(IToken! tok, Expression! lhs, Type! type, Expression! arraySize) { // array alloc statement
this.Lhs = lhs;
this.Rhs = new TypeRhs(type, arraySize);
base(tok);
}
- public AssignStmt(Token! tok, Expression! lhs) { // havoc
+ public AssignStmt(IToken! tok, Expression! lhs) { // havoc
this.Lhs = lhs;
this.Rhs = new HavocRhs();
base(tok);
@@ -830,7 +831,7 @@ namespace Microsoft.Dafny public readonly DeterminedAssignmentRhs Rhs;
invariant OptionalType != null || Rhs != null;
- public VarDecl(Token! tok, string! name, Type type, bool isGhost, DeterminedAssignmentRhs rhs)
+ public VarDecl(IToken! tok, string! name, Type type, bool isGhost, DeterminedAssignmentRhs rhs)
requires type != null || rhs != null;
{
this.name = name;
@@ -843,7 +844,7 @@ namespace Microsoft.Dafny public class AutoVarDecl : VarDecl {
public readonly int Index;
- public AutoVarDecl(Token! tok, string! name, Type! type, int index)
+ public AutoVarDecl(IToken! tok, string! name, Type! type, int index)
{
Index = index;
base(tok, name, type, false, null);
@@ -864,7 +865,7 @@ namespace Microsoft.Dafny public readonly List<Expression!>! Args;
public Method Method; // filled in by resolution
- public CallStmt(Token! tok, List<AutoVarDecl!>! newVars, List<IdentifierExpr!>! lhs, Expression! receiver, string! methodName, List<Expression!>! args) {
+ public CallStmt(IToken! tok, List<AutoVarDecl!>! newVars, List<IdentifierExpr!>! lhs, Expression! receiver, string! methodName, List<Expression!>! args) {
this.NewVars = newVars;
this.Lhs = lhs;
this.Receiver = receiver;
@@ -876,7 +877,7 @@ namespace Microsoft.Dafny public class BlockStmt : Statement {
public readonly List<Statement!>! Body;
- public BlockStmt(Token! tok, [Captured] List<Statement!>! body) {
+ public BlockStmt(IToken! tok, [Captured] List<Statement!>! body) {
this.Body = body;
base(tok);
}
@@ -888,7 +889,7 @@ namespace Microsoft.Dafny public readonly Statement Els;
invariant Els == null || Els is BlockStmt || Els is IfStmt;
- public IfStmt(Token! tok, Expression guard, Statement! thn, Statement els)
+ public IfStmt(IToken! tok, Expression guard, Statement! thn, Statement els)
requires els == null || els is BlockStmt || els is IfStmt;
{
this.Guard = guard;
@@ -904,7 +905,7 @@ namespace Microsoft.Dafny public readonly List<Expression!>! Decreases;
public readonly Statement! Body;
- public WhileStmt(Token! tok, Expression guard,
+ public WhileStmt(IToken! tok, Expression guard,
List<MaybeFreeExpression!>! invariants, List<Expression!>! decreases,
Statement! body) {
this.Guard = guard;
@@ -922,7 +923,7 @@ namespace Microsoft.Dafny public readonly List<PredicateStmt!>! BodyPrefix;
public readonly AssignStmt! BodyAssign;
- public ForeachStmt(Token! tok, BoundVar! boundVar, Expression! collection, Expression! range, List<PredicateStmt!>! bodyPrefix, AssignStmt! bodyAssign) {
+ public ForeachStmt(IToken! tok, BoundVar! boundVar, Expression! collection, Expression! range, List<PredicateStmt!>! bodyPrefix, AssignStmt! bodyAssign) {
this.BoundVar = boundVar;
this.Collection = collection;
this.Range = range;
@@ -936,7 +937,7 @@ namespace Microsoft.Dafny public readonly Expression! Source;
public readonly List<MatchCaseStmt!>! Cases;
- public MatchStmt(Token! tok, Expression! source, [Captured] List<MatchCaseStmt!>! cases) {
+ public MatchStmt(IToken! tok, Expression! source, [Captured] List<MatchCaseStmt!>! cases) {
this.Source = source;
this.Cases = cases;
base(tok);
@@ -944,13 +945,13 @@ namespace Microsoft.Dafny }
public class MatchCaseStmt {
- public readonly Token! tok;
+ public readonly IToken! tok;
public readonly string! Id;
public DatatypeCtor Ctor; // filled in by resolution
public readonly List<BoundVar!>! Arguments;
public readonly List<Statement!>! Body;
- public MatchCaseStmt(Token! tok, string! id, [Captured] List<BoundVar!>! arguments, [Captured] List<Statement!>! body) {
+ public MatchCaseStmt(IToken! tok, string! id, [Captured] List<BoundVar!>! arguments, [Captured] List<Statement!>! body) {
this.tok = tok;
this.Id = id;
this.Arguments = arguments;
@@ -961,7 +962,7 @@ namespace Microsoft.Dafny // ------------------------------------------------------------------------------------------------------
public abstract class Expression {
- public readonly Token! tok;
+ public readonly IToken! tok;
protected Type type;
public Type Type { // filled in during resolution
[Verify(false)] // TODO: how do we allow Type.get to modify type and still be [Pure]?
@@ -998,7 +999,7 @@ namespace Microsoft.Dafny }
}
- public Expression(Token! tok)
+ public Expression(IToken! tok)
ensures type == null; // we would have liked to have written Type==null, but that's not admissible or provable
{
this.tok = tok;
@@ -1017,25 +1018,25 @@ namespace Microsoft.Dafny }
}
- public LiteralExpr(Token! tok) { // represents the Dafny literal "null"
+ public LiteralExpr(IToken! tok) { // represents the Dafny literal "null"
this.Value = null;
base(tok);
}
- public LiteralExpr(Token! tok, BigInteger n)
+ public LiteralExpr(IToken! tok, BigInteger n)
requires 0 <= n.Sign;
{
this.Value = n;
base(tok);
}
- public LiteralExpr(Token! tok, int n)
+ public LiteralExpr(IToken! tok, int n)
requires 0 <= n;
{
this(tok, new BigInteger(n));
}
- public LiteralExpr(Token! tok, bool b) {
+ public LiteralExpr(IToken! tok, bool b) {
this.Value = b;
base(tok);
}
@@ -1048,7 +1049,7 @@ namespace Microsoft.Dafny public DatatypeCtor Ctor; // filled in by resolution
public List<Type!>! InferredTypeArgs = new List<Type!>(); // filled in by resolution
- public DatatypeValue(Token! tok, string! datatypeName, string! memberName, [Captured] List<Expression!>! arguments) {
+ public DatatypeValue(IToken! tok, string! datatypeName, string! memberName, [Captured] List<Expression!>! arguments) {
this.DatatypeName = datatypeName;
this.MemberName = memberName;
this.Arguments = arguments;
@@ -1057,13 +1058,13 @@ namespace Microsoft.Dafny }
public class ThisExpr : Expression {
- public ThisExpr(Token! tok) {
+ public ThisExpr(IToken! tok) {
base(tok);
}
}
public class ImplicitThisExpr : ThisExpr {
- public ImplicitThisExpr(Token! tok) {
+ public ImplicitThisExpr(IToken! tok) {
base(tok);
}
}
@@ -1072,7 +1073,7 @@ namespace Microsoft.Dafny public readonly string! Name;
public IVariable Var; // filled in by resolution
- public IdentifierExpr(Token! tok, string! name) {
+ public IdentifierExpr(IToken! tok, string! name) {
Name = name;
base(tok);
}
@@ -1080,20 +1081,20 @@ namespace Microsoft.Dafny public abstract class DisplayExpression : Expression {
public readonly List<Expression!>! Elements;
- public DisplayExpression(Token! tok, List<Expression!>! elements) {
+ public DisplayExpression(IToken! tok, List<Expression!>! elements) {
Elements = elements;
base(tok);
}
}
public class SetDisplayExpr : DisplayExpression {
- public SetDisplayExpr(Token! tok, List<Expression!>! elements) {
+ public SetDisplayExpr(IToken! tok, List<Expression!>! elements) {
base(tok, elements);
}
}
public class SeqDisplayExpr : DisplayExpression {
- public SeqDisplayExpr(Token! tok, List<Expression!>! elements) {
+ public SeqDisplayExpr(IToken! tok, List<Expression!>! elements) {
base(tok, elements);
}
}
@@ -1103,7 +1104,7 @@ namespace Microsoft.Dafny public readonly string! FieldName;
public Field Field; // filled in by resolution
- public FieldSelectExpr(Token! tok, Expression! obj, string! fieldName) {
+ public FieldSelectExpr(IToken! tok, Expression! obj, string! fieldName) {
this.Obj = obj;
this.FieldName = fieldName;
base(tok);
@@ -1118,7 +1119,7 @@ namespace Microsoft.Dafny invariant SelectOne ==> E1 == null;
invariant E0 != null || E1 != null;
- public SeqSelectExpr(Token! tok, bool selectOne, Expression! seq, Expression e0, Expression e1)
+ public SeqSelectExpr(IToken! tok, bool selectOne, Expression! seq, Expression e0, Expression e1)
requires selectOne ==> e1 == null;
requires e0 != null || e1 != null;
{
@@ -1135,7 +1136,7 @@ namespace Microsoft.Dafny public readonly Expression! Index;
public readonly Expression! Value;
- public SeqUpdateExpr(Token! tok, Expression! seq, Expression! index, Expression! val)
+ public SeqUpdateExpr(IToken! tok, Expression! seq, Expression! index, Expression! val)
{
Seq = seq;
Index = index;
@@ -1151,7 +1152,7 @@ namespace Microsoft.Dafny public Function Function; // filled in by resolution
[Captured]
- public FunctionCallExpr(Token! tok, string! fn, Expression! receiver, [Captured] List<Expression!>! args)
+ public FunctionCallExpr(IToken! tok, string! fn, Expression! receiver, [Captured] List<Expression!>! args)
ensures type == null;
ensures Owner.Same(this, receiver);
{
@@ -1166,7 +1167,7 @@ namespace Microsoft.Dafny public class OldExpr : Expression {
[Peer] public readonly Expression! E;
[Captured]
- public OldExpr(Token! tok, Expression! expr) {
+ public OldExpr(IToken! tok, Expression! expr) {
base(tok);
Owner.AssignSame(this, expr);
E = expr;
@@ -1175,7 +1176,7 @@ namespace Microsoft.Dafny public class FreshExpr : Expression {
public readonly Expression! E;
- public FreshExpr(Token! tok, Expression! expr) {
+ public FreshExpr(IToken! tok, Expression! expr) {
E = expr;
base(tok);
}
@@ -1186,7 +1187,7 @@ namespace Microsoft.Dafny public readonly Opcode Op;
public readonly Expression! E;
- public UnaryExpr(Token! tok, Opcode op, Expression! e) {
+ public UnaryExpr(IToken! tok, Opcode op, Expression! e) {
this.Op = op;
this.E = e;
base(tok);
@@ -1243,7 +1244,7 @@ namespace Microsoft.Dafny public readonly Expression! E0;
public readonly Expression! E1;
- public BinaryExpr(Token! tok, Opcode op, Expression! e0, Expression! e1) {
+ public BinaryExpr(IToken! tok, Opcode op, Expression! e0, Expression! e1) {
this.Op = op;
this.E0 = e0;
this.E1 = e1;
@@ -1257,7 +1258,7 @@ namespace Microsoft.Dafny public readonly Triggers Trigs;
public readonly Attributes Attributes;
- public QuantifierExpr(Token! tok, List<BoundVar!>! bvars, Expression! body, Triggers trigs, Attributes attrs) {
+ public QuantifierExpr(IToken! tok, List<BoundVar!>! bvars, Expression! body, Triggers trigs, Attributes attrs) {
this.BoundVars = bvars;
this.Body = body;
this.Trigs = trigs;
@@ -1277,19 +1278,19 @@ namespace Microsoft.Dafny }
public class ForallExpr : QuantifierExpr {
- public ForallExpr(Token! tok, List<BoundVar!>! bvars, Expression! body, Triggers trig, Attributes attrs) {
+ public ForallExpr(IToken! tok, List<BoundVar!>! bvars, Expression! body, Triggers trig, Attributes attrs) {
base(tok, bvars, body, trig, attrs);
}
}
public class ExistsExpr : QuantifierExpr {
- public ExistsExpr(Token! tok, List<BoundVar!>! bvars, Expression! body, Triggers trig, Attributes attrs) {
+ public ExistsExpr(IToken! tok, List<BoundVar!>! bvars, Expression! body, Triggers trig, Attributes attrs) {
base(tok, bvars, body, trig, attrs);
}
}
public class WildcardExpr : Expression { // a WildcardExpr can occur only in reads clauses and a loop's decreases clauses (with different meanings)
- public WildcardExpr(Token! tok) {
+ public WildcardExpr(IToken! tok) {
base(tok);
}
}
@@ -1299,7 +1300,7 @@ namespace Microsoft.Dafny public readonly Expression! Thn;
public readonly Expression! Els;
- public ITEExpr(Token! tok, Expression! test, Expression! thn, Expression! els) {
+ public ITEExpr(IToken! tok, Expression! test, Expression! thn, Expression! els) {
this.Test = test;
this.Thn = thn;
this.Els = els;
@@ -1311,7 +1312,7 @@ namespace Microsoft.Dafny public readonly Expression! Source;
public readonly List<MatchCaseExpr!>! Cases;
- public MatchExpr(Token! tok, Expression! source, [Captured] List<MatchCaseExpr!>! cases) {
+ public MatchExpr(IToken! tok, Expression! source, [Captured] List<MatchCaseExpr!>! cases) {
this.Source = source;
this.Cases = cases;
base(tok);
@@ -1319,13 +1320,13 @@ namespace Microsoft.Dafny }
public class MatchCaseExpr {
- public readonly Token! tok;
+ public readonly IToken! tok;
public readonly string! Id;
public DatatypeCtor Ctor; // filled in by resolution
public readonly List<BoundVar!>! Arguments;
public readonly Expression! Body;
- public MatchCaseExpr(Token! tok, string! id, [Captured] List<BoundVar!>! arguments, Expression! body) {
+ public MatchCaseExpr(IToken! tok, string! id, [Captured] List<BoundVar!>! arguments, Expression! body) {
this.tok = tok;
this.Id = id;
this.Arguments = arguments;
diff --git a/Dafny/DafnyMain.ssc b/Dafny/DafnyMain.ssc index a7d863fe..21375145 100644 --- a/Dafny/DafnyMain.ssc +++ b/Dafny/DafnyMain.ssc @@ -18,7 +18,6 @@ namespace Microsoft.Dafny { modifies Bpl.CommandLineOptions.Clo.XmlSink.*;
{
program = null;
- Dafny.Errors.count = 0;
List<ModuleDecl!> modules = new List<ModuleDecl!>();
foreach (string! dafnyFileName in fileNames){
if (Bpl.CommandLineOptions.Clo.XmlSink != null && Bpl.CommandLineOptions.Clo.XmlSink.IsOpen) {
@@ -35,7 +34,7 @@ namespace Microsoft.Dafny { errorCount = Dafny.Parser.Parse(dafnyFileName, modules);
if (errorCount != 0)
{
- return string.Format("{0} parse errors detected in {1}", Dafny.Errors.count, dafnyFileName);
+ return string.Format("{0} parse errors detected in {1}", errorCount, dafnyFileName);
}
}
catch (IOException e)
diff --git a/Dafny/Makefile b/Dafny/Makefile index fd2141b3..e545fbae 100644 --- a/Dafny/Makefile +++ b/Dafny/Makefile @@ -1,13 +1,18 @@ COCO = ..\..\Binaries\Coco.exe
ASML = ..\..\Binaries\asmlc.boot.exe
+# ###############################################################################
+# The frame files are no longer in this directory. They must be downloaded
+# from http://boogiepartners.codeplex.com/ and then copied into this directory.
+# ###############################################################################
+
# "all" depends on 2 files, really (Parser.cs and Scanner.cs), but they
# are both generated in one go and I don't know a better way to tell
# nmake that. --KRML
all: Parser.ssc
Parser.ssc: Scanner.frame Parser.frame Dafny.atg
- $(COCO) Dafny.atg
+ $(COCO) Dafny.atg -namespace Microsoft.Dafny
copy Parser.cs Parser.ssc
copy Scanner.cs Scanner.ssc
diff --git a/Dafny/Parser.ssc b/Dafny/Parser.ssc index 3752fd33..0f85bbe8 100644 --- a/Dafny/Parser.ssc +++ b/Dafny/Parser.ssc @@ -1,22 +1,38 @@ using System.Collections.Generic;
using System.Numerics;
using Microsoft.Boogie;
+using System.IO;
+using System.Text;
+
+
+
+
+using System;
using Microsoft.Contracts;
namespace Microsoft.Dafny {
+
+
public class Parser {
- const int maxT = 100;
+ public const int _EOF = 0;
+ public const int _ident = 1;
+ public const int _digits = 2;
+ public const int _string = 3;
+ public const int maxT = 100;
const bool T = true;
const bool x = false;
const int minErrDist = 2;
- static Token/*!*/ token; // last recognized token
- static Token/*!*/ t; // lookahead token
- static int errDist = minErrDist;
+ public Scanner/*!*/ scanner;
+ public Errors/*!*/ errors;
- static List<ModuleDecl!>! theModules = new List<ModuleDecl!>();
+ public Token/*!*/ t; // last recognized token
+ public Token/*!*/ la; // lookahead token
+ int errDist = minErrDist;
+
+static List<ModuleDecl!>! theModules = new List<ModuleDecl!>();
static Expression! dummyExpr = new LiteralExpr(Token.NoToken);
@@ -62,15 +78,14 @@ private static Expression! ConvertToLocal(Expression! e) /// Note: first initialize the Scanner.
///</summary>
public static int Parse (string! filename, List<ModuleDecl!>! modules) /* throws System.IO.IOException */ {
+ string s;
if (filename == "stdin.dfy") {
- BoogiePL.Buffer.Fill(System.Console.In);
- Scanner.Init(filename);
- return Parse(modules);
+ s = Microsoft.Boogie.ParserHelper.Fill(System.Console.In, new List<string!>());
+ return Parse(s, modules);
} else {
using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {
- BoogiePL.Buffer.Fill(reader);
- Scanner.Init(filename);
- return Parse(modules);
+ s = Microsoft.Boogie.ParserHelper.Fill(reader, new List<string!>());
+ return Parse(s, filename, modules);
}
}
}
@@ -81,106 +96,122 @@ public static int Parse (string! filename, List<ModuleDecl!>! modules) /* throws /// Returns the number of parsing errors encountered.
/// Note: first initialize the Scanner.
///</summary>
-public static int Parse (List<ModuleDecl!>! modules) {
+public static int Parse (string! s, string! filename, List<ModuleDecl!>! modules) {
List<ModuleDecl!> oldModules = theModules;
theModules = modules;
- Parse();
+ byte[]! buffer = (!) UTF8Encoding.Default.GetBytes(s);
+ MemoryStream ms = new MemoryStream(buffer,false);
+ Errors errors = new Errors();
+ Scanner scanner = new Scanner(ms, errors, filename);
+ Parser parser = new Parser(scanner, errors);
+ parser.Parse();
theModules = oldModules;
- return Errors.count;
+ return parser.errors.count;
}
/*--------------------------------------------------------------------------*/
- static void Error(int n) {
- if (errDist >= minErrDist) Errors.SynErr(n, t.filename, t.line, t.col);
- errDist = 0;
+ public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors) {
+ this.scanner = scanner;
+ this.errors = errors;
+ Token! tok = new Token();
+ tok.val = "";
+ this.la = tok;
+ this.t = new Token(); // just to satisfy its non-null constraint
}
-
- public static void SemErr(string! msg) {
- if (errDist >= minErrDist) Errors.SemErr(token.filename, token.line, token.col, msg);
+
+ void SynErr (int n) {
+ if (errDist >= minErrDist) errors.SynErr(la.filename, la.line, la.col, n);
errDist = 0;
}
- public static void SemErr(Token! tok, string! msg) {
- if (errDist >= minErrDist) Errors.SemErr(tok.filename, tok.line, tok.col, msg);
+ public void SemErr (string! msg) {
+ if (errDist >= minErrDist) errors.SemErr(t, msg);
errDist = 0;
}
+
+ public void SemErr(IToken! tok, string! msg) {
+ errors.SemErr(tok, msg);
+ }
- static void Get() {
+ void Get () {
for (;;) {
- token = t;
- t = Scanner.Scan();
- if (t.kind<=maxT) {errDist++; return;}
+ t = la;
+ la = scanner.Scan();
+ if (la.kind <= maxT) { ++errDist; break; }
- t = token;
+ la = t;
}
}
- static void Expect(int n) {
- if (t.kind==n) Get(); else Error(n);
+ void Expect (int n) {
+ if (la.kind==n) Get(); else { SynErr(n); }
}
- static bool StartOf(int s) {
- return set[s, t.kind];
+ bool StartOf (int s) {
+ return set[s, la.kind];
}
- static void ExpectWeak(int n, int follow) {
- if (t.kind == n) Get();
+ void ExpectWeak (int n, int follow) {
+ if (la.kind == n) Get();
else {
- Error(n);
+ SynErr(n);
while (!StartOf(follow)) Get();
}
}
-
- static bool WeakSeparator(int n, int syFol, int repFol) {
- bool[] s = new bool[maxT+1];
- if (t.kind == n) {Get(); return true;}
- else if (StartOf(repFol)) return false;
+
+
+ bool WeakSeparator(int n, int syFol, int repFol) {
+ int kind = la.kind;
+ if (kind == n) {Get(); return true;}
+ else if (StartOf(repFol)) {return false;}
else {
- for (int i=0; i <= maxT; i++) {
- s[i] = set[syFol, i] || set[repFol, i] || set[0, i];
+ SynErr(n);
+ while (!(set[syFol, kind] || set[repFol, kind] || set[0, kind])) {
+ Get();
+ kind = la.kind;
}
- Error(n);
- while (!s[t.kind]) Get();
return StartOf(syFol);
}
}
+
- static void Dafny() {
+ void Dafny() {
ClassDecl! c; DatatypeDecl! dt;
- Attributes attrs; Token! id; List<string!> theImports;
- List<MemberDecl!> membersDefaultClass = new List<MemberDecl!>();
- ModuleDecl module;
-
- // to support multiple files, create a default module only if theModules doesn't already contain one
- DefaultModuleDecl defaultModule = null;
- foreach (ModuleDecl mdecl in theModules) {
- defaultModule = mdecl as DefaultModuleDecl;
- if (defaultModule != null) { break; }
- }
- bool defaultModuleCreatedHere = false;
- if (defaultModule == null) {
- defaultModuleCreatedHere = true;
- defaultModule = new DefaultModuleDecl();
- }
+ Attributes attrs; IToken! id; List<string!> theImports;
+ List<MemberDecl!> membersDefaultClass = new List<MemberDecl!>();
+ ModuleDecl module;
+
+ // to support multiple files, create a default module only if theModules doesn't already contain one
+ DefaultModuleDecl defaultModule = null;
+ foreach (ModuleDecl mdecl in theModules) {
+ defaultModule = mdecl as DefaultModuleDecl;
+ if (defaultModule != null) { break; }
+ }
+ bool defaultModuleCreatedHere = false;
+ if (defaultModule == null) {
+ defaultModuleCreatedHere = true;
+ defaultModule = new DefaultModuleDecl();
+ }
+
while (StartOf(1)) {
- if (t.kind == 4) {
+ if (la.kind == 4) {
Get();
attrs = null; theImports = new List<string!>();
- while (t.kind == 6) {
+ while (la.kind == 6) {
Attribute(ref attrs);
}
Ident(out id);
- if (t.kind == 5) {
+ if (la.kind == 5) {
Get();
Idents(theImports);
}
module = new ModuleDecl(id, id.val, theImports, attrs);
Expect(6);
- while (t.kind == 8 || t.kind == 12) {
- if (t.kind == 8) {
+ while (la.kind == 8 || la.kind == 12) {
+ if (la.kind == 8) {
ClassDecl(module, out c);
module.TopLevelDecls.Add(c);
} else {
@@ -190,10 +221,10 @@ public static int Parse (List<ModuleDecl!>! modules) { }
theModules.Add(module);
Expect(7);
- } else if (t.kind == 8) {
+ } else if (la.kind == 8) {
ClassDecl(defaultModule, out c);
defaultModule.TopLevelDecls.Add(c);
- } else if (t.kind == 12) {
+ } else if (la.kind == 12) {
DatatypeDecl(defaultModule, out dt);
defaultModule.TopLevelDecls.Add(dt);
} else {
@@ -217,40 +248,40 @@ public static int Parse (List<ModuleDecl!>! modules) { Expect(0);
}
- static void Attribute(ref Attributes attrs) {
+ void Attribute(ref Attributes attrs) {
Expect(6);
AttributeBody(ref attrs);
Expect(7);
}
- static void Ident(out Token! x) {
+ void Ident(out IToken! x) {
Expect(1);
- x = token;
+ x = t;
}
- static void Idents(List<string!>! ids) {
- Token! id;
+ void Idents(List<string!>! ids) {
+ IToken! id;
Ident(out id);
ids.Add(id.val);
- while (t.kind == 15) {
+ while (la.kind == 15) {
Get();
Ident(out id);
ids.Add(id.val);
}
}
- static void ClassDecl(ModuleDecl! module, out ClassDecl! c) {
- Token! id;
+ void ClassDecl(ModuleDecl! module, out ClassDecl! c) {
+ IToken! id;
Attributes attrs = null;
List<TypeParameter!> typeArgs = new List<TypeParameter!>();
List<MemberDecl!> members = new List<MemberDecl!>();
Expect(8);
- while (t.kind == 6) {
+ while (la.kind == 6) {
Attribute(ref attrs);
}
Ident(out id);
- if (t.kind == 17) {
+ if (la.kind == 17) {
GenericParameters(typeArgs);
}
Expect(6);
@@ -261,38 +292,38 @@ public static int Parse (List<ModuleDecl!>! modules) { c = new ClassDecl(id, id.val, module, typeArgs, members, attrs);
}
- static void DatatypeDecl(ModuleDecl! module, out DatatypeDecl! dt) {
- Token! id;
+ void DatatypeDecl(ModuleDecl! module, out DatatypeDecl! dt) {
+ IToken! id;
Attributes attrs = null;
List<TypeParameter!> typeArgs = new List<TypeParameter!>();
List<DatatypeCtor!> ctors = new List<DatatypeCtor!>();
Expect(12);
- while (t.kind == 6) {
+ while (la.kind == 6) {
Attribute(ref attrs);
}
Ident(out id);
- if (t.kind == 17) {
+ if (la.kind == 17) {
GenericParameters(typeArgs);
}
Expect(6);
- while (t.kind == 1 || t.kind == 6) {
+ while (la.kind == 1 || la.kind == 6) {
DatatypeMemberDecl(ctors);
}
Expect(7);
dt = new DatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);
}
- static void ClassMemberDecl(List<MemberDecl!>! mm) {
+ void ClassMemberDecl(List<MemberDecl!>! mm) {
Method! m;
Function! f;
MemberModifiers mmod = new MemberModifiers();
- while (t.kind == 9 || t.kind == 10 || t.kind == 11) {
- if (t.kind == 9) {
+ while (la.kind == 9 || la.kind == 10 || la.kind == 11) {
+ if (la.kind == 9) {
Get();
mmod.IsGhost = true;
- } else if (t.kind == 10) {
+ } else if (la.kind == 10) {
Get();
mmod.IsStatic = true;
} else {
@@ -300,23 +331,23 @@ public static int Parse (List<ModuleDecl!>! modules) { mmod.IsUnlimited = true;
}
}
- if (t.kind == 14) {
+ if (la.kind == 14) {
FieldDecl(mmod, mm);
- } else if (t.kind == 34) {
+ } else if (la.kind == 34) {
FunctionDecl(mmod, out f);
mm.Add(f);
- } else if (t.kind == 19) {
+ } else if (la.kind == 19) {
MethodDecl(mmod, out m);
mm.Add(m);
- } else Error(101);
+ } else SynErr(101);
}
- static void GenericParameters(List<TypeParameter!>! typeArgs) {
- Token! id;
+ void GenericParameters(List<TypeParameter!>! typeArgs) {
+ IToken! id;
Expect(17);
Ident(out id);
typeArgs.Add(new TypeParameter(id, id.val));
- while (t.kind == 15) {
+ while (la.kind == 15) {
Get();
Ident(out id);
typeArgs.Add(new TypeParameter(id, id.val));
@@ -324,20 +355,20 @@ public static int Parse (List<ModuleDecl!>! modules) { Expect(18);
}
- static void FieldDecl(MemberModifiers mmod, List<MemberDecl!>! mm) {
+ void FieldDecl(MemberModifiers mmod, List<MemberDecl!>! mm) {
Attributes attrs = null;
- Token! id; Type! ty;
+ IToken! id; Type! ty;
Expect(14);
- if (mmod.IsUnlimited) { SemErr(token, "fields cannot be declared 'unlimited'"); }
- if (mmod.IsStatic) { SemErr(token, "fields cannot be declared 'static'"); }
+ if (mmod.IsUnlimited) { SemErr(t, "fields cannot be declared 'unlimited'"); }
+ if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }
- while (t.kind == 6) {
+ while (la.kind == 6) {
Attribute(ref attrs);
}
IdentType(out id, out ty);
mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs));
- while (t.kind == 15) {
+ while (la.kind == 15) {
Get();
IdentType(out id, out ty);
mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs));
@@ -345,9 +376,9 @@ public static int Parse (List<ModuleDecl!>! modules) { Expect(13);
}
- static void FunctionDecl(MemberModifiers mmod, out Function! f) {
+ void FunctionDecl(MemberModifiers mmod, out Function! f) {
Attributes attrs = null;
- Token! id;
+ IToken! id;
List<TypeParameter!> typeArgs = new List<TypeParameter!>();
List<Formal!> formals = new List<Formal!>();
Type! returnType;
@@ -358,42 +389,42 @@ public static int Parse (List<ModuleDecl!>! modules) { bool isFunctionMethod = false;
Expect(34);
- if (t.kind == 19) {
+ if (la.kind == 19) {
Get();
isFunctionMethod = true;
}
- if (mmod.IsGhost) { SemErr(token, "functions cannot be declared 'ghost' (they are ghost by default)"); }
+ if (mmod.IsGhost) { SemErr(t, "functions cannot be declared 'ghost' (they are ghost by default)"); }
- while (t.kind == 6) {
+ while (la.kind == 6) {
Attribute(ref attrs);
}
Ident(out id);
- if (t.kind == 17) {
+ if (la.kind == 17) {
GenericParameters(typeArgs);
}
parseVarScope.PushMarker();
Formals(true, false, formals);
Expect(16);
Type(out returnType);
- if (t.kind == 13) {
+ if (la.kind == 13) {
Get();
- while (t.kind == 23 || t.kind == 25 || t.kind == 35) {
+ while (la.kind == 23 || la.kind == 25 || la.kind == 35) {
FunctionSpec(reqs, reads, decreases);
}
} else if (StartOf(3)) {
- while (t.kind == 23 || t.kind == 25 || t.kind == 35) {
+ while (la.kind == 23 || la.kind == 25 || la.kind == 35) {
FunctionSpec(reqs, reads, decreases);
}
FunctionBody(out bb);
body = bb;
- } else Error(102);
+ } else SynErr(102);
parseVarScope.PopMarker();
f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, returnType, reqs, reads, decreases, body, attrs);
}
- static void MethodDecl(MemberModifiers mmod, out Method! m) {
- Token! id;
+ void MethodDecl(MemberModifiers mmod, out Method! m) {
+ IToken! id;
Attributes attrs = null;
List<TypeParameter!>! typeArgs = new List<TypeParameter!>();
List<Formal!> ins = new List<Formal!>();
@@ -405,22 +436,22 @@ public static int Parse (List<ModuleDecl!>! modules) { Statement! bb; BlockStmt body = null;
Expect(19);
- if (mmod.IsUnlimited) { SemErr(token, "methods cannot be declared 'unlimited'"); }
+ if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); }
- while (t.kind == 6) {
+ while (la.kind == 6) {
Attribute(ref attrs);
}
Ident(out id);
- if (t.kind == 17) {
+ if (la.kind == 17) {
GenericParameters(typeArgs);
}
parseVarScope.PushMarker();
Formals(true, true, ins);
- if (t.kind == 20) {
+ if (la.kind == 20) {
Get();
Formals(false, true, outs);
}
- if (t.kind == 13) {
+ if (la.kind == 13) {
Get();
while (StartOf(4)) {
MethodSpec(req, mod, ens, dec);
@@ -431,27 +462,27 @@ public static int Parse (List<ModuleDecl!>! modules) { }
BlockStmt(out bb);
body = (BlockStmt)bb;
- } else Error(103);
+ } else SynErr(103);
parseVarScope.PopMarker();
m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
}
- static void DatatypeMemberDecl(List<DatatypeCtor!>! ctors) {
+ void DatatypeMemberDecl(List<DatatypeCtor!>! ctors) {
Attributes attrs = null;
- Token! id;
+ IToken! id;
List<TypeParameter!> typeArgs = new List<TypeParameter!>();
List<Formal!> formals = new List<Formal!>();
- while (t.kind == 6) {
+ while (la.kind == 6) {
Attribute(ref attrs);
}
Ident(out id);
- if (t.kind == 17) {
+ if (la.kind == 17) {
GenericParameters(typeArgs);
}
parseVarScope.PushMarker();
- if (t.kind == 26) {
+ if (la.kind == 26) {
FormalsOptionalIds(formals);
}
parseVarScope.PopMarker();
@@ -460,13 +491,13 @@ public static int Parse (List<ModuleDecl!>! modules) { Expect(13);
}
- static void FormalsOptionalIds(List<Formal!>! formals) {
- Token! id; Type! ty; string! name; bool isGhost;
+ void FormalsOptionalIds(List<Formal!>! formals) {
+ IToken! id; Type! ty; string! name; bool isGhost;
Expect(26);
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);
- while (t.kind == 15) {
+ while (la.kind == 15) {
Get();
TypeIdentOptional(out id, out name, out ty, out isGhost);
formals.Add(new Formal(id, name, ty, true, isGhost)); parseVarScope.Push(name, name);
@@ -475,31 +506,31 @@ public static int Parse (List<ModuleDecl!>! modules) { Expect(27);
}
- static void IdentType(out Token! id, out Type! ty) {
+ void IdentType(out IToken! id, out Type! ty) {
Ident(out id);
Expect(16);
Type(out ty);
}
- static void GIdentType(bool allowGhost, out Token! id, out Type! ty, out bool isGhost) {
+ void GIdentType(bool allowGhost, out IToken! id, out Type! ty, out bool isGhost) {
isGhost = false;
- if (t.kind == 9) {
+ if (la.kind == 9) {
Get();
- if (allowGhost) { isGhost = true; } else { SemErr(token, "formal cannot be declared 'ghost' in this context"); }
+ if (allowGhost) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); }
}
IdentType(out id, out ty);
}
- static void Type(out Type! ty) {
- Token! tok;
+ void Type(out Type! ty) {
+ IToken! tok;
TypeAndToken(out tok, out ty);
}
- static void IdentTypeOptional(out BoundVar! var) {
- Token! id; Type! ty; Type optType = null;
+ void IdentTypeOptional(out BoundVar! var) {
+ IToken! id; Type! ty; Type optType = null;
Ident(out id);
- if (t.kind == 16) {
+ if (la.kind == 16) {
Get();
Type(out ty);
optType = ty;
@@ -507,14 +538,14 @@ public static int Parse (List<ModuleDecl!>! modules) { var = new BoundVar(id, id.val, optType == null ? new InferredTypeProxy() : optType);
}
- static void TypeIdentOptional(out Token! id, out string! identName, out Type! ty, out bool isGhost) {
+ void TypeIdentOptional(out IToken! id, out string! identName, out Type! ty, out bool isGhost) {
string name = null; isGhost = false;
- if (t.kind == 9) {
+ if (la.kind == 9) {
Get();
isGhost = true;
}
TypeAndToken(out id, out ty);
- if (t.kind == 16) {
+ if (la.kind == 16) {
Get();
UserDefinedType udt = ty as UserDefinedType;
if (udt != null && udt.TypeArgs.Count == 0) {
@@ -533,46 +564,46 @@ public static int Parse (List<ModuleDecl!>! modules) { }
- static void TypeAndToken(out Token! tok, out Type! ty) {
+ void TypeAndToken(out IToken! tok, out Type! ty) {
tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
List<Type!>! gt;
- if (t.kind == 28) {
+ if (la.kind == 28) {
Get();
- tok = token;
- } else if (t.kind == 29) {
+ tok = t;
+ } else if (la.kind == 29) {
Get();
- tok = token; ty = new IntType();
- } else if (t.kind == 30) {
+ tok = t; ty = new IntType();
+ } else if (la.kind == 30) {
Get();
- tok = token; gt = new List<Type!>();
+ tok = t; gt = new List<Type!>();
GenericInstantiation(gt);
if (gt.Count != 1) {
SemErr("set type expects exactly one type argument");
}
ty = new SetType(gt[0]);
- } else if (t.kind == 31) {
+ } else if (la.kind == 31) {
Get();
- tok = token; gt = new List<Type!>();
+ tok = t; gt = new List<Type!>();
GenericInstantiation(gt);
if (gt.Count != 1) {
SemErr("seq type expects exactly one type argument");
}
ty = new SeqType(gt[0]);
- } else if (t.kind == 1 || t.kind == 32 || t.kind == 33) {
+ } else if (la.kind == 1 || la.kind == 32 || la.kind == 33) {
ReferenceType(out tok, out ty);
- } else Error(104);
+ } else SynErr(104);
}
- static void Formals(bool incoming, bool allowGhosts, List<Formal!>! formals) {
- Token! id; Type! ty; bool isGhost;
+ void Formals(bool incoming, bool allowGhosts, List<Formal!>! formals) {
+ IToken! id; Type! ty; bool isGhost;
Expect(26);
- if (t.kind == 1 || t.kind == 9) {
+ if (la.kind == 1 || la.kind == 9) {
GIdentType(allowGhosts, out id, out ty, out isGhost);
formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); parseVarScope.Push(id.val, id.val);
- while (t.kind == 15) {
+ while (la.kind == 15) {
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);
@@ -581,53 +612,53 @@ public static int Parse (List<ModuleDecl!>! modules) { Expect(27);
}
- static void MethodSpec(List<MaybeFreeExpression!>! req, List<FrameExpression!>! mod, List<MaybeFreeExpression!>! ens,
+ void MethodSpec(List<MaybeFreeExpression!>! req, List<FrameExpression!>! mod, List<MaybeFreeExpression!>! ens,
List<Expression!>! decreases) {
Expression! e; FrameExpression! fe; bool isFree = false;
- if (t.kind == 21) {
+ if (la.kind == 21) {
Get();
if (StartOf(7)) {
FrameExpression(out fe);
mod.Add(fe);
- while (t.kind == 15) {
+ while (la.kind == 15) {
Get();
FrameExpression(out fe);
mod.Add(fe);
}
}
Expect(13);
- } else if (t.kind == 22 || t.kind == 23 || t.kind == 24) {
- if (t.kind == 22) {
+ } else if (la.kind == 22 || la.kind == 23 || la.kind == 24) {
+ if (la.kind == 22) {
Get();
isFree = true;
}
- if (t.kind == 23) {
+ if (la.kind == 23) {
Get();
Expression(out e);
Expect(13);
req.Add(new MaybeFreeExpression(e, isFree));
- } else if (t.kind == 24) {
+ } else if (la.kind == 24) {
Get();
Expression(out e);
Expect(13);
ens.Add(new MaybeFreeExpression(e, isFree));
- } else Error(105);
- } else if (t.kind == 25) {
+ } else SynErr(105);
+ } else if (la.kind == 25) {
Get();
Expressions(decreases);
Expect(13);
- } else Error(106);
+ } else SynErr(106);
}
- static void BlockStmt(out Statement! block) {
- Token! x;
+ void BlockStmt(out Statement! block) {
+ IToken! x;
List<Statement!> body = new List<Statement!>();
Statement! s;
parseVarScope.PushMarker();
Expect(6);
- x = token;
+ x = t;
while (StartOf(8)) {
Stmt(body);
}
@@ -636,10 +667,10 @@ List<Expression!>! decreases) { parseVarScope.PopMarker();
}
- static void FrameExpression(out FrameExpression! fe) {
- Expression! e; Token! id; string fieldName = null;
+ void FrameExpression(out FrameExpression! fe) {
+ Expression! e; IToken! id; string fieldName = null;
Expression(out e);
- if (t.kind == 37) {
+ if (la.kind == 37) {
Get();
Ident(out id);
fieldName = id.val;
@@ -647,13 +678,13 @@ List<Expression!>! decreases) { fe = new FrameExpression(e, fieldName);
}
- static void Expression(out Expression! e) {
- Token! x; Expression! e0; Expression! e1 = dummyExpr;
+ void Expression(out Expression! e) {
+ IToken! x; Expression! e0; Expression! e1 = dummyExpr;
e = dummyExpr;
- if (t.kind == 49) {
+ if (la.kind == 49) {
Get();
- x = token;
+ x = t;
Expression(out e);
Expect(61);
Expression(out e0);
@@ -662,26 +693,26 @@ List<Expression!>! decreases) { e = new ITEExpr(x, e, e0, e1);
} else if (StartOf(9)) {
EquivExpression(out e);
- } else Error(107);
+ } else SynErr(107);
}
- static void Expressions(List<Expression!>! args) {
+ void Expressions(List<Expression!>! args) {
Expression! e;
Expression(out e);
args.Add(e);
- while (t.kind == 15) {
+ while (la.kind == 15) {
Get();
Expression(out e);
args.Add(e);
}
}
- static void GenericInstantiation(List<Type!>! gt) {
+ void GenericInstantiation(List<Type!>! gt) {
Type! ty;
Expect(17);
Type(out ty);
gt.Add(ty);
- while (t.kind == 15) {
+ while (la.kind == 15) {
Get();
Type(out ty);
gt.Add(ty);
@@ -689,117 +720,117 @@ List<Expression!>! decreases) { Expect(18);
}
- static void ReferenceType(out Token! tok, out Type! ty) {
+ void ReferenceType(out IToken! tok, out Type! ty) {
tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
List<Type!>! gt;
- if (t.kind == 32) {
+ if (la.kind == 32) {
Get();
- tok = token; ty = new ObjectType();
- } else if (t.kind == 33) {
+ tok = t; ty = new ObjectType();
+ } else if (la.kind == 33) {
Get();
- tok = token; gt = new List<Type!>();
+ tok = t; gt = new List<Type!>();
GenericInstantiation(gt);
if (gt.Count != 1) {
SemErr("array type expects exactly one type argument");
}
ty = UserDefinedType.ArrayType(tok, gt[0]);
- } else if (t.kind == 1) {
+ } else if (la.kind == 1) {
Ident(out tok);
gt = new List<Type!>();
- if (t.kind == 17) {
+ if (la.kind == 17) {
GenericInstantiation(gt);
}
ty = new UserDefinedType(tok, tok.val, gt);
- } else Error(108);
+ } else SynErr(108);
}
- static void FunctionSpec(List<Expression!>! reqs, List<FrameExpression!>! reads, List<Expression!>! decreases) {
+ void FunctionSpec(List<Expression!>! reqs, List<FrameExpression!>! reads, List<Expression!>! decreases) {
Expression! e; FrameExpression! fe;
- if (t.kind == 23) {
+ if (la.kind == 23) {
Get();
Expression(out e);
Expect(13);
reqs.Add(e);
- } else if (t.kind == 35) {
+ } else if (la.kind == 35) {
Get();
if (StartOf(10)) {
PossiblyWildFrameExpression(out fe);
reads.Add(fe);
- while (t.kind == 15) {
+ while (la.kind == 15) {
Get();
PossiblyWildFrameExpression(out fe);
reads.Add(fe);
}
}
Expect(13);
- } else if (t.kind == 25) {
+ } else if (la.kind == 25) {
Get();
Expressions(decreases);
Expect(13);
- } else Error(109);
+ } else SynErr(109);
}
- static void FunctionBody(out Expression! e) {
+ void FunctionBody(out Expression! e) {
e = dummyExpr;
Expect(6);
- if (t.kind == 38) {
+ if (la.kind == 38) {
MatchExpression(out e);
} else if (StartOf(7)) {
Expression(out e);
- } else Error(110);
+ } else SynErr(110);
Expect(7);
}
- static void PossiblyWildFrameExpression(out FrameExpression! fe) {
+ void PossiblyWildFrameExpression(out FrameExpression! fe) {
fe = dummyFrameExpr;
- if (t.kind == 36) {
+ if (la.kind == 36) {
Get();
- fe = new FrameExpression(new WildcardExpr(token), null);
+ fe = new FrameExpression(new WildcardExpr(t), null);
} else if (StartOf(7)) {
FrameExpression(out fe);
- } else Error(111);
+ } else SynErr(111);
}
- static void PossiblyWildExpression(out Expression! e) {
+ void PossiblyWildExpression(out Expression! e) {
e = dummyExpr;
- if (t.kind == 36) {
+ if (la.kind == 36) {
Get();
- e = new WildcardExpr(token);
+ e = new WildcardExpr(t);
} else if (StartOf(7)) {
Expression(out e);
- } else Error(112);
+ } else SynErr(112);
}
- static void MatchExpression(out Expression! e) {
- Token! x; MatchCaseExpr! c;
+ void MatchExpression(out Expression! e) {
+ IToken! x; MatchCaseExpr! c;
List<MatchCaseExpr!> cases = new List<MatchCaseExpr!>();
Expect(38);
- x = token;
+ x = t;
Expression(out e);
- while (t.kind == 39) {
+ while (la.kind == 39) {
CaseExpression(out c);
cases.Add(c);
}
e = new MatchExpr(x, e, cases);
}
- static void CaseExpression(out MatchCaseExpr! c) {
- Token! x, id, arg;
+ void CaseExpression(out MatchCaseExpr! c) {
+ IToken! x, id, arg;
List<BoundVar!> arguments = new List<BoundVar!>();
Expression! body;
Expect(39);
- x = token; parseVarScope.PushMarker();
+ x = t; parseVarScope.PushMarker();
Ident(out id);
- if (t.kind == 26) {
+ if (la.kind == 26) {
Get();
Ident(out arg);
arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
parseVarScope.Push(arg.val, arg.val);
- while (t.kind == 15) {
+ while (la.kind == 15) {
Get();
Ident(out arg);
arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
@@ -813,25 +844,25 @@ List<Expression!>! decreases) { parseVarScope.PopMarker();
}
- static void Stmt(List<Statement!>! ss) {
+ void Stmt(List<Statement!>! ss) {
Statement! s;
- while (t.kind == 6) {
+ while (la.kind == 6) {
BlockStmt(out s);
ss.Add(s);
}
if (StartOf(11)) {
OneStmt(out s);
ss.Add(s);
- } else if (t.kind == 9 || t.kind == 14) {
+ } else if (la.kind == 9 || la.kind == 14) {
VarDeclStmts(ss);
- } else Error(113);
+ } else SynErr(113);
}
- static void OneStmt(out Statement! s) {
- Token! x; Token! id; string label = null;
+ void OneStmt(out Statement! s) {
+ IToken! x; IToken! id; string label = null;
s = dummyStmt; /* to please the compiler */
- switch (t.kind) {
+ switch (la.kind) {
case 57: {
AssertStmt(out s);
break;
@@ -878,7 +909,7 @@ List<Expression!>! decreases) { }
case 41: {
Get();
- x = token;
+ x = t;
Ident(out id);
Expect(16);
s = new LabelStmt(x, id.val);
@@ -886,8 +917,8 @@ List<Expression!>! decreases) { }
case 42: {
Get();
- x = token;
- if (t.kind == 1) {
+ x = t;
+ if (la.kind == 1) {
Ident(out id);
label = id.val;
}
@@ -897,25 +928,25 @@ List<Expression!>! decreases) { }
case 43: {
Get();
- x = token;
+ x = t;
Expect(13);
s = new ReturnStmt(x);
break;
}
- default: Error(114); break;
+ default: SynErr(114); break;
}
}
- static void VarDeclStmts(List<Statement!>! ss) {
+ void VarDeclStmts(List<Statement!>! ss) {
VarDecl! d; bool isGhost = false;
- if (t.kind == 9) {
+ if (la.kind == 9) {
Get();
isGhost = true;
}
Expect(14);
IdentTypeRhs(out d, isGhost);
ss.Add(d); parseVarScope.Push(d.Name, d.Name);
- while (t.kind == 15) {
+ while (la.kind == 15) {
Get();
IdentTypeRhs(out d, isGhost);
ss.Add(d); parseVarScope.Push(d.Name, d.Name);
@@ -923,42 +954,42 @@ List<Expression!>! decreases) { Expect(13);
}
- static void AssertStmt(out Statement! s) {
- Token! x; Expression! e;
+ void AssertStmt(out Statement! s) {
+ IToken! x; Expression! e;
Expect(57);
- x = token;
+ x = t;
Expression(out e);
Expect(13);
s = new AssertStmt(x, e);
}
- static void AssumeStmt(out Statement! s) {
- Token! x; Expression! e;
+ void AssumeStmt(out Statement! s) {
+ IToken! x; Expression! e;
Expect(58);
- x = token;
+ x = t;
Expression(out e);
Expect(13);
s = new AssumeStmt(x, e);
}
- static void UseStmt(out Statement! s) {
- Token! x; Expression! e;
+ void UseStmt(out Statement! s) {
+ IToken! x; Expression! e;
Expect(59);
- x = token;
+ x = t;
Expression(out e);
Expect(13);
s = new UseStmt(x, e);
}
- static void PrintStmt(out Statement! s) {
- Token! x; Attributes.Argument! arg;
+ void PrintStmt(out Statement! s) {
+ IToken! x; Attributes.Argument! arg;
List<Attributes.Argument!> args = new List<Attributes.Argument!>();
Expect(60);
- x = token;
+ x = t;
AttributeArg(out arg);
args.Add(arg);
- while (t.kind == 15) {
+ while (la.kind == 15) {
Get();
AttributeArg(out arg);
args.Add(arg);
@@ -967,8 +998,8 @@ List<Expression!>! decreases) { s = new PrintStmt(x, args);
}
- static void AssignStmt(out Statement! s) {
- Token! x;
+ void AssignStmt(out Statement! s) {
+ IToken! x;
Expression! lhs;
Expression rhs;
Type ty;
@@ -976,7 +1007,7 @@ List<Expression!>! decreases) { LhsExpr(out lhs);
Expect(44);
- x = token;
+ x = t;
AssignRhs(out rhs, out ty);
if (ty == null) {
assert rhs != null;
@@ -990,26 +1021,26 @@ List<Expression!>! decreases) { Expect(13);
}
- static void HavocStmt(out Statement! s) {
- Token! x; Expression! lhs;
+ void HavocStmt(out Statement! s) {
+ IToken! x; Expression! lhs;
Expect(48);
- x = token;
+ x = t;
LhsExpr(out lhs);
Expect(13);
s = new AssignStmt(x, lhs);
}
- static void CallStmt(out Statement! s) {
- Token! x, id;
+ void CallStmt(out Statement! s) {
+ IToken! x, id;
Expression! e;
List<IdentifierExpr!> lhs = new List<IdentifierExpr!>();
List<AutoVarDecl!> newVars = new List<AutoVarDecl!>();
Expect(53);
- x = token;
+ x = t;
CallStmtSubExpr(out e);
- if (t.kind == 15 || t.kind == 44) {
- if (t.kind == 15) {
+ if (la.kind == 15 || la.kind == 44) {
+ if (la.kind == 15) {
Get();
e = ConvertToLocal(e);
if (e is IdentifierExpr) {
@@ -1022,7 +1053,7 @@ List<Expression!>! decreases) { Ident(out id);
RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars);
- while (t.kind == 15) {
+ while (la.kind == 15) {
Get();
Ident(out id);
RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars);
@@ -1054,32 +1085,32 @@ List<Expression!>! decreases) { }
- static void IfStmt(out Statement! ifStmt) {
- Token! x;
+ void IfStmt(out Statement! ifStmt) {
+ IToken! x;
Expression guard;
Statement! thn;
Statement! s;
Statement els = null;
Expect(49);
- x = token;
+ x = t;
Guard(out guard);
BlockStmt(out thn);
- if (t.kind == 50) {
+ if (la.kind == 50) {
Get();
- if (t.kind == 49) {
+ if (la.kind == 49) {
IfStmt(out s);
els = s;
- } else if (t.kind == 6) {
+ } else if (la.kind == 6) {
BlockStmt(out s);
els = s;
- } else Error(115);
+ } else SynErr(115);
}
ifStmt = new IfStmt(x, guard, thn, els);
}
- static void WhileStmt(out Statement! stmt) {
- Token! x;
+ void WhileStmt(out Statement! stmt) {
+ IToken! x;
Expression guard;
bool isFree; Expression! e;
List<MaybeFreeExpression!> invariants = new List<MaybeFreeExpression!>();
@@ -1087,13 +1118,13 @@ List<Expression!>! decreases) { Statement! body;
Expect(51);
- x = token;
+ x = t;
Guard(out guard);
assume guard == null || Owner.None(guard);
- while (t.kind == 22 || t.kind == 25 || t.kind == 52) {
- if (t.kind == 22 || t.kind == 52) {
+ while (la.kind == 22 || la.kind == 25 || la.kind == 52) {
+ if (la.kind == 22 || la.kind == 52) {
isFree = false;
- if (t.kind == 22) {
+ if (la.kind == 22) {
Get();
isFree = true;
}
@@ -1105,7 +1136,7 @@ List<Expression!>! decreases) { Get();
PossiblyWildExpression(out e);
decreases.Add(e);
- while (t.kind == 15) {
+ while (la.kind == 15) {
Get();
PossiblyWildExpression(out e);
decreases.Add(e);
@@ -1117,14 +1148,14 @@ List<Expression!>! decreases) { stmt = new WhileStmt(x, guard, invariants, decreases, body);
}
- static void MatchStmt(out Statement! s) {
+ void MatchStmt(out Statement! s) {
Token x; Expression! e; MatchCaseStmt! c;
List<MatchCaseStmt!> cases = new List<MatchCaseStmt!>();
Expect(38);
- x = token;
+ x = t;
Expression(out e);
Expect(6);
- while (t.kind == 39) {
+ while (la.kind == 39) {
CaseStatement(out c);
cases.Add(c);
}
@@ -1132,8 +1163,8 @@ List<Expression!>! decreases) { s = new MatchStmt(x, e, cases);
}
- static void ForeachStmt(out Statement! s) {
- Token! x, boundVar;
+ void ForeachStmt(out Statement! s) {
+ IToken! x, boundVar;
Type! ty;
Expression! collection;
Expression! range;
@@ -1142,30 +1173,30 @@ List<Expression!>! decreases) { parseVarScope.PushMarker();
Expect(54);
- x = token;
+ x = t;
range = new LiteralExpr(x, true);
ty = new InferredTypeProxy();
Expect(26);
Ident(out boundVar);
- if (t.kind == 16) {
+ if (la.kind == 16) {
Get();
Type(out ty);
}
Expect(55);
Expression(out collection);
parseVarScope.Push(boundVar.val, boundVar.val);
- if (t.kind == 56) {
+ if (la.kind == 56) {
Get();
Expression(out range);
}
Expect(27);
Expect(6);
- while (t.kind == 57 || t.kind == 58 || t.kind == 59) {
- if (t.kind == 57) {
+ while (la.kind == 57 || la.kind == 58 || la.kind == 59) {
+ if (la.kind == 57) {
AssertStmt(out s);
if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); }
- } else if (t.kind == 58) {
+ } else if (la.kind == 58) {
AssumeStmt(out s);
if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); }
} else {
@@ -1176,10 +1207,10 @@ List<Expression!>! decreases) { if (StartOf(12)) {
AssignStmt(out s);
if (s is AssignStmt) { bodyAssign = (AssignStmt)s; }
- } else if (t.kind == 48) {
+ } else if (la.kind == 48) {
HavocStmt(out s);
if (s is AssignStmt) { bodyAssign = (AssignStmt)s; }
- } else Error(116);
+ } else SynErr(116);
Expect(7);
if (bodyAssign != null) {
s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);
@@ -1190,19 +1221,19 @@ List<Expression!>! decreases) { parseVarScope.PopMarker();
}
- static void LhsExpr(out Expression! e) {
+ void LhsExpr(out Expression! e) {
SelectExpression(out e);
}
- static void AssignRhs(out Expression e, out Type ty) {
- Token! x; Expression! ee; Type! tt;
+ void AssignRhs(out Expression e, out Type ty) {
+ IToken! x; Expression! ee; Type! tt;
e = null; ty = null;
- if (t.kind == 45) {
+ if (la.kind == 45) {
Get();
TypeAndToken(out x, out tt);
ty = tt;
- if (t.kind == 46) {
+ if (la.kind == 46) {
Get();
Expression(out ee);
Expect(47);
@@ -1211,34 +1242,34 @@ List<Expression!>! decreases) { } else if (StartOf(7)) {
Expression(out ee);
e = ee;
- } else Error(117);
+ } else SynErr(117);
if (e == null && ty == null) { e = dummyExpr; }
}
- static void SelectExpression(out Expression! e) {
- Token! id; e = dummyExpr;
- if (t.kind == 1) {
+ void SelectExpression(out Expression! e) {
+ IToken! id; e = dummyExpr;
+ if (la.kind == 1) {
IdentOrFuncExpression(out e);
- } else if (t.kind == 26 || t.kind == 92 || t.kind == 93) {
+ } else if (la.kind == 26 || la.kind == 92 || la.kind == 93) {
ObjectExpression(out e);
- } else Error(118);
- while (t.kind == 46 || t.kind == 89) {
+ } else SynErr(118);
+ while (la.kind == 46 || la.kind == 89) {
SelectOrCallSuffix(ref e);
}
}
- static void IdentTypeRhs(out VarDecl! d, bool isGhost) {
- Token! id; Type! ty; Expression! e;
+ void IdentTypeRhs(out VarDecl! d, bool isGhost) {
+ IToken! id; Type! ty; Expression! e;
Expression rhs = null; Type newType = null;
Type optionalType = null; DeterminedAssignmentRhs optionalRhs = null;
Ident(out id);
- if (t.kind == 16) {
+ if (la.kind == 16) {
Get();
Type(out ty);
optionalType = ty;
}
- if (t.kind == 44) {
+ if (la.kind == 44) {
Get();
AssignRhs(out rhs, out newType);
}
@@ -1257,33 +1288,33 @@ List<Expression!>! decreases) { }
- static void Guard(out Expression e) {
+ void Guard(out Expression e) {
Expression! ee; e = null;
Expect(26);
- if (t.kind == 36) {
+ if (la.kind == 36) {
Get();
e = null;
} else if (StartOf(7)) {
Expression(out ee);
e = ee;
- } else Error(119);
+ } else SynErr(119);
Expect(27);
}
- static void CaseStatement(out MatchCaseStmt! c) {
- Token! x, id, arg;
+ void CaseStatement(out MatchCaseStmt! c) {
+ IToken! x, id, arg;
List<BoundVar!> arguments = new List<BoundVar!>();
List<Statement!> body = new List<Statement!>();
Expect(39);
- x = token; parseVarScope.PushMarker();
+ x = t; parseVarScope.PushMarker();
Ident(out id);
- if (t.kind == 26) {
+ if (la.kind == 26) {
Get();
Ident(out arg);
arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
parseVarScope.Push(arg.val, arg.val);
- while (t.kind == 15) {
+ while (la.kind == 15) {
Get();
Ident(out arg);
arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
@@ -1301,83 +1332,83 @@ List<Expression!>! decreases) { parseVarScope.PopMarker();
}
- static void CallStmtSubExpr(out Expression! e) {
+ void CallStmtSubExpr(out Expression! e) {
e = dummyExpr;
- if (t.kind == 1) {
+ if (la.kind == 1) {
IdentOrFuncExpression(out e);
- } else if (t.kind == 26 || t.kind == 92 || t.kind == 93) {
+ } else if (la.kind == 26 || la.kind == 92 || la.kind == 93) {
ObjectExpression(out e);
SelectOrCallSuffix(ref e);
- } else Error(120);
- while (t.kind == 46 || t.kind == 89) {
+ } else SynErr(120);
+ while (la.kind == 46 || la.kind == 89) {
SelectOrCallSuffix(ref e);
}
}
- static void AttributeArg(out Attributes.Argument! arg) {
+ void AttributeArg(out Attributes.Argument! arg) {
Expression! e; arg = dummyAttrArg;
- if (t.kind == 3) {
+ if (la.kind == 3) {
Get();
- arg = new Attributes.Argument(token.val.Substring(1, token.val.Length-2));
+ arg = new Attributes.Argument(t.val.Substring(1, t.val.Length-2));
} else if (StartOf(7)) {
Expression(out e);
arg = new Attributes.Argument(e);
- } else Error(121);
+ } else SynErr(121);
}
- static void EquivExpression(out Expression! e0) {
- Token! x; Expression! e1;
+ void EquivExpression(out Expression! e0) {
+ IToken! x; Expression! e1;
ImpliesExpression(out e0);
- while (t.kind == 62 || t.kind == 63) {
+ while (la.kind == 62 || la.kind == 63) {
EquivOp();
- x = token;
+ x = t;
ImpliesExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Iff, e0, e1);
}
}
- static void ImpliesExpression(out Expression! e0) {
- Token! x; Expression! e1;
+ void ImpliesExpression(out Expression! e0) {
+ IToken! x; Expression! e1;
LogicalExpression(out e0);
- if (t.kind == 64 || t.kind == 65) {
+ if (la.kind == 64 || la.kind == 65) {
ImpliesOp();
- x = token;
+ x = t;
ImpliesExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Imp, e0, e1);
}
}
- static void EquivOp() {
- if (t.kind == 62) {
+ void EquivOp() {
+ if (la.kind == 62) {
Get();
- } else if (t.kind == 63) {
+ } else if (la.kind == 63) {
Get();
- } else Error(122);
+ } else SynErr(122);
}
- static void LogicalExpression(out Expression! e0) {
- Token! x; Expression! e1;
+ void LogicalExpression(out Expression! e0) {
+ IToken! x; Expression! e1;
RelationalExpression(out e0);
if (StartOf(13)) {
- if (t.kind == 66 || t.kind == 67) {
+ if (la.kind == 66 || la.kind == 67) {
AndOp();
- x = token;
+ x = t;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1);
- while (t.kind == 66 || t.kind == 67) {
+ while (la.kind == 66 || la.kind == 67) {
AndOp();
- x = token;
+ x = t;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1);
}
} else {
OrOp();
- x = token;
+ x = t;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1);
- while (t.kind == 68 || t.kind == 69) {
+ while (la.kind == 68 || la.kind == 69) {
OrOp();
- x = token;
+ x = t;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1);
}
@@ -1385,16 +1416,16 @@ List<Expression!>! decreases) { }
}
- static void ImpliesOp() {
- if (t.kind == 64) {
+ void ImpliesOp() {
+ if (la.kind == 64) {
Get();
- } else if (t.kind == 65) {
+ } else if (la.kind == 65) {
Get();
- } else Error(123);
+ } else SynErr(123);
}
- static void RelationalExpression(out Expression! e0) {
- Token! x; Expression! e1; BinaryExpr.Opcode op;
+ void RelationalExpression(out Expression! e0) {
+ IToken! x; Expression! e1; BinaryExpr.Opcode op;
Term(out e0);
if (StartOf(14)) {
RelOp(out x, out op);
@@ -1403,206 +1434,206 @@ List<Expression!>! decreases) { }
}
- static void AndOp() {
- if (t.kind == 66) {
+ void AndOp() {
+ if (la.kind == 66) {
Get();
- } else if (t.kind == 67) {
+ } else if (la.kind == 67) {
Get();
- } else Error(124);
+ } else SynErr(124);
}
- static void OrOp() {
- if (t.kind == 68) {
+ void OrOp() {
+ if (la.kind == 68) {
Get();
- } else if (t.kind == 69) {
+ } else if (la.kind == 69) {
Get();
- } else Error(125);
+ } else SynErr(125);
}
- static void Term(out Expression! e0) {
- Token! x; Expression! e1; BinaryExpr.Opcode op;
+ void Term(out Expression! e0) {
+ IToken! x; Expression! e1; BinaryExpr.Opcode op;
Factor(out e0);
- while (t.kind == 79 || t.kind == 80) {
+ while (la.kind == 79 || la.kind == 80) {
AddOp(out x, out op);
Factor(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
}
}
- static void RelOp(out Token! x, out BinaryExpr.Opcode op) {
+ void RelOp(out IToken! x, out BinaryExpr.Opcode op) {
x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
- switch (t.kind) {
+ switch (la.kind) {
case 70: {
Get();
- x = token; op = BinaryExpr.Opcode.Eq;
+ x = t; op = BinaryExpr.Opcode.Eq;
break;
}
case 17: {
Get();
- x = token; op = BinaryExpr.Opcode.Lt;
+ x = t; op = BinaryExpr.Opcode.Lt;
break;
}
case 18: {
Get();
- x = token; op = BinaryExpr.Opcode.Gt;
+ x = t; op = BinaryExpr.Opcode.Gt;
break;
}
case 71: {
Get();
- x = token; op = BinaryExpr.Opcode.Le;
+ x = t; op = BinaryExpr.Opcode.Le;
break;
}
case 72: {
Get();
- x = token; op = BinaryExpr.Opcode.Ge;
+ x = t; op = BinaryExpr.Opcode.Ge;
break;
}
case 73: {
Get();
- x = token; op = BinaryExpr.Opcode.Neq;
+ x = t; op = BinaryExpr.Opcode.Neq;
break;
}
case 74: {
Get();
- x = token; op = BinaryExpr.Opcode.Disjoint;
+ x = t; op = BinaryExpr.Opcode.Disjoint;
break;
}
case 55: {
Get();
- x = token; op = BinaryExpr.Opcode.In;
+ x = t; op = BinaryExpr.Opcode.In;
break;
}
case 75: {
Get();
- x = token; op = BinaryExpr.Opcode.NotIn;
+ x = t; op = BinaryExpr.Opcode.NotIn;
break;
}
case 76: {
Get();
- x = token; op = BinaryExpr.Opcode.Neq;
+ x = t; op = BinaryExpr.Opcode.Neq;
break;
}
case 77: {
Get();
- x = token; op = BinaryExpr.Opcode.Le;
+ x = t; op = BinaryExpr.Opcode.Le;
break;
}
case 78: {
Get();
- x = token; op = BinaryExpr.Opcode.Ge;
+ x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- default: Error(126); break;
+ default: SynErr(126); break;
}
}
- static void Factor(out Expression! e0) {
- Token! x; Expression! e1; BinaryExpr.Opcode op;
+ void Factor(out Expression! e0) {
+ IToken! x; Expression! e1; BinaryExpr.Opcode op;
UnaryExpression(out e0);
- while (t.kind == 36 || t.kind == 81 || t.kind == 82) {
+ while (la.kind == 36 || la.kind == 81 || la.kind == 82) {
MulOp(out x, out op);
UnaryExpression(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
}
}
- static void AddOp(out Token! x, out BinaryExpr.Opcode op) {
+ void AddOp(out IToken! x, out BinaryExpr.Opcode op) {
x = Token.NoToken; op=BinaryExpr.Opcode.Add/*(dummy)*/;
- if (t.kind == 79) {
+ if (la.kind == 79) {
Get();
- x = token; op = BinaryExpr.Opcode.Add;
- } else if (t.kind == 80) {
+ x = t; op = BinaryExpr.Opcode.Add;
+ } else if (la.kind == 80) {
Get();
- x = token; op = BinaryExpr.Opcode.Sub;
- } else Error(127);
+ x = t; op = BinaryExpr.Opcode.Sub;
+ } else SynErr(127);
}
- static void UnaryExpression(out Expression! e) {
- Token! x; e = dummyExpr;
- if (t.kind == 80) {
+ void UnaryExpression(out Expression! e) {
+ IToken! x; e = dummyExpr;
+ if (la.kind == 80) {
Get();
- x = token;
+ x = t;
UnaryExpression(out e);
e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e);
- } else if (t.kind == 83 || t.kind == 84) {
+ } else if (la.kind == 83 || la.kind == 84) {
NegOp();
- x = token;
+ x = t;
UnaryExpression(out e);
e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e);
} else if (StartOf(12)) {
SelectExpression(out e);
} else if (StartOf(15)) {
ConstAtomExpression(out e);
- } else Error(128);
+ } else SynErr(128);
}
- static void MulOp(out Token! x, out BinaryExpr.Opcode op) {
+ void MulOp(out IToken! x, out BinaryExpr.Opcode op) {
x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
- if (t.kind == 36) {
+ if (la.kind == 36) {
Get();
- x = token; op = BinaryExpr.Opcode.Mul;
- } else if (t.kind == 81) {
+ x = t; op = BinaryExpr.Opcode.Mul;
+ } else if (la.kind == 81) {
Get();
- x = token; op = BinaryExpr.Opcode.Div;
- } else if (t.kind == 82) {
+ x = t; op = BinaryExpr.Opcode.Div;
+ } else if (la.kind == 82) {
Get();
- x = token; op = BinaryExpr.Opcode.Mod;
- } else Error(129);
+ x = t; op = BinaryExpr.Opcode.Mod;
+ } else SynErr(129);
}
- static void NegOp() {
- if (t.kind == 83) {
+ void NegOp() {
+ if (la.kind == 83) {
Get();
- } else if (t.kind == 84) {
+ } else if (la.kind == 84) {
Get();
- } else Error(130);
+ } else SynErr(130);
}
- static void ConstAtomExpression(out Expression! e) {
- Token! x, dtName, id; BigInteger n; List<Expression!>! elements;
+ void ConstAtomExpression(out Expression! e) {
+ IToken! x, dtName, id; BigInteger n; List<Expression!>! elements;
e = dummyExpr;
- switch (t.kind) {
+ switch (la.kind) {
case 85: {
Get();
- e = new LiteralExpr(token, false);
+ e = new LiteralExpr(t, false);
break;
}
case 86: {
Get();
- e = new LiteralExpr(token, true);
+ e = new LiteralExpr(t, true);
break;
}
case 87: {
Get();
- e = new LiteralExpr(token);
+ e = new LiteralExpr(t);
break;
}
case 2: {
Nat(out n);
- e = new LiteralExpr(token, n);
+ e = new LiteralExpr(t, n);
break;
}
case 88: {
Get();
- x = token;
+ x = t;
Ident(out dtName);
Expect(89);
Ident(out id);
elements = new List<Expression!>();
- if (t.kind == 26) {
+ if (la.kind == 26) {
Get();
if (StartOf(7)) {
Expressions(elements);
}
Expect(27);
}
- e = new DatatypeValue(token, dtName.val, id.val, elements);
+ e = new DatatypeValue(t, dtName.val, id.val, elements);
break;
}
case 90: {
Get();
- x = token;
+ x = t;
Expect(26);
Expression(out e);
Expect(27);
@@ -1611,7 +1642,7 @@ List<Expression!>! decreases) { }
case 56: {
Get();
- x = token;
+ x = t;
Expression(out e);
e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e);
Expect(56);
@@ -1619,7 +1650,7 @@ List<Expression!>! decreases) { }
case 6: {
Get();
- x = token; elements = new List<Expression!>();
+ x = t; elements = new List<Expression!>();
if (StartOf(7)) {
Expressions(elements);
}
@@ -1629,7 +1660,7 @@ List<Expression!>! decreases) { }
case 46: {
Get();
- x = token; elements = new List<Expression!>();
+ x = t; elements = new List<Expression!>();
if (StartOf(7)) {
Expressions(elements);
}
@@ -1637,14 +1668,14 @@ List<Expression!>! decreases) { Expect(47);
break;
}
- default: Error(131); break;
+ default: SynErr(131); break;
}
}
- static void Nat(out BigInteger n) {
+ void Nat(out BigInteger n) {
Expect(2);
try {
- n = BigInteger.Parse(token.val);
+ n = BigInteger.Parse(t.val);
} catch (System.FormatException) {
SemErr("incorrectly formatted number");
n = BigInteger.Zero;
@@ -1652,10 +1683,10 @@ List<Expression!>! decreases) { }
- static void IdentOrFuncExpression(out Expression! e) {
- Token! id; e = dummyExpr; List<Expression!>! args;
+ void IdentOrFuncExpression(out Expression! e) {
+ IToken! id; e = dummyExpr; List<Expression!>! args;
Ident(out id);
- if (t.kind == 26) {
+ if (la.kind == 26) {
Get();
args = new List<Expression!>();
if (StartOf(7)) {
@@ -1674,38 +1705,38 @@ List<Expression!>! decreases) { }
- static void ObjectExpression(out Expression! e) {
- Token! x; e = dummyExpr;
- if (t.kind == 92) {
+ void ObjectExpression(out Expression! e) {
+ IToken! x; e = dummyExpr;
+ if (la.kind == 92) {
Get();
- e = new ThisExpr(token);
- } else if (t.kind == 93) {
+ e = new ThisExpr(t);
+ } else if (la.kind == 93) {
Get();
- x = token;
+ x = t;
Expect(26);
Expression(out e);
Expect(27);
e = new OldExpr(x, e);
- } else if (t.kind == 26) {
+ } else if (la.kind == 26) {
Get();
if (StartOf(16)) {
QuantifierGuts(out e);
} else if (StartOf(7)) {
Expression(out e);
- } else Error(132);
+ } else SynErr(132);
Expect(27);
- } else Error(133);
+ } else SynErr(133);
}
- static void SelectOrCallSuffix(ref Expression! e) {
- Token! id, x; List<Expression!>! args;
+ void SelectOrCallSuffix(ref Expression! e) {
+ IToken! id, x; List<Expression!>! args;
Expression e0 = null; Expression e1 = null; Expression! ee; bool anyDots = false;
bool func = false;
- if (t.kind == 89) {
+ if (la.kind == 89) {
Get();
Ident(out id);
- if (t.kind == 26) {
+ if (la.kind == 26) {
Get();
args = new List<Expression!>(); func = true;
if (StartOf(7)) {
@@ -1715,14 +1746,14 @@ List<Expression!>! decreases) { e = new FunctionCallExpr(id, id.val, e, args);
}
if (!func) { e = new FieldSelectExpr(id, e, id.val); }
- } else if (t.kind == 46) {
+ } else if (la.kind == 46) {
Get();
- x = token;
+ x = t;
if (StartOf(7)) {
Expression(out ee);
e0 = ee;
- if (t.kind == 44 || t.kind == 91) {
- if (t.kind == 91) {
+ if (la.kind == 44 || la.kind == 91) {
+ if (la.kind == 91) {
Get();
anyDots = true;
if (StartOf(7)) {
@@ -1735,11 +1766,11 @@ List<Expression!>! decreases) { e1 = ee;
}
}
- } else if (t.kind == 91) {
+ } else if (la.kind == 91) {
Get();
Expression(out ee);
anyDots = true; e1 = ee;
- } else Error(134);
+ } else SynErr(134);
if (!anyDots && e0 == null) {
/* a parsing error occurred */
e0 = dummyExpr;
@@ -1757,35 +1788,35 @@ List<Expression!>! decreases) { }
Expect(47);
- } else Error(135);
+ } else SynErr(135);
}
- static void QuantifierGuts(out Expression! q) {
- Token! x = Token.NoToken;
+ void QuantifierGuts(out Expression! q) {
+ IToken! x = Token.NoToken;
bool univ = false;
BoundVar! bv;
List<BoundVar!> bvars = new List<BoundVar!>();
- Token! tok; Expr! e; ExprSeq! es;
+ IToken! tok; Expr! e; ExprSeq! es;
Attributes attrs = null;
Triggers trigs = null;
Expression! body;
- if (t.kind == 94 || t.kind == 95) {
+ if (la.kind == 94 || la.kind == 95) {
Forall();
- x = token; univ = true;
- } else if (t.kind == 96 || t.kind == 97) {
+ x = t; univ = true;
+ } else if (la.kind == 96 || la.kind == 97) {
Exists();
- x = token;
- } else Error(136);
+ x = t;
+ } else SynErr(136);
parseVarScope.PushMarker();
IdentTypeOptional(out bv);
bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name);
- while (t.kind == 15) {
+ while (la.kind == 15) {
Get();
IdentTypeOptional(out bv);
bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name);
}
- while (t.kind == 6) {
+ while (la.kind == 6) {
AttributeOrTrigger(ref attrs, ref trigs);
}
QSep();
@@ -1799,56 +1830,56 @@ List<Expression!>! decreases) { }
- static void Forall() {
- if (t.kind == 94) {
+ void Forall() {
+ if (la.kind == 94) {
Get();
- } else if (t.kind == 95) {
+ } else if (la.kind == 95) {
Get();
- } else Error(137);
+ } else SynErr(137);
}
- static void Exists() {
- if (t.kind == 96) {
+ void Exists() {
+ if (la.kind == 96) {
Get();
- } else if (t.kind == 97) {
+ } else if (la.kind == 97) {
Get();
- } else Error(138);
+ } else SynErr(138);
}
- static void AttributeOrTrigger(ref Attributes attrs, ref Triggers trigs) {
+ void AttributeOrTrigger(ref Attributes attrs, ref Triggers trigs) {
List<Expression!> es = new List<Expression!>();
Expect(6);
- if (t.kind == 16) {
+ if (la.kind == 16) {
AttributeBody(ref attrs);
} else if (StartOf(7)) {
es = new List<Expression!>();
Expressions(es);
trigs = new Triggers(es, trigs);
- } else Error(139);
+ } else SynErr(139);
Expect(7);
}
- static void QSep() {
- if (t.kind == 98) {
+ void QSep() {
+ if (la.kind == 98) {
Get();
- } else if (t.kind == 99) {
+ } else if (la.kind == 99) {
Get();
- } else Error(140);
+ } else SynErr(140);
}
- static void AttributeBody(ref Attributes attrs) {
+ void AttributeBody(ref Attributes attrs) {
string aName;
List<Attributes.Argument!> aArgs = new List<Attributes.Argument!>();
Attributes.Argument! aArg;
Expect(16);
Expect(1);
- aName = token.val;
+ aName = t.val;
if (StartOf(17)) {
AttributeArg(out aArg);
aArgs.Add(aArg);
- while (t.kind == 15) {
+ while (la.kind == 15) {
Get();
AttributeArg(out aArg);
aArgs.Add(aArg);
@@ -1859,120 +1890,150 @@ List<Expression!>! decreases) { - public static void Parse() {
- Errors.SynErr = new ErrorProc(SynErr);
- t = new Token();
+ public void Parse() {
+ la = new Token();
+ la.val = "";
Get();
Dafny();
+ 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, T,x,x,x, T,T,T,T, T,x,T,x, x,x,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,T,x, x,x,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,T, x,T,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,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, 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,T,T,x, x,x,T,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,T,x, x,T,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,x,x,T, T,T,T,T, T,x,T,x, T,T,x,x, x,x,x,x, x,x},
+ {x,T,x,x, x,x,T,x, x,T,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, x,x,x,x, T,T,x,T, x,T,T,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, T,T,x,x, x,x,x,x, x,x},
+ {x,T,T,x, x,x,T,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,T,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, T,x,T,x, T,T,x,x, x,x,x,x, x,x},
+ {x,T,T,x, x,x,T,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, T,x,x,x, x,x,x,x, x,x,T,x, x,T,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,x,x,T, T,T,T,T, T,x,T,x, T,T,x,x, x,x,x,x, x,x},
+ {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, x,x,x,x, T,T,x,T, x,T,T,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, T,T,x,x, x,x,x,x, x,x},
+ {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,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,T, x,x,x,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,T,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,T,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,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,T,T, T,T,x,x, x,x},
+ {x,T,T,T, x,x,T,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,T,x, x,T,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,x,x,T, T,T,T,T, T,x,T,x, T,T,x,x, x,x,x,x, x,x}
- [Microsoft.Contracts.Verify(false)]
- static void SynErr(int n, string filename, int line, int col) {
- Errors.count++;
- System.Console.Write("{0}({1},{2}): syntax error: ", filename, line, col);
+ };
+} // end Parser
+
+
+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 = "-- line {0} col {1}: {2}"; // 0=line, 1=column, 2=text
+ public string! errMsgFormat4 = "{0}({1},{2}): Error: {3}"; // 0=line, 1=column, 2=text
+ public string! errMsgFormat = "-- line {0} col {1}: {2}"; // 0=line, 1=column, 2=text
+
+ public void SynErr (string filename, int line, int col, int n) {
string s;
+ Console.Write("{0}({1},{2}): syntax error: ", filename, line, col);
switch (n) {
case 0: s = "EOF expected"; break;
case 1: s = "ident expected"; break;
case 2: s = "digits expected"; break;
case 3: s = "string expected"; break;
- case 4: s = "module expected"; break;
- case 5: s = "imports expected"; break;
- case 6: s = "{ expected"; break;
- case 7: s = "} expected"; break;
- case 8: s = "class expected"; break;
- case 9: s = "ghost expected"; break;
- case 10: s = "static expected"; break;
- case 11: s = "unlimited expected"; break;
- case 12: s = "datatype expected"; break;
- case 13: s = "; expected"; break;
- case 14: s = "var expected"; break;
- case 15: s = ", expected"; break;
- case 16: s = ": expected"; break;
- case 17: s = "< expected"; break;
- case 18: s = "> expected"; break;
- case 19: s = "method expected"; break;
- case 20: s = "returns expected"; break;
- case 21: s = "modifies expected"; break;
- case 22: s = "free expected"; break;
- case 23: s = "requires expected"; break;
- case 24: s = "ensures expected"; break;
- case 25: s = "decreases expected"; break;
- case 26: s = "( expected"; break;
- case 27: s = ") expected"; break;
- case 28: s = "bool expected"; break;
- case 29: s = "int expected"; break;
- case 30: s = "set expected"; break;
- case 31: s = "seq expected"; break;
- case 32: s = "object expected"; break;
- case 33: s = "array expected"; break;
- case 34: s = "function expected"; break;
- case 35: s = "reads expected"; break;
- case 36: s = "* expected"; break;
- case 37: s = "` expected"; break;
- case 38: s = "match expected"; break;
- case 39: s = "case expected"; break;
- case 40: s = "=> expected"; break;
- case 41: s = "label expected"; break;
- case 42: s = "break expected"; break;
- case 43: s = "return expected"; break;
- case 44: s = ":= expected"; break;
- case 45: s = "new expected"; break;
- case 46: s = "[ expected"; break;
- case 47: s = "] expected"; break;
- case 48: s = "havoc expected"; break;
- case 49: s = "if expected"; break;
- case 50: s = "else expected"; break;
- case 51: s = "while expected"; break;
- case 52: s = "invariant expected"; break;
- case 53: s = "call expected"; break;
- case 54: s = "foreach expected"; break;
- case 55: s = "in expected"; break;
- case 56: s = "| expected"; break;
- case 57: s = "assert expected"; break;
- case 58: s = "assume expected"; break;
- case 59: s = "use expected"; break;
- case 60: s = "print expected"; break;
- case 61: s = "then expected"; break;
- case 62: s = "<==> expected"; break;
- case 63: s = "\\u21d4 expected"; break;
- case 64: s = "==> expected"; break;
- case 65: s = "\\u21d2 expected"; break;
- case 66: s = "&& expected"; break;
- case 67: s = "\\u2227 expected"; break;
- case 68: s = "|| expected"; break;
- case 69: s = "\\u2228 expected"; break;
- case 70: s = "== expected"; break;
- case 71: s = "<= expected"; break;
- case 72: s = ">= expected"; break;
- case 73: s = "!= expected"; break;
- case 74: s = "!! expected"; break;
- case 75: s = "!in expected"; break;
- case 76: s = "\\u2260 expected"; break;
- case 77: s = "\\u2264 expected"; break;
- case 78: s = "\\u2265 expected"; break;
- case 79: s = "+ expected"; break;
- case 80: s = "- expected"; break;
- case 81: s = "/ expected"; break;
- case 82: s = "% expected"; break;
- case 83: s = "! expected"; break;
- case 84: s = "\\u00ac expected"; break;
- case 85: s = "false expected"; break;
- case 86: s = "true expected"; break;
- case 87: s = "null expected"; break;
- case 88: s = "# expected"; break;
- case 89: s = ". expected"; break;
- case 90: s = "fresh expected"; break;
- case 91: s = ".. expected"; break;
- case 92: s = "this expected"; break;
- case 93: s = "old expected"; break;
- case 94: s = "forall expected"; break;
- case 95: s = "\\u2200 expected"; break;
- case 96: s = "exists expected"; break;
- case 97: s = "\\u2203 expected"; break;
- case 98: s = ":: expected"; break;
- case 99: s = "\\u2022 expected"; break;
+ case 4: s = "\"module\" expected"; break;
+ case 5: s = "\"imports\" expected"; break;
+ case 6: s = "\"{\" expected"; break;
+ case 7: s = "\"}\" expected"; break;
+ case 8: s = "\"class\" expected"; break;
+ case 9: s = "\"ghost\" expected"; break;
+ case 10: s = "\"static\" expected"; break;
+ case 11: s = "\"unlimited\" expected"; break;
+ case 12: s = "\"datatype\" expected"; break;
+ case 13: s = "\";\" expected"; break;
+ case 14: s = "\"var\" expected"; break;
+ case 15: s = "\",\" expected"; break;
+ case 16: s = "\":\" expected"; break;
+ case 17: s = "\"<\" expected"; break;
+ case 18: s = "\">\" expected"; break;
+ case 19: s = "\"method\" expected"; break;
+ case 20: s = "\"returns\" expected"; break;
+ case 21: s = "\"modifies\" expected"; break;
+ case 22: s = "\"free\" expected"; break;
+ case 23: s = "\"requires\" expected"; break;
+ case 24: s = "\"ensures\" expected"; break;
+ case 25: s = "\"decreases\" expected"; break;
+ case 26: s = "\"(\" expected"; break;
+ case 27: s = "\")\" expected"; break;
+ case 28: s = "\"bool\" expected"; break;
+ case 29: s = "\"int\" expected"; break;
+ case 30: s = "\"set\" expected"; break;
+ case 31: s = "\"seq\" expected"; break;
+ case 32: s = "\"object\" expected"; break;
+ case 33: s = "\"array\" expected"; break;
+ case 34: s = "\"function\" expected"; break;
+ case 35: s = "\"reads\" expected"; break;
+ case 36: s = "\"*\" expected"; break;
+ case 37: s = "\"`\" expected"; break;
+ case 38: s = "\"match\" expected"; break;
+ case 39: s = "\"case\" expected"; break;
+ case 40: s = "\"=>\" expected"; break;
+ case 41: s = "\"label\" expected"; break;
+ case 42: s = "\"break\" expected"; break;
+ case 43: s = "\"return\" expected"; break;
+ case 44: s = "\":=\" expected"; break;
+ case 45: s = "\"new\" expected"; break;
+ case 46: s = "\"[\" expected"; break;
+ case 47: s = "\"]\" expected"; break;
+ case 48: s = "\"havoc\" expected"; break;
+ case 49: s = "\"if\" expected"; break;
+ case 50: s = "\"else\" expected"; break;
+ case 51: s = "\"while\" expected"; break;
+ case 52: s = "\"invariant\" expected"; break;
+ case 53: s = "\"call\" expected"; break;
+ case 54: s = "\"foreach\" expected"; break;
+ case 55: s = "\"in\" expected"; break;
+ case 56: s = "\"|\" expected"; break;
+ case 57: s = "\"assert\" expected"; break;
+ case 58: s = "\"assume\" expected"; break;
+ case 59: s = "\"use\" expected"; break;
+ case 60: s = "\"print\" expected"; break;
+ case 61: s = "\"then\" expected"; break;
+ case 62: s = "\"<==>\" expected"; break;
+ case 63: s = "\"\\u21d4\" expected"; break;
+ case 64: s = "\"==>\" expected"; break;
+ case 65: s = "\"\\u21d2\" expected"; break;
+ case 66: s = "\"&&\" expected"; break;
+ case 67: s = "\"\\u2227\" expected"; break;
+ case 68: s = "\"||\" expected"; break;
+ case 69: s = "\"\\u2228\" expected"; break;
+ case 70: s = "\"==\" expected"; break;
+ case 71: s = "\"<=\" expected"; break;
+ case 72: s = "\">=\" expected"; break;
+ case 73: s = "\"!=\" expected"; break;
+ case 74: s = "\"!!\" expected"; break;
+ case 75: s = "\"!in\" expected"; break;
+ case 76: s = "\"\\u2260\" expected"; break;
+ case 77: s = "\"\\u2264\" expected"; break;
+ case 78: s = "\"\\u2265\" expected"; break;
+ case 79: s = "\"+\" expected"; break;
+ case 80: s = "\"-\" expected"; break;
+ case 81: s = "\"/\" expected"; break;
+ case 82: s = "\"%\" expected"; break;
+ case 83: s = "\"!\" expected"; break;
+ case 84: s = "\"\\u00ac\" expected"; break;
+ case 85: s = "\"false\" expected"; break;
+ case 86: s = "\"true\" expected"; break;
+ case 87: s = "\"null\" expected"; break;
+ case 88: s = "\"#\" expected"; break;
+ case 89: s = "\".\" expected"; break;
+ case 90: s = "\"fresh\" expected"; break;
+ case 91: s = "\"..\" expected"; break;
+ case 92: s = "\"this\" expected"; break;
+ case 93: s = "\"old\" expected"; break;
+ case 94: s = "\"forall\" expected"; break;
+ case 95: s = "\"\\u2200\" expected"; break;
+ case 96: s = "\"exists\" expected"; break;
+ case 97: s = "\"\\u2203\" expected"; break;
+ case 98: s = "\"::\" expected"; break;
+ case 99: s = "\"\\u2022\" expected"; break;
case 100: s = "??? expected"; break;
case 101: s = "invalid ClassMemberDecl"; break;
case 102: s = "invalid FunctionDecl"; break;
@@ -2017,33 +2078,42 @@ List<Expression!>! decreases) { default: s = "error " + n; break;
}
- System.Console.WriteLine(s);
- }
-
- static 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, T,x,x,x, T,T,T,T, T,x,T,x, x,x,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,T,x, x,x,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,T, x,T,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,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, 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,T,T,x, x,x,T,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,T,x, x,T,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,x,x,T, T,T,T,T, T,x,T,x, T,T,x,x, x,x,x,x, x,x},
- {x,T,x,x, x,x,T,x, x,T,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, x,x,x,x, T,T,x,T, x,T,T,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, T,T,x,x, x,x,x,x, x,x},
- {x,T,T,x, x,x,T,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,T,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, T,x,T,x, T,T,x,x, x,x,x,x, x,x},
- {x,T,T,x, x,x,T,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, T,x,x,x, x,x,x,x, x,x,T,x, x,T,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,x,x,T, T,T,T,T, T,x,T,x, T,T,x,x, x,x,x,x, x,x},
- {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, x,x,x,x, T,T,x,T, x,T,T,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, T,T,x,x, x,x,x,x, x,x},
- {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,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,T, x,x,x,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,T,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,T,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,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,T,T, T,T,x,x, x,x},
- {x,T,T,T, x,x,T,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,T,x, x,T,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,x,x,T, T,T,T,T, T,x,T,x, T,T,x,x, x,x,x,x, x,x}
+ //errorStream.WriteLine(errMsgFormat, line, col, s);
+ errorStream.WriteLine(s);
+ count++;
+ }
- };
+ public void SemErr (int line, int col, string! s) {
+ errorStream.WriteLine(errMsgFormat, line, col, s);
+ count++;
+ }
- [Microsoft.Contracts.Verify(false)]
- static Parser() {}
-} // end Parser
+ public void SemErr (string filename, int line, int col, string! s) {
+ errorStream.WriteLine(errMsgFormat4, filename, line, col, s);
+ count++;
+ }
+
+ public void SemErr (string s) {
+ errorStream.WriteLine(s);
+ count++;
+ }
+
+ public void SemErr(IToken! tok, string! msg) { // semantic errors
+ SemErr(tok.filename, tok.line, tok.col, msg);
+ }
+
+ public void Warning (int line, int col, string s) {
+ errorStream.WriteLine(errMsgFormat, line, col, s);
+ }
+
+ public void Warning(string s) {
+ errorStream.WriteLine(s);
+ }
+} // Errors
+
+
+public class FatalError: Exception {
+ public FatalError(string m): base(m) {}
+}
-} // end namespace
+}
\ No newline at end of file diff --git a/Dafny/Resolver.ssc b/Dafny/Resolver.ssc index 671469f3..701668db 100644 --- a/Dafny/Resolver.ssc +++ b/Dafny/Resolver.ssc @@ -7,11 +7,12 @@ using System; using System.Collections.Generic;
using System.Numerics;
using Microsoft.Contracts;
+using Microsoft.Boogie;
namespace Microsoft.Dafny {
public class Resolver {
public int ErrorCount = 0;
- void Error(Token! tok, string! msg, params object[] args) {
+ void Error(IToken! tok, string! msg, params object[] args) {
ConsoleColor col = Console.ForegroundColor;
Console.ForegroundColor = ConsoleColor.Red;
Console.WriteLine("{0}({1},{2}): Error: {3}",
@@ -1370,7 +1371,7 @@ namespace Microsoft.Dafny { return rr.EType;
}
- MemberDecl ResolveMember(Token! tok, Type! receiverType, string! memberName, out UserDefinedType ctype)
+ MemberDecl ResolveMember(IToken! tok, Type! receiverType, string! memberName, out UserDefinedType ctype)
ensures result != null ==> ctype != null && ctype.ResolvedClass != null;
{
ctype = UserDefinedType.DenotesClass(receiverType);
@@ -1455,7 +1456,7 @@ namespace Microsoft.Dafny { }
}
- public static UserDefinedType! GetThisType(Token! tok, ClassDecl! cl) {
+ public static UserDefinedType! GetThisType(IToken! tok, ClassDecl! cl) {
List<Type!> args = new List<Type!>();
foreach (TypeParameter tp in cl.TypeArgs) {
args.Add(new UserDefinedType(tok, tp.Name, tp));
diff --git a/Dafny/Scanner.ssc b/Dafny/Scanner.ssc index 5fdeefed..98114e54 100644 --- a/Dafny/Scanner.ssc +++ b/Dafny/Scanner.ssc @@ -1,248 +1,437 @@ +
+using System;
using System.IO;
using System.Collections;
using System.Collections.Generic;
using System.Text;
using Microsoft.Contracts;
-using Bpl = Microsoft.Boogie;
+using Microsoft.Boogie;
using BoogiePL;
+namespace Microsoft.Dafny {
-namespace Microsoft.Dafny {
+//-----------------------------------------------------------------------------------
+// Buffer
+//-----------------------------------------------------------------------------------
+public class Buffer {
+ // This Buffer supports the following cases:
+ // 1) seekable stream (file)
+ // 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
+ byte[]! buf; // input buffer
+ int bufStart; // position of first byte in buffer relative to input stream
+ int bufLen; // length of buffer
+ int fileLen; // length of input stream (may change if the stream is no file)
+ int bufPos; // current position in buffer
+ Stream! stream; // input stream (seekable)
+ bool isUserStream; // was the stream opened by the user?
+
+ [NotDelayed]
+ public Buffer (Stream! s, bool isUserStream) {
+ stream = s; this.isUserStream = isUserStream;
+
+ int fl, bl;
+ if (s.CanSeek) {
+ fl = (int) s.Length;
+ bl = fl < MAX_BUFFER_LENGTH ? fl : MAX_BUFFER_LENGTH; // Math.Min(fileLen, MAX_BUFFER_LENGTH);
+ bufStart = Int32.MaxValue; // nothing in the buffer so far
+ } else {
+ fl = bl = bufStart = 0;
+ }
+
+ buf = new byte[(bl>0) ? bl : MIN_BUFFER_LENGTH];
+ fileLen = fl; bufLen = bl;
+ base();
+ 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
+ buf = b.buf;
+ bufStart = b.bufStart;
+ bufLen = b.bufLen;
+ fileLen = b.fileLen;
+ bufPos = b.bufPos;
+ stream = b.stream;
+ // keep destructor from closing the stream
+ //b.stream = null;
+ isUserStream = b.isUserStream;
+ // keep destructor from closing the stream
+ b.isUserStream = true;
+ }
+
+ ~Buffer() { Close(); }
+
+ protected void Close() {
+ if (!isUserStream && stream != null) {
+ stream.Close();
+ //stream = null;
+ }
+ }
+
+ public virtual int Read () {
+ if (bufPos < bufLen) {
+ return buf[bufPos++];
+ } else if (Pos < fileLen) {
+ Pos = Pos; // shift buffer start to Pos
+ return buf[bufPos++];
+ } else if (stream != null && !stream.CanSeek && ReadNextStreamChunk() > 0) {
+ return buf[bufPos++];
+ } else {
+ return EOF;
+ }
+ }
+
+ public int Peek () {
+ int curPos = Pos;
+ int ch = Read();
+ Pos = curPos;
+ return ch;
+ }
+
+ public string! GetString (int beg, int end) {
+ int len = 0;
+ char[] buf = new char[end - beg];
+ int oldPos = Pos;
+ Pos = beg;
+ while (Pos < end) buf[len++] = (char) Read();
+ Pos = oldPos;
+ return new String(buf, 0, len);
+ }
+
+ public int Pos {
+ get { return bufPos + bufStart; }
+ set {
+ if (value >= fileLen && stream != null && !stream.CanSeek) {
+ // Wanted position is after buffer and the stream
+ // is not seek-able e.g. network or console,
+ // thus we have to read the stream manually till
+ // the wanted position is in sight.
+ while (value >= fileLen && ReadNextStreamChunk() > 0);
+ }
- [Immutable]
- public class Token : Bpl.Token {
- public Token();
- public Token(int linenum, int colnum) {
- base(linenum, colnum);
- }
- public new static Token! NoToken = new Token();
- }
+ if (value < 0 || value > fileLen) {
+ throw new FatalError("buffer out of bounds access, position: " + value);
+ }
+ if (value >= bufStart && value < bufStart + bufLen) { // already in buffer
+ bufPos = value - bufStart;
+ } else if (stream != null) { // must be swapped in
+ stream.Seek(value, SeekOrigin.Begin);
+ bufLen = stream.Read(buf, 0, buf.Length);
+ bufStart = value; bufPos = 0;
+ } else {
+ // set the position to the end of the file, Pos will return fileLen.
+ bufPos = fileLen - bufStart;
+ }
+ }
+ }
+
+ // 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.
+ private int ReadNextStreamChunk() {
+ int free = buf.Length - bufLen;
+ if (free == 0) {
+ // in the case of a growing input stream
+ // we can neither seek in the stream, nor can we
+ // foresee the maximum length, thus we must adapt
+ // the buffer size on demand.
+ byte[] newBuf = new byte[bufLen * 2];
+ Array.Copy(buf, newBuf, bufLen);
+ buf = newBuf;
+ free = bufLen;
+ }
+ int read = stream.Read(buf, bufLen, free);
+ if (read > 0) {
+ fileLen = bufLen = (bufLen + read);
+ return read;
+ }
+ // end of stream reached
+ return 0;
+ }
}
-namespace Microsoft.Dafny {
+//-----------------------------------------------------------------------------------
+// UTF8Buffer
+//-----------------------------------------------------------------------------------
+public class UTF8Buffer: Buffer {
+ public UTF8Buffer(Buffer! b): base(b) {}
+ public override int Read() {
+ int ch;
+ do {
+ ch = base.Read();
+ // until we find a utf8 start (0xxxxxxx or 11xxxxxx)
+ } while ((ch >= 128) && ((ch & 0xC0) != 0xC0) && (ch != EOF));
+ if (ch < 128 || ch == EOF) {
+ // nothing to do, first 127 chars are the same in ascii and utf8
+ // 0xxxxxxx or end of file character
+ } else if ((ch & 0xF0) == 0xF0) {
+ // 11110xxx 10xxxxxx 10xxxxxx 10xxxxxx
+ int c1 = ch & 0x07; ch = base.Read();
+ int c2 = ch & 0x3F; ch = base.Read();
+ int c3 = ch & 0x3F; ch = base.Read();
+ int c4 = ch & 0x3F;
+ ch = (((((c1 << 6) | c2) << 6) | c3) << 6) | c4;
+ } else if ((ch & 0xE0) == 0xE0) {
+ // 1110xxxx 10xxxxxx 10xxxxxx
+ int c1 = ch & 0x0F; ch = base.Read();
+ int c2 = ch & 0x3F; ch = base.Read();
+ int c3 = ch & 0x3F;
+ ch = (((c1 << 6) | c2) << 6) | c3;
+ } else if ((ch & 0xC0) == 0xC0) {
+ // 110xxxxx 10xxxxxx
+ int c1 = ch & 0x1F; ch = base.Read();
+ int c2 = ch & 0x3F;
+ ch = (c1 << 6) | c2;
+ }
+ return ch;
+ }
+}
+//-----------------------------------------------------------------------------------
+// Scanner
+//-----------------------------------------------------------------------------------
public class Scanner {
- const char EOF = '\0';
- const char CR = '\r';
- const char LF = '\n';
+ const char EOL = '\n';
+ const int eofSym = 0; /* pdt */
+ const int maxT = 100;
+ const int noSym = 100;
+
+
+ public Buffer! buffer; // scanner buffer
+
+ Token! t; // current token
+ int ch; // current input character
+ int pos; // byte position of current character
+ int col; // column number of current character
+ int line; // line number of current character
+ int oldEols; // EOLs that appeared in a comment;
+ static readonly Hashtable! start; // maps first token character to start state
- [Microsoft.Contracts.Verify(false)]
+ 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[0] = 55;
- start[33] = 35;
- start[34] = 3;
- start[35] = 48;
- start[37] = 46;
- start[38] = 29;
- start[39] = 1;
- start[40] = 12;
- start[41] = 13;
- start[42] = 14;
- start[43] = 43;
- start[44] = 8;
- start[45] = 44;
- start[46] = 49;
- start[47] = 45;
- start[48] = 2;
- start[49] = 2;
- start[50] = 2;
- start[51] = 2;
- start[52] = 2;
- start[53] = 2;
- start[54] = 2;
- start[55] = 2;
- start[56] = 2;
- start[57] = 2;
- start[58] = 9;
- start[59] = 7;
- start[60] = 10;
- start[61] = 16;
- start[62] = 11;
- start[63] = 1;
- start[65] = 1;
- start[66] = 1;
- start[67] = 1;
- start[68] = 1;
- start[69] = 1;
- start[70] = 1;
- start[71] = 1;
- start[72] = 1;
- start[73] = 1;
- start[74] = 1;
- start[75] = 1;
- start[76] = 1;
- start[77] = 1;
- start[78] = 1;
- start[79] = 1;
- start[80] = 1;
- start[81] = 1;
- start[82] = 1;
- start[83] = 1;
- start[84] = 1;
- start[85] = 1;
- start[86] = 1;
- start[87] = 1;
- start[88] = 1;
- start[89] = 1;
- start[90] = 1;
- start[91] = 19;
- start[92] = 1;
- start[93] = 20;
- start[95] = 1;
- start[96] = 15;
- start[97] = 1;
- start[98] = 1;
- start[99] = 1;
- start[100] = 1;
- start[101] = 1;
- start[102] = 1;
- start[103] = 1;
- start[104] = 1;
- start[105] = 1;
- start[106] = 1;
- start[107] = 1;
- start[108] = 1;
- start[109] = 1;
- start[110] = 1;
- start[111] = 1;
- start[112] = 1;
- start[113] = 1;
- start[114] = 1;
- start[115] = 1;
- start[116] = 1;
- start[117] = 1;
- start[118] = 1;
- start[119] = 1;
- start[120] = 1;
- start[121] = 1;
- start[122] = 1;
- start[123] = 5;
- start[124] = 21;
- start[125] = 6;
- start[172] = 47;
- start[8226] = 54;
- start[8658] = 28;
- start[8660] = 25;
- start[8704] = 51;
- start[8707] = 52;
- start[8743] = 31;
- start[8744] = 33;
- start[8800] = 40;
- start[8804] = 41;
- start[8805] = 42;
+ start = new Hashtable(128);
+ for (int i = 39; i <= 39; ++i) start[i] = 1;
+ for (int i = 63; i <= 63; ++i) start[i] = 1;
+ for (int i = 65; i <= 90; ++i) start[i] = 1;
+ for (int i = 92; i <= 92; ++i) start[i] = 1;
+ for (int i = 95; i <= 95; ++i) start[i] = 1;
+ 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[Buffer.EOF] = -1;
+
}
- const int noSym = 100;
- static short[] start = new short[16385];
-
-
-
- static Token/*!*/ t; // current token
- static char ch; // current input character
- static int pos; // column number of current character
- static int line; // line number of current character
- static int lineStart; // start position of current line
- static Queue! oldEols; // EOLs that appeared in a comment;
- static BitArray/*!*/ ignore; // set of characters to be ignored by the scanner
- static string Filename;
-
- ///<summary>
- ///Initializes the scanner. Note: first fill the Buffer.
- ///</summary>
- ///<param name="filename">File name used for error reporting</param>
- public static void Init (string filename) {
- Filename = filename;
- pos = -1; line = 1; lineStart = 0;
- oldEols = new Queue();
- NextCh();
- ignore = new BitArray(16384);
- ignore[9] = true; ignore[10] = true; ignore[13] = true; ignore[32] = true;
-
- }
-
- private static void NextCh() {
- if (oldEols.Count > 0) {
- ch = (char) ((!)oldEols.Dequeue());
- } else {
- while (true) {
- ch = (char)BoogiePL.Buffer.Read(); pos++;
- if (ch == BoogiePL.Buffer.eof) {
- ch = EOF;
- } else if (ch == LF) {
- line++;
- lineStart = pos + 1;
-
- } else if (ch == '#' && pos == lineStart) {
- int prLine = line;
- int prColumn = pos - lineStart; // which is 0
-
- string hashLine = BoogiePL.Buffer.ReadToEOL(); pos += hashLine.Length;
- line++;
- lineStart = pos + 1;
-
- hashLine = hashLine.TrimEnd(null);
- if (hashLine.StartsWith("line ") || hashLine == "line") {
- // parse #line pragma: #line num [filename]
- string h = hashLine.Substring(4).TrimStart(null);
- int x = h.IndexOf(' ');
- if (x == -1) {
- x = h.Length; // this will be convenient below when we look for a filename
- }
- try {
- int li = int.Parse(h.Substring(0, x));
-
- h = h.Substring(x).Trim();
-
- // act on #line
- line = li;
- if (h.Length != 0) {
- // a filename was specified
- Filename = h;
- }
- continue; // successfully parsed and acted on the #line pragma
-
- } catch (System.FormatException) {
- // just fall down through to produce an error message
- }
- Errors.SemErr(Filename, prLine, prColumn, "Malformed (#line num [filename]) pragma: #" + hashLine);
- continue;
- }
-
- Errors.SemErr(Filename, prLine, prColumn, "Unrecognized pragma: #" + hashLine);
- continue;
- }
- return;
- }
- }
- }
-
- - static bool Comment0() {
- int level = 1, line0 = line, lineStart0 = lineStart;
+
+ [NotDelayed]
+ public Scanner (string! fileName, Errors! errorHandler) {
+ this.errorHandler = errorHandler;
+ pt = tokens = new Token(); // first token is a dummy
+ t = new Token(); // dummy because t is a non-null field
+ try {
+ Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read);
+ buffer = new Buffer(stream, false);
+ Filename = fileName;
+ base();
+ Init();
+ } catch (IOException) {
+ throw new FatalError("Cannot open file " + fileName);
+ }
+ }
+
+ [NotDelayed]
+ public Scanner (Stream! s, Errors! errorHandler, string! fileName) {
+ pt = tokens = new Token(); // first token is a dummy
+ t = new Token(); // dummy because t is a non-null field
+ buffer = new Buffer(s, true);
+ this.errorHandler = errorHandler;
+ this.Filename = fileName;
+ base();
+ Init();
+ }
+
+ void Init() {
+ pos = -1; line = 1; col = 0;
+ oldEols = 0;
+ NextCh();
+ if (ch == 0xEF) { // check optional byte order mark for UTF-8
+ NextCh(); int ch1 = ch;
+ NextCh(); int ch2 = ch;
+ if (ch1 != 0xBB || ch2 != 0xBF) {
+ throw new FatalError(String.Format("illegal byte order mark: EF {0,2:X} {1,2:X}", ch1, ch2));
+ }
+ buffer = new UTF8Buffer(buffer); col = 0;
+ NextCh();
+ }
+ pt = tokens = new Token(); // first token is a dummy
+ }
+
+ string! ReadToEOL(){
+ int p = buffer.Pos;
+ int 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;
+ while (ch != EOL && ch != Buffer.EOF){
+ 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;
+ }
+ string! s = buffer.GetString(p, buffer.Pos);
+ return s;
+ }
+
+ void NextCh() {
+ if (oldEols > 0) { ch = EOL; oldEols--; }
+ else {
+// pos = buffer.Pos;
+// ch = buffer.Read(); col++;
+// // 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;
+// if (ch == EOL) { line++; col = 0; }
+
+ while (true) {
+ pos = buffer.Pos;
+ ch = buffer.Read(); col++;
+ // 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;
+ if (ch == EOL) {
+ line++; col = 0;
+ } else if (ch == '#' && col == 1) {
+ int prLine = line;
+ int prColumn = 0;
+
+ string! hashLine = ReadToEOL();
+ col = 0;
+ line++;
+
+ hashLine = hashLine.TrimEnd(null);
+ if (hashLine.StartsWith("line ") || hashLine == "line") {
+ // parse #line pragma: #line num [filename]
+ string h = hashLine.Substring(4).TrimStart(null);
+ int x = h.IndexOf(' ');
+ if (x == -1) {
+ x = h.Length; // this will be convenient below when we look for a filename
+ }
+ try {
+ int li = int.Parse(h.Substring(0, x));
+
+ h = h.Substring(x).Trim();
+
+ // act on #line
+ line = li;
+ if (h.Length != 0) {
+ // a filename was specified
+ Filename = h;
+ }
+ continue; // successfully parsed and acted on the #line pragma
+
+ } catch (FormatException) {
+ // just fall down through to produce an error message
+ }
+ this.errorHandler.SemErr(Filename, prLine, prColumn, "Malformed (#line num [filename]) pragma: #" + hashLine);
+ continue;
+ }
+
+ this.errorHandler.SemErr(Filename, prLine, prColumn, "Unrecognized pragma: #" + hashLine);
+ continue;
+ }
+ return;
+ }
+
+
+ }
+
+ }
+
+ void AddCh() {
+ if (tlen >= tval.Length) {
+ char[] newBuf = new char[2 * tval.Length];
+ Array.Copy(tval, 0, newBuf, 0, tval.Length);
+ tval = newBuf;
+ }
+ if (ch != Buffer.EOF) {
+ tval[tlen++] = (char) ch;
+ NextCh();
+ }
+ }
+
+
+
+ bool Comment0() {
+ int level = 1, pos0 = pos, line0 = line, col0 = col;
NextCh();
if (ch == '/') {
NextCh();
for(;;) {
if (ch == 10) {
level--;
- if (level == 0) {
- while(line0 < line) {oldEols.Enqueue('\r'); oldEols.Enqueue('\n'); line0++;}
- NextCh(); return true;
- }
+ if (level == 0) { oldEols = line - line0; NextCh(); return true; }
NextCh();
- } else if (ch == EOF) return false;
+ } else if (ch == Buffer.EOF) return false;
else NextCh();
}
} else {
- if (ch==CR) {line--; lineStart = lineStart0;}
- pos = pos - 2; Buffer.Pos = pos+1; NextCh();
+ buffer.Pos = pos0; NextCh(); line = line0; col = col0;
}
return false;
}
- - static bool Comment1() {
- int level = 1, line0 = line, lineStart0 = lineStart;
+
+ bool Comment1() {
+ int level = 1, pos0 = pos, line0 = line, col0 = col;
NextCh();
if (ch == '*') {
NextCh();
@@ -251,10 +440,7 @@ public class Scanner { NextCh();
if (ch == '/') {
level--;
- if (level == 0) {
- while(line0 < line) {oldEols.Enqueue('\r'); oldEols.Enqueue('\n'); line0++;}
- NextCh(); return true;
- }
+ if (level == 0) { oldEols = line - line0; NextCh(); return true; }
NextCh();
}
} else if (ch == '/') {
@@ -262,19 +448,18 @@ public class Scanner { if (ch == '*') {
level++; NextCh();
}
- } else if (ch == EOF) return false;
+ } else if (ch == Buffer.EOF) return false;
else NextCh();
}
} else {
- if (ch==CR) {line--; lineStart = lineStart0;}
- pos = pos - 2; Buffer.Pos = pos+1; NextCh();
+ buffer.Pos = pos0; NextCh(); line = line0; col = col0;
}
return false;
}
-
- static void CheckLiteral() {
- switch (t.val) {
+
+ void CheckLiteral() {
+ switch (t.val) {
case "module": t.kind = 4; break;
case "imports": t.kind = 5; break;
case "class": t.kind = 8; break;
@@ -326,185 +511,212 @@ public class Scanner { case "forall": t.kind = 94; break;
case "exists": t.kind = 96; break;
default: break;
+ }
+ }
- }
- }
-
- public static Token/*!*/ Scan() {
- while (ignore[ch]) { NextCh(); }
- if (ch == '/' && Comment0() || ch == '/' && Comment1() ) return Scan();
- t = new Token();
- t.pos = pos; t.col = pos - lineStart + 1; t.line = line; t.filename = Filename;
- int state = (/*^ (!) ^*/ start)[ch];
- StringBuilder buf = new StringBuilder(16);
- buf.Append(ch); NextCh();
-
- switch (state) {
- case 0: {t.kind = noSym; goto done;} // NextCh already done
+ Token! NextToken() {
+ while (ch == ' ' ||
+ ch >= 9 && ch <= 10 || ch == 13
+ ) NextCh();
+ if (ch == '/' && Comment0() ||ch == '/' && Comment1()) return NextToken();
+ int recKind = noSym;
+ int recEnd = pos;
+ t = new Token();
+ t.pos = pos; t.col = col; t.line = line;
+ t.filename = this.Filename;
+ int state;
+ if (start.ContainsKey(ch)) { state = (int) (!) start[ch]; }
+ else { state = 0; }
+ tlen = 0; AddCh();
+
+ switch (state) {
+ case -1: { t.kind = eofSym; break; } // NextCh already done
+ case 0: {
+ if (recKind != noSym) {
+ tlen = recEnd - t.pos;
+ SetScannerBehindT();
+ }
+ t.kind = recKind; break;
+ } // NextCh already done
case 1:
- if ((ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'z')) {buf.Append(ch); NextCh(); goto case 1;}
- else {t.kind = 1; t.val = buf.ToString(); CheckLiteral(); return t;}
+ recEnd = pos; recKind = 1;
+ if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 1;}
+ else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
case 2:
- if ((ch >= '0' && ch <= '9')) {buf.Append(ch); NextCh(); goto case 2;}
- else {t.kind = 2; goto done;}
+ recEnd = pos; recKind = 2;
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 2;}
+ else {t.kind = 2; break;}
case 3:
- if ((ch == '"')) {buf.Append(ch); NextCh(); goto case 4;}
- else if ((ch >= ' ' && ch <= '!' || ch >= '#' && ch <= '~')) {buf.Append(ch); NextCh(); goto case 3;}
- else {t.kind = noSym; goto done;}
+ if (ch == '"') {AddCh(); goto case 4;}
+ else if (ch >= ' ' && ch <= '!' || ch >= '#' && ch <= '~') {AddCh(); goto case 3;}
+ else {goto case 0;}
case 4:
- {t.kind = 3; goto done;}
+ {t.kind = 3; break;}
case 5:
- {t.kind = 6; goto done;}
+ {t.kind = 6; break;}
case 6:
- {t.kind = 7; goto done;}
+ {t.kind = 7; break;}
case 7:
- {t.kind = 13; goto done;}
+ {t.kind = 13; break;}
case 8:
- {t.kind = 15; goto done;}
+ {t.kind = 15; break;}
case 9:
- if (ch == '=') {buf.Append(ch); NextCh(); goto case 18;}
- else if (ch == ':') {buf.Append(ch); NextCh(); goto case 53;}
- else {t.kind = 16; goto done;}
+ {t.kind = 26; break;}
case 10:
- if (ch == '=') {buf.Append(ch); NextCh(); goto case 22;}
- else {t.kind = 17; goto done;}
+ {t.kind = 27; break;}
case 11:
- if (ch == '=') {buf.Append(ch); NextCh(); goto case 34;}
- else {t.kind = 18; goto done;}
+ {t.kind = 36; break;}
case 12:
- {t.kind = 26; goto done;}
+ {t.kind = 37; break;}
case 13:
- {t.kind = 27; goto done;}
+ {t.kind = 40; break;}
case 14:
- {t.kind = 36; goto done;}
+ {t.kind = 44; break;}
case 15:
- {t.kind = 37; goto done;}
+ {t.kind = 46; break;}
case 16:
- if (ch == '>') {buf.Append(ch); NextCh(); goto case 17;}
- else if (ch == '=') {buf.Append(ch); NextCh(); goto case 26;}
- else {t.kind = noSym; goto done;}
+ {t.kind = 47; break;}
case 17:
- {t.kind = 40; goto done;}
+ if (ch == '>') {AddCh(); goto case 18;}
+ else {goto case 0;}
case 18:
- {t.kind = 44; goto done;}
+ {t.kind = 62; break;}
case 19:
- {t.kind = 46; goto done;}
+ {t.kind = 63; break;}
case 20:
- {t.kind = 47; goto done;}
+ {t.kind = 64; break;}
case 21:
- if (ch == '|') {buf.Append(ch); NextCh(); goto case 32;}
- else {t.kind = 56; goto done;}
+ {t.kind = 65; break;}
case 22:
- if (ch == '=') {buf.Append(ch); NextCh(); goto case 23;}
- else {t.kind = 71; goto done;}
+ if (ch == '&') {AddCh(); goto case 23;}
+ else {goto case 0;}
case 23:
- if (ch == '>') {buf.Append(ch); NextCh(); goto case 24;}
- else {t.kind = noSym; goto done;}
+ {t.kind = 66; break;}
case 24:
- {t.kind = 62; goto done;}
+ {t.kind = 67; break;}
case 25:
- {t.kind = 63; goto done;}
+ {t.kind = 68; break;}
case 26:
- if (ch == '>') {buf.Append(ch); NextCh(); goto case 27;}
- else {t.kind = 70; goto done;}
+ {t.kind = 69; break;}
case 27:
- {t.kind = 64; goto done;}
+ {t.kind = 72; break;}
case 28:
- {t.kind = 65; goto done;}
+ {t.kind = 73; break;}
case 29:
- if (ch == '&') {buf.Append(ch); NextCh(); goto case 30;}
- else {t.kind = noSym; goto done;}
+ {t.kind = 74; break;}
case 30:
- {t.kind = 66; goto done;}
+ if (ch == 'n') {AddCh(); goto case 31;}
+ else {goto case 0;}
case 31:
- {t.kind = 67; goto done;}
+ {t.kind = 75; break;}
case 32:
- {t.kind = 68; goto done;}
+ {t.kind = 76; break;}
case 33:
- {t.kind = 69; goto done;}
+ {t.kind = 77; break;}
case 34:
- {t.kind = 72; goto done;}
+ {t.kind = 78; break;}
case 35:
- if (ch == '=') {buf.Append(ch); NextCh(); goto case 36;}
- else if (ch == '!') {buf.Append(ch); NextCh(); goto case 37;}
- else if (ch == 'i') {buf.Append(ch); NextCh(); goto case 38;}
- else {t.kind = 83; goto done;}
+ {t.kind = 79; break;}
case 36:
- {t.kind = 73; goto done;}
+ {t.kind = 80; break;}
case 37:
- {t.kind = 74; goto done;}
+ {t.kind = 81; break;}
case 38:
- if (ch == 'n') {buf.Append(ch); NextCh(); goto case 39;}
- else {t.kind = noSym; goto done;}
+ {t.kind = 82; break;}
case 39:
- {t.kind = 75; goto done;}
+ {t.kind = 84; break;}
case 40:
- {t.kind = 76; goto done;}
+ {t.kind = 88; break;}
case 41:
- {t.kind = 77; goto done;}
+ {t.kind = 91; break;}
case 42:
- {t.kind = 78; goto done;}
+ {t.kind = 95; break;}
case 43:
- {t.kind = 79; goto done;}
+ {t.kind = 97; break;}
case 44:
- {t.kind = 80; goto done;}
+ {t.kind = 98; break;}
case 45:
- {t.kind = 81; goto done;}
+ {t.kind = 99; break;}
case 46:
- {t.kind = 82; goto done;}
+ recEnd = pos; recKind = 16;
+ if (ch == '=') {AddCh(); goto case 14;}
+ else if (ch == ':') {AddCh(); goto case 44;}
+ else {t.kind = 16; break;}
case 47:
- {t.kind = 84; goto done;}
+ recEnd = pos; recKind = 17;
+ if (ch == '=') {AddCh(); goto case 53;}
+ else {t.kind = 17; break;}
case 48:
- {t.kind = 88; goto done;}
+ recEnd = pos; recKind = 18;
+ if (ch == '=') {AddCh(); goto case 27;}
+ else {t.kind = 18; break;}
case 49:
- if (ch == '.') {buf.Append(ch); NextCh(); goto case 50;}
- else {t.kind = 89; goto done;}
+ if (ch == '>') {AddCh(); goto case 13;}
+ else if (ch == '=') {AddCh(); goto case 54;}
+ else {goto case 0;}
case 50:
- {t.kind = 91; goto done;}
+ recEnd = pos; recKind = 56;
+ if (ch == '|') {AddCh(); goto case 25;}
+ else {t.kind = 56; break;}
case 51:
- {t.kind = 95; goto done;}
+ recEnd = pos; recKind = 83;
+ if (ch == '=') {AddCh(); goto case 28;}
+ else if (ch == '!') {AddCh(); goto case 29;}
+ else if (ch == 'i') {AddCh(); goto case 30;}
+ else {t.kind = 83; break;}
case 52:
- {t.kind = 97; goto done;}
+ recEnd = pos; recKind = 89;
+ if (ch == '.') {AddCh(); goto case 41;}
+ else {t.kind = 89; break;}
case 53:
- {t.kind = 98; goto done;}
+ recEnd = pos; recKind = 71;
+ if (ch == '=') {AddCh(); goto case 17;}
+ else {t.kind = 71; break;}
case 54:
- {t.kind = 99; goto done;}
- case 55: {t.kind = 0; goto done;}
- }
- done:
- t.val = buf.ToString();
- return t;
- }
+ recEnd = pos; recKind = 70;
+ if (ch == '>') {AddCh(); goto case 20;}
+ else {t.kind = 70; break;}
-} // end Scanner
+ }
+ 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 () {
+ if (tokens.next == null) {
+ return NextToken();
+ } else {
+ pt = tokens = tokens.next;
+ return tokens;
+ }
+ }
+ // peek for the next token, ignore pragmas
+ public Token! Peek () {
+ do {
+ if (pt.next == null) {
+ pt.next = NextToken();
+ }
+ pt = pt.next;
+ } while (pt.kind > maxT); // skip pragmas
+
+ return pt;
+ }
-public delegate void ErrorProc(int n, string filename, int line, int col);
+ // make sure that peeking starts at the current scan position
+ public void ResetPeek () { pt = tokens; }
-public class Errors {
- public static int count = 0; // number of errors detected
- public static ErrorProc/*!*/ SynErr; // syntactic errors
-
- public static void SemErr(string filename, int line, int col, string! msg) { // semantic errors
- System.ConsoleColor color = System.Console.ForegroundColor;
- System.Console.ForegroundColor = System.ConsoleColor.Red;
- System.Console.WriteLine("{0}({1},{2}): Error: {3}", filename, line, col, msg);
- System.Console.ForegroundColor = color;
- count++;
- }
-
- public static void SemErr(Bpl.IToken! tok, string! msg) { // semantic errors
- SemErr(tok.filename, tok.line, tok.col, msg);
- }
-
- public static void Exception (string s) {
- System.ConsoleColor color = System.Console.ForegroundColor;
- System.Console.ForegroundColor = System.ConsoleColor.Red;
- System.Console.WriteLine(s);
- System.Console.ForegroundColor = color;
- System.Environment.Exit(0);
- }
+} // end Scanner
+
+public delegate void ErrorProc(int n, string filename, int line, int col);
-} // Errors
-} // end namespace
+}
\ No newline at end of file diff --git a/Dafny/Translator.ssc b/Dafny/Translator.ssc index 348fdd2b..4d9f3993 100644 --- a/Dafny/Translator.ssc +++ b/Dafny/Translator.ssc @@ -9,6 +9,7 @@ using System.Numerics; using Microsoft.Contracts;
using Bpl = Microsoft.Boogie;
using System.Text;
+using Microsoft.Boogie;
namespace Microsoft.Dafny {
public class Translator {
@@ -31,9 +32,9 @@ namespace Microsoft.Dafny { // Machinery for providing information to the Counterexample Visualizer
readonly Dictionary<string!,int>! cevFilenames = new Dictionary<string!,int>();
- readonly Dictionary<Token!,Bpl.Constant!>! cevLocations = new Dictionary<Token!,Bpl.Constant!>();
+ readonly Dictionary<IToken!,Bpl.Constant!>! cevLocations = new Dictionary<IToken!,Bpl.Constant!>();
readonly Dictionary<string!,Bpl.Constant!>! cevVariables = new Dictionary<string!,Bpl.Constant!>();
- Bpl.Expr! CevLocation(Token! tok)
+ Bpl.Expr! CevLocation(IToken! tok)
requires predef != null && sink != null;
{
Bpl.Constant c;
@@ -89,15 +90,15 @@ namespace Microsoft.Dafny { public readonly Bpl.Type! CevVariableKind;
public readonly Bpl.Type! CevEventType;
private readonly Bpl.TypeSynonymDecl! setTypeCtor;
- public Bpl.Type! SetType(Token! tok, Bpl.Type! ty) {
+ public Bpl.Type! SetType(IToken! tok, Bpl.Type! ty) {
return new Bpl.TypeSynonymAnnotation(Token.NoToken, setTypeCtor, new Bpl.TypeSeq(ty));
}
private readonly Bpl.TypeCtorDecl! seqTypeCtor;
- public Bpl.Type! SeqType(Token! tok, Bpl.Type! ty) {
+ public Bpl.Type! SeqType(IToken! tok, Bpl.Type! ty) {
return new Bpl.CtorType(Token.NoToken, seqTypeCtor, new Bpl.TypeSeq(ty));
}
readonly Bpl.TypeCtorDecl! fieldName;
- public Bpl.Type! FieldName(Token! tok, Bpl.Type! ty) {
+ public Bpl.Type! FieldName(IToken! tok, Bpl.Type! ty) {
return new Bpl.CtorType(tok, fieldName, new Bpl.TypeSeq(ty));
}
public readonly Bpl.Type! HeapType;
@@ -109,7 +110,7 @@ namespace Microsoft.Dafny { public readonly Bpl.Type! DtCtorId;
public readonly Bpl.Expr! Null;
private readonly Bpl.Constant! allocField;
- public Bpl.IdentifierExpr! Alloc(Token! tok) {
+ public Bpl.IdentifierExpr! Alloc(IToken! tok) {
return new Bpl.IdentifierExpr(tok, allocField);
}
@@ -247,11 +248,20 @@ namespace Microsoft.Dafny { //using (System.IO.Stream stream = (!) System.Reflection.Assembly.GetExecutingAssembly().GetManifestResourceStream("DafnyPrelude.bpl")) // Use this once Spec#/VSIP supports designating a non-.resx project item as an embedded resource
string! codebase = (!) System.IO.Path.GetDirectoryName((!)System.Reflection.Assembly.GetExecutingAssembly().Location);
string! preludePath = System.IO.Path.Combine(codebase, "DafnyPrelude.bpl");
+
+ Bpl.Program prelude;
+ int errorCount = Bpl.Parser.Parse(preludePath, out prelude);
+ if (prelude == null || errorCount > 0) {
+ return null;
+ } else {
+ return prelude;
+ }
+/*
List<string!> defines = new List<string!>();
using (System.IO.Stream stream = new System.IO.FileStream(preludePath, System.IO.FileMode.Open, System.IO.FileAccess.Read))
{
BoogiePL.Buffer.Fill(new System.IO.StreamReader(stream), defines);
- BoogiePL.Scanner.Init("<DafnyPrelude.bpl>");
+ //BoogiePL.Scanner.Init("<DafnyPrelude.bpl>");
Bpl.Program prelude;
int errorCount = BoogiePL.Parser.Parse(out prelude);
if (prelude == null || errorCount > 0) {
@@ -260,6 +270,7 @@ namespace Microsoft.Dafny { return prelude;
}
}
+*/
}
public Bpl.Program! Translate(Program! program) {
@@ -660,7 +671,7 @@ namespace Microsoft.Dafny { }
}
- Bpl.Expr! InSeqRange(Token! tok, Bpl.Expr! index, Bpl.Expr! seq, bool isSequence, Bpl.Expr lowerBound, bool includeUpperBound) {
+ Bpl.Expr! InSeqRange(IToken! tok, Bpl.Expr! index, Bpl.Expr! seq, bool isSequence, Bpl.Expr lowerBound, bool includeUpperBound) {
if (lowerBound == null) {
lowerBound = Bpl.Expr.Literal(0);
}
@@ -679,7 +690,7 @@ namespace Microsoft.Dafny { int loopHeapVarCount = 0;
int otherTmpVarCount = 0;
Bpl.IdentifierExpr _phvie = null;
- Bpl.IdentifierExpr! GetPrevHeapVar_IdExpr(Token! tok, Bpl.VariableSeq! locals) // local variable that's shared between statements that need it
+ Bpl.IdentifierExpr! GetPrevHeapVar_IdExpr(IToken! tok, Bpl.VariableSeq! locals) // local variable that's shared between statements that need it
requires predef != null;
{
if (_phvie == null) {
@@ -691,7 +702,7 @@ namespace Microsoft.Dafny { return _phvie;
}
Bpl.IdentifierExpr _nwie = null;
- Bpl.IdentifierExpr! GetNewVar_IdExpr(Token! tok, Bpl.VariableSeq! locals) // local variable that's shared between statements that need it
+ Bpl.IdentifierExpr! GetNewVar_IdExpr(IToken! tok, Bpl.VariableSeq! locals) // local variable that's shared between statements that need it
requires predef != null;
{
if (_nwie == null) {
@@ -795,7 +806,7 @@ namespace Microsoft.Dafny { assert p != null;
builder.Add(new Bpl.CallCmd(p.tok, "CevVarIntro",
new Bpl.ExprSeq(
- CevLocation((Dafny.Token)p.tok),
+ CevLocation(p.tok),
new Bpl.IdentifierExpr(p.tok, "cev_parameter", predef.CevVariableKind),
CevVariable(p.tok, p.Name),
new Bpl.IdentifierExpr(p.tok, p.Name, p.TypedIdent.Type)), // it's important not to pass in just p, because that resolves to the proc's param, not the impl's param
@@ -805,7 +816,7 @@ namespace Microsoft.Dafny { assert p != null;
builder.Add(new Bpl.CallCmd(p.tok, "CevVarIntro",
new Bpl.ExprSeq(
- CevLocation((Dafny.Token)p.tok),
+ CevLocation(p.tok),
new Bpl.IdentifierExpr(p.tok, "cev_local", predef.CevVariableKind), // treat out-parameters as locals
CevVariable(p.tok, p.Name),
new Bpl.IdentifierExpr(p.tok, p.Name, p.TypedIdent.Type)), // it's important not to pass in just p, because that resolves to the proc's param, not the impl's param
@@ -816,7 +827,7 @@ namespace Microsoft.Dafny { DefineFrame(m.tok, m.Mod, builder, localVariables);
}
- void DefineFrame(Token! tok, List<FrameExpression!>! frameClause, Bpl.StmtListBuilder! builder, Bpl.VariableSeq! localVariables)
+ void DefineFrame(IToken! tok, List<FrameExpression!>! frameClause, Bpl.StmtListBuilder! builder, Bpl.VariableSeq! localVariables)
requires predef != null;
{
ExpressionTranslator etran = new ExpressionTranslator(this, predef, tok);
@@ -839,7 +850,7 @@ namespace Microsoft.Dafny { builder.Add(Bpl.Cmd.SimpleAssign(tok, new Bpl.IdentifierExpr(tok, frame), lambda));
}
- void CheckFrameSubset(Token! tok, List<FrameExpression!>! calleeFrame,
+ void CheckFrameSubset(IToken! tok, List<FrameExpression!>! calleeFrame,
Expression receiverReplacement, Dictionary<IVariable,Expression!> substMap,
ExpressionTranslator! etran, Bpl.StmtListBuilder! builder, string! errorMessage)
requires predef != null;
@@ -959,7 +970,7 @@ namespace Microsoft.Dafny { }
}
- Bpl.Expr! InRWClause(Token! tok, Bpl.Expr! o, Bpl.Expr! f, List<FrameExpression!>! rw, ExpressionTranslator! etran,
+ Bpl.Expr! InRWClause(IToken! tok, Bpl.Expr! o, Bpl.Expr! f, List<FrameExpression!>! rw, ExpressionTranslator! etran,
Expression receiverReplacement, Dictionary<IVariable,Expression!> substMap)
requires predef != null;
// requires o to denote an expression of type RefType
@@ -1225,7 +1236,7 @@ namespace Microsoft.Dafny { }
}
- void CheckNonNull(Token! tok, Expression! e, Bpl.StmtListBuilder! builder, ExpressionTranslator! etran)
+ void CheckNonNull(IToken! tok, Expression! e, Bpl.StmtListBuilder! builder, ExpressionTranslator! etran)
requires predef != null;
{
if (e is ThisExpr) {
@@ -1490,7 +1501,7 @@ namespace Microsoft.Dafny { return cc;
}
- Bpl.Expr GetTypeExpr(Token! tok, Type! type)
+ Bpl.Expr GetTypeExpr(IToken! tok, Type! type)
requires predef != null;
{
while (true) {
@@ -1706,13 +1717,13 @@ namespace Microsoft.Dafny { }
class BoilerplateTriple { // a triple that is now a quintuple
- public readonly Token! tok;
+ public readonly IToken! tok;
public readonly bool IsFree;
public readonly Bpl.Expr! Expr;
public readonly string ErrorMessage;
invariant IsFree || ErrorMessage != null;
public readonly string Comment;
- public BoilerplateTriple(Token! tok, bool isFree, Bpl.Expr! expr, string errorMessage, string comment)
+ public BoilerplateTriple(IToken! tok, bool isFree, Bpl.Expr! expr, string errorMessage, string comment)
requires isFree || errorMessage != null;
{
this.tok = tok;
@@ -1730,7 +1741,7 @@ namespace Microsoft.Dafny { /// S2. the post-state of the two-state interval
/// This method assumes that etranPre denotes S1, etran denotes S2, and that etran.Old denotes S0.
/// </summary>
- List<BoilerplateTriple!>! GetTwoStateBoilerplate(Token! tok, Method! method, ExpressionTranslator! etranPre, ExpressionTranslator! etran)
+ List<BoilerplateTriple!>! GetTwoStateBoilerplate(IToken! tok, Method! method, ExpressionTranslator! etranPre, ExpressionTranslator! etran)
{
List<BoilerplateTriple!> boilerplate = new List<BoilerplateTriple!>();
@@ -1751,7 +1762,7 @@ namespace Microsoft.Dafny { /// S2. the post-state of the two-state interval
/// This method assumes that etranPre denotes S1, etran denotes S2, and that etran.Old denotes S0.
/// </summary>
- Bpl.Expr! FrameCondition(Token! tok, List<FrameExpression!>! modifiesClause, ExpressionTranslator! etranPre, ExpressionTranslator! etran)
+ Bpl.Expr! FrameCondition(IToken! tok, List<FrameExpression!>! modifiesClause, ExpressionTranslator! etranPre, ExpressionTranslator! etran)
requires predef != null;
{
// generate:
@@ -1838,7 +1849,7 @@ namespace Microsoft.Dafny { return cmd;
}
- Bpl.Ensures! Ensures(Token! tok, bool free, Bpl.Expr! condition, string errorMessage, string comment)
+ Bpl.Ensures! Ensures(IToken! tok, bool free, Bpl.Expr! condition, string errorMessage, string comment)
{
Bpl.Ensures ens = new Bpl.Ensures(tok, free, condition, comment);
if (errorMessage != null) {
@@ -1847,7 +1858,7 @@ namespace Microsoft.Dafny { return ens;
}
- Bpl.Requires! Requires(Token! tok, bool free, Bpl.Expr! condition, string errorMessage, string comment)
+ Bpl.Requires! Requires(IToken! tok, bool free, Bpl.Expr! condition, string errorMessage, string comment)
{
Bpl.Requires req = new Bpl.Requires(tok, free, condition, comment);
if (errorMessage != null) {
@@ -2266,7 +2277,7 @@ namespace Microsoft.Dafny { // time for the actual loop body
TrStmt(s.Body, loopBodyBuilder, locals, etran);
// check definedness of decreases expressions
- List<Token!> toks = new List<Token!>();
+ List<IToken!> toks = new List<IToken!>();
List<Type!> types = new List<Type!>();
List<Bpl.Expr!> decrs = new List<Bpl.Expr!>();
foreach (Expression e in theDecreases) {
@@ -2457,7 +2468,7 @@ namespace Microsoft.Dafny { }
}
- static Expression! CreateIntLiteral(Token! tok, int n)
+ static Expression! CreateIntLiteral(IToken! tok, int n)
{
if (0 <= n) {
Expression lit = new LiteralExpr(tok, n);
@@ -2468,7 +2479,7 @@ namespace Microsoft.Dafny { }
}
- static Expression! CreateIntSub(Token! tok, Expression! e0, Expression! e1)
+ static Expression! CreateIntSub(IToken! tok, Expression! e0, Expression! e1)
requires e0.Type is IntType && e1.Type is IntType;
{
BinaryExpr s = new BinaryExpr(tok, BinaryExpr.Opcode.Sub, e0, e1);
@@ -2477,7 +2488,7 @@ namespace Microsoft.Dafny { return s;
}
- static Expression! CreateIntITE(Token! tok, Expression! test, Expression! e0, Expression! e1)
+ static Expression! CreateIntITE(IToken! tok, Expression! test, Expression! e0, Expression! e1)
requires test.Type is BoolType && e0.Type is IntType && e1.Type is IntType;
{
ITEExpr ite = new ITEExpr(tok, test, e0, e1);
@@ -2504,12 +2515,12 @@ namespace Microsoft.Dafny { yield return expr;
}
- void CheckCallTermination(Token! tok, List<Expression!>! contextDecreases, List<Expression!>! calleeDecreases,
+ void CheckCallTermination(IToken! tok, List<Expression!>! contextDecreases, List<Expression!>! calleeDecreases,
Expression receiverReplacement, Dictionary<IVariable,Expression!>! substMap,
ExpressionTranslator! etran, Bpl.StmtListBuilder! builder)
{
int N = min{contextDecreases.Count, calleeDecreases.Count};
- List<Token!> toks = new List<Token!>();
+ List<IToken!> toks = new List<IToken!>();
List<Type!> types = new List<Type!>();
List<Bpl.Expr!> callee = new List<Bpl.Expr!>();
List<Bpl.Expr!> caller = new List<Bpl.Expr!>();
@@ -2532,7 +2543,7 @@ namespace Microsoft.Dafny { /// Returns the expression that says whether or not the decreases function has gone down. ee0 represents the new
/// values and ee1 represents old values.
/// </summary>
- Bpl.Expr! DecreasesCheck(List<Token!>! toks, List<Type!>! types, List<Bpl.Expr!>! ee0, List<Bpl.Expr!>! ee1,
+ Bpl.Expr! DecreasesCheck(List<IToken!>! toks, List<Type!>! types, List<Bpl.Expr!>! ee0, List<Bpl.Expr!>! ee1,
Bpl.StmtListBuilder! builder, ExpressionTranslator! etran, string! suffixMsg)
requires predef != null;
requires types.Count == ee0.Count && ee0.Count == ee1.Count;
@@ -2605,7 +2616,7 @@ namespace Microsoft.Dafny { }
}
- void ComputeLessEq(Token! tok, Type! ty, Bpl.Expr! e0, Bpl.Expr! e1, out Bpl.Expr! less, out Bpl.Expr! eq, ExpressionTranslator! etran)
+ void ComputeLessEq(IToken! tok, Type! ty, Bpl.Expr! e0, Bpl.Expr! e1, out Bpl.Expr! less, out Bpl.Expr! eq, ExpressionTranslator! etran)
requires predef != null;
{
if (ty is BoolType) {
@@ -2641,7 +2652,7 @@ namespace Microsoft.Dafny { builder.Add(new Bpl.CommentCmd(string.Format("----- {0} ----- {1}({2},{3})", comment, stmt.Tok.filename, stmt.Tok.line, stmt.Tok.col)));
}
- Bpl.Expr GetWhereClause(Token! tok, Bpl.Expr! x, Type! type, ExpressionTranslator! etran)
+ Bpl.Expr GetWhereClause(IToken! tok, Bpl.Expr! x, Type! type, ExpressionTranslator! etran)
requires predef != null;
{
if (type is TypeProxy) {
@@ -2703,7 +2714,7 @@ namespace Microsoft.Dafny { }
}
- void TrAssignment(Token! tok, Expression! lhs, AssignmentRhs! rhs, Bpl.StmtListBuilder! builder, Bpl.VariableSeq! locals,
+ void TrAssignment(IToken! tok, Expression! lhs, AssignmentRhs! rhs, Bpl.StmtListBuilder! builder, Bpl.VariableSeq! locals,
ExpressionTranslator! etran)
requires predef != null;
{
@@ -2809,7 +2820,7 @@ namespace Microsoft.Dafny { }
}
- Bpl.AssumeCmd! AssumeGoodHeap(Token! tok, ExpressionTranslator! etran) {
+ Bpl.AssumeCmd! AssumeGoodHeap(IToken! tok, ExpressionTranslator! etran) {
return new Bpl.AssumeCmd(tok, FunctionCall(tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr));
}
@@ -2821,7 +2832,7 @@ namespace Microsoft.Dafny { public readonly Translator! translator;
readonly Function applyLimited_CurrentFunction;
- public ExpressionTranslator(Translator! translator, PredefinedDecls! predef, Token! heapToken) {
+ public ExpressionTranslator(Translator! translator, PredefinedDecls! predef, IToken! heapToken) {
this.translator = translator;
this.predef = predef;
HeapExpr = new Bpl.IdentifierExpr(heapToken, predef.HeapVarName, predef.HeapType);
@@ -2854,7 +2865,7 @@ namespace Microsoft.Dafny { return new ExpressionTranslator(translator, predef, HeapExpr, applyLimited_CurrentFunction);
}
- public Bpl.IdentifierExpr! TheFrame(Token! tok)
+ public Bpl.IdentifierExpr! TheFrame(IToken! tok)
ensures result.Type != null;
{
Bpl.TypeVariable alpha = new Bpl.TypeVariable(tok, "beta");
@@ -3211,12 +3222,12 @@ namespace Microsoft.Dafny { }
}
- public Bpl.Expr! ProperSubset(Token! tok, Bpl.Expr! e0, Bpl.Expr! e1) {
+ public Bpl.Expr! ProperSubset(IToken! tok, Bpl.Expr! e0, Bpl.Expr! e1) {
return Bpl.Expr.And(
translator.FunctionCall(tok, BuiltinFunction.SetSubset, null, e0, e1),
Bpl.Expr.Not(translator.FunctionCall(tok, BuiltinFunction.SetSubset, null, e1, e0)));
}
- public Bpl.Expr! ProperPrefix(Token! tok, Bpl.Expr! e0, Bpl.Expr! e1) {
+ public Bpl.Expr! ProperPrefix(IToken! tok, Bpl.Expr! e0, Bpl.Expr! e1) {
Bpl.Expr len0 = translator.FunctionCall(tok, BuiltinFunction.SeqLength, null, e0);
Bpl.Expr len1 = translator.FunctionCall(tok, BuiltinFunction.SeqLength, null, e1);
return Bpl.Expr.And(
@@ -3246,7 +3257,7 @@ namespace Microsoft.Dafny { return Bpl.Expr.Eq(f0, f1);
}
- public Bpl.Expr! CondApplyBox(Token! tok, Bpl.Expr! e, Type! fromType, Type! toType) {
+ public Bpl.Expr! CondApplyBox(IToken! tok, Bpl.Expr! e, Type! fromType, Type! toType) {
if (!ModeledAsBoxType(fromType) && ModeledAsBoxType(toType)) {
return translator.FunctionCall(tok, BuiltinFunction.Box, null, e);
} else {
@@ -3254,7 +3265,7 @@ namespace Microsoft.Dafny { }
}
- public Bpl.Expr! BoxIfNecessary(Token! tok, Bpl.Expr! e, Type! fromType) {
+ public Bpl.Expr! BoxIfNecessary(IToken! tok, Bpl.Expr! e, Type! fromType) {
if (!ModeledAsBoxType(fromType)) {
return translator.FunctionCall(tok, BuiltinFunction.Box, null, e);
} else {
@@ -3262,7 +3273,7 @@ namespace Microsoft.Dafny { }
}
- public Bpl.Expr! CondApplyUnbox(Token! tok, Bpl.Expr! e, Type! fromType, Type! toType) {
+ public Bpl.Expr! CondApplyUnbox(IToken! tok, Bpl.Expr! e, Type! fromType, Type! toType) {
if (ModeledAsBoxType(fromType) && !ModeledAsBoxType(toType)) {
return translator.FunctionCall(tok, BuiltinFunction.Unbox, translator.TrType(toType), e);
} else {
@@ -3285,7 +3296,7 @@ namespace Microsoft.Dafny { return t.IsTypeParameter;
}
- public Bpl.IdentifierExpr! TrVar(Token! tok, IVariable! var) {
+ public Bpl.IdentifierExpr! TrVar(IToken! tok, IVariable! var) {
return new Bpl.IdentifierExpr(tok, var.UniqueName, translator.TrType(var.Type));
}
@@ -3293,7 +3304,7 @@ namespace Microsoft.Dafny { /// Translate like s[Box(elmt)], but try to avoid as many set functions as possible in the
/// translation, because such functions can mess up triggering.
/// </summary>
- public Bpl.Expr! TrInSet(Token! tok, Bpl.Expr! elmt, Expression! s, Type! elmtType) {
+ public Bpl.Expr! TrInSet(IToken! tok, Bpl.Expr! elmt, Expression! s, Type! elmtType) {
if (s is BinaryExpr) {
BinaryExpr bin = (BinaryExpr)s;
switch (bin.ResolvedOp) {
@@ -3345,15 +3356,15 @@ namespace Microsoft.Dafny { // --------------- help routines ---------------
- public Bpl.Expr! IsAlloced(Token! tok, Bpl.Expr! e) {
+ public Bpl.Expr! IsAlloced(IToken! tok, Bpl.Expr! e) {
return IsAlloced(tok, e, HeapExpr);
}
- Bpl.Expr! IsAlloced(Token! tok, Bpl.Expr! e, Bpl.Expr! heap) {
+ Bpl.Expr! IsAlloced(IToken! tok, Bpl.Expr! e, Bpl.Expr! heap) {
return Bpl.Expr.SelectTok(tok, heap, e, predef.Alloc(tok));
}
- public Bpl.Expr! GoodRef(Token! tok, Bpl.Expr! e, Type! type) {
+ public Bpl.Expr! GoodRef(IToken! tok, Bpl.Expr! e, Type! type) {
Bpl.Expr goodRef;
if (type is UserDefinedType && ((UserDefinedType)type).ResolvedClass != null) {
// Heap[e, alloc] && dtype(e) == T
@@ -3364,13 +3375,13 @@ namespace Microsoft.Dafny { }
}
- public Bpl.Expr! GoodRef_Class(Token! tok, Bpl.Expr! e, UserDefinedType! type, bool isNew)
+ public Bpl.Expr! GoodRef_Class(IToken! tok, Bpl.Expr! e, UserDefinedType! type, bool isNew)
requires type.ResolvedClass is ClassDecl;
{
return GoodRef_Ref(tok, e, new Bpl.IdentifierExpr(tok, translator.GetClass(type.ResolvedClass)), type.TypeArgs, isNew);
}
- public Bpl.Expr! GoodRef_Ref(Token! tok, Bpl.Expr! e, Bpl.Expr! type, List<Type!>! typeArgs, bool isNew) {
+ public Bpl.Expr! GoodRef_Ref(IToken! tok, Bpl.Expr! e, Bpl.Expr! type, List<Type!>! typeArgs, bool isNew) {
// Heap[e, alloc]
Bpl.Expr r = IsAlloced(tok, e);
if (isNew) {
@@ -3396,7 +3407,7 @@ namespace Microsoft.Dafny { return r;
}
- public Bpl.Expr TypeAlloced(Token! tok, Bpl.Expr! e, Type! type) {
+ public Bpl.Expr TypeAlloced(IToken! tok, Bpl.Expr! e, Type! type) {
while (true) {
TypeProxy proxy = type as TypeProxy;
if (proxy == null) {
@@ -3493,7 +3504,7 @@ namespace Microsoft.Dafny { }
// The "typeInstantiation" argument is passed in to help construct the result type of the function.
- Bpl.NAryExpr! FunctionCall(Token! tok, BuiltinFunction f, Bpl.Type typeInstantiation, params Bpl.Expr[]! args)
+ Bpl.NAryExpr! FunctionCall(IToken! tok, BuiltinFunction f, Bpl.Type typeInstantiation, params Bpl.Expr[]! args)
requires predef != null;
{
switch (f) {
@@ -3667,12 +3678,12 @@ namespace Microsoft.Dafny { }
}
- Bpl.NAryExpr! FunctionCall(Token! tok, string! function, Bpl.Type! returnType, params Bpl.Expr[]! args)
+ Bpl.NAryExpr! FunctionCall(IToken! tok, string! function, Bpl.Type! returnType, params Bpl.Expr[]! args)
{
return new Bpl.NAryExpr(tok, new Bpl.FunctionCall(new Bpl.IdentifierExpr(tok, function, returnType)), new Bpl.ExprSeq(args));
}
- Bpl.NAryExpr! FunctionCall(Token! tok, string! function, Bpl.Type! returnType, List<Bpl.Expr!>! args)
+ Bpl.NAryExpr! FunctionCall(IToken! tok, string! function, Bpl.Type! returnType, List<Bpl.Expr!>! args)
{
Bpl.ExprSeq aa = new Bpl.ExprSeq();
foreach (Bpl.Expr arg in args) {
diff --git a/Dafny/parser.frame b/Dafny/parser.frame deleted file mode 100644 index de0ba1fb..00000000 --- a/Dafny/parser.frame +++ /dev/null @@ -1,103 +0,0 @@ -
-using Microsoft.Contracts;
-
-namespace Microsoft.-->namespace {
-
-public class Parser {
--->constants
- const bool T = true;
- const bool x = false;
- const int minErrDist = 2;
-
- static Token/*!*/ token; // last recognized token
- static Token/*!*/ t; // lookahead token
- static int errDist = minErrDist;
-
- -->declarations
-
- static void Error(int n) {
- if (errDist >= minErrDist) Errors.SynErr(n, t.filename, t.line, t.col);
- errDist = 0;
- }
-
- public static void SemErr(string! msg) {
- if (errDist >= minErrDist) Errors.SemErr(token.filename, token.line, token.col, msg);
- errDist = 0;
- }
-
- public static void SemErr(Token! tok, string! msg) {
- if (errDist >= minErrDist) Errors.SemErr(tok.filename, tok.line, tok.col, msg);
- errDist = 0;
- }
-
- static void Get() {
- for (;;) {
- token = t;
- t = Scanner.Scan();
- if (t.kind<=maxT) {errDist++; return;}
--->pragmas
- t = token;
- }
- }
-
- static void Expect(int n) {
- if (t.kind==n) Get(); else Error(n);
- }
-
- static bool StartOf(int s) {
- return set[s, t.kind];
- }
-
- static void ExpectWeak(int n, int follow) {
- if (t.kind == n) Get();
- else {
- Error(n);
- while (!StartOf(follow)) Get();
- }
- }
-
- static bool WeakSeparator(int n, int syFol, int repFol) {
- bool[] s = new bool[maxT+1];
- if (t.kind == n) {Get(); return true;}
- else if (StartOf(repFol)) return false;
- else {
- for (int i=0; i <= maxT; i++) {
- s[i] = set[syFol, i] || set[repFol, i] || set[0, i];
- }
- Error(n);
- while (!s[t.kind]) Get();
- return StartOf(syFol);
- }
- }
-
--->productions
-
- public static void Parse() {
- Errors.SynErr = new ErrorProc(SynErr);
- t = new Token();
- Get();
--->parseRoot
- }
-
- [Microsoft.Contracts.Verify(false)]
- static void SynErr(int n, string filename, int line, int col) {
- Errors.count++;
- System.Console.Write("{0}({1},{2}): syntax error: ", filename, line, col);
- string s;
- switch (n) {
--->errors
- default: s = "error " + n; break;
- }
- System.Console.WriteLine(s);
- }
-
- static bool[,]! set = {
--->initialization
- };
-
- [Microsoft.Contracts.Verify(false)]
- static Parser() {}
-} // end Parser
-
-} // end namespace
-$$$
\ No newline at end of file diff --git a/Dafny/scanner.frame b/Dafny/scanner.frame deleted file mode 100644 index a526c7f2..00000000 --- a/Dafny/scanner.frame +++ /dev/null @@ -1,170 +0,0 @@ -using System.IO;
-using System.Collections;
-using System.Collections.Generic;
-using System.Text;
-using Microsoft.Contracts;
-using Bpl = Microsoft.Boogie;
-using BoogiePL;
-
-
-namespace Microsoft.Dafny {
-
- [Immutable]
- public class Token : Bpl.Token {
- public Token();
- public Token(int linenum, int colnum) {
- base(linenum, colnum);
- }
- public new static Token! NoToken = new Token();
- }
-
-}
-
-namespace Microsoft.-->namespace {
-
-
-public class Scanner {
- const char EOF = '\0';
- const char CR = '\r';
- const char LF = '\n';
-
- [Microsoft.Contracts.Verify(false)]
--->declarations
-
-
- static Token/*!*/ t; // current token
- static char ch; // current input character
- static int pos; // column number of current character
- static int line; // line number of current character
- static int lineStart; // start position of current line
- static Queue! oldEols; // EOLs that appeared in a comment;
- static BitArray/*!*/ ignore; // set of characters to be ignored by the scanner
- static string Filename;
-
- ///<summary>
- ///Initializes the scanner. Note: first fill the Buffer.
- ///</summary>
- ///<param name="filename">File name used for error reporting</param>
- public static void Init (string filename) {
- Filename = filename;
- pos = -1; line = 1; lineStart = 0;
- oldEols = new Queue();
- NextCh();
--->initialization
- }
-
- private static void NextCh() {
- if (oldEols.Count > 0) {
- ch = (char) ((!)oldEols.Dequeue());
- } else {
- while (true) {
- ch = (char)BoogiePL.Buffer.Read(); pos++;
- if (ch == BoogiePL.Buffer.eof) {
- ch = EOF;
- } else if (ch == LF) {
- line++;
- lineStart = pos + 1;
-
- } else if (ch == '#' && pos == lineStart) {
- int prLine = line;
- int prColumn = pos - lineStart; // which is 0
-
- string hashLine = BoogiePL.Buffer.ReadToEOL(); pos += hashLine.Length;
- line++;
- lineStart = pos + 1;
-
- hashLine = hashLine.TrimEnd(null);
- if (hashLine.StartsWith("line ") || hashLine == "line") {
- // parse #line pragma: #line num [filename]
- string h = hashLine.Substring(4).TrimStart(null);
- int x = h.IndexOf(' ');
- if (x == -1) {
- x = h.Length; // this will be convenient below when we look for a filename
- }
- try {
- int li = int.Parse(h.Substring(0, x));
-
- h = h.Substring(x).Trim();
-
- // act on #line
- line = li;
- if (h.Length != 0) {
- // a filename was specified
- Filename = h;
- }
- continue; // successfully parsed and acted on the #line pragma
-
- } catch (System.FormatException) {
- // just fall down through to produce an error message
- }
- Errors.SemErr(Filename, prLine, prColumn, "Malformed (#line num [filename]) pragma: #" + hashLine);
- continue;
- }
-
- Errors.SemErr(Filename, prLine, prColumn, "Unrecognized pragma: #" + hashLine);
- continue;
- }
- return;
- }
- }
- }
-
--->comment
-
- static void CheckLiteral() {
- switch (t.val) {
--->literals
- }
- }
-
- public static Token/*!*/ Scan() {
- while (ignore[ch]) { NextCh(); }
--->scan1
- t = new Token();
- t.pos = pos; t.col = pos - lineStart + 1; t.line = line; t.filename = Filename;
- int state = (/*^ (!) ^*/ start)[ch];
- StringBuilder buf = new StringBuilder(16);
- buf.Append(ch); NextCh();
-
- switch (state) {
- case 0: {t.kind = noSym; goto done;} // NextCh already done
--->scan2
- }
- done:
- t.val = buf.ToString();
- return t;
- }
-
-} // end Scanner
-
-
-public delegate void ErrorProc(int n, string filename, int line, int col);
-
-public class Errors {
- public static int count = 0; // number of errors detected
- public static ErrorProc/*!*/ SynErr; // syntactic errors
-
- public static void SemErr(string filename, int line, int col, string! msg) { // semantic errors
- System.ConsoleColor color = System.Console.ForegroundColor;
- System.Console.ForegroundColor = System.ConsoleColor.Red;
- System.Console.WriteLine("{0}({1},{2}): Error: {3}", filename, line, col, msg);
- System.Console.ForegroundColor = color;
- count++;
- }
-
- public static void SemErr(Bpl.IToken! tok, string! msg) { // semantic errors
- SemErr(tok.filename, tok.line, tok.col, msg);
- }
-
- public static void Exception (string s) {
- System.ConsoleColor color = System.Console.ForegroundColor;
- System.Console.ForegroundColor = System.ConsoleColor.Red;
- System.Console.WriteLine(s);
- System.Console.ForegroundColor = color;
- System.Environment.Exit(0);
- }
-
-} // Errors
-
-} // end namespace
-$$$
diff --git a/DafnyDriver/DafnyDriver.ssc b/DafnyDriver/DafnyDriver.ssc index 8920db94..d9d9a6be 100644 --- a/DafnyDriver/DafnyDriver.ssc +++ b/DafnyDriver/DafnyDriver.ssc @@ -350,7 +350,7 @@ namespace Microsoft.Boogie /// </summary>
static Program ParseBoogieProgram(List<string!>! fileNames, bool suppressTraceOutput)
{
- BoogiePL.Errors.count = 0;
+ //BoogiePL.Errors.count = 0;
Program program = null;
bool okay = true;
foreach (string bplFileName in fileNames) {
@@ -366,9 +366,9 @@ namespace Microsoft.Boogie Program programSnippet;
int errorCount;
try {
- errorCount = BoogiePL.Parser.Parse(bplFileName, out programSnippet);
+ errorCount = Microsoft.Boogie.Parser.Parse(bplFileName, out programSnippet);
if (programSnippet == null || errorCount != 0) {
- Console.WriteLine("{0} parse errors detected in {1}", BoogiePL.Errors.count, bplFileName);
+ Console.WriteLine("{0} parse errors detected in {1}", errorCount, bplFileName);
okay = false;
continue;
}
|