From e840f558d5079001d222a289c9a14ed82c9573c3 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Fri, 27 May 2011 00:56:15 -0700
Subject: Dafny: added chaining operators

---
 Source/Dafny/DafnyAst.cs | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

(limited to 'Source/Dafny/DafnyAst.cs')

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index bb5f4f67..421ec5e1 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -2877,6 +2877,25 @@ namespace Microsoft.Dafny {
     }
   }
 
+  public class ChainingExpression : ConcreteSyntaxExpression
+  {
+    public readonly List<Expression> Operands;
+    public readonly List<BinaryExpr.Opcode> Operators;
+    public readonly Expression E;
+    public ChainingExpression(IToken tok, List<Expression> operands, List<BinaryExpr.Opcode> operators, Expression desugaring)
+      : base(tok) {
+      Contract.Requires(tok != null);
+      Contract.Requires(operands != null);
+      Contract.Requires(operators != null);
+      Contract.Requires(desugaring != null);
+      Contract.Requires(operators.Count == operators.Count + 1);
+
+      Operands = operands;
+      Operators = operators;
+      E = desugaring;
+    }
+  }
+
   public class IdentifierSequence : ConcreteSyntaxExpression
   {
     public readonly List<IToken> Tokens;
-- 
cgit v1.2.3