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 : Lake.Name
• type : Lean.Expr
• borrow : Bool

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

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

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

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

• alt: {Code : Type} → Lake.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)

inductive Lean.Compiler.LCNF.LitValue : Type

• natVal: Nat → Lean.Compiler.LCNF.LitValue
• strVal: String → Lean.Compiler.LCNF.LitValue

instance Lean.Compiler.LCNF.instInhabitedLitValue : Inhabited Lean.Compiler.LCNF.LitValue

instance Lean.Compiler.LCNF.instBEqLitValue : BEq Lean.Compiler.LCNF.LitValue

instance Lean.Compiler.LCNF.instHashableLitValue : Hashable Lean.Compiler.LCNF.LitValue

def Lean.Compiler.LCNF.LitValue.toExpr : Lean.Compiler.LCNF.LitValue → Lean.Expr

inductive Lean.Compiler.LCNF.Arg : Type

• erased: Lean.Compiler.LCNF.Arg
• fvar: Lean.FVarId → Lean.Compiler.LCNF.Arg
• type: Lean.Expr → Lean.Compiler.LCNF.Arg

instance Lean.Compiler.LCNF.instInhabitedArg : Inhabited Lean.Compiler.LCNF.Arg

instance Lean.Compiler.LCNF.instBEqArg : BEq Lean.Compiler.LCNF.Arg

instance Lean.Compiler.LCNF.instHashableArg : Hashable Lean.Compiler.LCNF.Arg

def Lean.Compiler.LCNF.Param.toArg (p : Lean.Compiler.LCNF.Param) : Lean.Compiler.LCNF.Arg

def Lean.Compiler.LCNF.Arg.toExpr (arg : Lean.Compiler.LCNF.Arg) : Lean.Expr

@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.Arg.updateTypeImp]

opaque Lean.Compiler.LCNF.Arg.updateType! (arg : Lean.Compiler.LCNF.Arg) (type : Lean.Expr) : Lean.Compiler.LCNF.Arg

@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.Arg.updateFVarImp]

opaque Lean.Compiler.LCNF.Arg.updateFVar! (arg : Lean.Compiler.LCNF.Arg) (fvarId' : Lean.FVarId) : Lean.Compiler.LCNF.Arg

inductive Lean.Compiler.LCNF.LetValue : Type

• value: Lean.Compiler.LCNF.LitValue → Lean.Compiler.LCNF.LetValue
• erased: Lean.Compiler.LCNF.LetValue
• proj: Lake.Name → Nat → Lean.FVarId → Lean.Compiler.LCNF.LetValue
• const: Lake.Name → List Lean.Level → Array Lean.Compiler.LCNF.Arg → Lean.Compiler.LCNF.LetValue
• fvar: Lean.FVarId → Array Lean.Compiler.LCNF.Arg → Lean.Compiler.LCNF.LetValue

instance Lean.Compiler.LCNF.instInhabitedLetValue : Inhabited Lean.Compiler.LCNF.LetValue

instance Lean.Compiler.LCNF.instBEqLetValue : BEq Lean.Compiler.LCNF.LetValue

instance Lean.Compiler.LCNF.instHashableLetValue : Hashable Lean.Compiler.LCNF.LetValue

def Lean.Compiler.LCNF.Arg.toLetValue (arg : Lean.Compiler.LCNF.Arg) : Lean.Compiler.LCNF.LetValue

@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.LetValue.updateProjImp]

opaque Lean.Compiler.LCNF.LetValue.updateProj! (e : Lean.Compiler.LCNF.LetValue) (fvarId' : Lean.FVarId) : Lean.Compiler.LCNF.LetValue

@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.LetValue.updateConstImp]

opaque Lean.Compiler.LCNF.LetValue.updateConst! (e : Lean.Compiler.LCNF.LetValue) (declName' : Lake.Name) (us' : List Lean.Level) (args' : Array Lean.Compiler.LCNF.Arg) : Lean.Compiler.LCNF.LetValue

@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.LetValue.updateFVarImp]

opaque Lean.Compiler.LCNF.LetValue.updateFVar! (e : Lean.Compiler.LCNF.LetValue) (fvarId' : Lean.FVarId) (args' : Array Lean.Compiler.LCNF.Arg) : Lean.Compiler.LCNF.LetValue

@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.LetValue.updateArgsImp]

