Make attributes enumerable.

Use an extension method to properly deal with null attributes

4 files changed, 48 insertions, 49 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index eac64f80..af51d650 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -10,6 +10,7 @@ using System.Diagnostics.Contracts;
 using System.Numerics;

 using System.Linq;

 using Microsoft.Boogie;

+using System.Diagnostics;

 

 namespace Microsoft.Dafny {

   public class Program {

@@ -232,21 +233,12 @@ namespace Microsoft.Dafny {
     }

 

     public static IEnumerable<Expression> SubExpressions(Attributes attrs) {

-      for (; attrs != null; attrs = attrs.Prev) {

-        foreach (var arg in attrs.Args) {

-          yield return arg;

-        }

-      }

+      return attrs.AsEnumerable().SelectMany(aa => attrs.Args);

     }

 

     public static bool Contains(Attributes attrs, string nm) {

       Contract.Requires(nm != null);

-      for (; attrs != null; attrs = attrs.Prev) {

-        if (attrs.Name == nm) {

-          return true;

-        }

-      }

-      return false;

+      return attrs.AsEnumerable().Any(aa => aa.Name == nm);

     }

 

     /// <summary>

@@ -258,10 +250,10 @@ namespace Microsoft.Dafny {
     [Pure]

     public static bool ContainsBool(Attributes attrs, string nm, ref bool value) {

       Contract.Requires(nm != null);

-      for (; attrs != null; attrs = attrs.Prev) {

-        if (attrs.Name == nm) {

-          if (attrs.Args.Count == 1) {

-            var arg = attrs.Args[0] as LiteralExpr;

+      foreach (var attr in attrs.AsEnumerable()) {

+        if (attr.Name == nm) {

+          if (attr.Args.Count == 1) {

+            var arg = attr.Args[0] as LiteralExpr;

             if (arg != null && arg.Value is bool) {

               value = (bool)arg.Value;

             }

@@ -306,9 +298,9 @@ namespace Microsoft.Dafny {
     /// </summary>

     public static List<Expression> FindExpressions(Attributes attrs, string nm) {

       Contract.Requires(nm != null);

-      for (; attrs != null; attrs = attrs.Prev) {

-        if (attrs.Name == nm) {

-          return attrs.Args;

+      foreach (var attr in attrs.AsEnumerable()) {

+        if (attr.Name == nm) {

+          return attr.Args;

         }

       }

       return null;

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

   }

 

+  internal static class AttributesExtensions {

+    public static IEnumerable<Attributes> AsEnumerable(this Attributes attr) {

+      while (attr != null) {

+        yield return attr;

+        attr = attr.Prev;

+      }

+    }

+  }

+

   // ------------------------------------------------------------------------------------------------------

 

   public abstract class Type {

@@ -3042,7 +3043,7 @@ namespace Microsoft.Dafny {
       prefixPredCall.TypeArgumentSubstitutions = new Dictionary<TypeParameter, Type>();

       var old_to_new = new Dictionary<TypeParameter, TypeParameter>();

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

-	 old_to_new[this.TypeArgs[i]] = this.PrefixPredicate.TypeArgs[i];

+   old_to_new[this.TypeArgs[i]] = this.PrefixPredicate.TypeArgs[i];

       }

       foreach (var p in fexp.TypeArgumentSubstitutions) {

         prefixPredCall.TypeArgumentSubstitutions[old_to_new[p.Key]] = p.Value;

@@ -4950,7 +4951,7 @@ namespace Microsoft.Dafny {
   }

 

   // ------------------------------------------------------------------------------------------------------

-

+  [DebuggerDisplay("{Printer.ExprToString(this)}")]

   public abstract class Expression

   {

     public readonly IToken tok;

@@ -5568,8 +5569,8 @@ namespace Microsoft.Dafny {
       Contract.Invariant(cce.NonNullElements(Arguments));

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

       Contract.Invariant(

-	Ctor == null ||

-	InferredTypeArgs.Count == Ctor.EnclosingDatatype.TypeArgs.Count);

+  Ctor == null ||

+  InferredTypeArgs.Count == Ctor.EnclosingDatatype.TypeArgs.Count);

     }

 

     public DatatypeValue(IToken tok, string datatypeName, string memberName, [Captured] List<Expression> arguments)

@@ -6003,10 +6004,10 @@ namespace Microsoft.Dafny {
         Function == null || TypeArgumentSubstitutions == null ||

         Contract.ForAll(

           Function.TypeArgs,

-        	  a => TypeArgumentSubstitutions.ContainsKey(a)) &&

+            a => TypeArgumentSubstitutions.ContainsKey(a)) &&

         Contract.ForAll(

           TypeArgumentSubstitutions.Keys,

-        	  a => Function.TypeArgs.Contains(a) || Function.EnclosingClass.TypeArgs.Contains(a)));

+            a => Function.TypeArgs.Contains(a) || Function.EnclosingClass.TypeArgs.Contains(a)));

     }

 

     public Function Function;  // filled in by resolution

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 5e08a38a..c5535808 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -3429,9 +3429,9 @@ namespace Microsoft.Dafny
       Contract.Requires(opts != null);

       Contract.Requires(opts.DontCareAboutCompilation);  // attributes are never compiled

       // order does not matter much for resolution, so resolve them in reverse order

-      for (; attrs != null; attrs = attrs.Prev) {

-        if (attrs.Args != null) {

-          ResolveAttributeArgs(attrs.Args, opts, true);

+      foreach (var attr in attrs.AsEnumerable()) {

+        if (attr.Args != null) {

+          ResolveAttributeArgs(attr.Args, opts, true);

         }

       }

     }

diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index 1dd985cb..c0a25a82 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -1087,15 +1087,15 @@ namespace Microsoft.Dafny
               // Check for the timeLimitMultiplier attribute

               if (Attributes.Contains(member.Attributes, "timeLimitMultiplier")) {

                 Attributes attrs = member.Attributes;

-                for (; attrs != null; attrs = attrs.Prev) {

-                  if (attrs.Name == "timeLimitMultiplier") {

-                    if (attrs.Args.Count == 1 && attrs.Args[0] is LiteralExpr) {

-                      var arg = attrs.Args[0] as LiteralExpr;

+                foreach (var attr in attrs.AsEnumerable()) {

+                  if (attr.Name == "timeLimitMultiplier") {

+                    if (attr.Args.Count == 1 && attr.Args[0] is LiteralExpr) {

+                      var arg = attr.Args[0] as LiteralExpr;

                       System.Numerics.BigInteger value = (System.Numerics.BigInteger)arg.Value;

                       if (value.Sign > 0) {

                         int current_limit = DafnyOptions.O.ProverKillTime > 0 ? DafnyOptions.O.ProverKillTime : 10;  // Default to 10 seconds

-                        attrs.Args[0] = new LiteralExpr(attrs.Args[0].tok, value * current_limit);

-                        attrs.Name = "timeLimit";

+                        attr.Args[0] = new LiteralExpr(attr.Args[0].tok, value * current_limit);

+                        attr.Name = "timeLimit";

                       }

                     }

                   }

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 26412384..d375c2bb 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -11774,13 +11774,13 @@ namespace Microsoft.Dafny {
 

       public Bpl.QKeyValue TrAttributes(Attributes attrs, string skipThisAttribute) {

         Bpl.QKeyValue kv = null;

-        for ( ; attrs != null; attrs = attrs.Prev) {

-          if (attrs.Name == skipThisAttribute

-           || attrs.Name == "axiom") {  // Dafny's axiom attribute clashes with Boogie's axiom keyword

+        foreach (var attr in attrs.AsEnumerable()) {

+          if (attr.Name == skipThisAttribute

+           || attr.Name == "axiom") {  // Dafny's axiom attribute clashes with Boogie's axiom keyword

             continue;

           }

           List<object> parms = new List<object>();

-          foreach (var arg in attrs.Args) {

+          foreach (var arg in attr.Args) {

             var s = arg.AsStringLiteral();

             if (s != null) {

               // pass string literals down to Boogie as string literals, not as their expression translation

@@ -11791,7 +11791,7 @@ namespace Microsoft.Dafny {
               parms.Add(e);

             }

           }

-          kv = new Bpl.QKeyValue(Token.NoToken, attrs.Name, parms, kv);

+          kv = new Bpl.QKeyValue(Token.NoToken, attr.Name, parms, kv);

         }

         return kv;

       }

@@ -12470,18 +12470,16 @@ namespace Microsoft.Dafny {
     Bpl.Trigger TrTrigger(ExpressionTranslator etran, Attributes attribs, IToken tok, Dictionary<IVariable, Expression> substMap = null)

     {

       Bpl.Trigger tr = null;

-      for (Attributes aa = attribs; aa != null; aa = aa.Prev) {

-        if (aa.Name == "trigger") {

-          List<Bpl.Expr> tt = new List<Bpl.Expr>();

-          foreach (var arg in aa.Args) {

-            if (substMap == null) {

-              tt.Add(etran.TrExpr(arg));

-            } else {

-              tt.Add(etran.TrExpr(Substitute(arg, null, substMap)));

-            }

+      foreach (var trigger in attribs.AsEnumerable().Where(aa => aa.Name == "trigger").Select(aa => aa.Args)) {

+        List<Bpl.Expr> tt = new List<Bpl.Expr>();

+        foreach (var arg in trigger) {

+          if (substMap == null) {

+            tt.Add(etran.TrExpr(arg));

+          } else {

+            tt.Add(etran.TrExpr(Substitute(arg, null, substMap)));

           }

-          tr = new Bpl.Trigger(tok, true, tt, tr);

         }

+        tr = new Bpl.Trigger(tok, true, tt, tr);

       }

       return tr;

     }

@@ -12920,7 +12918,7 @@ namespace Microsoft.Dafny {
         return new List<VarType>();  // don't apply induction

       }

 

-      for (var a = attributes; a != null; a = a.Prev) {

+      foreach (var a in attributes.AsEnumerable()) {

         if (a.Name == "induction") {

           // Here are the supported forms of the :induction attribute.

           //    :induction           -- apply induction to all bound variables