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.

Instances For

source
instance Lean.Compiler.LCNF.instInhabitedPhase :
Inhabited Phase
Equations

- Lean.Compiler.LCNF.instInhabitedPhase = { default := Lean.Compiler.LCNF.instInhabitedPhase.default }

source
def Lean.Compiler.LCNF.instInhabitedPhase.default :
Phase
Equations

- Lean.Compiler.LCNF.instInhabitedPhase.default = Lean.Compiler.LCNF.Phase.base

Instances For

source
def Lean.Compiler.LCNF.instBEqPhase.beq :
Phase → Phase → Bool
Equations

- Lean.Compiler.LCNF.instBEqPhase.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source
instance Lean.Compiler.LCNF.instBEqPhase :
BEq Phase
Equations

- Lean.Compiler.LCNF.instBEqPhase = { beq := Lean.Compiler.LCNF.instBEqPhase.beq }

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 `Expr`s.

- nextIdx : Nat

  Next auxiliary variable suffix

Instances For

source
instance Lean.Compiler.LCNF.CompilerM.instInhabitedState :
Inhabited State
Equations

- Lean.Compiler.LCNF.CompilerM.instInhabitedState = { default := Lean.Compiler.LCNF.CompilerM.instInhabitedState.default }

source
def Lean.Compiler.LCNF.CompilerM.instInhabitedState.default :
State
Equations

- Lean.Compiler.LCNF.CompilerM.instInhabitedState.default = { lctx := default, nextIdx := default }

Instances For

source
structure Lean.Compiler.LCNF.CompilerM.Context :
Type

- phase : Phase
- config : ConfigOptions

Instances For

source
def Lean.Compiler.LCNF.CompilerM.instInhabitedContext.default :
Context
Equations

- Lean.Compiler.LCNF.CompilerM.instInhabitedContext.default = { phase := default, config := default }

Instances For

source
instance Lean.Compiler.LCNF.CompilerM.instInhabitedContext :
Inhabited Context
Equations

- Lean.Compiler.LCNF.CompilerM.instInhabitedContext = { default := Lean.Compiler.LCNF.CompilerM.instInhabitedContext.default }

source
@[reducible, inline]
abbrev Lean.Compiler.LCNF.CompilerM (α : Type) :
Type
Equations

