source
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.line`s as possible:

      [1, 2,
       3]

- allOrNone : FlattenBehavior

  Either all `Format.line`s in the group will be newlines, or all of them will be spaces.

- fill : FlattenBehavior

  As few `Format.line`s in the group as possible will be newlines.

Instances For

source
instance Std.Format.instInhabitedFlattenBehavior :
Inhabited FlattenBehavior
Equations

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

source
def Std.Format.instInhabitedFlattenBehavior.default :
FlattenBehavior
Equations

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

Instances For

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

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

Instances For

source
instance Std.Format.instBEqFlattenBehavior :
BEq FlattenBehavior
Equations

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

source
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 `Format`s.

- 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. `Expr`s) with `Format` objects.

Instances For

source
instance Std.instInhabitedFormat :
Inhabited Format
Equations

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

source
def Std.instInhabitedFormat.default :
Format
Equations

- Std.instInhabitedFormat.default = Std.Format.nil

Instances For

source
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

Instances For

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

Creates a group in which as few `Format.line`s 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

Instances For

source
instance Std.Format.instAppend :
Append Format
Equations

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

source
instance Std.Format.instCoeString :
Coe String Format
Equations

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

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

Concatenates a list of `Format`s with `++`.

Equations

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

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

source
instance Std.Format.instBEqFlattenAllowability :
BEq FlattenAllowability
Equations

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

source
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

Instances For

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

Instances

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

Instances For

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

Instances For

source
@[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 ")"

Instances For

source
@[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 "]"

Instances For

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

Instances For

source
def Std.Format.defIndent :
Nat

The default indentation level, which is two spaces.

Equations

- Std.Format.defIndent = 2

Instances For

source
def Std.Format.defUnicode :
Bool
Equations

- Std.Format.defUnicode = true

Instances For

source
def Std.Format.defWidth :
Nat

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

Equations

- Std.Format.defWidth = 120

Instances For

source
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

Instances For

source
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

Instances For

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

Instances For

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

Instances

source
instance Std.instToFormatFormat :
ToFormat Format
Equations

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

source
instance Std.instToFormatString :
ToFormat String
Equations

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

source
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

Instances For

source
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

Instances For

source
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

Instances For