Changed computation of ghosts until pass 2 of resolution.

Other clean-up in resolution passes, like:
Include everything of type "char" into bounds that are discovered, and likewise for reference types.
Allow more set comprehensions, determining if they are finite based on their argument type.
Changed CalcExpr.SubExpressions to not include computed expressions.

1 files changed, 163 insertions, 9 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 2a98d5c2..b460d9b4 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -509,6 +509,27 @@ namespace Microsoft.Dafny {
       }

     }

 

+    public bool HasFinitePossibleValues {

+      get {

+        if (IsBoolType || IsCharType || IsRefType) {

+          return true;

+        }

+        var st = AsSetType;

+        if (st != null && st.Arg.HasFinitePossibleValues) {

+          return true;

+        }

+        var mt = AsMapType;

+        if (mt != null && mt.Domain.HasFinitePossibleValues) {

+          return true;

+        }

+        var dt = AsDatatype;

+        if (dt != null && dt.HasFinitePossibleValues) {

+          return true;

+        }

+        return false;

+      }

+    }

+

     public CollectionType AsCollectionType { get { return NormalizeExpand() as CollectionType; } }

     public SetType AsSetType { get { return NormalizeExpand() as SetType; } }

     public MultiSetType AsMultiSetType { get { return NormalizeExpand() as MultiSetType; } }

@@ -2377,6 +2398,48 @@ namespace Microsoft.Dafny {
     }

 

     /// <summary>

+    /// Returns the non-null expressions of this declaration proper (that is, do not include the expressions of substatements).

+    /// Does not include the generated class members.

+    /// </summary>

+    public virtual IEnumerable<Expression> SubExpressions {

+      get {

+        foreach (var e in Attributes.SubExpressions(Attributes)) {

+          yield return e;

+        }

+        foreach (var e in Attributes.SubExpressions(Reads.Attributes)) {

+          yield return e;

+        }

+        foreach (var e in Reads.Expressions) {

+          yield return e.E;

+        }

+        foreach (var e in Attributes.SubExpressions(Modifies.Attributes)) {

+          yield return e;

+        }

+        foreach (var e in Modifies.Expressions) {

+          yield return e.E;

+        }

+        foreach (var e in Attributes.SubExpressions(Decreases.Attributes)) {

+          yield return e;

+        }

+        foreach (var e in Decreases.Expressions) {

+          yield return e;

+        }

+        foreach (var e in Requires) {

+          yield return e.E;

+        }

+        foreach (var e in Ensures) {

+          yield return e.E;

+        }

+        foreach (var e in YieldRequires) {

+          yield return e.E;

+        }

+        foreach (var e in YieldEnsures) {

+          yield return e.E;

+        }

+      }

+    }

+

+    /// <summary>

     /// This Dafny type exists only for the purpose of giving the yield-count variable a type, so

     /// that the type can be recognized during translation of Dafny into Boogie.  It represents

     /// an integer component in a "decreases" clause whose order is (\lambda x,y :: x GREATER y),

@@ -2475,6 +2538,11 @@ namespace Microsoft.Dafny {
         return EnclosingClass.FullCompileName + ".@" + CompileName;

       }

     }

