From 8f024b5cf0cf19bc75a4526d957770b6fcf8749a Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Tue, 25 Sep 2012 15:06:54 -0700 Subject: Dafny: added iterators; for now, only parsing and resolving (and printing and refining), no compilation or verification --- Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs') diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs index 81dd0dd1..9d6f0882 100644 --- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs +++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs @@ -17,12 +17,13 @@ namespace Demo StringLiteral stringLiteral = TerminalFactory.CreateCSharpString("String"); this.MarkReservedWords( // NOTE: these keywords must also appear once more below - "class", "ghost", "static", "var", "method", "constructor", "datatype", "codatatype", "type", + "class", "ghost", "static", "var", "method", "constructor", "datatype", "codatatype", + "iterator", "type", "assert", "assume", "new", "this", "object", "refines", "module", "import", "as", "default", "opened", "if", "then", "else", "while", "invariant", - "break", "label", "return", "parallel", "print", - "returns", "requires", "ensures", "modifies", "reads", "decreases", + "break", "label", "return", "yield", "parallel", "print", + "returns", "yields", "requires", "ensures", "modifies", "reads", "decreases", "bool", "nat", "int", "false", "true", "null", "function", "predicate", "copredicate", "free", "in", "forall", "exists", @@ -269,6 +270,7 @@ namespace Demo | "datatype" | "codatatype" | "type" + | "iterator" | "assert" | "assume" | "new" @@ -288,9 +290,11 @@ namespace Demo | "break" | "label" | "return" + | "yield" | "parallel" | "print" | "returns" + | "yields" | "requires" | "ensures" | "modifies" -- cgit v1.2.3