Dafny: handle decreases clause for iterators

3 files changed, 53 insertions, 10 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 6b056200..277cb282 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1154,6 +1154,7 @@ namespace Microsoft.Dafny {
     List<Formal> Ins { get ; }

     List<Formal> Outs { get; }

     Specification<FrameExpression> Modifies { get; }

+    Specification<Expression> Decreases { get; }

     ModuleDefinition EnclosingModule { get; }  // to be called only after signature-resolution is complete

     bool MustReverify { get; }

   }

@@ -1164,9 +1165,11 @@ namespace Microsoft.Dafny {
     public readonly List<Formal> Outs;

     public readonly List<Formal> OutsHistory;  // these are the 'xs' variables

     public readonly List<Formal> ExtraVars;  // _reads, _modifies, _new

+    public readonly List<Field> DecreasesFields;  // filled in during resolution

     public readonly Specification<FrameExpression> Reads;

     public readonly Specification<FrameExpression> Modifies;

     public readonly Specification<Expression> Decreases;

+    public bool InferredDecreases;  // fill in during resolution/registration

     public readonly List<MaybeFreeExpression> Requires;

     public readonly List<MaybeFreeExpression> Ensures;

     public readonly List<MaybeFreeExpression> YieldRequires;

@@ -1223,6 +1226,7 @@ namespace Microsoft.Dafny {
       ExtraVars.Add(new Formal(tok, "_reads", new SetType(new ObjectType()), true, true));

       ExtraVars.Add(new Formal(tok, "_modifies", new SetType(new ObjectType()), true, true));

       ExtraVars.Add(new Formal(tok, "_new", new SetType(new ObjectType()), false, true));

+      DecreasesFields = new List<Field>();

     }

 

     bool ICodeContext.IsGhost { get { return false; } }

@@ -1231,6 +1235,7 @@ namespace Microsoft.Dafny {
     List<Formal> ICodeContext.Ins { get { return this.Ins; } }

     List<Formal> ICodeContext.Outs { get { return this.Outs; } }

     Specification<FrameExpression> ICodeContext.Modifies { get { return this.Modifies; } }

+    Specification<Expression> ICodeContext.Decreases { get { return this.Decreases; } }

     ModuleDefinition ICodeContext.EnclosingModule { get { return this.Module; } }

     bool ICodeContext.MustReverify { get { return false; } }

   }

@@ -1758,6 +1763,7 @@ namespace Microsoft.Dafny {
     List<Formal> ICodeContext.Ins { get { return this.Ins; } }

     List<Formal> ICodeContext.Outs { get { return this.Outs; } }

     Specification<FrameExpression> ICodeContext.Modifies { get { return Mod; } }

+    Specification<Expression> ICodeContext.Decreases { get { return this.Decreases; } }

     ModuleDefinition ICodeContext.EnclosingModule {

       get {

         Contract.Assert(this.EnclosingClass != null);  // this getter is supposed to be called only after signature-resolution is complete

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index bde3afb1..8f005368 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -541,13 +541,32 @@ namespace Microsoft.Dafny
             members.Add(f.Name, f);

             iter.Members.Add(f);

           });

-          // finally, add the additional special variables as fields

+          // add the additional special variables as fields

           foreach (var p in iter.ExtraVars) {

             var field = new SpecialField(p.tok, p.Name, p.CompileName, "", "", p.IsGhost, !p.InParam, false, p.Type, null);

             field.EnclosingClass = iter;  // resolve here

             members.Add(field.Name, field);

             iter.Members.Add(field);

           }

+          // finally, add special variables to hold the components of the (explicit or implicit) decreases clause

+          bool inferredDecreases;

+          var decr = Translator.MethodDecreasesWithDefault(iter, out inferredDecreases);

+          if (inferredDecreases) {

+            iter.InferredDecreases = true;

+            Contract.Assert(iter.Decreases.Expressions.Count == 0);

+            iter.Decreases.Expressions.AddRange(decr);

+          }

+          // create the fields; unfortunately, we don't know their types yet, so we'll just insert type proxies for now

+          var i = 0;

+          foreach (var p in iter.Decreases.Expressions) {

+            var nm = "_decreases" + i;

+            var field = new SpecialField(p.tok, nm, nm, "", "", true, false, false, new InferredTypeProxy(), null);

+            field.EnclosingClass = iter;  // resolve here

+            members.Add(field.Name, field);

+            iter.Members.Add(field);

+            iter.DecreasesFields.Add(field);

+            i++;

+          }

 

           // Note, the typeArgs parameter to the following Method/Predicate constructors is passed in as the empty list.  What that is

           // saying is that the Method/Predicate does not take any type parameters over and beyond what the enclosing type (namely, the

@@ -2548,9 +2567,15 @@ namespace Microsoft.Dafny
           Error(e.E, "Precondition must be a boolean (got {0})", e.E.Type);

         }

       }

