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 : FVarId
• binderName : Name
• type : Expr
• borrow : Bool

instance Lean.Compiler.LCNF.instInhabitedParam : Inhabited Param

Equations

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

instance Lean.Compiler.LCNF.instBEqParam : BEq Param

Equations

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

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

Equations

• p.toExpr = Lean.Expr.fvar p.fvarId

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

• alt {Code : Type} (ctorName : Name) (params : Array Param) (code : Code) : AltCore Code
• default {Code : Type} (code : Code) : AltCore Code

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

Equations

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

inductive Lean.Compiler.LCNF.LitValue : Type

• natVal (val : Nat) : LitValue
• strVal (val : String) : LitValue

instance Lean.Compiler.LCNF.instInhabitedLitValue : Inhabited LitValue

Equations

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

instance Lean.Compiler.LCNF.instBEqLitValue : BEq LitValue

Equations

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

instance Lean.Compiler.LCNF.instHashableLitValue : Hashable LitValue

Equations

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

def Lean.Compiler.LCNF.LitValue.toExpr : LitValue → 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 : Arg
• fvar (fvarId : FVarId) : Arg
• type (expr : Expr) : Arg

instance Lean.Compiler.LCNF.instInhabitedArg : Inhabited Arg

Equations

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

instance Lean.Compiler.LCNF.instBEqArg : BEq Arg

Equations

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

instance Lean.Compiler.LCNF.instHashableArg : Hashable Arg

Equations

• Lean.Compiler.LCNF.instHashableArg = { hash := Lean.Compiler.LCNF.hashArg✝ }

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

Equations

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

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

Equations

• Lean.Compiler.LCNF.Arg.erased.toExpr = Lean.Compiler.LCNF.erasedExpr
• (Lean.Compiler.LCNF.Arg.fvar a).toExpr = Lean.Expr.fvar a
• (Lean.Compiler.LCNF.Arg.type a).toExpr = a

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

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

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

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

inductive Lean.Compiler.LCNF.LetValue : Type

• value (value : LitValue) : LetValue
• erased : LetValue
• proj (typeName : Name) (idx : Nat) (struct : FVarId) : LetValue
• const (declName : Name) (us : List Level) (args : Array Arg) : LetValue
• fvar (fvarId : FVarId) (args : Array Arg) : LetValue

instance Lean.Compiler.LCNF.instInhabitedLetValue : Inhabited LetValue

Equations

• Lean.Compiler.LCNF.instInhabitedLetValue = { default := Lean.Compiler.LCNF.LetValue.value default }

instance Lean.Compiler.LCNF.instBEqLetValue : BEq LetValue

Equations

• Lean.Compiler.LCNF.instBEqLetValue = { beq := Lean.Compiler.LCNF.beqLetValue✝ }

instance Lean.Compiler.LCNF.instHashableLetValue : Hashable LetValue

Equations

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

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

Equations

• (Lean.Compiler.LCNF.Arg.fvar fvarId).toLetValue = Lean.Compiler.LCNF.LetValue.fvar fvarId #[]
• Lean.Compiler.LCNF.Arg.erased.toLetValue = Lean.Compiler.LCNF.LetValue.erased
• (Lean.Compiler.LCNF.Arg.type expr).toLetValue = Lean.Compiler.LCNF.LetValue.erased

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

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

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

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

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

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

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

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

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

Equations

• (Lean.Compiler.LCNF.LetValue.value (Lean.Compiler.LCNF.LitValue.natVal val)).toExpr = Lean.Expr.lit (Lean.Literal.natVal val)
• (Lean.Compiler.LCNF.LetValue.value (Lean.Compiler.LCNF.LitValue.strVal val)).toExpr = Lean.Expr.lit (Lean.Literal.strVal val)
• Lean.Compiler.LCNF.LetValue.erased.toExpr = Lean.Compiler.LCNF.erasedExpr
• (Lean.Compiler.LCNF.LetValue.proj n i s).toExpr = Lean.Expr.proj n i (Lean.Expr.fvar s)
• (Lean.Compiler.LCNF.LetValue.const n us as).toExpr = Lean.mkAppN (Lean.Expr.const n us) (Array.map Lean.Compiler.LCNF.Arg.toExpr as)
• (Lean.Compiler.LCNF.LetValue.fvar fvarId as).toExpr = Lean.mkAppN (Lean.Expr.fvar fvarId) (Array.map Lean.Compiler.LCNF.Arg.toExpr as)

structure Lean.Compiler.LCNF.LetDecl : Type

• fvarId : FVarId
• binderName : Name
• type : Expr
• value : LetValue

