Documentation

Lean.Compiler.IR.Format

instance Lean.IR.instToFormatArg :

Lean.ToFormat Lean.IR.Arg

Equations

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

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

Equations

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

instance Lean.IR.instToFormatLitVal :

Lean.ToFormat Lean.IR.LitVal

Equations

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

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.Format.pretty (Lean.format e) }

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

Equations

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

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

Lean.IR.Alt → Lean.Format

Equations

Lean.IR.formatAlt fmt indent x = match x with | Lean.IR.AltCore.ctor i b => Lean.format i.name ++ Std.Format.text " →" ++ Lean.Format.nest (Int.ofNat indent) (Lean.Format.line ++ fmt b) | Lean.IR.AltCore.default b => Std.Format.text "default →" ++ Lean.Format.nest (Int.ofNat indent) (Lean.Format.line ++ fmt b)

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

Equations

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

def Lean.IR.formatFnBodyHead :

Lean.IR.FnBody → Lean.Format

Equations

Lean.IR.formatFnBodyHead x = match x with | Lean.IR.FnBody.vdecl x ty e b => Std.Format.text "let " ++ Lean.format x ++ Std.Format.text " : " ++ Lean.format ty ++ Std.Format.text " := " ++ Lean.format e | Lean.IR.FnBody.jdecl j xs v b => Lean.format j ++ Lean.IR.formatParams xs ++ Std.Format.text " := ..." | Lean.IR.FnBody.set x i y b => Std.Format.text "set " ++ Lean.format x ++ Std.Format.text "[" ++ Lean.format i ++ Std.Format.text "] := " ++ Lean.format y | Lean.IR.FnBody.uset x i y b => Std.Format.text "uset " ++ Lean.format x ++ Std.Format.text "[" ++ Lean.format i ++ Std.Format.text "] := " ++ Lean.format y | Lean.IR.FnBody.sset x i o y ty b => Std.Format.text "sset " ++ Lean.format x ++ Std.Format.text "[" ++ Lean.format i ++ Std.Format.text ", " ++ Lean.format o ++ Std.Format.text "] : " ++ Lean.format ty ++ Std.Format.text " := " ++ Lean.format y | Lean.IR.FnBody.setTag x cidx b => Std.Format.text "setTag " ++ Lean.format x ++ Std.Format.text " := " ++ Lean.format cidx | Lean.IR.FnBody.inc x n c x_1 b => (Std.Format.text "inc" ++ if (n != 1) = true then Lean.Format.sbracket (Lean.format n) else Std.Format.text "") ++ Std.Format.text " " ++ Lean.format x | Lean.IR.FnBody.dec x n c x_1 b => (Std.Format.text "dec" ++ if (n != 1) = true then Lean.Format.sbracket (Lean.format n) else Std.Format.text "") ++ Std.Format.text " " ++ Lean.format x | Lean.IR.FnBody.del x b => Std.Format.text "del " ++ Lean.format x | Lean.IR.FnBody.mdata d b => Std.Format.text "mdata " ++ Lean.format d | Lean.IR.FnBody.case tid x xType cs => Std.Format.text "case " ++ Lean.format x ++ Std.Format.text " of ..." | Lean.IR.FnBody.jmp j ys => Std.Format.text "jmp " ++ Lean.format j ++ Lean.IR.formatArray ys | Lean.IR.FnBody.ret x => Std.Format.text "ret " ++ Lean.format x | Lean.IR.FnBody.unreachable => Std.Format.text "⊥"

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

Equations

Lean.IR.formatFnBody fnBody indent = (fun loop => loop fnBody) (Lean.IR.formatFnBody.loop indent)

partial def Lean.IR.formatFnBody.loop (indent : optParam Nat 2) :

Lean.IR.FnBody → Lean.Format

instance Lean.IR.instToFormatFnBody :

Lean.ToFormat Lean.IR.FnBody

Equations

Lean.IR.instToFormatFnBody = { format := fun fnBody => Lean.IR.formatFnBody fnBody }

instance Lean.IR.instToStringFnBody :

ToString Lean.IR.FnBody

Equations

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

def Lean.IR.formatDecl (decl : Lean.IR.Decl) (indent : optParam Nat 2) :

Equations

Lean.IR.formatDecl decl indent = match decl with | Lean.IR.Decl.fdecl f xs ty b x => Std.Format.text "def " ++ Lean.format f ++ Lean.IR.formatParams xs ++ Lean.format " : " ++ Lean.format ty ++ Std.Format.text " :=" ++ Lean.Format.nest (Int.ofNat indent) (Lean.Format.line ++ Lean.IR.formatFnBody b indent) | Lean.IR.Decl.extern f xs ty x => 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.formatDecl decl }

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

Equations

Lean.IR.declToString d = Lean.Format.pretty (Lean.format d)

instance Lean.IR.instToStringDecl :

ToString Lean.IR.Decl

Equations

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