Adding utility functions; tightening types (#3973)

These changes are in support of dafny doc, but are generally useful.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Co-authored-by: davidcok <[email protected]>

Author: davidcok

Source/DafnyCore/AST/DafnyAst.cs

@@ -49,16 +49,15 @@ void ObjectInvariant() {
     // Contains the definitions to be used for compilation.
 
     public Method MainMethod; // Method to be used as main if compiled
-    public readonly ModuleDecl DefaultModule;
+    public readonly LiteralModuleDecl DefaultModule;
     public readonly DefaultModuleDefinition DefaultModuleDef;
     public readonly BuiltIns BuiltIns;
     public DafnyOptions Options => Reporter.Options;
     public ErrorReporter Reporter { get; set; }
 
-    public Program(string name, [Captured] ModuleDecl module, [Captured] BuiltIns builtIns, ErrorReporter reporter) {
+    public Program(string name, [Captured] LiteralModuleDecl module, [Captured] BuiltIns builtIns, ErrorReporter reporter) {
       Contract.Requires(name != null);
       Contract.Requires(module != null);
-      Contract.Requires(module is LiteralModuleDecl);
       Contract.Requires(reporter != null);
       FullName = name;
       DefaultModule = module;
@@ -193,6 +192,16 @@ public Attributes(string name, [Captured] List<Expression> args, Attributes prev
       Prev = prev;
     }
 
+    public override string ToString() {
+      string result = Prev?.ToString() + "{:" + Name;
+      if (Args == null || Args.Count() == 0) {
+        return result + "}";
+      } else {
+        var exprs = String.Join(", ", Args.Select(e => e.ToString()));
+        return result + " " + exprs + "}";
+      }
+    }
+
     public static IEnumerable<Expression> SubExpressions(Attributes attrs) {
       return attrs.AsEnumerable().SelectMany(aa => aa.Args);
     }

Source/DafnyCore/AST/MemberDecls.cs

@@ -19,6 +19,20 @@ public virtual bool IsStatic {
   protected readonly bool isGhost;
   public bool IsGhost { get { return isGhost; } }
 
+  public string ModifiersAsString() {
+    string result = "";
+    if (IsGhost) {
+      result += "ghost ";
+    }
+    if (IsStatic) {
+      result += "static ";
+    }
+    if (IsOpaque) {
+      result += "opaque ";
+    }
+    return result;
+  }
+
   /// <summary>
   /// The term "instance independent" can be confusing. It means that the constant does not get its value in
   /// a constructor. (But the RHS of the const's declaration may mention "this".)
@@ -712,4 +726,4 @@ public GreatestLemma(RangeToken rangeToken, Name name,
     Contract.Requires(cce.NonNullElements(ens));
     Contract.Requires(decreases != null);
   }
-}
+}

Source/DafnyCore/AST/TopLevelDeclarations.cs

@@ -201,6 +201,16 @@ public override string SanitizedName {
   /// Contravariant            -      - contra-variant
   /// </summary>
   public enum TPVarianceSyntax { NonVariant_Strict, NonVariant_Permissive, Covariant_Strict, Covariant_Permissive, Contravariance }
+  public static string VarianceString(TPVarianceSyntax varianceSyntax) {
+    switch (varianceSyntax) {
+      case TPVarianceSyntax.NonVariant_Strict: return "";
+      case TPVarianceSyntax.NonVariant_Permissive: return "!";
+      case TPVarianceSyntax.Covariant_Strict: return "+";
+      case TPVarianceSyntax.Covariant_Permissive: return "*";
+      case TPVarianceSyntax.Contravariance: return "-";
+    }
+    return ""; // Should not happen, but compiler complains
+  }
   public enum TPVariance { Co, Non, Contra }
   public static TPVariance Negate(TPVariance v) {
     switch (v) {
@@ -275,6 +285,25 @@ public TypeParameterCharacteristics(EqualitySupportValue eqSupport, Type.AutoIni
       AutoInit = autoInit;
       ContainsNoReferenceTypes = containsNoReferenceTypes;
     }
+    public override string ToString() {
+      string result = "";
+      if (EqualitySupport == EqualitySupportValue.Required) {
+        result += ",==";
+      }
+      if (HasCompiledValue) {
+        result += ",0";
+      }
+      if (AutoInit == Type.AutoInitInfo.Nonempty) {
+        result += ",00";
+      }
+      if (ContainsNoReferenceTypes) {
+        result += ",!new";
+      }
+      if (result.Length != 0) {
+        result = "(" + result.Substring(1) + ")";
+      }
+      return result;
+    }
   }
   public TypeParameterCharacteristics Characteristics;
   public bool SupportsEquality {

Source/DafnyCore/DafnyMain.cs

@@ -269,7 +269,7 @@ public static string Parse(IList<DafnyFile> files, string programName, DafnyOpti
 
       if (options.PrintIncludesMode == DafnyOptions.IncludesModes.Immediate) {
         DependencyMap dmap = new DependencyMap();
-        dmap.AddIncludes(((LiteralModuleDecl)module).ModuleDef.Includes);
+        dmap.AddIncludes(module.ModuleDef.Includes);
         dmap.PrintMap();
       }
 

Source/DafnyPipeline.Test/FormatterBaseTest.cs

@@ -54,7 +54,7 @@ protected void FormatterWorksFor(string testCase, string? expectedProgramString
         var uri = new Uri("virtual:virtual");
         var outerModule = new DefaultModuleDefinition(new List<Uri>() { uri });
         BatchErrorReporter reporter = new BatchErrorReporter(options, outerModule);
-        ModuleDecl module = new LiteralModuleDecl(outerModule, null);
+        var module = new LiteralModuleDecl(outerModule, null);
         Microsoft.Dafny.Type.ResetScopes();
         BuiltIns builtIns = new BuiltIns(options);
         Parser.Parse(programNotIndented, uri, module, builtIns, reporter);

Source/DafnyServer/DafnyHelper.cs

@@ -40,7 +40,7 @@ public bool Verify() {
     private bool Parse() {
       var uri = new Uri("transcript:///" + fname);
       var defaultModuleDefinition = new DefaultModuleDefinition(new List<Uri>() { uri });
-      ModuleDecl module = new LiteralModuleDecl(defaultModuleDefinition, null);
+      var module = new LiteralModuleDecl(defaultModuleDefinition, null);
       reporter = new ConsoleErrorReporter(options, defaultModuleDefinition);
       BuiltIns builtIns = new BuiltIns(options);
       var success = (Parser.Parse(source, uri, module, builtIns, new Errors(reporter)) == 0 &&
@@ -152,4 +152,4 @@ private static string ConvertToJson<T>(T data) {
       }
     }
   }
-}
+}

Source/DafnyTestGeneration/Utils.cs

@@ -76,7 +76,7 @@ public static Type CopyWithReplacements(Type type, List<string> from, List<Type>
     public static Program/*?*/ Parse(DafnyOptions options, string source, bool resolve = true, Uri uri = null) {
       uri ??= new Uri(Path.GetTempPath());
       var defaultModuleDefinition = new DefaultModuleDefinition(new List<Uri>() { uri });
-      ModuleDecl module = new LiteralModuleDecl(defaultModuleDefinition, null);
+      var module = new LiteralModuleDecl(defaultModuleDefinition, null);
       var builtIns = new BuiltIns(options);
       var reporter = new BatchErrorReporter(options, defaultModuleDefinition);
       var success = Parser.Parse(source, uri, module, builtIns,