diff options
author | 2011-05-15 22:02:08 -0700 | |
---|---|---|
committer | 2011-05-15 22:02:08 -0700 | |
commit | 904fcded9ae0a3219ccccf7c62f116b332deb9ac (patch) | |
tree | 6d58451fa685fc7cf294373c4dfd84b74c3d7c83 /Source/Dafny/DafnyAst.cs | |
parent | 3628ed3ac55bc79515c0cb2c1bec9a21470c9d54 (diff) |
Dafny: added optional range expressions to logical quantifiers, preparing for addition other other comprehensions (like set comprehension)
Diffstat (limited to 'Source/Dafny/DafnyAst.cs')
-rw-r--r-- | Source/Dafny/DafnyAst.cs | 73 |
1 files changed, 57 insertions, 16 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index f76f24de..ad7f5fb6 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -2300,17 +2300,23 @@ namespace Microsoft.Dafny { }
}
- public abstract class QuantifierExpr : Expression {
+ /// <summary>
+ /// A ComprehensionExpr has the form:
+ /// BINDER x Attributes | Range(x) :: Term(x)
+ /// 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>
+ public abstract class ComprehensionExpr : Expression {
public readonly List<BoundVar/*!*/>/*!*/ BoundVars;
- public readonly Expression/*!*/ Body;
+ public readonly Expression Range;
+ public readonly Expression/*!*/ Term;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(BoundVars != null);
- Contract.Invariant(Body != null);
+ Contract.Invariant(Term != null);
}
- public readonly Triggers Trigs;
public readonly Attributes Attributes;
public abstract class BoundedPool { }
@@ -2338,23 +2344,40 @@ namespace Microsoft.Dafny { }
public List<BoundedPool> Bounds; // initialized and filled in by resolver
- // invariant bounds == null || bounds.Count == BoundVars.Count;
+ // invariant Bounds == null || Bounds.Count == BoundVars.Count;
- public QuantifierExpr(IToken/*!*/ tok, List<BoundVar/*!*/>/*!*/ bvars, Expression/*!*/ body, Triggers trigs, 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));
- Contract.Requires(body != null);
+ Contract.Requires(term != null);
this.BoundVars = bvars;
- this.Body = body;
- this.Trigs = trigs;
+ this.Range = range;
+ this.Term = term;
this.Attributes = attrs;
}
public override IEnumerable<Expression> SubExpressions {
- get { yield return Body; }
+ get {
+ if (Range != null) { yield return Range; }
+ yield return Term;
+ }
+ }
+ }
+
+ public abstract class QuantifierExpr : ComprehensionExpr {
+ public readonly Triggers Trigs;
+
+ 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));
+ Contract.Requires(term != null);
+
+ this.Trigs = trigs;
}
+ public abstract Expression/*!*/ LogicalBody();
}
public class Triggers {
@@ -2373,20 +2396,38 @@ namespace Microsoft.Dafny { }
public class ForallExpr : QuantifierExpr {
- public ForallExpr(IToken tok, List<BoundVar/*!*/>/*!*/ bvars, Expression body, Triggers trig, Attributes attrs)
- : base(tok, bvars, body, trig, attrs) {
+ public ForallExpr(IToken tok, List<BoundVar/*!*/>/*!*/ bvars, Expression range, Expression term, Triggers trig, Attributes attrs)
+ : base(tok, bvars, range, term, trig, attrs) {
Contract.Requires(cce.NonNullElements(bvars));
Contract.Requires(tok != null);
- Contract.Requires(body != null);
+ Contract.Requires(term != null);
+ }
+ public override Expression/*!*/ LogicalBody() {
+ if (Range == null) {
+ return Term;
+ }
+ var body = new BinaryExpr(Term.tok, BinaryExpr.Opcode.Imp, Range, Term);
+ body.ResolvedOp = BinaryExpr.ResolvedOpcode.Imp;
+ body.Type = Term.Type;
+ return body;
}
}
public class ExistsExpr : QuantifierExpr {
- public ExistsExpr(IToken tok, List<BoundVar/*!*/>/*!*/ bvars, Expression body, Triggers trig, Attributes attrs)
- : base(tok, bvars, body, trig, attrs) {
+ public ExistsExpr(IToken tok, List<BoundVar/*!*/>/*!*/ bvars, Expression range, Expression term, Triggers trig, Attributes attrs)
+ : base(tok, bvars, range, term, trig, attrs) {
Contract.Requires(cce.NonNullElements(bvars));
Contract.Requires(tok != null);
- Contract.Requires(body != null);
+ Contract.Requires(term != null);
+ }
+ public override Expression/*!*/ LogicalBody() {
+ if (Range == null) {
+ return Term;
+ }
+ var body = new BinaryExpr(Term.tok, BinaryExpr.Opcode.And, Range, Term);
+ body.ResolvedOp = BinaryExpr.ResolvedOpcode.And;
+ body.Type = Term.Type;
+ return body;
}
}
|