+    public virtual IEnumerable<Expression> SubExpressions {

+      get {

+        yield break;

+      }

+    }

   }

 

   public class Field : MemberDecl {

@@ -2999,6 +3067,26 @@ namespace Microsoft.Dafny {
     public bool IsBuiltin;

     public Function OverriddenFunction;

 

+    public override IEnumerable<Expression> SubExpressions {

+      get {

+        foreach (var e in Req) {

+          yield return e;

+        }

+        foreach (var e in Reads) {

+          yield return e.E;

+        }

+        foreach (var e in Ens) {

+          yield return e;

+        }

+        foreach (var e in Decreases.Expressions) {

+          yield return e;

+        }

+        if (Body != null) {

+          yield return Body;

+        }

+      }

+    }

+

     public Type Type {

       get {

         // Note, the following returned type can contain type parameters from the function and its enclosing class

@@ -3213,6 +3301,24 @@ namespace Microsoft.Dafny {
     public readonly ISet<IVariable> AssignedAssumptionVariables = new HashSet<IVariable>();

     public Method OverriddenMethod;

 

+    public override IEnumerable<Expression> SubExpressions {

+      get {

+        foreach (var e in Req) {

+          yield return e.E;

+        }

+        foreach (var e in Mod.Expressions) {

+          yield return e.E;

+        }

+        foreach (var e in Ens) {

+          yield return e.E;

+        }

+        foreach (var e in Decreases.Expressions) {

+          yield return e;

+        }

+      }

+    }

+

+

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(cce.NonNullElements(TypeArgs));

@@ -4821,18 +4927,32 @@ namespace Microsoft.Dafny {
     }

     public override IEnumerable<Expression> SubExpressions

     {

-      get { // FIXME: This can return duplicates; this could confuse BottomUpVisitors that modify the AST in place

+      get {

         foreach (var e in base.SubExpressions) { yield return e; }

         foreach (var e in Attributes.SubExpressions(Attributes)) { yield return e; }

-        

-        foreach (var l in Lines) {

-          yield return l;

+

+        for (int i = 0; i < Lines.Count - 1; i++) {  // note, we skip the duplicated line at the end

+          yield return Lines[i];

         }

-        foreach (var e in Steps) {

-          yield return e;

+        foreach (var calcop in AllCalcOps) {

+          var o3 = calcop as TernaryCalcOp;

+          if (o3 != null) {

+            yield return o3.Index;

+          }

+        }

+      }

+    }

+

+    IEnumerable<CalcOp> AllCalcOps {

+      get {

+        if (Op != null) {

+          yield return Op;

         }

-        if (Result != null) {

-          yield return Result;

+        foreach (var stepop in StepOps) {

+          yield return stepop;

+        }

+        if (ResultOp != null) {

+          yield return ResultOp;

         }

       }

     }

@@ -6637,7 +6757,7 @@ namespace Microsoft.Dafny {
     public readonly Expression Body;

     public readonly bool Exact;  // Exact==true means a regular let expression; Exact==false means an assign-such-that expression

     public readonly Attributes Attributes;

-    public List<ComprehensionExpr.BoundedPool> Constraint_Bounds;  // initialized and filled in by resolver; null for Exact=true and for a ghost statement

+    public List<ComprehensionExpr.BoundedPool> Constraint_Bounds;  // initialized and filled in by resolver; null for Exact=true and for when expression is in a ghost context

     // invariant Constraint_Bounds == null || Constraint_Bounds.Count == BoundVars.Count;

     public List<IVariable> Constraint_MissingBounds;  // filled in during resolution; remains "null" if Exact==true or if bounds can be found

     // invariant Constraint_Bounds == null || Constraint_MissingBounds == null;

@@ -6790,6 +6910,22 @@ namespace Microsoft.Dafny {
         return 5;

       }

     }

+    public class CharBoundedPool : BoundedPool

+    {

+      public override int Preference() {

+        return 4;

+      }

+    }

+    public class RefBoundedPool : BoundedPool

+    {

+      public Type Type;

+      public RefBoundedPool(Type t) {

+        Type = t;

+      }

+      public override int Preference() {

+        return 2;

+      }

+    }

     public class IntBoundedPool : BoundedPool

     {

       public readonly Expression LowerBound;

@@ -6864,6 +7000,24 @@ namespace Microsoft.Dafny {
     public List<BoundVar> MissingBounds;  // filled in during resolution; remains "null" if bounds can be found

     // invariant Bounds == null || MissingBounds == null;

 

+    public List<BoundVar> UncompilableBoundVars() {

+      var bvs = new List<BoundVar>();

+      if (MissingBounds != null) {

+        bvs.AddRange(MissingBounds);

+      }

+      if (Bounds != null) {

+        Contract.Assert(Bounds.Count == BoundVars.Count);

+        for (int i = 0; i < Bounds.Count; i++) {

+          var bound = Bounds[i];

+          if (bound is RefBoundedPool) {

+            // yes, this is in principle a bound, but it's not one we'd like to compile

+            bvs.Add(BoundVars[i]);

+          }

+        }

+      }

+      return bvs;

+    }

+

     public ComprehensionExpr(IToken tok, List<BoundVar> bvars, Expression range, Expression term, Attributes attrs)

       : base(tok) {

       Contract.Requires(tok != null);