opaque Lean.Compiler.LCNF.LetValue.updateArgs! (e : Lean.Compiler.LCNF.LetValue) (args' : Array Lean.Compiler.LCNF.Arg) : Lean.Compiler.LCNF.LetValue

def Lean.Compiler.LCNF.LetValue.toExpr (e : Lean.Compiler.LCNF.LetValue) : Lean.Expr

structure Lean.Compiler.LCNF.LetDecl : Type

• fvarId : Lean.FVarId
• binderName : Lake.Name
• type : Lean.Expr
• value : Lean.Compiler.LCNF.LetValue

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

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

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

• fvarId : Lean.FVarId
• binderName : Lake.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)

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

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

• typeName : Lake.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)

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.Compiler.LCNF.Arg → 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

@[inline, reducible]

abbrev Lean.Compiler.LCNF.Alt : Type

@[inline, reducible]

abbrev Lean.Compiler.LCNF.FunDecl : Type

@[inline, reducible]

abbrev Lean.Compiler.LCNF.Cases : Type

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

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

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

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

def Lean.Compiler.LCNF.attachCodeDecls (decls : Array Lean.Compiler.LCNF.CodeDecl) (code : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.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.

@[implemented_by _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

@[implemented_by _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

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

def Lean.Compiler.LCNF.AltCore.getParams : Lean.Compiler.LCNF.Alt → Array Lean.Compiler.LCNF.Param

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

@[implemented_by _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

@[implemented_by _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

@[implemented_by _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

@[implemented_by _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

@[implemented_by _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

@[implemented_by _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

@[implemented_by _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

@[implemented_by _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

@[implemented_by _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.Compiler.LCNF.Arg) : Lean.Compiler.LCNF.Code

@[implemented_by _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

@[implemented_by _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.

@[implemented_by _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.Compiler.LCNF.LetValue) : 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.

@[implemented_by _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 : Lake.Name) : Lean.Compiler.LCNF.Alt × Lean.Compiler.LCNF.Cases

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

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

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

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

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

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

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

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} [Monad m] (c : Lean.Compiler.LCNF.Code) (f : Lean.Compiler.LCNF.Code → m Unit) : m Unit

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

structure Lean.Compiler.LCNF.Decl : Type

• name : Lake.Name

  The name of the declaration from the Environment it came from

• levelParams : List Lake.Name

  Universe level parameter names.

• type : Lean.Expr

  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.

• params : Array Lean.Compiler.LCNF.Param

  Parameters.

• value : Lean.Compiler.LCNF.Code

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

• recursive : Bool

  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.

• safe : 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.

• inlineAttr? : Option Lean.Compiler.InlineAttributeKind

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

Declaration being processed by the Lean to Lean compiler passes.

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

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

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

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

def Lean.Compiler.LCNF.Decl.inlineAttr (decl : Lean.Compiler.LCNF.Decl) : Bool

def Lean.Compiler.LCNF.Decl.noinlineAttr (decl : Lean.Compiler.LCNF.Decl) : Bool

def Lean.Compiler.LCNF.Decl.inlineIfReduceAttr (decl : Lean.Compiler.LCNF.Decl) : Bool

def Lean.Compiler.LCNF.Decl.alwaysInlineAttr (decl : Lean.Compiler.LCNF.Decl) : Bool

def Lean.Compiler.LCNF.Decl.inlineable (decl : Lean.Compiler.LCNF.Decl) : Bool

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

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

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

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

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

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

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

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

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.instArg (decl : Lean.Compiler.LCNF.Decl) (us : List Lean.Level) (arg : Lean.Compiler.LCNF.Arg) : Lean.Compiler.LCNF.Arg

def Lean.Compiler.LCNF.Decl.instantiateValueLevelParams.instLetValue (decl : Lean.Compiler.LCNF.Decl) (us : List Lean.Level) (e : Lean.Compiler.LCNF.LetValue) : Lean.Compiler.LCNF.LetValue

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

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

def Lean.Compiler.LCNF.hasLocalInst (type : Lean.Expr) : Bool

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

Equations

• Lean.Compiler.LCNF.hasLocalInst (Lean.Expr.forallE binderName binderType b bi) = (Lean.BinderInfo.isInstImplicit bi || Lean.Compiler.LCNF.hasLocalInst b)
• Lean.Compiler.LCNF.hasLocalInst type = false

def Lean.Compiler.LCNF.Decl.isTemplateLike (decl : Lean.Compiler.LCNF.Decl) : Lean.CoreM Bool

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

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, reducible]

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

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.

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

def Lean.Compiler.LCNF.instantiateRangeArgs (e : Lean.Expr) (beginIdx : Nat) (endIdx : Nat) (args : Array Lean.Compiler.LCNF.Arg) : Lean.Expr

def Lean.Compiler.LCNF.instantiateRevRangeArgs (e : Lean.Expr) (beginIdx : Nat) (endIdx : Nat) (args : Array Lean.Compiler.LCNF.Arg) : Lean.Expr