Dafny: added copredicates

5 files changed, 7 insertions, 51 deletions

diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el
index 05f06b41..cf2b357f 100644
--- a/Util/Emacs/dafny-mode.el
+++ b/Util/Emacs/dafny-mode.el
@@ -30,7 +30,8 @@
 ]\\)*" . font-lock-comment-face)

 

    `(,(dafny-regexp-opt '(

-        "class" "datatype" "codatatype" "type" "function" "predicate" "ghost" "var" "method" "constructor"

+        "class" "datatype" "codatatype" "type" "function" "predicate" "copredicate"

+        "ghost" "var" "method" "constructor"

         "module" "imports" "static" "refines"

         "returns" "requires" "ensures" "modifies" "reads" "free"

         "invariant" "decreases"

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":

diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index af789102..cfd8863f 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -6,7 +6,7 @@
 

 \lstdefinelanguage{dafny}{

   morekeywords={class,datatype,codatatype,type,bool,nat,int,object,set,multiset,seq,array,array2,array3,%

-      function,predicate,

+      function,predicate,copredicate,

       ghost,var,static,refines,

       method,constructor,returns,module,imports,in,

       requires,modifies,ensures,reads,decreases,free,

diff --git a/Util/vim/syntax/dafny.vim b/Util/vim/syntax/dafny.vim
index 6af28094..33d447fe 100644
--- a/Util/vim/syntax/dafny.vim
+++ b/Util/vim/syntax/dafny.vim
@@ -5,7 +5,7 @@
 
 syntax clear
 syntax case match
-syntax keyword dafnyFunction function predicate method constructor
+syntax keyword dafnyFunction function predicate copredicate method constructor
 syntax keyword dafnyTypeDef class datatype codatatype type
 syntax keyword dafnyConditional if then else match case 
 syntax keyword dafnyRepeat while parallel