Documentation

Lean.Compiler.LCNF.CSE

Common Sub-expression Elimination

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

                  Common sub-expression elimination

                  Instances For
                    source
                    def Lean.Compiler.LCNF.cse (phase : optParam Lean.Compiler.LCNF.Phase Lean.Compiler.LCNF.Phase.base) (occurrence : optParam Nat 0) :
                    Lean.Compiler.LCNF.Pass
                    Instances For