summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Rustan Leino <leino@microsoft.com>2013-01-16 19:33:15 -0800
committerGravatar Rustan Leino <leino@microsoft.com>2013-01-16 19:33:15 -0800
commit678f36ea920b1be7c7633b9ab7a50672ad54c7b4 (patch)
treebccb63f1141697ca3fb57654bafef704eaf0b54f
parentb47707c222e2d68fb27d4ace45f106e34b2b9f7f (diff)
Removed the syntactic form copredicate #-form with the implicit argument.
Added syntactic support for codatatype #-form equalities.
Diffstat
-rw-r--r--Source/Dafny/Cloner.cs4
-rw-r--r--Source/Dafny/Compiler.cs3
-rw-r--r--Source/Dafny/Dafny.atg48
-rw-r--r--Source/Dafny/DafnyAst.cs49
-rw-r--r--Source/Dafny/Parser.cs184
-rw-r--r--Source/Dafny/Printer.cs43
-rw-r--r--Source/Dafny/Resolver.cs69
-rw-r--r--Source/Dafny/Scanner.cs38
-rw-r--r--Source/Dafny/Translator.cs120
-rw-r--r--Test/dafny0/Answer30
-rw-r--r--Test/dafny0/CoResolution.dfy42
-rw-r--r--Test/dafny0/CoinductiveProofs.dfy25
-rw-r--r--Test/dafny3/Answer2
-rw-r--r--Test/dafny3/Streams.dfy187
14 files changed, 599 insertions, 245 deletions
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 4da38f51..55ac2092 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -283,6 +283,10 @@ namespace Microsoft.Dafny
var e = (BinaryExpr)expr;
return new BinaryExpr(Tok(e.tok), e.Op, CloneExpr(e.E0), CloneExpr(e.E1));
+ } else if (expr is TernaryExpr) {
+ var e = (TernaryExpr)expr;
+ return new TernaryExpr(Tok(e.tok), e.Op, CloneExpr(e.E0), CloneExpr(e.E1), CloneExpr(e.E2));
+
} else if (expr is ChainingExpression) {
var e = (ChainingExpression)expr;
return CloneExpr(e.E); // just clone the desugaring, since it's already available
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 4b59682f..03d89683 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -2174,6 +2174,9 @@ namespace Microsoft.Dafny {
wr.Write(")");
}
+ } else if (expr is TernaryExpr) {
+ Contract.Assume(false); // currently, none of the ternary expressions is compilable
+
} else if (expr is LetExpr) {
var e = (LetExpr)expr;
// The Dafny "let" expression
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 21891e4b..07ce8e8d 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1426,6 +1426,8 @@ RelationalExpression<out Expression/*!*/ e>
IToken x, firstOpTok = null; Expression e0, e1, acc = null; BinaryExpr.Opcode op;
List<Expression> chain = null;
List<BinaryExpr.Opcode> ops = null;
+ List<Expression/*?*/> prefixLimits = null;
+ Expression k;
int kind = 0; // 0 ("uncommitted") indicates chain of ==, possibly with one !=
// 1 ("ascending") indicates chain of ==, <, <=, possibly with one !=
// 2 ("descending") indicates chain of ==, >, >=, possibly with one !=
@@ -1434,15 +1436,21 @@ RelationalExpression<out Expression/*!*/ e>
bool hasSeenNeq = false;
.)
Term<out e0> (. e = e0; .)
- [ RelOp<out x, out op> (. firstOpTok = x; .)
- 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.
+ [ RelOp<out x, out op, out k> (. firstOpTok = x; .)
+ Term<out e1> (. if (k == null) {
+ 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.
+ } else {
+ Contract.Assert(op == BinaryExpr.Opcode.Eq || op == BinaryExpr.Opcode.Neq);
+ e = new TernaryExpr(x, op == BinaryExpr.Opcode.Eq ? TernaryExpr.Opcode.PrefixEqOp : TernaryExpr.Opcode.PrefixNeqOp, k, e0, e1);
+ }
.)
{ (. if (chain == null) {
chain = new List<Expression>();
ops = new List<BinaryExpr.Opcode>();
- chain.Add(e0); ops.Add(op); chain.Add(e1);
+ prefixLimits = new List<Expression>();
+ chain.Add(e0); ops.Add(op); prefixLimits.Add(k); chain.Add(e1);
switch (op) {
case BinaryExpr.Opcode.Eq:
kind = 0; break;
@@ -1462,7 +1470,7 @@ RelationalExpression<out Expression/*!*/ e>
}
e0 = e1;
.)
- RelOp<out x, out op> (. switch (op) {
+ RelOp<out x, out op, out k> (. switch (op) {
case BinaryExpr.Opcode.Eq:
if (kind != 0 && kind != 1 && kind != 2) { SemErr(x, "chaining not allowed from the previous operator"); }
break;
@@ -1488,32 +1496,38 @@ RelationalExpression<out Expression/*!*/ e>
kind = 3; break;
}
.)
- Term<out e1> (. ops.Add(op); chain.Add(e1);
- if (op == BinaryExpr.Opcode.Disjoint) {
+ Term<out e1> (. ops.Add(op); prefixLimits.Add(k); chain.Add(e1);
+ if (k != null) {
+ Contract.Assert(op == BinaryExpr.Opcode.Eq || op == BinaryExpr.Opcode.Neq);
+ e = new TernaryExpr(x, op == BinaryExpr.Opcode.Eq ? TernaryExpr.Opcode.PrefixEqOp : TernaryExpr.Opcode.PrefixNeqOp, k, e0, e1);
+ } else 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
+ } else {
e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, e0, e1));
+ }
.)
}
]
(. if (chain != null) {
- e = new ChainingExpression(firstOpTok, chain, ops, e);
+ e = new ChainingExpression(firstOpTok, chain, ops, prefixLimits, e);
}
.)
.
-RelOp<out IToken/*!*/ x, out BinaryExpr.Opcode op>
+RelOp<out IToken/*!*/ x, out BinaryExpr.Opcode op, out Expression k>
= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null);
x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
IToken y;
+ k = null;
.)
( "==" (. x = t; op = BinaryExpr.Opcode.Eq; .)
+ [ "#" "[" Expression<out k> "]" ]
| "<" (. x = t; op = BinaryExpr.Opcode.Lt; .)
| ">" (. x = t; op = BinaryExpr.Opcode.Gt; .)
| "<=" (. x = t; op = BinaryExpr.Opcode.Le; .)
| ">=" (. x = t; op = BinaryExpr.Opcode.Ge; .)
| "!=" (. x = t; op = BinaryExpr.Opcode.Neq; .)
+ [ "#" "[" Expression<out k> "]" ]
| "!!" (. x = t; op = BinaryExpr.Opcode.Disjoint; .)
| "in" (. x = t; op = BinaryExpr.Opcode.In; .)
| /* The next operator is "!in", but Coco evidently parses "!in" even when it is a prefix of, say, "!initialized".
@@ -1778,9 +1792,8 @@ DottedIdentifiersAndFunction<out Expression e>
Ident<out id> (. idents.Add(id); .)
}
[ (. args = new List<Expression>(); .)
- [ "#" (. Expression k = new ImplicitIdentifierExpr(t, "_k"); .)
- [ "[" Expression<out k> "]"
- ] (. id.val = id.val + "#"; args.Add(k); .)
+ [ "#" (. id.val = id.val + "#"; Expression k; .)
+ "[" Expression<out k> "]" (. args.Add(k); .)
]
"(" (. openParen = t; .)
[ Expressions<args> ]
@@ -1797,9 +1810,8 @@ Suffix<ref Expression/*!*/ e>
( "."
Ident<out id>
[ (. args = new List<Expression/*!*/>(); func = true; .)
- [ "#" (. Expression k = new ImplicitIdentifierExpr(t, "_k"); .)
- [ "[" Expression<out k> "]"
- ] (. id.val = id.val + "#"; args.Add(k); .)
+ [ "#" (. id.val = id.val + "#"; Expression k; .)
+ "[" Expression<out k> "]" (. args.Add(k); .)
]
"(" (. IToken openParen = t; .)
[ Expressions<args> ]
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index c0a085c1..bfc08a5c 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -658,6 +658,10 @@ namespace Microsoft.Dafny {
/// This proxy stands for any datatype.
/// </summary>
public class DatatypeProxy : RestrictedTypeProxy {
+ public readonly bool Co; // false means only inductive datatypes; true means only co-inductive datatypes
+ public DatatypeProxy(bool co) {
+ Co = co;
+ }
public override int OrderID {
get {
return 0;
@@ -3450,19 +3454,6 @@ namespace Microsoft.Dafny {
}
/// <summary>
- /// Indicates the that identifier did not appear explicitly in the source text (like the "_k" in
- /// calls to co-recursive things).
- /// </summary>
- public class ImplicitIdentifierExpr : IdentifierExpr
- {
- public ImplicitIdentifierExpr(IToken tok, string name)
- : base(tok, name) {
- Contract.Requires(tok != null);
- Contract.Requires(name != null);
- }
- }
-
- /// <summary>
/// If an "AutoGhostIdentifierExpr" is used as the out-parameter of a ghost method or
/// a method with a ghost parameter, resolution will change the .Var's .IsGhost to true
/// automatically. This class is intended to be used only as a communicate between the
@@ -4023,6 +4014,34 @@ namespace Microsoft.Dafny {
}
}
+ public class TernaryExpr : Expression
+ {
+ public readonly Opcode Op;
+ public readonly Expression E0;
+ public readonly Expression E1;
+ public readonly Expression E2;
+ public enum Opcode { /*SOON: IfOp,*/ PrefixEqOp, PrefixNeqOp }
+ public TernaryExpr(IToken tok, Opcode op, Expression e0, Expression e1, Expression e2)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ Contract.Requires(e0 != null);
+ Contract.Requires(e1 != null);
+ Contract.Requires(e2 != null);
+ Op = op;
+ E0 = e0;
+ E1 = e1;
+ E2 = e2;
+ }
+
+ public override IEnumerable<Expression> SubExpressions {
+ get {
+ yield return E0;
+ yield return E1;
+ yield return E2;
+ }
+ }
+ }
+
public class LetExpr : Expression
{
public readonly List<BoundVar> Vars;
@@ -4543,8 +4562,9 @@ namespace Microsoft.Dafny {
{
public readonly List<Expression> Operands;
public readonly List<BinaryExpr.Opcode> Operators;
+ public readonly List<Expression/*?*/> PrefixLimits;
public readonly Expression E;
- public ChainingExpression(IToken tok, List<Expression> operands, List<BinaryExpr.Opcode> operators, Expression desugaring)
+ public ChainingExpression(IToken tok, List<Expression> operands, List<BinaryExpr.Opcode> operators, List<Expression/*?*/> prefixLimits, Expression desugaring)
: base(tok) {
Contract.Requires(tok != null);
Contract.Requires(operands != null);
@@ -4554,6 +4574,7 @@ namespace Microsoft.Dafny {
Operands = operands;
Operators = operators;
+ PrefixLimits = prefixLimits;
E = desugaring;
}
}
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 47fb0d3f..7b62344c 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1398,7 +1398,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
PrintStmt(out s);
break;
}
- case 1: case 2: case 23: case 27: case 103: case 104: case 105: case 106: case 107: case 108: {
+ case 1: case 2: case 23: case 27: case 104: case 105: case 106: case 107: case 108: case 109: {
UpdateStmt(out s);
break;
}
@@ -2327,6 +2327,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
IToken x, firstOpTok = null; Expression e0, e1, acc = null; BinaryExpr.Opcode op;
List<Expression> chain = null;
List<BinaryExpr.Opcode> ops = null;
+ List<Expression/*?*/> prefixLimits = null;
+ Expression k;
int kind = 0; // 0 ("uncommitted") indicates chain of ==, possibly with one !=
// 1 ("ascending") indicates chain of ==, <, <=, possibly with one !=
// 2 ("descending") indicates chain of ==, >, >=, possibly with one !=
@@ -2337,18 +2339,24 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Term(out e0);
e = e0;
if (StartOf(24)) {
- RelOp(out x, out op);
+ RelOp(out x, out op, out k);
firstOpTok = x;
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.
+ if (k == null) {
+ 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.
+ } else {
+ Contract.Assert(op == BinaryExpr.Opcode.Eq || op == BinaryExpr.Opcode.Neq);
+ e = new TernaryExpr(x, op == BinaryExpr.Opcode.Eq ? TernaryExpr.Opcode.PrefixEqOp : TernaryExpr.Opcode.PrefixNeqOp, k, e0, e1);
+ }
while (StartOf(24)) {
if (chain == null) {
chain = new List<Expression>();
ops = new List<BinaryExpr.Opcode>();
- chain.Add(e0); ops.Add(op); chain.Add(e1);
+ prefixLimits = new List<Expression>();
+ chain.Add(e0); ops.Add(op); prefixLimits.Add(k); chain.Add(e1);
switch (op) {
case BinaryExpr.Opcode.Eq:
kind = 0; break;
@@ -2368,7 +2376,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
e0 = e1;
- RelOp(out x, out op);
+ RelOp(out x, out op, out k);
switch (op) {
case BinaryExpr.Opcode.Eq:
if (kind != 0 && kind != 1 && kind != 2) { SemErr(x, "chaining not allowed from the previous operator"); }
@@ -2396,18 +2404,21 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
Term(out e1);
- ops.Add(op); chain.Add(e1);
- if (op == BinaryExpr.Opcode.Disjoint) {
+ ops.Add(op); prefixLimits.Add(k); chain.Add(e1);
+ if (k != null) {
+ Contract.Assert(op == BinaryExpr.Opcode.Eq || op == BinaryExpr.Opcode.Neq);
+ e = new TernaryExpr(x, op == BinaryExpr.Opcode.Eq ? TernaryExpr.Opcode.PrefixEqOp : TernaryExpr.Opcode.PrefixNeqOp, k, e0, e1);
+ } else 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
+ } else {
e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, e0, e1));
+ }
}
}
if (chain != null) {
- e = new ChainingExpression(firstOpTok, chain, ops, e);
+ e = new ChainingExpression(firstOpTok, chain, ops, prefixLimits, e);
}
}
@@ -2431,22 +2442,29 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
void Term(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
Factor(out e0);
- while (la.kind == 98 || la.kind == 99) {
+ while (la.kind == 99 || la.kind == 100) {
AddOp(out x, out op);
Factor(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
}
}
- void RelOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {
+ void RelOp(out IToken/*!*/ x, out BinaryExpr.Opcode op, out Expression k) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null);
x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
IToken y;
+ k = null;
switch (la.kind) {
case 28: {
Get();
x = t; op = BinaryExpr.Opcode.Eq;
+ if (la.kind == 95) {
+ Get();
+ Expect(67);
+ Expression(out k);
+ Expect(68);
+ }
break;
}
case 34: {
@@ -2472,22 +2490,28 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
case 83: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
+ if (la.kind == 95) {
+ Get();
+ Expect(67);
+ Expression(out k);
+ Expect(68);
+ }
break;
}
- case 95: {
+ case 96: {
Get();
x = t; op = BinaryExpr.Opcode.Disjoint;
break;
}
- case 96: {
+ case 97: {
Get();
x = t; op = BinaryExpr.Opcode.In;
break;
}
- case 97: {
+ case 98: {
Get();
x = t; y = Token.NoToken;
- if (la.kind == 96) {
+ if (la.kind == 97) {
Get();
y = t;
}
@@ -2524,7 +2548,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
void Factor(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
UnaryExpression(out e0);
- while (la.kind == 57 || la.kind == 100 || la.kind == 101) {
+ while (la.kind == 57 || la.kind == 101 || la.kind == 102) {
MulOp(out x, out op);
UnaryExpression(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -2533,10 +2557,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
void AddOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryExpr.Opcode.Add/*(dummy)*/;
- if (la.kind == 98) {
+ if (la.kind == 99) {
Get();
x = t; op = BinaryExpr.Opcode.Add;
- } else if (la.kind == 99) {
+ } else if (la.kind == 100) {
Get();
x = t; op = BinaryExpr.Opcode.Sub;
} else SynErr(194);
@@ -2545,14 +2569,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
void UnaryExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr;
switch (la.kind) {
- case 99: {
+ case 100: {
Get();
x = t;
UnaryExpression(out e);
e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e);
break;
}
- case 97: case 102: {
+ case 98: case 103: {
NegOp();
x = t;
UnaryExpression(out e);
@@ -2599,7 +2623,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else SynErr(195);
break;
}
- case 2: case 23: case 27: case 103: case 104: case 105: case 106: case 107: case 108: {
+ case 2: case 23: case 27: case 104: case 105: case 106: case 107: case 108: case 109: {
ConstAtomExpression(out e);
while (la.kind == 17 || la.kind == 67) {
Suffix(ref e);
@@ -2615,19 +2639,19 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (la.kind == 57) {
Get();
x = t; op = BinaryExpr.Opcode.Mul;
- } else if (la.kind == 100) {
+ } else if (la.kind == 101) {
Get();
x = t; op = BinaryExpr.Opcode.Div;
- } else if (la.kind == 101) {
+ } else if (la.kind == 102) {
Get();
x = t; op = BinaryExpr.Opcode.Mod;
} else SynErr(197);
}
void NegOp() {
- if (la.kind == 97) {
+ if (la.kind == 98) {
Get();
- } else if (la.kind == 102) {
+ } else if (la.kind == 103) {
Get();
} else SynErr(198);
}
@@ -2642,7 +2666,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Get();
x = t;
Expression(out e);
- Expect(109);
+ Expect(110);
Expression(out e0);
Expect(71);
Expression(out e1);
@@ -2703,17 +2727,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Ident(out id);
idents.Add(id);
}
- if (la.kind == 27 || la.kind == 110) {
+ if (la.kind == 27 || la.kind == 95) {
args = new List<Expression>();
- if (la.kind == 110) {
+ if (la.kind == 95) {
Get();
- Expression k = new ImplicitIdentifierExpr(t, "_k");
- if (la.kind == 67) {
- Get();
- Expression(out k);
- Expect(68);
- }
- id.val = id.val + "#"; args.Add(k);
+ id.val = id.val + "#"; Expression k;
+ Expect(67);
+ Expression(out k);
+ Expect(68);
+ args.Add(k);
}
Expect(27);
openParen = t;
@@ -2734,17 +2756,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (la.kind == 17) {
Get();
Ident(out id);
- if (la.kind == 27 || la.kind == 110) {
+ if (la.kind == 27 || la.kind == 95) {
args = new List<Expression/*!*/>(); func = true;
- if (la.kind == 110) {
+ if (la.kind == 95) {
Get();
- Expression k = new ImplicitIdentifierExpr(t, "_k");
- if (la.kind == 67) {
- Get();
- Expression(out k);
- Expect(68);
- }
- id.val = id.val + "#"; args.Add(k);
+ id.val = id.val + "#"; Expression k;
+ Expect(67);
+ Expression(out k);
+ Expect(68);
+ args.Add(k);
}
Expect(27);
IToken openParen = t;
@@ -2906,17 +2926,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = dummyExpr;
switch (la.kind) {
- case 103: {
+ case 104: {
Get();
e = new LiteralExpr(t, false);
break;
}
- case 104: {
+ case 105: {
Get();
e = new LiteralExpr(t, true);
break;
}
- case 105: {
+ case 106: {
Get();
e = new LiteralExpr(t);
break;
@@ -2926,12 +2946,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = new LiteralExpr(t, n);
break;
}
- case 106: {
+ case 107: {
Get();
e = new ThisExpr(t);
break;
}
- case 107: {
+ case 108: {
Get();
x = t;
Expect(27);
@@ -2940,7 +2960,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = new FreshExpr(x, e);
break;
}
- case 108: {
+ case 109: {
Get();
x = t;
Expect(27);
@@ -3190,7 +3210,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
static readonly bool[,]/*!*/ set = {
- {T,T,T,x, x,x,T,x, x,x,x,x, x,x,T,x, x,x,T,T, x,T,T,T, T,x,x,T, x,x,T,x, x,T,x,x, T,T,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,T,x,x, x,x,T,x, x,x,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x},
+ {T,T,T,x, x,x,T,x, x,x,x,x, x,x,T,x, x,x,T,T, x,T,T,T, T,x,x,T, x,x,T,x, x,T,x,x, T,T,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,T,x,x, x,x,T,x, x,x,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x},
{x,x,x,x, x,x,x,x, T,T,x,T, x,x,x,x, x,x,T,T, T,T,T,x, T,x,T,x, x,x,T,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
@@ -3200,24 +3220,24 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
{x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, T,x,x,x, x,x,T,T, x,x,x,x, x,T,x,T, x,x,T,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,T,T, T,T,T,T, T,x,x,x, T,T,T,T, x,x,x,x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, T,x,x,x, x,x,T,T, x,x,x,x, x,T,x,T, x,x,T,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,T,x,x, x,x,T,x, x,x,T,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,T,x,x, x,x,T,x, x,x,T,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x},
{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, T,x,x,x, x,x,x,T, x,x,x,x, x,T,x,T, x,x,T,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,T,T, T,T,T,T, T,x,x,x, T,T,T,T, x,x,x,x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, T,x,x,x, x,T,T,T, x,x,x,x, x,T,x,T, x,x,T,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,T,T, T,T,T,T, T,x,x,x, T,T,T,T, x,x,x,x},
- {T,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,T,x,x, x,x,T,x, x,x,T,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, T,x,x,x, x,x,x,T, x,x,x,x, x,T,x,T, x,x,T,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, T,x,x,x, x,T,T,T, x,x,x,x, x,T,x,T, x,x,T,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x},
+ {T,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,T,x,x, x,x,T,x, x,x,T,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x},
{x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, T,x,x,x, x,x,x,T, x,x,x,x, x,T,x,T, x,x,T,x, x,x,x,x, T,T,x,x, T,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,T,x,T, x,x,T,T, T,T,T,T, T,x,x,x, T,T,T,T, x,x,x,x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, T,x,x,x, x,T,x,T, x,x,x,x, x,T,T,T, x,T,T,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,T,T, T,T,T,T, T,x,x,x, T,T,T,T, x,x,x,x},
- {x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, T,x,x,x, x,x,x,T, x,x,x,x, x,T,x,T, x,x,T,x, x,x,x,x, T,T,x,x, T,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, T,x,x,x, x,T,x,T, x,x,x,x, x,T,T,T, x,T,T,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x},
+ {x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,T,T, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,T,x, x,x,x,x, T,x,x,T, T,T,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,T,x,T, x,x,x,x, T,T,x,x},
- {x,x,x,x, x,x,T,T, x,x,x,x, x,x,T,x, x,T,x,x, x,x,x,T, x,T,x,x, T,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,T,x, x,x,x,T, T,x,x,T, T,T,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,T,x,T, x,x,x,x, T,T,x,x},
- {x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, T,x,x,x, x,x,x,T, x,x,x,x, x,T,x,T, x,x,T,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,T,T, T,T,T,T, T,x,x,x, T,T,T,T, x,x,x,x}
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,x,x,x, x,x,T,T, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,T,x, x,x,x,x, T,x,x,T, T,T,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,T,T, T,T,T,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,T,T, x,x,x,x, T,T,x,x},
+ {x,x,x,x, x,x,T,T, x,x,x,x, x,x,T,x, x,T,x,x, x,x,x,T, x,T,x,x, T,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,T,x, x,x,x,T, T,x,x,T, T,T,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,T,T, T,T,T,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,T,T, x,x,x,x, T,T,x,x},
+ {x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, T,x,x,x, x,x,x,T, x,x,x,x, x,T,x,T, x,x,T,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x}
};
} // end Parser
@@ -3337,22 +3357,22 @@ public class Errors {
case 92: s = "\"\\u2227\" expected"; break;
case 93: s = "\"||\" expected"; break;
case 94: s = "\"\\u2228\" expected"; break;
- case 95: s = "\"!!\" expected"; break;
- case 96: s = "\"in\" expected"; break;
- case 97: s = "\"!\" expected"; break;
- case 98: s = "\"+\" expected"; break;
- case 99: s = "\"-\" expected"; break;
- case 100: s = "\"/\" expected"; break;
- case 101: s = "\"%\" expected"; break;
- case 102: s = "\"\\u00ac\" expected"; break;
- case 103: s = "\"false\" expected"; break;
- case 104: s = "\"true\" expected"; break;
- case 105: s = "\"null\" expected"; break;
- case 106: s = "\"this\" expected"; break;
- case 107: s = "\"fresh\" expected"; break;
- case 108: s = "\"old\" expected"; break;
- case 109: s = "\"then\" expected"; break;
- case 110: s = "\"#\" expected"; break;
+ case 95: s = "\"#\" expected"; break;
+ case 96: s = "\"!!\" expected"; break;
+ case 97: s = "\"in\" expected"; break;
+ case 98: s = "\"!\" expected"; break;
+ case 99: s = "\"+\" expected"; break;
+ case 100: s = "\"-\" expected"; break;
+ case 101: s = "\"/\" expected"; break;
+ case 102: s = "\"%\" expected"; break;
+ case 103: s = "\"\\u00ac\" expected"; break;
+ case 104: s = "\"false\" expected"; break;
+ case 105: s = "\"true\" expected"; break;
+ case 106: s = "\"null\" expected"; break;
+ case 107: s = "\"this\" expected"; break;
+ case 108: s = "\"fresh\" expected"; break;
+ case 109: s = "\"old\" expected"; break;
+ case 110: s = "\"then\" expected"; break;
case 111: s = "\"..\" expected"; break;
case 112: s = "\"forall\" expected"; break;
case 113: s = "\"\\u2200\" expected"; break;
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 55a793e5..9394ef40 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -1224,6 +1224,33 @@ namespace Microsoft.Dafny {
}
if (parensNeeded) { wr.Write(")"); }
+ } else if (expr is TernaryExpr) {
+ var e = (TernaryExpr)expr;
+ switch (e.Op) {
+ case TernaryExpr.Opcode.PrefixEqOp:
+ case TernaryExpr.Opcode.PrefixNeqOp:
+ var opBindingStrength = 0x30;
+ var fragileLeftContext = true;
+ var fragileRightContext = true;
+
+ int opBS = opBindingStrength & 0xF8;
+ int ctxtBS = contextBindingStrength & 0xF8;
+ bool parensNeeded = opBS < ctxtBS ||
+ (opBS == ctxtBS && (opBindingStrength != contextBindingStrength || fragileContext));
+
+ if (parensNeeded) { wr.Write("("); }
+ PrintExpr(e.E1, opBindingStrength, fragileLeftContext, false, -1);
+ wr.Write(" {0}#[", e.Op == TernaryExpr.Opcode.PrefixEqOp ? "==" : "!=");
+ PrintExpression(e.E0);
+ wr.Write("] ");
+ PrintExpr(e.E2, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, -1);
+ if (parensNeeded) { wr.Write(")"); }
+ break;
+ default:
+ Contract.Assert(false); // unexpected ternary operator
+ break;
+ }
+
} else if (expr is ChainingExpression) {
var e = (ChainingExpression)expr;
// determine if parens are needed
@@ -1237,7 +1264,13 @@ namespace Microsoft.Dafny {
PrintExpr(e.Operands[0], opBindingStrength, true, false, -1);
for (int i = 0; i < e.Operators.Count; i++) {
string op = BinaryExpr.OpcodeString(e.Operators[i]);
- wr.Write(" {0} ", op);
+ if (e.PrefixLimits[i] == null) {
+ wr.Write(" {0} ", op);
+ } else {
+ wr.Write(" {0}#[", op);
+ PrintExpression(e.PrefixLimits[i]);
+ wr.Write("] ");
+ }
PrintExpr(e.Operands[i+1], opBindingStrength, true, i == e.Operators.Count - 1 && (parensNeeded || isRightmost), -1);
}
if (parensNeeded) { wr.Write(")"); }
@@ -1388,11 +1421,9 @@ namespace Microsoft.Dafny {
rest.Add(a);
}
}
- if (!(k is ImplicitIdentifierExpr)) {
- wr.Write("[");
- PrintExpression(k);
- wr.Write("]");
- }
+ wr.Write("[");
+ PrintExpression(k);
+ wr.Write("]");
args = rest;
}
wr.Write("(");
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index b0dccf77..8a11e6a6 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1022,6 +1022,10 @@ namespace Microsoft.Dafny
var e = (BinaryExpr)expr;
return new BinaryExpr(e.tok, e.Op, CloneExpr(e.E0), CloneExpr(e.E1));
+ } else if (expr is TernaryExpr) {
+ var e = (TernaryExpr)expr;
+ return new TernaryExpr(e.tok, e.Op, CloneExpr(e.E0), CloneExpr(e.E1), CloneExpr(e.E2));
+
} else if (expr is ChainingExpression) {
var e = (ChainingExpression)expr;
return CloneExpr(e.E); // just clone the desugaring, since it's already available
@@ -1654,6 +1658,7 @@ namespace Microsoft.Dafny
CoPredicateChecks(e.Test, context, CallingPosition.Neither);
CoPredicateChecks(e.Thn, context, cp);
CoPredicateChecks(e.Els, context, cp);
+ return;
} else if (expr is LetExpr) {
var e = (LetExpr)expr;
CoPredicateChecks(e.Body, context, cp);
@@ -3205,7 +3210,10 @@ namespace Microsoft.Dafny
// In the remaining cases, proxy is a restricted proxy and t is a non-proxy
} else if (proxy is DatatypeProxy) {
- if (t.IsIndDatatype) {
+ var dtp = (DatatypeProxy)proxy;
+ if (!dtp.Co && t.IsIndDatatype) {
+ // all is fine, proxy can be redirected to t
+ } else if (dtp.Co && t.IsCoDatatype) {
// all is fine, proxy can be redirected to t
} else {
return false;
@@ -3287,7 +3295,7 @@ namespace Microsoft.Dafny
Contract.Ensures(!Contract.Result<bool>() || a.T != null || b.T != null);
if (a is DatatypeProxy) {
- if (b is DatatypeProxy) {
+ if (b is DatatypeProxy && ((DatatypeProxy)a).Co == ((DatatypeProxy)b).Co) {
// all is fine
a.T = b;
return true;
@@ -4733,10 +4741,6 @@ namespace Microsoft.Dafny
e.Var = scope.Find(e.Name);
if (e.Var != null) {
expr.Type = e.Var.Type;
- } else if (e is ImplicitIdentifierExpr) {
- // Evidently, the variable _k has been introduced in a context where it is not allowed. This is a symptom of
- // a prefix predicate being called without an explicit depth parameter in a context where a depth is expected.
- Error(expr, "a call to a prefix predicate/method in this context must explicitly specify a depth argument (given in square brackets just after the # sign)");
} else {
Error(expr, "Identifier does not denote a local variable, parameter, or bound variable: {0}", e.Name);
}
@@ -5005,12 +5009,12 @@ namespace Microsoft.Dafny
case BinaryExpr.Opcode.Le:
case BinaryExpr.Opcode.Add: {
if (e.Op == BinaryExpr.Opcode.Lt && e.E0.Type.IsIndDatatype) {
- if (!UnifyTypes(e.E1.Type, new DatatypeProxy())) {
+ if (!UnifyTypes(e.E1.Type, new DatatypeProxy(false))) {
Error(expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E1.Type);
}
expr.Type = Type.Bool;
} else if (e.Op == BinaryExpr.Opcode.Lt && e.E1.Type.IsIndDatatype) {
- if (!UnifyTypes(e.E0.Type, new DatatypeProxy())) {
+ if (!UnifyTypes(e.E0.Type, new DatatypeProxy(false))) {
Error(expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E0.Type);
}
expr.Type = Type.Bool;
@@ -5038,7 +5042,7 @@ namespace Microsoft.Dafny
case BinaryExpr.Opcode.Gt:
case BinaryExpr.Opcode.Ge: {
if (e.Op == BinaryExpr.Opcode.Gt && e.E0.Type.IsIndDatatype) {
- if (!UnifyTypes(e.E1.Type, new DatatypeProxy())) {
+ if (!UnifyTypes(e.E1.Type, new DatatypeProxy(false))) {
Error(expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E1.Type);
}
expr.Type = Type.Bool;
@@ -5085,6 +5089,30 @@ namespace Microsoft.Dafny
}
e.ResolvedOp = ResolveOp(e.Op, e.E1.Type);
+ } else if (expr is TernaryExpr) {
+ var e = (TernaryExpr)expr;
+ ResolveExpression(e.E0, twoState);
+ ResolveExpression(e.E1, twoState);
+ ResolveExpression(e.E2, twoState);
+ switch (e.Op) {
+ case TernaryExpr.Opcode.PrefixEqOp:
+ case TernaryExpr.Opcode.PrefixNeqOp:
+ if (!UnifyTypes(e.E0.Type, Type.Int)) {
+ Error(e.E0, "prefix-equality limit argument must be an integer expression (got {0})", e.E0.Type);
+ }
+ if (!UnifyTypes(e.E1.Type, new DatatypeProxy(true))) {
+ Error(expr, "arguments to prefix equality must be codatatypes (instead of {0})", e.E1.Type);
+ }
+ if (!UnifyTypes(e.E1.Type, e.E2.Type)) {
+ Error(expr, "arguments must have the same type (got {0} and {1})", e.E1.Type, e.E2.Type);
+ }
+ expr.Type = Type.Bool;
+ break;
+ default:
+ Contract.Assert(false); // unexpected ternary operator
+ break;
+ }
+
} else if (expr is LetExpr) {
var e = (LetExpr)expr;
foreach (var rhs in e.RHSs) {
@@ -5545,6 +5573,17 @@ namespace Microsoft.Dafny
break;
}
+ } else if (expr is TernaryExpr) {
+ var e = (TernaryExpr)expr;
+ switch (e.Op) {
+ case TernaryExpr.Opcode.PrefixEqOp:
+ case TernaryExpr.Opcode.PrefixNeqOp:
+ Error(expr, "prefix equalities are allowed only in specification and ghost contexts");
+ return;
+ default:
+ break;
+ }
+
} else if (expr is QuantifierExpr) {
var e = (QuantifierExpr)expr;
if (e.MissingBounds != null) {
@@ -6514,7 +6553,7 @@ namespace Microsoft.Dafny
return BinaryExpr.ResolvedOpcode.Disjoint;
}
case BinaryExpr.Opcode.Lt:
- if (operandType.IsIndDatatype || operandType is DatatypeProxy) {
+ if (operandType.IsIndDatatype || (operandType is DatatypeProxy && !((DatatypeProxy)operandType).Co)) {
return BinaryExpr.ResolvedOpcode.RankLt;
} else if (operandType is SetType) {
return BinaryExpr.ResolvedOpcode.ProperSubset;
@@ -6669,6 +6708,16 @@ namespace Microsoft.Dafny
return true;
}
return UsesSpecFeatures(e.E0) || UsesSpecFeatures(e.E1);
+ } else if (expr is TernaryExpr) {
+ var e = (TernaryExpr)expr;
+ switch (e.Op) {
+ case TernaryExpr.Opcode.PrefixEqOp:
+ case TernaryExpr.Opcode.PrefixNeqOp:
+ return true;
+ default:
+ break;
+ }
+ return UsesSpecFeatures(e.E0) || UsesSpecFeatures(e.E1) || UsesSpecFeatures(e.E2);
} else if (expr is NamedExpr) {
return moduleInfo.IsGhost ? false : UsesSpecFeatures(((NamedExpr)expr).Body);
} else if (expr is ComprehensionExpr) {
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index dc028be5..ccefe48d 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/Dafny/Scanner.cs
@@ -283,12 +283,12 @@ public class Scanner {
start[38] = 41;
start[8743] = 43;
start[8744] = 45;
- start[43] = 47;
- start[45] = 48;
- start[47] = 49;
- start[37] = 50;
- start[172] = 51;
- start[35] = 52;
+ start[35] = 46;
+ start[43] = 48;
+ start[45] = 49;
+ start[47] = 50;
+ start[37] = 51;
+ start[172] = 52;
start[8704] = 53;
start[8707] = 54;
start[8226] = 56;
@@ -544,14 +544,14 @@ public class Scanner {
case "print": t.kind = 78; break;
case "parallel": t.kind = 79; break;
case "calc": t.kind = 80; break;
- case "in": t.kind = 96; break;
- case "false": t.kind = 103; break;
- case "true": t.kind = 104; break;
- case "null": t.kind = 105; break;
- case "this": t.kind = 106; break;
- case "fresh": t.kind = 107; break;
- case "old": t.kind = 108; break;
- case "then": t.kind = 109; break;
+ case "in": t.kind = 97; break;
+ case "false": t.kind = 104; break;
+ case "true": t.kind = 105; break;
+ case "null": t.kind = 106; break;
+ case "this": t.kind = 107; break;
+ case "fresh": t.kind = 108; break;
+ case "old": t.kind = 109; break;
+ case "then": t.kind = 110; break;
case "forall": t.kind = 112; break;
case "exists": t.kind = 114; break;
default: break;
@@ -717,7 +717,7 @@ public class Scanner {
case 46:
{t.kind = 95; break;}
case 47:
- {t.kind = 98; break;}
+ {t.kind = 96; break;}
case 48:
{t.kind = 99; break;}
case 49:
@@ -727,7 +727,7 @@ public class Scanner {
case 51:
{t.kind = 102; break;}
case 52:
- {t.kind = 110; break;}
+ {t.kind = 103; break;}
case 53:
{t.kind = 113; break;}
case 54:
@@ -764,10 +764,10 @@ public class Scanner {
if (ch == '=') {AddCh(); goto case 31;}
else {t.kind = 35; break;}
case 63:
- recEnd = pos; recKind = 97;
+ recEnd = pos; recKind = 98;
if (ch == '=') {AddCh(); goto case 32;}
- else if (ch == '!') {AddCh(); goto case 46;}
- else {t.kind = 97; break;}
+ else if (ch == '!') {AddCh(); goto case 47;}
+ else {t.kind = 98; break;}
case 64:
recEnd = pos; recKind = 28;
if (ch == '>') {AddCh(); goto case 39;}
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 04ad8039..bd8475f2 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -564,7 +564,7 @@ namespace Microsoft.Dafny {
fff.Body = BplAnd(CoPrefixEquality(dt.tok, codecl, d0, d1, null/*TODO: BOGUS*/, true));
sink.TopLevelDeclarations.Add(fff);
- // axiom (forall d0, d1: DatatypeType :: { Eq$Dt(d0, d1) } Eq$Dt(d0, d1) ==> d0 == d1);
+ // axiom (forall d0, d1: DatatypeType :: { Eq$Dt(d0, d1) } Eq$Dt(d0, d1) <==> d0 == d1);
var d0Var = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "d0", predef.DatatypeType));
d0 = new Bpl.IdentifierExpr(dt.tok, d0Var);
var d1Var = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "d1", predef.DatatypeType));
@@ -572,7 +572,7 @@ namespace Microsoft.Dafny {
var eqDt = FunctionCall(dt.tok, "$Eq#" + dt.FullCompileName, Bpl.Type.Bool, d0, d1);
var eq = Bpl.Expr.Eq(d0, d1);
var tr = new Bpl.Trigger(dt.tok, true, new ExprSeq(eqDt));
- var ax = new Bpl.ForallExpr(dt.tok, new VariableSeq(d0Var, d1Var), tr, Bpl.Expr.Imp(eqDt, eq));
+ var ax = new Bpl.ForallExpr(dt.tok, new VariableSeq(d0Var, d1Var), tr, Bpl.Expr.Iff(eqDt, eq));
sink.TopLevelDeclarations.Add(new Bpl.Axiom(dt.tok, ax));
// And here's the limited version:
@@ -600,7 +600,8 @@ namespace Microsoft.Dafny {
// function $PrefixEqual#Dt(k: int, d0: DatatypeType, d1: DatatypeType): bool
// {
- // d0.head == d1.head && $PrefixEqual#0#Dt(k-1, d0.tail, d1.tail))
+ // 0 < k ==>
+ // (d0.head == d1.head && $PrefixEqual#0#Dt(k-1, d0.tail, d1.tail)))
// }
var peq_k = new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, "k", Bpl.Type.Int), true);
k = new Bpl.IdentifierExpr(dt.tok, peq_k);
@@ -612,7 +613,8 @@ namespace Microsoft.Dafny {
var peq1 = new Bpl.Function(dt.tok, CoPrefixName(codecl, false), new Bpl.VariableSeq(peq_k, peq_d0, peq_d1), peq_resType,
"prefix equality for codatatype " + dt.FullName);
var kMinusOne = Bpl.Expr.Sub(k, Bpl.Expr.Literal(1));
- peq1.Body = BplAnd(CoPrefixEquality(dt.tok, codecl, d0, d1, kMinusOne, true));
+ var z = Bpl.Expr.Lt(Bpl.Expr.Literal(0), k);
+ peq1.Body = Bpl.Expr.Imp(z, BplAnd(CoPrefixEquality(dt.tok, codecl, d0, d1, kMinusOne, true)));
sink.TopLevelDeclarations.Add(peq1);
// Add the 'limited' version:
@@ -637,7 +639,7 @@ namespace Microsoft.Dafny {
ax = new Bpl.ForallExpr(dt.tok, new VariableSeq(kVar, d0Var, d1Var), tr, Bpl.Expr.Eq(p1, p0));
sink.TopLevelDeclarations.Add(new Bpl.Axiom(dt.tok, ax));
- // Finally, the connection between the full codatatype equality and its prefix version
+ // The connection between the full codatatype equality and its prefix version
// axiom (forall d0, d1: DatatypeType :: $Eq#Dt(d0, d1) <==>
// (forall k: int :: 0 <= k ==> $PrefixEqual#Dt(k, d0, d1)));
kVar = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "k", Bpl.Type.Int));
@@ -653,6 +655,21 @@ namespace Microsoft.Dafny {
body = Bpl.Expr.Iff(eqDt, q);
q = new Bpl.ForallExpr(dt.tok, new VariableSeq(d0Var, d1Var), body);
sink.TopLevelDeclarations.Add(new Bpl.Axiom(dt.tok, q));
+
+ // With the axioms above, going from d0==d1 to a prefix equality requires going via the full codatatype
+ // equality, which in turn requires the full codatatype equality to be present. The following axiom
+ // provides a shortcut:
+ // axiom (forall d0, d1: DatatypeType, k: int :: d0 == d1 && 0 <= k ==> $PrefixEqual#_module.Stream(k, d0, d1));
+ kVar = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "k", Bpl.Type.Int));
+ k = new Bpl.IdentifierExpr(dt.tok, kVar);
+ d0Var = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "d0", predef.DatatypeType));
+ d0 = new Bpl.IdentifierExpr(dt.tok, d0Var);
+ d1Var = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "d1", predef.DatatypeType));
+ d1 = new Bpl.IdentifierExpr(dt.tok, d1Var);
+ prefixEq = FunctionCall(dt.tok, CoPrefixName(codecl, false), null, k, d0, d1);
+ body = Bpl.Expr.Imp(BplAnd(Bpl.Expr.Eq(d0, d1), Bpl.Expr.Le(Bpl.Expr.Literal(0), k)), prefixEq);
+ q = new Bpl.ForallExpr(dt.tok, new VariableSeq(kVar, d0Var, d1Var), body);
+ sink.TopLevelDeclarations.Add(new Bpl.Axiom(dt.tok, q));
}
}
@@ -2528,6 +2545,23 @@ namespace Microsoft.Dafny {
}
Bpl.Expr r = BplAnd(t0, t1);
return z == null ? r : BplAnd(r, z);
+
+ } else if (expr is TernaryExpr) {
+ var e = (TernaryExpr)expr;
+ var t0 = IsTotal(e.E0, etran);
+ var t1 = IsTotal(e.E1, etran);
+ var t2 = IsTotal(e.E2, etran);
+ switch (e.Op) {
+ case TernaryExpr.Opcode.PrefixEqOp:
+ case TernaryExpr.Opcode.PrefixNeqOp:
+ var z = Bpl.Expr.Le(Bpl.Expr.Literal(0), etran.TrExpr(e.E0));
+ return BplAnd(
+ BplAnd(IsTotal(e.E0, etran), z),
+ BplAnd(IsTotal(e.E1, etran), IsTotal(e.E2, etran)));
+ default:
+ Contract.Assert(false); throw new cce.UnreachableException(); // unexpected ternary expression
+ }
+
} else if (expr is LetExpr) {
var e = (LetExpr)expr;
Bpl.Expr total = Bpl.Expr.True;
@@ -2686,6 +2720,10 @@ namespace Microsoft.Dafny {
break;
}
return BplAnd(t0, t1);
+ } else if (expr is TernaryExpr) {
+ var e = (TernaryExpr)expr;
+ return BplAnd(CanCallAssumption(e.E0, etran), BplAnd(CanCallAssumption(e.E1, etran), CanCallAssumption(e.E2, etran)));
+
} else if (expr is LetExpr) {
var e = (LetExpr)expr;
Bpl.Expr canCall = Bpl.Expr.True;
@@ -3182,6 +3220,22 @@ namespace Microsoft.Dafny {
break;
}
+ } else if (expr is TernaryExpr) {
+ var e = (TernaryExpr)expr;
+ foreach (var ee in e.SubExpressions) {
+ CheckWellformed(ee, options, locals, builder, etran);
+ }
+ switch (e.Op) {
+ case TernaryExpr.Opcode.PrefixEqOp:
+ case TernaryExpr.Opcode.PrefixNeqOp:
+ builder.Add(Assert(expr.tok, Bpl.Expr.Le(Bpl.Expr.Literal(0), etran.TrExpr(e.E0)), "prefix-equality limit must be at least 0", options.AssertKv));
+
+ break;
+ default:
+ Contract.Assert(false); // unexpected ternary expression
+ break;
+ }
+
} else if (expr is LetExpr) {
var e = (LetExpr)expr;
@@ -7484,6 +7538,25 @@ namespace Microsoft.Dafny {
}
return Bpl.Expr.Binary(expr.tok, bOpcode, e0, e1);
+ } else if (expr is TernaryExpr) {
+ var e = (TernaryExpr)expr;
+ var e0 = TrExpr(e.E0);
+ var e1 = TrExpr(e.E1);
+ var e2 = TrExpr(e.E2);
+ switch (e.Op) {
+ case TernaryExpr.Opcode.PrefixEqOp:
+ case TernaryExpr.Opcode.PrefixNeqOp:
+ var cot = e.E1.Type.AsCoDatatype;
+ Contract.Assert(cot != null); // the argument types of prefix equality (and prefix disequality) are codatatypes
+ var r = translator.FunctionCall(expr.tok, CoPrefixName(cot, false), Bpl.Type.Bool, e0, e1, e2);
+ if (e.Op == TernaryExpr.Opcode.PrefixEqOp) {
+ return r;
+ } else {
+ return Bpl.Expr.Unary(expr.tok, UnaryOperator.Opcode.Not, r);
+ }
+ default:
+ Contract.Assert(false); throw new cce.UnreachableException(); // unexpected ternary expression
+ }
} else if (expr is LetExpr) {
var e = (LetExpr)expr;
return TrExpr(GetSubstitutedBody(e));
@@ -8535,9 +8608,14 @@ namespace Microsoft.Dafny {
} else if (position && coContextDepth != null && bin.ResolvedOp == BinaryExpr.ResolvedOpcode.EqCommon && bin.E0.Type.IsCoDatatype) {
var codecl = bin.E0.Type.AsCoDatatype;
Contract.Assert(codecl != null);
- foreach (var c in CoPrefixEquality(bin.tok, codecl, etran.TrExpr(bin.E0), etran.TrExpr(bin.E1), etran.TrExpr(coContextDepth), false)) {
- splits.Add(new SplitExprInfo(SplitExprInfo.K.Both, c));
- }
+ var k = etran.TrExpr(coContextDepth);
+ var e0 = etran.TrExpr(bin.E0);
+ var e1 = etran.TrExpr(bin.E1);
+ var coEqK = FunctionCall(bin.tok, CoPrefixName(codecl, false), null, k, e0, e1);
+ foreach (var c in CoPrefixEquality(bin.tok, codecl, e0, e1, k, false)) {
+ splits.Add(new SplitExprInfo(SplitExprInfo.K.Checked, BplOr(coEqK, c)));
+ }
+ splits.Add(new SplitExprInfo(SplitExprInfo.K.Free, coEqK));
return true;
#if SOON
} else if (position && coContextDepth == 1 && bin.ResolvedOp == BinaryExpr.ResolvedOpcode.EqCommon && bin.E0.Type.IsCoDatatype) {
@@ -8800,8 +8878,8 @@ namespace Microsoft.Dafny {
translatedExpression = etran.TrExpr(expr);
splitHappened = etran.Statistics_CustomLayerFunctionCount != 0; // return true if the LayerOffset(1) came into play
}
- // TODO: Is the the following call to ContainsChange expensive? It's linear in the size of "expr", but we get here many times in TrSpliExpr, so wouldn't the total
- // time in the size of the expression passed to the first TrSpliExpr be quadratic?
+ // TODO: Is the the following call to ContainsChange expensive? It's linear in the size of "expr", but we get here many times in TrSplitExpr, so wouldn't the total
+ // time in the size of the expression passed to the first TrSplitExpr be quadratic?
if (RefinementToken.IsInherited(expr.tok, currentModule) && (codeContext == null || !codeContext.MustReverify) && RefinementTransformer.ContainsChange(expr, currentModule)) {
// If "expr" contains a subexpression that has changed from the inherited expression, we'll destructively
// change the token of the translated expression to make it look like it's not inherited. This will cause "e" to
@@ -8961,7 +9039,7 @@ namespace Microsoft.Dafny {
/// <summary>
/// Worker routine for VarOccursInArgumentToRecursiveFunction(expr,n), where the additional parameter 'exprIsProminent' says whether or
- /// not 'expr' prominent status in its context.
+ /// not 'expr' has prominent status in its context.
/// DafnyInductionHeuristic cases 0 and 1 are assumed to be handled elsewhere (i.e., a precondition of this method is DafnyInductionHeuristic is at least 2).
/// Parameter 'n' is allowed to be a ThisSurrogate.
/// </summary>
@@ -9024,6 +9102,17 @@ namespace Microsoft.Dafny {
}
}
return false;
+ } else if (expr is TernaryExpr) {
+ var e = (TernaryExpr)expr;
+ switch (e.Op) {
+ case TernaryExpr.Opcode.PrefixEqOp:
+ case TernaryExpr.Opcode.PrefixNeqOp:
+ return VarOccursInArgumentToRecursiveFunction(e.E0, n, true) ||
+ VarOccursInArgumentToRecursiveFunction(e.E1, n, subExprIsProminent) ||
+ VarOccursInArgumentToRecursiveFunction(e.E2, n, subExprIsProminent);
+ default:
+ Contract.Assert(false); throw new cce.UnreachableException(); // unexpected ternary expression
+ }
} else if (expr is DatatypeValue) {
var e = (DatatypeValue)expr;
var q = n.Type.IsDatatype ? exprIsProminent : subExprIsProminent; // prominent status continues, if we're looking for a variable whose type is a datatype
@@ -9345,6 +9434,15 @@ namespace Microsoft.Dafny {
newExpr = newBin;
}
+ } else if (expr is TernaryExpr) {
+ var e = (TernaryExpr)expr;
+ var e0 = Substitute(e.E0);
+ var e1 = Substitute(e.E1);
+ var e2 = Substitute(e.E2);
+ if (e0 != e.E0 || e1 != e.E1 || e2 != e.E2) {
+ newExpr = new TernaryExpr(expr.tok, e.Op, e0, e1, e2);
+ }
+
} else if (expr is LetExpr) {
var e = (LetExpr)expr;
var rhss = new List<Expression>();
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 964b69a4..87e6e93f 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1327,20 +1327,12 @@ Execution trace:
Dafny program verifier finished with 5 verified, 2 errors
-------------------- CoResolution.dfy --------------------
-CoResolution.dfy(22,8): Error: a call to a prefix predicate/method in this context must explicitly specify a depth argument (given in square brackets just after the # sign)
-CoResolution.dfy(23,3): Error: a call to a prefix predicate/method in this context must explicitly specify a depth argument (given in square brackets just after the # sign)
-CoResolution.dfy(24,7): Error: member Undeclared# does not exist in class _default
-CoResolution.dfy(25,7): Error: member Undeclared# does not exist in class _default
-CoResolution.dfy(26,2): Error: unresolved identifier: Undeclared#
-CoResolution.dfy(26,12): Error: a call to a prefix predicate/method in this context must explicitly specify a depth argument (given in square brackets just after the # sign)
-CoResolution.dfy(27,2): Error: unresolved identifier: Undeclared#
-CoResolution.dfy(30,2): Error: wrong number of function arguments (got 3, expected 2)
-CoResolution.dfy(31,5): Error: unresolved identifier: _k
-CoResolution.dfy(37,30): Error: a call to a prefix predicate/method in this context must explicitly specify a depth argument (given in square brackets just after the # sign)
-CoResolution.dfy(38,20): Error: a call to a prefix predicate/method in this context must explicitly specify a depth argument (given in square brackets just after the # sign)
-CoResolution.dfy(41,9): Error: a call to a prefix predicate/method in this context must explicitly specify a depth argument (given in square brackets just after the # sign)
-CoResolution.dfy(42,4): Error: a call to a prefix predicate/method in this context must explicitly specify a depth argument (given in square brackets just after the # sign)
-13 resolution/type errors detected in CoResolution.dfy
+CoResolution.dfy(43,8): Error: == can only be applied to expressions of types that support equality (got Stream<_T0>)
+CoResolution.dfy(54,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+CoResolution.dfy(22,7): Error: member Undeclared# does not exist in class _default
+CoResolution.dfy(23,2): Error: unresolved identifier: Undeclared#
+CoResolution.dfy(26,5): Error: unresolved identifier: _k
+5 resolution/type errors detected in CoResolution.dfy
-------------------- CoPrefix.dfy --------------------
CoPrefix.dfy(61,7): Error: failure to decrease termination measure
@@ -1348,7 +1340,7 @@ Execution trace:
(0,0): anon0
(0,0): anon5_Else
(0,0): anon6_Then
-CoPrefix.dfy(74,7): Error: failure to decrease termination measure
+CoPrefix.dfy(74,7): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon5_Else
@@ -1358,8 +1350,12 @@ CoPrefix.dfy(111,11): Related location: This is the postcondition that might not
CoPrefix.dfy(99,17): Related location: Related location
Execution trace:
(0,0): anon0
+CoPrefix.dfy(136,25): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon7_Then
-Dafny program verifier finished with 17 verified, 3 errors
+Dafny program verifier finished with 23 verified, 4 errors
-------------------- CoinductiveProofs.dfy --------------------
CoinductiveProofs.dfy(26,12): Error: assertion violation
@@ -1401,7 +1397,7 @@ CoinductiveProofs.dfy(152,22): Related location: This is the postcondition that
Execution trace:
(0,0): anon0
-Dafny program verifier finished with 32 verified, 8 errors
+Dafny program verifier finished with 35 verified, 8 errors
-------------------- TypeAntecedents.dfy --------------------
TypeAntecedents.dfy(32,13): Error: assertion violation
diff --git a/Test/dafny0/CoResolution.dfy b/Test/dafny0/CoResolution.dfy
index 233a818b..3146147e 100644
--- a/Test/dafny0/CoResolution.dfy
+++ b/Test/dafny0/CoResolution.dfy
@@ -19,25 +19,49 @@ copredicate D()
copredicate S(d: set<int>)
{
- this.S#(d) && // error: the call to S# must give an explicit depth argument
- S#(d) && // error: the call to S# must give an explicit depth argument
- this.Undeclared#(d) && // error: 'Undeclared#' is undeclared, and depth argument is left implicit
this.Undeclared#[5](d) && // error: 'Undeclared#' is undeclared
- Undeclared#(d) && // error: 'Undeclared#' is undeclared, and depth argument is left implicit
Undeclared#[5](d) && // error: 'Undeclared#' is undeclared
this.S#[5](d) &&
S#[5](d) &&
- S#(5, d) && // error: the '5' here does not give the depth argument
S#[_k](d) // error: _k is not an identifier in scope
}
comethod CM(d: set<int>)
{
var b;
- b := this.S#[5](d) && this.S#(d + d); // error: cannot rely on implicit depth argument here
- b := S#[5](d) && S#(d + d); // error: cannot rely on implicit depth argument here
+ b := this.S#[5](d);
+ b := S#[5](d);
this.CM#[5](d);
CM#[5](d);
- this.CM#(d + d); // error: must give an explicit depth argument
- CM#(d + d); // error: must give an explicit depth argument
+}
+
+module GhostCheck0 {
+ codatatype Stream<G> = Cons(head: G, tail: Stream);
+ method UseStream0(s: Stream)
+ {
+ var x := 3;
+ if (s == s.tail) { // error: this operation is allowed only in ghost contexts
+ x := x + 2;
+ }
+ }
+}
+module GhostCheck1 {
+ codatatype Stream<G> = Cons(head: G, tail: Stream);
+ method UseStream1(s: Stream)
+ {
+ var x := 3;
+ if (s ==#[20] s.tail) { // this seems innocent enough, but it's currently not supported by the compiler, so...
+ x := x + 7; // error: therefore, this is an error
+ }
+ }
+}
+module GhostCheck2 {
+ codatatype Stream<G> = Cons(head: G, tail: Stream);
+ ghost method UseStreamGhost(s: Stream)
+ {
+ var x := 3;
+ if (s == s.tail) { // fine
+ x := x + 2;
+ }
+ }
}
diff --git a/Test/dafny0/CoinductiveProofs.dfy b/Test/dafny0/CoinductiveProofs.dfy
index ddb23b5b..47c5f262 100644
--- a/Test/dafny0/CoinductiveProofs.dfy
+++ b/Test/dafny0/CoinductiveProofs.dfy
@@ -153,3 +153,28 @@ comethod BadEquality1(n: int)
{ // error: postcondition does not hold
BadEquality1(n+1);
}
+
+// test that match statements/expressions get the correct assumption (which wasn't always the case)
+
+codatatype IList<T> = INil | ICons(head: T, tail: IList<T>);
+
+ghost method M(s: IList)
+{
+ match (s) {
+ case INil =>
+ assert s == INil;
+ case ICons(a, b) =>
+ assert s == ICons(a, b);
+ }
+}
+
+function G(s: IList): int
+{
+ match s
+ case INil =>
+ assert s == INil;
+ 0
+ case ICons(a, b) =>
+ assert s == ICons(a, b);
+ 0
+}
diff --git a/Test/dafny3/Answer b/Test/dafny3/Answer
index 5ab835e7..9cd8fc82 100644
--- a/Test/dafny3/Answer
+++ b/Test/dafny3/Answer
@@ -5,7 +5,7 @@ Dafny program verifier finished with 15 verified, 0 errors
-------------------- Streams.dfy --------------------
-Dafny program verifier finished with 38 verified, 0 errors
+Dafny program verifier finished with 50 verified, 0 errors
-------------------- Dijkstra.dfy --------------------
diff --git a/Test/dafny3/Streams.dfy b/Test/dafny3/Streams.dfy
index 1369e584..757d6a37 100644
--- a/Test/dafny3/Streams.dfy
+++ b/Test/dafny3/Streams.dfy
@@ -49,13 +49,35 @@ comethod Theorem0(M: Stream<X>)
Theorem0(N);
}
}
-comethod Theorem0_alt(M: Stream<X>)
+comethod Theorem0_Alt(M: Stream<X>)
ensures map_fg(M) == map_f(map_g(M));
{
if (M.Cons?) {
- Theorem0(M.tail);
+ Theorem0_Alt(M.tail);
}
}
+ghost method Theorem0_Par(M: Stream<X>)
+ ensures map_fg(M) == map_f(map_g(M));
+{
+ parallel (k: nat) {
+ Theorem0_Ind(k, M);
+ }
+}
+ghost method Theorem0_Ind(k: nat, M: Stream<X>)
+ ensures map_fg(M) ==#[k] map_f(map_g(M));
+{
+ if (k != 0) {
+ match (M) {
+ case Nil =>
+ case Cons(x, N) =>
+ Theorem0_Ind(k-1, N);
+ }
+ }
+}
+ghost method Theorem0_AutoInd(k: nat, M: Stream<X>)
+ ensures map_fg(M) ==#[k] map_f(map_g(M));
+// { // TODO: this is not working yet, apparently
+// }
// map f (append M N) = append (map f M) (map f N)
comethod Theorem1(M: Stream<X>, N: Stream<X>)
@@ -67,13 +89,40 @@ comethod Theorem1(M: Stream<X>, N: Stream<X>)
Theorem1(M', N);
}
}
-comethod Theorem1_alt(M: Stream<X>, N: Stream<X>)
+comethod Theorem1_Alt(M: Stream<X>, N: Stream<X>)
ensures map_f(append(M, N)) == append(map_f(M), map_f(N));
{
if (M.Cons?) {
- Theorem1(M.tail, N);
+ Theorem1_Alt(M.tail, N);
}
}
+ghost method Theorem1_Par(M: Stream<X>, N: Stream<X>)
+ ensures map_f(append(M, N)) == append(map_f(M), map_f(N));
+{
+ parallel (k: nat) {
+ Theorem1_Ind(k, M, N);
+ }
+}
+ghost method Theorem1_Ind(k: nat, M: Stream<X>, N: Stream<X>)
+ ensures map_f(append(M, N)) ==#[k] append(map_f(M), map_f(N));
+{
+ // this time, try doing the 'if' inside the 'match' (instead of the other way around)
+ match (M) {
+ case Nil =>
+ case Cons(x, M') =>
+ if (k != 0) {
+ Theorem1_Ind(k-1, M', N);
+ }
+ }
+}
+ghost method Theorem1_AutoInd(k: nat, M: Stream<X>, N: Stream<X>)
+ ensures map_f(append(M, N)) ==#[k] append(map_f(M), map_f(N));
+// { // TODO: this is not working yet, apparently
+// }
+ghost method Theorem1_AutoForall()
+{
+// assert forall k: nat, M, N :: map_f(append(M, N)) ==#[k] append(map_f(M), map_f(N)); // TODO: this is not working yet, apparently
+}
// append NIL M = M
ghost method Theorem2(M: Stream<X>)
@@ -92,11 +141,11 @@ comethod Theorem3(M: Stream<X>)
Theorem3(N);
}
}
-comethod Theorem3_alt(M: Stream<X>)
+comethod Theorem3_Alt(M: Stream<X>)
ensures append(M, Nil) == M;
{
if (M.Cons?) {
- Theorem3(M.tail);
+ Theorem3_Alt(M.tail);
}
}
@@ -110,11 +159,11 @@ comethod Theorem4(M: Stream<X>, N: Stream<X>, P: Stream<X>)
Theorem4(M', N, P);
}
}
-comethod Theorem4_alt(M: Stream<X>, N: Stream<X>, P: Stream<X>)
+comethod Theorem4_Alt(M: Stream<X>, N: Stream<X>, P: Stream<X>)
ensures append(M, append(N, P)) == append(append(M, N), P);
{
if (M.Cons?) {
- Theorem4(M.tail, N, P);
+ Theorem4_Alt(M.tail, N, P);
}
}
@@ -122,7 +171,7 @@ comethod Theorem4_alt(M: Stream<X>, N: Stream<X>, P: Stream<X>)
// Flatten can't be written as just:
//
-// function SimpleFlatten<T>(M: Stream<Stream>): Stream
+// function SimpleFlatten(M: Stream<Stream>): Stream
// {
// match M
// case Nil => Nil
@@ -130,9 +179,9 @@ comethod Theorem4_alt(M: Stream<X>, N: Stream<X>, P: Stream<X>)
// }
//
// because this function fails to be productive given an infinite stream of Nil's.
-// Instead, here are two variations SimpleFlatten. The first variation (FlattenStartMarker)
+// Instead, here are two variations of SimpleFlatten. The first variation (FlattenStartMarker)
// prepends a "startMarker" to each of the streams in "M". The other (FlattenNonEmpties)
-// insists that "M" contains no empty streams. One can prove a theorem that relates these
+// insists that "M" contain no empty streams. One can prove a theorem that relates these
// two versions.
// This first variation of Flatten returns a stream of the streams in M, each preceded with
@@ -140,18 +189,18 @@ comethod Theorem4_alt(M: Stream<X>, N: Stream<X>, P: Stream<X>)
function FlattenStartMarker<T>(M: Stream<Stream>, startMarker: T): Stream
{
- FlattenStartMarkerAcc(Nil, M, startMarker)
+ PrependThenFlattenStartMarker(Nil, M, startMarker)
}
-function FlattenStartMarkerAcc<T>(accumulator: Stream, M: Stream<Stream>, startMarker: T): Stream
+function PrependThenFlattenStartMarker<T>(prefix: Stream, M: Stream<Stream>, startMarker: T): Stream
{
- match accumulator
+ match prefix
case Cons(hd, tl) =>
- Cons(hd, FlattenStartMarkerAcc(tl, M, startMarker))
+ Cons(hd, PrependThenFlattenStartMarker(tl, M, startMarker))
case Nil =>
match M
case Nil => Nil
- case Cons(s, N) => Cons(startMarker, FlattenStartMarkerAcc(s, N, startMarker))
+ case Cons(s, N) => Cons(startMarker, PrependThenFlattenStartMarker(s, N, startMarker))
}
// The next variation of Flatten requires M to contain no empty streams.
@@ -166,26 +215,24 @@ copredicate StreamOfNonEmpties(M: Stream<Stream>)
function FlattenNonEmpties(M: Stream<Stream>): Stream
requires StreamOfNonEmpties(M);
{
- FlattenNonEmptiesAcc(Nil, M)
+ PrependThenFlattenNonEmpties(Nil, M)
}
-function FlattenNonEmptiesAcc(accumulator: Stream, M: Stream<Stream>): Stream
+function PrependThenFlattenNonEmpties(prefix: Stream, M: Stream<Stream>): Stream
requires StreamOfNonEmpties(M);
{
- match accumulator
+ match prefix
case Cons(hd, tl) =>
- Cons(hd, FlattenNonEmptiesAcc(tl, M))
+ Cons(hd, PrependThenFlattenNonEmpties(tl, M))
case Nil =>
match M
case Nil => Nil
- case Cons(s, N) => Cons(s.head, FlattenNonEmptiesAcc(s.tail, N))
+ case Cons(s, N) => Cons(s.head, PrependThenFlattenNonEmpties(s.tail, N))
}
// We can prove a theorem that links the previous two variations of flatten. To
// do that, we first define a function that prepends an element to each stream
// of a given stream of streams.
-// The "assume" statements below are temporary workaround. They make the proofs
-// unsound, but, as a temporary measure, they express the intent of the proofs.
function Prepend<T>(x: T, M: Stream<Stream>): Stream<Stream>
ensures StreamOfNonEmpties(Prepend(x, M));
@@ -201,58 +248,82 @@ ghost method Theorem_Flatten<T>(M: Stream<Stream>, startMarker: T)
Lemma_Flatten(Nil, M, startMarker);
}
-comethod Lemma_Flatten<T>(accumulator: Stream, M: Stream<Stream>, startMarker: T)
- ensures FlattenStartMarkerAcc(accumulator, M, startMarker) == FlattenNonEmptiesAcc(accumulator, Prepend(startMarker, M));
+comethod Lemma_Flatten<T>(prefix: Stream, M: Stream<Stream>, startMarker: T)
+ ensures PrependThenFlattenStartMarker(prefix, M, startMarker) == PrependThenFlattenNonEmpties(prefix, Prepend(startMarker, M));
{
- calc {
- FlattenStartMarkerAcc(accumulator, M, startMarker);
- { Lemma_FlattenAppend0(accumulator, M, startMarker); }
- append(accumulator, FlattenStartMarkerAcc(Nil, M, startMarker));
- { Lemma_Flatten(Nil, M, startMarker);
- assume FlattenStartMarkerAcc(Nil, M, startMarker) == FlattenNonEmptiesAcc(Nil, Prepend(startMarker, M)); // postcondition of the co-recursive call
- }
- append(accumulator, FlattenNonEmptiesAcc(Nil, Prepend(startMarker, M)));
- { Lemma_FlattenAppend1(accumulator, Prepend(startMarker, M)); }
- FlattenNonEmptiesAcc(accumulator, Prepend(startMarker, M));
+ match (prefix) {
+ case Cons(hd, tl) =>
+ Lemma_Flatten(tl, M, startMarker);
+ case Nil =>
+ match (M) {
+ case Nil =>
+ case Cons(s, N) =>
+ if (*) {
+ // This is all that's needed for the proof
+ Lemma_Flatten(s, N, startMarker);
+ } else {
+ // ...but here are some calculations that try to show more of what's going on
+ // (It would be nice to have ==#[...] available as an operator in calculations.)
+
+ // massage the LHS:
+ calc {
+ PrependThenFlattenStartMarker(prefix, M, startMarker);
+ == // def. PrependThenFlattenStartMarker
+ Cons(startMarker, PrependThenFlattenStartMarker(s, N, startMarker));
+ }
+ // massage the RHS:
+ calc {
+ PrependThenFlattenNonEmpties(prefix, Prepend(startMarker, M));
+ == // M == Cons(s, N)
+ PrependThenFlattenNonEmpties(prefix, Prepend(startMarker, Cons(s, N)));
+ == // def. Prepend
+ PrependThenFlattenNonEmpties(prefix, Cons(Cons(startMarker, s), Prepend(startMarker, N)));
+ == // def. PrependThenFlattenNonEmpties
+ Cons(Cons(startMarker, s).head, PrependThenFlattenNonEmpties(Cons(startMarker, s).tail, Prepend(startMarker, N)));
+ == // Cons, head, tail
+ Cons(startMarker, PrependThenFlattenNonEmpties(s, Prepend(startMarker, N)));
+ }
+
+ // all together now:
+ calc {
+ PrependThenFlattenStartMarker(prefix, M, startMarker) ==#[_k] PrependThenFlattenNonEmpties(prefix, Prepend(startMarker, M));
+ { // by the calculation above, we have:
+ assert PrependThenFlattenStartMarker(prefix, M, startMarker) == Cons(startMarker, PrependThenFlattenStartMarker(s, N, startMarker)); }
+ Cons(startMarker, PrependThenFlattenStartMarker(s, N, startMarker)) ==#[_k] PrependThenFlattenNonEmpties(prefix, Prepend(startMarker, M));
+ { // and by the other calculation above, we have:
+ assert PrependThenFlattenNonEmpties(prefix, Prepend(startMarker, M)) == Cons(startMarker, PrependThenFlattenNonEmpties(s, Prepend(startMarker, N))); }
+ Cons(startMarker, PrependThenFlattenStartMarker(s, N, startMarker)) ==#[_k] Cons(startMarker, PrependThenFlattenNonEmpties(s, Prepend(startMarker, N)));
+ == // def. of ==#[_k] for _k != 0
+ startMarker == startMarker &&
+ PrependThenFlattenStartMarker(s, N, startMarker) ==#[_k-1] PrependThenFlattenNonEmpties(s, Prepend(startMarker, N));
+ { Lemma_Flatten(s, N, startMarker);
+ // the postcondition of the call we just made (which invokes the co-induction hypothesis) is:
+ assert PrependThenFlattenStartMarker(s, N, startMarker) ==#[_k-1] PrependThenFlattenNonEmpties(s, Prepend(startMarker, N));
+ }
+ true;
+ }
+ }
+ }
}
}
comethod Lemma_FlattenAppend0<T>(s: Stream, M: Stream<Stream>, startMarker: T)
- ensures FlattenStartMarkerAcc(s, M, startMarker) == append(s, FlattenStartMarkerAcc(Nil, M, startMarker));
+ ensures PrependThenFlattenStartMarker(s, M, startMarker) == append(s, PrependThenFlattenStartMarker(Nil, M, startMarker));
{
match (s) {
case Nil =>
case Cons(hd, tl) =>
- calc {
- FlattenStartMarkerAcc(Cons(hd, tl), M, startMarker);
- Cons(hd, FlattenStartMarkerAcc(tl, M, startMarker));
- { Lemma_FlattenAppend0(tl, M, startMarker);
- assume FlattenStartMarkerAcc(tl, M, startMarker) == append(tl, FlattenStartMarkerAcc(Nil, M, startMarker)); // this is the postcondition of the co-recursive call
- }
- Cons(hd, append(tl, FlattenStartMarkerAcc(Nil, M, startMarker)));
- // def. append
- append(Cons(hd, tl), FlattenStartMarkerAcc(Nil, M, startMarker));
- }
+ Lemma_FlattenAppend0(tl, M, startMarker);
}
}
comethod Lemma_FlattenAppend1<T>(s: Stream, M: Stream<Stream>)
requires StreamOfNonEmpties(M);
- ensures FlattenNonEmptiesAcc(s, M) == append(s, FlattenNonEmptiesAcc(Nil, M));
+ ensures PrependThenFlattenNonEmpties(s, M) == append(s, PrependThenFlattenNonEmpties(Nil, M));
{
match (s) {
case Nil =>
case Cons(hd, tl) =>
- calc {
- FlattenNonEmptiesAcc(Cons(hd, tl), M);
- // def. FlattenNonEmptiesAcc
- Cons(hd, FlattenNonEmptiesAcc(tl, M));
- { Lemma_FlattenAppend1(tl, M);
- assume FlattenNonEmptiesAcc(tl, M) == append(tl, FlattenNonEmptiesAcc(Nil, M)); // postcondition of the co-recursive call
- }
- Cons(hd, append(tl, FlattenNonEmptiesAcc(Nil, M)));
- // def. append
- append(Cons(hd, tl), FlattenNonEmptiesAcc(Nil, M));
- }
+ Lemma_FlattenAppend1(tl, M);
}
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-31 01:14:52 +0000