diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-08-08 21:57:20 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-08-08 21:57:20 -0700 |
| commit | b10153f3d755048dbce2fadf9996fc73c279fc7c (patch) | |
| tree | a3a336d8f0a7659e9a97442598694b5e5f295a46 /Util | |
| parent | 345506163bdd26cf8d3a958e069cf4b0e97fc5af (diff) | |
DafnyExtension: fixed build issues; added support for some refinement features
Diffstat (limited to 'Util')
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>
|