diff options
Diffstat (limited to 'Source/Dafny/Printer.cs')
| -rw-r--r-- | Source/Dafny/Printer.cs | 57 |
1 files changed, 50 insertions, 7 deletions
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 86c493f1..0ba6f439 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -14,7 +14,8 @@ using Bpl = Microsoft.Boogie; namespace Microsoft.Dafny { public class Printer { TextWriter wr; - DafnyOptions.PrintModes printMode; + DafnyOptions.PrintModes printMode;
+ bool afterResolver; [ContractInvariantMethod] void ObjectInvariant() @@ -129,8 +130,9 @@ namespace Microsoft.Dafny { return sb.ToString(0, len); } - public void PrintProgram(Program prog) { - Contract.Requires(prog != null); + public void PrintProgram(Program prog, bool afterResolver) { + Contract.Requires(prog != null);
+ this.afterResolver = afterResolver; if (Bpl.CommandLineOptions.Clo.ShowEnv != Bpl.CommandLineOptions.ShowEnvironment.Never) { wr.WriteLine("// " + Bpl.CommandLineOptions.Clo.Version); wr.WriteLine("// " + Bpl.CommandLineOptions.Clo.Environment); @@ -239,7 +241,7 @@ namespace Microsoft.Dafny { PrintMembers(cl.Members, indent, fileBeingPrinted); } - } else if (d is ModuleDecl) { + } else if (d is ModuleDecl) {
wr.WriteLine(); Indent(indent); if (d is LiteralModuleDecl) { @@ -252,13 +254,37 @@ namespace Microsoft.Dafny { } else if (d is ModuleFacadeDecl) { wr.Write("import"); if (((ModuleFacadeDecl)d).Opened) wr.Write(" opened"); wr.Write(" {0} ", ((ModuleFacadeDecl)d).Name); - wr.WriteLine("as {0}", Util.Comma(".", ((ModuleFacadeDecl)d).Path, id => id.val)); + wr.WriteLine("as {0}", Util.Comma(".", ((ModuleFacadeDecl)d).Path, id => id.val));
+ } else if (d is ModuleExportDecl) {
+ ModuleExportDecl e = (ModuleExportDecl)d;
+ if (e.IsDefault) wr.Write("default ");
+ wr.Write("export {0}", e.Name);
+ if (e.Extends.Count > 0) wr.Write(" extends {0}", Util.Comma(e.Extends, id => id));
+ PrintModuleExportDecl(e, indent, fileBeingPrinted);
} } else { Contract.Assert(false); // unexpected TopLevelDecl } } + }
+
+ void PrintModuleExportDecl(ModuleExportDecl m, int indent, string fileBeingPrinted) {
+ ModuleSignature sig = m.Signature;
+ if (sig == null) {
+ wr.Write(" {");
+ // has been resolved yet, just print the strings
+ wr.Write("{0}", Util.Comma(m.Exports, id => id.Name));
+ wr.Write("}");
+ } else {
+ wr.WriteLine(" {");
+ // print the decls and members in the module
+ List<TopLevelDecl> decls = sig.TopLevels.Values.ToList();
+ List<MemberDecl> members = sig.StaticMembers.Values.ToList();
+ PrintTopLevelDecls(decls, indent + IndentAmount, fileBeingPrinted);
+ PrintMembers(members, indent + IndentAmount, fileBeingPrinted);
+ Indent(indent); wr.WriteLine("}");
+ }
} void PrintModuleDefinition(ModuleDefinition module, int indent, string fileBeingPrinted) { @@ -277,11 +303,28 @@ namespace Microsoft.Dafny { wr.WriteLine("{ }"); } else { wr.WriteLine("{"); - PrintCallGraph(module, indent + IndentAmount); - PrintTopLevelDecls(module.TopLevelDecls, indent + IndentAmount, fileBeingPrinted); + PrintCallGraph(module, indent + IndentAmount);
+ PrintTopLevelDeclsOrExportedView(module, indent, fileBeingPrinted); Indent(indent); wr.WriteLine("}"); } + }
+
+ void PrintTopLevelDeclsOrExportedView(ModuleDefinition module, int indent, string fileBeingPrinted) {
+ bool printViewsOnly = false;
+ List<TopLevelDecl> decls = new List<TopLevelDecl>();
+ // only filter based on view name after resolver.
+ if (afterResolver) {
+ foreach (var nameOfView in DafnyOptions.O.DafnyPrintExportedViews) {
+ foreach (var decl in module.TopLevelDecls) {
+ if (decl.FullName.Equals(nameOfView)) {
+ printViewsOnly = true;
+ decls.Add(decl);
+ }
+ }
+ }
+ }
+ PrintTopLevelDecls(printViewsOnly ? decls : module.TopLevelDecls, indent + IndentAmount, fileBeingPrinted);
} void PrintIteratorSignature(IteratorDecl iter, int indent) { |