diff options
| author |  rustanleino <unknown> | 2010-06-24 01:13:16 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-06-24 01:13:16 +0000 |
| commit | d6d6e64df3130bae7d28eb165ea861e5eb298464 (patch) | |
| tree | 74585d4942732de9e6ef72693b5e5e859788927a /Source | |
| parent | cf26b0336a404760302bd57eb822fa906105cf1d (diff) | |
Dafny:
* re-introduced the feature where an input filename of "stdin.dfy" says to read the program from standard input
* supplied missing case (NotInSet) in Compiler.ssc
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Dafny/Compiler.ssc | 7 | ||||
| -rw-r--r-- | Source/Dafny/Dafny.atg | 2 | ||||
| -rw-r--r-- | Source/Dafny/Makefile | 13 | ||||
| -rw-r--r-- | Source/Dafny/Parser.ssc | 2 |
4 files changed, 18 insertions, 6 deletions
diff --git a/Source/Dafny/Compiler.ssc b/Source/Dafny/Compiler.ssc index c7dc73eb..03a83862 100644 --- a/Source/Dafny/Compiler.ssc +++ b/Source/Dafny/Compiler.ssc @@ -1057,6 +1057,13 @@ namespace Microsoft.Dafny { TrExpr(e.E0);
wr.Write(")");
break;
+ case BinaryExpr.ResolvedOpcode.NotInSet:
+ wr.Write("!");
+ TrParenExpr(e.E1);
+ wr.Write(".Contains(");
+ TrExpr(e.E0);
+ wr.Write(")");
+ break;
case BinaryExpr.ResolvedOpcode.Union:
callString = "Union"; break;
case BinaryExpr.ResolvedOpcode.Intersection:
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index ca02d3cf..d69bf19a 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -69,7 +69,7 @@ public static int Parse (string! filename, List<ModuleDecl!>! modules) /* throws string s;
if (filename == "stdin.dfy") {
s = Microsoft.Boogie.ParserHelper.Fill(System.Console.In, new List<string!>());
- return Parse(s, modules);
+ return Parse(s, filename, modules);
} else {
using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {
s = Microsoft.Boogie.ParserHelper.Fill(reader, new List<string!>());
diff --git a/Source/Dafny/Makefile b/Source/Dafny/Makefile index e545fbae..a723042c 100644 --- a/Source/Dafny/Makefile +++ b/Source/Dafny/Makefile @@ -1,20 +1,25 @@ 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.
# ###############################################################################
+FRAME_DIR = c:\boogiepartners\Dafny\Source
# "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 -namespace Microsoft.Dafny
+Parser.ssc: $(FRAME_DIR)\Scanner.frame $(FRAME_DIR)\Parser.frame Dafny.atg
+ $(COCO) Dafny.atg -namespace Microsoft.Dafny -frames $(FRAME_DIR)
copy Parser.cs Parser.ssc
copy Scanner.cs Scanner.ssc
clean:
- rm -f Scanner.ssc Parser.ssc
+ if exist Scanner.ssc del Scanner.ssc
+ if exist Scanner.cs del Scanner.cs
+ if exist Scanner.cs.old del Scanner.cs.old
+ if exist Parser.ssc del Parser.ssc
+ if exist Parser.cs del Parser.cs
+ if exist Parser.cs.old del Parser.cs.old
diff --git a/Source/Dafny/Parser.ssc b/Source/Dafny/Parser.ssc index 0f85bbe8..1ed06227 100644 --- a/Source/Dafny/Parser.ssc +++ b/Source/Dafny/Parser.ssc @@ -81,7 +81,7 @@ public static int Parse (string! filename, List<ModuleDecl!>! modules) /* throws string s;
if (filename == "stdin.dfy") {
s = Microsoft.Boogie.ParserHelper.Fill(System.Console.In, new List<string!>());
- return Parse(s, modules);
+ return Parse(s, filename, modules);
} else {
using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {
s = Microsoft.Boogie.ParserHelper.Fill(reader, new List<string!>());
|