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
• fill : FlattenBehavior

instance Std.Format.instInhabitedFlattenBehavior : Inhabited FlattenBehavior

Equations

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

instance Std.Format.instBEqFlattenBehavior : BEq FlattenBehavior

Equations

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

inductive Std.Format : Type

A string with pretty-printing information for rendering in a column-width-aware way.

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 indent, or else add a newline if we are already at or past the indent. For example:

  nest 2 <| "." ++ align ++ "a" ++ line ++ "b"
  

  results in:

  . a
    b
  

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

• text : String → Format

  A node containing a plain string.

• nest (indent : Int) : Format → Format

  nest n f tells the formatter that f is nested inside something with length n so that it is pretty-printed with the correct indentation on a line break. For example, we can define a formatter for list l : List Format as:

  let f := join <| l.intersperse <| ", " ++ 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.Format.nil }

def Std.Format.isEmpty : Format → Bool

Check 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

Alias for a 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

Equations

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

def Std.Format.isNil : Format → Bool

Equations

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

instance Std.Format.instInhabitedSpaceResult : Inhabited Std.Format.SpaceResult✝

Equations

• Std.Format.instInhabitedSpaceResult = { default := { foundLine := default, foundFlattenedHardLine := default, space := default } }

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

instance Std.Format.instBEqFlattenAllowability : BEq FlattenAllowability

Equations

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

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 in which we can pretty-print Format objects.

• pushOutput (s : String) : m Unit
• pushNewline (indent : Nat) : m Unit
• currColumn : m Nat
• startTag : Nat → m Unit

  Start a scope tagged with n.

• endTags : Nat → m Unit

  Exit the scope of n-many opened tags.

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

Render the given f : Format with a line width of w. indent is the starting amount to indent each line by.

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

Create a format l ++ f ++ r with a flatten group. FlattenBehaviour is allOrNone; for fill use bracketFill.

Equations

• Std.Format.bracket l f r = (Std.Format.nest (↑l.length) (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.

Equations

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

@[inline]

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

Creates the format "[" ++ f ++ "]" with a flattening group.

Equations

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

@[inline]

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

Same as bracket except uses the fill flattening behaviour.

Equations

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

def Std.Format.defIndent : Nat

Default indentation.

Equations

• Std.Format.defIndent = 2

def Std.Format.defUnicode : Bool

Equations

• Std.Format.defUnicode = true

def Std.Format.defWidth : Nat

Default width of the targeted output pane.

Equations

• Std.Format.defWidth = 120

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

Nest with the default indentation 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

instance Std.Format.instMonadPrettyFormatStateMState : MonadPrettyFormat (StateM Std.Format.State✝)

Equations

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

@[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 = (f.prettyM width indent { column := column }).snd.out

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

Class for converting a given type α to a Format object for pretty-printing. See also Repr, which also outputs a Format object.

• format : α → Format

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

Intersperse the given list (each item printed with format) with the given sep 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

Format each item in items and prepend prefix pre.

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

Format each item in items and append suffix.

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