diff options
author | 2011-05-18 17:19:18 -0700 | |
---|---|---|
committer | 2011-05-18 17:19:18 -0700 | |
commit | 4baa0fad00861977f7ab9b11161adb1cb0d691cf (patch) | |
tree | 323339486f58c4117ef5f1e0b6b2f45ec5b1cdf5 /Source/Dafny/DafnyAst.cs | |
parent | 0d02c233dc44f763911cfe7daeb0cb0c7a2ec624 (diff) |
Dafny: added set comprehension expressions
Diffstat (limited to 'Source/Dafny/DafnyAst.cs')
-rw-r--r-- | Source/Dafny/DafnyAst.cs | 24 |
1 files changed, 21 insertions, 3 deletions
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);
|