source
instance Lean.IR.instToFormatArg :
ToFormat Arg
Equations

- Lean.IR.instToFormatArg = { format := Lean.IR.instToFormatArg._private_1 }

source
def Lean.IR.formatArray {α : Type} [ToFormat α] (args : Array α) :
Format
Equations

- Lean.IR.formatArray args = Array.foldl (fun (r : Std.Format) (a : α) => r ++ Std.Format.text " " ++ Std.format a) Std.Format.nil args

Instances For

source
instance Lean.IR.instToFormatLitVal :
ToFormat LitVal
Equations

- Lean.IR.instToFormatLitVal = { format := Lean.IR.instToFormatLitVal._private_1 }

source
instance Lean.IR.instToFormatCtorInfo :
ToFormat CtorInfo
Equations

- Lean.IR.instToFormatCtorInfo = { format := Lean.IR.instToFormatCtorInfo._private_1 }

source
instance Lean.IR.instToFormatExpr :
ToFormat Expr
Equations

- Lean.IR.instToFormatExpr = { format := Lean.IR.instToFormatExpr._private_1 }

source
instance Lean.IR.instToStringExpr :
ToString Expr
Equations

- Lean.IR.instToStringExpr = { toString := fun (e : Lean.IR.Expr) => (Std.format e).pretty }

source
instance Lean.IR.instToFormatIRType :
ToFormat IRType
Equations

- Lean.IR.instToFormatIRType = { format := Lean.IR.instToFormatIRType._private_1 }

source
instance Lean.IR.instToStringIRType :
ToString IRType
Equations

- Lean.IR.instToStringIRType = { toString := toString ∘ Std.format }

source
instance Lean.IR.instToFormatParam :
ToFormat Param
Equations

- Lean.IR.instToFormatParam = { format := Lean.IR.instToFormatParam._private_1 }

source
def Lean.IR.formatAlt (fmt : FnBody → Format) (indent : Nat) :
Alt → Format
Equations

- Lean.IR.formatAlt fmt indent (Lean.IR.Alt.ctor i b) = Std.format i.name ++ Std.Format.text " →" ++ Std.Format.nest (↑indent) (Std.Format.line ++ fmt b)
- Lean.IR.formatAlt fmt indent (Lean.IR.Alt.default b) = Std.Format.text "default →" ++ Std.Format.nest (↑indent) (Std.Format.line ++ fmt b)

Instances For

source
def Lean.IR.formatParams (ps : Array Param) :
Format
Equations

- Lean.IR.formatParams ps = Lean.IR.formatArray ps

Instances For

source
def Lean.IR.formatFnBodyHead :
FnBody → Format
Equations

- One or more equations did not get rendered due to their size.
- Lean.IR.formatFnBodyHead (Lean.IR.FnBody.vdecl x_1 ty e b) = Std.Format.text "let " ++ Std.format x_1 ++ Std.Format.text " : " ++ Std.format ty ++ Std.Format.text " := " ++ Std.format e
- Lean.IR.formatFnBodyHead (Lean.IR.FnBody.jdecl j xs v b) = Std.format j ++ Lean.IR.formatParams xs ++ Std.Format.text " := ..."
- Lean.IR.formatFnBodyHead (Lean.IR.FnBody.set x_1 i y b) = Std.Format.text "set " ++ Std.format x_1 ++ Std.Format.text "[" ++ Std.format i ++ Std.Format.text "] := " ++ Std.format y
- Lean.IR.formatFnBodyHead (Lean.IR.FnBody.uset x_1 i y b) = Std.Format.text "uset " ++ Std.format x_1 ++ Std.Format.text "[" ++ Std.format i ++ Std.Format.text "] := " ++ Std.format y
- Lean.IR.formatFnBodyHead (Lean.IR.FnBody.setTag x_1 cidx b) = Std.Format.text "setTag " ++ Std.format x_1 ++ Std.Format.text " := " ++ Std.format cidx
- Lean.IR.formatFnBodyHead (Lean.IR.FnBody.del x_1 b) = Std.Format.text "del " ++ Std.format x_1
- Lean.IR.formatFnBodyHead (Lean.IR.FnBody.case tid x_1 xType cs) = Std.Format.text "case " ++ Std.format x_1 ++ Std.Format.text " of ..."
- Lean.IR.formatFnBodyHead (Lean.IR.FnBody.jmp j ys) = Std.Format.text "jmp " ++ Std.format j ++ Lean.IR.formatArray ys
- Lean.IR.formatFnBodyHead (Lean.IR.FnBody.ret x_1) = Std.Format.text "ret " ++ Std.format x_1
- Lean.IR.formatFnBodyHead Lean.IR.FnBody.unreachable = Std.Format.text "⊥"

Instances For

source
def Lean.IR.formatFnBody (fnBody : FnBody) (indent : Nat := 2) :
Format
Equations

- Lean.IR.formatFnBody fnBody indent = Lean.IR.formatFnBody.loop✝ indent fnBody

Instances For

source
instance Lean.IR.instToFormatFnBody :
ToFormat FnBody
Equations

- Lean.IR.instToFormatFnBody = { format := fun (fnBody : Lean.IR.FnBody) => Lean.IR.formatFnBody fnBody }

source
instance Lean.IR.instToStringFnBody :
ToString FnBody
Equations

- Lean.IR.instToStringFnBody = { toString := fun (b : Lean.IR.FnBody) => (Std.format b).pretty }

source
def Lean.IR.formatDecl (decl : Decl) (indent : Nat := 2) :
Format
Equations

- One or more equations did not get rendered due to their size.
- Lean.IR.formatDecl (Lean.IR.Decl.extern f xs ty ext) indent = Std.Format.text "extern " ++ Std.format f ++ Lean.IR.formatParams xs ++ Std.format " : " ++ Std.format ty

Instances For

source
instance Lean.IR.instToFormatDecl :
ToFormat Decl
Equations

- Lean.IR.instToFormatDecl = { format := fun (decl : Lean.IR.Decl) => Lean.IR.formatDecl decl }

source
def Lean.IR.declToString (d : Decl) :
String
Equations

- Lean.IR.declToString d = (Std.format d).pretty

Instances For

source
instance Lean.IR.instToStringDecl :
ToString Decl
Equations

- Lean.IR.instToStringDecl = { toString := Lean.IR.declToString }