Merge

9 files changed, 28 insertions, 16 deletions

diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el
index 4f437d23..1ba6186b 100644
--- a/Util/Emacs/dafny-mode.el
+++ b/Util/Emacs/dafny-mode.el
@@ -40,7 +40,7 @@
    `(,(dafny-regexp-opt '(

         "assert" "assume" "break" "choose" "then" "else" "if" "label" "return" "yield"

         "while" "print" "where"

-        "old" "forall" "exists" "new" "parallel" "in" "this" "fresh"

+        "old" "forall" "exists" "new" "parallel" "calc" "in" "this" "fresh"

         "match" "case" "false" "true" "null")) . font-lock-keyword-face)

    `(,(dafny-regexp-opt '("array" "array2" "array3" "bool" "multiset" "map" "nat" "int" "object" "set" "seq")) . font-lock-type-face)

    )

diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
index 9d6f0882..ac1b755c 100644
--- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
+++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
@@ -29,7 +29,7 @@ namespace Demo
           "in", "forall", "exists",

           "seq", "set", "map", "multiset", "array", "array2", "array3",

           "match", "case",

-          "fresh", "old", "choose", "where"

+          "fresh", "old", "choose", "where", "calc"

           );

 

         StringLiteral s = new StringLiteral("String", "'", StringFlags.AllowsDoubledQuote);

@@ -292,6 +292,7 @@ namespace Demo
           | "return"

           | "yield"

           | "parallel"

+          | "calc"

           | "print"

           | "returns"

           | "yields"

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension.sln b/Util/VS2010/DafnyExtension/DafnyExtension.sln
index e7391254..fd450cc8 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension.sln
+++ b/Util/VS2010/DafnyExtension/DafnyExtension.sln
@@ -1,6 +1,6 @@
 

-Microsoft Visual Studio Solution File, Format Version 11.00

-# Visual Studio 2010

+Microsoft Visual Studio Solution File, Format Version 12.00

