Use a DafnyProject instead of a root file for printing

Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs

@@ -29,7 +29,7 @@ public partial class Printer {
     public void PrintStatement(Statement stmt, int indent) {
       Contract.Requires(stmt != null);
 
-      if (stmt.IsGhost && printMode == PrintModes.NoGhost) { return; }
+      if (stmt.IsGhost && printMode == PrintModes.NoGhostOrIncludes) { return; }
       for (LList<Label> label = stmt.Labels; label != null; label = label.Next) {
         if (label.Data.Name != null) {
           wr.WriteLine("label {0}:", label.Data.Name);
@@ -38,7 +38,7 @@ public void PrintStatement(Statement stmt, int indent) {
       }
 
       if (stmt is PredicateStmt) {
-        if (printMode == PrintModes.NoGhost) { return; }
+        if (printMode == PrintModes.NoGhostOrIncludes) { return; }
         Expression expr = ((PredicateStmt)stmt).Expr;
         var assertStmt = stmt as AssertStmt;
         var expectStmt = stmt as ExpectStmt;
@@ -220,7 +220,7 @@ public void PrintStatement(Statement stmt, int indent) {
 
       } else if (stmt is CalcStmt) {
         CalcStmt s = (CalcStmt)stmt;
-        if (printMode == PrintModes.NoGhost) { return; }   // Calcs don't get a "ghost" attribute, but they are.
+        if (printMode == PrintModes.NoGhostOrIncludes) { return; }   // Calcs don't get a "ghost" attribute, but they are.
         wr.Write("calc");
         PrintAttributes(stmt.Attributes);
         wr.Write(" ");
@@ -374,7 +374,7 @@ public void PrintStatement(Statement stmt, int indent) {
 
       } else if (stmt is VarDeclStmt) {
         var s = (VarDeclStmt)stmt;
-        if (s.Locals.Exists(v => v.IsGhost) && printMode == PrintModes.NoGhost) { return; }
+        if (s.Locals.Exists(v => v.IsGhost) && printMode == PrintModes.NoGhostOrIncludes) { return; }
         if (s.Locals.TrueForAll((v => v.IsGhost))) {
           // Emit the "ghost" modifier if all of the variables are ghost. If some are ghost, but not others,
           // then some of these ghosts are auto-converted to ghost, so we should not emit the "ghost" keyword.

Source/DafnyCore/AST/Grammar/Printer/Printer.cs

@@ -23,10 +23,9 @@ public enum PrintModes {
     Everything,
     Serialization, // Serializing the program to a file for lossless loading later
     NoIncludes,
-    NoGhost
+    NoGhostOrIncludes
   }
 
-
   public record PrintFlags(bool UseOriginalDafnyNames = false);
 
   public partial class Printer {
@@ -207,7 +206,7 @@ public void PrintProgram(Program prog, bool afterResolver) {
       if (options.DafnyPrintResolvedFile != null && options.PrintMode == PrintModes.Everything) {
         wr.WriteLine();
         wr.WriteLine("/*");
-        PrintModuleDefinition(prog.Compilation, prog.SystemModuleManager.SystemModule, null, 0, null, Path.GetFullPath(options.DafnyPrintResolvedFile));
+        PrintModuleDefinition(prog.Compilation, prog.SystemModuleManager.SystemModule, null, 0, null);
         wr.Write("// bitvector types in use:");
         foreach (var w in prog.SystemModuleManager.Bitwidths) {
           wr.Write(" bv{0}", w);
@@ -217,10 +216,10 @@ public void PrintProgram(Program prog, bool afterResolver) {
       }
       wr.WriteLine();
       PrintCallGraph(prog.DefaultModuleDef, 0);
-      PrintTopLevelDecls(prog.Compilation, prog.DefaultModuleDef.TopLevelDecls, 0, null, Path.GetFullPath(prog.FullName));
+      PrintTopLevelDecls(prog.Compilation, prog.DefaultModuleDef.TopLevelDecls, 0, null);
       foreach (var tup in prog.DefaultModuleDef.PrefixNamedModules) {
         var decls = new List<TopLevelDecl>() { tup.Module };
-        PrintTopLevelDecls(prog.Compilation, decls, 0, tup.Parts, Path.GetFullPath(prog.FullName));
+        PrintTopLevelDecls(prog.Compilation, decls, 0, tup.Parts);
       }
       wr.Flush();
     }
@@ -266,12 +265,14 @@ public void PrintCallGraph(ModuleDefinition module, int indent) {
       }
     }
 
-    public void PrintTopLevelDecls(CompilationData compilation, IEnumerable<TopLevelDecl> decls, int indent, IEnumerable<IToken>/*?*/ prefixIds, string fileBeingPrinted) {
+    public void PrintTopLevelDecls(CompilationData compilation, IEnumerable<TopLevelDecl> decls, int indent,
+      IEnumerable<IToken>/*?*/ prefixIds) {
       Contract.Requires(decls != null);
       int i = 0;
       foreach (TopLevelDecl d in decls) {
         Contract.Assert(d != null);
-        if (PrintModeSkipGeneral(d.tok, fileBeingPrinted)) { continue; }
+        var project = compilation.Options.DafnyProject;
+        if (PrintModeSkipGeneral(project, d.tok)) { continue; }
         if (d is AbstractTypeDecl) {
           var at = (AbstractTypeDecl)d;
           if (i++ != 0) { wr.WriteLine(); }
@@ -282,7 +283,7 @@ public void PrintTopLevelDecls(CompilationData compilation, IEnumerable<TopLevel
             wr.WriteLine();
           } else {
             wr.WriteLine(" {");
-            PrintMembers(at.Members, indent + IndentAmount, fileBeingPrinted);
+            PrintMembers(at.Members, indent + IndentAmount, project);
             Indent(indent);
             wr.WriteLine("}");
           }
@@ -316,7 +317,7 @@ public void PrintTopLevelDecls(CompilationData compilation, IEnumerable<TopLevel
           if (dd.Members.Count != 0) {
             Indent(indent);
             wr.WriteLine("{");
-            PrintMembers(dd.Members, indent + IndentAmount, fileBeingPrinted);
+            PrintMembers(dd.Members, indent + IndentAmount, project);
             Indent(indent);
             wr.WriteLine("}");
           }
@@ -335,7 +336,7 @@ public void PrintTopLevelDecls(CompilationData compilation, IEnumerable<TopLevel
         } else if (d is DatatypeDecl) {
           var dd = (DatatypeDecl)d;
           if (i++ != 0) { wr.WriteLine(); }
-          PrintDatatype(dd, indent, fileBeingPrinted);
+          PrintDatatype(dd, indent, project);
         } else if (d is IteratorDecl) {
           var iter = (IteratorDecl)d;
           if (i++ != 0) { wr.WriteLine(); }
@@ -351,7 +352,7 @@ public void PrintTopLevelDecls(CompilationData compilation, IEnumerable<TopLevel
             // also print the members that were created as part of the interpretation of the iterator
             Contract.Assert(iter.Members.Count != 0);  // filled in during resolution
             Indent(indent); wr.WriteLine("/*---------- iterator members ----------");
-            Indent(indent); PrintIteratorClass(iter, indent, fileBeingPrinted);
+            Indent(indent); PrintIteratorClass(iter, indent, project);
             Indent(indent); wr.WriteLine("---------- iterator members ----------*/");
           }
 
@@ -360,17 +361,17 @@ public void PrintTopLevelDecls(CompilationData compilation, IEnumerable<TopLevel
             // print nothing
           } else {
             if (i++ != 0) { wr.WriteLine(); }
-            PrintMembers(defaultClassDecl.Members, indent, fileBeingPrinted);
+            PrintMembers(defaultClassDecl.Members, indent, project);
           }
         } else if (d is ClassLikeDecl) {
           var cl = (ClassLikeDecl)d;
           if (i++ != 0) { wr.WriteLine(); }
-          PrintClass(cl, indent, fileBeingPrinted);
+          PrintClass(cl, indent, project);
 
         } else if (d is ClassLikeDecl) {
           var cl = (ClassLikeDecl)d;
           if (i++ != 0) { wr.WriteLine(); }
-          PrintClass(cl, indent, fileBeingPrinted);
+          PrintClass(cl, indent, project);
 
         } else if (d is ValuetypeDecl) {
           var vtd = (ValuetypeDecl)d;
@@ -381,7 +382,7 @@ public void PrintTopLevelDecls(CompilationData compilation, IEnumerable<TopLevel
             wr.WriteLine(" { }");
           } else {
             wr.WriteLine(" {");
-            PrintMembers(vtd.Members, indent + IndentAmount, fileBeingPrinted);
+            PrintMembers(vtd.Members, indent + IndentAmount, project);
             Indent(indent);
             wr.WriteLine("}");
           }
@@ -401,7 +402,7 @@ public void PrintTopLevelDecls(CompilationData compilation, IEnumerable<TopLevel
             if (modDecl.Signature != null) {
               scope = modDecl.Signature.VisibilityScope;
             }
-            PrintModuleDefinition(compilation, modDecl.ModuleDef, scope, indent, prefixIds, fileBeingPrinted);
+            PrintModuleDefinition(compilation, modDecl.ModuleDef, scope, indent, prefixIds);
           } else if (d is AliasModuleDecl) {
             var dd = (AliasModuleDecl)d;
 
@@ -450,7 +451,7 @@ public void PrintTopLevelDecls(CompilationData compilation, IEnumerable<TopLevel
             }
 
             wr.WriteLine();
-            PrintModuleExportDecl(compilation, e, indent + IndentAmount, fileBeingPrinted);
+            PrintModuleExportDecl(compilation, e, indent + IndentAmount, project);
             wr.WriteLine();
           } else {
             Contract.Assert(false); // unexpected ModuleDecl
@@ -519,7 +520,7 @@ private void PrintWitnessClause(RedirectingTypeDecl dd) {
       }
     }
 
-    void PrintModuleExportDecl(CompilationData compilation, ModuleExportDecl m, int indent, string fileBeingPrinted) {
+    void PrintModuleExportDecl(CompilationData compilation, ModuleExportDecl m, int indent, DafnyProject project) {
       Contract.Requires(m != null);
 
       if (m.RevealAll) {
@@ -550,9 +551,9 @@ void PrintModuleExportDecl(CompilationData compilation, ModuleExportDecl m, int
           for (int j = start; j < i; j++) {
             var id = m.Exports[j];
             if (id.Decl is TopLevelDecl) {
-              PrintTopLevelDecls(compilation, new List<TopLevelDecl> { (TopLevelDecl)id.Decl }, indent + IndentAmount, null, fileBeingPrinted);
+              PrintTopLevelDecls(compilation, new List<TopLevelDecl> { (TopLevelDecl)id.Decl }, indent + IndentAmount, null);
             } else if (id.Decl is MemberDecl) {
-              PrintMembers(new List<MemberDecl> { (MemberDecl)id.Decl }, indent + IndentAmount, fileBeingPrinted);
+              PrintMembers(new List<MemberDecl> { (MemberDecl)id.Decl }, indent + IndentAmount, project);
             }
           }
           Indent(indent);
@@ -563,7 +564,7 @@ void PrintModuleExportDecl(CompilationData compilation, ModuleExportDecl m, int
       }
     }
 
-    public void PrintModuleDefinition(CompilationData compilation, ModuleDefinition module, VisibilityScope scope, int indent, IEnumerable<IToken>/*?*/ prefixIds, string fileBeingPrinted) {
+    public void PrintModuleDefinition(CompilationData compilation, ModuleDefinition module, VisibilityScope scope, int indent, IEnumerable<IToken>/*?*/ prefixIds) {
       Contract.Requires(module != null);
       Contract.Requires(0 <= indent);
       Type.PushScope(scope);
@@ -595,23 +596,23 @@ public void PrintModuleDefinition(CompilationData compilation, ModuleDefinition
       } else {
         wr.WriteLine("{");
         PrintCallGraph(module, indent + IndentAmount);
-        PrintTopLevelDeclsOrExportedView(compilation, module, indent, fileBeingPrinted);
+        PrintTopLevelDeclsOrExportedView(compilation, module, indent);
         Indent(indent);
         wr.WriteLine("}");
       }
       Type.PopScope(scope);
     }
 
-    void PrintTopLevelDeclsOrExportedView(CompilationData compilation, ModuleDefinition module, int indent, string fileBeingPrinted) {
+    void PrintTopLevelDeclsOrExportedView(CompilationData compilation, ModuleDefinition module, int indent) {
       var decls = module.TopLevelDecls;
       // only filter based on view name after resolver.
       if (afterResolver && options.DafnyPrintExportedViews.Count != 0) {
         var views = options.DafnyPrintExportedViews.ToHashSet();
         decls = decls.Where(d => views.Contains(d.FullName));
       }
-      PrintTopLevelDecls(compilation, decls, indent + IndentAmount, null, fileBeingPrinted);
+      PrintTopLevelDecls(compilation, decls, indent + IndentAmount, null);
       foreach (var tup in module.PrefixNamedModules) {
-        PrintTopLevelDecls(compilation, new TopLevelDecl[] { tup.Module }, indent + IndentAmount, tup.Parts, fileBeingPrinted);
+        PrintTopLevelDecls(compilation, new TopLevelDecl[] { tup.Module }, indent + IndentAmount, tup.Parts);
       }
     }
 
@@ -649,17 +650,17 @@ void PrintIteratorSignature(IteratorDecl iter, int indent) {
       wr.WriteLine();
     }
 
-    private void PrintIteratorClass(IteratorDecl iter, int indent, string fileBeingPrinted) {
+    private void PrintIteratorClass(IteratorDecl iter, int indent, DafnyProject project) {
       PrintClassMethodHelper("class", null, iter.Name, iter.TypeArgs);
       wr.WriteLine(" {");
-      PrintMembers(iter.Members, indent + IndentAmount, fileBeingPrinted);
+      PrintMembers(iter.Members, indent + IndentAmount, project);
       Indent(indent); wr.WriteLine("}");
 
       Contract.Assert(iter.NonNullTypeDecl != null);
       PrintSubsetTypeDecl(iter.NonNullTypeDecl, indent);
     }
 
-    public void PrintClass(ClassLikeDecl c, int indent, string fileBeingPrinted) {
+    public void PrintClass(ClassLikeDecl c, int indent, DafnyProject project) {
       Contract.Requires(c != null);
 
       Indent(indent);
@@ -674,7 +675,7 @@ public void PrintClass(ClassLikeDecl c, int indent, string fileBeingPrinted) {
         wr.WriteLine(" { }");
       } else {
         wr.WriteLine(" {");
-        PrintMembers(c.Members, indent + IndentAmount, fileBeingPrinted);
+        PrintMembers(c.Members, indent + IndentAmount, project);
         Indent(indent);
         wr.WriteLine("}");
       }
@@ -699,12 +700,12 @@ private void PrintExtendsClause(TopLevelDeclWithMembers c) {
       }
     }
 
-    public void PrintMembers(List<MemberDecl> members, int indent, string fileBeingPrinted) {
+    public void PrintMembers(List<MemberDecl> members, int indent, DafnyProject project) {
       Contract.Requires(members != null);
 
       int state = 0;  // 0 - no members yet; 1 - previous member was a field; 2 - previous member was non-field
       foreach (MemberDecl m in members) {
-        if (PrintModeSkipGeneral(m.tok, fileBeingPrinted)) { continue; }
+        if (PrintModeSkipGeneral(project, m.tok)) { continue; }
         if (printMode == PrintModes.Serialization && Attributes.Contains(m.Attributes, "auto_generated")) {
           // omit this declaration
         } else if (m is Method) {
@@ -824,7 +825,7 @@ private void PrintTypeInstantiation(List<Type> typeArgs) {
       wr.Write(Type.TypeArgsToString(options, typeArgs));
     }
 
-    public void PrintDatatype(DatatypeDecl dt, int indent, string fileBeingPrinted) {
+    public void PrintDatatype(DatatypeDecl dt, int indent, DafnyProject dafnyProject) {
       Contract.Requires(dt != null);
       Indent(indent);
       PrintClassMethodHelper(dt is IndDatatypeDecl ? "datatype" : "codatatype", dt.Attributes, dt.Name, dt.TypeArgs);
@@ -843,7 +844,7 @@ public void PrintDatatype(DatatypeDecl dt, int indent, string fileBeingPrinted)
         wr.WriteLine();
       } else {
         wr.WriteLine(" {");
-        PrintMembers(dt.Members, indent + IndentAmount, fileBeingPrinted);
+        PrintMembers(dt.Members, indent + IndentAmount, dafnyProject);
         Indent(indent);
         wr.WriteLine("}");
       }
@@ -974,18 +975,18 @@ void Indent(int amount) {
     }
 
     private bool PrintModeSkipFunctionOrMethod(bool IsGhost, Attributes attributes, string name) {
-      if (printMode == PrintModes.NoGhost && IsGhost) { return true; }
-      if (printMode == PrintModes.NoIncludes || printMode == PrintModes.NoGhost) {
+      if (printMode == PrintModes.NoGhostOrIncludes && IsGhost) { return true; }
+      if (printMode == PrintModes.NoIncludes || printMode == PrintModes.NoGhostOrIncludes) {
         bool verify = true;
         if (Attributes.ContainsBool(attributes, "verify", ref verify) && !verify) { return true; }
         if (name.Contains("INTERNAL") || name.StartsWith(RevealStmt.RevealLemmaPrefix)) { return true; }
       }
       return false;
     }
 
-    private bool PrintModeSkipGeneral(IToken tok, string fileBeingPrinted) {
-      return (printMode == PrintModes.NoIncludes || printMode == PrintModes.NoGhost)
-             && tok.Uri != null && fileBeingPrinted != null && tok.Uri.LocalPath != fileBeingPrinted;
+    private bool PrintModeSkipGeneral(DafnyProject project, IToken tok) {
+      return (printMode == PrintModes.NoIncludes || printMode == PrintModes.NoGhostOrIncludes)
+             && tok.Uri != null && !project.ContainsSourceFile(tok.Uri);
     }
 
     public void PrintMethod(Method method, int indent, bool printSignatureOnly) {
@@ -1110,7 +1111,7 @@ void PrintFormal(Formal f, bool showNewKeyword) {
 
     internal void PrintDecreasesSpec(Specification<Expression> decs, int indent) {
       Contract.Requires(decs != null);
-      if (printMode == PrintModes.NoGhost) { return; }
+      if (printMode == PrintModes.NoGhostOrIncludes) { return; }
       if (decs.Expressions != null && decs.Expressions.Count != 0) {
         wr.WriteLine();
         Indent(indent);
@@ -1139,7 +1140,7 @@ internal void PrintFrameSpecLine(string kind, Specification<FrameExpression> ee,
     internal void PrintSpec(string kind, List<AttributedExpression> ee, int indent) {
       Contract.Requires(kind != null);
       Contract.Requires(ee != null);
-      if (printMode == PrintModes.NoGhost) { return; }
+      if (printMode == PrintModes.NoGhostOrIncludes) { return; }
       foreach (AttributedExpression e in ee) {
         Contract.Assert(e != null);
         wr.WriteLine();

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -461,7 +461,7 @@ void ParsePrintMode(Option<PrintModes> option, Boogie.CommandLineParseState ps,
         } else if (ps.args[ps.i].Equals("NoIncludes")) {
           options.Set(option, PrintModes.NoIncludes);
         } else if (ps.args[ps.i].Equals("NoGhost")) {
-          options.Set(option, PrintModes.NoGhost);
+          options.Set(option, PrintModes.NoGhostOrIncludes);
         } else if (ps.args[ps.i].Equals("DllEmbed")) {
           // This is called DllEmbed because it was previously only used inside Dafny-compiled .dll files for C#,
           // but it is now used by the LibraryBackend when building .doo files as well. 

Source/DafnyCore/Resolver/ModuleResolver.cs

@@ -548,7 +548,7 @@ public void CheckModuleExportConsistency(CompilationData compilation, ModuleDefi
           var wr = Options.OutputWriter;
           wr.WriteLine("/* ===== export set {0}", exportDecl.FullName);
           var pr = new Printer(wr, Options);
-          pr.PrintTopLevelDecls(compilation, exportView.TopLevelDecls, 0, null, null);
+          pr.PrintTopLevelDecls(compilation, exportView.TopLevelDecls, 0, null);
           wr.WriteLine("*/");
         }
 

Source/DafnyDriver/CliCompilation.cs

@@ -36,7 +36,7 @@ private CliCompilation(
     if (options.DafnyProject == null) {
       var firstFile = options.CliRootSourceUris.FirstOrDefault();
       var uri = firstFile ?? new Uri(Directory.GetCurrentDirectory());
-      options.DafnyProject = new DafnyProject(uri, null, new HashSet<string>(), new HashSet<string>(),
+      options.DafnyProject = new DafnyProject(uri, null, new HashSet<string>() { uri.LocalPath }, new HashSet<string>(),
         new Dictionary<string, object>()) {
         ImplicitFromCli = true
       };

Source/IntegrationTests/TestFiles/LitTests/LitTest/printing/Input/included.dfy

@@ -0,0 +1,2 @@
+method Foo() {
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ModulePrint.dfy → Source/IntegrationTests/TestFiles/LitTests/LitTest/printing/ModulePrint.dfy

@@ -2,9 +2,15 @@
 // RUN: %resolve --print "%t.dfy" "%s" > "%t"
 // RUN: %resolve --print-mode Serialization --print:"%t1.dfy" "%t.dfy" >> "%t"
 // RUN: %run --print-mode Serialization --print:"%t2.dfy" "%t1.dfy" >> "%t"
+// RUN: %resolve --print-mode NoGhostOrIncludes --print:"%t3.dfy" %s >> "%t"
+// RUN: %resolve --print-mode NoIncludes --print:"%t4.dfy" %s >> "%t"
 // RUN: %diff "%t1.dfy" "%t2.dfy" >> "%t"
+// RUN: ! %diff "%t.dfy" "%t3.dfy" >> "%t"
+// RUN: ! %diff "%t.dfy" "%t4.dfy" >> "%t"
 // RUN: %diff "%s.expect" "%t"
 
+include "./Input/included.dfy"
+
 abstract module S {
   class C {
     var f: int

docs/dev/news/5645.fix

@@ -0,0 +1 @@
+Let the options --print-mode=NoGhostOrIncludes and --print-mode=NoIncludes work