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: Std.Format
line: Std.Format
text: String → Std.Format
nest: Int → Std.Format → Std.Format
append: Std.Format → Std.Format → Std.Format
group: Std.Format → optParam Std.Format.FlattenBehavior Std.Format.FlattenBehavior.allOrNone → Std.Format
tag: Nat → Std.Format → Std.Format

instance Std.instInhabitedFormat :

Inhabited Std.Format

Equations

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

def Std.Format.isEmpty :

Std.Format → Bool

Equations

Std.Format.isEmpty Std.Format.nil = true
Std.Format.isEmpty Std.Format.line = false
Std.Format.isEmpty (Std.Format.text msg) = (msg == "")
Std.Format.isEmpty (Std.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 (Std.Format.group f behavior) = Std.Format.isEmpty f
Std.Format.isEmpty (Std.Format.tag a f) = Std.Format.isEmpty f

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

Equations

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

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

Equations

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

def Std.Format.groupEx :

Std.Format → Std.Format

Equations

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

instance Std.Format.instAppendFormat :

Append Std.Format

Equations

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

instance Std.Format.instCoeStringFormat :

Coe String Std.Format

Equations

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

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

Equations

Std.Format.join xs = List.foldl (fun a a_1 => a ++ a_1) (Std.Format.text "") xs

def Std.Format.isNil :

Std.Format → Bool

Equations

Std.Format.isNil _fun_discr = match _fun_discr with | Std.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

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

Instances

Std.Format.instMonadPrettyFormatStateMState

def Std.Format.prettyM {m : Type → Type} (f : Std.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 : Std.Format) (r : String) :

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

Std.Format.bracketFill l f r = Std.Format.fill (Std.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 : Std.Format) :

Equations

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

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

Equations

Std.Format.indentD f = Std.Format.nestD (Std.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 := column } => { out := out ++ String.pushn "\n" (Char.ofNat 32) indent, column := indent }, currColumn := do let a ← get pure a.column, startTag := fun x => pure (), endTags := fun x => pure () }

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

Equations

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

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

class Std.ToFormat (α : Type u) :

Type u

format : α → Std.Format

Instances

instance Std.instToFormatFormat :

Std.ToFormat Std.Format

Equations

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

instance Std.instToFormatString :

Std.ToFormat String

Equations

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

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

List α → Std.Format → Std.Format

Equations

Std.Format.joinSep [] _fun_discr = Std.Format.nil
Std.Format.joinSep [a] _fun_discr = Std.format a
Std.Format.joinSep (a :: as) _fun_discr = Std.format a ++ _fun_discr ++ Std.Format.joinSep as _fun_discr

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

List α → Std.Format

Equations

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

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

List α → Std.Format → Std.Format

Equations

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