Lean.Compiler.LCNF.CSE

Common Sub-expression Elimination

source

structure Lean.Compiler.LCNF.CSE.State :

Type

map : PHashMap Expr FVarId
subst : FVarSubst Purity.pure

Instances For

source

@[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

source

@[implicit_reducible]

instance Lean.Compiler.LCNF.CSE.instMonadFVarSubstMPureFalse :

MonadFVarSubst M Purity.pure false

Equations

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

source

@[implicit_reducible]

instance Lean.Compiler.LCNF.CSE.instMonadFVarSubstStateMPure :

MonadFVarSubstState M Purity.pure

Equations

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

source

@[inline]

def Lean.Compiler.LCNF.CSE.getSubst :

M (FVarSubst Purity.pure)

Equations

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

Instances For

source

@[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 }

Instances For

source

@[inline]

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

M α

Equations

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

Instances For

source

def Lean.Compiler.LCNF.CSE.replaceLet (decl : LetDecl Purity.pure) (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

Instances For

source

def Lean.Compiler.LCNF.CSE.replaceFun (decl : FunDecl Purity.pure) (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

Instances For

source

def Lean.Compiler.LCNF.CSE.hasNeverExtract (v : LetValue Purity.pure) :

CompilerM Bool

Equations

Lean.Compiler.LCNF.CSE.hasNeverExtract (Lean.Compiler.LCNF.LetValue.const declName us args h) = do let __do_lift ← Lean.getEnv pure (Lean.hasNeverExtractAttribute __do_lift declName)
Lean.Compiler.LCNF.CSE.hasNeverExtract (Lean.Compiler.LCNF.LetValue.lit value) = pure false
Lean.Compiler.LCNF.CSE.hasNeverExtract Lean.Compiler.LCNF.LetValue.erased = pure false
Lean.Compiler.LCNF.CSE.hasNeverExtract (Lean.Compiler.LCNF.LetValue.proj typeName idx struct h) = pure false
Lean.Compiler.LCNF.CSE.hasNeverExtract (Lean.Compiler.LCNF.LetValue.fvar fvarId args) = pure false

Instances For

source

def Lean.Compiler.LCNF.Code.cse (shouldElimFunDecls : Bool) (code : Code Purity.pure) :

CompilerM (Code Purity.pure)

Equations

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

Instances For

source

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

CompilerM (Decl Purity.pure)

Common sub-expression elimination

Equations

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

Instances For

source

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

Pass

Equations

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

Instances For