Add autoReq support for matches.

Add better handling of resolved data types in autoReq.

6 files changed, 70 insertions, 19 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index ee3820b3..55b23827 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -123,7 +123,7 @@ namespace Microsoft.Dafny
       }

     }

 

-    public Type CloneType(Type t) {

+    virtual public Type CloneType(Type t) {

       if (t is BasicType) {

         return t;

       } else if (t is SetType) {

@@ -697,4 +697,23 @@ namespace Microsoft.Dafny
       return base.CloneStmt(stmt);

     }

   }

+

+

+  class ResolvedCloner : Cloner {

+

+    public override Type CloneType(Type t) {

+      Type new_t = base.CloneType(t);

+

+      if (t is UserDefinedType) {

+        var tt = (UserDefinedType)t;

+        var new_tt = (UserDefinedType)new_t;

+

+        new_tt.ResolvedClass = tt.ResolvedClass;

+        new_tt.ResolvedParam = tt.ResolvedParam;                

+      }

+

+      return new_t;

+    }

+  }

+

 }

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 994a9d7e..6908a373 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -4069,8 +4069,6 @@ namespace Microsoft.Dafny {
       return ite;

     }

 

-    /*  Still under development

-     

     /// <summary>

     /// Create a resolved case expression for a match expression

     /// </summary>

@@ -4078,8 +4076,8 @@ namespace Microsoft.Dafny {
       Contract.Requires(old_case != null);

       Contract.Requires(new_body != null);   

       Contract.Ensures(Contract.Result<Expression>() != null);

-      

-      Cloner cloner = new Cloner();

+

+      ResolvedCloner cloner = new ResolvedCloner();

       var newVars = old_case.Arguments.ConvertAll(cloner.CloneBoundVar);

       new_body = VarSubstituter(old_case.Arguments, newVars, new_body);

 

@@ -4098,8 +4096,7 @@ namespace Microsoft.Dafny {
 

       return e;

     }

-    */

-

+ 

     /// <summary>

     /// Create a let expression with a resolved type and fresh variables

     /// </summary>

@@ -4109,7 +4106,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(vars.Count == RHSs.Count);

       Contract.Requires(body != null);

 

-      Cloner cloner = new Cloner();

+      ResolvedCloner cloner = new ResolvedCloner();

       var newVars = vars.ConvertAll(cloner.CloneBoundVar);

       body = VarSubstituter(vars, newVars, body);

 

