Pretty-printing imports

This module defines the following utilities for pretty-printing imports:

• ImportGraph.Lean.Import.pretty and prettyHeader for printing Array Import as source blocks or headers, respectively.
  • These take an optional Import.FormatBehavior parameter to control import sorting and grouping. By default, imports are grouped by visibility (public/(private)/all), sorted by phase and module name, and visibility groups are separated by extra newlines.
• headerToImportRefs(WithWhitespace) to track source positions and comments around existing imports in source
• prettyWithSourceWhitespace to pretty-print new Imports while attaching comments from source header syntax. This allows us to reformat existing imports while preserving e.g. shake annotations (and any other informative comments).
  • If comments cannot be carried over (or may no longer apply), this is (by default) explained in a comment shown below the import block.
• mkImportSuggestionMessage, which creates a suggestion reformatting imports. This is used by #norm_imports.

Future Work

• Some parts of this API only work in the module system. In general, we should also support non-modules.

structure ImportGraph.Lean.ImportRef extends Lean.Import : Type

Extends Import with stx : TSyntax `Lean.Parser.Module.import to allow reporting at the given import and processing of whitespace.

• module : Name
• importAll : Bool
• isExported : Bool
• isMeta : Bool
• stx : Lean.TSyntax `Lean.Parser.Module.import

def ImportGraph.Lean.instReprImportRef.repr : ImportRef → Nat → Std.Format

@[instance_reducible]

instance ImportGraph.Lean.instReprImportRef : Repr ImportRef

@[instance_reducible]

instance ImportGraph.Lean.instInhabitedImportRef : Inhabited ImportRef

def ImportGraph.Lean.instBEqImportRef.beq : ImportRef → ImportRef → Bool

@[instance_reducible]

instance ImportGraph.Lean.instBEqImportRef : BEq ImportRef

def ImportGraph.Lean.ImportRef.getIdent (i : ImportRef) : Lean.Ident