instance Lean.Compiler.LCNF.instInhabitedLetDecl : Inhabited LetDecl

Equations

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

instance Lean.Compiler.LCNF.instBEqLetDecl : BEq LetDecl

Equations

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

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

• fvarId : FVarId
• binderName : Name
• params : Array Param
• type : Expr
• value : Code

instance Lean.Compiler.LCNF.instInhabitedFunDeclCore {a✝ : Type} [Inhabited a✝] : Inhabited (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 : FunDeclCore Code) : Nat

Equations

• decl.getArity = decl.params.size

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

• typeName : Name
• resultType : Expr
• discr : FVarId
• alts : Array (AltCore Code)

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

Equations

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

inductive Lean.Compiler.LCNF.Code : Type

• let (decl : LetDecl) (k : Code) : Code
• fun (decl : FunDeclCore Code) (k : Code) : Code
• jp (decl : FunDeclCore Code) (k : Code) : Code
• jmp (fvarId : FVarId) (args : Array Arg) : Code
• cases (cases : CasesCore Code) : Code
• return (fvarId : FVarId) : Code
• unreach (type : Expr) : Code

instance Lean.Compiler.LCNF.instInhabitedCode : Inhabited 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 : Cases) : 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 (decl : LetDecl) : CodeDecl
• fun (decl : FunDecl) : CodeDecl
• jp (decl : FunDecl) : CodeDecl

instance Lean.Compiler.LCNF.instInhabitedCodeDecl : Inhabited CodeDecl

Equations

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

def Lean.Compiler.LCNF.CodeDecl.fvarId : CodeDecl → 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 CodeDecl) (code : Code) : 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 CodeDecl) (i : Nat) (code : Code) : 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 : Code → Code → Bool

instance Lean.Compiler.LCNF.instBEqCode : BEq Code

Equations

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

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

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

instance Lean.Compiler.LCNF.instBEqFunDecl : BEq FunDecl

Equations

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

def Lean.Compiler.LCNF.AltCore.getCode : Alt → 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 : Alt → Array Param

Equations

• (Lean.Compiler.LCNF.AltCore.default k).getParams = #[]
• (Lean.Compiler.LCNF.AltCore.alt ctorName params k).getParams = params

def Lean.Compiler.LCNF.AltCore.forCodeM {m : Type → Type u_1} [Monad m] (alt : Alt) (f : 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 : Alt) (c : Code) : Alt

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

opaque Lean.Compiler.LCNF.Param.updateCore (p : Param) (type : Expr) : 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 : LetDecl) (type : Expr) (value : LetValue) : 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 : FunDecl) (type : Expr) (params : Array Param) (value : Code) : 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 : Cases) (ctorName : Name) : Alt × 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 : Alt) (f : Code → m Code) : m 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 : 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 : Code → Bool

Equations

• (Lean.Compiler.LCNF.Code.fun decl k).isFun = true
• x✝.isFun = false

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

Equations

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

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

Equations

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

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

def Lean.Compiler.LCNF.Code.sizeLe (c : 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 : Code) : EStateM Unit Nat Unit

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

def Lean.Compiler.LCNF.Code.instantiateValueLevelParams (code : Code) (levelParams : List Name) (us : List Level) : Code

Equations

• code.instantiateValueLevelParams levelParams us = Lean.Compiler.LCNF.Code.instantiateValueLevelParams.instCode levelParams us code

def Lean.Compiler.LCNF.Code.instantiateValueLevelParams.instLevel (levelParams : List Name) (us : List Level) (u : Level) : Level

Equations

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

def Lean.Compiler.LCNF.Code.instantiateValueLevelParams.instExpr (levelParams : List Name) (us : List Level) (e : Expr) : Expr

Equations

• Lean.Compiler.LCNF.Code.instantiateValueLevelParams.instExpr levelParams us e = e.instantiateLevelParamsNoCache levelParams us

def Lean.Compiler.LCNF.Code.instantiateValueLevelParams.instParams (levelParams : List Name) (us : List Level) (ps : Array Param) : Array Param

Equations

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

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

def Lean.Compiler.LCNF.Code.instantiateValueLevelParams.instArg (levelParams : List Name) (us : List Level) (arg : Arg) : Arg

Equations

• One or more equations did not get rendered due to their size.
• Lean.Compiler.LCNF.Code.instantiateValueLevelParams.instArg levelParams us (Lean.Compiler.LCNF.Arg.fvar fvarId) = Lean.Compiler.LCNF.Arg.fvar fvarId
• Lean.Compiler.LCNF.Code.instantiateValueLevelParams.instArg levelParams us Lean.Compiler.LCNF.Arg.erased = Lean.Compiler.LCNF.Arg.erased

