Documentation

Init.Data.Format.Basic

inductive Std.Format.FlattenBehavior :

Type

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

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 := [anonymous] }

inductive Std.Format :

Type

nil: Lean.Format
line: Lean.Format
text: String → Lean.Format
nest: Int → Lean.Format → Lean.Format
append: Lean.Format → Lean.Format → Lean.Format
group: Lean.Format → optParam Std.Format.FlattenBehavior Std.Format.FlattenBehavior.allOrNone → Lean.Format
tag: Nat → Lean.Format → Lean.Format

instance Std.instInhabitedFormat :

Inhabited Lean.Format

Equations

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

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

Equations

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

def Std.Format.appendEx (a : Lean.Format) (b : Lean.Format) :

Equations

Std.Format.appendEx a b = Std.Format.append a b

def Std.Format.groupEx :

Lean.Format → Lean.Format

Equations

Std.Format.groupEx a = Lean.Format.group a

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 a a_1 => a ++ a_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) :

Type

pushOutput : String → m Unit
pushNewline : Nat → m Unit
currColumn : m Nat
startTag : Nat → m Unit
endTags : Nat → m Unit

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

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

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

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 :

Equations

Std.Format.defIndent = 2

def Std.Format.defUnicode :

Equations

Std.Format.defUnicode = true

def Std.Format.defWidth :

Equations

Std.Format.defWidth = 120

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

Equations

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

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

Equations

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

instance Std.Format.instMonadPrettyFormatStateMState :

Std.Format.MonadPrettyFormat (StateM Std.Format.State)

Equations

Std.Format.instMonadPrettyFormatStateMState = { pushOutput := fun s => modify fun x => match x with | { out := out, column := col } => { out := out ++ s, column := col + String.length s }, pushNewline := fun indent => modify fun x => match x with | { out := out, column := col } => { out := out ++ String.pushn "\n" (Char.ofNat 32) indent, column := indent }, currColumn := do let a ← get pure a.column, startTag := fun n => pure (), endTags := fun n => pure () }

def Std.Format.pretty (f : Lean.Format) (w : optParam Nat Std.Format.defWidth) :

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

Type u

format : α → Lean.Format

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

Equations

Lean.Format.joinSep [] x = Lean.Format.nil
Lean.Format.joinSep [a] x = Lean.format a
Lean.Format.joinSep (a :: as) x = Lean.format a ++ x ++ Lean.Format.joinSep as x

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

List α → Lean.Format

Equations

Std.Format.prefixJoin pre [] = Lean.Format.nil
Std.Format.prefixJoin pre (a :: as) = pre ++ Lean.format a ++ Std.Format.prefixJoin pre as

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

List α → Lean.Format → Lean.Format

Equations

Std.Format.joinSuffix [] x = Lean.Format.nil
Std.Format.joinSuffix (a :: as) x = Lean.format a ++ x ++ Std.Format.joinSuffix as x