Documentation

Init.Data.Format.Basic

inductive Std.Format.FlattenBehavior :

allOrNone: Std.Format.FlattenBehavior
fill: Std.Format.FlattenBehavior

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]
```

Instances For

instance Std.Format.instInhabitedFlattenBehavior :

Inhabited Std.Format.FlattenBehavior

Equations

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

instance Std.Format.instBEqFlattenBehavior :

BEq Std.Format.FlattenBehavior

Equations

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

inductive Std.Format :

The empty format.
nil: Lean.Format
A position where a newline may be inserted if the current group does not fit within the allotted column width.
line: Lean.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.
align: Bool → Lean.Format
A node containing a plain string.
text: String → Lean.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.
nest: Int → Lean.Format → Lean.Format
Concatenation of two Formats.
append: Lean.Format → Lean.Format → Lean.Format
Creates a new flattening group for the given inner format.
group: Lean.Format → optParam Std.Format.FlattenBehavior Std.Format.FlattenBehavior.allOrNone → Lean.Format
Used for associating auxiliary information (e.g. Exprs) with Format objects.
tag: Nat → Lean.Format → Lean.Format

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.

Instances For

instance Std.instInhabitedFormat :

Inhabited Lean.Format

Equations

Std.instInhabitedFormat = { default := Lean.Format.nil }

def Std.Format.isEmpty :

Lean.Format → Bool

Check whether the given format contains no characters.

Equations

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

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

Alias for a group with FlattenBehavior set to fill.

Equations

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

instance Std.Format.instAppendFormat :

Append Lean.Format

Equations

Std.Format.instAppendFormat = { append := Std.Format.append }

instance Std.Format.instCoeStringFormat :

Coe String Lean.Format

Equations

Std.Format.instCoeStringFormat = { coe := Std.Format.text }

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

Equations

Lean.Format.join xs = List.foldl (fun x x_1 => x ++ x_1) (Std.Format.text "") xs

def Std.Format.isNil :

Lean.Format → Bool

Equations

Std.Format.isNil x = match x with | Lean.Format.nil => true | x => false

instance Std.Format.instInhabitedSpaceResult :

Inhabited Std.Format.SpaceResult

Equations

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

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

pushOutput : String → m Unit
pushNewline : Nat → m Unit
currColumn : m Nat
Start a scope tagged with n.
startTag : Nat → m Unit
Exit the scope of n-many opened tags.
endTags : Nat → m Unit

A monad in which we can pretty-print Format objects.

Instances

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

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

Equations

Std.Format.prettyM f w indent = Std.Format.be w [{ flatten := false, flb := Std.Format.FlattenBehavior.allOrNone, items := [{ f := f, indent := Int.ofNat indent, activeTags := 0 }] }]

@[inline]

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

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

Equations

Lean.Format.bracket l f r = Lean.Format.group (Lean.Format.nest (Int.ofNat (String.length l)) (Std.Format.text l ++ f ++ Std.Format.text r))

@[inline]

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

Creates the format "(" ++ f ++ ")" with a flattening group.

Equations

Lean.Format.paren f = Lean.Format.bracket "(" f ")"

@[inline]

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

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

Equations

Lean.Format.sbracket f = Lean.Format.bracket "[" f "]"

@[inline]

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

Same as bracket except uses the fill flattening behaviour.

Equations

Std.Format.bracketFill l f r = Lean.Format.fill (Lean.Format.nest (Int.ofNat (String.length l)) (Std.Format.text l ++ f ++ Std.Format.text r))

def Std.Format.defIndent :

Default indentation.

Equations

Std.Format.defIndent = 2

def Std.Format.defUnicode :

Equations

Std.Format.defUnicode = true

def Std.Format.defWidth :

Default width of the targeted output pane.

Equations

Std.Format.defWidth = 120

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

Nest with the default indentation amount.

Equations

Std.Format.nestD f = Lean.Format.nest (Int.ofNat Std.Format.defIndent) f

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

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

Equations

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

instance Std.Format.instMonadPrettyFormatStateMState :

Std.Format.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 : Lean.Format) (w : optParam Nat Std.Format.defWidth) :

Pretty-print a Format object as a string with expected width w.

Equations

Lean.Format.pretty f w = let act := Std.Format.prettyM f w 0; (act { out := "", column := 0 }).snd.out

class Std.ToFormat (α : Type u) :

format : α → Lean.Format

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

Instances

instance Std.instToFormatFormat :

Lean.ToFormat Lean.Format

Equations

Std.instToFormatFormat = { format := fun f => f }

instance Std.instToFormatString :

Lean.ToFormat String

Equations

Std.instToFormatString = { format := fun s => Std.Format.text s }

def Std.Format.joinSep {α : Type u} [inst : Lean.ToFormat α] :

List α → Lean.Format → Lean.Format

Intersperse the given list (each item printed with format) with the given sep format.

Equations

Lean.Format.joinSep x x = match x, x with | [], x => Lean.Format.nil | [a], x => Std.format a | a :: as, sep => List.foldl (fun x x_1 => x ++ sep ++ Std.format x_1) (Std.format a) as

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

List α → Lean.Format

Format each item in items and prepend prefix pre.

Equations

Std.Format.prefixJoin pre x = match x with | [] => Lean.Format.nil | a :: as => List.foldl (fun x x_1 => x ++ pre ++ Std.format x_1) (pre ++ Std.format a) as

def Std.Format.joinSuffix {α : Type u} [inst : Lean.ToFormat α] :

List α → Lean.Format → Lean.Format

Format each item in items and append suffix.

Equations

Std.Format.joinSuffix x x = match x, x with | [], x => Lean.Format.nil | a :: as, suffix => List.foldl (fun x x_1 => x ++ Std.format x_1 ++ suffix) (Std.format a ++ suffix) as