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.ImportRefextends 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

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance ImportGraph.Lean.instReprImportRef : Repr ImportRef

Equations

• ImportGraph.Lean.instReprImportRef = { reprPrec := ImportGraph.Lean.instReprImportRef.repr }

@[instance_reducible]

instance ImportGraph.Lean.instInhabitedImportRef : Inhabited ImportRef

Equations

• ImportGraph.Lean.instInhabitedImportRef = { default := ImportGraph.Lean.instInhabitedImportRef.default }

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

Equations

• ImportGraph.Lean.instBEqImportRef.beq { toImport := a, stx := a_1 } { toImport := b, stx := b_1 } = (a == b && a_1 == b_1)
• ImportGraph.Lean.instBEqImportRef.beq x✝¹ x✝ = false

@[instance_reducible]

instance ImportGraph.Lean.instBEqImportRef : BEq ImportRef

Equations

• ImportGraph.Lean.instBEqImportRef = { beq := ImportGraph.Lean.instBEqImportRef.beq }

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• i₁.comparePretty i₂ = (ImportGraph.Lean.Import.comparePretty i₁.toImport i₂.toImport).then (compare i₁.stx.raw.getPos? i₂.stx.raw.getPos?)

@[instance_reducible]

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

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

Equations

• ImportGraph.Lean.Import.instImportOrdPretty = { compare := ImportGraph.Lean.Import.comparePretty }

@[instance_reducible]

def ImportGraph.Lean.Import.instImportRefOrdPretty : Ord ImportRef

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

Equations

• ImportGraph.Lean.Import.instImportRefOrdPretty = { compare := ImportGraph.Lean.ImportRef.comparePretty }

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.

Equations

• ImportGraph.Lean.Import.beqUpToOrder imps₁ imps₂ = (imps₁.qsortOrd == imps₂.qsortOrd)

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

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance ImportGraph.Lean.Import.instReprWhitespace : Repr Whitespace

Equations

• ImportGraph.Lean.Import.instReprWhitespace = { reprPrec := ImportGraph.Lean.Import.instReprWhitespace.repr }

@[instance_reducible]

instance ImportGraph.Lean.Import.instInhabitedWhitespace : Inhabited Whitespace

Equations

• ImportGraph.Lean.Import.instInhabitedWhitespace = { default := ImportGraph.Lean.Import.instInhabitedWhitespace.default }

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

Equations

• ImportGraph.Lean.Import.instHashableWhitespace.hash { leading := a, trailing := a_1 } = mixHash (mixHash 0 (hash a)) (hash a_1)

@[instance_reducible]

instance ImportGraph.Lean.Import.instHashableWhitespace : Hashable Whitespace

Equations

• ImportGraph.Lean.Import.instHashableWhitespace = { hash := ImportGraph.Lean.Import.instHashableWhitespace.hash }

@[instance_reducible]

instance ImportGraph.Lean.Import.instBEqWhitespace : BEq Whitespace

Equations

• ImportGraph.Lean.Import.instBEqWhitespace = { beq := ImportGraph.Lean.Import.instBEqWhitespace.beq }

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

Equations

• ImportGraph.Lean.Import.instBEqWhitespace.beq { leading := a, trailing := a_1 } { leading := b, trailing := b_1 } = (a == b && a_1 == b_1)
• ImportGraph.Lean.Import.instBEqWhitespace.beq x✝¹ x✝ = false

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

Equations

• ImportGraph.Lean.Import.instToJsonWhitespace.toJson x✝ = Lean.Json.mkObj [[("leading", Lean.toJson x✝.leading)], [("trailing", Lean.toJson x✝.trailing)]].flatten

@[instance_reducible]

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

Equations

• ImportGraph.Lean.Import.instToJsonWhitespace = { toJson := ImportGraph.Lean.Import.instToJsonWhitespace.toJson }

@[instance_reducible]

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

Equations

• ImportGraph.Lean.Import.instFromJsonWhitespace = { fromJson? := ImportGraph.Lean.Import.instFromJsonWhitespace.fromJson }

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

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

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

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

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[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.

Equations

• ImportGraph.Lean.Import.Whitespace.around a ws = Std.format ws.leading ++ Std.format a ++ Std.format ws.trailing

@[inline]

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

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

Equations

• ImportGraph.Lean.Import.Whitespace.empty = { leading := "", trailing := "" }

@[inline]

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

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

Equations

• ws.isEmpty = (ws.leading.isEmpty && ws.trailing.isEmpty)

@[instance_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• ImportGraph.Lean.Import.sortPretty imports = imports.qsortOrd

@[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.

Equations

• ImportGraph.Lean.ImportRef.sortPretty imports = imports.qsortOrd

@[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.

Equations

• One or more equations did not get rendered due to their size.
• ImportGraph.Lean.Import.pretty imports ImportGraph.Lean.Import.FormatBehavior.sorted = Std.Format.joinSep (ImportGraph.Lean.Import.sortPretty imports).toList (Std.format "\n")
• ImportGraph.Lean.Import.pretty imports ImportGraph.Lean.Import.FormatBehavior.none = Std.Format.joinSep imports.toList (Std.format "\n")

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).

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.
• ImportGraph.Lean.Import.instBEqFormatErrors.beq x✝¹ x✝ = false

@[instance_reducible]

instance ImportGraph.Lean.Import.instBEqFormatErrors : BEq FormatErrors

Equations

• ImportGraph.Lean.Import.instBEqFormatErrors = { beq := ImportGraph.Lean.Import.instBEqFormatErrors.beq }

@[instance_reducible]

instance ImportGraph.Lean.Import.instReprFormatErrors : Repr FormatErrors

Equations

• ImportGraph.Lean.Import.instReprFormatErrors = { reprPrec := ImportGraph.Lean.Import.instReprFormatErrors.repr }

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

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance ImportGraph.Lean.Import.instInhabitedFormatErrors : Inhabited FormatErrors

Equations

• ImportGraph.Lean.Import.instInhabitedFormatErrors = { default := ImportGraph.Lean.Import.instInhabitedFormatErrors.default }

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

Equations

• errs.isEmpty = (errs.multipleTrailing.isEmpty && errs.reviewWhitespace.isEmpty && errs.unusedWithComments.isEmpty)

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.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

@[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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.