Common Sub-expression Elimination

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

• map : Lean.PHashMap Lean.Expr Lean.FVarId
• subst : Lean.Compiler.LCNF.FVarSubst

@[reducible, inline]

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

Equations

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

instance Lean.Compiler.LCNF.CSE.instMonadFVarSubstMFalse : Lean.Compiler.LCNF.MonadFVarSubst Lean.Compiler.LCNF.CSE.M false

Equations

• Lean.Compiler.LCNF.CSE.instMonadFVarSubstMFalse = { getSubst := do let __do_lift ← get pure __do_lift.subst }

instance Lean.Compiler.LCNF.CSE.instMonadFVarSubstStateM : Lean.Compiler.LCNF.MonadFVarSubstState Lean.Compiler.LCNF.CSE.M

Equations

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

@[inline]

def Lean.Compiler.LCNF.CSE.getSubst : Lean.Compiler.LCNF.CSE.M Lean.Compiler.LCNF.FVarSubst

Equations

• Lean.Compiler.LCNF.CSE.getSubst = do let __do_lift ← get pure __do_lift.subst

@[inline]

def Lean.Compiler.LCNF.CSE.addEntry (value : Lean.Expr) (fvarId : Lean.FVarId) : Lean.Compiler.LCNF.CSE.M Unit

Equations

• Lean.Compiler.LCNF.CSE.addEntry value fvarId = modify fun (s : Lean.Compiler.LCNF.CSE.State) => { map := Lean.PersistentHashMap.insert s.map value fvarId, subst := s.subst }

@[inline]

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

def Lean.Compiler.LCNF.CSE.replaceLet (decl : Lean.Compiler.LCNF.LetDecl) (fvarId : Lean.FVarId) : Lean.Compiler.LCNF.CSE.M Unit

def Lean.Compiler.LCNF.CSE.replaceFun (decl : Lean.Compiler.LCNF.FunDecl) (fvarId : Lean.FVarId) : Lean.Compiler.LCNF.CSE.M Unit

Equations

• Lean.Compiler.LCNF.CSE.replaceFun decl fvarId = do liftM (Lean.Compiler.LCNF.eraseFunDecl decl) Lean.Compiler.LCNF.addFVarSubst decl.fvarId fvarId

def Lean.Compiler.LCNF.Code.cse (code : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.Code

partial def Lean.Compiler.LCNF.Code.cse.goFunDecl (decl : Lean.Compiler.LCNF.FunDecl) : Lean.Compiler.LCNF.CSE.M Lean.Compiler.LCNF.FunDecl

partial def Lean.Compiler.LCNF.Code.cse.go (code : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.CSE.M Lean.Compiler.LCNF.Code

def Lean.Compiler.LCNF.Decl.cse (decl : Lean.Compiler.LCNF.Decl) : Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.Decl

Common sub-expression elimination

Equations

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

def Lean.Compiler.LCNF.cse (phase : Lean.Compiler.LCNF.Phase := Lean.Compiler.LCNF.Phase.base) (occurrence : Nat := 0) : Lean.Compiler.LCNF.Pass

Equations

• Lean.Compiler.LCNF.cse phase occurrence = Lean.Compiler.LCNF.Pass.mkPerDeclaration `cse Lean.Compiler.LCNF.Decl.cse phase occurrence