inductive Std.Format.FlattenBehavior : Type

Determines how groups should have linebreaks inserted when the text would overfill its remaining space.

• allOrNone will make a linebreak on every Format.line in the group or none of them.

  [1,
   2,
   3]
  

• fill will only make linebreaks on as few Format.lines as possible:

  [1, 2,
   3]
  

• allOrNone : FlattenBehavior

  Either all Format.lines in the group will be newlines, or all of them will be spaces.

• fill : FlattenBehavior

  As few Format.lines in the group as possible will be newlines.

instance Std.Format.instInhabitedFlattenBehavior : Inhabited FlattenBehavior

Equations

• Std.Format.instInhabitedFlattenBehavior = { default := Std.Format.instInhabitedFlattenBehavior.default }

def Std.Format.instInhabitedFlattenBehavior.default : FlattenBehavior

Equations

• Std.Format.instInhabitedFlattenBehavior.default = Std.Format.FlattenBehavior.allOrNone

def Std.Format.instBEqFlattenBehavior.beq : FlattenBehavior → FlattenBehavior → Bool

Equations

• Std.Format.instBEqFlattenBehavior.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Std.Format.instBEqFlattenBehavior : BEq FlattenBehavior

Equations

• Std.Format.instBEqFlattenBehavior = { beq := Std.Format.instBEqFlattenBehavior.beq }

inductive Std.Format : Type

A representation of a set of strings, in which the placement of newlines and indentation differ.

Given a specific line width, specified in columns, the string that uses the fewest lines can be selected.

The pretty-printing algorithm is based on Wadler's paper A Prettier Printer.

• nil : Format

  The empty format.

• line : Format

  A position where a newline may be inserted if the current group does not fit within the allotted column width.

• align (force : Bool) : Format

  align tells the formatter to pad with spaces to the current indentation level, or else add a newline if we are already at or past the indent.

  If force is true, then it will pad to the indent even if it is in a flattened group.

  Example:

  open Std Format in
  #eval IO.println (nest 2 <| "." ++ align ++ "a" ++ line ++ "b")
  

  . a
    b
  

• text : String → Format

  A node containing a plain string.

  If the string contains newlines, the formatter emits them and then indents to the current level.

• nest (indent : Int) (f : Format) : Format

  nest indent f increases the current indentation level by indent while rendering f.

  Example:

  open Std Format in
  def fmtList (l : List Format) : Format :=
    let f := joinSep l  (", " ++ Format.line)
    group (nest 1 <| "[" ++ f ++ "]")
  

  This will be written all on one line, but if the text is too large, the formatter will put in linebreaks after the commas and indent later lines by 1.

• append : Format → Format → Format

  Concatenation of two Formats.

• group : Format → (behavior : optParam FlattenBehavior FlattenBehavior.allOrNone) → Format

  Creates a new flattening group for the given inner Format.

• tag : Nat → Format → Format

  Used for associating auxiliary information (e.g. Exprs) with Format objects.

instance Std.instInhabitedFormat : Inhabited Format

Equations

• Std.instInhabitedFormat = { default := Std.instInhabitedFormat.default }

def Std.instInhabitedFormat.default : Format

Equations

• Std.instInhabitedFormat.default = Std.Format.nil

def Std.Format.isEmpty : Format → Bool

Checks whether the given format contains no characters.

Equations

• Std.Format.nil.isEmpty = true
• Std.Format.line.isEmpty = false
• (Std.Format.align force).isEmpty = true
• (Std.Format.text msg).isEmpty = (msg == "")
• (Std.Format.nest indent f).isEmpty = f.isEmpty
• (f₁.append f₂).isEmpty = (f₁.isEmpty && f₂.isEmpty)
• (f.group behavior).isEmpty = f.isEmpty
• (Std.Format.tag a f).isEmpty = f.isEmpty

def Std.Format.fill (f : Format) : Format

Creates a group in which as few Format.lines as possible are rendered as newlines.

This is an alias for Format.group, with FlattenBehavior set to fill.

