diff options
author | 2011-05-21 23:57:44 -0700 | |
---|---|---|
committer | 2011-05-21 23:57:44 -0700 | |
commit | 87d1a39324891e5556149c7798b3b14973c93d52 (patch) | |
tree | 44457c19999bcf8fb7fb6b06f2addd91f8aeba47 /Source/Dafny/DafnyAst.cs | |
parent | 9dbf2a6ce1e130f634c27da7bc300001e28aedaf (diff) |
Dafny: allow class names to be used when referring to static functions (and, soon, methods), and test cases for new name resolution rules
Diffstat (limited to 'Source/Dafny/DafnyAst.cs')
-rw-r--r-- | Source/Dafny/DafnyAst.cs | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index df49e8c7..f6d96bab 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -1850,6 +1850,25 @@ namespace Microsoft.Dafny { }
}
+ /// <summary>
+ /// Instances of this class are introduced during resolution to indicate that a static method or function has
+ /// been invoked without specifying a receiver (that is, by just giving the name of the enclosing class).
+ /// </summary>
+ public class StaticReceiverExpr : LiteralExpr
+ {
+ public StaticReceiverExpr(IToken tok, ClassDecl cl)
+ : base(tok) // constructs a LiteralExpr representing the 'null' literal
+ {
+ Contract.Requires(tok != null);
+ Contract.Requires(cl != null);
+ var typeArgs = new List<Type>();
+ foreach (var ta in cl.TypeArgs) {
+ typeArgs.Add(new InferredTypeProxy());
+ }
+ Type = new UserDefinedType(tok, cl.Name, cl, typeArgs);
+ }
+ }
+
public class LiteralExpr : Expression {
public readonly object Value;
|