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.

instance Lean.Compiler.LCNF.instInhabitedPhase : Inhabited Phase

Equations

• Lean.Compiler.LCNF.instInhabitedPhase = { default := Lean.Compiler.LCNF.Phase.base }

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

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

Equations

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

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

• phase : Phase
• config : ConfigOptions

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

Equations

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

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

@[always_inline]

instance Lean.Compiler.LCNF.instMonadCompilerM : Monad CompilerM

Equations

• Lean.Compiler.LCNF.instMonadCompilerM = Monad.mk

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

def Lean.Compiler.LCNF.getPhase : CompilerM Phase

Equations

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

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)

instance Lean.Compiler.LCNF.instAddMessageContextCompilerM : AddMessageContext CompilerM

Equations

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

def Lean.Compiler.LCNF.getType (fvarId : FVarId) : CompilerM Expr

Equations

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

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

Equations

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

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]?

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]?

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]?

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

Equations

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

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

Equations

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

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

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

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

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

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

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

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

@[reducible, inline]

abbrev Lean.Compiler.LCNF.Decl.erase (decl : Decl) : CompilerM Unit

Equations

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

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

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.

instance Lean.Compiler.LCNF.instInhabitedNormFVarResult : Inhabited NormFVarResult

Equations

• Lean.Compiler.LCNF.instInhabitedNormFVarResult = { default := Lean.Compiler.LCNF.NormFVarResult.fvar default }

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

Interface for monads that have a free substitutions.

• getSubst : m FVarSubst

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 }

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

• modifySubst : (FVarSubst → FVarSubst) → m Unit

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.

@[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.Expr.fvar fvarId')

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

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

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

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

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

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

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

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

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)

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

Equations

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

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

Helper functions for creating LCNF local declarations.

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.

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.

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.

def Lean.Compiler.LCNF.mkLetDeclErased : CompilerM LetDecl

Equations

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

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

@[implemented_by _private.Lean.Compiler.LCNF.CompilerM.0.Lean.Compiler.LCNF.updateParamImp]

opaque Lean.Compiler.LCNF.Param.update (p : Param) (type : Expr) : CompilerM Param

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

def Lean.Compiler.LCNF.LetDecl.updateValue (decl : LetDecl) (value : LetValue) : CompilerM LetDecl

Equations

• decl.updateValue value = decl.update decl.type value

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

@[reducible, inline]

abbrev Lean.Compiler.LCNF.FunDeclCore.update' (decl : FunDecl) (type : Expr) (value : Code) : CompilerM FunDecl

Equations

• Lean.Compiler.LCNF.FunDeclCore.update' decl type value = Lean.Compiler.LCNF.FunDeclCore.update decl type decl.params value

@[reducible, inline]

abbrev Lean.Compiler.LCNF.FunDeclCore.updateValue (decl : FunDecl) (value : Code) : CompilerM FunDecl

Equations

• Lean.Compiler.LCNF.FunDeclCore.updateValue decl value = Lean.Compiler.LCNF.FunDeclCore.update decl decl.type decl.params value

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

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

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.

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

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

Equations

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

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

partial def Lean.Compiler.LCNF.normFunDeclImp {t : Bool} (decl : FunDecl) : NormalizerM t FunDecl

partial def Lean.Compiler.LCNF.normCodeImp {t : Bool} (code : Code) : NormalizerM t Code

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

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

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

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

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

def Lean.Compiler.LCNF.mkFreshJpName : CompilerM Name

Equations

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

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

def Lean.Compiler.LCNF.getConfig : CompilerM ConfigOptions

Equations

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

def Lean.Compiler.LCNF.CompilerM.run {α : Type} (x : CompilerM α) (s : State := { lctx := { params := ∅, letDecls := ∅, funDecls := ∅ }, nextIdx := 1 }) (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