diff --git a/Source/DafnyCore.Test/DooFileTest.cs b/Source/DafnyCore.Test/DooFileTest.cs index 98705c6a52..00f4371890 100644 --- a/Source/DafnyCore.Test/DooFileTest.cs +++ b/Source/DafnyCore.Test/DooFileTest.cs @@ -11,6 +11,7 @@ public void RoundTripCurrentVersion() { var options = DafnyOptions.Default; options.ApplyDefaultOptionsWithoutSettingsDefault(); var program = ParseProgram("module MyModule { function TheAnswer(): int { 42 } }", options); + options.ProcessSolverOptions(program.Reporter, Token.Cli); var dooFile = new DooFile(program); var path = Path.GetTempFileName(); diff --git a/Source/DafnyCore/AST/Expressions/Conditional/Patterns/IdPattern.cs b/Source/DafnyCore/AST/Expressions/Conditional/Patterns/IdPattern.cs index 08000d8ff6..e1b5386d54 100644 --- a/Source/DafnyCore/AST/Expressions/Conditional/Patterns/IdPattern.cs +++ b/Source/DafnyCore/AST/Expressions/Conditional/Patterns/IdPattern.cs @@ -33,11 +33,9 @@ public IdPattern(Cloner cloner, IdPattern original) : base(cloner.Tok(original.T Id = original.Id; Arguments = original.Arguments?.Select(cloner.CloneExtendedPattern).ToList(); HasParenthesis = original.HasParenthesis; + Type = cloner.CloneType(original.Type); if (cloner.CloneResolvedFields) { BoundVar = cloner.CloneIVariable(original.BoundVar, false); - Type = original.Type; - } else { - Type = new InferredTypeProxy(); } } @@ -54,7 +52,7 @@ public IdPattern(IToken tok, String id, Type type, List argumen Contract.Requires(id != null); Contract.Requires(arguments != null); // Arguments can be empty, but shouldn't be null this.Id = id; - this.Type = type == null ? new InferredTypeProxy() : type; + this.Type = type ?? new InferredTypeProxy(); this.Arguments = arguments; this.IsGhost = isGhost; } diff --git a/Source/DafnyCore/AST/Grammar/Printer.cs b/Source/DafnyCore/AST/Grammar/Printer.cs deleted file mode 100644 index 5e8b2ec17c..0000000000 --- a/Source/DafnyCore/AST/Grammar/Printer.cs +++ /dev/null @@ -1,3128 +0,0 @@ -//----------------------------------------------------------------------------- -// -// Copyright (C) Microsoft Corporation. All Rights Reserved. -// Copyright by the contributors to the Dafny Project -// SPDX-License-Identifier: MIT -// -//----------------------------------------------------------------------------- - -using System; -using System.IO; -using System.Collections.Generic; -using System.CommandLine; -using System.Diagnostics.Contracts; -using System.Numerics; -using System.Linq; -using DafnyCore; -using JetBrains.Annotations; -using Bpl = Microsoft.Boogie; - -namespace Microsoft.Dafny { - - public enum PrintModes { - Everything, - Serialization, // Serializing the program to a file for lossless loading later - NoIncludes, - NoGhost - } - - - public record PrintFlags(bool UseOriginalDafnyNames = false); - - public class Printer { - private DafnyOptions options; - static Printer() { - DafnyOptions.RegisterLegacyBinding(PrintMode, (options, value) => { - options.PrintMode = value; - }); - - DooFile.RegisterNoChecksNeeded(new Option[] { - PrintMode - }); - } - - public static readonly Option PrintMode = new("--print-mode", () => PrintModes.Everything, @" -Everything - Print everything listed below. -Serialization - print the source that will be included in a compiled dll. -NoIncludes - disable printing of {:verify false} methods - incorporated via the include mechanism, as well as datatypes and - fields included from other files. -NoGhost - disable printing of functions, ghost methods, and proof - statements in implementation methods. It also disables anything - NoIncludes disables.".TrimStart()) { - IsHidden = true - }; - - TextWriter wr; - PrintModes printMode; - bool afterResolver; - bool printingExportSet = false; - bool printingDesugared = false; - private readonly PrintFlags printFlags; - - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(wr != null); - } - - public Printer(TextWriter wr, DafnyOptions options, PrintModes printMode = PrintModes.Everything, [CanBeNull] PrintFlags printFlags = null) { - Contract.Requires(wr != null); - this.wr = wr; - this.options = options; - this.printMode = printMode; - this.printFlags = printFlags ?? new PrintFlags(); - } - - public static string ExprToString(DafnyOptions options, Expression expr, [CanBeNull] PrintFlags printFlags = null) { - Contract.Requires(expr != null); - using var wr = new StringWriter(); - var pr = new Printer(wr, options, printFlags: printFlags); - pr.PrintExpression(expr, false); - return wr.ToString(); - } - - public static string GuardToString(DafnyOptions options, bool isBindingGuard, Expression expr) { - Contract.Requires(!isBindingGuard || (expr is ExistsExpr && ((ExistsExpr)expr).Range == null)); - using (var wr = new System.IO.StringWriter()) { - var pr = new Printer(wr, options); - pr.PrintGuard(isBindingGuard, expr); - return wr.ToString(); - } - } - - public static string ExtendedExprToString(DafnyOptions options, Expression expr) { - Contract.Requires(expr != null); - using (var wr = new System.IO.StringWriter()) { - var pr = new Printer(wr, options); - pr.PrintExtendedExpr(expr, 0, true, false); - return wr.ToString(); - } - } - - public static string FrameExprListToString(DafnyOptions options, List fexprs) { - Contract.Requires(fexprs != null); - using var wr = new StringWriter(); - var pr = new Printer(wr, options); - pr.PrintFrameExpressionList(fexprs); - return wr.ToString(); - } - - public static string StatementToString(DafnyOptions options, Statement stmt) { - Contract.Requires(stmt != null); - using var wr = new StringWriter(); - var pr = new Printer(wr, options); - pr.PrintStatement(stmt, 0); - return ToStringWithoutNewline(wr); - } - - public static string IteratorClassToString(DafnyOptions options, IteratorDecl iter) { - Contract.Requires(iter != null); - using (var wr = new System.IO.StringWriter()) { - var pr = new Printer(wr, options); - pr.PrintIteratorClass(iter, 0, null); - return ToStringWithoutNewline(wr); - } - } - - public static string IteratorSignatureToString(DafnyOptions options, IteratorDecl iter) { - Contract.Requires(iter != null); - using (var wr = new System.IO.StringWriter()) { - var pr = new Printer(wr, options); - pr.PrintIteratorSignature(iter, 0); - return ToStringWithoutNewline(wr); - } - } - - public static string FieldToString(DafnyOptions options, Field field) { - Contract.Requires(field != null); - using (var wr = new StringWriter()) { - var pr = new Printer(wr, options); - pr.PrintField(field, 0); - return ToStringWithoutNewline(wr); - } - } - - public static string FunctionSignatureToString(DafnyOptions options, Function f) { - Contract.Requires(f != null); - using var wr = new StringWriter(); - var pr = new Printer(wr, options); - pr.PrintFunction(f, 0, true); - return ToStringWithoutNewline(wr); - } - - public static string MethodSignatureToString(DafnyOptions options, Method m) { - Contract.Requires(m != null); - using (var wr = new System.IO.StringWriter()) { - var pr = new Printer(wr, options); - pr.PrintMethod(m, 0, true); - return ToStringWithoutNewline(wr); - } - } - - /// - /// Returns a string for all attributes on the list "a". Each attribute is - /// followed by a space. - /// - public static string AttributesToString(DafnyOptions options, Attributes a) { - if (a == null) { - return ""; - } else { - return AttributesToString(options, a.Prev) + OneAttributeToString(options, a) + " "; - } - } - - public static string OneAttributeToString(DafnyOptions options, Attributes a, string nameSubstitution = null) { - Contract.Requires(a != null); - using (var wr = new System.IO.StringWriter()) { - var pr = new Printer(wr, options); - pr.PrintOneAttribute(a, nameSubstitution); - return ToStringWithoutNewline(wr); - } - } - - public static string ToStringWithoutNewline(System.IO.StringWriter wr) { - Contract.Requires(wr != null); - var sb = wr.GetStringBuilder(); - var len = sb.Length; - while (len > 0 && (sb[len - 1] == '\n' || sb[len - 1] == '\r')) { - len--; - } - return sb.ToString(0, len); - } - - public void PrintProgramLargeStack(Program prog, bool afterResolver) { -#pragma warning disable VSTHRD002 - DafnyMain.LargeStackFactory.StartNew(() => PrintProgram(prog, afterResolver)).Wait(); -#pragma warning restore VSTHRD002 - } - - public void PrintProgram(Program prog, bool afterResolver) { - Contract.Requires(prog != null); - this.afterResolver = afterResolver; - if (options.ShowEnv != Bpl.ExecutionEngineOptions.ShowEnvironment.Never) { - wr.WriteLine("// " + options.Version); - wr.WriteLine("// " + options.Environment); - } - if (options.PrintMode != PrintModes.Serialization) { - wr.WriteLine("// {0}", prog.Name); - } - 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)); - wr.Write("// bitvector types in use:"); - foreach (var w in prog.SystemModuleManager.Bitwidths) { - wr.Write(" bv{0}", w); - } - wr.WriteLine(); - wr.WriteLine("*/"); - } - wr.WriteLine(); - PrintCallGraph(prog.DefaultModuleDef, 0); - PrintTopLevelDecls(prog.Compilation, prog.DefaultModuleDef.TopLevelDecls, 0, null, Path.GetFullPath(prog.FullName)); - foreach (var tup in prog.DefaultModuleDef.PrefixNamedModules) { - var decls = new List() { tup.Module }; - PrintTopLevelDecls(prog.Compilation, decls, 0, tup.Parts, Path.GetFullPath(prog.FullName)); - } - wr.Flush(); - } - - public void PrintCallGraph(ModuleDefinition module, int indent) { - Contract.Requires(module != null); - Contract.Requires(0 <= indent); - if (options.DafnyPrintResolvedFile != null && options.PrintMode == PrintModes.Everything) { - // print call graph - Indent(indent); wr.WriteLine("/* CALL GRAPH for module {0}:", module.Name); - var SCCs = module.CallGraph.TopologicallySortedComponents(); - // Sort output SCCs in order of: descending height, then decreasing size of SCC, then alphabetical order of the name of - // the representative element. By being this specific, we reduce changes in output from minor changes in the code. (With - // more effort, we could be even more deterministic, if needed in the future.) - SCCs.Sort((m, n) => { - var mm = module.CallGraph.GetSCCRepresentativePredecessorCount(m); - var nn = module.CallGraph.GetSCCRepresentativePredecessorCount(n); - if (mm < nn) { - return 1; - } else if (mm > nn) { - return -1; - } - mm = module.CallGraph.GetSCCSize(m); - nn = module.CallGraph.GetSCCSize(n); - if (mm < nn) { - return 1; - } else if (mm > nn) { - return -1; - } - return string.CompareOrdinal(m.NameRelativeToModule, n.NameRelativeToModule); - }); - foreach (var callable in SCCs) { - Indent(indent); - wr.WriteLine(" * SCC at height {0}:", module.CallGraph.GetSCCRepresentativePredecessorCount(callable)); - var r = module.CallGraph.GetSCC(callable); - foreach (var m in r) { - Indent(indent); - var maybeByMethod = m is Method method && method.IsByMethod ? " (by method)" : ""; - wr.WriteLine($" * {m.NameRelativeToModule}{maybeByMethod}"); - } - } - Indent(indent); wr.WriteLine(" */"); - } - } - - public void PrintTopLevelDecls(CompilationData compilation, IEnumerable decls, int indent, IEnumerable/*?*/ prefixIds, string fileBeingPrinted) { - Contract.Requires(decls != null); - int i = 0; - foreach (TopLevelDecl d in decls) { - Contract.Assert(d != null); - if (PrintModeSkipGeneral(d.tok, fileBeingPrinted)) { continue; } - if (d is AbstractTypeDecl) { - var at = (AbstractTypeDecl)d; - if (i++ != 0) { wr.WriteLine(); } - Indent(indent); - PrintClassMethodHelper("type", at.Attributes, at.Name + TPCharacteristicsSuffix(at.Characteristics), d.TypeArgs); - PrintExtendsClause(at); - if (at.Members.Count == 0) { - wr.WriteLine(); - } else { - wr.WriteLine(" {"); - PrintMembers(at.Members, indent + IndentAmount, fileBeingPrinted); - Indent(indent); - wr.WriteLine("}"); - } - } else if (d is NewtypeDecl) { - var dd = (NewtypeDecl)d; - if (i++ != 0) { wr.WriteLine(); } - Indent(indent); - PrintClassMethodHelper("newtype", dd.Attributes, dd.Name, new List()); - PrintExtendsClause(dd); - wr.Write(" = "); - if (dd.Var == null) { - PrintType(dd.BaseType); - wr.WriteLine(); - } else { - wr.Write(dd.Var.DisplayName); - if (ShowType(dd.Var.Type)) { - wr.Write(": "); - PrintType(dd.BaseType); - } - wr.WriteLine(); - Indent(indent + IndentAmount); - wr.Write("| "); - PrintExpression(dd.Constraint, true); - wr.WriteLine(); - if (dd.WitnessKind != SubsetTypeDecl.WKind.CompiledZero) { - Indent(indent + IndentAmount); - PrintWitnessClause(dd); - wr.WriteLine(); - } - } - if (dd.Members.Count != 0) { - Indent(indent); - wr.WriteLine("{"); - PrintMembers(dd.Members, indent + IndentAmount, fileBeingPrinted); - Indent(indent); - wr.WriteLine("}"); - } - } else if (d is SubsetTypeDecl subsetTypeDecl) { - if (i++ != 0) { wr.WriteLine(); } - - PrintSubsetTypeDecl(subsetTypeDecl, indent); - } else if (d is TypeSynonymDecl) { - var dd = (TypeSynonymDecl)d; - if (i++ != 0) { wr.WriteLine(); } - Indent(indent); - PrintClassMethodHelper("type", dd.Attributes, dd.Name + TPCharacteristicsSuffix(dd.Characteristics), dd.TypeArgs); - wr.Write(" = "); - PrintType(dd.Rhs); - wr.WriteLine(); - } else if (d is DatatypeDecl) { - var dd = (DatatypeDecl)d; - if (i++ != 0) { wr.WriteLine(); } - PrintDatatype(dd, indent, fileBeingPrinted); - } else if (d is IteratorDecl) { - var iter = (IteratorDecl)d; - if (i++ != 0) { wr.WriteLine(); } - PrintIteratorSignature(iter, indent); - - if (iter.Body != null) { - Indent(indent); - PrintStatement(iter.Body, indent); - wr.WriteLine(); - } - - if (afterResolver) { - // 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); wr.WriteLine("---------- iterator members ----------*/"); - } - - } else if (d is DefaultClassDecl defaultClassDecl) { - if (defaultClassDecl.Members.Count == 0) { - // print nothing - } else { - if (i++ != 0) { wr.WriteLine(); } - PrintMembers(defaultClassDecl.Members, indent, fileBeingPrinted); - } - } else if (d is ClassLikeDecl) { - var cl = (ClassLikeDecl)d; - if (i++ != 0) { wr.WriteLine(); } - PrintClass(cl, indent, fileBeingPrinted); - - } else if (d is ClassLikeDecl) { - var cl = (ClassLikeDecl)d; - if (i++ != 0) { wr.WriteLine(); } - PrintClass(cl, indent, fileBeingPrinted); - - } else if (d is ValuetypeDecl) { - var vtd = (ValuetypeDecl)d; - if (i++ != 0) { wr.WriteLine(); } - Indent(indent); - PrintClassMethodHelper("type", vtd.Attributes, vtd.Name, vtd.TypeArgs); - if (vtd.Members.Count == 0) { - wr.WriteLine(" { }"); - } else { - wr.WriteLine(" {"); - PrintMembers(vtd.Members, indent + IndentAmount, fileBeingPrinted); - Indent(indent); - wr.WriteLine("}"); - } - - } else if (d is ModuleDecl md) { - wr.WriteLine(); - Indent(indent); - if (d is LiteralModuleDecl modDecl) { - if (printMode == PrintModes.Serialization && !modDecl.ModuleDef.ShouldCompile(compilation)) { - // This mode is used to losslessly serialize the source program by the C# and Library backends. - // Backends don't compile any code for modules not marked for compilation, - // so it's consistent to skip those modules here too. - continue; - } - - VisibilityScope scope = null; - if (modDecl.Signature != null) { - scope = modDecl.Signature.VisibilityScope; - } - PrintModuleDefinition(compilation, modDecl.ModuleDef, scope, indent, prefixIds, fileBeingPrinted); - } else if (d is AliasModuleDecl) { - var dd = (AliasModuleDecl)d; - - wr.Write("import"); - if (dd.Opened) { - wr.Write(" opened"); - } - wr.Write(" {0}", dd.Name); - if (dd.Name != dd.TargetQId.ToString()) { - wr.Write(" = {0}", dd.TargetQId.ToString()); - } - if (dd.Exports.Count == 1) { - wr.Write("`{0}", dd.Exports[0].val); - } - if (dd.Exports.Count > 1) { - wr.Write("`{{{0}}}", Util.Comma(dd.Exports, id => id.val)); - } - wr.WriteLine(); - } else if (d is AbstractModuleDecl) { - var dd = (AbstractModuleDecl)d; - - wr.Write("import"); - if (dd.Opened) { - wr.Write(" opened"); - } - wr.Write(" {0} ", dd.Name); - wr.Write(": {0}", dd.QId.ToString()); - if (dd.Exports.Count > 0) { - wr.Write("`{{{0}}}", Util.Comma(dd.Exports, id => id.val)); - } - wr.WriteLine(); - - } else if (d is ModuleExportDecl) { - ModuleExportDecl e = (ModuleExportDecl)d; - if (!e.IsDefault) { - wr.Write("export {0}", e.Name); - } else { - wr.Write("export"); - } - - if (e.IsRefining) { - wr.Write(" ..."); - } - if (e.Extends.Count > 0) { - wr.Write(" extends {0}", Util.Comma(e.Extends, id => id.val)); - } - - wr.WriteLine(); - PrintModuleExportDecl(compilation, e, indent + IndentAmount, fileBeingPrinted); - wr.WriteLine(); - } else { - Contract.Assert(false); // unexpected ModuleDecl - } - } else { - Contract.Assert(false); // unexpected TopLevelDecl - } - } - } - - private void PrintSubsetTypeDecl(SubsetTypeDecl dd, int indent) { - Indent(indent); - PrintClassMethodHelper("type", dd.Attributes, dd.Name + TPCharacteristicsSuffix(dd.Characteristics), dd.TypeArgs); - wr.Write(" = "); - wr.Write(dd.Var.DisplayName); - if (ShowType(dd.Var.Type)) { - wr.Write(": "); - PrintType(dd.Rhs); - } - - if (dd is NonNullTypeDecl) { - wr.Write(" "); - } else { - wr.WriteLine(); - Indent(indent + IndentAmount); - } - - wr.Write("| "); - PrintExpression(dd.Constraint, true); - if (dd.WitnessKind != SubsetTypeDecl.WKind.CompiledZero) { - if (dd is NonNullTypeDecl) { - wr.Write(" "); - } else { - wr.WriteLine(); - Indent(indent + IndentAmount); - } - - PrintWitnessClause(dd); - } - - wr.WriteLine(); - } - - private void PrintWitnessClause(RedirectingTypeDecl dd) { - Contract.Requires(dd != null); - Contract.Requires(dd.WitnessKind != SubsetTypeDecl.WKind.CompiledZero); - - switch (dd.WitnessKind) { - case SubsetTypeDecl.WKind.Ghost: - wr.Write("ghost "); - goto case SubsetTypeDecl.WKind.Compiled; - case SubsetTypeDecl.WKind.Compiled: - wr.Write("witness "); - PrintExpression(dd.Witness, true); - break; - case SubsetTypeDecl.WKind.OptOut: - wr.Write("witness *"); - break; - case SubsetTypeDecl.WKind.Special: - wr.Write("/*special witness*/"); - break; - case SubsetTypeDecl.WKind.CompiledZero: - default: - Contract.Assert(false); // unexpected WKind - break; - } - } - - void PrintModuleExportDecl(CompilationData compilation, ModuleExportDecl m, int indent, string fileBeingPrinted) { - Contract.Requires(m != null); - - if (m.RevealAll) { - Indent(indent); - wr.WriteLine("reveals *"); - } - if (m.ProvideAll) { - Indent(indent); - wr.WriteLine("provides *"); - } - var i = 0; - while (i < m.Exports.Count) { - var start = i; - var bodyKind = m.Exports[start].Opaque; - do { - i++; - } while (i < m.Exports.Count && m.Exports[i].Opaque == bodyKind); - // print [start..i) - Indent(indent); - wr.Write("{0} ", bodyKind ? "provides" : "reveals"); - wr.WriteLine(Util.Comma(i - start, j => m.Exports[start + j].ToString())); - - if (options.DafnyPrintResolvedFile != null) { - Contract.Assert(!printingExportSet); - printingExportSet = true; - Indent(indent); - wr.WriteLine("/*----- exported view:"); - for (int j = start; j < i; j++) { - var id = m.Exports[j]; - if (id.Decl is TopLevelDecl) { - PrintTopLevelDecls(compilation, new List { (TopLevelDecl)id.Decl }, indent + IndentAmount, null, fileBeingPrinted); - } else if (id.Decl is MemberDecl) { - PrintMembers(new List { (MemberDecl)id.Decl }, indent + IndentAmount, fileBeingPrinted); - } - } - Indent(indent); - wr.WriteLine("-----*/"); - Contract.Assert(printingExportSet); - printingExportSet = false; - } - } - } - - public void PrintModuleDefinition(CompilationData compilation, ModuleDefinition module, VisibilityScope scope, int indent, IEnumerable/*?*/ prefixIds, string fileBeingPrinted) { - Contract.Requires(module != null); - Contract.Requires(0 <= indent); - Type.PushScope(scope); - if (module.ModuleKind == ModuleKindEnum.Abstract) { - wr.Write("abstract "); - } - if (module.ModuleKind == ModuleKindEnum.Replaceable) { - wr.Write("replaceable "); - } - wr.Write("module"); - PrintAttributes(module.Attributes); - wr.Write(" "); - if (prefixIds != null) { - foreach (var p in prefixIds) { - wr.Write("{0}.", p.val); - } - } - wr.Write("{0} ", module.Name); - if (module.Implements != null) { - var kindString = module.Implements.Kind switch { - ImplementationKind.Refinement => "refines", - ImplementationKind.Replacement => "replaces", - _ => throw new ArgumentOutOfRangeException() - }; - wr.Write($"{kindString} {module.Implements.Target} "); - } - if (!module.TopLevelDecls.Any()) { - wr.WriteLine("{ }"); - } else { - wr.WriteLine("{"); - PrintCallGraph(module, indent + IndentAmount); - PrintTopLevelDeclsOrExportedView(compilation, module, indent, fileBeingPrinted); - Indent(indent); - wr.WriteLine("}"); - } - Type.PopScope(scope); - } - - void PrintTopLevelDeclsOrExportedView(CompilationData compilation, ModuleDefinition module, int indent, string fileBeingPrinted) { - 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); - foreach (var tup in module.PrefixNamedModules) { - PrintTopLevelDecls(compilation, new TopLevelDecl[] { tup.Module }, indent + IndentAmount, tup.Parts, fileBeingPrinted); - } - } - - void PrintIteratorSignature(IteratorDecl iter, int indent) { - Indent(indent); - PrintClassMethodHelper("iterator", iter.Attributes, iter.Name, iter.TypeArgs); - if (iter.IsRefining) { - wr.Write(" ..."); - } else { - PrintFormals(iter.Ins, iter); - if (iter.Outs.Count != 0) { - if (iter.Ins.Count + iter.Outs.Count <= 3) { - wr.Write(" yields "); - } else { - wr.WriteLine(); - Indent(indent + 2 * IndentAmount); - wr.Write("yields "); - } - PrintFormals(iter.Outs, iter); - } - } - - int ind = indent + IndentAmount; - PrintSpec("requires", iter.Requires, ind); - if (iter.Reads.Expressions != null) { - PrintFrameSpecLine("reads", iter.Reads, ind); - } - if (iter.Modifies.Expressions != null) { - PrintFrameSpecLine("modifies", iter.Modifies, ind); - } - PrintSpec("yield requires", iter.YieldRequires, ind); - PrintSpec("yield ensures", iter.YieldEnsures, ind); - PrintSpec("ensures", iter.Ensures, ind); - PrintDecreasesSpec(iter.Decreases, ind); - wr.WriteLine(); - } - - private void PrintIteratorClass(IteratorDecl iter, int indent, string fileBeingPrinted) { - PrintClassMethodHelper("class", null, iter.Name, iter.TypeArgs); - wr.WriteLine(" {"); - PrintMembers(iter.Members, indent + IndentAmount, fileBeingPrinted); - Indent(indent); wr.WriteLine("}"); - - Contract.Assert(iter.NonNullTypeDecl != null); - PrintSubsetTypeDecl(iter.NonNullTypeDecl, indent); - } - - public void PrintClass(ClassLikeDecl c, int indent, string fileBeingPrinted) { - Contract.Requires(c != null); - - Indent(indent); - PrintClassMethodHelper((c is TraitDecl) ? "trait" : "class", c.Attributes, c.Name, c.TypeArgs); - if (c.IsRefining) { - wr.Write(" ..."); - } else { - PrintExtendsClause(c); - } - - if (c.Members.Count == 0) { - wr.WriteLine(" { }"); - } else { - wr.WriteLine(" {"); - PrintMembers(c.Members, indent + IndentAmount, fileBeingPrinted); - Indent(indent); - wr.WriteLine("}"); - } - - if (options.DafnyPrintResolvedFile != null && c.NonNullTypeDecl != null) { - if (!printingExportSet) { - Indent(indent); wr.WriteLine("/*-- non-null type"); - } - PrintSubsetTypeDecl(c.NonNullTypeDecl, indent); - if (!printingExportSet) { - Indent(indent); wr.WriteLine("*/"); - } - } - } - - private void PrintExtendsClause(TopLevelDeclWithMembers c) { - string sep = " extends "; - foreach (var trait in c.ParentTraits) { - wr.Write(sep); - PrintType(trait); - sep = ", "; - } - } - - public void PrintMembers(List members, int indent, string fileBeingPrinted) { - 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 (printMode == PrintModes.Serialization && Attributes.Contains(m.Attributes, "auto_generated")) { - // omit this declaration - } else if (m is Method) { - if (state != 0) { wr.WriteLine(); } - PrintMethod((Method)m, indent, false); - var com = m as ExtremeLemma; - if (com != null && com.PrefixLemma != null) { - Indent(indent); wr.WriteLine("/***"); - PrintMethod(com.PrefixLemma, indent, false); - Indent(indent); wr.WriteLine("***/"); - } - state = 2; - } else if (m is Field) { - if (state == 2) { wr.WriteLine(); } - PrintField((Field)m, indent); - state = 1; - } else if (m is Function) { - if (state != 0) { wr.WriteLine(); } - PrintFunction((Function)m, indent, false); - if (m is ExtremePredicate fixp && fixp.PrefixPredicate != null) { - Indent(indent); wr.WriteLine("/*** (note, what is printed here does not show substitutions of calls to prefix predicates)"); - PrintFunction(fixp.PrefixPredicate, indent, false); - Indent(indent); wr.WriteLine("***/"); - } - state = 2; - } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected member - } - } - } - - /// - /// Prints no space before "kind", but does print a space before "attrs" and "name". - /// - void PrintClassMethodHelper(string kind, Attributes attrs, string name, List typeArgs) { - Contract.Requires(kind != null); - Contract.Requires(name != null); - Contract.Requires(typeArgs != null); - - wr.Write(kind); - PrintAttributes(attrs); - - if (ArrowType.IsArrowTypeName(name)) { - PrintArrowType(ArrowType.ANY_ARROW, name, typeArgs); - } else if (ArrowType.IsPartialArrowTypeName(name)) { - PrintArrowType(ArrowType.PARTIAL_ARROW, name, typeArgs); - } else if (ArrowType.IsTotalArrowTypeName(name)) { - PrintArrowType(ArrowType.TOTAL_ARROW, name, typeArgs); - } else if (SystemModuleManager.IsTupleTypeName(name)) { - wr.Write(" /*{0}*/ ({1})", name, Util.Comma(typeArgs, TypeParamString)); - } else { - wr.Write(" {0}", name); - PrintTypeParams(typeArgs); - } - } - - private void PrintTypeParams(List typeArgs) { - Contract.Requires(typeArgs != null); - Contract.Requires( - typeArgs.All(tp => tp.Name.StartsWith("_")) || - typeArgs.All(tp => !tp.Name.StartsWith("_"))); - - if (typeArgs.Count != 0 && !typeArgs[0].Name.StartsWith("_")) { - wr.Write("<{0}>", Util.Comma(typeArgs, TypeParamString)); - } - } - - public string TypeParamString(TypeParameter tp) { - Contract.Requires(tp != null); - string variance; - switch (tp.VarianceSyntax) { - case TypeParameter.TPVarianceSyntax.Covariant_Permissive: - variance = "*"; - break; - case TypeParameter.TPVarianceSyntax.Covariant_Strict: - variance = "+"; - break; - case TypeParameter.TPVarianceSyntax.NonVariant_Permissive: - variance = "!"; - break; - case TypeParameter.TPVarianceSyntax.NonVariant_Strict: - variance = ""; - break; - case TypeParameter.TPVarianceSyntax.Contravariance: - variance = "-"; - break; - default: - Contract.Assert(false); // unexpected VarianceSyntax - throw new cce.UnreachableException(); - } - return variance + tp.Name + TPCharacteristicsSuffix(tp.Characteristics); - } - - private void PrintArrowType(string arrow, string internalName, List typeArgs) { - Contract.Requires(arrow != null); - Contract.Requires(internalName != null); - Contract.Requires(typeArgs != null); - Contract.Requires(1 <= typeArgs.Count); // argument list ends with the result type - wr.Write(" /*{0}*/ ", internalName); - int arity = typeArgs.Count - 1; - if (arity != 1) { - wr.Write("("); - } - wr.Write(Util.Comma(arity, i => TypeParamString(typeArgs[i]))); - if (arity != 1) { - wr.Write(")"); - } - wr.Write(" {0} {1}", arrow, TypeParamString(typeArgs[arity])); - } - - private void PrintTypeInstantiation(List typeArgs) { - Contract.Requires(typeArgs == null || typeArgs.Count != 0); - wr.Write(Type.TypeArgsToString(options, typeArgs)); - } - - public void PrintDatatype(DatatypeDecl dt, int indent, string fileBeingPrinted) { - Contract.Requires(dt != null); - Indent(indent); - PrintClassMethodHelper(dt is IndDatatypeDecl ? "datatype" : "codatatype", dt.Attributes, dt.Name, dt.TypeArgs); - PrintExtendsClause(dt); - wr.Write(" ="); - string sep = ""; - foreach (DatatypeCtor ctor in dt.Ctors) { - wr.Write(sep); - PrintClassMethodHelper(ctor.IsGhost ? " ghost" : "", ctor.Attributes, ctor.Name, new List()); - if (ctor.Formals.Count != 0) { - PrintFormals(ctor.Formals, null); - } - sep = " |"; - } - if (dt.Members.Count == 0) { - wr.WriteLine(); - } else { - wr.WriteLine(" {"); - PrintMembers(dt.Members, indent + IndentAmount, fileBeingPrinted); - Indent(indent); - wr.WriteLine("}"); - } - } - - /// - /// Prints a space before each attribute. - /// - public void PrintAttributes(Attributes a) { - if (a != null) { - PrintAttributes(a.Prev); - wr.Write(" "); - PrintOneAttribute(a); - } - } - public void PrintOneAttribute(Attributes a, string nameSubstitution = null) { - Contract.Requires(a != null); - var name = nameSubstitution ?? a.Name; - var usAttribute = name.StartsWith("_") || (options.DisallowExterns && name == "extern"); - wr.Write("{1}{{:{0}", name, usAttribute ? "/*" : ""); - if (a.Args != null) { - PrintAttributeArgs(a.Args, false); - } - wr.Write("}}{0}", usAttribute ? "*/" : ""); - - } - - public void PrintAttributeArgs(List args, bool isFollowedBySemicolon) { - Contract.Requires(args != null); - string prefix = " "; - foreach (var arg in args) { - Contract.Assert(arg != null); - wr.Write(prefix); - prefix = ", "; - PrintExpression(arg, isFollowedBySemicolon); - } - } - - public void PrintField(Field field, int indent) { - Contract.Requires(field != null); - Indent(indent); - if (field.HasStaticKeyword) { - wr.Write("static "); - } - if (field.IsGhost) { - wr.Write("ghost "); - } - if (field is ConstantField) { - wr.Write("const"); - } else { - wr.Write("var"); - } - PrintAttributes(field.Attributes); - wr.Write(" {0}", field.Name); - if (ShowType(field.Type)) { - wr.Write(": "); - PrintType(field.Type); - } - if (field is ConstantField) { - var c = (ConstantField)field; - if (c.Rhs != null) { - wr.Write(" := "); - PrintExpression(c.Rhs, true); - } - } else if (field.IsUserMutable) { - // nothing more to say - } else if (field.IsMutable) { - wr.Write(" // non-assignable"); - } else { - wr.Write(" // immutable"); - } - wr.WriteLine(); - } - - public void PrintFunction(Function f, int indent, bool printSignatureOnly) { - Contract.Requires(f != null); - - if (PrintModeSkipFunctionOrMethod(f.IsGhost, f.Attributes, f.Name)) { return; } - Indent(indent); - PrintClassMethodHelper(f.GetFunctionDeclarationKeywords(options), f.Attributes, f.Name, f.TypeArgs); - if (f.SignatureIsOmitted) { - wr.Write(" ..."); - } else { - if (f is ExtremePredicate) { - PrintKTypeIndication(((ExtremePredicate)f).TypeOfK); - } - PrintFormals(f.Formals, f, f.Name); - if (f.Result != null || (f is not Predicate && f is not ExtremePredicate && f is not TwoStatePredicate && f is not PrefixPredicate)) { - wr.Write(": "); - if (f.Result != null) { - wr.Write("("); - PrintFormal(f.Result, false); - wr.Write(")"); - } else { - PrintType(f.ResultType); - } - } - } - - int ind = indent + IndentAmount; - PrintSpec("requires", f.Req, ind); - PrintFrameSpecLine("reads", f.Reads, ind); - PrintSpec("ensures", f.Ens, ind); - PrintDecreasesSpec(f.Decreases, ind); - wr.WriteLine(); - if (f.Body != null && !printSignatureOnly) { - Indent(indent); - wr.WriteLine("{"); - PrintExtendedExpr(f.Body, ind, true, false); - Indent(indent); - wr.Write("}"); - if (f.ByMethodBody != null) { - wr.Write(" by method "); - if (options.DafnyPrintResolvedFile != null && f.ByMethodDecl != null) { - Contract.Assert(f.ByMethodDecl.Ens.Count == 1); - wr.Write("/* ensures"); - PrintAttributedExpression(f.ByMethodDecl.Ens[0]); - wr.Write(" */ "); - } - PrintStatement(f.ByMethodBody, indent); - } - wr.WriteLine(); - } - } - - // ----------------------------- PrintMethod ----------------------------- - - const int IndentAmount = 2; // The amount of indent for each new scope - void Indent(int amount) { - Contract.Requires(0 <= amount); - wr.Write(new String(' ', amount)); - } - - private bool PrintModeSkipFunctionOrMethod(bool IsGhost, Attributes attributes, string name) { - if (printMode == PrintModes.NoGhost && IsGhost) { return true; } - if (printMode == PrintModes.NoIncludes || printMode == PrintModes.NoGhost) { - bool verify = true; - if (Attributes.ContainsBool(attributes, "verify", ref verify) && !verify) { return true; } - if (name.Contains("INTERNAL") || name.StartsWith("reveal_")) { 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; - } - - public void PrintMethod(Method method, int indent, bool printSignatureOnly) { - Contract.Requires(method != null); - - if (PrintModeSkipFunctionOrMethod(method.IsGhost, method.Attributes, method.Name)) { return; } - Indent(indent); - string k = method is Constructor ? "constructor" : - method is LeastLemma ? "least lemma" : - method is GreatestLemma ? "greatest lemma" : - method is Lemma || method is PrefixLemma ? "lemma" : - method is TwoStateLemma ? "twostate lemma" : - "method"; - if (method.HasStaticKeyword) { k = "static " + k; } - if (method.IsGhost && !method.IsLemmaLike) { - k = "ghost " + k; - } - string nm = method is Constructor && !((Constructor)method).HasName ? "" : method.Name; - PrintClassMethodHelper(k, method.Attributes, nm, method.TypeArgs); - if (method.SignatureIsOmitted) { - wr.Write(" ..."); - } else { - if (method is ExtremeLemma) { - PrintKTypeIndication(((ExtremeLemma)method).TypeOfK); - } - PrintFormals(method.Ins, method, method.Name); - if (method.Outs.Count != 0) { - if (method.Ins.Count + method.Outs.Count <= 3) { - wr.Write(" returns "); - } else { - wr.WriteLine(); - Indent(indent + 2 * IndentAmount); - wr.Write("returns "); - } - PrintFormals(method.Outs, method); - } - } - - int ind = indent + IndentAmount; - PrintSpec("requires", method.Req, ind); - var readsExpressions = method.Reads.Expressions; - if (readsExpressions != null) { - var isDefault = readsExpressions.Count == 1 && readsExpressions[0].E is WildcardExpr; - if (!isDefault) { - PrintFrameSpecLine("reads", method.Reads, ind); - } - } - if (method.Mod.Expressions != null) { - PrintFrameSpecLine("modifies", method.Mod, ind); - } - PrintSpec("ensures", method.Ens, ind); - PrintDecreasesSpec(method.Decreases, ind); - wr.WriteLine(); - - if (method.Body != null && !printSignatureOnly) { - Indent(indent); - PrintStatement(method.Body, indent); - wr.WriteLine(); - } - } - - void PrintKTypeIndication(ExtremePredicate.KType kType) { - switch (kType) { - case ExtremePredicate.KType.Nat: - wr.Write("[nat]"); - break; - case ExtremePredicate.KType.ORDINAL: - wr.Write("[ORDINAL]"); - break; - case ExtremePredicate.KType.Unspecified: - break; - default: - Contract.Assume(false); // unexpected KType value - break; - } - } - - internal void PrintFormals(List ff, ICallable/*?*/ context, string name = null) { - Contract.Requires(ff != null); - if (name != null && name.EndsWith("#")) { - wr.Write("["); - PrintFormal(ff[0], false); - wr.Write("]"); - ff = new List(ff.Skip(1)); - } - wr.Write("("); - string sep = ""; - foreach (Formal f in ff) { - Contract.Assert(f != null); - wr.Write(sep); - sep = ", "; - PrintFormal(f, (context is TwoStateLemma || context is TwoStateFunction) && f.InParam); - } - wr.Write(")"); - } - - void PrintFormal(Formal f, bool showNewKeyword) { - Contract.Requires(f != null); - if (showNewKeyword && !f.IsOld) { - wr.Write("new "); - } - if (f.IsOlder) { - Contract.Assert(f.HasName); - wr.Write("older "); - } - if (f.IsGhost) { - wr.Write("ghost "); - } - if (f.IsNameOnly) { - Contract.Assert(f.HasName); - wr.Write("nameonly "); - } - if (f.HasName) { - wr.Write("{0}: ", f.DisplayName); - } - PrintType(f.Type); - if (f.DefaultValue != null) { - wr.Write(" := "); - PrintExpression(f.DefaultValue, false); - } - } - - internal void PrintDecreasesSpec(Specification decs, int indent) { - Contract.Requires(decs != null); - if (printMode == PrintModes.NoGhost) { return; } - if (decs.Expressions != null && decs.Expressions.Count != 0) { - wr.WriteLine(); - Indent(indent); - wr.Write("decreases"); - if (decs.HasAttributes()) { - PrintAttributes(decs.Attributes); - } - wr.Write(" "); - PrintExpressionList(decs.Expressions, true); - } - } - - internal void PrintFrameSpecLine(string kind, Specification ee, int indent) { - Contract.Requires(kind != null); - Contract.Requires(ee != null); - if (ee != null && ee.Expressions != null && ee.Expressions.Count != 0) { - wr.WriteLine(); - Indent(indent); - wr.Write("{0}", kind); - PrintAttributes(ee.Attributes); - wr.Write(" "); - PrintFrameExpressionList(ee.Expressions); - } - } - - internal void PrintSpec(string kind, List ee, int indent) { - Contract.Requires(kind != null); - Contract.Requires(ee != null); - if (printMode == PrintModes.NoGhost) { return; } - foreach (AttributedExpression e in ee) { - Contract.Assert(e != null); - wr.WriteLine(); - Indent(indent); - wr.Write("{0}", kind); - PrintAttributedExpression(e); - } - } - - void PrintAttributedExpression(AttributedExpression e) { - Contract.Requires(e != null); - - if (e.HasAttributes()) { - PrintAttributes(e.Attributes); - } - - wr.Write(" "); - if (e.Label != null) { - wr.Write("{0}: ", e.Label.Name); - } - PrintExpression(e.E, true); - } - - // ----------------------------- PrintType ----------------------------- - - public void PrintType(Type ty) { - Contract.Requires(ty != null); - wr.Write(ty.TypeName(options, null, true)); - } - - public void PrintType(string prefix, Type ty) { - Contract.Requires(prefix != null); - Contract.Requires(ty != null); - if (options.DafnyPrintResolvedFile != null) { - ty = AdjustableType.NormalizeSansAdjustableType(ty); - } - string s = ty.TypeName(options, null, true); - if (ty is AdjustableType or not TypeProxy && !s.StartsWith("_")) { - wr.Write("{0}{1}", prefix, s); - } - } - - public string TPCharacteristicsSuffix(TypeParameter.TypeParameterCharacteristics characteristics) { - string s = null; - if (characteristics.EqualitySupport == TypeParameter.EqualitySupportValue.Required || - (characteristics.EqualitySupport == TypeParameter.EqualitySupportValue.InferredRequired && options.DafnyPrintResolvedFile != null)) { - s = "=="; - } - if (characteristics.HasCompiledValue) { - var prefix = s == null ? "" : s + ","; - s = prefix + "0"; - } else if (characteristics.IsNonempty) { - var prefix = s == null ? "" : s + ","; - s = prefix + "00"; - } - if (characteristics.ContainsNoReferenceTypes) { - var prefix = s == null ? "" : s + ","; - s = prefix + "!new"; - } - if (s == null) { - return ""; - } else { - return "(" + s + ")"; - } - } - - bool ShowType(Type t) { - Contract.Requires(t != null); - return !(t is TypeProxy) || options.DafnyPrintResolvedFile != null; - } - - // ----------------------------- PrintStatement ----------------------------- - - /// - /// Prints from the current position of the current line. - /// If the statement requires several lines, subsequent lines are indented at "indent". - /// No newline is printed after the statement. - /// - public void PrintStatement(Statement stmt, int indent) { - Contract.Requires(stmt != null); - - if (stmt.IsGhost && printMode == PrintModes.NoGhost) { return; } - for (LList