Documentation

Lean.Compiler.LCNF.CSE

Common Sub-expression Elimination

source
structure Lean.Compiler.LCNF.CSE.State :
Type
Instances For
    source
    @[reducible, inline]
    abbrev Lean.Compiler.LCNF.CSE.M (α : Type) :
    Type
    Equations
      Instances For
        source
        instance Lean.Compiler.LCNF.CSE.instMonadFVarSubstMFalse :
        MonadFVarSubst M false
        Equations
          source
          instance Lean.Compiler.LCNF.CSE.instMonadFVarSubstStateM :
          MonadFVarSubstState M
          Equations
            source
            @[inline]
            def Lean.Compiler.LCNF.CSE.getSubst :
            M FVarSubst
            Equations
              Instances For
                source
                @[inline]
                def Lean.Compiler.LCNF.CSE.addEntry (value : Expr) (fvarId : FVarId) :
                M Unit
                Equations
                  Instances For
                    source
                    @[inline]
                    def Lean.Compiler.LCNF.CSE.withNewScope {α : Type} (x : M α) :
                    M α
                    Equations
                      Instances For
                        source
                        def Lean.Compiler.LCNF.CSE.replaceLet (decl : LetDecl) (fvarId : FVarId) :
                        M Unit
                        Equations
                          Instances For
                            source
                            def Lean.Compiler.LCNF.CSE.replaceFun (decl : FunDecl) (fvarId : FVarId) :
                            M Unit
                            Equations
                              Instances For
                                source
                                def Lean.Compiler.LCNF.CSE.hasNeverExtract (v : LetValue) :
                                CompilerM Bool
                                Equations
                                  Instances For
                                    source
                                    def Lean.Compiler.LCNF.Code.cse (shouldElimFunDecls : Bool) (code : Code) :
                                    CompilerM Code
                                    Equations
                                      Instances For
                                        source
                                        partial def Lean.Compiler.LCNF.Code.cse.goFunDecl (shouldElimFunDecls : Bool) (decl : FunDecl) :
                                        CSE.M FunDecl
                                        source
                                        partial def Lean.Compiler.LCNF.Code.cse.go (shouldElimFunDecls : Bool) (code : Code) :
                                        CSE.M Code
                                        source
                                        def Lean.Compiler.LCNF.Decl.cse (shouldElimFunDecls : Bool) (decl : Decl) :
                                        CompilerM Decl

                                        Common sub-expression elimination

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