Documentation

Lean.Compiler.IR.CompilerM

inductive Lean.IR.LogEntry :

Type

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

def Lean.IR.LogEntry.fmt :

Lean.IR.LogEntry → Lean.Format

Equations

Lean.IR.LogEntry.fmt x = match x with | Lean.IR.LogEntry.step cls decls => Lean.Format.bracket "[" (Lean.format cls) "]" ++ Array.foldl (fun fmt decl => fmt ++ Lean.Format.line ++ Lean.format decl) Lean.Format.nil decls 0 (Array.size decls) | Lean.IR.LogEntry.message msg => msg

instance Lean.IR.LogEntry.instToFormatLogEntry :

Lean.ToFormat Lean.IR.LogEntry

Equations

Lean.IR.LogEntry.instToFormatLogEntry = { format := Lean.IR.LogEntry.fmt }

@[inline]

abbrev Lean.IR.Log :

Type

Equations

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

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

Equations

Lean.IR.Log.format log = Array.foldl (fun fmt entry => Lean.format "" ++ Lean.format fmt ++ Lean.format "" ++ Lean.format Lean.Format.line ++ Lean.format "" ++ Lean.format entry ++ Lean.format "") Lean.Format.nil log 0 (Array.size log)

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

Equations

Lean.IR.Log.toString log = Lean.Format.pretty (Lean.IR.Log.format log)

structure Lean.IR.CompilerState :

Type

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

@[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 => { env := s.env, log := Array.push s.log entry }

def Lean.IR.tracePrefixOptionName :

Equations

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

@[inline]

def Lean.IR.logDecls (cls : Lean.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} [inst : Lean.ToFormat α] (cls : Lean.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} [inst : Lean.ToFormat α] (cls : Lean.Name) (a : α) :

Lean.IR.CompilerM Unit

Equations

Lean.IR.logMessage cls 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 => { env := f s.env, log := s.log }

@[inline]

abbrev Lean.IR.DeclMap :

Type

Equations

Lean.IR.DeclMap = Lean.SMap Lean.Name Lean.IR.Decl

constant Lean.IR.declMapExt :

Lean.SimplePersistentEnvExtension Lean.IR.Decl Lean.IR.DeclMap

def Lean.IR.findEnvDecl (env : Lean.Environment) (n : Lean.Name) :

Option Lean.IR.Decl

Equations

Lean.IR.findEnvDecl env n = Lean.SMap.find? (Lean.SimplePersistentEnvExtension.getState Lean.IR.declMapExt env) n

def Lean.IR.findDecl (n : Lean.Name) :

Lean.IR.CompilerM (Option Lean.IR.Decl)

Equations

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

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

Lean.IR.CompilerM Bool

Equations

Lean.IR.containsDecl n = do let a ← get pure (Lean.SMap.contains (Lean.SimplePersistentEnvExtension.getState Lean.IR.declMapExt a.env) n)

def Lean.IR.getDecl (n : Lean.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 "'")

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 decl

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

List Lean.IR.Decl

Equations

Lean.IR.getDecls env = Lean.SimplePersistentEnvExtension.getEntries Lean.IR.declMapExt 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.PersistentEnvExtension.addEntry Lean.IR.declMapExt env 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 0 (Array.size decls)

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

Option Lean.IR.Decl

Equations

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

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

Lean.IR.CompilerM (Option Lean.IR.Decl)

Equations

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

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

Lean.IR.CompilerM Bool

Equations

Lean.IR.containsDecl' n decls = if Array.any decls (fun decl => Lean.IR.Decl.name decl == n) 0 (Array.size decls) = true then pure true else do let a ← get pure (Lean.SMap.contains (Lean.SimplePersistentEnvExtension.getState Lean.IR.declMapExt a.env) n)

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

Lean.IR.CompilerM Lean.IR.Decl

Equations

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

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

Option Lean.Name

Equations

Lean.IR.getSorryDep env declName = match Lean.SMap.find? (Lean.SimplePersistentEnvExtension.getState Lean.IR.declMapExt env) declName with | some (Lean.IR.Decl.fdecl x x_1 x_2 x_3 { sorryDep? := dep? }) => dep? | x => none