Lean Compiler Normal Form (LCNF) #

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

source

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

source

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

Type

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

Instances For

Lean.Compiler.LCNF.instInhabitedCasesCore

source

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

source

instance Lean.Compiler.LCNF.instInhabitedCode :

Inhabited Lean.Compiler.LCNF.Code

Equations

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

source

@[inline, reducible]

abbrev Lean.Compiler.LCNF.Alt :

Type

Equations

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

Instances For

Lean.Compiler.LCNF.instTraverseFVarAlt

source

@[inline, reducible]

abbrev Lean.Compiler.LCNF.FunDecl :

Type

Equations

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

Instances For

source

@[inline, reducible]

abbrev Lean.Compiler.LCNF.Cases :

Type

Equations

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

source

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.

source

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

Instances For

source

instance Lean.Compiler.LCNF.instInhabitedCodeDecl :

Inhabited Lean.Compiler.LCNF.CodeDecl

Equations

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

source

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.

source

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

source

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.

source

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

source

instance Lean.Compiler.LCNF.instBEqCode :

BEq Lean.Compiler.LCNF.Code

Equations

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

source

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

source

instance Lean.Compiler.LCNF.instBEqFunDecl :

BEq Lean.Compiler.LCNF.FunDecl

Equations

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

source

def Lean.Compiler.LCNF.AltCore.getCode :

Lean.Compiler.LCNF.Alt → Lean.Compiler.LCNF.Code

Equations

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

source

def Lean.Compiler.LCNF.AltCore.getParams :

Lean.Compiler.LCNF.Alt → Array Lean.Compiler.LCNF.Param

Equations

Lean.Compiler.LCNF.AltCore.getParams x = match x with | Lean.Compiler.LCNF.AltCore.default code => #[] | Lean.Compiler.LCNF.AltCore.alt ctorName ps code => ps

source

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.forCodeM alt f = match alt with | Lean.Compiler.LCNF.AltCore.default k => f k | Lean.Compiler.LCNF.AltCore.alt ctorName params k => f k

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

Lean.Compiler.LCNF.Alt × Lean.Compiler.LCNF.Cases

Equations

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

source

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)

source

def Lean.Compiler.LCNF.Code.isDecl :

Lean.Compiler.LCNF.Code → Bool

Equations

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

source

def Lean.Compiler.LCNF.Code.isFun :

Lean.Compiler.LCNF.Code → Bool

Equations

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

source

def Lean.Compiler.LCNF.Code.isReturnOf :

Lean.Compiler.LCNF.Code → Lean.FVarId → Bool

Equations

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

source

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

source

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

Nat

source

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

source

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

source

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

EStateM Unit Nat Unit

source

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

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

source

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

source

structure Lean.Compiler.LCNF.Decl :

Type

Declaration being processed by the Lean to Lean compiler passes.

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

Instances For

source

instance Lean.Compiler.LCNF.instInhabitedDecl :

Inhabited Lean.Compiler.LCNF.Decl

Equations

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

source

instance Lean.Compiler.LCNF.instBEqDecl :

BEq Lean.Compiler.LCNF.Decl

Equations

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

source

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

source

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

Nat

Equations

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

source

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

Bool

Equations

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

source

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

Bool

Equations

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

source

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

Bool

Equations

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

source

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

Bool

Equations

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

source

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

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

source

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

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

source

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 : Lean.Compiler.LCNF.Param) => param.fvarId == c.discr
Lean.Compiler.LCNF.Decl.isCasesOnParam?.go decl code = none

source

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.instantiateLevelParamsNoCache decl.type decl.levelParams us

source

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.

source

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

source

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 = Lean.Level.instantiateParams u decl.levelParams us

source

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.instantiateLevelParamsNoCache e decl.levelParams us

source

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.

source

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

source

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

Equations

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

source

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.

source

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.

source

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

source

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

source

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

source

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.

source

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

Lean.FVarIdSet

source

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

Lean.FVarIdSet

source

@[inline, reducible]

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

source

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