Documentation

Lean.Compiler.LCNF.CompilerM

source
inductive Lean.Compiler.LCNF.Phase :
Type

The pipeline phase a certain Pass is supposed to happen in.

  • base : Phase

    Here we still carry most of the original type information, most of the dependent portion is already (partially) erased though.

  • mono : Phase

    In this phase polymorphism has been eliminated.

  • impure : Phase

    In this phase impure stuff such as RC or efficient BaseIO transformations happen.

Instances For
source
instance Lean.Compiler.LCNF.instInhabitedPhase :
Inhabited Phase
Equations
source
structure Lean.Compiler.LCNF.CompilerM.State :
Type

The state managed by the CompilerM Monad.

  • lctx : LCtx

    A LocalContext to store local declarations from let binders and other constructs in as we move through Exprs.

  • nextIdx : Nat

    Next auxiliary variable suffix

Instances For
source
instance Lean.Compiler.LCNF.CompilerM.instInhabitedState :
Inhabited State
Equations
source
structure Lean.Compiler.LCNF.CompilerM.Context :
Type
Instances For
source
instance Lean.Compiler.LCNF.CompilerM.instInhabitedContext :
Inhabited Context
Equations
source
@[reducible, inline]
abbrev Lean.Compiler.LCNF.CompilerM (α : Type) :
Type
Equations
Instances For
source
@[always_inline]
instance Lean.Compiler.LCNF.instMonadCompilerM :
Monad CompilerM
Equations
  • One or more equations did not get rendered due to their size.
source
@[inline]
def Lean.Compiler.LCNF.withPhase {α : Type} (phase : Phase) (x : CompilerM α) :
CompilerM α
Equations
source
def Lean.Compiler.LCNF.getPhase :
CompilerM Phase
Equations
source
def Lean.Compiler.LCNF.inBasePhase :
CompilerM Bool
Equations
source
instance Lean.Compiler.LCNF.instAddMessageContextCompilerM :
AddMessageContext CompilerM
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Compiler.LCNF.getType (fvarId : FVarId) :
CompilerM Expr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Compiler.LCNF.getBinderName (fvarId : FVarId) :
CompilerM Name
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Compiler.LCNF.findParam? (fvarId : FVarId) :
CompilerM (Option Param)
Equations
source
def Lean.Compiler.LCNF.findLetDecl? (fvarId : FVarId) :
CompilerM (Option LetDecl)
Equations
source
def Lean.Compiler.LCNF.findFunDecl? (fvarId : FVarId) :
CompilerM (Option FunDecl)
Equations
source
def Lean.Compiler.LCNF.findLetValue? (fvarId : FVarId) :
CompilerM (Option LetValue)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Compiler.LCNF.isConstructorApp (fvarId : FVarId) :
CompilerM Bool
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Compiler.LCNF.Arg.isConstructorApp (arg : Arg) :
CompilerM Bool
Equations
source
def Lean.Compiler.LCNF.getParam (fvarId : FVarId) :
CompilerM Param
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Compiler.LCNF.getLetDecl (fvarId : FVarId) :
CompilerM LetDecl
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Compiler.LCNF.getFunDecl (fvarId : FVarId) :
CompilerM FunDecl
Equations
  • One or more equations did not get rendered due to their size.
source
@[inline]
def Lean.Compiler.LCNF.modifyLCtx (f : LCtx → LCtx) :
CompilerM Unit
Equations
source
def Lean.Compiler.LCNF.eraseLetDecl (decl : LetDecl) :
CompilerM Unit
Equations
source
def Lean.Compiler.LCNF.eraseFunDecl (decl : FunDecl) (recursive : Bool := true) :
CompilerM Unit
Equations
source
def Lean.Compiler.LCNF.eraseCode (code : Code) :
CompilerM Unit
Equations
source
def Lean.Compiler.LCNF.eraseParam (param : Param) :
CompilerM Unit
Equations
source
def Lean.Compiler.LCNF.eraseParams (params : Array Param) :
CompilerM Unit
Equations
source
def Lean.Compiler.LCNF.eraseCodeDecl (decl : CodeDecl) :
CompilerM Unit
Equations
source
def Lean.Compiler.LCNF.eraseCodeDecls (decls : Array CodeDecl) :
CompilerM Unit