Equations

• f.fill = f.group Std.Format.FlattenBehavior.fill

instance Std.Format.instAppend : Append Format

Equations

• Std.Format.instAppend = { append := Std.Format.append }

instance Std.Format.instCoeString : Coe String Format

Equations

• Std.Format.instCoeString = { coe := Std.Format.text }

def Std.Format.join (xs : List Format) : Format

Concatenates a list of Formats with ++.

Equations

• Std.Format.join xs = List.foldl (fun (x1 x2 : Std.Format) => x1 ++ x2) (Std.Format.text "") xs

def Std.Format.isNil : Format → Bool

Checks whether a Format is the constructor Format.nil.

This does not check whether the resulting rendered strings are always empty. To do that, use Format.isEmpty.

Equations

• Std.Format.nil.isNil = true
• x✝.isNil = false

inductive Std.Format.FlattenAllowability : Type

A directive indicating whether a given work group is able to be flattened.

• allow indicates that the group is allowed to be flattened; its argument is true if there is sufficient space for it to be flattened (and so it should be), or false if not.
• disallow means that this group should not be flattened irrespective of space concerns. This is used at levels of a Format outside of any flattening groups. It is necessary to track this so that, after a hard line break, we know whether to try to flatten the next line.

• allow (fits : Bool) : FlattenAllowability
• disallow : FlattenAllowability

def Std.Format.instBEqFlattenAllowability.beq : FlattenAllowability → FlattenAllowability → Bool

Equations

• Std.Format.instBEqFlattenAllowability.beq (Std.Format.FlattenAllowability.allow a) (Std.Format.FlattenAllowability.allow b) = (a == b)
• Std.Format.instBEqFlattenAllowability.beq Std.Format.FlattenAllowability.disallow Std.Format.FlattenAllowability.disallow = true
• Std.Format.instBEqFlattenAllowability.beq x✝¹ x✝ = false

instance Std.Format.instBEqFlattenAllowability : BEq FlattenAllowability

Equations

• Std.Format.instBEqFlattenAllowability = { beq := Std.Format.instBEqFlattenAllowability.beq }

def Std.Format.FlattenAllowability.shouldFlatten : FlattenAllowability → Bool

Whether the given directive indicates that flattening should occur.

Equations

• (Std.Format.FlattenAllowability.allow true).shouldFlatten = true
• x✝.shouldFlatten = false

class Std.Format.MonadPrettyFormat (m : Type → Type) : Type

A monad that can be used to incrementally render Format objects.

• pushOutput (s : String) : m Unit

  Emits the string s.

• pushNewline (indent : Nat) : m Unit

  Emits a newline followed by indent columns of indentation.

• currColumn : m Nat

  Gets the current column at which the next string will be emitted.

• startTag (tag : Nat) : m Unit

  Starts a region tagged with tag.

• endTags (count : Nat) : m Unit

  Exits the scope of count opened tags.

def Std.Format.prettyM {m : Type → Type} (f : Format) (w : Nat) (indent : Nat := 0) [Monad m] [MonadPrettyFormat m] : m Unit

Renders a Format using effects in the monad m, using the methods of MonadPrettyFormat.

Each line is emitted as soon as it is rendered, rather than waiting for the entire document to be rendered.

• w: the total width
• indent: the initial indentation to use for wrapped lines (subsequent wrapping may increase the indentation)

Equations

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

@[inline]

def Std.Format.bracket (l : String) (f : Format) (r : String) : Format

Creates a format l ++ f ++ r with a flattening group, nesting the contents by the length of l.

The group's FlattenBehavior is allOrNone; for fill use Std.Format.bracketFill.

Equations

• Std.Format.bracket l f r = (Std.Format.nest (↑(String.Internal.length l)) (Std.Format.text l ++ f ++ Std.Format.text r)).group

@[inline]

def Std.Format.paren (f : Format) : Format

Creates the format "(" ++ f ++ ")" with a flattening group, nesting by one space.

Equations

• f.paren = Std.Format.bracket "(" f ")"

