Dafny: fixed part of a type-inference issue with datatypes and the < operator on datatypes

Dafny: allow the well-formedness check of a function's specification to know that the function, on the current arguments, returns a value of the declared result type

4 files changed, 57 insertions, 3 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index a4d99bd0..2d3ddcca 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -2674,6 +2674,11 @@ namespace Microsoft.Dafny {
                   Error(expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E1.Type);

                 }

                 expr.Type = Type.Bool;

+              } else if (e.Op == BinaryExpr.Opcode.Lt && e.E1.Type.IsDatatype) {

+                if (!UnifyTypes(e.E0.Type, new DatatypeProxy())) {

+                  Error(expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E0.Type);

+                }

+                expr.Type = Type.Bool;

               } else {

                 bool err = false;

                 if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(true))) {

@@ -3768,7 +3773,7 @@ namespace Microsoft.Dafny {
             return BinaryExpr.ResolvedOpcode.Disjoint;

           } 

         case BinaryExpr.Opcode.Lt:

-          if (operandType.IsDatatype) {

+          if (operandType.IsDatatype || operandType is DatatypeProxy) {

             return BinaryExpr.ResolvedOpcode.RankLt;

           } else if (operandType is SetType) {

             return BinaryExpr.ResolvedOpcode.ProperSubset;

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 2cc15c5a..66cfbc57 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -1514,6 +1514,25 @@ namespace Microsoft.Dafny {
       //   }

       // Here go the postconditions (termination checks included, but no reads checks)

       StmtListBuilder postCheckBuilder = new StmtListBuilder();

+      // Assume the type returned by the call itself respects its type (this matter if the type is "nat", for example)

+      {

+        var args = new Bpl.ExprSeq();

+        args.Add(etran.HeapExpr);

+        if (!f.IsStatic) {

+          args.Add(new Bpl.IdentifierExpr(f.tok, etran.This, predef.RefType));

+        }

+        foreach (var p in f.Formals) {

+          args.Add(new Bpl.IdentifierExpr(p.tok, p.UniqueName, TrType(p.Type)));

+        }

+        Bpl.IdentifierExpr funcID = new Bpl.IdentifierExpr(f.tok, FunctionName(f, 1), TrType(f.ResultType));

+        Bpl.Expr funcAppl = new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(funcID), args);

+

+        var wh = GetWhereClause(f.tok, funcAppl, f.ResultType, etran);

+        if (wh != null) {

+          postCheckBuilder.Add(new Bpl.AssumeCmd(f.tok, wh));

+        }

+      }

+      // Now for the ensures clauses

       foreach (Expression p in f.Ens) {

         CheckWellformed(p, new WFOptions(f, f, false), locals, postCheckBuilder, etran);

         // assume the postcondition for the benefit of checking the remaining postconditions

@@ -3109,7 +3128,7 @@ namespace Microsoft.Dafny {
       } else if (type.IsRefType) {

         // object and class types translate to ref

         return predef.RefType;

-      } else if (type.IsDatatype) {

+      } else if (type.IsDatatype || type is DatatypeProxy) {

         return predef.DatatypeType;

       } else if (type is SetType) {

         return predef.SetType(Token.NoToken, predef.BoxType);

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index bdbb8822..bae3aa50 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -133,8 +133,11 @@ Execution trace:
     (0,0): anon6_Else

     (0,0): anon7_Else

     (0,0): anon8_Then

+NatTypes.dfy(127,21): Error: value assigned to a nat must be non-negative

+Execution trace:

+    (0,0): anon3_Then

 

-Dafny program verifier finished with 12 verified, 8 errors

+Dafny program verifier finished with 15 verified, 9 errors

 

 -------------------- SmallTests.dfy --------------------

 SmallTests.dfy(30,11): Error: index out of range

diff --git a/Test/dafny0/NatTypes.dfy b/Test/dafny0/NatTypes.dfy
index 47bc22e1..0513591c 100644
--- a/Test/dafny0/NatTypes.dfy
+++ b/Test/dafny0/NatTypes.dfy
@@ -108,3 +108,30 @@ function Abs(x: int): nat
 {

   if 0 <= x then x else -x

 }

+

+// ----- Here are tests that the type of the result value of a function is known by the

+// ----- time the well-formedness of the function's specification is checked.

+

+function TakesANat(n: nat): bool

+{

+  n < 29

+}

+

+function Naturally(): nat

+  ensures TakesANat(Naturally());  // the wellformedness of this check requires 

+{

+  17

+}

+

+function Integrally_Bad(): int

+  ensures TakesANat(Integrally_Bad());  // error: well-formedness check fails

+{

+  17

+}

+

+function Integrally_Good(): int

+  ensures 0 <= Integrally_Good();

+  ensures TakesANat(Integrally_Good());  // here, the needed information follows from the preceding ensures clause

+{

+  17

+}