diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-05-27 00:56:15 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-05-27 00:56:15 -0700 |
| commit | e840f558d5079001d222a289c9a14ed82c9573c3 (patch) | |
| tree | ef500970b7721a4fc11fbd5dd934ecac1d860c33 /Source/Dafny/DafnyAst.cs | |
| parent | 6e800617ff738c4cce44b6cb1f49221c8ae3e3d9 (diff) | |
Dafny: added chaining operators
Diffstat (limited to 'Source/Dafny/DafnyAst.cs')
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 19 |
1 files changed, 19 insertions, 0 deletions
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;
|