diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-11-24 22:30:27 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-11-24 22:30:27 -0800 |
| commit | f951a8d7ff6d4df3852b026e216ed439164b5457 (patch) | |
| tree | 7cd7472ec9bd44663d7025fe1cf580439f0eda93 /Source/Dafny/Dafny.atg | |
| parent | 70523547fb07542156e744df2123e844aa928001 (diff) | |
Parse prefix predicates/methods
Diffstat (limited to 'Source/Dafny/Dafny.atg')
| -rw-r--r-- | Source/Dafny/Dafny.atg | 16 |
1 files changed, 13 insertions, 3 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index d7bf11c4..07e1b5f8 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -27,7 +27,7 @@ struct MemberModifiers { public bool IsGhost;
public bool IsStatic;
}
-// helper routine for parsing call statements
+
///<summary>
/// Parses top-level things (modules, classes, datatypes, class members) from "filename"
/// and appends them in appropriate form to "module".
@@ -1775,7 +1775,12 @@ DottedIdentifiersAndFunction<out Expression e> { "."
Ident<out id> (. idents.Add(id); .)
}
- [ "(" (. openParen = t; args = new List<Expression>(); .)
+ [ (. args = new List<Expression>(); .)
+ [ "#" (. Expression k = new ImplicitIdentifierExpr(t, "_k"); .)
+ [ "[" Expression<out k> "]"
+ ] (. id.val = id.val + "#"; args.Add(k); .)
+ ]
+ "(" (. openParen = t; .)
[ Expressions<args> ]
")"
]
@@ -1789,7 +1794,12 @@ Suffix<ref Expression/*!*/ e> .)
( "."
Ident<out id>
- [ "(" (. IToken openParen = t; args = new List<Expression/*!*/>(); func = true; .)
+ [ (. args = new List<Expression/*!*/>(); func = true; .)
+ [ "#" (. Expression k = new ImplicitIdentifierExpr(t, "_k"); .)
+ [ "[" Expression<out k> "]"
+ ] (. id.val = id.val + "#"; args.Add(k); .)
+ ]
+ "(" (. IToken openParen = t; .)
[ Expressions<args> ]
")" (. e = new FunctionCallExpr(id, id.val, e, openParen, args); .)
] (. if (!func) { e = new ExprDotName(id, e, id.val); } .)
|