Dafny: change labels to use a generic singly linked list

8 files changed, 53 insertions, 28 deletions

diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs
index fad4e7fa..58c73561 100644
--- a/Dafny/Compiler.cs
+++ b/Dafny/Compiler.cs
@@ -871,7 +871,7 @@ namespace Microsoft.Dafny {
       } else if (stmt is BreakStmt) {

         var s = (BreakStmt)stmt;

         Indent(indent);

-        wr.WriteLine("goto after_{0};", s.TargetStmt.Labels.UniqueId);

+        wr.WriteLine("goto after_{0};", s.TargetStmt.Labels.Data.UniqueId);

       } else if (stmt is ReturnStmt) {

         var s = (ReturnStmt)stmt;

         if (s.hiddenUpdate != null)

@@ -1451,7 +1451,7 @@ namespace Microsoft.Dafny {
         TrStmt(ss, indent + IndentAmount);

         if (ss.Labels != null) {

           Indent(indent);  // labels are not indented as much as the statements

-          wr.WriteLine("after_{0}: ;", ss.Labels.UniqueId);

+          wr.WriteLine("after_{0}: ;", ss.Labels.Data.UniqueId);

         }

       }

     }

diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg
index 97da97e3..56eeb5b6 100644
--- a/Dafny/Dafny.atg
+++ b/Dafny/Dafny.atg
@@ -691,7 +691,7 @@ OneStmt<out Statement/*!*/ s>
   | ParallelStmt<out s>

   | "label"                            (. x = t; .)

     Ident<out id> ":"

-    OneStmt<out s>                     (. s.Labels = new LabelNode(x, id.val, s.Labels); .)

