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

• p.toExpr = 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} [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

Equations

• Lean.Compiler.LCNF.instInhabitedLitValue = { default := Lean.Compiler.LCNF.LitValue.natVal default }

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

Equations

• Lean.Compiler.LCNF.instBEqLitValue = { beq := Lean.Compiler.LCNF.beqLitValue✝ }

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

Equations

• Lean.Compiler.LCNF.instHashableLitValue = { hash := Lean.Compiler.LCNF.hashLitValue✝ }

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

Equations

• (Lean.Compiler.LCNF.LitValue.natVal a).toExpr = Lean.Expr.lit (Lean.Literal.natVal a)
• (Lean.Compiler.LCNF.LitValue.strVal a).toExpr = Lean.Expr.lit (Lean.Literal.strVal a)

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

Equations

• Lean.Compiler.LCNF.instInhabitedArg = { default := Lean.Compiler.LCNF.Arg.erased }

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

Equations

• Lean.Compiler.LCNF.instBEqArg = { beq := Lean.Compiler.LCNF.beqArg✝ }

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

Equations

• p.toArg = Lean.Compiler.LCNF.Arg.fvar p.fvarId

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: Lean.Name → Nat → Lean.FVarId → Lean.Compiler.LCNF.LetValue
• const: Lean.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

Equations

• Lean.Compiler.LCNF.instHashableLetValue = { hash := Lean.Compiler.LCNF.hashLetValue✝ }

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' : Lean.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 : Lean.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 : Lean.Name
• params : Array Lean.Compiler.LCNF.Param
• type : Lean.Expr
• value : Code

instance Lean.Compiler.LCNF.instInhabitedFunDeclCore {a✝ : Type} [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

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✝)

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

Equations

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

@[reducible, inline]

abbrev Lean.Compiler.LCNF.Alt : Type

Equations

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

@[reducible, inline]

abbrev Lean.Compiler.LCNF.FunDecl : Type

Equations

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

@[reducible, 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.

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

Equations

• (Lean.Compiler.LCNF.CodeDecl.let decl).fvarId = decl.fvarId
• (Lean.Compiler.LCNF.CodeDecl.fun decl).fvarId = decl.fvarId
• (Lean.Compiler.LCNF.CodeDecl.jp decl).fvarId = decl.fvarId

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 decls.size code

@[irreducible]

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

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

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.default k).getCode = k
• (Lean.Compiler.LCNF.AltCore.alt ctorName params k).getCode = k

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

Equations

• (Lean.Compiler.LCNF.AltCore.default k).forCodeM f = f k
• (Lean.Compiler.LCNF.AltCore.alt ctorName params k).forCodeM f = f k

@[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 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 : 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} [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 __do_lift ← f (Lean.Compiler.LCNF.AltCore.getCode alt) pure (Lean.Compiler.LCNF.AltCore.updateCode alt __do_lift)

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

Equations

• (Lean.Compiler.LCNF.Code.let decl k).isDecl = true
• (Lean.Compiler.LCNF.Code.fun decl k).isDecl = true
• (Lean.Compiler.LCNF.Code.jp decl k).isDecl = true
• x.isDecl = false

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

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

Equations

• (Lean.Compiler.LCNF.Code.return fvarId).isReturnOf x = (fvarId == x)
• x✝.isReturnOf x = false

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

Equations

• c.size = 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

• c.sizeLe n = match (Lean.Compiler.LCNF.Code.sizeLe.go n c).run 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 (x : Nat) => x + 1 let __do_lift ← get if __do_lift ≤ 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} [Monad m] (c : Lean.Compiler.LCNF.Code) (f : Lean.Compiler.LCNF.Code → m Unit) : m Unit

Equations

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

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

Declaration being processed by the Lean to Lean compiler passes.

• name : Lean.Name

  The name of the declaration from the Environment it came from

• levelParams : List Lean.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 we have 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 auxiliary declarations created during compilation.

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

• decl.size = decl.value.size

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

Equations

• decl.noinlineAttr = match decl.inlineAttr? with | some Lean.Compiler.InlineAttributeKind.noinline => true | x => false

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]

Equations

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

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.

Equations

• decl.isCasesOnParam? = 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? (fun (param : Lean.Compiler.LCNF.Param) => param.fvarId == c.discr) decl.params
• 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

Equations

• decl.instantiateParamsLevelParams us = decl.params.mapMono fun (param : Lean.Compiler.LCNF.Param) => param.updateCore (param.type.instantiateLevelParamsNoCache decl.levelParams us)

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

Equations

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

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

Equations

• Lean.Compiler.LCNF.Decl.instantiateValueLevelParams.instLevel decl us u = u.instantiateParams decl.levelParams us

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

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.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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Compiler.LCNF.Decl.instantiateValueLevelParams.instLetValue decl us (Lean.Compiler.LCNF.LetValue.proj typeName idx struct) = Lean.Compiler.LCNF.LetValue.proj typeName idx struct
• Lean.Compiler.LCNF.Decl.instantiateValueLevelParams.instLetValue decl us (Lean.Compiler.LCNF.LetValue.value value) = Lean.Compiler.LCNF.LetValue.value value
• Lean.Compiler.LCNF.Decl.instantiateValueLevelParams.instLetValue decl us Lean.Compiler.LCNF.LetValue.erased = Lean.Compiler.LCNF.LetValue.erased

def Lean.Compiler.LCNF.Decl.instantiateValueLevelParams.instLetDecl (decl : Lean.Compiler.LCNF.Decl) (us : List Lean.Level) : 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) : 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) = (bi.isInstImplicit || 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.

Equations

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

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

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

@[reducible, inline]

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

Equations

• Lean.Compiler.LCNF.collectUsedAtExpr s e = Lean.Compiler.LCNF.collectType✝ 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

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

Equations

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

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