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
    Instances For
      source
      @[implicit_reducible]
      instance Lean.Compiler.LCNF.CSE.instMonadFVarSubstMPureFalse :
      MonadFVarSubst M Purity.pure false
      source
      @[implicit_reducible]
      instance Lean.Compiler.LCNF.CSE.instMonadFVarSubstStateMPure :
      MonadFVarSubstState M Purity.pure
      source
      @[inline]
      def Lean.Compiler.LCNF.CSE.getSubst :
      M (FVarSubst Purity.pure)
      Instances For
        source
        @[inline]
        def Lean.Compiler.LCNF.CSE.addEntry (value : Expr) (fvarId : FVarId) :
        M Unit
        Instances For
          source
          @[inline]
          def Lean.Compiler.LCNF.CSE.withNewScope {α : Type} (x : M α) :
          M α
          Instances For
            source
            def Lean.Compiler.LCNF.CSE.replaceLet (decl : LetDecl Purity.pure) (fvarId : FVarId) :
            M Unit
            Instances For
              source
              def Lean.Compiler.LCNF.CSE.replaceFun (decl : FunDecl Purity.pure) (fvarId : FVarId) :
              M Unit
              Instances For
                source
                def Lean.Compiler.LCNF.CSE.hasNeverExtract (v : LetValue Purity.pure) :
                CompilerM Bool
                Instances For
                  source
                  def Lean.Compiler.LCNF.Code.cse (shouldElimFunDecls : Bool) (code : Code Purity.pure) :
                  CompilerM (Code Purity.pure)
                  Instances For
                    source
                    def Lean.Compiler.LCNF.Decl.cse (shouldElimFunDecls : Bool) (decl : Decl Purity.pure) :
                    CompilerM (Decl Purity.pure)

                    Common sub-expression elimination

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