- Lean.Compiler.LCNF.CompilerM = ReaderT Lean.Compiler.LCNF.CompilerM.Context (StateRefT' IO.RealWorld Lean.Compiler.LCNF.CompilerM.State Lean.CoreM)

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

- Lean.Compiler.LCNF.withPhase phase x = withReader (fun (ctx : Lean.Compiler.LCNF.CompilerM.Context) => { phase := phase, config := ctx.config }) x

Instances For

source
def Lean.Compiler.LCNF.getPhase :
CompilerM Phase
Equations

- Lean.Compiler.LCNF.getPhase = do let __do_lift ← read pure __do_lift.phase

Instances For

source
def Lean.Compiler.LCNF.inBasePhase :
CompilerM Bool
Equations

- Lean.Compiler.LCNF.inBasePhase = do let __do_lift ← Lean.Compiler.LCNF.getPhase pure (match __do_lift with | Lean.Compiler.LCNF.Phase.base => true | x => false)

Instances For

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.

Instances For

source
def Lean.Compiler.LCNF.getBinderName (fvarId : FVarId) :
CompilerM Name
Equations

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

Instances For

source
def Lean.Compiler.LCNF.findParam? (fvarId : FVarId) :
CompilerM (Option Param)
Equations

- Lean.Compiler.LCNF.findParam? fvarId = do let __do_lift ← get pure __do_lift.lctx.params[fvarId]?

Instances For

source
def Lean.Compiler.LCNF.findLetDecl? (fvarId : FVarId) :
CompilerM (Option LetDecl)
Equations

- Lean.Compiler.LCNF.findLetDecl? fvarId = do let __do_lift ← get pure __do_lift.lctx.letDecls[fvarId]?

Instances For

source
def Lean.Compiler.LCNF.findFunDecl? (fvarId : FVarId) :
CompilerM (Option FunDecl)
Equations

- Lean.Compiler.LCNF.findFunDecl? fvarId = do let __do_lift ← get pure __do_lift.lctx.funDecls[fvarId]?

Instances For

source
def Lean.Compiler.LCNF.findLetValue? (fvarId : FVarId) :
CompilerM (Option LetValue)
Equations

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

Instances For

source
def Lean.Compiler.LCNF.isConstructorApp (fvarId : FVarId) :
CompilerM Bool
Equations

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

Instances For

source
def Lean.Compiler.LCNF.Arg.isConstructorApp (arg : Arg) :
CompilerM Bool
Equations

- (Lean.Compiler.LCNF.Arg.fvar fvarId).isConstructorApp = Lean.Compiler.LCNF.isConstructorApp fvarId
- arg.isConstructorApp = pure false

Instances For

source
def Lean.Compiler.LCNF.getParam (fvarId : FVarId) :
CompilerM Param
Equations

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

Instances For

source
def Lean.Compiler.LCNF.getLetDecl (fvarId : FVarId) :
CompilerM LetDecl
Equations

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

Instances For

source
def Lean.Compiler.LCNF.getFunDecl (fvarId : FVarId) :
CompilerM FunDecl
Equations

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

Instances For

source
@[inline]
def Lean.Compiler.LCNF.modifyLCtx (f : LCtx → LCtx) :
CompilerM Unit
Equations

- Lean.Compiler.LCNF.modifyLCtx f = modify fun (s : Lean.Compiler.LCNF.CompilerM.State) => { lctx := f s.lctx, nextIdx := s.nextIdx }

Instances For

source
def Lean.Compiler.LCNF.eraseLetDecl (decl : LetDecl) :
CompilerM Unit
Equations

- Lean.Compiler.LCNF.eraseLetDecl decl = Lean.Compiler.LCNF.modifyLCtx fun (lctx : Lean.Compiler.LCNF.LCtx) => lctx.eraseLetDecl decl

Instances For

source
def Lean.Compiler.LCNF.eraseFunDecl (decl : FunDecl) (recursive : Bool := true) :
CompilerM Unit
Equations

- Lean.Compiler.LCNF.eraseFunDecl decl recursive = Lean.Compiler.LCNF.modifyLCtx fun (lctx : Lean.Compiler.LCNF.LCtx) => lctx.eraseFunDecl decl recursive

Instances For

source
def Lean.Compiler.LCNF.eraseCode (code : Code) :
CompilerM Unit
Equations

- Lean.Compiler.LCNF.eraseCode code = Lean.Compiler.LCNF.modifyLCtx fun (lctx : Lean.Compiler.LCNF.LCtx) => Lean.Compiler.LCNF.LCtx.eraseCode code lctx

Instances For

source
def Lean.Compiler.LCNF.eraseParam (param : Param) :
CompilerM Unit
Equations

- Lean.Compiler.LCNF.eraseParam param = Lean.Compiler.LCNF.modifyLCtx fun (lctx : Lean.Compiler.LCNF.LCtx) => lctx.eraseParam param

Instances For

source
def Lean.Compiler.LCNF.eraseParams (params : Array Param) :
CompilerM Unit
Equations

- Lean.Compiler.LCNF.eraseParams params = Lean.Compiler.LCNF.modifyLCtx fun (lctx : Lean.Compiler.LCNF.LCtx) => lctx.eraseParams params

Instances For

source
def Lean.Compiler.LCNF.eraseCodeDecl (decl : CodeDecl) :
CompilerM Unit
Equations

- Lean.Compiler.LCNF.eraseCodeDecl (Lean.Compiler.LCNF.CodeDecl.let decl_2) = Lean.Compiler.LCNF.eraseLetDecl decl_2
- Lean.Compiler.LCNF.eraseCodeDecl (Lean.Compiler.LCNF.CodeDecl.jp decl_2) = Lean.Compiler.LCNF.eraseFunDecl decl_2
- Lean.Compiler.LCNF.eraseCodeDecl (Lean.Compiler.LCNF.CodeDecl.fun decl_2) = Lean.Compiler.LCNF.eraseFunDecl decl_2

Instances For

source
def Lean.Compiler.LCNF.eraseCodeDecls (decls : Array CodeDecl) :
CompilerM Unit

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

Equations

- Lean.Compiler.LCNF.eraseCodeDecls decls = Array.forM (fun (decl : Lean.Compiler.LCNF.CodeDecl) => Lean.Compiler.LCNF.eraseCodeDecl decl) decls

Instances For

source
def Lean.Compiler.LCNF.eraseDecl (decl : Decl) :
CompilerM Unit
Equations

- Lean.Compiler.LCNF.eraseDecl decl = do Lean.Compiler.LCNF.eraseParams decl.params Lean.Compiler.LCNF.DeclValue.forCodeM Lean.Compiler.LCNF.eraseCode decl.value

Instances For

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

- decl.erase = Lean.Compiler.LCNF.eraseDecl decl

Instances For

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

- Lean.Compiler.LCNF.FVarSubst = Std.HashMap Lean.FVarId Lean.Compiler.LCNF.Arg

Instances For

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

Instances For

source
def Lean.Compiler.LCNF.instInhabitedNormFVarResult.default :
NormFVarResult
Equations

- Lean.Compiler.LCNF.instInhabitedNormFVarResult.default = Lean.Compiler.LCNF.NormFVarResult.fvar default

Instances For

source
instance Lean.Compiler.LCNF.instInhabitedNormFVarResult :
Inhabited NormFVarResult
Equations

- Lean.Compiler.LCNF.instInhabitedNormFVarResult = { default := Lean.Compiler.LCNF.instInhabitedNormFVarResult.default }

source
partial def Lean.Compiler.LCNF.normFVarImp (s : FVarSubst) (fvarId : FVarId) (translator : Bool) :
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.

source
class Lean.Compiler.LCNF.MonadFVarSubst (m : Type → Type) (translator : outParam Bool) :
Type

Interface for monads that have a free substitutions.

- getSubst : m FVarSubst

Instances

source
instance Lean.Compiler.LCNF.instMonadFVarSubstOfMonadLift {t : Bool} (m n : Type → Type) [MonadLift m n] [MonadFVarSubst m t] :
MonadFVarSubst n t
Equations

- Lean.Compiler.LCNF.instMonadFVarSubstOfMonadLift m n = { getSubst := liftM Lean.Compiler.LCNF.getSubst }

source
class Lean.Compiler.LCNF.MonadFVarSubstState (m : Type → Type) :
Type

- modifySubst : (FVarSubst → FVarSubst) → m Unit

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.addSubst {m : Type → Type} [MonadFVarSubstState m] (fvarId : FVarId) (arg : Arg) :
m Unit

Add the substitution `fvarId ↦ e`, `e` must be a valid LCNF `Arg`.

See `Check.lean` for the free variable substitution checker.

Equations

- Lean.Compiler.LCNF.addSubst fvarId arg = Lean.Compiler.LCNF.modifySubst fun (s : Lean.Compiler.LCNF.FVarSubst) => Std.HashMap.insert s fvarId arg

Instances For

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

- Lean.Compiler.LCNF.addFVarSubst fvarId fvarId' = Lean.Compiler.LCNF.modifySubst fun (s : Lean.Compiler.LCNF.FVarSubst) => Std.HashMap.insert s fvarId (Lean.Compiler.LCNF.Arg.fvar fvarId')