-      foreach (Expression e in iter.Decreases.Expressions) {

+      Contract.Assert(iter.Decreases.Expressions.Count == iter.DecreasesFields.Count);

+      for (int i = 0; i < iter.Decreases.Expressions.Count; i++) {

+        var e = iter.Decreases.Expressions[i];

         ResolveExpression(e, false);

-        // any type is fine

+        // any type is fine, but associate this type with the corresponding _decreases<n> field

+        var d = iter.DecreasesFields[i];

+        if (!UnifyTypes(d.Type, e.Type)) {

+          Error(e, "type of field {0} is {1}, but has been constrained elsewhere to be of type {2}", d.Name, e.Type, d.Type);

+        }

       }

 

       // Now add the yield-history variables to the scope

@@ -2662,6 +2687,15 @@ namespace Microsoft.Dafny
       ens.Add(new MaybeFreeExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.Eq,

         new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new"),

         new SetDisplayExpr(iter.tok, new List<Expression>()))));

+      // ensures this._decreases0 == old(DecreasesClause[0]) && ...;

+      Contract.Assert(iter.Decreases.Expressions.Count == iter.DecreasesFields.Count);

+      for (int i = 0; i < iter.Decreases.Expressions.Count; i++) {

+        var p = iter.Decreases.Expressions[i];

+        ens.Add(new MaybeFreeExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.Eq,

+          new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), iter.DecreasesFields[i].Name),

+          new OldExpr(iter.tok, p))));

+      }

+      

 

       // ---------- here comes predicate Valid() ----------

       var reads = iter.Member_Valid.Reads;

@@ -2735,10 +2769,11 @@ namespace Microsoft.Dafny
           subst.Substitute(e.E)),

           e.IsFree));

       }

-      // decreases DecreasesClause[subst];

-      foreach (var d in iter.Decreases.Expressions) {

-        // TODO:  in the following line, "old(E)" should also be replaced by "at(iter._preHeap, E)"

-        iter.Member_MoveNext.Decreases.Expressions.Add(subst.Substitute(d));

+      // decreases this._decreases0, this._decreases1, ...;

+      Contract.Assert(iter.Decreases.Expressions.Count == iter.DecreasesFields.Count);

+      for (int i = 0; i < iter.Decreases.Expressions.Count; i++) {

+        var p = iter.Decreases.Expressions[i];

+        iter.Member_MoveNext.Decreases.Expressions.Add(new FieldSelectExpr(p.tok, new ThisExpr(p.tok), iter.DecreasesFields[i].Name));

       }

       iter.Member_MoveNext.Decreases.Attributes = subst.SubstAttributes(iter.Decreases.Attributes);

     }

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index bd000e8b..bb998e1b 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -2973,11 +2973,11 @@ namespace Microsoft.Dafny {
     /// <summary>

     /// Returns true if it is known how to meaningfully compare the type's inhabitants.

     /// </summary>

-    bool IsOrdered(Type t) {

+    static bool IsOrdered(Type t) {

       return !t.IsTypeParameter && !t.IsCoDatatype;

     }

 

-    List<Expression> MethodDecreasesWithDefault(Method m, out bool inferredDecreases) {

+    public static List<Expression> MethodDecreasesWithDefault(ICodeContext m, out bool inferredDecreases) {

       Contract.Requires(m != null);

 

       inferredDecreases = false;

@@ -2986,12 +2986,14 @@ namespace Microsoft.Dafny {
         decr = new List<Expression>();

         foreach (Formal p in m.Ins) {

           if (IsOrdered(p.Type)) {

-            IdentifierExpr ie = new IdentifierExpr(p.tok, p.UniqueName);

+            IdentifierExpr ie = new IdentifierExpr(p.tok, p.Name);

             ie.Var = p; ie.Type = ie.Var.Type;  // resolve it here

             decr.Add(ie);  // use the method's first parameter instead

           }

         }

         inferredDecreases = true;

+      } else if (m is IteratorDecl) {

+        inferredDecreases = ((IteratorDecl)m).InferredDecreases;

       }

       return decr;

     }