+# Visual Studio 2012

 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyExtension", "DafnyExtension\DafnyExtension.csproj", "{6E9A5E14-0763-471C-A129-80A879D9E7BA}"

 EndProject

 Global

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs
index 9f22b887..39829bb0 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs
@@ -231,9 +231,6 @@ namespace DafnyLanguage
       if (Bpl.CommandLineOptions.Clo.UseAbstractInterpretation) {

         if (Bpl.CommandLineOptions.Clo.Ai.J_Intervals || Bpl.CommandLineOptions.Clo.Ai.J_Trivial) {

           Microsoft.Boogie.AbstractInterpretation.NativeAbstractInterpretation.RunAbstractInterpretation(program);

-        } else if (Bpl.CommandLineOptions.Clo.Ai.AnySet) {

-          // run one of the old domains

-          Microsoft.Boogie.AbstractInterpretation.AbstractInterpretation.RunAbstractInterpretation(program);

         } else {

           // use /infer:j as the default

           Bpl.CommandLineOptions.Clo.Ai.J_Intervals = true;

@@ -258,11 +255,7 @@ namespace DafnyLanguage
 

       ConditionGeneration vcgen = null;

       try {

-        if (Bpl.CommandLineOptions.Clo.vcVariety == Bpl.CommandLineOptions.VCVariety.Doomed) {

-          vcgen = new DCGen(program, Bpl.CommandLineOptions.Clo.SimplifyLogFilePath, Bpl.CommandLineOptions.Clo.SimplifyLogFileAppend);

-        } else {

-          vcgen = new VCGen(program, Bpl.CommandLineOptions.Clo.SimplifyLogFilePath, Bpl.CommandLineOptions.Clo.SimplifyLogFileAppend);

-        }

+        vcgen = new VCGen(program, Bpl.CommandLineOptions.Clo.SimplifyLogFilePath, Bpl.CommandLineOptions.Clo.SimplifyLogFileAppend);

       } catch (Bpl.ProverException) {

         return PipelineOutcome.FatalError;

       }

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj
index 66370dec..2580c396 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj
@@ -1,5 +1,6 @@
 <?xml version="1.0" encoding="utf-8"?>

 <Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">

+  <Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" />

   <PropertyGroup>

     <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>

     <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>

@@ -14,6 +15,12 @@
     <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>

     <FileAlignment>512</FileAlignment>

     <GeneratePkgDefFile>false</GeneratePkgDefFile>

+    <MinimumVisualStudioVersion>11.0</MinimumVisualStudioVersion>

+    <FileUpgradeFlags>

+    </FileUpgradeFlags>

+    <UpgradeBackupLocation>

+    </UpgradeBackupLocation>

+    <OldToolsVersion>4.0</OldToolsVersion>

   </PropertyGroup>

   <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">

     <DebugSymbols>true</DebugSymbols>

@@ -158,8 +165,13 @@
   <ItemGroup>

     <WCFMetadata Include="Service References\" />

   </ItemGroup>

+  <PropertyGroup>

+    <VisualStudioVersion Condition="'$(VisualStudioVersion)' == ''">10.0</VisualStudioVersion>

+    <VSToolsPath Condition="'$(VSToolsPath)' == ''">$(MSBuildExtensionsPath32)\Microsoft\VisualStudio\v$(VisualStudioVersion)</VSToolsPath>

+  </PropertyGroup>

   <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />

-  <Import Project="$(MSBuildExtensionsPath)\Microsoft\VisualStudio\v10.0\VSSDK\Microsoft.VsSDK.targets" />

+  <Import Project="$(VSToolsPath)\VSSDK\Microsoft.VsSDK.targets" Condition="'$(VSToolsPath)' != ''" />

+  <Import Project="$(MSBuildExtensionsPath32)\Microsoft\VisualStudio\v10.0\VSSDK\Microsoft.VsSDK.targets" Condition="false" />

   <PropertyGroup>

     <PostBuildEvent>cd</PostBuildEvent>

     <PostBuildEvent>

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
index 22388704..2f295429 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
@@ -227,10 +227,12 @@ namespace DafnyLanguage
                 #region keywords

                 case "allocated":

                 case "array":

+                case "as":

                 case "assert":

                 case "assume":

                 case "bool":

                 case "break":

+                case "calc":

                 case "case":

                 case "choose":

                 case "class":

@@ -249,7 +251,7 @@ namespace DafnyLanguage
                 case "function":

                 case "ghost":

                 case "if":

-                case "imports":

+                case "import":

                 case "in":

                 case "int":

                 case "invariant":

@@ -265,6 +267,7 @@ namespace DafnyLanguage
                 case "null":

                 case "object":

                 case "old":

+                case "opened":

                 case "parallel":

                 case "predicate":

                 case "print":

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/source.extension.vsixmanifest b/Util/VS2010/DafnyExtension/DafnyExtension/source.extension.vsixmanifest
index d822fbfc..ef5c1cf5 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/source.extension.vsixmanifest
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/source.extension.vsixmanifest
@@ -10,6 +10,9 @@
       <VisualStudio Version="10.0">

         <Edition>Pro</Edition>

       </VisualStudio>

+      <VisualStudio Version="11.0">

+        <Edition>Pro</Edition>

+      </VisualStudio>

     </SupportedProducts>

     <SupportedFrameworkRuntimeEdition MinVersion="4.0" MaxVersion="4.0" />

   </Identifier>

diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index 88f9c2a2..879b90cb 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -15,7 +15,7 @@
       match,case,false,true,null,old,fresh,choose,this,

       % statements

       assert,assume,print,new,if,then,else,while,invariant,break,label,return,yield,

-      parallel,where

+      parallel,where,calc

       },

   literate=%

     {:}{$\colon$}1

diff --git a/Util/vim/syntax/dafny.vim b/Util/vim/syntax/dafny.vim
index d67d275a..45afbcf0 100644
--- a/Util/vim/syntax/dafny.vim
+++ b/Util/vim/syntax/dafny.vim
@@ -10,7 +10,7 @@ syntax keyword dafnyTypeDef class datatype codatatype type iterator
 syntax keyword module import opened as default
 syntax keyword dafnyConditional if then else match case 
 syntax keyword dafnyRepeat while parallel
-syntax keyword dafnyStatement assume assert return yield new print break label where
+syntax keyword dafnyStatement assume assert return yield new print break label where calc
 syntax keyword dafnyKeyword var ghost returns yields null static this refines
 syntax keyword dafnyType bool nat int seq set multiset object array array2 array3 map
 syntax keyword dafnyLogic requires ensures modifies reads decreases invariant