+    OneStmt<out s>                     (. s.Labels = new LList<Label>(new Label(x, id.val), s.Labels); .)

   | "break"                            (. x = t; breakCount = 1; label = null; .)

     ( Ident<out id>                    (. label = id.val; .)

     | { "break"                        (. breakCount++; .)

diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index 5fd34e65..0a842025 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -1320,7 +1320,7 @@ namespace Microsoft.Dafny {
 

   public abstract class Statement {

     public readonly IToken Tok;

-    public LabelNode Labels;  // mutable during resolution

+    public LList<Label> Labels;  // mutable during resolution

 

     private Attributes attributes;

     public Attributes Attributes {

@@ -1363,19 +1363,43 @@ namespace Microsoft.Dafny {
     }

   }

 

-  public class LabelNode

+  public class LList<T>

+  {

+    public readonly T Data;

+    public readonly LList<T> Next;

+    const LList<T> Empty = null;

+

+    public LList(T d, LList<T> next) {

+      Data = d;

+      Next = next;

+    }

+

+    public static LList<T> Append(LList<T> a, LList<T> b) {

+      if (a == null) return b;

+      return new LList<T>(a.Data, Append(a.Next, b));

+      // pretend this is ML

+    }

+    public static int Count(LList<T> n) {

+      int count = 0;

+      while (n != null) {

+        count++;

+        n = n.Next;

+      }

+      return count;

+    }

+  }

+

+  public class Label

   {

     public readonly IToken Tok;

-    public readonly string Label;

+    public readonly string Name;

     public readonly int UniqueId;

-    public readonly LabelNode Next;

     static int nodes = 0;

 

-    public LabelNode(IToken tok, string label, LabelNode next) {

+    public Label(IToken tok, string label) {

       Contract.Requires(tok != null);

       Tok = tok;

-      Label = label;

-      Next = next;

+      Name = label;

       UniqueId = nodes++;

     }

   }

diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs
index fe4d58a9..4634c87a 100644
--- a/Dafny/Parser.cs
+++ b/Dafny/Parser.cs
@@ -1098,7 +1098,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Ident(out id);

 			Expect(5);

 			OneStmt(out s);

-			s.Labels = new LabelNode(x, id.val, s.Labels); 

+			s.Labels = new LList<Label>(new Label(x, id.val), s.Labels); 

 			break;

 		}

 		case 50: {

diff --git a/Dafny/Printer.cs b/Dafny/Printer.cs
index 6cf71fa1..e7cfbf27 100644
--- a/Dafny/Printer.cs
+++ b/Dafny/Printer.cs
@@ -421,9 +421,9 @@ namespace Microsoft.Dafny {
     /// </summary>

     public void PrintStatement(Statement stmt, int indent) {

       Contract.Requires(stmt != null);

-      for (LabelNode label = stmt.Labels; label != null; label = label.Next) {

-        if (label.Label != null) {

-          wr.WriteLine("label {0}:", label.Label);

+      for (LList<Label> label = stmt.Labels; label != null; label = label.Next) {

+        if (label.Data.Name != null) {

+          wr.WriteLine("label {0}:", label.Data.Name);

           Indent(indent);

         }

       }

diff --git a/Dafny/RefinementTransformer.cs b/Dafny/RefinementTransformer.cs
index d966a76f..e73d9762 100644
--- a/Dafny/RefinementTransformer.cs
+++ b/Dafny/RefinementTransformer.cs
@@ -513,13 +513,13 @@ namespace Microsoft.Dafny {
       return r;

     }

 

-    void AddStmtLabels(Statement s, LabelNode node) {

+    void AddStmtLabels(Statement s, LList<Label> node) {

       if (node != null) {

         AddStmtLabels(s, node.Next);

-        if (node.Label == null) {

+        if (node.Data.Name == null) {

           // this indicates an implicit-target break statement that has been resolved; don't add it

         } else {

-          s.Labels = new LabelNode(Tok(node.Tok), node.Label, s.Labels);

+          s.Labels = new LList<Label>(new Label(Tok(node.Data.Tok), node.Data.Name), s.Labels);

         }

       }

     }

@@ -1090,8 +1090,8 @@ namespace Microsoft.Dafny {
       Contract.Requires(labels != null);

       Contract.Requires(0 <= loopLevels);

 

-      for (LabelNode n = s.Labels; n != null; n = n.Next) {

-        labels.Push(n.Label);

+      for (LList<Label> n = s.Labels; n != null; n = n.Next) {

+        labels.Push(n.Data.Name);

       }

 

       if (s is SkeletonStatement) {

@@ -1116,7 +1116,7 @@ namespace Microsoft.Dafny {
         }

       }

 

-      for (LabelNode n = s.Labels; n != null; n = n.Next) {

+      for (LList<Label> n = s.Labels; n != null; n = n.Next) {

         labels.Pop();

       }

     }

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index 7be3fca2..23cf892e 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -1355,7 +1355,7 @@ namespace Microsoft.Dafny {
             Statement target = loopStack[loopStack.Count - s.BreakCount];

             if (target.Labels == null) {

               // make sure there is a label, because the compiler and translator will want to see a unique ID

-              target.Labels = new LabelNode(target.Tok, null, null);

+              target.Labels = new LList<Label>(new Label(target.Tok, null), null);

             }

             s.TargetStmt = target;

             if (specContextOnly && !target.IsGhost && !inSpecOnlyContext[target]) {

@@ -2158,17 +2158,18 @@ namespace Microsoft.Dafny {
       foreach (Statement ss in blockStmt.Body) {

         labeledStatements.PushMarker();

         // push labels

-        for (var lnode = ss.Labels; lnode != null; lnode = lnode.Next) {

-          Contract.Assert(lnode.Label != null);  // LabelNode's with .Label==null are added only during resolution of the break statements with 'stmt' as their target, which hasn't happened yet

-          var prev = labeledStatements.Find(lnode.Label);

+        for (var l = ss.Labels; l != null; l = l.Next) {

+          var lnode = l.Data;

+          Contract.Assert(lnode.Name != null);  // LabelNode's with .Label==null are added only during resolution of the break statements with 'stmt' as their target, which hasn't happened yet

+          var prev = labeledStatements.Find(lnode.Name);

           if (prev == ss) {

             Error(lnode.Tok, "duplicate label");

           } else if (prev != null) {

             Error(lnode.Tok, "label shadows an enclosing label");

           } else {

-            bool b = labeledStatements.Push(lnode.Label, ss);

+            bool b = labeledStatements.Push(lnode.Name, ss);

             Contract.Assert(b);  // since we just checked for duplicates, we expect the Push to succeed

-            if (lnode == ss.Labels) {  // add it only once

+            if (l == ss.Labels) {  // add it only once

               inSpecOnlyContext.Add(ss, specContextOnly);

             }

           }

diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index 0189c11b..58c367b8 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -3403,7 +3403,7 @@ namespace Microsoft.Dafny {
       } else if (stmt is BreakStmt) {

         AddComment(builder, stmt, "break statement");

         var s = (BreakStmt)stmt;

-        builder.Add(new GotoCmd(s.Tok, new StringSeq("after_" + s.TargetStmt.Labels.UniqueId)));

+        builder.Add(new GotoCmd(s.Tok, new StringSeq("after_" + s.TargetStmt.Labels.Data.UniqueId)));

       } else if (stmt is ReturnStmt) {

         var s = (ReturnStmt)stmt;

         AddComment(builder, stmt, "return statement");

@@ -3471,7 +3471,7 @@ namespace Microsoft.Dafny {
         foreach (Statement ss in ((BlockStmt)stmt).Body) {

           TrStmt(ss, builder, locals, etran);

           if (ss.Labels != null) {

-            builder.AddLabelCmd("after_" + ss.Labels.UniqueId);

+            builder.AddLabelCmd("after_" + ss.Labels.Data.UniqueId);

           }

         }

       } else if (stmt is IfStmt) {