Documentation

Lean.Compiler.IR

constant Lean.IR.compiler.reuse :

Lean.Option Bool

def Lean.IR.compile (env : Lean.Environment) (opts : Lean.Options) (decls : Array Lean.IR.Decl) :

Lean.IR.Log × Except String Lean.Environment

Equations

Lean.IR.compile env opts decls = match EStateM.run (Lean.IR.compileAux decls opts) { env := env, log := #[] } with | EStateM.Result.ok x s => (s.log, Except.ok s.env) | EStateM.Result.error msg s => (s.log, Except.error msg)

def Lean.IR.addBoxedVersionAux (decl : Lean.IR.Decl) :

Lean.IR.CompilerM Unit

Equations

Lean.IR.addBoxedVersionAux decl = do let env ← Lean.IR.getEnv if (!Lean.IR.ExplicitBoxing.requiresBoxedVersion env decl) = true then pure () else let decl := Lean.IR.ExplicitBoxing.mkBoxedVersion decl; let decls := #[decl]; do let decls ← Lean.IR.explicitRC decls Array.forM (fun decl => Lean.IR.modifyEnv fun env => Lean.IR.addDeclAux env decl) decls 0 (Array.size decls) pure ()

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

Except String Lean.Environment

Equations

Lean.IR.addBoxedVersion env decl = match EStateM.run (Lean.IR.addBoxedVersionAux decl Lean.Options.empty) { env := env, log := #[] } with | EStateM.Result.ok x s => Except.ok s.env | EStateM.Result.error msg s => Except.error msg