@[reducible, inline]

abbrev Lean.IR.Borrow.OwnedSet.Key : Type

def Lean.IR.Borrow.OwnedSet.beq : Key → Key → Bool

instance Lean.IR.Borrow.OwnedSet.instBEqKey : BEq Key

def Lean.IR.Borrow.OwnedSet.getHash : Key → UInt64

instance Lean.IR.Borrow.OwnedSet.instHashableKey : Hashable Key

@[reducible, inline]

abbrev Lean.IR.Borrow.OwnedSet : Type

def Lean.IR.Borrow.OwnedSet.insert (s : OwnedSet) (k : Key) : OwnedSet

def Lean.IR.Borrow.OwnedSet.contains (s : OwnedSet) (k : Key) : Bool

We perform borrow inference in a block of mutually recursive functions. Join points are viewed as local functions, and are identified using their local id + the name of the surrounding function. We keep a mapping from function and joint points to parameters (Array Param). Recall that Param contains the field borrow.

inductive Lean.IR.Borrow.ParamMap.Key : Type

• decl (name : FunId) : Key
• jp (name : FunId) (jpid : JoinPointId) : Key

instance Lean.IR.Borrow.ParamMap.instBEqKey : BEq Key

def Lean.IR.Borrow.ParamMap.getHash : Key → UInt64

instance Lean.IR.Borrow.ParamMap.instHashableKey : Hashable Key

@[reducible, inline]

abbrev Lean.IR.Borrow.ParamMap : Type

def Lean.IR.Borrow.ParamMap.fmt (map : ParamMap) : Format

instance Lean.IR.Borrow.instToFormatParamMap : ToFormat ParamMap

instance Lean.IR.Borrow.instToStringParamMap : ToString ParamMap

def Lean.IR.Borrow.InitParamMap.initBorrow (ps : Array Param) : Array Param

Mark parameters that take a reference as borrow

def Lean.IR.Borrow.InitParamMap.initBorrowIfNotExported (exported : Bool) (ps : Array Param) : Array Param

We do not perform borrow inference for constants marked as export. Reason: we current write wrappers in C++ for using exported functions. These wrappers use smart pointers such as object_ref. When writing a new wrapper we need to know whether an argument is a borrow inference or not. We can revise this decision when we implement code for generating the wrappers automatically.

partial def Lean.IR.Borrow.InitParamMap.visitFnBody (fnid : FunId) : FnBody → StateM ParamMap Unit

def Lean.IR.Borrow.InitParamMap.visitDecls (env : Environment) (decls : Array Decl) : StateM ParamMap Unit

def Lean.IR.Borrow.mkInitParamMap (env : Environment) (decls : Array Decl) : ParamMap

Apply the inferred borrow annotations stored at ParamMap to a block of mutually recursive functions.

partial def Lean.IR.Borrow.ApplyParamMap.visitFnBody (fn : FunId) (paramMap : ParamMap) : FnBody → FnBody

def Lean.IR.Borrow.ApplyParamMap.visitDecls (decls : Array Decl) (paramMap : ParamMap) : Array Decl

def Lean.IR.Borrow.applyParamMap (decls : Array Decl) (map : ParamMap) : Array Decl

structure Lean.IR.Borrow.BorrowInfCtx : Type

• env : Environment
• decls : Array Decl
• currFn : FunId
• paramSet : IndexSet

structure Lean.IR.Borrow.BorrowInfState : Type

• owned : OwnedSet

  Set of variables that must be owned.

• modified : Bool
• paramMap : ParamMap

@[reducible, inline]

abbrev Lean.IR.Borrow.M (α : Type) : Type

def Lean.IR.Borrow.getCurrFn : M FunId

def Lean.IR.Borrow.markModified : M Unit

def Lean.IR.Borrow.ownVar (x : VarId) : M Unit

def Lean.IR.Borrow.ownArg (x : Arg) : M Unit

def Lean.IR.Borrow.ownArgs (xs : Array Arg) : M Unit

def Lean.IR.Borrow.isOwned (x : VarId) : M Bool

def Lean.IR.Borrow.updateParamMap (k : ParamMap.Key) : M Unit

Updates map[k] using the current set of owned variables.

def Lean.IR.Borrow.getParamInfo (k : ParamMap.Key) : M (Array Param)

def Lean.IR.Borrow.ownArgsUsingParams (xs : Array Arg) (ps : Array Param) : M Unit

For each ps[i], if ps[i] is owned, then mark xs[i] as owned.

def Lean.IR.Borrow.ownParamsUsingArgs (xs : Array Arg) (ps : Array Param) : M Unit

For each xs[i], if xs[i] is owned, then mark ps[i] as owned. We use this action to preserve tail calls. That is, if we have a tail call f xs, if the i-th parameter is borrowed, but xs[i] is owned we would have to insert a dec xs[i] after f xs and consequently "break" the tail call.

def Lean.IR.Borrow.ownArgsIfParam (xs : Array Arg) : M Unit

Mark xs[i] as owned if it is one of the parameters ps. We use this action to mark function parameters that are being "packed" inside constructors. This is a heuristic, and is not related with the effectiveness of the reset/reuse optimization. It is useful for code such as

def f (x y : obj) :=
let z := ctor_1 x y;
ret z

def Lean.IR.Borrow.collectExpr (z : VarId) : Expr → M Unit

def Lean.IR.Borrow.preserveTailCall (x : VarId) (v : Expr) (b : FnBody) : M Unit

def Lean.IR.Borrow.updateParamSet (ctx : BorrowInfCtx) (ps : Array Param) : BorrowInfCtx

partial def Lean.IR.Borrow.collectFnBody : FnBody → M Unit

def Lean.IR.Borrow.collectDecl : Decl → M Unit

partial def Lean.IR.Borrow.whileModifing (x : M Unit) : M Unit

Keep executing x until it reaches a fixpoint

def Lean.IR.Borrow.collectDecls : M ParamMap

def Lean.IR.Borrow.infer (env : Environment) (decls : Array Decl) : ParamMap

def Lean.IR.inferBorrow (decls : Array Decl) : CompilerM (Array Decl)