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

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

Equations

• Lean.Compiler.LCNF.ToLCNF.isLCProof e = Lean.Expr.isAppOfArity e `lcProof 1

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

Create the temporary lcProof

Equations

• Lean.Compiler.LCNF.ToLCNF.mkLcProof p = Lean.mkApp (Lean.mkConst `lcProof) p

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

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

Equations

• Lean.Compiler.LCNF.ToLCNF.instInhabitedElement = { default := Lean.Compiler.LCNF.ToLCNF.Element.jp default }

@[inline, reducible]

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

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

Equations

• Lean.Compiler.LCNF.ToLCNF.BindCasesM.State = Lean.FVarIdMap Lean.Compiler.LCNF.FunDecl

@[inline, reducible]

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

Auxiliary monad for implementing bindCases

Equations

• Lean.Compiler.LCNF.ToLCNF.BindCasesM = StateRefT' IO.RealWorld Lean.Compiler.LCNF.ToLCNF.BindCasesM.State Lean.Compiler.LCNF.CompilerM

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

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.

Equations

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

def Lean.Compiler.LCNF.ToLCNF.bindCases.visitAlts (jpDecl : Lean.Compiler.LCNF.FunDecl) (alts : Array Lean.Compiler.LCNF.Alt) : Lean.Compiler.LCNF.ToLCNF.BindCasesM (Array Lean.Compiler.LCNF.Alt)

Equations

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

partial def Lean.Compiler.LCNF.ToLCNF.bindCases.findFun? (f : Lean.FVarId) : Lean.Compiler.LCNF.CompilerM (Option Lean.Compiler.LCNF.FunDecl)

