diff options
author | 2011-05-21 18:15:17 -0700 | |
---|---|---|
committer | 2011-05-21 18:15:17 -0700 | |
commit | 9dbf2a6ce1e130f634c27da7bc300001e28aedaf (patch) | |
tree | 929593e6a181ba2cfb4fe94d5157f73f3667fae2 /Source/Dafny/DafnyAst.cs | |
parent | 1aa1ca45fc066c9f8d94eeff1a2dc140c49db393 (diff) |
Dafny:
* started rewriting parsing of qualified identifiers in expressions
* annoyingly, had to introduce AST nodes for concrete syntax
* previous syntax for invoking datatype constructors: #List.Cons(h, t)
new syntax: List.Cons(h, t)
or, if only one datatype has a constructor named Cons: Cons(h, t)
* Removed type parameters for datatype constructors from the grammar
* Helped Test/VSI-Benchmarks/b4.dfy along with a couple of assertions (previously, its proving performance was highly varied)
Diffstat (limited to 'Source/Dafny/DafnyAst.cs')
-rw-r--r-- | Source/Dafny/DafnyAst.cs | 70 |
1 files changed, 59 insertions, 11 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index f0a58293..df49e8c7 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -725,28 +725,21 @@ namespace Microsoft.Dafny { }
public class DatatypeCtor : Declaration, TypeParameter.ParentType {
- public readonly List<TypeParameter/*!*/>/*!*/ TypeArgs;
public readonly List<Formal/*!*/>/*!*/ Formals;
[ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(cce.NonNullElements(TypeArgs));
Contract.Invariant(cce.NonNullElements(Formals));
}
// TODO: One could imagine having a precondition on datatype constructors
public DatatypeDecl EnclosingDatatype; // filled in during resolution
- public DatatypeCtor(IToken/*!*/ tok, string/*!*/ name, [Captured] List<TypeParameter/*!*/>/*!*/ typeArgs,
- [Captured] List<Formal/*!*/>/*!*/ formals,
- Attributes attributes)
+ public DatatypeCtor(IToken/*!*/ tok, string/*!*/ name, [Captured] List<Formal/*!*/>/*!*/ formals, Attributes attributes)
: base(tok, name, attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
- Contract.Requires(cce.NonNullElements(typeArgs));
Contract.Requires(cce.NonNullElements(formals));
- this.TypeArgs = typeArgs;
this.Formals = formals;
-
}
public string FullName {
@@ -1235,6 +1228,8 @@ namespace Microsoft.Dafny { if (expr is OldExpr) {
expr = ((OldExpr)expr).E;
+ } else if (expr is ConcreteSyntaxExpression) {
+ expr = ((ConcreteSyntaxExpression)expr).ResolvedExpression;
} else {
break;
}
@@ -1795,6 +1790,20 @@ namespace Microsoft.Dafny { Contract.Invariant(tok != null);
}
+ public Expression Resolved {
+ get {
+ Contract.Requires(type != null); // should be called only on resolved expressions; this approximates that precondition
+ Expression r = this;
+ while (true) {
+ var rr = r as ConcreteSyntaxExpression;
+ if (rr == null) { break; }
+ r = rr.ResolvedExpression;
+ Contract.Assert(r != null); // this is true if the expression is indeed resolved
+ }
+ return r;
+ }
+ }
+
protected Type type;
public Type Type { // filled in during resolution
[Verify(false)] // TODO: how do we allow Type.get to modify type and still be [Pure]?
@@ -1899,7 +1908,6 @@ namespace Microsoft.Dafny { Contract.Invariant(cce.NonNullElements(InferredTypeArgs));
}
-
public DatatypeValue(IToken tok, string datatypeName, string memberName, [Captured] List<Expression/*!*/>/*!*/ arguments)
: base(tok) {
Contract.Requires(cce.NonNullElements(arguments));
@@ -2707,7 +2715,6 @@ namespace Microsoft.Dafny { public readonly string FieldName;
public Field Field; // filled in during resolution (but is null if FieldName is)
-
public FrameExpression(Expression e, string fieldName) {
Contract.Requires(e != null);
Contract.Requires(!(e is WildcardExpr) || fieldName == null);
@@ -2716,4 +2723,45 @@ namespace Microsoft.Dafny { FieldName = fieldName;
}
}
-}
\ No newline at end of file +
+ /// <summary>
+ /// This class represents a piece of concrete syntax in the parse tree. During resolution,
+ /// it gets "replaced" by the expression in "ResolvedExpression".
+ /// </summary>
+ public abstract class ConcreteSyntaxExpression : Expression
+ {
+ public Expression ResolvedExpression; // filled in during resolution; after resolution, manipulation of "this" should proceed as with manipulating "this.ResolvedExpression"
+ public ConcreteSyntaxExpression(IToken tok)
+ : base(tok) {
+ }
+ public override IEnumerable<Expression> SubExpressions {
+ get { yield return ResolvedExpression; }
+ }
+ }
+
+ public class ParensExpression : ConcreteSyntaxExpression
+ {
+ public readonly Expression E;
+ public ParensExpression(IToken tok, Expression e)
+ : base(tok) {
+ E = e;
+ }
+ }
+
+ public class IdentifierSequence : ConcreteSyntaxExpression
+ {
+ public readonly List<IToken> Tokens;
+ public readonly IToken OpenParen;
+ public readonly List<Expression> Arguments;
+ public IdentifierSequence(List<IToken> tokens, IToken openParen, List<Expression> args)
+ : base(tokens[0]) {
+ Contract.Requires(tokens != null && 1 <= tokens.Count);
+ /* "args" is null to indicate the absence of a parenthesized suffix */
+ Contract.Requires(args == null || openParen != null);
+
+ Tokens = tokens;
+ OpenParen = openParen;
+ Arguments = args;
+ }
+ }
+}
|