# Documentation

Lean.Compiler.LCNF.Basic

# Lean Compiler Normal Form (LCNF) #

It is based on the A-normal form, and the approach described in the paper Compiling without continuations.

Instances For
Equations
Equations
Equations
• alt: {Code : Type} → Lean.NameCode
• default: {Code : Type} → Code
Instances For
instance Lean.Compiler.LCNF.instInhabitedAltCore :
{a : Type} → [inst : ] →
Equations
• natVal:
• strVal:
Instances For
Equations
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
Equations
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.Arg.updateTypeImp]
@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.Arg.updateFVarImp]
Instances For
Equations
Equations
• One or more equations did not get rendered due to their size.
@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.LetValue.updateProjImp]
@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.LetValue.updateConstImp]
@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.LetValue.updateFVarImp]
@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.LetValue.updateArgsImp]
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
Equations
Instances For
instance Lean.Compiler.LCNF.instInhabitedFunDeclCore :
{a : Type} → [inst : ] →
Equations
• Lean.Compiler.LCNF.instInhabitedFunDeclCore = { default := { fvarId := default, binderName := default, params := default, type := default, value := default } }
Equations
Instances For
Equations
• Lean.Compiler.LCNF.instInhabitedCasesCore = { default := { typeName := default, resultType := default, discr := default, alts := default } }
@[inline]
Equations
@[inline]
Equations
@[inline]
Equations

Return the constructor names that have an explicit (non-default) alternative.

Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.eqImp]
Equations
@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.eqFunDecl]
Equations
Equations
Equations
def Lean.Compiler.LCNF.AltCore.forCodeM {m : TypeType u_1} [inst : ] (alt : Lean.Compiler.LCNF.Alt) (f : ) :
Equations
@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateAltCodeImp]
@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateAltImp]
@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateAltsImp]
@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateCasesImp]
@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateLetImp]
@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateContImp]
@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateFunImp]
@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateReturnImp]
@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateJmpImp]
@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateUnreachImp]
@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateParamCoreImp]

Low-level update Param function. It does not update the local context. Consider using Param.update : Param → Expr → CompilerM Param→ Expr → CompilerM Param→ CompilerM Param if you want the local context to be updated.

@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateLetDeclCoreImp]

Low-level update LetDecl function. It does not update the local context. Consider using LetDecl.update : LetDecl → Expr → Expr → CompilerM LetDecl→ Expr → Expr → CompilerM LetDecl→ Expr → CompilerM LetDecl→ CompilerM LetDecl if you want the local context to be updated.

@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateFunDeclCoreImp]

Low-level update FunDecl function. It does not update the local context. Consider using FunDecl.update : LetDecl → Expr → Array Param → Code → CompilerM FunDecl→ Expr → Array Param → Code → CompilerM FunDecl→ Array Param → Code → CompilerM FunDecl→ Code → CompilerM FunDecl→ CompilerM FunDecl if you want the local context to be updated.

Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• = match x with | => true | x => false
Equations
• = match x, x with | , fvarId' => fvarId == fvarId' | x, x_1 => false
Equations

Return true iff c.size ≤ n≤ n

Equations
• = match with | => true | => false
Equations
• = do modify fun x => x + 1 let __do_lift ← get if __do_lift n then else
def Lean.Compiler.LCNF.Code.forM {m : TypeType u_1} [inst : ] (f : ) :
Equations
partial def Lean.Compiler.LCNF.Code.forM.go {m : TypeType u_1} [inst : ] (f : ) :
• The name of the declaration from the Environment it came from

name : Lean.Name
• Universe level parameter names.

levelParams :
• The type of the declaration. Note that this is an erased LCNF type instead of the fully dependent one that might have been the original type of the declaration in the Environment.

type : Lean.Expr
• Parameters.

params :
• The body of the declaration, usually changes as it progresses through compiler passes.

• We set this flag to true during LCNF conversion. When we receive a block of functions to be compiled, we set this flag to true if there is an application to the function in the block containing it. This is an approximation, but it should be good enough because in the frontend, we invoke the compiler with blocks of strongly connected components only. We use this information to control inlining.

recursive : Bool
• We set this flag to false during LCNF conversion if the Lean function associated with this function was tagged as partial or unsafe. This information affects how static analyzers treat function applications of this kind. See DefinitionSafety. partial and unsafe functions may not be terminating, but Lean functions terminate, and some static analyzers exploit this fact. So, we use the following semantics. Suppose whe hav a (large) natural number C. We consider a nondeterministic model for computation of Lean expressions as follows: Each call to a partial/unsafe function uses up one "recursion token". Prior to consuming C recursion tokens all partial functions must be called as normal. Once the model has used up C recursion tokens, a subsequent call to a partial function has the following nondeterministic options: it can either call the function again, or return any value of the target type (even a noncomputable one). Larger values of C yield less nondeterminism in the model, but even the intersection of all choices of C yields nondeterminism where def loop : A := loop returns any value of type A. The compiler fixes a choice for C. This is a fixed constant greater than 2^2^64, which is allowed to be compiler and architecture dependent, and promises that it will produce an execution consistent with every possible nondeterministic outcome of the C-model. In the event that different nondeterministic executions disagree, the compiler is required to exhaust resources or output a looping computation.

safe : Bool
• We store the inline attribute at LCNF declarations to make sure we can set them for auxliary declarations created during compilation.

inlineAttr? :

Declaration being processed by the Lean to Lean compiler passes.

Instances For
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
Equations
• = match decl.inlineAttr? with | => true | x => false
Equations
• = match decl.inlineAttr? with | => true | x => false
Equations
• = match decl.inlineAttr? with | => true | x => false
Equations
• = match decl.inlineAttr? with | => true | x => false

Return true if the given declaration has been annotated with [inline], [inline_if_reduce], [macro_inline], or [always_inline]

Equations
• = match decl.inlineAttr? with | some Lean.Compiler.InlineAttributeKind.noinline => false | some val => true | none => false

Return some i if decl is of the form

def f (a_0 ... a_i ...) :=
...
cases a_i
| ...
| ...


That is, f is a sequence of declarations followed by a cases on the parameter i. We use this function to decide whether we should inline a declaration tagged with [inline_if_reduce] or not.

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

Return true if the arrow type contains an instance implicit argument.

Equations

Return true if decl is supposed to be inlined/specialized.

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

Traverse the given block of potentially mutually recursive functions and mark a declaration f as recursive if there is an application f ... in the block. This is an overapproximation, and relies on the fact that our frontend computes strongly connected components. See comment at recursive field.

Equations
• One or more equations did not get rendered due to their size.
Equations
def Lean.Compiler.LCNF.instantiateRangeArgs (e : Lean.Expr) (beginIdx : Nat) (endIdx : Nat) (args : ) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.Compiler.LCNF.instantiateRevRangeArgs (e : Lean.Expr) (beginIdx : Nat) (endIdx : Nat) (args : ) :
Equations
• One or more equations did not get rendered due to their size.