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

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

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

Instances For

source
def Lean.Compiler.isEagerLambdaLiftingName :
Name → Bool
Equations

- Lean.Compiler.isEagerLambdaLiftingName (p.str s) = ("_elambda".isPrefixOf s || Lean.Compiler.isEagerLambdaLiftingName p)
- Lean.Compiler.isEagerLambdaLiftingName (p.num i) = Lean.Compiler.isEagerLambdaLiftingName p
- Lean.Compiler.isEagerLambdaLiftingName x✝ = false

Instances For

source
def Lean.Compiler.getDeclNamesForCodeGen :
Declaration → Array 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.
- Lean.Compiler.getDeclNamesForCodeGen (Lean.Declaration.opaqueDecl { name := name, levelParams := levelParams, type := type, value := value, isUnsafe := isUnsafe, all := all }) = #[name]
- Lean.Compiler.getDeclNamesForCodeGen (Lean.Declaration.axiomDecl { name := name, levelParams := levelParams, type := type, isUnsafe := isUnsafe }) = #[name]
- Lean.Compiler.getDeclNamesForCodeGen (Lean.Declaration.mutualDefnDecl defs) = Array.map (fun (x : Lean.DefinitionVal) => x.name) defs.toArray
- Lean.Compiler.getDeclNamesForCodeGen x✝ = #[]

Instances For

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

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

Instances For

source
def Lean.Compiler.mkUnsafeRecName (declName : Name) :
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 = declName.mkStr "_unsafe_rec"

Instances For

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

Return `some _` if the given name was created using `mkUnsafeRecName`

Equations

- Lean.Compiler.isUnsafeRecName? (n.str "_unsafe_rec") = some n
- Lean.Compiler.isUnsafeRecName? x✝ = none

Instances For