summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Rustan Leino <leino@microsoft.com>2012-08-08 21:57:20 -0700
committerGravatar Rustan Leino <leino@microsoft.com>2012-08-08 21:57:20 -0700
commitb10153f3d755048dbce2fadf9996fc73c279fc7c (patch)
treea3a336d8f0a7659e9a97442598694b5e5f295a46
parent345506163bdd26cf8d3a958e069cf4b0e97fc5af (diff)
DafnyExtension: fixed build issues; added support for some refinement features
-rw-r--r--Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj8
-rw-r--r--Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs23
-rw-r--r--Util/VS2010/DafnyExtension/DafnyExtension/source.extension.vsixmanifest2
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>