- base: Lean.Compiler.LCNF.Phase
Here we still carry most of the original type information, most of the dependent portion is already (partially) erased though.
- mono: Lean.Compiler.LCNF.Phase
In this phase polymorphism has been eliminated.
- impure: Lean.Compiler.LCNF.Phase
In this phase impure stuff such as RC or efficient BaseIO transformations happen.
The pipeline phase a certain Pass
is supposed to happen in.
Instances For
- lctx : Lean.Compiler.LCNF.LCtx
A
LocalContext
to store local declarations from let binders and other constructs in as we move throughExpr
s. - nextIdx : Nat
Next auxiliary variable suffix
The state managed by the CompilerM
Monad
.
Instances For
- phase : Lean.Compiler.LCNF.Phase
- config : Lean.Compiler.LCNF.ConfigOptions
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Erase all free variables occurring in decls
from the local context.
Instances For
Instances For
Instances For
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.
Instances For
- fvar: Lean.FVarId → Lean.Compiler.LCNF.NormFVarResult
New free variable.
- erased: Lean.Compiler.LCNF.NormFVarResult
Free variable has been erased. This can happen when instantiating polymorphic code with computationally irrelant stuff.
Result type for normFVar
and normFVarImp
.
Instances For
- getSubst : m Lean.Compiler.LCNF.FVarSubst
Interface for monads that have a free substitutions.
Instances
- modifySubst : (Lean.Compiler.LCNF.FVarSubst → Lean.Compiler.LCNF.FVarSubst) → m Unit
Instances
Add the entry fvarId ↦ fvarId'
to the free variable substitution.
Instances For
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.
Instances For
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.
Instances For
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.
Instances For
Replace the free variables in arg
using the given substitution.
See normExprImp
Instances For
Replace the free variables in e
using the given substitution.
See normExprImp
Instances For
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.
Instances For
Normalize the given arguments using the current substitution.
Instances For
Instances For
Instances For
Helper functions for creating LCNF local declarations.
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
If result
is .fvar fvarId
, then return x fvarId
. Otherwise, it is .erased
,
and method returns let _x.i := .erased; return _x.i
.
Instances For
Instances For
Similar to internalize
, but does not refresh FVarId
s.