diff options
| author |  leino <unknown> | 2014-09-09 19:14:19 -0700 |
|---|---|---|
| committer | leino <unknown> | 2014-09-09 19:14:19 -0700 |
| commit | 36a4f8a3f8be8e769f198c401f1b7b92ae7d67f6 (patch) | |
| tree | 01558f7dff318bec4d1887a4b8d777613e55b756 /Source/Dafny/Printer.cs | |
| parent | db4d9e34aa774f3167a4842aaf75221bc24d50bc (diff) | |
Print system module (in a comment) with /rprint.
Cleaner printing of .reads and .requires members of the built-in arrow "classes".
Diffstat (limited to 'Source/Dafny/Printer.cs')
| -rw-r--r-- | Source/Dafny/Printer.cs | 47 |
1 files changed, 30 insertions, 17 deletions
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 56722543..6ec05a50 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -124,6 +124,12 @@ namespace Microsoft.Dafny { wr.WriteLine("// " + Bpl.CommandLineOptions.Clo.Environment);
}
wr.WriteLine("// {0}", prog.Name);
+ if (DafnyOptions.O.DafnyPrintResolvedFile != null) {
+ wr.WriteLine();
+ wr.WriteLine("/*");
+ PrintModuleDefinition(prog.BuiltIns.SystemModule, 0);
+ wr.WriteLine("*/");
+ }
wr.WriteLine();
PrintTopLevelDecls(prog.DefaultModuleDef.TopLevelDecls, 0);
}
@@ -204,23 +210,7 @@ namespace Microsoft.Dafny { Indent(indent);
if (d is LiteralModuleDecl) {
ModuleDefinition module = ((LiteralModuleDecl)d).ModuleDef;
- if (module.IsAbstract) {
- wr.Write("abstract ");
- }
- wr.Write("module");
- PrintAttributes(module.Attributes);
- wr.Write(" {0} ", module.Name);
- if (module.RefinementBaseName != null) {
- wr.Write("refines {0} ", Util.Comma(".", module.RefinementBaseName, id => id.val));
- }
- if (module.TopLevelDecls.Count == 0) {
- wr.WriteLine("{ }");
- } else {
- wr.WriteLine("{");
- PrintTopLevelDecls(module.TopLevelDecls, indent + IndentAmount);
- Indent(indent);
- wr.WriteLine("}");
- }
+ PrintModuleDefinition(module, indent);
} else if (d is AliasModuleDecl) {
wr.Write("import"); if (((AliasModuleDecl)d).Opened) wr.Write(" opened");
wr.Write(" {0} ", ((AliasModuleDecl)d).Name);
@@ -230,12 +220,35 @@ namespace Microsoft.Dafny { wr.Write(" {0} ", ((ModuleFacadeDecl)d).Name);
wr.WriteLine("as {0}", Util.Comma(".", ((ModuleFacadeDecl)d).Path, id => id.val));
}
+
} else {
Contract.Assert(false); // unexpected TopLevelDecl
}
}
}
+ void PrintModuleDefinition(ModuleDefinition module, int indent) {
+ Contract.Requires(module != null);
+ Contract.Requires(0 <= indent);
+ if (module.IsAbstract) {
+ wr.Write("abstract ");
+ }
+ wr.Write("module");
+ PrintAttributes(module.Attributes);
+ wr.Write(" {0} ", module.Name);
+ if (module.RefinementBaseName != null) {
+ wr.Write("refines {0} ", Util.Comma(".", module.RefinementBaseName, id => id.val));
+ }
+ if (module.TopLevelDecls.Count == 0) {
+ wr.WriteLine("{ }");
+ } else {
+ wr.WriteLine("{");
+ PrintTopLevelDecls(module.TopLevelDecls, indent + IndentAmount);
+ Indent(indent);
+ wr.WriteLine("}");
+ }
+ }
+
void PrintIteratorSignature(IteratorDecl iter, int indent) {
Indent(indent);
PrintClassMethodHelper("iterator", iter.Attributes, iter.Name, iter.TypeArgs);
|