Helper functions for creating auxiliary names used in (old) compiler passes.

@[export lean_mk_eager_lambda_lifting_name]

def Lean.Compiler.mkEagerLambdaLiftingName (n : Lake.Name) (idx : Nat) : Lake.Name

Equations

• Lean.Compiler.mkEagerLambdaLiftingName n idx = Lean.Name.mkStr n ("_elambda_" ++ toString idx)

@[export lean_is_eager_lambda_lifting_name]

def Lean.Compiler.isEagerLambdaLiftingName : Lake.Name → Bool

Equations

• Lean.Compiler.isEagerLambdaLiftingName (Lean.Name.str p s) = (String.isPrefixOf "_elambda" s || Lean.Compiler.isEagerLambdaLiftingName p)
• Lean.Compiler.isEagerLambdaLiftingName (Lean.Name.num p i) = Lean.Compiler.isEagerLambdaLiftingName p
• Lean.Compiler.isEagerLambdaLiftingName x = false

def Lean.Compiler.getDeclNamesForCodeGen : Lean.Declaration → List Lake.Name

Return the name of new definitions in the a given declaration. Here we consider only declarations we generate code for. We use this definition to implement add_and_compile.

Equations

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

def Lean.Compiler.checkIsDefinition (env : Lean.Environment) (n : Lake.Name) : Except String Unit

Equations

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

@[export lean_mk_unsafe_rec_name]

def Lean.Compiler.mkUnsafeRecName (declName : Lake.Name) : Lake.Name

We generate auxiliary unsafe definitions for regular recursive definitions. The auxiliary unsafe definition has a clear runtime cost execution model. This function returns the auxiliary unsafe definition name for the given name.

Equations

• Lean.Compiler.mkUnsafeRecName declName = Lean.Name.mkStr declName "_unsafe_rec"

@[export lean_is_unsafe_rec_name]

def Lean.Compiler.isUnsafeRecName? : Lake.Name → Option Lake.Name

Return some _ if the given name was created using mkUnsafeRecName

Equations

• Lean.Compiler.isUnsafeRecName? x = match x with | Lean.Name.str n "_unsafe_rec" => some n | x => none

@[extern lean_compile_decls]

opaque Lean.Environment.compileDecls (env : Lean.Environment) (opt : Lean.Options) (decls : List Lake.Name) : Except Lean.KernelException Lean.Environment

Compile the given block of mutual declarations. Assumes the declarations have already been added to the environment using addDecl.

def Lean.Environment.compileDecl (env : Lean.Environment) (opt : Lean.Options) (decl : Lean.Declaration) : Except Lean.KernelException Lean.Environment

Compile the given declaration, it assumes the declaration has already been added to the environment using addDecl.

Equations

• Lean.Environment.compileDecl env opt decl = Lean.Environment.compileDecls env opt (Lean.Compiler.getDeclNamesForCodeGen decl)

def Lean.Environment.addAndCompile (env : Lean.Environment) (opt : Lean.Options) (decl : Lean.Declaration) : Except Lean.KernelException Lean.Environment

Equations

• Lean.Environment.addAndCompile env opt decl = do let env ← Lean.Environment.addDecl env decl Lean.Environment.compileDecl env opt decl