Common Sub-expression Elimination

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

• map : PHashMap Expr FVarId
• subst : 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

Instances For

• Lean.Compiler.LCNF.CSE.instMonadFVarSubstMFalse
• Lean.Compiler.LCNF.CSE.instMonadFVarSubstStateM

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

Equations

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

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

Equations

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

@[inline]

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

Equations

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

@[inline]

def Lean.Compiler.LCNF.CSE.addEntry (value : Expr) (fvarId : FVarId) : 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 : M α) : M α

Equations

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

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

Equations

• Lean.Compiler.LCNF.CSE.replaceLet decl fvarId = do liftM (Lean.Compiler.LCNF.eraseLetDecl decl) Lean.Compiler.LCNF.addFVarSubst decl.fvarId fvarId

def Lean.Compiler.LCNF.CSE.replaceFun (decl : FunDecl) (fvarId : FVarId) : 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 (shouldElimFunDecls : Bool) (code : Code) : CompilerM Code

Equations

• Lean.Compiler.LCNF.Code.cse shouldElimFunDecls code = StateRefT'.run' (Lean.Compiler.LCNF.Code.cse.go shouldElimFunDecls code) { }

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

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

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

Common sub-expression elimination

Equations

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

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

Equations

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