Lean Compiler Normal Form (LCNF)

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

structure Lean.Compiler.LCNF.Param : Type

• fvarId : Lean.FVarId
• binderName : Lean.Name
• type : Lean.Expr
• borrow : Bool

instance Lean.Compiler.LCNF.instInhabitedParam : Inhabited Lean.Compiler.LCNF.Param

Equations

• Lean.Compiler.LCNF.instInhabitedParam = { default := { fvarId := default, binderName := default, type := default, borrow := default } }

instance Lean.Compiler.LCNF.instBEqParam : BEq Lean.Compiler.LCNF.Param

Equations

• Lean.Compiler.LCNF.instBEqParam = { beq := Lean.Compiler.LCNF.beqParam✝ }

def Lean.Compiler.LCNF.Param.toExpr (p : Lean.Compiler.LCNF.Param) : Lean.Expr

Equations

• Lean.Compiler.LCNF.Param.toExpr p = Lean.Expr.fvar p.fvarId

inductive Lean.Compiler.LCNF.AltCore (Code : Type) : Type

• alt: {Code : Type} → Lean.Name → Array Lean.Compiler.LCNF.Param → Code → Lean.Compiler.LCNF.AltCore Code
• default: {Code : Type} → Code → Lean.Compiler.LCNF.AltCore Code

instance Lean.Compiler.LCNF.instInhabitedAltCore : {a : Type} → [inst : Inhabited a] → Inhabited (Lean.Compiler.LCNF.AltCore a)

Equations

• Lean.Compiler.LCNF.instInhabitedAltCore = { default := Lean.Compiler.LCNF.AltCore.alt default default default }

structure Lean.Compiler.LCNF.LetDecl : Type

• fvarId : Lean.FVarId
• binderName : Lean.Name
• type : Lean.Expr
• value : Lean.Expr

instance Lean.Compiler.LCNF.instInhabitedLetDecl : Inhabited Lean.Compiler.LCNF.LetDecl

Equations

• Lean.Compiler.LCNF.instInhabitedLetDecl = { default := { fvarId := default, binderName := default, type := default, value := default } }

instance Lean.Compiler.LCNF.instBEqLetDecl : BEq Lean.Compiler.LCNF.LetDecl

Equations

• Lean.Compiler.LCNF.instBEqLetDecl = { beq := Lean.Compiler.LCNF.beqLetDecl✝ }

structure Lean.Compiler.LCNF.FunDeclCore (Code : Type) : Type

• fvarId : Lean.FVarId
• binderName : Lean.Name
• params : Array Lean.Compiler.LCNF.Param
• type : Lean.Expr
• value : Code

instance Lean.Compiler.LCNF.instInhabitedFunDeclCore : {a : Type} → [inst : Inhabited a] → Inhabited (Lean.Compiler.LCNF.FunDeclCore a)

Equations

• Lean.Compiler.LCNF.instInhabitedFunDeclCore = { default := { fvarId := default, binderName := default, params := default, type := default, value := default } }

def Lean.Compiler.LCNF.FunDeclCore.getArity {Code : Type} (decl : Lean.Compiler.LCNF.FunDeclCore Code) : Nat

Equations

• Lean.Compiler.LCNF.FunDeclCore.getArity decl = Array.size decl.params

structure Lean.Compiler.LCNF.CasesCore (Code : Type) : Type

• typeName : Lean.Name
• resultType : Lean.Expr
• discr : Lean.FVarId
• alts : Array (Lean.Compiler.LCNF.AltCore Code)

instance Lean.Compiler.LCNF.instInhabitedCasesCore : {a : Type} → Inhabited (Lean.Compiler.LCNF.CasesCore a)

Equations

• Lean.Compiler.LCNF.instInhabitedCasesCore = { default := { typeName := default, resultType := default, discr := default, alts := default } }

inductive Lean.Compiler.LCNF.Code : Type

• let: Lean.Compiler.LCNF.LetDecl → Lean.Compiler.LCNF.Code → Lean.Compiler.LCNF.Code
• fun: Lean.Compiler.LCNF.FunDeclCore Lean.Compiler.LCNF.Code → Lean.Compiler.LCNF.Code → Lean.Compiler.LCNF.Code
• jp: Lean.Compiler.LCNF.FunDeclCore Lean.Compiler.LCNF.Code → Lean.Compiler.LCNF.Code → Lean.Compiler.LCNF.Code
• jmp: Lean.FVarId → Array Lean.Expr → Lean.Compiler.LCNF.Code
• cases: Lean.Compiler.LCNF.CasesCore Lean.Compiler.LCNF.Code → Lean.Compiler.LCNF.Code
• return: Lean.FVarId → Lean.Compiler.LCNF.Code
• unreach: Lean.Expr → Lean.Compiler.LCNF.Code