@@ -4126,7 +4123,7 @@ namespace Microsoft.Dafny {
       //(IToken tok, List<BoundVar> vars, Expression range, Expression body, Attributes attribs, Qu) {

       Contract.Requires(expr != null);

 

-      Cloner cloner = new Cloner();

+      ResolvedCloner cloner = new ResolvedCloner();

       var newVars = expr.BoundVars.ConvertAll(cloner.CloneBoundVar);

 

       if (body == null) {

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 3ca5872c..3d8f84c9 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -36,16 +36,15 @@ namespace Microsoft.Dafny {
       }

     }

 

-    /*

+ 

     public static string ExtendedExprToString(Expression expr) {

       Contract.Requires(expr != null);

       using (var wr = new System.IO.StringWriter()) {

         var pr = new Printer(wr);

-        pr.PrintExtendedExpr(expr, 0, true, false, false);        

+        pr.PrintExtendedExpr(expr, 0, true, false);        

         return wr.ToString();

       }

     }

-     */

 

     public static string IteratorClassToString(IteratorDecl iter) {

       Contract.Requires(iter != null);

diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index f6460e63..601ef935 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -532,6 +532,7 @@ namespace Microsoft.Dafny
   public class AutoReqFunctionRewriter : IRewriter {

     Function parentFunction;

     Resolver resolver;

+    bool containsMatch; // TODO: Track this per-requirement, rather than per-function

 

     public AutoReqFunctionRewriter(Resolver r) {

       this.resolver = r;

@@ -548,6 +549,7 @@ namespace Microsoft.Dafny
           Function fn = (Function)scComponent;

           if (Attributes.ContainsBoolAtAnyLevel(fn, "autoReq")) {

             parentFunction = fn;  // Remember where the recursion started

+            containsMatch = false;  // Assume no match statements are involved

 

             List<Expression> auto_reqs = new List<Expression>();

 

@@ -573,8 +575,11 @@ namespace Microsoft.Dafny
       string tip = "";

 

       foreach (var req in reqs) {

-        //tip += prefix + Printer.ExtendedExprToString(req) + ";\n";

-        tip += prefix + Printer.ExprToString(req) + ";\n";

+        if (containsMatch) {  // Pretty print the requirements

+          tip += prefix + Printer.ExtendedExprToString(req) + ";\n";

+        } else {

+          tip += prefix + Printer.ExprToString(req) + ";\n";

+        }

       }

 

       if (!tip.Equals("")) {

@@ -687,9 +692,9 @@ namespace Microsoft.Dafny
       } else if (expr is OldExpr) {  

       } else if (expr is MatchExpr) {

         MatchExpr e = (MatchExpr)expr;

+        containsMatch = true;

         reqs.AddRange(generateAutoReqs(e.Source));

         

-        /*  Still under development

         List<MatchCaseExpr> newMatches = new List<MatchCaseExpr>();

         foreach (MatchCaseExpr caseExpr in e.Cases) {

           //MatchCaseExpr c = new MatchCaseExpr(caseExpr.tok, caseExpr.Id, caseExpr.Arguments, andify(caseExpr.tok, generateAutoReqs(caseExpr.Body)));

@@ -699,7 +704,6 @@ namespace Microsoft.Dafny
         }

         

         reqs.Add(Expression.CreateMatch(e.tok, e.Source, newMatches, e.Type));

-        */

       } else if (expr is MultiSetFormingExpr) {

         MultiSetFormingExpr e = (MultiSetFormingExpr)expr;

         reqs.AddRange(generateAutoReqs(e.E));

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index d7996361..c46f780c 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -2044,6 +2044,10 @@ Dafny program verifier finished with 3 verified, 3 errors
 Dafny program verifier finished with 2 verified, 0 errors

 

 -------------------- AutoReq.dfy --------------------

+AutoReq.dfy(245,3): Error: possible violation of function precondition

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

 AutoReq.dfy(11,3): Error: possible violation of function precondition

 Execution trace:

     (0,0): anon0

@@ -2079,7 +2083,7 @@ Execution trace:
     (0,0): anon0

     (0,0): anon11_Then

 

-Dafny program verifier finished with 37 verified, 7 errors

+Dafny program verifier finished with 43 verified, 8 errors

 

 -------------------- Superposition.dfy --------------------

 

diff --git a/Test/dafny0/AutoReq.dfy b/Test/dafny0/AutoReq.dfy
index 9e221900..00c74f50 100644
--- a/Test/dafny0/AutoReq.dfy
+++ b/Test/dafny0/AutoReq.dfy
@@ -222,7 +222,36 @@ module {:autoReq} M1 {
     }

 }

 

-/*  Not yet implemented

+module Datatypes {

+	datatype TheType = TheType_builder(x:int) | TheType_copier(t:TheType);

+

+	function f1(t:TheType):bool

+		requires t.TheType_builder? && t.x > 3;

+

+	function {:autoReq} test(t:TheType) : bool

+	{

+		f1(t)

+	}

+

+	function f2(x:int) : bool

+		requires forall t:TheType :: t.TheType_builder? && t.x > x;

+	{

+		true

+	}

+

+	// Should cause a function-requirement violation without autoReq

+	function f3(y:int) : bool

+	{

+		f2(y)

+	}

+

+	function {:autoReq} test2(z:int) : bool

+	{

+		f2(z)

+	}

+

+}

+

 module Matches {

 	datatype TheType = TheType_builder(x:int) | TheType_copier(t:TheType);

 

@@ -236,6 +265,5 @@ module Matches {
 			case TheType_copier(t) => true

 	}

 }

-*/