Erase all free variables occurring in decls from the local context.

Equations
source
def Lean.Compiler.LCNF.eraseDecl (decl : Decl) :
CompilerM Unit
Equations
source
@[reducible, inline]
abbrev Lean.Compiler.LCNF.Decl.erase (decl : Decl) :
CompilerM Unit
Equations
source
@[reducible, inline]
abbrev Lean.Compiler.LCNF.FVarSubst :
Type

A free variable substitution. We use these substitutions when inlining definitions and "internalizing" LCNF code into CompilerM. During the internalization process, we ensure all free variables in the LCNF code do not collide with existing ones at the CompilerM local context. Remark: in LCNF, (computationally relevant) data is in A-normal form, but this is not the case for types and type formers. So, when inlining we often want to replace a free variable with a type or type former.

The substitution contains entries fvarId ↦ e s.t., e is a valid LCNF argument. That is, it is a free variable, a type (or type former), or lcErased.

Check.lean contains a substitution validator.

Equations
source
inductive Lean.Compiler.LCNF.NormFVarResult :
Type

Result type for normFVar and normFVarImp.

  • fvar (fvarId : FVarId) : NormFVarResult

    New free variable.

  • erased : NormFVarResult

    Free variable has been erased. This can happen when instantiating polymorphic code with computationally irrelant stuff.

Instances For
source
instance Lean.Compiler.LCNF.instInhabitedNormFVarResult :
Inhabited NormFVarResult
Equations
source
class Lean.Compiler.LCNF.MonadFVarSubst (m : Type → Type) (translator : outParam Bool) :
Type

Interface for monads that have a free substitutions.

Instances
source
instance Lean.Compiler.LCNF.instMonadFVarSubstOfMonadLift {t : Bool} (m n : Type → Type) [MonadLift m n] [MonadFVarSubst m t] :
MonadFVarSubst n t
Equations
source
class Lean.Compiler.LCNF.MonadFVarSubstState (m : Type → Type) :
Type
Instances
source
instance Lean.Compiler.LCNF.instMonadFVarSubstStateOfMonadLift (m n : Type → Type) [MonadLift m n] [MonadFVarSubstState m] :
MonadFVarSubstState n
Equations
  • One or more equations did not get rendered due to their size.
