instance Lean.IR.instToFormatArg : Lean.ToFormat Lean.IR.Arg

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

Equations

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

instance Lean.IR.instToFormatLitVal : Lean.ToFormat Lean.IR.LitVal

instance Lean.IR.instToFormatCtorInfo : Lean.ToFormat Lean.IR.CtorInfo

Equations

• Lean.IR.instToFormatCtorInfo = { format := Lean.IR.formatCtorInfo✝ }

instance Lean.IR.instToFormatExpr : Lean.ToFormat Lean.IR.Expr

Equations

• Lean.IR.instToFormatExpr = { format := Lean.IR.formatExpr✝ }

instance Lean.IR.instToStringExpr : ToString Lean.IR.Expr

Equations

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

instance Lean.IR.instToFormatIRType : Lean.ToFormat Lean.IR.IRType

Equations

• Lean.IR.instToFormatIRType = { format := Lean.IR.formatIRType✝ }

instance Lean.IR.instToStringIRType : ToString Lean.IR.IRType

Equations

• Lean.IR.instToStringIRType = { toString := toString ∘ Lean.format }

instance Lean.IR.instToFormatParam : Lean.ToFormat Lean.IR.Param

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

Equations

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

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

Equations

• Lean.IR.formatParams ps = Lean.IR.formatArray ps

def Lean.IR.formatFnBodyHead : Lean.IR.FnBody → Lean.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 " ++ Lean.format x_1 ++ Std.Format.text " : " ++ Lean.format ty ++ Std.Format.text " := " ++ Lean.format e
• Lean.IR.formatFnBodyHead (Lean.IR.FnBody.jdecl j xs v b) = Lean.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 " ++ Lean.format x_1 ++ Std.Format.text "[" ++ Lean.format i ++ Std.Format.text "] := " ++ Lean.format y
• Lean.IR.formatFnBodyHead (Lean.IR.FnBody.uset x_1 i y b) = Std.Format.text "uset " ++ Lean.format x_1 ++ Std.Format.text "[" ++ Lean.format i ++ Std.Format.text "] := " ++ Lean.format y
• Lean.IR.formatFnBodyHead (Lean.IR.FnBody.setTag x_1 cidx b) = Std.Format.text "setTag " ++ Lean.format x_1 ++ Std.Format.text " := " ++ Lean.format cidx
• Lean.IR.formatFnBodyHead (Lean.IR.FnBody.del x_1 b) = Std.Format.text "del " ++ Lean.format x_1
• Lean.IR.formatFnBodyHead (Lean.IR.FnBody.mdata d b) = Std.Format.text "mdata " ++ Lean.format d
• Lean.IR.formatFnBodyHead (Lean.IR.FnBody.case tid x_1 xType cs) = Std.Format.text "case " ++ Lean.format x_1 ++ Std.Format.text " of ..."
• Lean.IR.formatFnBodyHead (Lean.IR.FnBody.jmp j ys) = Std.Format.text "jmp " ++ Lean.format j ++ Lean.IR.formatArray ys
• Lean.IR.formatFnBodyHead (Lean.IR.FnBody.ret x_1) = Std.Format.text "ret " ++ Lean.format x_1
• Lean.IR.formatFnBodyHead Lean.IR.FnBody.unreachable = Std.Format.text "⊥"

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

partial def Lean.IR.formatFnBody.loop (indent : Nat := 2) : Lean.IR.FnBody → Lean.Format

instance Lean.IR.instToFormatFnBody : Lean.ToFormat Lean.IR.FnBody

instance Lean.IR.instToStringFnBody : ToString Lean.IR.FnBody

def Lean.IR.formatDecl (decl : Lean.IR.Decl) (indent : Nat := 2) : Lean.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 " ++ Lean.format f ++ Lean.IR.formatParams xs ++ Lean.format " : " ++ Lean.format ty

instance Lean.IR.instToFormatDecl : Lean.ToFormat Lean.IR.Decl

Equations

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

@[export lean_ir_decl_to_string]

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

instance Lean.IR.instToStringDecl : ToString Lean.IR.Decl

Equations

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