def Lean.Compiler.LCNF.ToLCNF.isLCProof (e : Expr) : Bool

Return true if e is a lcProof application. Recall that we use lcProof to erase all nested proofs.

def Lean.Compiler.LCNF.ToLCNF.mkLcProof (p : Expr) : Expr

Create the temporary lcProof

inductive Lean.Compiler.LCNF.ToLCNF.Element : Type

Auxiliary inductive datatype for constructing LCNF Code objects. The toLCNF function maintains a sequence of elements that is eventually converted into Code.

• jp (decl : FunDecl Purity.pure) : Element
• fun (decl : FunDecl Purity.pure) : Element
• let (decl : LetDecl Purity.pure) : Element
• cases (p : Param Purity.pure) (cases : Cases Purity.pure) : Element
• unreach (p : Param Purity.pure) : Element

def Lean.Compiler.LCNF.ToLCNF.instInhabitedElement.default : Element

@[implicit_reducible]

instance Lean.Compiler.LCNF.ToLCNF.instInhabitedElement : Inhabited Element

@[reducible, inline]

abbrev Lean.Compiler.LCNF.ToLCNF.BindCasesM.State : Type

State for BindCasesM monad Mapping from _alt.<idx> variables to new join points

@[reducible, inline]

abbrev Lean.Compiler.LCNF.ToLCNF.BindCasesM (α : Type) : Type

Auxiliary monad for implementing bindCases

def Lean.Compiler.LCNF.ToLCNF.bindCases (jpDecl : FunDecl Purity.pure) (cases : Cases Purity.pure) : CompilerM (Code Purity.pure)

This method returns code that at each exit point of cases, it jumps to jpDecl. It is similar to Code.bind, but we add special support for inlineMatcher. The inlineMatcher function inlines the auxiliary _match_<idx> declarations. To make sure there is no code duplication, inlineMatcher creates auxiliary declarations _alt.<idx>. We can say the _alt.<idx> 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 _alt.<idx>, and then jumps to jpDecl. The goal is to make sure the auxiliary join point is the only occurrence of _alt.<idx>, then simp will inline it. That is, our goal is to try to promote the pre join points _alt.<idx> into a proper join point.

def Lean.Compiler.LCNF.ToLCNF.seqToCode (seq : Array Element) (k : Code Purity.pure) : CompilerM (Code Purity.pure)

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

• ignoreNoncomputable : Bool

  Whether uses of noncomputable defs should be ignored; used in contexts that will be erased eventually.

structure Lean.Compiler.LCNF.ToLCNF.State : Type

• lctx : LocalContext

  Local context containing the original Lean types (not LCNF ones).

• cache : PHashMap Expr (Arg Purity.pure)

  Cache from Lean regular expression to LCNF argument.

• shouldCache : Bool

  Determines whether caching has been disabled due to finding a use of a constant marked with never_extract.

• typeCache : Std.HashMap Expr Expr

  toLCNFType cache

• isTypeFormerTypeCache : Std.HashMap Expr Bool

  isTypeFormerType cache

• seq : Array Element

  LCNF sequence, we chain it to create a LCNF Code object.

• toAny : FVarIdSet

  Fields that are type formers must be replaced with ◾ in the resulting code. Otherwise, we have data occurring in types. When converting a casesOn into LCNF, we add constructor fields that are types and type formers into this set. See visitCases.

@[reducible, inline]

abbrev Lean.Compiler.LCNF.ToLCNF.M (α : Type) : Type

@[inline]

def Lean.Compiler.LCNF.ToLCNF.liftMetaM {α : Type} (x : MetaM α) : M α

def Lean.Compiler.LCNF.ToLCNF.pushElement (elem : Element) : M Unit

Add LCNF element to the current sequence

def Lean.Compiler.LCNF.ToLCNF.mkUnreachable (type : Expr) : M (Arg Purity.pure)

def Lean.Compiler.LCNF.ToLCNF.mkAuxLetDecl (e : LetValue Purity.pure) (prefixName : Name := `_x) : M FVarId

def Lean.Compiler.LCNF.ToLCNF.letValueToArg (e : LetValue Purity.pure) (prefixName : Name := `_x) : M (Arg Purity.pure)

def Lean.Compiler.LCNF.ToLCNF.toCode (result : Arg Purity.pure) : M (Code Purity.pure)

Create Code that executes the current seq and then returns result

def Lean.Compiler.LCNF.ToLCNF.run {α : Type} (x : M α) : CompilerM α

def Lean.Compiler.LCNF.ToLCNF.withNewScope {α : Type} (x : M α) : M α

def Lean.Compiler.LCNF.ToLCNF.applyToAny (type : Expr) : M Expr

def Lean.Compiler.LCNF.ToLCNF.toLCNFType (type : Expr) : M Expr

def Lean.Compiler.LCNF.ToLCNF.cleanupBinderName (binderName : Name) : CompilerM Name

def Lean.Compiler.LCNF.ToLCNF.mkParam (binderName : Name) (type : Expr) : M (Param Purity.pure)

Create a new local declaration using a Lean regular type.

def Lean.Compiler.LCNF.ToLCNF.mkLetDecl (binderName : Name) (type value type' : Expr) (arg : Arg Purity.pure) (nondep : Bool) : M (LetDecl Purity.pure)

def Lean.Compiler.LCNF.ToLCNF.visitLambda (e : Expr) : M (Array (Param Purity.pure) × Expr)

def Lean.Compiler.LCNF.ToLCNF.visitBoundedLambda (e : Expr) (n : Nat) : M (Array (Param Purity.pure) × Expr)

def Lean.Compiler.LCNF.ToLCNF.mkTypeCorrectApp (e : Expr) (args : Array (Arg Purity.pure)) : M Expr

Given e and args where mkAppN e (args.map (·.toExpr)) is not necessarily well-typed (because of dependent typing), returns e.beta args' where args' are new local declarations each assigned to a value in args with adjusted type (such that the resulting expression is well-typed).

def Lean.Compiler.LCNF.ToLCNF.mustEtaExpand (env : Environment) (e : Expr) : Bool

def Lean.Compiler.LCNF.ToLCNF.etaExpandN (e : Expr) (n : Nat) : M Expr

Eta-expand with n lambdas.

partial def Lean.Compiler.LCNF.ToLCNF.etaReduceImplicit (e : Expr) : Expr

Eta reduce implicits. We use this function to eliminate introduced by the implicit lambda feature, where it generates terms such as fun {α} => ReaderT.pure

def Lean.Compiler.LCNF.ToLCNF.litToValue (lit : Literal) : LitValue

def Lean.Compiler.LCNF.ToLCNF.toLCNF (e : Expr) : CompilerM (Code Purity.pure)

Put the given expression in LCNF.

• Nested proofs are replaced with lcProof-applications.
• Eta-expand applications of declarations that satisfy shouldEtaExpand.
• Put computationally relevant expressions in A-normal form.