inductive Lean.IR.LogEntry : Type

• step (cls : Name) (decls : Array Decl) : LogEntry
• message (msg : Format) : LogEntry

def Lean.IR.LogEntry.fmt : LogEntry → Format

Equations

• One or more equations did not get rendered due to their size.
• (Lean.IR.LogEntry.message msg).fmt = msg

instance Lean.IR.LogEntry.instToFormat : ToFormat LogEntry

Equations

• Lean.IR.LogEntry.instToFormat = { format := Lean.IR.LogEntry.fmt }

@[reducible, inline]

abbrev Lean.IR.Log : Type

Equations

• Lean.IR.Log = Array Lean.IR.LogEntry

def Lean.IR.Log.format (log : Log) : Format

Equations

• One or more equations did not get rendered due to their size.

def Lean.IR.Log.toString (log : Log) : String

Equations

• log.toString = log.format.pretty

@[reducible, inline]

abbrev Lean.IR.CompilerM (α : Type) : Type

Equations

• Lean.IR.CompilerM = Lean.CoreM

def Lean.IR.log (entry : LogEntry) : CompilerM Unit

Equations

• Lean.IR.log entry = Lean.addTrace `Compiler.IR (Lean.toMessageData "" ++ Lean.toMessageData entry ++ Lean.toMessageData "")

def Lean.IR.tracePrefixOptionName : Name

Equations

• Lean.IR.tracePrefixOptionName = `trace.compiler.ir

@[inline]

def Lean.IR.logDecls (cls : Name) (decl : Array Decl) : CompilerM Unit

Equations

• Lean.IR.logDecls cls decl = Lean.IR.logDeclsAux✝ (Lean.IR.tracePrefixOptionName ++ cls) cls decl

@[inline]

def Lean.IR.logMessageIf {α : Type} [ToFormat α] (cls : Name) (a : α) : CompilerM Unit

Equations

• Lean.IR.logMessageIf cls a = Lean.IR.logMessageIfAux✝ (Lean.IR.tracePrefixOptionName ++ cls) a

@[inline]

def Lean.IR.logMessage {α : Type} [ToFormat α] (a : α) : CompilerM Unit

Equations

• Lean.IR.logMessage a = Lean.IR.logMessageIfAux✝ Lean.IR.tracePrefixOptionName a

@[reducible, inline]

abbrev Lean.IR.DeclMap : Type

Equations

• Lean.IR.DeclMap = Lean.PHashMap Lean.Name Lean.IR.Decl

def Lean.IR.isDeclMeta (env : Environment) (declName : Name) : Bool

Whether a declaration should be exported for interpretation.

Equations

• Lean.IR.isDeclMeta env (n.str "_boxed") = if (!env.header.isModule) = true then true else have inferFor := n; (Lean.IR.declMetaExt✝.getState env).snd.contains inferFor
• Lean.IR.isDeclMeta env declName = if (!env.header.isModule) = true then true else have inferFor := declName; (Lean.IR.declMetaExt✝.getState env).snd.contains inferFor

def Lean.IR.setDeclMeta (env : Environment) (declName : Name) : Environment

Marks a declaration to be exported for interpretation.

Equations

• One or more equations did not get rendered due to their size.

opaque Lean.IR.declMapExt : SimplePersistentEnvExtension Decl DeclMap

@[export lean_ir_find_env_decl]

def Lean.IR.findEnvDecl (env : Environment) (declName : Name) : Option Decl

Equations

• One or more equations did not get rendered due to their size.

def Lean.IR.findDecl (n : Name) : CompilerM (Option Decl)

Equations

• Lean.IR.findDecl n = do let __do_lift ← Lean.getEnv pure (Lean.IR.findEnvDecl __do_lift n)

def Lean.IR.containsDecl (n : Name) : CompilerM Bool

Equations

• Lean.IR.containsDecl n = do let __do_lift ← Lean.IR.findDecl n pure __do_lift.isSome

def Lean.IR.getDecl (n : Name) : CompilerM Decl

Equations

• One or more equations did not get rendered due to their size.

def Lean.IR.findLocalDecl (n : Name) : CompilerM (Option Decl)

Equations

• Lean.IR.findLocalDecl n = do let __do_lift ← Lean.getEnv pure (Lean.PersistentHashMap.find? (Lean.IR.declMapExt.getState __do_lift) n)

def Lean.IR.getDecls (env : Environment) : List Decl

Returns the list of IR declarations in declaration order.

Equations

• Lean.IR.getDecls env = Lean.IR.declMapExt.getEntries env

def Lean.IR.addDecl (decl : Decl) : CompilerM Unit

Equations

• Lean.IR.addDecl decl = Lean.modifyEnv fun (x : Lean.Environment) => Lean.PersistentEnvExtension.addEntry Lean.IR.declMapExt x decl

def Lean.IR.addDecls (decls : Array Decl) : CompilerM Unit

Equations

• Lean.IR.addDecls decls = Array.forM Lean.IR.addDecl decls

def Lean.IR.findEnvDecl' (env : Environment) (n : Name) (decls : Array Decl) : Option Decl

Equations

• Lean.IR.findEnvDecl' env n decls = match Array.find? (fun (decl : Lean.IR.Decl) => decl.name == n) decls with | some decl => some decl | none => Lean.IR.findEnvDecl env n

def Lean.IR.findDecl' (n : Name) (decls : Array Decl) : CompilerM (Option Decl)

Equations

• Lean.IR.findDecl' n decls = do let __do_lift ← Lean.getEnv pure (Lean.IR.findEnvDecl' __do_lift n decls)

def Lean.IR.containsDecl' (n : Name) (decls : Array Decl) : CompilerM Bool

Equations

• Lean.IR.containsDecl' n decls = if (decls.any fun (decl : Lean.IR.Decl) => decl.name == n) = true then pure true else Lean.IR.containsDecl n

def Lean.IR.getDecl' (n : Name) (decls : Array Decl) : CompilerM Decl

Equations

• One or more equations did not get rendered due to their size.

@[export lean_decl_get_sorry_dep]

def Lean.IR.getSorryDep (env : Environment) (declName : Name) : Option Name

Equations

• Lean.IR.getSorryDep env declName = match Lean.IR.findEnvDecl env declName with | some (Lean.IR.Decl.fdecl f xs type body { sorryDep? := dep? }) => dep? | x => none