From 3e2bab90aac63622eff8fde33b1f5fcb97a5f6c5 Mon Sep 17 00:00:00 2001 From: Jason Koenig Date: Mon, 11 Jul 2011 17:22:32 -0700 Subject: Added s[..] syntax in anticipation of sequence forming operation. (also updated regression tests.) --- Source/Dafny/Dafny.atg | 6 +++-- Source/Dafny/DafnyAst.cs | 2 -- Source/Dafny/Parser.cs | 64 ++++++++++++++++++++++++---------------------- Source/Dafny/Translator.cs | 1 + 4 files changed, 38 insertions(+), 35 deletions(-) (limited to 'Source') diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index f6e40722..bcd23618 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -1354,7 +1354,9 @@ Suffix .) } ) - | ".." Expression (. anyDots = true; e1 = ee; .) + | ".." (. anyDots = true; .) + [ Expression (. e1 = ee; .) + ] ) (. if (multipleIndices != null) { e = new MultiSelectExpr(x, e, multipleIndices); @@ -1367,7 +1369,7 @@ Suffix } Contract.Assert(anyDots || e0 != null); if (anyDots) { - Contract.Assert(e0 != null || e1 != null); + //Contract.Assert(e0 != null || e1 != null); e = new SeqSelectExpr(x, false, e, e0, e1); } else if (e1 == null) { Contract.Assert(e0 != null); diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 4868be10..ce3e479e 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -2113,7 +2113,6 @@ namespace Microsoft.Dafny { void ObjectInvariant() { Contract.Invariant(Seq != null); Contract.Invariant(!SelectOne || E1 == null); - Contract.Invariant(E0 != null || E1 != null); } public SeqSelectExpr(IToken tok, bool selectOne, Expression seq, Expression e0, Expression e1) @@ -2121,7 +2120,6 @@ namespace Microsoft.Dafny { Contract.Requires(tok != null); Contract.Requires(seq != null); Contract.Requires(!selectOne || e1 == null); - Contract.Requires(e0 != null || e1 != null); SelectOne = selectOne; Seq = seq; diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index e12ab7e3..4041ad45 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -1570,7 +1570,7 @@ List/*!*/ decreases) { Term(out e1); e = new BinaryExpr(x, op, e0, e1); if (op == BinaryExpr.Opcode.Disjoint) - acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, e0, e1); // accumulate first two operands. + acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, e0, e1); // accumulate first two operands. while (StartOf(16)) { if (chain == null) { @@ -1603,36 +1603,35 @@ List/*!*/ decreases) { break; case BinaryExpr.Opcode.Neq: if (hasSeenNeq) { SemErr(x, "a chain cannot have more than one != operator"); } - if (kind != 0 && kind != 1 && kind != 2) { SemErr(x, "this operator cannot continue this chain"); } - hasSeenNeq = true; break; - case BinaryExpr.Opcode.Lt: - case BinaryExpr.Opcode.Le: - if (kind == 0) { kind = 1; } - else if (kind != 1) { SemErr(x, "this operator chain cannot continue with an ascending operator"); } - break; - case BinaryExpr.Opcode.Gt: - case BinaryExpr.Opcode.Ge: - if (kind == 0) { kind = 2; } - else if (kind != 2) { SemErr(x, "this operator chain cannot continue with a descending operator"); } - break; - case BinaryExpr.Opcode.Disjoint: - if (kind != 4) { SemErr(x, "can only chain disjoint (!!) with itself."); kind = 3; } - break; - default: - SemErr(x, "this operator cannot be part of a chain"); - kind = 3; break; - } - + if (kind != 0 && kind != 1 && kind != 2) { SemErr(x, "this operator cannot continue this chain"); } + hasSeenNeq = true; break; + case BinaryExpr.Opcode.Lt: + case BinaryExpr.Opcode.Le: + if (kind == 0) { kind = 1; } + else if (kind != 1) { SemErr(x, "this operator chain cannot continue with an ascending operator"); } + break; + case BinaryExpr.Opcode.Gt: + case BinaryExpr.Opcode.Ge: + if (kind == 0) { kind = 2; } + else if (kind != 2) { SemErr(x, "this operator chain cannot continue with a descending operator"); } + break; + case BinaryExpr.Opcode.Disjoint: + if (kind != 4) { SemErr(x, "can only chain disjoint (!!) with itself."); kind = 3; } + break; + default: + SemErr(x, "this operator cannot be part of a chain"); + kind = 3; break; + } + Term(out e1); ops.Add(op); chain.Add(e1); - if (op == BinaryExpr.Opcode.Disjoint) - { + if (op == BinaryExpr.Opcode.Disjoint) { e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, acc, e1)); - acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, acc, e1); //e0 has already been added. - } - else - e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, e0, e1)); - + acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, acc, e1); //e0 has already been added. + } + else + e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, e0, e1)); + } } if (chain != null) { @@ -1916,8 +1915,11 @@ List/*!*/ decreases) { } else SynErr(136); } else if (la.kind == 97) { Get(); - Expression(out ee); - anyDots = true; e1 = ee; + anyDots = true; + if (StartOf(8)) { + Expression(out ee); + e1 = ee; + } } else SynErr(137); if (multipleIndices != null) { e = new MultiSelectExpr(x, e, multipleIndices); @@ -1930,7 +1932,7 @@ List/*!*/ decreases) { } Contract.Assert(anyDots || e0 != null); if (anyDots) { - Contract.Assert(e0 != null || e1 != null); + //Contract.Assert(e0 != null || e1 != null); e = new SeqSelectExpr(x, false, e, e0, e1); } else if (e1 == null) { Contract.Assert(e0 != null); diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index d1c77122..6b77ca71 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -4674,6 +4674,7 @@ namespace Microsoft.Dafny { if (e0 != null) { seq = translator.FunctionCall(expr.tok, BuiltinFunction.SeqDrop, elType, seq, e0); } + // if e0 == null && e1 == null, then we have the identity operation seq[..]; return seq; } -- cgit v1.2.3