- jp: Lean.Compiler.LCNF.FunDecl → Lean.Compiler.LCNF.ToLCNF.Element
- fun: Lean.Compiler.LCNF.FunDecl → Lean.Compiler.LCNF.ToLCNF.Element
- let: Lean.Compiler.LCNF.LetDecl → Lean.Compiler.LCNF.ToLCNF.Element
- cases: Lean.Compiler.LCNF.Param → Lean.Compiler.LCNF.Cases → Lean.Compiler.LCNF.ToLCNF.Element
- unreach: Lean.Compiler.LCNF.Param → Lean.Compiler.LCNF.ToLCNF.Element
Auxiliary inductive datatype for constructing LCNF
toLCNF function maintains a sequence of elements that is eventually
This method returns code that at each exit point of
cases, it jumps to
It is similar to
Code.bind, but we add special support for
inlineMatcher function inlines the auxiliary
To make sure there is no code duplication,
inlineMatcher creates auxiliary declarations
We can say the
_alt. declarations are pre join points. For each auxiliary declaration used at
an exit point of
cases, this method creates an new auxiliary join point that invokes
and then jumps to
jpDecl. The goal is to make sure the auxiliary join point is the only occurrence
simp will inline it.
That is, our goal is to try to promote the pre join points
_alt. into a proper join point.
- lctx : Lean.LocalContext
Local context containing the original Lean types (not LCNF ones).
Cache from Lean regular expression to LCNF argument.
LCNF sequence, we chain it to create a LCNF
- toAny : Lean.FVarIdSet
Fields that are type formers must be replaced with
◾in the resulting code. Otherwise, we have data occurring in types. When converting a
casesOninto LCNF, we add constructor fields that are types and type formers into this set. See
Put the given expression in
- Nested proofs are replaced with
- Eta-expand applications of declarations that satisfy
- Put computationally relevant expressions in A-normal form.