diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-07-03 01:13:44 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-07-03 01:13:44 -0700 |
| commit | f5b08b01bd06a4ce88f6cc28f30eb180b45d1419 (patch) | |
| tree | cae4418a6b07e0e8587e49929a86e560793aa11f /Util/VS2010 | |
| parent | c66dc1ecd384fdcd402a65ac86824327ee32eb1e (diff) | |
Dafny: added copredicates
Diffstat (limited to 'Util/VS2010')
| -rw-r--r-- | Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs | 50 | ||||
| -rw-r--r-- | Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs | 1 |
2 files changed, 3 insertions, 48 deletions
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs index 627353bf..01767ca6 100644 --- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs +++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs @@ -24,7 +24,7 @@ namespace Demo "break", "label", "return", "parallel", "havoc", "print",
"returns", "requires", "ensures", "modifies", "reads", "decreases",
"bool", "nat", "int", "false", "true", "null",
- "function", "predicate", "free",
+ "function", "predicate", "copredicate", "free",
"in", "forall", "exists",
"seq", "set", "map", "multiset", "array", "array2", "array3",
"match", "case",
@@ -303,6 +303,7 @@ namespace Demo | "null"
| "function"
| "predicate"
+ | "copredicate"
| "free"
| "in"
| "forall"
@@ -358,53 +359,6 @@ namespace Demo | stringLiteral
;
- idType.Rule
- = ident + ":" + typeDecl
- | ident
- ;
-
- typeDecl.Rule
- = (ToTerm("int") | "nat" | "bool" | ident | "seq" | "set" | "array") + (("<" + MakePlusRule(typeDecl, ToTerm(","), typeDecl) + ">") | Empty)
- | ToTerm("token") + "<" + (typeDecl + ".") + ident + ">"
- ;
-
- fieldDecl.Rule
- = ToTerm("var") + idType + Semi
- | ToTerm("ghost") + "var" + idType + Semi
- ;
-
- methodSpec.Rule = (ToTerm("requires") | "ensures" | "lockchange") + expression + Semi;
-
- formalsList.Rule = MakeStarRule(formalsList, comma, idType);
- formalParameters.Rule = LParen + formalsList + RParen;
- methodDecl.Rule = "method" + ident + formalParameters
- + (("returns" + formalParameters) | Empty)
- + methodSpec.Star()
- + blockStatement;
- functionDecl.Rule
- = ToTerm("function") + ident + formalParameters + ":" + typeDecl + methodSpec.Star() + "{" + expression + "}";
- predicateDecl.Rule
- = ToTerm("predicate") + ident + "{" + expression + "}";
- invariantDecl.Rule
- = ToTerm("invariant") + expression + Semi;
-
- memberDecl.Rule
- = fieldDecl
- | invariantDecl
- | methodDecl
- //| conditionDecl
- | predicateDecl
- | functionDecl
- ;
- classDecl.Rule
- = (ToTerm("external") | Empty) + "class" + ident + ("module" + ident | Empty) + "{" + memberDecl.Star() + "}";
- channelDecl.Rule
- = ToTerm("channel") + ident + formalParameters + "where" + expression + Semi
- | ToTerm("channel") + ident + formalParameters + Semi;
- declaration.Rule = classDecl | channelDecl
- ;
-
-
Terminal Comment = new CommentTerminal("Comment", "/*", "*/");
NonGrammarTerminals.Add(Comment);
Terminal LineComment = new CommentTerminal("LineComment", "//", "\n");
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs index d621b1a9..80976499 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs @@ -244,6 +244,7 @@ namespace DafnyLanguage case "class":
case "codatatype":
case "constructor":
+ case "copredicate":
case "datatype":
case "decreases":
case "else":
|