instance Lean.Compiler.LCNF.instInhabitedCode : Inhabited Lean.Compiler.LCNF.Code

Equations

• Lean.Compiler.LCNF.instInhabitedCode = { default := Lean.Compiler.LCNF.Code.jmp default default }

@[inline]

abbrev Lean.Compiler.LCNF.Alt : Type

Equations

• Lean.Compiler.LCNF.Alt = Lean.Compiler.LCNF.AltCore Lean.Compiler.LCNF.Code

@[inline]

abbrev Lean.Compiler.LCNF.FunDecl : Type

Equations

• Lean.Compiler.LCNF.FunDecl = Lean.Compiler.LCNF.FunDeclCore Lean.Compiler.LCNF.Code

@[inline]

abbrev Lean.Compiler.LCNF.Cases : Type

Equations

• Lean.Compiler.LCNF.Cases = Lean.Compiler.LCNF.CasesCore Lean.Compiler.LCNF.Code

def Lean.Compiler.LCNF.CasesCore.getCtorNames (c : Lean.Compiler.LCNF.Cases) : Lean.NameSet

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

Equations

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

inductive Lean.Compiler.LCNF.CodeDecl : Type

• let: Lean.Compiler.LCNF.LetDecl → Lean.Compiler.LCNF.CodeDecl
• fun: Lean.Compiler.LCNF.FunDecl → Lean.Compiler.LCNF.CodeDecl
• jp: Lean.Compiler.LCNF.FunDecl → Lean.Compiler.LCNF.CodeDecl

instance Lean.Compiler.LCNF.instInhabitedCodeDecl : Inhabited Lean.Compiler.LCNF.CodeDecl

Equations

• Lean.Compiler.LCNF.instInhabitedCodeDecl = { default := Lean.Compiler.LCNF.CodeDecl.let default }

def Lean.Compiler.LCNF.CodeDecl.fvarId : Lean.Compiler.LCNF.CodeDecl → Lean.FVarId

Equations

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

