diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index a99ad1029d7..71580bc9c2c 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -18,6 +18,7 @@ readonly Expression/*!*/ dummyExpr; readonly AssignmentRhs/*!*/ dummyRhs; readonly FrameExpression/*!*/ dummyFrameExpr; readonly Statement/*!*/ dummyStmt; +readonly Include theInclude; readonly ModuleDecl theModule; readonly BuiltIns theBuiltIns; readonly bool theVerifyThisFile; @@ -138,17 +139,17 @@ static void EncodeExternAsAttribute(DeclModifierData dmod, ref Attributes attrs, /// Returns the number of parsing errors encountered. /// Note: first initialize the Scanner. /// -public static int Parse (string/*!*/ filename, ModuleDecl module, BuiltIns builtIns, Errors/*!*/ errors, bool verifyThisFile=true) /* throws System.IO.IOException */ { +public static int Parse (string/*!*/ filename, Include include, ModuleDecl module, BuiltIns builtIns, Errors/*!*/ errors, bool verifyThisFile=true) /* throws System.IO.IOException */ { Contract.Requires(filename != null); Contract.Requires(module != null); string s; if (filename == "stdin.dfy") { s = Microsoft.Boogie.ParserHelper.Fill(System.Console.In, new List()); - return Parse(s, filename, filename, module, builtIns, errors, verifyThisFile); + return Parse(s, filename, filename, include, module, builtIns, errors, verifyThisFile); } else { using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) { s = Microsoft.Boogie.ParserHelper.Fill(reader, new List()); - return Parse(s, filename, DafnyOptions.Clo.UseBaseNameForFileName ? Path.GetFileName(filename) : filename, module, builtIns, errors, verifyThisFile); + return Parse(s, filename, DafnyOptions.Clo.UseBaseNameForFileName ? Path.GetFileName(filename) : filename, include, module, builtIns, errors, verifyThisFile); } } } @@ -163,7 +164,7 @@ public static int Parse (string/*!*/ s, string/*!*/ fullFilename, string/*!*/ fi Contract.Requires(filename != null); Contract.Requires(module != null); Errors errors = new Errors(reporter); - return Parse(s, fullFilename, filename, module, builtIns, errors, verifyThisFile); + return Parse(s, fullFilename, filename, null, module, builtIns, errors, verifyThisFile); } /// /// Parses top-level things (modules, classes, datatypes, class members) @@ -171,7 +172,7 @@ public static int Parse (string/*!*/ s, string/*!*/ fullFilename, string/*!*/ fi /// Returns the number of parsing errors encountered. /// Note: first initialize the Scanner with the given Errors sink. /// -public static int Parse (string/*!*/ s, string/*!*/ fullFilename, string/*!*/ filename, ModuleDecl module, +public static int Parse (string/*!*/ s, string/*!*/ fullFilename, string/*!*/ filename, Include include, ModuleDecl module, BuiltIns builtIns, Errors/*!*/ errors, bool verifyThisFile=true) { Contract.Requires(s != null); Contract.Requires(filename != null); @@ -180,11 +181,11 @@ public static int Parse (string/*!*/ s, string/*!*/ fullFilename, string/*!*/ fi byte[]/*!*/ buffer = cce.NonNull( UTF8Encoding.Default.GetBytes(s)); MemoryStream ms = new MemoryStream(buffer,false); Scanner scanner = new Scanner(ms, errors, fullFilename, filename); - Parser parser = new Parser(scanner, errors, module, builtIns, verifyThisFile); + Parser parser = new Parser(scanner, errors, include, module, builtIns, verifyThisFile); parser.Parse(); return parser.errors.ErrorCount; } -public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, ModuleDecl module, BuiltIns builtIns, bool verifyThisFile=true) +public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, Include include, ModuleDecl module, BuiltIns builtIns, bool verifyThisFile=true) : this(scanner, errors) // the real work { // initialize readonly fields @@ -192,6 +193,7 @@ public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, ModuleDecl module, Built dummyRhs = new ExprRhs(dummyExpr, null); dummyFrameExpr = new FrameExpression(dummyExpr.tok, dummyExpr, null); dummyStmt = new ReturnStmt(Token.NoToken, Token.NoToken, null); + theInclude = include; // the "include" that includes this file theModule = module; theBuiltIns = builtIns; theVerifyThisFile = verifyThisFile; @@ -1083,8 +1085,8 @@ NewtypeDecl NoUSIdent [ ":" Type ] (. if (baseType == null) { baseType = new InferredTypeProxy(); } .) "|" - Expression (. td = new NewtypeDecl(theVerifyThisFile ? id : new IncludeToken(id), id.val, module, new BoundVar(bvId, bvId.val, baseType), wh, attrs); .) - | Type (. td = new NewtypeDecl(theVerifyThisFile ? id : new IncludeToken(id), id.val, module, baseType, attrs); .) + Expression (. td = new NewtypeDecl(id, id.val, module, new BoundVar(bvId, bvId.val, baseType), wh, attrs); .) + | Type (. td = new NewtypeDecl(id, id.val, module, baseType, attrs); .) ) . OtherTypeDecl @@ -1110,7 +1112,7 @@ OtherTypeDecl ] (. if (ty == null) { ty = new InferredTypeProxy(); } .) "|" Expression - (. td = new SubsetTypeDecl(theVerifyThisFile ? id : new IncludeToken(id), id.val, typeArgs, module, new BoundVar(bvId, bvId.val, ty), constraint, attrs); + (. td = new SubsetTypeDecl(id, id.val, typeArgs, module, new BoundVar(bvId, bvId.val, ty), constraint, attrs); kind = "Subset type"; .) | @@ -1358,7 +1360,7 @@ MethodDecl(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis); @@ -1720,7 +1722,7 @@ FunctionDecl(decreases, null), body, attrs, signatureEllipsis); @@ -2261,7 +2263,7 @@ ExistentialGuard . MatchStmt = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); - Token x; Expression/*!*/ e; MatchCaseStmt/*!*/ c; + IToken x; Expression/*!*/ e; MatchCaseStmt/*!*/ c; List cases = new List(); bool usesOptionalBraces = false; .) @@ -2455,7 +2457,7 @@ ModifyStmt CalcStmt = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); - Token x; + IToken x; Attributes attrs = null; CalcStmt.CalcOp op, calcOp = Microsoft.Dafny.CalcStmt.DefaultOp, resOp = Microsoft.Dafny.CalcStmt.DefaultOp; var lines = new List(); diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 048f46f2ea1..bff4c978b05 100755 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -80,16 +80,16 @@ public class Parser { public const int _reveal = 64; public const int maxT = 149; - const bool _T = true; - const bool _x = false; - const int minErrDist = 2; + const bool _T = true; + const bool _x = false; + const int minErrDist = 2; - public Scanner scanner; - public Errors errors; + public Scanner scanner; + public Errors errors; - public IToken t; // last recognized token - public IToken la; // lookahead token - int errDist = minErrDist; + public IToken t; // last recognized token + public IToken la; // lookahead token + int errDist = minErrDist; readonly Expression/*!*/ dummyExpr; readonly AssignmentRhs/*!*/ dummyRhs; @@ -653,72 +653,72 @@ int StringToInt(string s, int defaultValue, string errString) { /*--------------------------------------------------------------------------*/ - 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 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 + } - void SynErr (int n) { - if (errDist >= minErrDist) errors.SynErr(la.filename, la.line, la.col, n); - errDist = 0; - } + void SynErr (int n) { + if (errDist >= minErrDist) errors.SynErr(la.filename, la.line, la.col, n); + errDist = 0; + } - public void SemErr (string msg) { - Contract.Requires(msg != null); - if (errDist >= minErrDist) errors.SemErr(t, msg); - errDist = 0; - } + public void SemErr (string msg) { + Contract.Requires(msg != null); + if (errDist >= minErrDist) errors.SemErr(t, msg); + errDist = 0; + } - public void SemErr(IToken tok, string msg) { - Contract.Requires(tok != null); - Contract.Requires(msg != null); - errors.SemErr(tok, msg); - } + public void SemErr(IToken tok, string msg) { + Contract.Requires(tok != null); + Contract.Requires(msg != null); + errors.SemErr(tok, msg); + } - void Get () { - for (;;) { - t = theVerifyThisFile ? la : new IncludeToken(theInclude, la); - la = scanner.Scan(); - if (la.kind <= maxT) { ++errDist; break; } + void Get () { + for (;;) { + t = theVerifyThisFile ? la : new IncludeToken(theInclude, la); + la = scanner.Scan(); + if (la.kind <= maxT) { ++errDist; break; } - la = t; - } - } + la = t; + } + } - void Expect (int n) { - if (la.kind==n) Get(); else { SynErr(n); } - } + void Expect (int n) { + if (la.kind==n) Get(); else { SynErr(n); } + } - bool StartOf (int s) { - return set[s, la.kind]; - } + bool StartOf (int s) { + return set[s, la.kind]; + } - void ExpectWeak (int n, int follow) { - if (la.kind == n) Get(); - else { - SynErr(n); - while (!StartOf(follow)) Get(); - } - } + void ExpectWeak (int n, int follow) { + if (la.kind == n) Get(); + else { + SynErr(n); + while (!StartOf(follow)) Get(); + } + } - 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 { - SynErr(n); - while (!(set[syFol, kind] || set[repFol, kind] || set[0, kind])) { - Get(); - kind = la.kind; - } - return StartOf(syFol); - } - } + 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 { + SynErr(n); + while (!(set[syFol, kind] || set[repFol, kind] || set[0, kind])) { + Get(); + kind = la.kind; + } + return StartOf(syFol); + } + } void Dafny() { @@ -1094,7 +1094,7 @@ void NewtypeDecl(DeclModifierData dmod, ModuleDefinition module, out TopLevelDec td = new NewtypeDecl(id, id.val, module, new BoundVar(bvId, bvId.val, baseType), wh, attrs); } else if (StartOf(6)) { Type(out baseType); - td = new NewtypeDecl(id, id.val, module, baseType, attrs); + td = new NewtypeDecl(id, id.val, module, baseType, attrs); } else SynErr(161); } @@ -1136,7 +1136,7 @@ void OtherTypeDecl(DeclModifierData dmod, ModuleDefinition module, out TopLevelD if (ty == null) { ty = new InferredTypeProxy(); } Expect(24); Expression(out constraint, false, true); - td = new SubsetTypeDecl(id, id.val, typeArgs, module, new BoundVar(bvId, bvId.val, ty), constraint, attrs); + td = new SubsetTypeDecl(id, id.val, typeArgs, module, new BoundVar(bvId, bvId.val, ty), constraint, attrs); kind = "Subset type"; } else if (StartOf(6)) { @@ -1667,7 +1667,7 @@ void FunctionDecl(DeclModifierData dmod, bool isWithinAbstractModule, out Functi SemErr(t, "a function with an ensures clause must have a body, unless given the :axiom attribute"); } EncodeExternAsAttribute(dmod, ref attrs, id, /* needAxiom */ true); - IToken tok = id; + IToken tok = id; if (isTwoState && isPredicate) { f = new TwoStatePredicate(tok, id.val, dmod.IsStatic, typeArgs, formals, reqs, reads, ens, new Specification(decreases, null), body, attrs, signatureEllipsis); @@ -1826,8 +1826,8 @@ void MethodDecl(DeclModifierData dmod, bool allowConstructor, bool isWithinAbstr if (!isWithinAbstractModule && DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom") && !Attributes.Contains(attrs, "imported") && !Attributes.Contains(attrs, "decl") && theVerifyThisFile) { SemErr(t, "a method with an ensures clause must have a body, unless given the :axiom attribute"); } - - IToken tok = id; + + IToken tok = id; if (isConstructor) { m = new Constructor(tok, hasName ? id.val : "_ctor", typeArgs, ins, req, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis); @@ -5043,16 +5043,16 @@ void MemberBindingUpdate(out IToken id, out Expression e) { - public void Parse() { - la = new Token(); - la.val = ""; - Get(); + public void Parse() { + la = new Token(); + la.val = ""; + Get(); Dafny(); Expect(0); - } + } - static readonly bool[,] set = { + static readonly bool[,] set = { {_T,_T,_T,_T, _T,_x,_x,_x, _x,_T,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _T,_x,_x,_x, _x,_x,_T,_x, _x,_T,_T,_T, _x,_x,_x,_T, _T,_x,_x,_T, _T,_T,_x,_T, _T,_T,_T,_T, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_T, _T,_T,_x,_x, _x,_x,_T,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_x,_T, _T,_T,_T,_T, _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, _T,_T,_T,_T, _T,_T,_T,_T, _x,_x,_x}, {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_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,_T,_T, _T,_T,_T,_T, _x,_T,_x,_x, _T,_x,_x,_x, _T,_T,_T,_T, _T,_T,_x,_T, _T,_x,_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, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x}, {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_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}, @@ -5089,32 +5089,32 @@ public void Parse() { {_T,_T,_T,_T, _T,_x,_x,_x, _x,_T,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_T,_T, _T,_T,_T,_T, _x,_T,_x,_x, _T,_x,_x,_x, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_T,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_x,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x}, {_T,_T,_T,_T, _T,_x,_x,_x, _x,_T,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_T, _T,_T,_x,_T, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_T,_T, _T,_T,_T,_T, _x,_T,_x,_x, _T,_x,_x,_x, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_T,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_x,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x} - }; + }; } // end Parser public class Errors { - readonly ErrorReporter Reporting; - public int ErrorCount; + readonly ErrorReporter Reporting; + public int ErrorCount; - public Errors(ErrorReporter Reporting) { - Contract.Requires(Reporting != null); - this.Reporting = Reporting; - } + public Errors(ErrorReporter Reporting) { + Contract.Requires(Reporting != null); + this.Reporting = Reporting; + } - public void SynErr(string filename, int line, int col, int n) { - SynErr(filename, line, col, GetSyntaxErrorString(n)); - } + public void SynErr(string filename, int line, int col, int n) { + SynErr(filename, line, col, GetSyntaxErrorString(n)); + } - public void SynErr(string filename, int line, int col, string msg) { - Contract.Requires(msg != null); - ErrorCount++; - Reporting.Error(MessageSource.Parser, filename, line, col, msg); - } + public void SynErr(string filename, int line, int col, string msg) { + Contract.Requires(msg != null); + ErrorCount++; + Reporting.Error(MessageSource.Parser, filename, line, col, msg); + } - string GetSyntaxErrorString(int n) { - string s; - switch (n) { + string GetSyntaxErrorString(int n) { + string s; + switch (n) { case 0: s = "EOF expected"; break; case 1: s = "ident expected"; break; case 2: s = "digits expected"; break; @@ -5390,23 +5390,23 @@ string GetSyntaxErrorString(int n) { case 272: s = "invalid CaseExpression"; break; case 273: s = "invalid MemberBindingUpdate"; break; - default: s = "error " + n; break; - } - return s; - } + default: s = "error " + n; break; + } + return s; + } - public void SemErr(IToken tok, string msg) { // semantic errors - Contract.Requires(tok != null); - Contract.Requires(msg != null); - ErrorCount++; - Reporting.Error(MessageSource.Parser, tok, msg); - } + public void SemErr(IToken tok, string msg) { // semantic errors + Contract.Requires(tok != null); + Contract.Requires(msg != null); + ErrorCount++; + Reporting.Error(MessageSource.Parser, tok, msg); + } - public void SemErr(string filename, int line, int col, string msg) { - Contract.Requires(msg != null); - ErrorCount++; - Reporting.Error(MessageSource.Parser, filename, line, col, msg); - } + public void SemErr(string filename, int line, int col, string msg) { + Contract.Requires(msg != null); + ErrorCount++; + Reporting.Error(MessageSource.Parser, filename, line, col, msg); + } public void Deprecated(IToken tok, string msg) { Contract.Requires(tok != null); @@ -5420,15 +5420,15 @@ public void DeprecatedStyle(IToken tok, string msg) { Reporting.DeprecatedStyle(MessageSource.Parser, tok, msg); } - public void Warning(IToken tok, string msg) { - Contract.Requires(tok != null); - Contract.Requires(msg != null); - Reporting.Warning(MessageSource.Parser, tok, msg); - } + public void Warning(IToken tok, string msg) { + Contract.Requires(tok != null); + Contract.Requires(msg != null); + Reporting.Warning(MessageSource.Parser, tok, msg); + } } // Errors public class FatalError: Exception { - public FatalError(string m): base(m) {} + public FatalError(string m): base(m) {} } } \ No newline at end of file diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs index 31b163bf784..0e7b3e20bcc 100644 --- a/Source/Dafny/Scanner.cs +++ b/Source/Dafny/Scanner.cs @@ -14,255 +14,255 @@ 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? - - [ContractInvariantMethod] - void ObjectInvariant(){ - Contract.Invariant(buf != null); - Contract.Invariant(stream != null); - } + // 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? + + [ContractInvariantMethod] + void ObjectInvariant(){ + Contract.Invariant(buf != null); + Contract.Invariant(stream != null); + } // [NotDelayed] - public Buffer (Stream/*!*/ s, bool isUserStream) : base() { - Contract.Requires(s != null); - stream = s; this.isUserStream = isUserStream; - - int fl, bl; - if (s.CanSeek) { - fl = (int) s.Length; - 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; - - if (fileLen > 0) Pos = 0; // setup buffer to position 0 (start) - else bufPos = 0; // index 0 is already after the file, thus Pos = 0 is invalid - if (bufLen == fileLen && s.CanSeek) Close(); - } - - protected Buffer(Buffer/*!*/ b) { // called in UTF8Buffer constructor - Contract.Requires(b != null); - buf = b.buf; - 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) { - Contract.Ensures(Contract.Result() != null); - 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); - } - - 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; - } + public Buffer (Stream/*!*/ s, bool isUserStream) : base() { + Contract.Requires(s != null); + stream = s; this.isUserStream = isUserStream; + + int fl, bl; + if (s.CanSeek) { + fl = (int) s.Length; + 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; + + if (fileLen > 0) Pos = 0; // setup buffer to position 0 (start) + else bufPos = 0; // index 0 is already after the file, thus Pos = 0 is invalid + if (bufLen == fileLen && s.CanSeek) Close(); + } + + protected Buffer(Buffer/*!*/ b) { // called in UTF8Buffer constructor + Contract.Requires(b != null); + buf = b.buf; + 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) { + Contract.Ensures(Contract.Result() != null); + 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); + } + + 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; + } } //----------------------------------------------------------------------------------- // UTF8Buffer //----------------------------------------------------------------------------------- public class UTF8Buffer: Buffer { - public UTF8Buffer(Buffer/*!*/ b): base(b) {Contract.Requires(b != null);} - - 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; - } + public UTF8Buffer(Buffer/*!*/ b): base(b) {Contract.Requires(b != null);} + + 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 EOL = '\n'; - const int eofSym = 0; /* pdt */ + const char EOL = '\n'; + const int eofSym = 0; /* pdt */ const int maxT = 149; const int noSym = 149; - [ContractInvariantMethod] - void objectInvariant(){ - Contract.Invariant(this._buffer != null); - Contract.Invariant(t != null); - Contract.Invariant(start != null); - Contract.Invariant(tokens != null); - Contract.Invariant(pt != null); - Contract.Invariant(tval != null); - Contract.Invariant(Filename != null); - Contract.Invariant(FullFilename != null); - Contract.Invariant(errorHandler != null); - } - - private Buffer/*!*/ _buffer; // scanner buffer - - public Buffer/*!*/ buffer { - get { - Contract.Ensures(Contract.Result() != null); - return this._buffer; - } - set { - Contract.Requires(value != null); - this._buffer = value; - } - } - - Token/*!*/ t; // current token - int ch; // current input character - int pos; // byte position of current character - int charPos; - 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 - - 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; - - internal string/*!*/ FullFilename { get; private set; } - - static Scanner() { - start = new Hashtable(128); + [ContractInvariantMethod] + void objectInvariant(){ + Contract.Invariant(this._buffer != null); + Contract.Invariant(t != null); + Contract.Invariant(start != null); + Contract.Invariant(tokens != null); + Contract.Invariant(pt != null); + Contract.Invariant(tval != null); + Contract.Invariant(Filename != null); + Contract.Invariant(FullFilename != null); + Contract.Invariant(errorHandler != null); + } + + private Buffer/*!*/ _buffer; // scanner buffer + + public Buffer/*!*/ buffer { + get { + Contract.Ensures(Contract.Result() != null); + return this._buffer; + } + set { + Contract.Requires(value != null); + this._buffer = value; + } + } + + Token/*!*/ t; // current token + int ch; // current input character + int pos; // byte position of current character + int charPos; + 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 + + 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; + + internal string/*!*/ FullFilename { get; private set; } + + static Scanner() { + start = new Hashtable(128); for (int i = 63; i <= 63; ++i) start[i] = 1; for (int i = 65; i <= 90; ++i) start[i] = 1; for (int i = 95; i <= 95; ++i) start[i] = 1; @@ -312,156 +312,155 @@ static Scanner() { start[94] = 96; start[Buffer.EOF] = -1; - } + } -// [NotDelayed] - public Scanner (string/*!*/ fullFilename, string/*!*/ fileName, Errors/*!*/ errorHandler, bool useBaseName = false) : base() { - Contract.Requires(fileName != null); - Contract.Requires(errorHandler != null); - 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); - this._buffer = new Buffer(stream, false); - this.FullFilename = fullFilename; - Filename = useBaseName? GetBaseName(fileName): fileName; - Init(1); - } catch (IOException) { - throw new FatalError("Cannot open file " + fileName); - } - } - -// [NotDelayed] - public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fullFilename, string/*!*/ fileName, int lineNumber = 1, bool useBaseName = false) : base() { - Contract.Requires(s != null); - Contract.Requires(errorHandler != null); - Contract.Requires(fileName != null); - pt = tokens = new Token(); // first token is a dummy - t = new Token(); // dummy because t is a non-null field - this._buffer = new Buffer(s, true); - this.errorHandler = errorHandler; - this.FullFilename = fullFilename; - this.Filename = useBaseName? GetBaseName(fileName) : fileName; - Init(lineNumber); - } - - - string GetBaseName(string fileName) { - return System.IO.Path.GetFileName(fileName); // Return basename - } - - void Init(int lineNumber) { - pos = -1; line = lineNumber; 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(){ - Contract.Ensures(Contract.Result() != null); - 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); - Contract.Assert(s!=null); - 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(); - Contract.Assert(hashLine!=null); - 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; - } - - - } - - } +// [NotDelayed] + public Scanner (string/*!*/ fullFilename, string/*!*/ fileName, Errors/*!*/ errorHandler, bool useBaseName = false) : base() { + Contract.Requires(fileName != null); + Contract.Requires(errorHandler != null); + 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); + this._buffer = new Buffer(stream, false); + this.FullFilename = fullFilename; + Filename = useBaseName? GetBaseName(fileName): fileName; + Init(1); + } catch (IOException) { + throw new FatalError("Cannot open file " + fileName); + } + } - 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) { +// [NotDelayed] + public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fullFilename, string/*!*/ fileName, int lineNumber = 1, bool useBaseName = false) : base() { + Contract.Requires(s != null); + Contract.Requires(errorHandler != null); + Contract.Requires(fileName != null); + pt = tokens = new Token(); // first token is a dummy + t = new Token(); // dummy because t is a non-null field + this._buffer = new Buffer(s, true); + this.errorHandler = errorHandler; + this.FullFilename = fullFilename; + this.Filename = useBaseName? GetBaseName(fileName) : fileName; + Init(lineNumber); + } + + string GetBaseName(string fileName) { + return System.IO.Path.GetFileName(fileName); // Return basename + } + + void Init(int lineNumber) { + pos = -1; line = lineNumber; 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(){ + Contract.Ensures(Contract.Result() != null); + 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); + Contract.Assert(s!=null); + 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(); + Contract.Assert(hashLine!=null); + 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(); - } - } + NextCh(); + } + } @@ -512,7 +511,7 @@ bool Comment1() { } - public void CheckLiteral() { + public void CheckLiteral() { switch (t.val) { case "bool": t.kind = 7; break; case "char": t.kind = 8; break; @@ -603,37 +602,37 @@ public void CheckLiteral() { case "old": t.kind = 147; break; default: break; } - } + } - Token/*!*/ NextToken() { - Contract.Ensures(Contract.Result() != null); - while (ch == ' ' || + Token/*!*/ NextToken() { + Contract.Ensures(Contract.Result() != null); + while (ch == ' ' || ch >= 9 && ch <= 10 || ch == 13 - ) NextCh(); + ) NextCh(); if (ch == '/' && Comment0() ||ch == '/' && Comment1()) return NextToken(); int apx = 0; - 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)) { - Contract.Assert(start[ch] != null); - state = (int) start[ch]; - } - else { state = 0; } - tlen = 0; AddCh(); - - switch (state) { - case -1: { t.kind = eofSym; break; } // NextCh already done - case 0: { - if (recKind != noSym) { - tlen = recEnd - t.pos; - SetScannerBehindT(); - } - t.kind = recKind; break; - } // NextCh already done + 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)) { + Contract.Assert(start[ch] != null); + state = (int) start[ch]; + } + else { state = 0; } + tlen = 0; AddCh(); + + switch (state) { + case -1: { t.kind = eofSym; break; } // NextCh already done + case 0: { + if (recKind != noSym) { + tlen = recEnd - t.pos; + SetScannerBehindT(); + } + t.kind = recKind; break; + } // NextCh already done case 1: recEnd = pos; recKind = 1; if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 1;} @@ -999,44 +998,44 @@ public void CheckLiteral() { if (ch == '>') {AddCh(); goto case 81;} else {t.kind = 122; break;} - } - t.val = new String(tval, 0, tlen); - return t; - } - - private void SetScannerBehindT() { - buffer.Pos = t.pos; - NextCh(); - line = t.line; col = t.col; - for (int i = 0; i < tlen; i++) NextCh(); - } - - // get the next token (possibly a token already seen during peeking) - public Token/*!*/ Scan () { - Contract.Ensures(Contract.Result() != null); - if (tokens.next == null) { - return NextToken(); - } else { - pt = tokens = tokens.next; - return tokens; - } - } - - // peek for the next token, ignore pragmas - public Token/*!*/ Peek () { - Contract.Ensures(Contract.Result() != null); - do { - if (pt.next == null) { - pt.next = NextToken(); - } - pt = pt.next; - } while (pt.kind > maxT); // skip pragmas - - return pt; - } - - // make sure that peeking starts at the current scan position - public void ResetPeek () { pt = tokens; } + } + t.val = new String(tval, 0, tlen); + return t; + } + + private void SetScannerBehindT() { + buffer.Pos = t.pos; + NextCh(); + line = t.line; col = t.col; + for (int i = 0; i < tlen; i++) NextCh(); + } + + // get the next token (possibly a token already seen during peeking) + public Token/*!*/ Scan () { + Contract.Ensures(Contract.Result() != null); + if (tokens.next == null) { + return NextToken(); + } else { + pt = tokens = tokens.next; + return tokens; + } + } + + // peek for the next token, ignore pragmas + public Token/*!*/ Peek () { + Contract.Ensures(Contract.Result() != null); + do { + if (pt.next == null) { + pt.next = NextToken(); + } + pt = pt.next; + } while (pt.kind > maxT); // skip pragmas + + return pt; + } + + // make sure that peeking starts at the current scan position + public void ResetPeek () { pt = tokens; } } // end Scanner