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

Equations

• Lean.IR.instToFormatArg = { format := Lean.IR.formatArg✝ }

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

Equations

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

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

Equations

• Lean.IR.instToFormatLitVal = { format := Lean.IR.formatLitVal✝ }

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

Equations

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

instance Lean.IR.instToFormatExpr : Std.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) => (Std.format e).pretty }

instance Lean.IR.instToFormatIRType : Std.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 ∘ Std.format }

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

Equations

• Lean.IR.instToFormatParam = { format := Lean.IR.formatParam✝ }

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

Equations

• Lean.IR.formatAlt fmt indent (Lean.IR.AltCore.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.AltCore.default b) = Std.Format.text "default →" ++ Std.Format.nest (↑indent) (Std.Format.line ++ fmt b)

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

Equations

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

def Lean.IR.formatFnBodyHead : Lean.IR.FnBody → Std.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.mdata d b) = Std.Format.text "mdata " ++ Std.format d
• 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 "⊥"

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

Equations

• Lean.IR.formatFnBody fnBody indent = Lean.IR.formatFnBody.loop indent fnBody

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

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

Equations

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

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

Equations

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

def Lean.IR.formatDecl (decl : Lean.IR.Decl) (indent : Nat := 2) : Std.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

instance Lean.IR.instToFormatDecl : Std.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

Equations

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

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

Equations

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