def Lean.Compiler.LCNF.Code.instantiateValueLevelParams.instLetValue (levelParams : List Name) (us : List Level) (e : LetValue) : LetValue

Equations

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

def Lean.Compiler.LCNF.Code.instantiateValueLevelParams.instLetDecl (levelParams : List Name) (us : List Level) (decl : LetDecl) : LetDecl

Equations

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

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

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

inductive Lean.Compiler.LCNF.DeclValue : Type

• code (code : Code) : DeclValue
• extern (externAttrData : ExternAttrData) : DeclValue

instance Lean.Compiler.LCNF.instInhabitedDeclValue : Inhabited DeclValue

Equations

• Lean.Compiler.LCNF.instInhabitedDeclValue = { default := Lean.Compiler.LCNF.DeclValue.code default }

instance Lean.Compiler.LCNF.instBEqDeclValue : BEq DeclValue

Equations

• Lean.Compiler.LCNF.instBEqDeclValue = { beq := Lean.Compiler.LCNF.beqDeclValue✝ }

def Lean.Compiler.LCNF.DeclValue.size : DeclValue → Nat

Equations

• (Lean.Compiler.LCNF.DeclValue.code c).size = c.size
• (Lean.Compiler.LCNF.DeclValue.extern externAttrData).size = 0

def Lean.Compiler.LCNF.DeclValue.mapCode (f : Code → Code) : DeclValue → DeclValue

Equations

• Lean.Compiler.LCNF.DeclValue.mapCode f (Lean.Compiler.LCNF.DeclValue.code c) = Lean.Compiler.LCNF.DeclValue.code (f c)
• Lean.Compiler.LCNF.DeclValue.mapCode f (Lean.Compiler.LCNF.DeclValue.extern externAttrData) = Lean.Compiler.LCNF.DeclValue.extern externAttrData

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

Equations

• Lean.Compiler.LCNF.DeclValue.mapCodeM f (Lean.Compiler.LCNF.DeclValue.code c) = do let __do_lift ← f c pure (Lean.Compiler.LCNF.DeclValue.code __do_lift)
• Lean.Compiler.LCNF.DeclValue.mapCodeM f (Lean.Compiler.LCNF.DeclValue.extern externAttrData) = pure (Lean.Compiler.LCNF.DeclValue.extern externAttrData)

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

Equations

• Lean.Compiler.LCNF.DeclValue.forCodeM f (Lean.Compiler.LCNF.DeclValue.code c) = f c
• Lean.Compiler.LCNF.DeclValue.forCodeM f (Lean.Compiler.LCNF.DeclValue.extern externAttrData) = pure ()

def Lean.Compiler.LCNF.DeclValue.isCodeAndM {m : Type → Type u_1} [Monad m] (v : DeclValue) (f : Code → m Bool) : m Bool

Equations

• (Lean.Compiler.LCNF.DeclValue.code c).isCodeAndM f = f c
• (Lean.Compiler.LCNF.DeclValue.extern externAttrData).isCodeAndM f = pure false

structure Lean.Compiler.LCNF.Decl : Type

Declaration being processed by the Lean to Lean compiler passes.

• name : Name

  The name of the declaration from the Environment it came from

• levelParams : List Name

  Universe level parameter names.

• type : 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 Param

  Parameters.

• value : DeclValue

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

Equations

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

instance Lean.Compiler.LCNF.instBEqDecl : BEq Decl

Equations

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

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

Equations

• decl.size = decl.value.size

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

Equations

• decl.getArity = decl.params.size

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Compiler.LCNF.Decl.inlineable (decl : 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 : 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

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

def Lean.Compiler.LCNF.Decl.isCasesOnParam?.go (decl : Decl) (code : 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 : Decl) (us : List Level) : Expr

Equations

• decl.instantiateTypeLevelParams us = decl.type.instantiateLevelParamsNoCache decl.levelParams us

def Lean.Compiler.LCNF.Decl.instantiateParamsLevelParams (decl : Decl) (us : List Level) : Array 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.hasLocalInst (type : 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 : Decl) : 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 : FunDecl) (s : FVarIdSet := ∅) : FVarIdSet

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

@[reducible, inline]

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

Equations

• Lean.Compiler.LCNF.collectUsedAtExpr s e = Lean.Compiler.LCNF.collectType✝ e s

def Lean.Compiler.LCNF.markRecDecls (decls : Array Decl) : Array 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 Decl) (code : Code) : StateM NameSet Unit

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

Equations

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

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

Equations

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

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

Equations

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