Returns the module Ident (following (public)? (meta)? import (all)? of a given ImportRef. Returns .missing if the identifier somehow has a dangling dot (the parser should, however, never succeed in producing such syntax) or is otherwise malformed.

def ImportGraph.Lean.headerToImportStx (header : Lean.TSyntax `Lean.Parser.Module.header) : Lean.TSyntaxArray `Lean.Parser.Module.import

Destructures header syntax ((module)? (prelude)? $imports*) into an array of Imports together with the import syntax that gave rise to them. Creates an array of .missing when the syntax is malformed. See also headerToImports.

def ImportGraph.Lean.getModule (header : Lean.TSyntax `Lean.Parser.Module.header) : Option Lean.Syntax

Destructures header syntax ((module)? (prelude)? $imports*) into an array of Imports together with the import syntax that gave rise to them. See also headerToImports.

def ImportGraph.Lean.headerToImportRefs (header : Lean.TSyntax `Lean.Parser.Module.header) : Array ImportRef

Destructures header syntax ((module)? (prelude)? $imports*) into an array of Imports together with the import syntax that gave rise to them. See also headerToImports.

def ImportGraph.Lean.Import.comparePretty (i₁ i₂ : Lean.Import) : Ordering

Considers imports with public to come first; then those without all; then those with meta; then compares the modules alphabetically.

def ImportGraph.Lean.ImportRef.comparePretty (i₁ i₂ : ImportRef) : Ordering

Considers imports with public to come first; then those without all; then those with meta; then compares the modules alphabetically; then compares starting source position, c considering those without a starting position to come first.

@[instance_reducible]

def ImportGraph.Lean.Import.instImportOrdPretty : Ord Lean.Import

Uses Import.comparePretty. Not tagged as an instance by default.

@[instance_reducible]

def ImportGraph.Lean.Import.instImportRefOrdPretty : Ord ImportRef

Uses ImportRef.comparePretty. Not tagged as an instance by default.

def ImportGraph.Lean.Import.beqUpToOrder (imps₁ imps₂ : Array Lean.Import) : Bool

Whether two Array Imports contain the same imports when considered as a (multi)set.

structure ImportGraph.Lean.Import.Whitespace : Type

Whitespace (including comments) surrounding an import.

• leading : String

  The leading whitespace after regrouping whitespace so that trailing does not include newlines. Includes exactly one newline of ASCII whitespace at the end of leading if there are non-whitespace characters in it (which is suitable for normalized import comments), and no ASCII whitespace at the beginning. If there are no non-ASCII-whitespace characters in leading, it is empty.

• trailing : String

  The trailing whitespace after regrouping whitespace so that the trailing whitespace has no newlines. May have ASCII whitespace on the left.

def ImportGraph.Lean.Import.instReprWhitespace.repr : Whitespace → Nat → Std.Format

@[instance_reducible]

instance ImportGraph.Lean.Import.instReprWhitespace : Repr Whitespace

@[instance_reducible]

instance ImportGraph.Lean.Import.instInhabitedWhitespace : Inhabited Whitespace

def ImportGraph.Lean.Import.instHashableWhitespace.hash : Whitespace → UInt64

@[instance_reducible]

instance ImportGraph.Lean.Import.instHashableWhitespace : Hashable Whitespace

@[instance_reducible]

instance ImportGraph.Lean.Import.instBEqWhitespace : BEq Whitespace

def ImportGraph.Lean.Import.instBEqWhitespace.beq : Whitespace → Whitespace → Bool

def ImportGraph.Lean.Import.instToJsonWhitespace.toJson : Whitespace → Lean.Json

@[instance_reducible]

instance ImportGraph.Lean.Import.instToJsonWhitespace : Lean.ToJson Whitespace

@[instance_reducible]

instance ImportGraph.Lean.Import.instFromJsonWhitespace : Lean.FromJson Whitespace

def ImportGraph.Lean.Import.instFromJsonWhitespace.fromJson : Lean.Json → Except String Whitespace

@[instance_reducible]

instance ImportGraph.Lean.Import.Whitespace.instOrd : Ord Whitespace

Sorts whitespace first by leading length, then trailing length, then alphabetical in each.

@[instance_reducible]

instance ImportGraph.Lean.Import.Whitespace.instOrdProdImport : Ord (Lean.Import × Whitespace)

@[inline]

def ImportGraph.Lean.Import.Whitespace.around {α : Type u_1} (a : α) (ws : Whitespace) [Std.ToFormat α] : Std.Format

Formats a with the whitespace ws wrapped around it.

@[inline]

def ImportGraph.Lean.Import.Whitespace.empty : Whitespace

Whitespace with empty strings for both the leading and trailing values.

@[inline]

def ImportGraph.Lean.Import.Whitespace.isEmpty (ws : Whitespace) : Bool

Whether both the leading and trailing fields of Whitespace are empty.

@[instance_reducible]

instance ImportGraph.Lean.Import.Whitespace.instToFormatProdImport : Std.ToFormat (Lean.Import × Whitespace)

def ImportGraph.headerToImportRefsWithWhitespace (header : Lean.TSyntax `Lean.Parser.Module.header) : Array (Lean.ImportRef × Lean.Import.Whitespace)

Convert parsed header syntax into ImportRefs after regrouping leading and trailing whitespace so that trailing whitespace has no newlines, and extract the leading and trailing whitespace into a useful ASCII-whitespace normalized form in Whitespace.

inductive ImportGraph.Lean.Import.FormatBehavior : Type

A configuration option guiding the behavior of import block pretty-printing functions (e.g ImportGraph.Lean.Import.pretty) which determines the order and grouping of imports.

• none : Import.FormatBehavior

  Does not sort or group imports at all.

• sorted : Import.FormatBehavior

  Sorts an array of imports first by visibility (public first, then private (no token), then all), then by phase (meta imports first), then alphabetically.

• grouped (splitMeta : Bool := false) : Import.FormatBehavior

  Groups imports by visibility (first public, then private (no token), then all) with an extra newline in between groups. Within groups, sorts first by the meta token then alphabetically within groups. If splitMeta := true (default: false), also inserts an extra newline between meta imports and non-meta imports.

@[inline]

def ImportGraph.Lean.Import.sortPretty (imports : Array Lean.Import) : Array Lean.Import

Sorts an array of imports first by visibility (public first, then private (no token), then all), then by phase (meta imports first), then alphabetically.

@[inline]

def ImportGraph.Lean.ImportRef.sortPretty (imports : Array ImportRef) : Array ImportRef

Sorts an array of imports first by visibility (public first, then private (no token), then all), then by phase (meta imports first), then alphabetically.

@[inline]

def ImportGraph.Lean.Import.pretty (imports : Array Lean.Import) (formatAs : Import.FormatBehavior := FormatBehavior.grouped) : Std.Format

Pretty-print an array of Imports as a block of import statements (not including module and/ or prelude). The grouping and sorting behavior may be controlled by the formatAs argument.

By default, this function groups imports by visibility (public, private (no token), or all) with an extra newline in between groups, and within groups, sorts first by the meta token then alphabetically. See Import.FormatBehavior for more details.

def ImportGraph.Lean.Import.prettyHeader (imports : Array Lean.Import) (isModule : Bool := true) (isPrelude : Bool := false) (formatAs : Import.FormatBehavior := FormatBehavior.grouped) : Std.Format

Pretty-print an array of Imports as a full header, including te module and prelude tokens as given by isModule (default: true) and isPrelude (default: false).

structure ImportGraph.Lean.Import.FormatErrors : Type

Descriptions of cases in which the import formatting procedure does not know how to proceed.

• multipleTrailing : Array (Lean.Import × Array (ImportRef × String))

  If we have multiple versions of the same import, and each have their own nontrivial trailing whitespace, we don't necessarily know how to combine them. In this case, each ref.toImport matches the imp exactly.

• reviewWhitespace : Array (Lean.Name × Array Lean.Import × Array (ImportRef × Whitespace))

  If a module was originally imported in one manner with nontrivial trailing whitespace, but we now import it in a different manner (e.g. if it was imported multiple times with different modifiers, and we've normalized the imports), then the user should review the whitespace (which may be a shake annotation) to make sure it still makes sense. We also tell the user to review the leading whitespace, just in case.

• unusedWithComments : Array (ImportRef × Whitespace)

  If we no longer use some imports that had nontrivial whitespace, record them here.

def ImportGraph.Lean.Import.instBEqFormatErrors.beq : FormatErrors → FormatErrors → Bool

@[instance_reducible]

instance ImportGraph.Lean.Import.instBEqFormatErrors : BEq FormatErrors

@[instance_reducible]

instance ImportGraph.Lean.Import.instReprFormatErrors : Repr FormatErrors

def ImportGraph.Lean.Import.instReprFormatErrors.repr : FormatErrors → Nat → Std.Format

@[instance_reducible]

instance ImportGraph.Lean.Import.instInhabitedFormatErrors : Inhabited FormatErrors

def ImportGraph.Lean.Import.FormatErrors.isEmpty (errs : FormatErrors) : Bool

def ImportGraph.Lean.Import.collectWithWhitespaceFromSource (newImps : Array Lean.Import) (sourceImps : Array (ImportRef × Whitespace)) : Array (Lean.Import × Whitespace) × FormatErrors

Assumes whitespace has been created with headerToImportRefsWithWhitespace.

@[instance_reducible]

instance ImportGraph.Lean.Import.instToFormatFormatErrors : Std.ToFormat FormatErrors

def ImportGraph.Lean.Import.prettyWithWhitespace (imps : Array (Lean.Import × Whitespace)) (formatAs : Import.FormatBehavior := FormatBehavior.grouped) : Std.Format

Wraps the Whitespace associated with each import around it, and formats the array of imports as an import block according to formatAs.

@[inline]

def ImportGraph.Lean.Import.prettyWithSourceWhitespace (imps : Array Lean.Import) (sourceImps : Array (ImportRef × Whitespace)) (fmtBehavior : Import.FormatBehavior := FormatBehavior.grouped) (includeErrorsAsComment : Bool := true) : Std.Format × FormatErrors

Formats the modified imps and attaches whitespace from the corresponding import in sourceImps when doing so is unambiguous. Ambiguity encountered while assigning nontrivial whitespace is recorded in the returned Array Import.FormatError.

If includeErrorsAsComment := true (the default), the errors are included as a source comment following the formatted import block.

We assume sourceImps has been created by ImportGraph.headerToImportRefsWithWhitespace.

def ImportGraph.Lean.Import.mkImportSuggestionMessage (ref : Lean.Syntax) (newImps : Array Lean.Import) (sourceImps : Array (ImportRef × Whitespace)) (formatAs : Import.FormatBehavior := FormatBehavior.grouped) (toCodeActionTitle? : Option (String → String) := some fun (x : String) => "Modify imports") (includeErrorsAsComment : Bool := true) : Lean.CoreM (Option (Lean.MessageData × FormatErrors))

Create a message that suggests replacing sourceImps with newImps. Includes errors as a comment. Returns none if the suggestion is would not modify the source at all (including whitespace).

Note that the resulting widget will show a diff view if the resulting errs : Import.FormatErrors satisfies errs.isEmpty or includeErrorsAsComment := false. Otherwise, if a comment is included, a try-this widget prefixed by an [apply] is shown. (This is because the repeated imports in errs don't behave well in the diff view.)

ref is passed to Meta.Hint.mkSuggestionsMessage.