inductive Lean.IR.LogEntry : Type

• step: Lake.Name → Array Lean.IR.Decl → Lean.IR.LogEntry
• message: Lean.Format → Lean.IR.LogEntry

Instances For

• Lean.IR.LogEntry.instToFormat

def Lean.IR.LogEntry.fmt : Lean.IR.LogEntry → Lean.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 : Lean.ToFormat Lean.IR.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 : Lean.IR.Log) : Lean.Format

Equations

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

@[export lean_ir_log_to_string]

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

Equations

• log.toString = log.format.pretty

structure Lean.IR.CompilerState : Type

• env : Lean.Environment
• log : Lean.IR.Log

@[reducible, inline]

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

Equations

• Lean.IR.CompilerM = ReaderT Lean.Options (EStateM String Lean.IR.CompilerState)

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

Equations

• Lean.IR.log entry = modify fun (s : Lean.IR.CompilerState) => { env := s.env, log := Array.push s.log entry }

def Lean.IR.tracePrefixOptionName : Lake.Name

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

def Lean.IR.modifyEnv (f : Lean.Environment → Lean.Environment) : Lean.IR.CompilerM Unit

Equations

• Lean.IR.modifyEnv f = modify fun (s : Lean.IR.CompilerState) => { env := f s.env, log := s.log }

@[reducible, inline]

abbrev Lean.IR.DeclMap : Type

Equations

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

opaque Lean.IR.declMapExt : Lean.SimplePersistentEnvExtension Lean.IR.Decl Lean.IR.DeclMap

@[export lean_ir_find_env_decl]

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.IR.getDecl n = do let __discr ← Lean.IR.findDecl n match __discr with | some decl => pure decl | x => throw (toString "unknown declaration '" ++ toString n ++ toString "'")

@[export lean_ir_add_decl]

def Lean.IR.addDeclAux (env : Lean.Environment) (decl : Lean.IR.Decl) : Lean.Environment

Equations

• Lean.IR.addDeclAux env decl = Lean.PersistentEnvExtension.addEntry Lean.IR.declMapExt (env.addExtraName decl.name) decl

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

Equations

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

def Lean.IR.getEnv : Lean.IR.CompilerM Lean.Environment

Equations

• Lean.IR.getEnv = do let s ← get pure s.env

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.IR.containsDecl' (n : Lake.Name) (decls : Array Lean.IR.Decl) : Lean.IR.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 : Lake.Name) (decls : Array Lean.IR.Decl) : Lean.IR.CompilerM Lean.IR.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 : Lean.Environment) (declName : Lake.Name) : Option Lake.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