def Lean.Compiler.LCNF.attachCodeDecls (decls : Array Lean.Compiler.LCNF.CodeDecl) (code : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.Code

Equations

• Lean.Compiler.LCNF.attachCodeDecls decls code = Lean.Compiler.LCNF.attachCodeDecls.go decls (Array.size decls) code

def Lean.Compiler.LCNF.attachCodeDecls.go (decls : Array Lean.Compiler.LCNF.CodeDecl) (i : Nat) (code : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.Code

Equations

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

@[implementedBy _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.eqImp]

opaque Lean.Compiler.LCNF.Code.beq : Lean.Compiler.LCNF.Code → Lean.Compiler.LCNF.Code → Bool

instance Lean.Compiler.LCNF.instBEqCode : BEq Lean.Compiler.LCNF.Code

Equations

• Lean.Compiler.LCNF.instBEqCode = { beq := Lean.Compiler.LCNF.Code.beq }

@[implementedBy _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.eqFunDecl]

opaque Lean.Compiler.LCNF.FunDecl.beq : Lean.Compiler.LCNF.FunDecl → Lean.Compiler.LCNF.FunDecl → Bool

instance Lean.Compiler.LCNF.instBEqFunDecl : BEq Lean.Compiler.LCNF.FunDecl

Equations

• Lean.Compiler.LCNF.instBEqFunDecl = { beq := Lean.Compiler.LCNF.FunDecl.beq }

def Lean.Compiler.LCNF.AltCore.getCode : Lean.Compiler.LCNF.Alt → Lean.Compiler.LCNF.Code

Equations

• Lean.Compiler.LCNF.AltCore.getCode _fun_discr = match _fun_discr with | Lean.Compiler.LCNF.AltCore.default k => k | Lean.Compiler.LCNF.AltCore.alt ctorName params k => k

def Lean.Compiler.LCNF.AltCore.forCodeM {m : Type → Type u_1} [inst : Monad m] (alt : Lean.Compiler.LCNF.Alt) (f : Lean.Compiler.LCNF.Code → m Unit) : m Unit

Equations

• Lean.Compiler.LCNF.AltCore.forCodeM alt f = match alt with | Lean.Compiler.LCNF.AltCore.default k => f k | Lean.Compiler.LCNF.AltCore.alt ctorName params k => f k

@[implementedBy _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateAltCodeImp]

opaque Lean.Compiler.LCNF.AltCore.updateCode (alt : Lean.Compiler.LCNF.Alt) (c : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.Alt

@[implementedBy _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateAltImp]

opaque Lean.Compiler.LCNF.AltCore.updateAlt! (alt : Lean.Compiler.LCNF.Alt) (ps' : Array Lean.Compiler.LCNF.Param) (k' : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.Alt

@[implementedBy _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateAltsImp]

opaque Lean.Compiler.LCNF.Code.updateAlts! (c : Lean.Compiler.LCNF.Code) (alts : Array Lean.Compiler.LCNF.Alt) : Lean.Compiler.LCNF.Code

@[implementedBy _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateCasesImp]

opaque Lean.Compiler.LCNF.Code.updateCases! (c : Lean.Compiler.LCNF.Code) (resultType : Lean.Expr) (discr : Lean.FVarId) (alts : Array Lean.Compiler.LCNF.Alt) : Lean.Compiler.LCNF.Code

@[implementedBy _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateLetImp]

opaque Lean.Compiler.LCNF.Code.updateLet! (c : Lean.Compiler.LCNF.Code) (decl' : Lean.Compiler.LCNF.LetDecl) (k' : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.Code

@[implementedBy _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateContImp]

opaque Lean.Compiler.LCNF.Code.updateCont! (c : Lean.Compiler.LCNF.Code) (k' : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.Code

@[implementedBy _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateFunImp]

opaque Lean.Compiler.LCNF.Code.updateFun! (c : Lean.Compiler.LCNF.Code) (decl' : Lean.Compiler.LCNF.FunDecl) (k' : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.Code

@[implementedBy _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateReturnImp]

opaque Lean.Compiler.LCNF.Code.updateReturn! (c : Lean.Compiler.LCNF.Code) (fvarId' : Lean.FVarId) : Lean.Compiler.LCNF.Code

@[implementedBy _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateJmpImp]

opaque Lean.Compiler.LCNF.Code.updateJmp! (c : Lean.Compiler.LCNF.Code) (fvarId' : Lean.FVarId) (args' : Array Lean.Expr) : Lean.Compiler.LCNF.Code

@[implementedBy _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateUnreachImp]

opaque Lean.Compiler.LCNF.Code.updateUnreach! (c : Lean.Compiler.LCNF.Code) (type' : Lean.Expr) : Lean.Compiler.LCNF.Code

@[implementedBy _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateParamCoreImp]

opaque Lean.Compiler.LCNF.Param.updateCore (p : Lean.Compiler.LCNF.Param) (type : Lean.Expr) : Lean.Compiler.LCNF.Param

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

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

opaque Lean.Compiler.LCNF.LetDecl.updateCore (decl : Lean.Compiler.LCNF.LetDecl) (type : Lean.Expr) (value : Lean.Expr) : Lean.Compiler.LCNF.LetDecl

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

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

opaque Lean.Compiler.LCNF.FunDeclCore.updateCore (decl : Lean.Compiler.LCNF.FunDecl) (type : Lean.Expr) (params : Array Lean.Compiler.LCNF.Param) (value : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.FunDecl

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

def Lean.Compiler.LCNF.CasesCore.extractAlt! (cases : Lean.Compiler.LCNF.Cases) (ctorName : Lean.Name) : Lean.Compiler.LCNF.Alt × Lean.Compiler.LCNF.Cases

Equations

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

def Lean.Compiler.LCNF.AltCore.mapCodeM {m : Type → Type u_1} [inst : Monad m] (alt : Lean.Compiler.LCNF.Alt) (f : Lean.Compiler.LCNF.Code → m Lean.Compiler.LCNF.Code) : m Lean.Compiler.LCNF.Alt

Equations

• Lean.Compiler.LCNF.AltCore.mapCodeM alt f = do let a ← f (Lean.Compiler.LCNF.AltCore.getCode alt) pure (Lean.Compiler.LCNF.AltCore.updateCode alt a)

def Lean.Compiler.LCNF.Code.isDecl : Lean.Compiler.LCNF.Code → Bool

Equations

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

def Lean.Compiler.LCNF.Code.isFun : Lean.Compiler.LCNF.Code → Bool

Equations

• Lean.Compiler.LCNF.Code.isFun _fun_discr = match _fun_discr with | Lean.Compiler.LCNF.Code.fun decl k => true | x => false

def Lean.Compiler.LCNF.Code.isReturnOf : Lean.Compiler.LCNF.Code → Lean.FVarId → Bool

Equations

• Lean.Compiler.LCNF.Code.isReturnOf _fun_discr _fun_discr = match _fun_discr, _fun_discr with | Lean.Compiler.LCNF.Code.return fvarId, fvarId' => fvarId == fvarId' | x, x_1 => false

def Lean.Compiler.LCNF.Code.size (c : Lean.Compiler.LCNF.Code) : Nat

Equations

• Lean.Compiler.LCNF.Code.size c = Lean.Compiler.LCNF.Code.size.go c 0

partial def Lean.Compiler.LCNF.Code.size.go (c : Lean.Compiler.LCNF.Code) (n : Nat) : Nat

def Lean.Compiler.LCNF.Code.sizeLe (c : Lean.Compiler.LCNF.Code) (n : Nat) : Bool

Return true iff c.size ≤ n

Equations

• Lean.Compiler.LCNF.Code.sizeLe c n = match EStateM.run (Lean.Compiler.LCNF.Code.sizeLe.go n c) 0 with | EStateM.Result.ok a a_1 => true | EStateM.Result.error a a_1 => false

def Lean.Compiler.LCNF.Code.sizeLe.inc (n : Nat) : EStateM Unit Nat Unit

Equations

• Lean.Compiler.LCNF.Code.sizeLe.inc n = do modify fun a => a + 1 let a ← get if a ≤ n then pure PUnit.unit else throw ()

partial def Lean.Compiler.LCNF.Code.sizeLe.go (n : Nat) (c : Lean.Compiler.LCNF.Code) : EStateM Unit Nat Unit

def Lean.Compiler.LCNF.Code.forM {m : Type → Type u_1} [inst : Monad m] (c : Lean.Compiler.LCNF.Code) (f : Lean.Compiler.LCNF.Code → m Unit) : m Unit

Equations

• Lean.Compiler.LCNF.Code.forM c f = Lean.Compiler.LCNF.Code.forM.go f c

partial def Lean.Compiler.LCNF.Code.forM.go {m : Type → Type u_1} [inst : Monad m] (f : Lean.Compiler.LCNF.Code → m Unit) (c : Lean.Compiler.LCNF.Code) : m Unit

structure Lean.Compiler.LCNF.Decl : Type

• The name of the declaration from the Environment it came from

  name : Lean.Name

• Universe level parameter names.

  levelParams : List Lean.Name

• 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 : Array Lean.Compiler.LCNF.Param

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

  value : Lean.Compiler.LCNF.Code

• 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

Declaration being processed by the Lean to Lean compiler passes.

instance Lean.Compiler.LCNF.instInhabitedDecl : Inhabited Lean.Compiler.LCNF.Decl

Equations

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

instance Lean.Compiler.LCNF.instBEqDecl : BEq Lean.Compiler.LCNF.Decl

Equations

• Lean.Compiler.LCNF.instBEqDecl = { beq := Lean.Compiler.LCNF.beqDecl✝ }

def Lean.Compiler.LCNF.Decl.size (decl : Lean.Compiler.LCNF.Decl) : Nat

Equations

• Lean.Compiler.LCNF.Decl.size decl = Lean.Compiler.LCNF.Code.size decl.value

def Lean.Compiler.LCNF.Decl.getArity (decl : Lean.Compiler.LCNF.Decl) : Nat

Equations

• Lean.Compiler.LCNF.Decl.getArity decl = Array.size decl.params

def Lean.Compiler.LCNF.Decl.isCasesOnParam? (decl : Lean.Compiler.LCNF.Decl) : Option Nat

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 [inlineIfReduce] or not.

Equations

• Lean.Compiler.LCNF.Decl.isCasesOnParam? decl = Lean.Compiler.LCNF.Decl.isCasesOnParam?.go decl decl.value

def Lean.Compiler.LCNF.Decl.isCasesOnParam?.go (decl : Lean.Compiler.LCNF.Decl) (code : Lean.Compiler.LCNF.Code) : Option Nat

Equations

• Lean.Compiler.LCNF.Decl.isCasesOnParam?.go decl (Lean.Compiler.LCNF.Code.let decl_1 k) = Lean.Compiler.LCNF.Decl.isCasesOnParam?.go decl k
• Lean.Compiler.LCNF.Decl.isCasesOnParam?.go decl (Lean.Compiler.LCNF.Code.jp decl_1 k) = Lean.Compiler.LCNF.Decl.isCasesOnParam?.go decl k
• Lean.Compiler.LCNF.Decl.isCasesOnParam?.go decl (Lean.Compiler.LCNF.Code.fun decl_1 k) = Lean.Compiler.LCNF.Decl.isCasesOnParam?.go decl k
• Lean.Compiler.LCNF.Decl.isCasesOnParam?.go decl (Lean.Compiler.LCNF.Code.cases c) = Array.findIdx? decl.params fun param => param.fvarId == c.discr
• Lean.Compiler.LCNF.Decl.isCasesOnParam?.go decl code = none

def Lean.Compiler.LCNF.Decl.instantiateTypeLevelParams (decl : Lean.Compiler.LCNF.Decl) (us : List Lean.Level) : Lean.Expr

Equations

• Lean.Compiler.LCNF.Decl.instantiateTypeLevelParams decl us = Lean.Expr.instantiateLevelParams decl.type decl.levelParams us

def Lean.Compiler.LCNF.Decl.instantiateParamsLevelParams (decl : Lean.Compiler.LCNF.Decl) (us : List Lean.Level) : Array Lean.Compiler.LCNF.Param

Equations

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

def Lean.Compiler.LCNF.Decl.instantiateValueLevelParams (decl : Lean.Compiler.LCNF.Decl) (us : List Lean.Level) : Lean.Compiler.LCNF.Code

Equations

• Lean.Compiler.LCNF.Decl.instantiateValueLevelParams decl us = Lean.Compiler.LCNF.Decl.instantiateValueLevelParams.instCode decl us decl.value

def Lean.Compiler.LCNF.Decl.instantiateValueLevelParams.instExpr (decl : Lean.Compiler.LCNF.Decl) (us : List Lean.Level) (e : Lean.Expr) : Lean.Expr

Equations

• Lean.Compiler.LCNF.Decl.instantiateValueLevelParams.instExpr decl us e = Lean.Expr.instantiateLevelParams e decl.levelParams us

def Lean.Compiler.LCNF.Decl.instantiateValueLevelParams.instParams (decl : Lean.Compiler.LCNF.Decl) (us : List Lean.Level) (ps : Array Lean.Compiler.LCNF.Param) : Array Lean.Compiler.LCNF.Param

Equations

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

partial def Lean.Compiler.LCNF.Decl.instantiateValueLevelParams.instAlt (decl : Lean.Compiler.LCNF.Decl) (us : List Lean.Level) (alt : Lean.Compiler.LCNF.Alt) : Lean.Compiler.LCNF.AltCore Lean.Compiler.LCNF.Code

def Lean.Compiler.LCNF.Decl.instantiateValueLevelParams.instLetDecl (decl : Lean.Compiler.LCNF.Decl) (us : List Lean.Level) (decl : Lean.Compiler.LCNF.LetDecl) : Lean.Compiler.LCNF.LetDecl

Equations

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

partial def Lean.Compiler.LCNF.Decl.instantiateValueLevelParams.instFunDecl (decl : Lean.Compiler.LCNF.Decl) (us : List Lean.Level) (decl : Lean.Compiler.LCNF.FunDecl) : Lean.Compiler.LCNF.FunDecl

partial def Lean.Compiler.LCNF.Decl.instantiateValueLevelParams.instCode (decl : Lean.Compiler.LCNF.Decl) (us : List Lean.Level) (code : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.Code

partial def Lean.Compiler.LCNF.FunDeclCore.collectUsed (decl : Lean.Compiler.LCNF.FunDecl) (s : optParam Lean.FVarIdSet ∅) : Lean.FVarIdSet

partial def Lean.Compiler.LCNF.Code.collectUsed (code : Lean.Compiler.LCNF.Code) (s : optParam Lean.FVarIdSet ∅) : Lean.FVarIdSet

@[inline]

abbrev Lean.Compiler.LCNF.collectUsedAtExpr (s : Lean.FVarIdSet) (e : Lean.Expr) : Lean.FVarIdSet

Equations

• Lean.Compiler.LCNF.collectUsedAtExpr s e = Lean.Compiler.LCNF.collectExpr e s

def Lean.Compiler.LCNF.markRecDecls (decls : Array Lean.Compiler.LCNF.Decl) : Array Lean.Compiler.LCNF.Decl

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.

partial def Lean.Compiler.LCNF.markRecDecls.visit (decls : Array Lean.Compiler.LCNF.Decl) (code : Lean.Compiler.LCNF.Code) : StateM Lean.NameSet Unit

def Lean.Compiler.LCNF.markRecDecls.go (decls : Array Lean.Compiler.LCNF.Decl) : StateM Lean.NameSet Unit

Equations

• Lean.Compiler.LCNF.markRecDecls.go decls = Array.forM (fun decl => Lean.Compiler.LCNF.markRecDecls.visit decls decl.value) decls 0 (Array.size decls)