DafnyExtension: fixed build issues; added support for some refinement features

3 files changed, 28 insertions, 5 deletions

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj
index e978f696..62413d03 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj
@@ -143,15 +143,15 @@
   </ItemGroup>

   <ItemGroup>

     <Content Include="DafnyPrelude.bpl">

-      <CopyToOutputDirectory>Always</CopyToOutputDirectory>

       <IncludeInVSIX>true</IncludeInVSIX>

+      <CopyToOutputDirectory>Always</CopyToOutputDirectory>

     </Content>

     <None Include="source.extension.vsixmanifest">

       <SubType>Designer</SubType>

     </None>

     <Content Include="UnivBackPred2.smt2">

-      <CopyToOutputDirectory>Always</CopyToOutputDirectory>

       <IncludeInVSIX>true</IncludeInVSIX>

+      <CopyToOutputDirectory>Always</CopyToOutputDirectory>

     </Content>

   </ItemGroup>

   <ItemGroup>

@@ -164,6 +164,10 @@
     <PostBuildEvent>

     </PostBuildEvent>

   </PropertyGroup>

+  <PropertyGroup>

+    <PreBuildEvent>copy ..\..\..\..\..\..\Binaries\DafnyPrelude.bpl $(ProjectDir)

+copy ..\..\..\..\..\..\Binaries\UnivBackPred2.smt2 $(ProjectDir)</PreBuildEvent>

+  </PropertyGroup>

   <!-- To modify your build process, add your task inside one of the targets below and uncomment it. 

        Other similar extension points exist, see Microsoft.Common.targets.

   <Target Name="BeforeBuild">

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs
index 3dcaf1cf..8cbdb9f6 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs
@@ -119,8 +119,17 @@ namespace DafnyLanguage
           newRegions.Add(new ORegion(module, "module"));

         }

         foreach (Dafny.TopLevelDecl d in module.TopLevelDecls) {

-          if (d is Dafny.DatatypeDecl) {

+          if (!HasBodyTokens(d)) {

+            continue;

+          }

+          if (d is Dafny.ArbitraryTypeDecl) {

+            newRegions.Add(new ORegion(d, "type"));

+          } else if (d is Dafny.CoDatatypeDecl) {

+            newRegions.Add(new ORegion(d, "codatatype"));

+          } else if (d is Dafny.DatatypeDecl) {

             newRegions.Add(new ORegion(d, "datatype"));

+          } else if (d is Dafny.ModuleDecl) {

+            // do nothing here, since the outer loop handles modules

           } else {

             Dafny.ClassDecl cl = (Dafny.ClassDecl)d;

             if (!cl.IsDefaultClass) {

@@ -128,10 +137,13 @@ namespace DafnyLanguage
             }

             // do the class members (in particular, functions and methods)

             foreach (Dafny.MemberDecl m in cl.Members) {

+              if (!HasBodyTokens(m)) {

+                continue;

+              }

               if (m is Dafny.Function && ((Dafny.Function)m).Body != null) {

-                newRegions.Add(new ORegion(m, "function"));

+                newRegions.Add(new ORegion(m, m is Dafny.CoPredicate ? "copredicate" : m is Dafny.Predicate ? "predicate" : "function"));

               } else if (m is Dafny.Method && ((Dafny.Method)m).Body != null) {

-                newRegions.Add(new ORegion(m, "method"));

+                newRegions.Add(new ORegion(m, m is Dafny.Constructor ? "constructor" : "method"));

               }

             }

           }

@@ -143,6 +155,11 @@ namespace DafnyLanguage
       return true;

     }

 

+    bool HasBodyTokens(Dafny.Declaration decl) {

+      Contract.Requires(decl != null);

+      return decl.BodyStartTok != Bpl.Token.NoToken && decl.BodyEndTok != Bpl.Token.NoToken;

+    }

+

     class ORegion

     {

       public readonly int Start;

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/source.extension.vsixmanifest b/Util/VS2010/DafnyExtension/DafnyExtension/source.extension.vsixmanifest
index 35e8f1f9..d822fbfc 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/source.extension.vsixmanifest
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/source.extension.vsixmanifest
@@ -16,5 +16,7 @@
   <References />

   <Content>

     <MefComponent>|%CurrentProject%|</MefComponent>

+    <CustomExtension Type="Boogie">DafnyPrelude.bpl</CustomExtension>

+    <CustomExtension Type="SMTLib 2">UnivBackPred2.smt2</CustomExtension>

   </Content>

 </Vsix>