source
@[inline]
def Lean.Compiler.LCNF.addFVarSubst {m : Type → Type} [MonadFVarSubstState m] (fvarId fvarId' : FVarId) :
m Unit

Add the entry fvarId ↦ fvarId' to the free variable substitution.

Equations
source
@[inline]
def Lean.Compiler.LCNF.addSubst {m : Type → Type} [MonadFVarSubstState m] (fvarId : FVarId) (e : Expr) :
m Unit

Add the substitution fvarId ↦ e, e must be a valid LCNF argument. That is, it must be a free variable, type (or type former), or lcErased.

See Check.lean for the free variable substitution checker.

Equations
source
@[inline]
def Lean.Compiler.LCNF.normFVar {m : Type → Type} {t : Bool} [MonadFVarSubst m t] [Monad m] (fvarId : FVarId) :
m NormFVarResult

Normalize the given free variable. See normExprImp for documentation on the translator parameter. This function is meant to be used in contexts where the input free-variable is computationally relevant. This function panics if the substitution is mapping fvarId to an expression that is not another free variable. That is, it is not a type (or type former), nor lcErased. Recall that a valid FVarSubst contains only expressions that are free variables, lcErased, or type formers.

Equations
source
@[inline]
def Lean.Compiler.LCNF.normExpr {m : Type → Type} {t : Bool} [MonadFVarSubst m t] [Monad m] (e : Expr) :
m Expr

Replace the free variables in e using the given substitution.

If translator = true, then we assume the free variables occurring in the range of the substitution are in another local context. For example, translator = true during internalization where we are making sure all free variables in a given expression are replaced with new ones that do not collide with the ones in the current local context.

If translator = false, we assume the substitution contains free variable replacements in the same local context, and given entries such as x₁ ↦ x₂, x₂ ↦ x₃, ..., xₙ₋₁ ↦ xₙ, and the expression f x₁ x₂, we want the resulting expression to be f xₙ xₙ. We use this setting, for example, in the simplifier.

Equations
source
@[inline]
def Lean.Compiler.LCNF.normArg {m : Type → Type} {t : Bool} [MonadFVarSubst m t] [Monad m] (arg : Arg) :
m Arg

Replace the free variables in arg using the given substitution.

See normExprImp

Equations
source
@[inline]
def Lean.Compiler.LCNF.normLetValue {m : Type → Type} {t : Bool} [MonadFVarSubst m t] [Monad m] (e : LetValue) :
m LetValue

Replace the free variables in e using the given substitution.

See normExprImp

Equations
source
@[reducible, inline]
abbrev Lean.Compiler.LCNF.normExprCore (s : FVarSubst) (e : Expr) (translator : Bool) :
Expr

Replace the free variables in e using the given substitution.

If translator = true, then we assume the free variables occurring in the range of the substitution are in another local context. For example, translator = true during internalization where we are making sure all free variables in a given expression are replaced with new ones that do not collide with the ones in the current local context.

If translator = false, we assume the substitution contains free variable replacements in the same local context, and given entries such as x₁ ↦ x₂, x₂ ↦ x₃, ..., xₙ₋₁ ↦ xₙ, and the expression f x₁ x₂, we want the resulting expression to be f xₙ xₙ. We use this setting, for example, in the simplifier.

Equations
source
def Lean.Compiler.LCNF.normArgs {m : Type → Type} {t : Bool} [MonadFVarSubst m t] [Monad m] (args : Array Arg) :
m (Array Arg)

Normalize the given arguments using the current substitution.

Equations
source
def Lean.Compiler.LCNF.mkFreshBinderName (binderName : Name := `_x) :
CompilerM Name
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Compiler.LCNF.ensureNotAnonymous (binderName baseName : Name) :
CompilerM Name
Equations

Helper functions for creating LCNF local declarations.

source
def Lean.Compiler.LCNF.mkParam (binderName : Name) (type : Expr) (borrow : Bool) :
CompilerM Param
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Compiler.LCNF.mkLetDecl (binderName : Name) (type : Expr) (value : LetValue) :
CompilerM LetDecl
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Compiler.LCNF.mkFunDecl (binderName : Name) (type : Expr) (params : Array Param) (value : Code) :
CompilerM FunDecl
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Compiler.LCNF.mkLetDeclErased :
CompilerM LetDecl
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Compiler.LCNF.mkReturnErased :
CompilerM Code
Equations
source
@[implemented_by _private.Lean.Compiler.LCNF.CompilerM.0.Lean.Compiler.LCNF.updateParamImp]
opaque Lean.Compiler.LCNF.Param.update (p : Param) (type : Expr) :
CompilerM Param
source
@[implemented_by _private.Lean.Compiler.LCNF.CompilerM.0.Lean.Compiler.LCNF.updateLetDeclImp]
opaque Lean.Compiler.LCNF.LetDecl.update (decl : LetDecl) (type : Expr) (value : LetValue) :
CompilerM LetDecl
source
def Lean.Compiler.LCNF.LetDecl.updateValue (decl : LetDecl) (value : LetValue) :
CompilerM LetDecl
Equations
source
@[implemented_by _private.Lean.Compiler.LCNF.CompilerM.0.Lean.Compiler.LCNF.updateFunDeclImp]
opaque Lean.Compiler.LCNF.FunDeclCore.update (decl : FunDecl) (type : Expr) (params : Array Param) (value : Code) :
CompilerM FunDecl
source
@[reducible, inline]
abbrev Lean.Compiler.LCNF.FunDeclCore.update' (decl : FunDecl) (type : Expr) (value : Code) :
CompilerM FunDecl
Equations
source
@[reducible, inline]
abbrev Lean.Compiler.LCNF.FunDeclCore.updateValue (decl : FunDecl) (value : Code) :
CompilerM FunDecl
Equations
source
@[inline]
def Lean.Compiler.LCNF.normParam {m : Type → Type} {t : Bool} [MonadLiftT CompilerM m] [Monad m] [MonadFVarSubst m t] (p : Param) :
m Param
Equations
source
def Lean.Compiler.LCNF.normParams {m : Type → Type} {t : Bool} [MonadLiftT CompilerM m] [Monad m] [MonadFVarSubst m t] (ps : Array Param) :
m (Array Param)
Equations
source
def Lean.Compiler.LCNF.normLetDecl {m : Type → Type} {t : Bool} [MonadLiftT CompilerM m] [Monad m] [MonadFVarSubst m t] (decl : LetDecl) :
m LetDecl
Equations
  • One or more equations did not get rendered due to their size.
source
@[reducible, inline]
abbrev Lean.Compiler.LCNF.NormalizerM (_translator : Bool) (α : Type) :
Type
Equations
Instances For
source
instance Lean.Compiler.LCNF.instMonadFVarSubstNormalizerM {t : Bool} :
MonadFVarSubst (NormalizerM t) t
Equations
source
@[inline]
def Lean.Compiler.LCNF.withNormFVarResult {m : Type → Type u_1} [MonadLiftT CompilerM m] [Monad m] (result : NormFVarResult) (x : FVarId → m Code) :
m Code

If result is .fvar fvarId, then return x fvarId. Otherwise, it is .erased, and method returns let _x.i := .erased; return _x.i.

Equations
source
partial def Lean.Compiler.LCNF.normFunDeclImp {t : Bool} (decl : FunDecl) :
NormalizerM t FunDecl
source
partial def Lean.Compiler.LCNF.normCodeImp {t : Bool} (code : Code) :
NormalizerM t Code
source
@[inline]
def Lean.Compiler.LCNF.normFunDecl {m : Type → Type} {t : Bool} [MonadLiftT CompilerM m] [Monad m] [MonadFVarSubst m t] (decl : FunDecl) :
m FunDecl
Equations
source
@[inline]
def Lean.Compiler.LCNF.normCode {m : Type → Type} {t : Bool} [MonadLiftT CompilerM m] [Monad m] [MonadFVarSubst m t] (code : Code) :
m Code

Similar to internalize, but does not refresh FVarIds.

Equations
source
def Lean.Compiler.LCNF.replaceExprFVars (e : Expr) (s : FVarSubst) (translator : Bool) :
CompilerM Expr
Equations
source
def Lean.Compiler.LCNF.replaceFVars (code : Code) (s : FVarSubst) (translator : Bool) :
CompilerM Code
Equations
source
def Lean.Compiler.LCNF.mkFreshJpName :
CompilerM Name
Equations
source
def Lean.Compiler.LCNF.mkAuxParam (type : Expr) (borrow : Bool := false) :
CompilerM Param
Equations
source
def Lean.Compiler.LCNF.getConfig :
CompilerM ConfigOptions
Equations
source
def Lean.Compiler.LCNF.CompilerM.run {α : Type} (x : CompilerM α) (s : State := { }) (phase : Phase := Phase.base) :
CoreM α
Equations
source
structure Lean.Compiler.LCNF.CacheExtension (α β : Type) [BEq α] [Hashable α] extends Lean.EnvExtension (List α × Lean.PHashMap α β) :
Type

Environment extension for local caching of key-value pairs, not persisted in .olean files.

Instances For
source
instance Lean.Compiler.LCNF.instInhabitedCacheExtension {a✝ a✝¹ : Type} {a✝² : BEq a✝} {a✝³ : Hashable a✝} :
Inhabited (CacheExtension a✝ a✝¹)
Equations
source
def Lean.Compiler.LCNF.CacheExtension.register {α β : Type} [BEq α] [Hashable α] [Inhabited β] :
IO (CacheExtension α β)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Compiler.LCNF.CacheExtension.insert {α β : Type} [BEq α] [Hashable α] [Inhabited β] (ext : CacheExtension α β) (a : α) (b : β) :
CoreM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Compiler.LCNF.CacheExtension.find? {α β : Type} [BEq α] [Hashable α] [Inhabited β] (ext : CacheExtension α β) (a : α) :
CoreM (Option β)
Equations