Documentation

Lean.Compiler.LCNF.CSE

Common Sub-expression Elimination

structure Lean.Compiler.LCNF.CSE.State :

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

Instances For

@[inline]

abbrev Lean.Compiler.LCNF.CSE.M (α : 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

Lean.Compiler.LCNF.CSE.instMonadFVarSubstStateM = { modifySubst := fun f => modify fun s => { map := s.map, subst := f s.subst } }

@[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 => { 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 α

Equations

Lean.Compiler.LCNF.CSE.withNewScope x = do let __do_lift ← get let map : Lean.PHashMap Lean.Expr Lean.FVarId := __do_lift.map tryFinally x (modify fun s => { map := map, subst := s.subst })

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

Lean.Compiler.LCNF.CSE.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 : 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 true) 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

Equations

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

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 : optParam Lean.Compiler.LCNF.Phase Lean.Compiler.LCNF.Phase.base) (occurrence : optParam 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