Instances For

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

- Lean.Compiler.LCNF.normFVar fvarId = do let __do_lift ← Lean.Compiler.LCNF.getSubst pure (Lean.Compiler.LCNF.normFVarImp __do_lift fvarId t)

Instances For

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

- Lean.Compiler.LCNF.normExpr e = do let __do_lift ← Lean.Compiler.LCNF.getSubst pure (Lean.Compiler.LCNF.normExprImp✝ __do_lift e t)

Instances For

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

- Lean.Compiler.LCNF.normArg arg = do let __do_lift ← Lean.Compiler.LCNF.getSubst pure (Lean.Compiler.LCNF.normArgImp✝ __do_lift arg t)

Instances For

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

- Lean.Compiler.LCNF.normLetValue e = do let __do_lift ← Lean.Compiler.LCNF.getSubst pure (Lean.Compiler.LCNF.normLetValueImp✝ __do_lift e t)

Instances For

source
@[inline]
def 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

- Lean.Compiler.LCNF.normExprCore s e translator = Lean.Compiler.LCNF.normExprImp✝ s e translator

Instances For

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

- Lean.Compiler.LCNF.normArgs args = do let __do_lift ← Lean.Compiler.LCNF.getSubst pure (Lean.Compiler.LCNF.normArgsImp✝ __do_lift args t)

