Dafny:

* First crack at a compiler (/compile:1 writes out.cs, if Dafny program verifies)
* Added "print" statement (to make running compiled programs more interesting)
* Changed name of default class from $default to _default
Boogie:
* Included "lambda" as a keyword in emacs and latex style files

1 files changed, 13 insertions, 0 deletions

diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc
index 3645e7a3..07a21627 100644
--- a/Source/Core/CommandLineOptions.ssc
+++ b/Source/Core/CommandLineOptions.ssc
@@ -106,6 +106,7 @@ namespace Microsoft.Boogie
     }

 

     public string DafnyPrintFile = null;

+    public bool Compile = true;

     

     public enum ProverWarnings { None, Stdout, Stderr }

     public ProverWarnings PrintProverWarnings = ProverWarnings.None;

@@ -534,6 +535,15 @@ namespace Microsoft.Boogie
             }

             break;

             

+          case "-compile":

+          case "/compile": {

+            int compile = 0;

+            if (ps.GetNumericArgument(ref compile, 2)) {

+              Compile = compile == 1;

+            }

+            break;

+          }

+

           case "-contracts":

           case "/contracts":

           case "-c":

@@ -1840,6 +1850,9 @@ namespace Microsoft.Boogie
 

   /dprint:<file> : print Dafny program after parsing it

                    (use - as <file> to print to console)

+  /compile:<n>   : 0 (default) - do not compile Dafny program

+                   1 - upon successful verification of the Dafny program,

+                       compile Dafny program to C# program out.cs

 

   ---- Boogie options --------------------------------------------------------