@[inline]

def Std.Format.sbracket (f : Format) : Format

Creates the format "[" ++ f ++ "]" with a flattening group, nesting by one space.

sbracket is short for “square bracket”.

Equations

• f.sbracket = Std.Format.bracket "[" f "]"

@[inline]

def Std.Format.bracketFill (l : String) (f : Format) (r : String) : Format

Creates a format l ++ f ++ r with a flattening group, nesting the contents by the length of l.

The group's FlattenBehavior is fill; for allOrNone use Std.Format.bracketFill.

Equations

• Std.Format.bracketFill l f r = (Std.Format.nest (↑(String.Internal.length l)) (Std.Format.text l ++ f ++ Std.Format.text r)).fill

def Std.Format.defIndent : Nat

The default indentation level, which is two spaces.

Equations

• Std.Format.defIndent = 2

def Std.Format.defUnicode : Bool

Equations

• Std.Format.defUnicode = true

def Std.Format.defWidth : Nat

The default width of the targeted output, which is 120 columns.

Equations

• Std.Format.defWidth = 120

def Std.Format.nestD (f : Format) : Format

Increases the indentation level by the default amount.

Equations

• f.nestD = Std.Format.nest (↑Std.Format.defIndent) f

def Std.Format.indentD (f : Format) : Format

Insert a newline and then f, all nested by the default indent amount.

Equations

• f.indentD = (Std.Format.line ++ f).nestD

@[export lean_format_pretty]

def Std.Format.pretty (f : Format) (width : Nat := defWidth) (indent column : Nat := 0) : String

Renders a Format to a string.

• width: the total width
• indent: the initial indentation to use for wrapped lines (subsequent wrapping may increase the indentation)
• column: begin the first line wrap column characters earlier than usual (this is useful when the output String will be printed starting at column)

Equations

• f.pretty width indent column = Std.Format.State.out✝ (f.prettyM width indent { column := column }).snd

class Std.ToFormat (α : Type u) : Type u

Specifies a “user-facing” way to convert from the type α to a Format object. There is no expectation that the resulting string is valid code.

The Repr class is similar, but the expectation is that instances produce valid Lean code.

• format : α → Format

  Converts a value to a Format object, with no expectation that the resulting string is valid code.

instance Std.instToFormatFormat : ToFormat Format

Equations

• Std.instToFormatFormat = { format := fun (f : Std.Format) => f }

instance Std.instToFormatString : ToFormat String

Equations

• Std.instToFormatString = { format := fun (s : String) => Std.Format.text s }

def Std.Format.joinSep {α : Type u} [ToFormat α] : List α → Format → Format

Intercalates the given list with the given sep format.

The list items are formatting using ToFormat.format.

Equations

• Std.Format.joinSep [] x✝ = Std.Format.nil
• Std.Format.joinSep [a] x✝ = Std.format a
• Std.Format.joinSep (a :: as) x✝ = List.foldl (fun (x1 : Std.Format) (x2 : α) => x1 ++ x✝ ++ Std.format x2) (Std.format a) as

def Std.Format.prefixJoin {α : Type u} [ToFormat α] (pre : Format) : List α → Format

Concatenates the given list after prepending pre to each element.

The list items are formatting using ToFormat.format.

Equations

• pre.prefixJoin [] = Std.Format.nil
• pre.prefixJoin (a :: as) = List.foldl (fun (x1 : Std.Format) (x2 : α) => x1 ++ pre ++ Std.format x2) (pre ++ Std.format a) as

def Std.Format.joinSuffix {α : Type u} [ToFormat α] : List α → Format → Format

Concatenates the given list after appending the given suffix to each element.

The list items are formatting using ToFormat.format.

Equations

• Std.Format.joinSuffix [] x✝ = Std.Format.nil
• Std.Format.joinSuffix (a :: as) x✝ = List.foldl (fun (x1 : Std.Format) (x2 : α) => x1 ++ Std.format x2 ++ x✝) (Std.format a ++ x✝) as