From f5b08b01bd06a4ce88f6cc28f30eb180b45d1419 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Tue, 3 Jul 2012 01:13:44 -0700
Subject: Dafny: added copredicates

---
 Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs  | 50 +---------------------
 .../DafnyExtension/DafnyExtension/TokenTagger.cs   |  1 +
 2 files changed, 3 insertions(+), 48 deletions(-)

(limited to 'Util/VS2010')

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":
-- 
cgit v1.2.3