Instances For

source
def Lean.Compiler.LCNF.mkFreshBinderName (binderName : Name := `_x) :
CompilerM Name
Equations

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

Instances For

source
def Lean.Compiler.LCNF.ensureNotAnonymous (binderName baseName : Name) :
CompilerM Name
Equations

- Lean.Compiler.LCNF.ensureNotAnonymous binderName baseName = if binderName.isAnonymous = true then Lean.Compiler.LCNF.mkFreshBinderName baseName else pure binderName

Instances For

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.

Instances For

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.

Instances For

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.

Instances For

source
def Lean.Compiler.LCNF.mkLetDeclErased :
CompilerM LetDecl
Equations

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

Instances For

source
def Lean.Compiler.LCNF.mkReturnErased :
CompilerM Code
Equations

- Lean.Compiler.LCNF.mkReturnErased = do let auxDecl ← Lean.Compiler.LCNF.mkLetDeclErased pure (Lean.Compiler.LCNF.Code.let auxDecl (Lean.Compiler.LCNF.Code.return auxDecl.fvarId))

Instances For

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

- decl.updateValue value = decl.update decl.type value

Instances For

source
@[implemented_by _private.Lean.Compiler.LCNF.CompilerM.0.Lean.Compiler.LCNF.updateFunDeclImp]
opaque Lean.Compiler.LCNF.FunDecl.update (decl : FunDecl) (type : Expr) (params : Array Param) (value : Code) :
CompilerM FunDecl
source
@[reducible, inline]
abbrev Lean.Compiler.LCNF.FunDecl.update' (decl : FunDecl) (type : Expr) (value : Code) :
CompilerM FunDecl
Equations

- decl.update' type value = decl.update type decl.params value

Instances For

source
@[reducible, inline]
abbrev Lean.Compiler.LCNF.FunDecl.updateValue (decl : FunDecl) (value : Code) :
CompilerM FunDecl
Equations

- decl.updateValue value = decl.update decl.type decl.params value

Instances For

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

- Lean.Compiler.LCNF.normParam p = do let __do_lift ← Lean.Compiler.LCNF.normExpr p.type liftM (p.update __do_lift)

Instances For

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

- Lean.Compiler.LCNF.normParams ps = ps.mapMonoM Lean.Compiler.LCNF.normParam

Instances For

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.

Instances For

source
@[reducible, inline]
abbrev Lean.Compiler.LCNF.NormalizerM (_translator : Bool) (α : Type) :
Type
Equations

- Lean.Compiler.LCNF.NormalizerM _translator = ReaderT Lean.Compiler.LCNF.FVarSubst Lean.Compiler.LCNF.CompilerM

Instances For

source
instance Lean.Compiler.LCNF.instMonadFVarSubstNormalizerM {t : Bool} :
MonadFVarSubst (NormalizerM t) t
Equations

- Lean.Compiler.LCNF.instMonadFVarSubstNormalizerM = { getSubst := read }

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

- Lean.Compiler.LCNF.withNormFVarResult (Lean.Compiler.LCNF.NormFVarResult.fvar fvarId') x = x fvarId'
- Lean.Compiler.LCNF.withNormFVarResult Lean.Compiler.LCNF.NormFVarResult.erased x = liftM Lean.Compiler.LCNF.mkReturnErased

Instances For

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

- Lean.Compiler.LCNF.normFunDecl decl = do let __do_lift ← Lean.Compiler.LCNF.getSubst liftM (Lean.Compiler.LCNF.normFunDeclImp decl __do_lift)

Instances For

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 `FVarId`s.

Equations

- Lean.Compiler.LCNF.normCode code = do let __do_lift ← Lean.Compiler.LCNF.getSubst liftM (Lean.Compiler.LCNF.normCodeImp code __do_lift)

Instances For

source
def Lean.Compiler.LCNF.replaceExprFVars (e : Expr) (s : FVarSubst) (translator : Bool) :
CompilerM Expr
Equations

- Lean.Compiler.LCNF.replaceExprFVars e s translator = ReaderT.run (Lean.Compiler.LCNF.normExpr e) s

Instances For

source
def Lean.Compiler.LCNF.replaceFVars (code : Code) (s : FVarSubst) (translator : Bool) :
CompilerM Code
Equations

- Lean.Compiler.LCNF.replaceFVars code s translator = ReaderT.run (Lean.Compiler.LCNF.normCode code) s

Instances For

source
def Lean.Compiler.LCNF.mkFreshJpName :
CompilerM Name
Equations

- Lean.Compiler.LCNF.mkFreshJpName = Lean.Compiler.LCNF.mkFreshBinderName `_jp

Instances For

source
def Lean.Compiler.LCNF.mkAuxParam (type : Expr) (borrow : Bool := false) :
CompilerM Param
Equations

- Lean.Compiler.LCNF.mkAuxParam type borrow = do let __do_lift ← Lean.Compiler.LCNF.mkFreshBinderName `_y Lean.Compiler.LCNF.mkParam __do_lift type borrow

Instances For

source
def Lean.Compiler.LCNF.getConfig :
CompilerM ConfigOptions
Equations

- Lean.Compiler.LCNF.getConfig = do let __do_lift ← read pure __do_lift.config

Instances For

source
def Lean.Compiler.LCNF.CompilerM.run {α : Type} (x : CompilerM α) (s : State := { }) (phase : Phase := Phase.base) :
CoreM α
Equations

- x.run s phase = do let __do_lift ← Lean.getOptions (x { phase := phase, config := Lean.Compiler.LCNF.toConfigOptions __do_lift }).run' s

Instances For

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.

- idx : Nat
- mkInitial : IO (List α × PHashMap α β)
- asyncMode : AsyncMode
- replay? : Option (ReplayFn (List α × PHashMap α β))

Instances For

source
def Lean.Compiler.LCNF.instInhabitedCacheExtension.default {a✝ a✝¹ : Type} {a✝² : BEq a✝} {a✝³ : Hashable a✝} :
CacheExtension a✝ a✝¹
Equations

- Lean.Compiler.LCNF.instInhabitedCacheExtension.default = { toEnvExtension := default }

Instances For

source
instance Lean.Compiler.LCNF.instInhabitedCacheExtension {a✝ a✝¹ : Type} {a✝² : BEq a✝} {a✝³ : Hashable a✝} :
Inhabited (CacheExtension a✝ a✝¹)
Equations

- Lean.Compiler.LCNF.instInhabitedCacheExtension = { default := Lean.Compiler.LCNF.instInhabitedCacheExtension.default }

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.

Instances For

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.

Instances For

source
def Lean.Compiler.LCNF.CacheExtension.find? {α β : Type} [BEq α] [Hashable α] [Inhabited β] (ext : CacheExtension α β) (a : α) :
CoreM (Option β)
Equations

- ext.find? a = do let __do_lift ← Lean.getEnv pure (Lean.PersistentHashMap.find? (ext.getState __do_lift).snd a)

Instances For