Unified the .frame files so that both Boogie and Dafny use exactly the same ones.

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