Boogie:

* Added support for polymorphism in lambda expressions
* Little clean-up here and there
* Added 'then' keyword to emacs and latex modes

Dafny:
* Added support for fine-grained framing, using the back-tick syntax from Region Logic
* Internally, changed checking of reads clauses to use a local variable $_Frame, analogous to the $_Frame variable used in checking modifies clauses

1 files changed, 23 insertions, 2 deletions

diff --git a/Source/Dafny/Printer.ssc b/Source/Dafny/Printer.ssc
index a49d1a7e..755c10b2 100644
--- a/Source/Dafny/Printer.ssc
+++ b/Source/Dafny/Printer.ssc
@@ -188,7 +188,7 @@ namespace Microsoft.Dafny {
 

       int ind = indent + IndentAmount;

       PrintSpec("requires", f.Req, ind);

-      PrintSpecLine("reads", f.Reads, ind);

+      PrintFrameSpecLine("reads", f.Reads, ind);

       PrintSpecLine("decreases", f.Decreases, ind);

       if (f.Body != null) {

         Indent(indent);

@@ -242,7 +242,7 @@ namespace Microsoft.Dafny {
 

       int ind = indent + IndentAmount;      

       PrintSpec("requires", method.Req, ind);

-      PrintSpecLine("modifies", method.Mod, ind);

+      PrintFrameSpecLine("modifies", method.Mod, ind);

       PrintSpec("ensures", method.Ens, ind);

       PrintSpecLine("decreases", method.Decreases, ind);

       

@@ -292,6 +292,15 @@ namespace Microsoft.Dafny {
       }

     }

 

+    void PrintFrameSpecLine(string! kind, List<FrameExpression!>! ee, int indent) {

+      if (ee.Count != 0) {

+        Indent(indent);

+        wr.Write("{0} ", kind);

+        PrintFrameExpressionList(ee);

+        wr.WriteLine(";");

+      }

+    }

+

     void PrintSpec(string! kind, List<MaybeFreeExpression!>! ee, int indent) {

       foreach (MaybeFreeExpression e in ee) {

         Indent(indent);

@@ -851,5 +860,17 @@ namespace Microsoft.Dafny {
         PrintExpression(e);

       }

     }

+    

+    void PrintFrameExpressionList(List<FrameExpression!>! fexprs) {

+      string sep = "";

+      foreach (FrameExpression fe in fexprs) {

+        wr.Write(sep);

+        sep = ", ";

+        PrintExpression(fe.E);

+        if (fe.FieldName != null) {

+          wr.Write("`{0}", fe.FieldName);

+        }

+      }

+    }

   }

 }