diff options
| -rw-r--r-- | Binaries/DafnyRuntime.cs | 34 | ||||
| -rw-r--r-- | Source/Dafny/Compiler.cs | 65 | ||||
| -rw-r--r-- | Source/Dafny/Dafny.atg | 26 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 24 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 90 | ||||
| -rw-r--r-- | Source/Dafny/Printer.cs | 23 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 60 | ||||
| -rw-r--r-- | Source/Dafny/Scanner.cs | 102 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 99 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 13 | ||||
| -rw-r--r-- | Test/dafny0/Comprehensions.dfy | 40 | ||||
| -rw-r--r-- | Test/dafny0/runtest.bat | 1 |
12 files changed, 441 insertions, 136 deletions
diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs index b10aeac9..46a3f3df 100644 --- a/Binaries/DafnyRuntime.cs +++ b/Binaries/DafnyRuntime.cs @@ -18,9 +18,16 @@ namespace Dafny public static Set<T> FromElements(params T[] values) {
Dictionary<T, bool> d = new Dictionary<T, bool>(values.Length);
foreach (T t in values)
- d.Add(t, true);
+ d[t] = true;
return new Set<T>(d);
}
+ public static Set<T> FromCollection(ICollection<T> values) {
+ Dictionary<T, bool> d = new Dictionary<T, bool>();
+ foreach (T t in values)
+ d[t] = true;
+ return new Set<T>(d);
+ }
+
public IEnumerable<T> Elements {
get {
return dict.Keys;
@@ -98,7 +105,7 @@ namespace Dafny } else {
a = other.dict; b = dict;
}
- Dictionary<T, bool> r = new Dictionary<T, bool>();
+ var r = new Dictionary<T, bool>();
foreach (T t in a.Keys) {
if (b.ContainsKey(t))
r.Add(t, true);
@@ -110,7 +117,7 @@ namespace Dafny return this;
else if (other.dict.Count == 0)
return this;
- Dictionary<T, bool> r = new Dictionary<T, bool>();
+ var r = new Dictionary<T, bool>();
foreach (T t in dict.Keys) {
if (!other.dict.ContainsKey(t))
r.Add(t, true);
@@ -226,6 +233,7 @@ namespace Dafny }
}
public partial class Helpers {
+ // Computing forall/exists quantifiers
public static bool QuantBool(bool frall, System.Predicate<bool> pred) {
if (frall) {
return pred(false) && pred(true);
@@ -239,17 +247,25 @@ namespace Dafny }
return frall;
}
- public static bool QuantSet<T>(Dafny.Set<T> set, bool frall, System.Predicate<T> pred) {
- foreach (var t in set.Elements) {
- if (pred(t) != frall) { return !frall; }
+ public static bool QuantSet<U>(Dafny.Set<U> set, bool frall, System.Predicate<U> pred) {
+ foreach (var u in set.Elements) {
+ if (pred(u) != frall) { return !frall; }
}
return frall;
}
- public static bool QuantSeq<T>(Dafny.Sequence<T> seq, bool frall, System.Predicate<T> pred) {
- foreach (var t in seq.Elements) {
- if (pred(t) != frall) { return !frall; }
+ public static bool QuantSeq<U>(Dafny.Sequence<U> seq, bool frall, System.Predicate<U> pred) {
+ foreach (var u in seq.Elements) {
+ if (pred(u) != frall) { return !frall; }
}
return frall;
}
+ // Enumerating other collections
+ public delegate Dafny.Set<T> ComprehensionDelegate<T>();
+ public static IEnumerable<bool> AllBooleans {
+ get {
+ yield return false;
+ yield return true;
+ }
+ }
}
}
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 4d352f65..f1a649ee 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -1306,7 +1306,7 @@ namespace Microsoft.Dafny { Contract.Assert(e.Bounds != null); // for non-ghost quantifiers, the resolver would have insisted on finding bounds
var n = e.BoundVars.Count;
Contract.Assert(e.Bounds.Count == n);
- for (int i = n; 0 <= --i; ) {
+ for (int i = 0; i < n; i++) {
var bound = e.Bounds[i];
var bv = e.BoundVars[i];
// emit: Dafny.Helpers.QuantX(boundsInformation, isForall, bv => body)
@@ -1339,7 +1339,68 @@ namespace Microsoft.Dafny { for (int i = 0; i < n; i++) {
wr.Write(")");
}
-
+
+ } else if (expr is SetComprehension) {
+ var e = (SetComprehension)expr;
+ // For "set i,j,k,l | R(i,j,k,l) :: Term(i,j,k,l)" where the term has type "G", emit something like:
+ // ((ComprehensionDelegate<G>)delegate() {
+ // var _coll = new List<G>();
+ // foreach (L l in sq.Elements) {
+ // foreach (K k in st.Elements) {
+ // for (BigInteger j = Lo; j < Hi; j++) {
+ // for (bool i in Helper.AllBooleans) {
+ // if (R(i,j,k,l)) {
+ // _coll.Add(Term(i,j,k,l));
+ // }
+ // }
+ // }
+ // }
+ // }
+ // return Dafny.Set<G>.FromCollection(_coll);
+ // })()
+ Contract.Assert(e.Bounds != null); // the resolver would have insisted on finding bounds
+ var typeName = TypeName(((SetType)e.Type).Arg);
+ wr.Write("((Dafny.Helpers.ComprehensionDelegate<{0}>)delegate() {{ ", typeName);
+ wr.Write("var _coll = new System.Collections.Generic.List<{0}>(); ", typeName);
+ var n = e.BoundVars.Count;
+ Contract.Assert(e.Bounds.Count == n);
+ for (int i = 0; i < n; i++) {
+ var bound = e.Bounds[i];
+ var bv = e.BoundVars[i];
+ if (bound is QuantifierExpr.BoolBoundedPool) {
+ wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.Name);
+ } else if (bound is QuantifierExpr.IntBoundedPool) {
+ var b = (QuantifierExpr.IntBoundedPool)bound;
+ wr.Write("for (var @{0} = ", bv.Name);
+ TrExpr(b.LowerBound);
+ wr.Write("; @{0} < ", bv.Name);
+ TrExpr(b.UpperBound);
+ wr.Write("; @{0}++) {{ ", bv.Name);
+ } else if (bound is QuantifierExpr.SetBoundedPool) {
+ var b = (QuantifierExpr.SetBoundedPool)bound;
+ wr.Write("foreach (var @{0} in (", bv.Name);
+ TrExpr(b.Set);
+ wr.Write(").Elements) { ");
+ } else if (bound is QuantifierExpr.SeqBoundedPool) {
+ var b = (QuantifierExpr.SeqBoundedPool)bound;
+ wr.Write("foreach (var @{0} in (", bv.Name);
+ TrExpr(b.Seq);
+ wr.Write(").Elements) { ");
+ } else {
+ Contract.Assert(false); throw new cce.UnreachableException(); // unexpected BoundedPool type
+ }
+ }
+ wr.Write("if (");
+ TrExpr(e.Range);
+ wr.Write(") { _coll.Add(");
+ TrExpr(e.Term);
+ wr.Write("); }");
+ for (int i = 0; i < n; i++) {
+ wr.Write("}");
+ }
+ wr.Write("return Dafny.Set<{0}>.FromCollection(_coll); ", typeName);
+ wr.Write("})()");
+
} else if (expr is ITEExpr) {
ITEExpr e = (ITEExpr)expr;
wr.Write("(");
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 0ce1835f..f2a0a762 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -1237,6 +1237,7 @@ ConstAtomExpression<out Expression/*!*/ e> "then" Expression<out e0>
"else" Expression<out e1> (. e = new ITEExpr(x, e, e0, e1); .)
| QuantifierGuts<out e>
+ | ComprehensionExpr<out e>
)
.
@@ -1391,6 +1392,31 @@ Forall = "forall" | '\u2200'. Exists = "exists" | '\u2203'.
QSep = "::" | '\u2022'.
+ComprehensionExpr<out Expression/*!*/ q>
+= (. Contract.Ensures(Contract.ValueAtReturn(out q) != null);
+ IToken/*!*/ x = Token.NoToken;
+ BoundVar/*!*/ bv;
+ List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();
+ Expression/*!*/ range;
+ Expression body = null;
+ .)
+ "set" (. x = t; .)
+ (. parseVarScope.PushMarker(); .)
+ IdentTypeOptional<out bv> (. bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name); .)
+ { ","
+ IdentTypeOptional<out bv> (. bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name); .)
+ }
+ "|" Expression<out range>
+ [
+ QSep
+ Expression<out body>
+ ]
+ (. if (body == null && bvars.Count != 1) { SemErr(t, "a set comprehension with more than one bound variable must have a term expression"); }
+ q = new SetComprehension(x, bvars, range, body);
+ parseVarScope.PopMarker();
+ .)
+ .
+
Expressions<.List<Expression/*!*/>/*!*/ args.>
= (. Contract.Requires(cce.NonNullElements(args)); Expression/*!*/ e; .)
Expression<out e> (. args.Add(e); .)
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index ad7f5fb6..d83560e0 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -2303,6 +2303,8 @@ namespace Microsoft.Dafny { /// <summary>
/// A ComprehensionExpr has the form:
/// BINDER x Attributes | Range(x) :: Term(x)
+ /// When BINDER is "forall" or "exists", the range may be "null" (which stands for the logical value "true").
+ /// For other BINDERs (currently, "set"), the range is non-null.
/// where "Attributes" is optional, and "| Range(x)" is optional and defaults to "true".
/// Currently, BINDER is one of the logical quantifiers "exists" or "forall".
/// </summary>
@@ -2346,7 +2348,7 @@ namespace Microsoft.Dafny { public List<BoundedPool> Bounds; // initialized and filled in by resolver
// invariant Bounds == null || Bounds.Count == BoundVars.Count;
- public ComprehensionExpr(IToken/*!*/ tok, List<BoundVar/*!*/>/*!*/ bvars, Expression/*!*/ range, Expression/*!*/ term, Attributes attrs)
+ public ComprehensionExpr(IToken/*!*/ tok, List<BoundVar/*!*/>/*!*/ bvars, Expression range, Expression/*!*/ term, Attributes attrs)
: base(tok) {
Contract.Requires(tok != null);
Contract.Requires(cce.NonNullElements(bvars));
@@ -2369,7 +2371,7 @@ namespace Microsoft.Dafny { public abstract class QuantifierExpr : ComprehensionExpr {
public readonly Triggers Trigs;
- public QuantifierExpr(IToken/*!*/ tok, List<BoundVar/*!*/>/*!*/ bvars, Expression/*!*/ range, Expression/*!*/ term, Triggers trigs, Attributes attrs)
+ public QuantifierExpr(IToken/*!*/ tok, List<BoundVar/*!*/>/*!*/ bvars, Expression range, Expression/*!*/ term, Triggers trigs, Attributes attrs)
: base(tok, bvars, range, term, attrs) {
Contract.Requires(tok != null);
Contract.Requires(cce.NonNullElements(bvars));
@@ -2431,7 +2433,23 @@ namespace Microsoft.Dafny { }
}
- public class WildcardExpr : Expression { // a WildcardExpr can occur only in reads clauses and a loop's decreases clauses (with different meanings)
+ public class SetComprehension : ComprehensionExpr
+ {
+ public readonly bool TermIsImplicit;
+
+ public SetComprehension(IToken/*!*/ tok, List<BoundVar/*!*/>/*!*/ bvars, Expression/*!*/ range, Expression term)
+ : base(tok, bvars, range, term ?? new IdentifierExpr(tok, bvars[0].Name), null) {
+ Contract.Requires(tok != null);
+ Contract.Requires(cce.NonNullElements(bvars));
+ Contract.Requires(1 <= bvars.Count);
+ Contract.Requires(range != null);
+
+ TermIsImplicit = term == null;
+ }
+ }
+
+ public class WildcardExpr : Expression
+ { // a WildcardExpr can occur only in reads clauses and a loop's decreases clauses (with different meanings)
public WildcardExpr(IToken tok)
: base(tok) {
Contract.Requires(tok != null);
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 983996d1..e707d859 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -25,7 +25,7 @@ public class Parser { const bool T = true;
const bool x = false;
const int minErrDist = 2;
-
+
public Scanner/*!*/ scanner;
public Errors/*!*/ errors;
@@ -161,10 +161,10 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! if (errDist >= minErrDist) errors.SemErr(t, msg);
errDist = 0;
}
-
- public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {
- Contract.Requires(tok != null);
- Contract.Requires(msg != null);
+
+ public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {
+ Contract.Requires(tok != null);
+ Contract.Requires(msg != null);
errors.SemErr(tok, msg);
}
@@ -177,15 +177,15 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! la = t;
}
}
-
+
void Expect (int n) {
if (la.kind==n) Get(); else { SynErr(n); }
}
-
+
bool StartOf (int s) {
return set[s, la.kind];
}
-
+
void ExpectWeak (int n, int follow) {
if (la.kind == n) Get();
else {
@@ -209,7 +209,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! }
}
-
+
void Dafny() {
ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt;
Attributes attrs; IToken/*!*/ id; List<string/*!*/> theImports;
@@ -1898,6 +1898,10 @@ List<Expression/*!*/>/*!*/ decreases) { QuantifierGuts(out e);
break;
}
+ case 37: {
+ ComprehensionExpr(out e);
+ break;
+ }
default: SynErr(140); break;
}
}
@@ -1956,6 +1960,35 @@ List<Expression/*!*/>/*!*/ decreases) { }
+ void ComprehensionExpr(out Expression/*!*/ q) {
+ Contract.Ensures(Contract.ValueAtReturn(out q) != null);
+ IToken/*!*/ x = Token.NoToken;
+ BoundVar/*!*/ bv;
+ List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();
+ Expression/*!*/ range;
+ Expression body = null;
+
+ Expect(37);
+ x = t;
+ parseVarScope.PushMarker();
+ IdentTypeOptional(out bv);
+ bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name);
+ while (la.kind == 19) {
+ Get();
+ IdentTypeOptional(out bv);
+ bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name);
+ }
+ Expect(17);
+ Expression(out range);
+ if (la.kind == 105 || la.kind == 106) {
+ QSep();
+ Expression(out body);
+ }
+ q = new SetComprehension(x, bvars, range, body);
+ parseVarScope.PopMarker();
+
+ }
+
void IdentOrFuncExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ id; e = dummyExpr; List<Expression/*!*/>/*!*/ args;
Ident(out id);
@@ -2138,13 +2171,13 @@ List<Expression/*!*/>/*!*/ decreases) { public void Parse() {
la = new Token();
- la.val = "";
+ la.val = "";
Get();
Dafny();
- Expect(0);
+ Expect(0);
}
-
+
static readonly bool[,]/*!*/ set = {
{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,T,x,x, x,T,T,T, T,T,T,x, x,x,T,x, T,x,x,x, x,T,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},
@@ -2154,15 +2187,15 @@ List<Expression/*!*/>/*!*/ decreases) { {x,x,x,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},
{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,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},
{x,T,x,T, 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,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,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,T,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, T,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,T,x, x,T,T,T, T,T,T,T, T,x,x,T, T,T,T,T, T,x,x,x, x},
+ {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,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,T,x, x,T,T,T, T,T,T,T, T,x,x,T, T,T,T,T, T,x,x,x, x},
{x,T,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,x,T,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, T,x,x,T, T,T,x,x, x,x,x,x, T,T,x,T, x,T,T,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,T, T,x,x,x, x,x,x,x, x},
- {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,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,T,x, x,T,T,T, T,T,T,T, T,x,x,T, T,T,T,T, T,x,x,x, x},
+ {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,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,T,x, x,T,T,T, T,T,T,T, T,x,x,T, T,T,T,T, T,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, T,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,x,x, x,x,x,x, T,T,x,T, x,T,T,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,T, T,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, 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, 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, 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,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,T, x,x,x,x, x,x,x,x, x,x,x,x, 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,T,x, x,x,x,T, 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, T,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,T, T,T,T,T, T,x,x,x, x,T,T,T, T,x,x,x, x},
- {x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, x,T,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, T,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,T,x, x,T,T,T, T,T,T,T, T,x,x,T, T,T,T,T, T,x,x,x, x}
+ {x,x,T,x, x,x,x,T, 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,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,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,T, T,T,T,T, T,x,x,x, x,T,T,T, T,x,x,x, x},
+ {x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,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,T,x, x,T,T,T, T,T,T,T, T,x,x,T, T,T,T,T, T,x,x,x, x}
};
} // end Parser
@@ -2171,20 +2204,18 @@ List<Expression/*!*/>/*!*/ decreases) { public class Errors {
public int count = 0; // number of errors detected
public System.IO.TextWriter/*!*/ errorStream = Console.Out; // error messages go to this stream
- public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text
- public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text
-
+ public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text
+ public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text
+
public void SynErr(string filename, int line, int col, int n) {
- SynErr(filename, line, col, GetSyntaxErrorString(n));
- }
-
- public virtual void SynErr(string filename, int line, int col, string/*!*/ msg) {
- Contract.Requires(msg != null);
+ SynErr(filename, line, col, GetSyntaxErrorString(n));
+ }
+ public virtual void SynErr(string filename, int line, int col, string msg) {
+ Contract.Requires(msg != null);
errorStream.WriteLine(errMsgFormat, filename, line, col, msg);
count++;
- }
-
- string GetSyntaxErrorString(int n) {
+ }
+ string GetSyntaxErrorString(int n) {
string s;
switch (n) {
case 0: s = "EOF expected"; break;
@@ -2340,7 +2371,7 @@ public class Errors { default: s = "error " + n; break;
}
- return s;
+ return s;
}
public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { // semantic errors
@@ -2348,9 +2379,8 @@ public class Errors { Contract.Requires(msg != null);
SemErr(tok.filename, tok.line, tok.col, msg);
}
-
public virtual void SemErr(string filename, int line, int col, string/*!*/ msg) {
- Contract.Requires(msg != null);
+ Contract.Requires(msg != null);
errorStream.WriteLine(errMsgFormat, filename, line, col, msg);
count++;
}
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 6dcf0020..d3c7ecea 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -946,7 +946,28 @@ namespace Microsoft.Dafny { PrintExpression(e.Term);
}
if (parensNeeded) { wr.Write(")"); }
-
+
+ } else if (expr is SetComprehension) {
+ var e = (SetComprehension)expr;
+ bool parensNeeded = !isRightmost;
+ if (parensNeeded) { wr.Write("("); }
+ wr.Write("set ");
+ string sep = "";
+ foreach (BoundVar bv in e.BoundVars) {
+ wr.Write("{0}{1}", sep, bv.Name);
+ sep = ", ";
+ PrintType(": ", bv.Type);
+ }
+ wr.Write(" ");
+ PrintAttributes(e.Attributes);
+ wr.Write("| ");
+ PrintExpression(e.Range);
+ if (!e.TermIsImplicit) {
+ wr.Write(" :: ");
+ PrintExpression(e.Term);
+ }
+ if (parensNeeded) { wr.Write(")"); }
+
} else if (expr is WildcardExpr) {
wr.Write("*");
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index c7deb42f..d8ca3448 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -2247,9 +2247,35 @@ namespace Microsoft.Dafny { expr.Type = Type.Bool;
if (prevErrorCount == ErrorCount) {
- e.Bounds = DiscoverBounds(e, specContext);
+ e.Bounds = DiscoverBounds(e.tok, e.BoundVars, e.LogicalBody(), e is ExistsExpr, specContext ? null : "quantifiers in non-ghost contexts must be compilable");
}
-
+
+ } else if (expr is SetComprehension) {
+ var e = (SetComprehension)expr;
+ int prevErrorCount = ErrorCount;
+ scope.PushMarker();
+ foreach (BoundVar v in e.BoundVars) {
+ if (!scope.Push(v.Name, v)) {
+ Error(v, "Duplicate bound-variable name: {0}", v.Name);
+ }
+ ResolveType(v.tok, v.Type);
+ }
+ ResolveExpression(e.Range, twoState, specContext);
+ Contract.Assert(e.Range.Type != null); // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(e.Range.Type, Type.Bool)) {
+ Error(expr, "range of comprehension must be of type bool (instead got {0})", e.Range.Type);
+ }
+ ResolveExpression(e.Term, twoState, specContext);
+ Contract.Assert(e.Term.Type != null); // follows from postcondition of ResolveExpression
+
+ ResolveAttributes(e.Attributes, twoState);
+ scope.PopMarker();
+ expr.Type = new SetType(e.Term.Type);
+
+ if (prevErrorCount == ErrorCount) {
+ e.Bounds = DiscoverBounds(e.tok, e.BoundVars, e.Range, true, "a set comprehension must produce a finite set");
+ }
+
} else if (expr is WildcardExpr) {
expr.Type = new SetType(new ObjectType());
@@ -2378,34 +2404,36 @@ namespace Microsoft.Dafny { }
/// <summary>
- /// Tries to find a bounded pool for each of the bound variables of "e". If this process fails, appropriate
- /// error messages are reported and "null" is returned, unless "friendlyTry" is "true", in which case no
- /// error messages are reported.
+ /// Tries to find a bounded pool for each of the bound variables "bvars" of "expr". If this process
+ /// fails, then "null" is returned and:
+ /// if "errorMessage" is non-null, then appropriate error messages are reported and "null" is returned;
+ /// if "errorMessage" is null, no error messages are reported.
/// Requires "e" to be successfully resolved.
/// </summary>
- List<QuantifierExpr.BoundedPool> DiscoverBounds(QuantifierExpr e, bool friendlyTry) {
- Contract.Requires(e != null);
- Contract.Requires(e.Type != null); // a sanity check (but not a complete proof) that "e" has been resolved
- Contract.Ensures(Contract.Result<List<QuantifierExpr.BoundedPool>>().Count == e.BoundVars.Count);
+ List<QuantifierExpr.BoundedPool> DiscoverBounds(IToken tok, List<BoundVar> bvars, Expression expr, bool polarity, string errorMessage) {
+ Contract.Requires(tok != null);
+ Contract.Requires(bvars != null);
+ Contract.Requires(expr.Type != null); // a sanity check (but not a complete proof) that "e" has been resolved
+ Contract.Ensures(Contract.Result<List<QuantifierExpr.BoundedPool>>().Count == bvars.Count);
var bounds = new List<QuantifierExpr.BoundedPool>();
- for (int j = 0; j < e.BoundVars.Count; j++) {
- var bv = e.BoundVars[j];
- if (bv.Type == Type.Bool) {
+ for (int j = 0; j < bvars.Count; j++) {
+ var bv = bvars[j];
+ if (bv.Type is BoolType) {
// easy
bounds.Add(new QuantifierExpr.BoolBoundedPool());
} else {
// Go through the conjuncts of the range expression look for bounds.
Expression lowerBound = bv.Type is NatType ? new LiteralExpr(bv.tok, new BigInteger(0)) : null;
Expression upperBound = null;
- foreach (var conjunct in NormalizedConjuncts(e.LogicalBody(), e is ExistsExpr)) {
+ foreach (var conjunct in NormalizedConjuncts(expr, polarity)) {
var c = conjunct as BinaryExpr;
if (c == null) {
goto CHECK_NEXT_CONJUNCT;
}
var e0 = c.E0;
var e1 = c.E1;
- int whereIsBv = SanitizeForBoundDiscovery(e.BoundVars, j, c.ResolvedOp, ref e0, ref e1);
+ int whereIsBv = SanitizeForBoundDiscovery(bvars, j, c.ResolvedOp, ref e0, ref e1);
if (whereIsBv < 0) {
goto CHECK_NEXT_CONJUNCT;
}
@@ -2457,8 +2485,8 @@ namespace Microsoft.Dafny { CHECK_NEXT_CONJUNCT: ;
}
// we have checked every conjunct in the range expression and still have not discovered good bounds
- if (!friendlyTry) {
- Error(e, "quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);
+ if (errorMessage != null) {
+ Error(tok, "{0}, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{1}'", errorMessage, bv.Name);
}
return null;
}
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs index 817df6cd..0af254f3 100644 --- a/Source/Dafny/Scanner.cs +++ b/Source/Dafny/Scanner.cs @@ -19,7 +19,7 @@ public class Buffer { // a) whole stream in buffer
// b) part of stream in buffer
// 2) non seekable stream (network, console)
-
+
public const int EOF = 65535 + 1; // char.MaxValue + 1;
const int MIN_BUFFER_LENGTH = 1024; // 1KB
const int MAX_BUFFER_LENGTH = MIN_BUFFER_LENGTH * 64; // 64KB
@@ -31,17 +31,15 @@ public class Buffer { Stream/*!*/ stream; // input stream (seekable)
bool isUserStream; // was the stream opened by the user?
- [ContractInvariantMethod]
- void ObjectInvariant(){
- Contract.Invariant(buf != null);
- Contract.Invariant(stream != null);
- }
-
-// [NotDelayed]
- public Buffer (Stream/*!*/ s, bool isUserStream) : base() {
+[ContractInvariantMethod]
+void ObjectInvariant(){
+ Contract.Invariant(buf != null);
+ Contract.Invariant(stream != null);}
+ [NotDelayed]
+ public Buffer (Stream/*!*/ s, bool isUserStream) :base() {
Contract.Requires(s != null);
stream = s; this.isUserStream = isUserStream;
-
+
int fl, bl;
if (s.CanSeek) {
fl = (int) s.Length;
@@ -53,12 +51,12 @@ public class Buffer { buf = new byte[(bl>0) ? bl : MIN_BUFFER_LENGTH];
fileLen = fl; bufLen = bl;
-
+
if (fileLen > 0) Pos = 0; // setup buffer to position 0 (start)
else bufPos = 0; // index 0 is already after the file, thus Pos = 0 is invalid
if (bufLen == fileLen && s.CanSeek) Close();
}
-
+
protected Buffer(Buffer/*!*/ b) { // called in UTF8Buffer constructor
Contract.Requires(b != null);
buf = b.buf;
@@ -75,14 +73,14 @@ public class Buffer { }
~Buffer() { Close(); }
-
+
protected void Close() {
if (!isUserStream && stream != null) {
stream.Close();
//stream = null;
}
}
-
+
public virtual int Read () {
if (bufPos < bufLen) {
return buf[bufPos++];
@@ -102,7 +100,7 @@ public class Buffer { Pos = curPos;
return ch;
}
-
+
public string/*!*/ GetString (int beg, int end) {
Contract.Ensures(Contract.Result<string>() != null);
int len = 0;
@@ -141,7 +139,7 @@ public class Buffer { }
}
}
-
+
// Read the next chunk of bytes from the stream, increases the buffer
// if needed and updates the fields fileLen and bufLen.
// Returns the number of bytes read.
@@ -215,20 +213,19 @@ public class Scanner { const int noSym = 107;
- [ContractInvariantMethod]
- void objectInvariant(){
- Contract.Invariant(buffer!=null);
- Contract.Invariant(t != null);
- Contract.Invariant(start != null);
- Contract.Invariant(tokens != null);
- Contract.Invariant(pt != null);
- Contract.Invariant(tval != null);
- Contract.Invariant(Filename != null);
- Contract.Invariant(errorHandler != null);
- }
-
+[ContractInvariantMethod]
+void objectInvariant(){
+ Contract.Invariant(buffer!=null);
+ Contract.Invariant(t != null);
+ Contract.Invariant(start != null);
+ Contract.Invariant(tokens != null);
+ Contract.Invariant(pt != null);
+ Contract.Invariant(tval != null);
+ Contract.Invariant(Filename != null);
+ Contract.Invariant(errorHandler != null);
+}
public Buffer/*!*/ buffer; // scanner buffer
-
+
Token/*!*/ t; // current token
int ch; // current input character
int pos; // byte position of current character
@@ -239,13 +236,13 @@ public class Scanner { Token/*!*/ tokens; // list of tokens already peeked (first token is a dummy)
Token/*!*/ pt; // current peek token
-
+
char[]/*!*/ tval = new char[128]; // text of current token
int tlen; // length of current token
-
+
private string/*!*/ Filename;
private Errors/*!*/ errorHandler;
-
+
static Scanner() {
start = new Hashtable(128);
for (int i = 39; i <= 39; ++i) start[i] = 1;
@@ -294,9 +291,9 @@ public class Scanner { start[Buffer.EOF] = -1;
}
-
-// [NotDelayed]
- public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) : base() {
+
+ [NotDelayed]
+ public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) :base(){
Contract.Requires(fileName != null);
Contract.Requires(errorHandler != null);
this.errorHandler = errorHandler;
@@ -306,14 +303,15 @@ public class Scanner { Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read);
buffer = new Buffer(stream, false);
Filename = fileName;
+
Init();
} catch (IOException) {
throw new FatalError("Cannot open file " + fileName);
}
}
-
-// [NotDelayed]
- public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) : base() {
+
+ [NotDelayed]
+ public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) :base(){
Contract.Requires(s != null);
Contract.Requires(errorHandler != null);
Contract.Requires(fileName != null);
@@ -322,9 +320,10 @@ public class Scanner { buffer = new Buffer(s, true);
this.errorHandler = errorHandler;
this.Filename = fileName;
+
Init();
}
-
+
void Init() {
pos = -1; line = 1; col = 0;
oldEols = 0;
@@ -345,11 +344,11 @@ public class Scanner { Contract.Ensures(Contract.Result<string>() != null);
int p = buffer.Pos;
int ch = buffer.Read();
- // replace isolated '\r' by '\n' in order to make
+ // replace isolated '\r' by '\n' in order to make
// eol handling uniform across Windows, Unix and Mac
if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
while (ch != EOL && ch != Buffer.EOF){
- ch = buffer.Read();
+ ch = buffer.Read();
// replace isolated '\r' by '\n' in order to make
// eol handling uniform across Windows, Unix and Mac
if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
@@ -360,7 +359,7 @@ public class Scanner { }
void NextCh() {
- if (oldEols > 0) { ch = EOL; oldEols--; }
+ if (oldEols > 0) { ch = EOL; oldEols--; }
else {
// pos = buffer.Pos;
// ch = buffer.Read(); col++;
@@ -368,9 +367,9 @@ public class Scanner { // // eol handling uniform across Windows, Unix and Mac
// if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
// if (ch == EOL) { line++; col = 0; }
-
+
while (true) {
- pos = buffer.Pos;
+ pos = buffer.Pos;
ch = buffer.Read(); col++;
// replace isolated '\r' by '\n' in order to make
// eol handling uniform across Windows, Unix and Mac
@@ -420,7 +419,7 @@ public class Scanner { return;
}
-
+
}
}
@@ -559,13 +558,10 @@ public class Scanner { t.pos = pos; t.col = col; t.line = line;
t.filename = this.Filename;
int state;
- if (start.ContainsKey(ch)) {
- Contract.Assert(start[ch] != null);
- state = (int) start[ch];
- }
+ if (start.ContainsKey(ch)) { state = (int) cce.NonNull( start[ch]); }
else { state = 0; }
tlen = 0; AddCh();
-
+
switch (state) {
case -1: { t.kind = eofSym; break; } // NextCh already done
case 0: {
@@ -773,14 +769,14 @@ public class Scanner { t.val = new String(tval, 0, tlen);
return t;
}
-
+
private void SetScannerBehindT() {
buffer.Pos = t.pos;
NextCh();
line = t.line; col = t.col;
for (int i = 0; i < tlen; i++) NextCh();
}
-
+
// get the next token (possibly a token already seen during peeking)
public Token/*!*/ Scan () {
Contract.Ensures(Contract.Result<Token>() != null);
@@ -801,7 +797,7 @@ public class Scanner { }
pt = pt.next;
} while (pt.kind > maxT); // skip pragmas
-
+
return pt;
}
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 67559aee..bba7b734 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -1509,9 +1509,12 @@ namespace Microsoft.Dafny { }
Bpl.Expr r = BplAnd(t0, t1);
return z == null ? r : BplAnd(r, z);
- } else if (expr is QuantifierExpr) {
- QuantifierExpr e = (QuantifierExpr)expr;
- Bpl.Expr total = IsTotal(e.LogicalBody(), etran);
+ } else if (expr is ComprehensionExpr) {
+ var e = (ComprehensionExpr)expr;
+ var total = IsTotal(e.Term, etran);
+ if (e.Range != null) {
+ total = BplAnd(IsTotal(e.Range, etran), BplImp(etran.TrExpr(e.Range), total));
+ }
if (total != Bpl.Expr.True) {
Bpl.VariableSeq bvars = new Bpl.VariableSeq();
Bpl.Expr typeAntecedent = etran.TrBoundVariables(e.BoundVars, bvars);
@@ -1636,9 +1639,12 @@ namespace Microsoft.Dafny { break;
}
return BplAnd(t0, t1);
- } else if (expr is QuantifierExpr) {
- QuantifierExpr e = (QuantifierExpr)expr;
- Bpl.Expr total = CanCallAssumption(e.LogicalBody(), etran);
+ } else if (expr is ComprehensionExpr) {
+ var e = (ComprehensionExpr)expr;
+ var total = CanCallAssumption(e.Term, etran);
+ if (e.Range != null) {
+ total = BplAnd(CanCallAssumption(e.Range, etran), BplImp(etran.TrExpr(e.Range), total));
+ }
if (total != Bpl.Expr.True) {
Bpl.VariableSeq bvars = new Bpl.VariableSeq();
Bpl.Expr typeAntecedent = etran.TrBoundVariables(e.BoundVars, bvars);
@@ -1684,6 +1690,18 @@ namespace Microsoft.Dafny { }
}
+ Bpl.Expr BplImp(Bpl.Expr a, Bpl.Expr b) {
+ Contract.Requires(a != null);
+ Contract.Requires(b != null);
+ Contract.Ensures(Contract.Result<Bpl.Expr>() != null);
+
+ if (a == Bpl.Expr.True || b == Bpl.Expr.True) {
+ return b;
+ } else {
+ return Bpl.Expr.Imp(a, b);
+ }
+ }
+
void CheckNonNull(IToken tok, Expression e, Bpl.StmtListBuilder builder, ExpressionTranslator etran, Bpl.QKeyValue kv) {
Contract.Requires(tok != null);
Contract.Requires(e != null);
@@ -1970,8 +1988,8 @@ namespace Microsoft.Dafny { break;
}
- } else if (expr is QuantifierExpr) {
- QuantifierExpr e = (QuantifierExpr)expr;
+ } else if (expr is ComprehensionExpr) {
+ var e = (ComprehensionExpr)expr;
Dictionary<IVariable,Expression> substMap = new Dictionary<IVariable,Expression>();
foreach (BoundVar bv in e.BoundVars) {
VarDecl local = new VarDecl(bv.tok, bv.Name, bv.Type, bv.IsGhost, null);
@@ -1986,8 +2004,18 @@ namespace Microsoft.Dafny { builder.Add(new Bpl.AssumeCmd(bv.tok, wh));
}
}
- Expression body = Substitute(e.LogicalBody(), null, substMap);
- CheckWellformed(body, options, locals, builder, etran);
+
+ Expression body = Substitute(e.Term, null, substMap);
+ if (e.Range == null) {
+ CheckWellformed(body, options, locals, builder, etran);
+ } else {
+ Expression range = Substitute(e.Range, null, substMap);
+ CheckWellformed(range, options, locals, builder, etran);
+
+ Bpl.StmtListBuilder b = new Bpl.StmtListBuilder();
+ CheckWellformed(body, options, locals, b, etran);
+ builder.Add(new Bpl.IfCmd(expr.tok, etran.TrExpr(range), b.Collect(expr.tok), null, null));
+ }
} else if (expr is ITEExpr) {
ITEExpr e = (ITEExpr)expr;
@@ -4443,7 +4471,24 @@ namespace Microsoft.Dafny { Contract.Assert(e is ExistsExpr);
return new Bpl.ExistsExpr(expr.tok, new Bpl.TypeVariableSeq(), bvars, kv, tr, Bpl.Expr.And(antecedent, body));
}
-
+
+ } else if (expr is SetComprehension) {
+ var e = (SetComprehension)expr;
+ // Translate "set xs | R :: T" into "lambda y: BoxType :: (exists xs :: CorrectType(xs) && R && y==Box(T))".
+ Bpl.VariableSeq bvars = new Bpl.VariableSeq();
+ Bpl.Expr typeAntecedent = TrBoundVariables(e.BoundVars, bvars);
+ Bpl.QKeyValue kv = TrAttributes(e.Attributes);
+
+ var yVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, "$y#" + translator.otherTmpVarCount, predef.BoxType));
+ translator.otherTmpVarCount++;
+ Bpl.Expr y = new Bpl.IdentifierExpr(expr.tok, yVar);
+
+ var eq = Bpl.Expr.Eq(y, BoxIfNecessary(expr.tok, TrExpr(e.Term), e.Term.Type));
+ var ebody = Bpl.Expr.And(translator.BplAnd(typeAntecedent, TrExpr(e.Range)), eq);
+ var exst = new Bpl.ExistsExpr(expr.tok, bvars, ebody);
+
+ return new Bpl.LambdaExpr(expr.tok, new Bpl.TypeVariableSeq(), new VariableSeq(yVar), kv, exst);
+
} else if (expr is ITEExpr) {
ITEExpr e = (ITEExpr)expr;
Bpl.Expr g = TrExpr(e.Test);
@@ -5470,9 +5515,10 @@ namespace Microsoft.Dafny { }
return VarOccursInArgumentToRecursiveFunction(e.E0, n, p) ||
VarOccursInArgumentToRecursiveFunction(e.E1, n, p);
- } else if (expr is QuantifierExpr) {
- var e = (QuantifierExpr)expr;
- return VarOccursInArgumentToRecursiveFunction(e.LogicalBody(), n, null);
+ } else if (expr is ComprehensionExpr) {
+ var e = (ComprehensionExpr)expr;
+ return (e.Range != null && VarOccursInArgumentToRecursiveFunction(e.Range, n, null)) ||
+ VarOccursInArgumentToRecursiveFunction(e.Term, n, null);
} else if (expr is ITEExpr) {
var e = (ITEExpr)expr;
return VarOccursInArgumentToRecursiveFunction(e.Test, n, null) || // test is not "elevated"
@@ -5640,18 +5686,27 @@ namespace Microsoft.Dafny { newExpr = newBin;
}
- } else if (expr is QuantifierExpr) {
- QuantifierExpr e = (QuantifierExpr)expr;
+ } else if (expr is ComprehensionExpr) {
+ var e = (ComprehensionExpr)expr;
Expression newRange = e.Range == null ? null : Substitute(e.Range, receiverReplacement, substMap);
Expression newTerm = Substitute(e.Term, receiverReplacement, substMap);
- Triggers newTrigs = SubstTriggers(e.Trigs, receiverReplacement, substMap);
Attributes newAttrs = SubstAttributes(e.Attributes, receiverReplacement, substMap);
- if (newRange != e.Range || newTerm != e.Term || newTrigs != e.Trigs || newAttrs != e.Attributes) {
- if (expr is ForallExpr) {
- newExpr = new ForallExpr(expr.tok, e.BoundVars, newRange, newTerm, newTrigs, newAttrs);
- } else {
- newExpr = new ExistsExpr(expr.tok, e.BoundVars, newRange, newTerm, newTrigs, newAttrs);
+ if (e is SetComprehension) {
+ if (newRange != e.Range || newTerm != e.Term || newAttrs != e.Attributes) {
+ newExpr = new SetComprehension(expr.tok, e.BoundVars, newRange, newTerm);
}
+ } else if (e is QuantifierExpr) {
+ var q = (QuantifierExpr)e;
+ Triggers newTrigs = SubstTriggers(q.Trigs, receiverReplacement, substMap);
+ if (newRange != e.Range || newTerm != e.Term || newAttrs != e.Attributes || newTrigs != q.Trigs) {
+ if (expr is ForallExpr) {
+ newExpr = new ForallExpr(expr.tok, e.BoundVars, newRange, newTerm, newTrigs, newAttrs);
+ } else {
+ newExpr = new ExistsExpr(expr.tok, e.BoundVars, newRange, newTerm, newTrigs, newAttrs);
+ }
+ }
+ } else {
+ Contract.Assume(false); // unexpected ComprehensionExpr
}
} else if (expr is ITEExpr) {
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 2463b0e5..34aea30b 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -527,6 +527,19 @@ Execution trace: Dafny program verifier finished with 2 verified, 1 error
+-------------------- Comprehensions.dfy --------------------
+Comprehensions.dfy(9,14): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon9_Then
+ (0,0): anon10_Then
+ (0,0): anon4
+ (0,0): anon11_Then
+ (0,0): anon12_Then
+ (0,0): anon8
+
+Dafny program verifier finished with 6 verified, 1 error
+
-------------------- Termination.dfy --------------------
Termination.dfy(102,3): Error: cannot prove termination; try supplying a decreases clause for the loop
Execution trace:
diff --git a/Test/dafny0/Comprehensions.dfy b/Test/dafny0/Comprehensions.dfy new file mode 100644 index 00000000..8629a418 --- /dev/null +++ b/Test/dafny0/Comprehensions.dfy @@ -0,0 +1,40 @@ +method M()
+{
+ var numbers := set i | 0 <= i && i < 100;
+ var squares := set i | 0 <= i && i < 100 :: Id(i)*i; // verifying properties about set comprehensions with a term expression is hard
+
+ assert 12 in numbers;
+ assert Id(5) == 5;
+ assert 25 in squares;
+ assert 200 in numbers; // error
+}
+
+function method Id(x: int): int { x } // for triggering
+
+// The following mainly test that set comprehensions can be compiled, but one would
+// have to run the resulting program to check that the compiler is doing the right thing.
+method Main()
+{
+ var q := set i,j | 0 <= i && i < 10 && 0 <= j && j < 3 :: i+j;
+ call PrintSet(q);
+ q := set b: bool | true :: if b then 3 else 7;
+ call PrintSet(q);
+ var m := set k | k in q :: 2*k;
+ call PrintSet(m);
+ call PrintSet(set k | k in q && k % 2 == 0);
+ var sq := [30, 40, 20];
+ call PrintSet(set k, i | k in sq && 0 <= i && i < k && i % 7 == 0 :: k + i);
+ var bb := forall k, i | k in sq && 0 <= i && i < k && i % 7 == 0 :: k + i == 17;
+}
+
+method PrintSet<T>(s: set<T>) {
+ var q := s;
+ while (q != {})
+ decreases q;
+ {
+ var x := choose q;
+ print x, " ";
+ q := q - {x};
+ }
+ print "\n";
+}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index 12d9bcf4..f67429d2 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -15,6 +15,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy FunctionSpecifications.dfy ResolutionErrors.dfy
Array.dfy MultiDimArray.dfy NonGhostQuantifiers.dfy AdvancedLHS.dfy
Modules0.dfy Modules1.dfy BadFunction.dfy
+ Comprehensions.dfy
Termination.dfy Use.dfy DTypes.dfy
TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy
Refinement.dfy RefinementErrors.dfy) do (
|