partial def Lean.Compiler.LCNF.ToLCNF.bindCases.go (jpDecl : Lean.Compiler.LCNF.FunDecl) (code : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.ToLCNF.BindCasesM Lean.Compiler.LCNF.Code

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

Equations

• Lean.Compiler.LCNF.ToLCNF.seqToCode seq k = Lean.Compiler.LCNF.ToLCNF.seqToCode.go seq (Array.size seq) k

def Lean.Compiler.LCNF.ToLCNF.seqToCode.go (seq : Array Lean.Compiler.LCNF.ToLCNF.Element) (i : Nat) (c : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.Code

Equations

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

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

• lctx : Lean.LocalContext

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

• cache : Lean.PHashMap Lean.Expr Lean.Compiler.LCNF.Arg

  Cache from Lean regular expression to LCNF argument.

• typeCache : Lean.HashMap Lean.Expr Lean.Expr

  toLCNFType cache

• isTypeFormerTypeCache : Lean.HashMap Lean.Expr Bool

  isTypeFormerType cache

• seq : Array Lean.Compiler.LCNF.ToLCNF.Element

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

• 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 casesOn into LCNF, we add constructor fields that are types and type formers into this set. See visitCases.

@[inline, reducible]

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

Equations

• Lean.Compiler.LCNF.ToLCNF.M = StateRefT' IO.RealWorld Lean.Compiler.LCNF.ToLCNF.State Lean.Compiler.LCNF.CompilerM

@[inline]

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

Equations

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

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

Add LCNF element to the current sequence

Equations

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

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

Equations

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

def Lean.Compiler.LCNF.ToLCNF.mkAuxLetDecl (e : Lean.Compiler.LCNF.LetValue) (prefixName : optParam Lake.Name `_x) : Lean.Compiler.LCNF.ToLCNF.M Lean.FVarId

Equations

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

def Lean.Compiler.LCNF.ToLCNF.letValueToArg (e : Lean.Compiler.LCNF.LetValue) (prefixName : optParam Lake.Name `_x) : Lean.Compiler.LCNF.ToLCNF.M Lean.Compiler.LCNF.Arg

Equations

• Lean.Compiler.LCNF.ToLCNF.letValueToArg e prefixName = do let __do_lift ← Lean.Compiler.LCNF.ToLCNF.mkAuxLetDecl e prefixName pure (Lean.Compiler.LCNF.Arg.fvar __do_lift)

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

Create Code that executes the current seq and then returns result

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Create a new local declaration using a Lean regular type.

Equations

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

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

Equations

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

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

Equations

• Lean.Compiler.LCNF.ToLCNF.visitLambda e = Lean.Compiler.LCNF.ToLCNF.visitLambda.go e #[] #[]

def Lean.Compiler.LCNF.ToLCNF.visitLambda.go (e : Lean.Expr) (xs : Array Lean.Expr) (ps : Array Lean.Compiler.LCNF.Param) : Lean.Compiler.LCNF.ToLCNF.M (Array Lean.Compiler.LCNF.Param × Lean.Expr)

Equations

• One or more equations did not get rendered due to their size.
• Lean.Compiler.LCNF.ToLCNF.visitLambda.go e xs ps = pure (ps, Lean.Expr.instantiateRev e xs)

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

Equations

• Lean.Compiler.LCNF.ToLCNF.visitBoundedLambda e n = Lean.Compiler.LCNF.ToLCNF.visitBoundedLambda.go e n #[] #[]

def Lean.Compiler.LCNF.ToLCNF.visitBoundedLambda.go (e : Lean.Expr) (n : Nat) (xs : Array Lean.Expr) (ps : Array Lean.Compiler.LCNF.Param) : Lean.Compiler.LCNF.ToLCNF.M (Array Lean.Compiler.LCNF.Param × Lean.Expr)

Equations

• One or more equations did not get rendered due to their size.
• Lean.Compiler.LCNF.ToLCNF.visitBoundedLambda.go e n xs ps = if (n == 0) = true then pure (ps, Lean.Expr.instantiateRev e xs) else pure (ps, Lean.Expr.instantiateRev e xs)

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

Equations

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

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

Eta-expand with n lambdas.

Equations

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

partial def Lean.Compiler.LCNF.ToLCNF.etaReduceImplicit (e : Lean.Expr) : Lean.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 : Lean.Literal) : Lean.Compiler.LCNF.LitValue

Equations

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

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

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.

Equations

• Lean.Compiler.LCNF.toLCNF e = Lean.Compiler.LCNF.ToLCNF.run do let __do_lift ← Lean.Compiler.LCNF.ToLCNF.toLCNF.visit e Lean.Compiler.LCNF.ToLCNF.toCode __do_lift

partial def Lean.Compiler.LCNF.ToLCNF.toLCNF.visitCore (e : Lean.Expr) : Lean.Compiler.LCNF.ToLCNF.M Lean.Compiler.LCNF.Arg

partial def Lean.Compiler.LCNF.ToLCNF.toLCNF.visit (e : Lean.Expr) : Lean.Compiler.LCNF.ToLCNF.M Lean.Compiler.LCNF.Arg

def Lean.Compiler.LCNF.ToLCNF.toLCNF.visitLit (lit : Lean.Literal) : Lean.Compiler.LCNF.ToLCNF.M Lean.Compiler.LCNF.Arg

Equations

• Lean.Compiler.LCNF.ToLCNF.toLCNF.visitLit lit = Lean.Compiler.LCNF.ToLCNF.letValueToArg (Lean.Compiler.LCNF.LetValue.value (Lean.Compiler.LCNF.ToLCNF.litToValue lit))

partial def Lean.Compiler.LCNF.ToLCNF.toLCNF.visitAppArg (e : Lean.Expr) : Lean.Compiler.LCNF.ToLCNF.M Lean.Compiler.LCNF.Arg

partial def Lean.Compiler.LCNF.ToLCNF.toLCNF.visitAppDefaultConst (f : Lean.Expr) (args : Array Lean.Expr) : Lean.Compiler.LCNF.ToLCNF.M Lean.Compiler.LCNF.Arg

Giving f a constant .const declName us, convert args into args', and return .const declName us args'

partial def Lean.Compiler.LCNF.ToLCNF.toLCNF.etaIfUnderApplied (e : Lean.Expr) (arity : Nat) (k : Lean.Compiler.LCNF.ToLCNF.M Lean.Compiler.LCNF.Arg) : Lean.Compiler.LCNF.ToLCNF.M Lean.Compiler.LCNF.Arg

Eta expand if under applied, otherwise apply k

partial def Lean.Compiler.LCNF.ToLCNF.toLCNF.mkOverApplication (app : Lean.Compiler.LCNF.Arg) (args : Array Lean.Expr) (arity : Nat) : Lean.Compiler.LCNF.ToLCNF.M Lean.Compiler.LCNF.Arg

If args.size == arity, then just return app. Otherwise return

let k := app
k args[arity:]

partial def Lean.Compiler.LCNF.ToLCNF.toLCNF.visitAlt (ctorName : Lake.Name) (numParams : Nat) (e : Lean.Expr) : Lean.Compiler.LCNF.ToLCNF.M (Lean.Expr × Lean.Compiler.LCNF.Alt)

Visit a matcher/casesOn alternative.

partial def Lean.Compiler.LCNF.ToLCNF.toLCNF.visitCases (casesInfo : Lean.Compiler.LCNF.CasesInfo) (e : Lean.Expr) : Lean.Compiler.LCNF.ToLCNF.M Lean.Compiler.LCNF.Arg

partial def Lean.Compiler.LCNF.ToLCNF.toLCNF.visitCtor (arity : Nat) (e : Lean.Expr) : Lean.Compiler.LCNF.ToLCNF.M Lean.Compiler.LCNF.Arg

partial def Lean.Compiler.LCNF.ToLCNF.toLCNF.visitQuotLift (e : Lean.Expr) : Lean.Compiler.LCNF.ToLCNF.M Lean.Compiler.LCNF.Arg

partial def Lean.Compiler.LCNF.ToLCNF.toLCNF.visitEqRec (e : Lean.Expr) : Lean.Compiler.LCNF.ToLCNF.M Lean.Compiler.LCNF.Arg

partial def Lean.Compiler.LCNF.ToLCNF.toLCNF.visitFalseRec (e : Lean.Expr) : Lean.Compiler.LCNF.ToLCNF.M Lean.Compiler.LCNF.Arg

partial def Lean.Compiler.LCNF.ToLCNF.toLCNF.visitAndIffRecCore (e : Lean.Expr) (minorPos : Nat) : Lean.Compiler.LCNF.ToLCNF.M Lean.Compiler.LCNF.Arg

partial def Lean.Compiler.LCNF.ToLCNF.toLCNF.visitNoConfusion (e : Lean.Expr) : Lean.Compiler.LCNF.ToLCNF.M Lean.Compiler.LCNF.Arg

partial def Lean.Compiler.LCNF.ToLCNF.toLCNF.expandNoConfusionMajor (major : Lean.Expr) (numFields : Nat) : Lean.Compiler.LCNF.ToLCNF.M Lean.Expr

partial def Lean.Compiler.LCNF.ToLCNF.toLCNF.visitProjFn (projInfo : Lean.ProjectionFunctionInfo) (e : Lean.Expr) : Lean.Compiler.LCNF.ToLCNF.M Lean.Compiler.LCNF.Arg

partial def Lean.Compiler.LCNF.ToLCNF.toLCNF.visitApp (e : Lean.Expr) : Lean.Compiler.LCNF.ToLCNF.M Lean.Compiler.LCNF.Arg

partial def Lean.Compiler.LCNF.ToLCNF.toLCNF.visitLambda (e : Lean.Expr) : Lean.Compiler.LCNF.ToLCNF.M Lean.Compiler.LCNF.Arg

partial def Lean.Compiler.LCNF.ToLCNF.toLCNF.visitMData (_mdata : Lean.MData) (e : Lean.Expr) : Lean.Compiler.LCNF.ToLCNF.M Lean.Compiler.LCNF.Arg

partial def Lean.Compiler.LCNF.ToLCNF.toLCNF.visitProj (s : Lake.Name) (i : Nat) (e : Lean.Expr) : Lean.Compiler.LCNF.ToLCNF.M Lean.Compiler.LCNF.Arg

partial def Lean.Compiler.LCNF.ToLCNF.toLCNF.visitLet (e : Lean.Expr) (xs : Array Lean.Expr) : Lean.Compiler.LCNF.ToLCNF.M Lean.Compiler.LCNF.Arg