From 6da9d946cab8aeb7306de50a7470e3a14c7e2e9c Mon Sep 17 00:00:00 2001 From: mikebarnett Date: Fri, 25 Jun 2010 16:36:48 +0000 Subject: Unified the .frame files so that both Boogie and Dafny use exactly the same ones. --- Source/Core/Makefile | 8 +++-- Source/Core/ParserHelper.ssc | 72 ++++++++++++++++++++++++++++++++++++++++++++ Source/Core/Scanner.ssc | 71 ++----------------------------------------- Source/Dafny/Makefile | 5 +-- 4 files changed, 82 insertions(+), 74 deletions(-) diff --git a/Source/Core/Makefile b/Source/Core/Makefile index d7236a5b..a549dd81 100644 --- a/Source/Core/Makefile +++ b/Source/Core/Makefile @@ -3,8 +3,10 @@ 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. +# from http://boogiepartners.codeplex.com/. Update the FRAME_DIR variable to +# point to whatever directory you install that into. # ############################################################################### +FRAME_DIR = c:\BoogiePartners\CocoR\Modified # "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 @@ -14,8 +16,8 @@ all: Parser.ssc #Graph.dll: Graph.as # $(ASML) /target:library Graph.as -Parser.ssc: Scanner.frame Parser.frame BoogiePL.atg - $(COCO) BoogiePL.atg -namespace Microsoft.Boogie +Parser.ssc: $(FRAME_DIR)\Scanner.frame $(FRAME_DIR)\Parser.frame BoogiePL.atg + $(COCO) BoogiePL.atg -namespace Microsoft.Boogie -frames $(FRAME_DIR) copy Parser.cs Parser.ssc copy Scanner.cs Scanner.ssc diff --git a/Source/Core/ParserHelper.ssc b/Source/Core/ParserHelper.ssc index ee01880a..8b0d3fed 100644 --- a/Source/Core/ParserHelper.ssc +++ b/Source/Core/ParserHelper.ssc @@ -1,7 +1,79 @@ using System.Text; using System.Collections.Generic; using System.IO; +using Microsoft.Contracts; + namespace Microsoft.Boogie { + + [Immutable] + public interface IToken { + int kind {get; set; } // token kind + string filename {get; set; } // token file + int pos {get; set; } // token position in the source text (starting at 0) + int col {get; set; } // token column (starting at 0) + int line {get; set; } // token line (starting at 1) + string/*!*/ val {get; set; } // token value + + bool IsValid { get; } + } + + [Immutable] + public class Token : IToken { + public int _kind; // token kind + string _filename; // token file + public int _pos; // token position in the source text (starting at 0) + public int _col; // token column (starting at 1) + public int _line; // token line (starting at 1) + public string/*!*/ _val; // token value + public Token next; // ML 2005-03-11 Tokens are kept in linked list + + public static IToken! NoToken = new Token(); + + public Token() { + this._val = "anything so that it is nonnull"; + } + public Token(int linenum, int colnum) { + this._line = linenum; + this._col = colnum; + this._val = "anything so that it is nonnull"; + base(); + } + + public int kind { + get { return this._kind; } + set { this._kind = value; } + } + + public string filename{ + get { return this._filename; } + set { this._filename = value; } + } + + public int pos{ + get { return this._pos; } + set { this._pos = value; } + } + + public int col{ + get { return this._col; } + set { this._col = value; } + } + + public int line{ + get { return this._line; } + set { this._line = value; } + } + + public string/*!*/ val{ + get { return this._val; } + set { this._val = value; } + } + + public bool IsValid { get { return this._filename != null; } } + + +} + public static class ParserHelper { struct ReadState { public bool hasSeenElse; diff --git a/Source/Core/Scanner.ssc b/Source/Core/Scanner.ssc index 3765574e..d7f8dc69 100644 --- a/Source/Core/Scanner.ssc +++ b/Source/Core/Scanner.ssc @@ -5,77 +5,10 @@ using System.Collections; using System.Collections.Generic; using System.Text; using Microsoft.Contracts; - +using Microsoft.Boogie; +using BoogiePL; namespace Microsoft.Boogie { - [Immutable] - public interface IToken { - int kind {get; set; } // token kind - string filename {get; set; } // token file - int pos {get; set; } // token position in the source text (starting at 0) - int col {get; set; } // token column (starting at 0) - int line {get; set; } // token line (starting at 1) - string/*!*/ val {get; set; } // token value - - bool IsValid { get; } - } - - [Immutable] - public class Token : IToken { - public int _kind; // token kind - string _filename; // token file - public int _pos; // token position in the source text (starting at 0) - public int _col; // token column (starting at 1) - public int _line; // token line (starting at 1) - public string/*!*/ _val; // token value - public Token next; // ML 2005-03-11 Tokens are kept in linked list - - public static IToken! NoToken = new Token(); - - public Token() { - this._val = "anything so that it is nonnull"; - } - public Token(int linenum, int colnum) { - this._line = linenum; - this._col = colnum; - this._val = "anything so that it is nonnull"; - base(); - } - - public int kind { - get { return this._kind; } - set { this._kind = value; } - } - - public string filename{ - get { return this._filename; } - set { this._filename = value; } - } - - public int pos{ - get { return this._pos; } - set { this._pos = value; } - } - - public int col{ - get { return this._col; } - set { this._col = value; } - } - - public int line{ - get { return this._line; } - set { this._line = value; } - } - - public string/*!*/ val{ - get { return this._val; } - set { this._val = value; } - } - - public bool IsValid { get { return this._filename != null; } } - - -} //----------------------------------------------------------------------------------- // Buffer diff --git a/Source/Dafny/Makefile b/Source/Dafny/Makefile index a723042c..3fc283a0 100644 --- a/Source/Dafny/Makefile +++ b/Source/Dafny/Makefile @@ -2,9 +2,10 @@ COCO = ..\..\Binaries\Coco.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. +# from http://boogiepartners.codeplex.com/. Update the FRAME_DIR variable to +# point to whatever directory you install that into. # ############################################################################### -FRAME_DIR = c:\boogiepartners\Dafny\Source +FRAME_DIR = c:\BoogiePartners\CocoR\Modified # "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 -- cgit v1.2.3