Documentation

Lean.Compiler.LCNF.PropagateBorrow

This module contains a pass for propagating user provided borrows as far forward in the function as possible. This analysis is used to inform the reset-reuse insertion as to avoid inserting reset-reuse on values that the user explicitly requested to be borrowed.

source
inductive Lean.Compiler.LCNF.Ownedness :
Type
Instances For
    source
    def Lean.Compiler.LCNF.instInhabitedOwnedness.default :
    Ownedness
    Instances For
      source
      @[implicit_reducible]
      instance Lean.Compiler.LCNF.instInhabitedOwnedness :
      Inhabited Ownedness
      source
      @[implicit_reducible]
      instance Lean.Compiler.LCNF.instBEqOwnedness :
      BEq Ownedness
      source
      def Lean.Compiler.LCNF.instBEqOwnedness.beq :
      Ownedness → Ownedness → Bool
      Instances For
        source
        def Lean.Compiler.LCNF.Decl.analyzePropagatedBorrows (decl : Decl Purity.impure) :
        CompilerM (Std.HashMap FVarId Ownedness)
        Instances For
          source
          def Lean.Compiler.LCNF.Decl.applyOwnedness (decl : Decl Purity.impure) (values : Std.HashMap FVarId Ownedness) :
          CompilerM (Decl Purity.impure)
          Instances For