@[inline, reducible]

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

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

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

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

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

@[inline, reducible]

abbrev Lean.IR.Borrow.OwnedSet : Type

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

def Lean.IR.Borrow.OwnedSet.contains (s : Lean.IR.Borrow.OwnedSet) (k : Lean.IR.Borrow.OwnedSet.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: Lean.IR.FunId → Lean.IR.Borrow.ParamMap.Key
• jp: Lean.IR.FunId → Lean.IR.JoinPointId → Lean.IR.Borrow.ParamMap.Key

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

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

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

@[inline, reducible]

abbrev Lean.IR.Borrow.ParamMap : Type

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

instance Lean.IR.Borrow.instToFormatParamMap : Lean.ToFormat Lean.IR.Borrow.ParamMap

instance Lean.IR.Borrow.instToStringParamMap : ToString Lean.IR.Borrow.ParamMap

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

Mark parameters that take a reference as borrow

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

We do 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 : Lean.IR.FunId) : Lean.IR.FnBody → StateM Lean.IR.Borrow.ParamMap Unit

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

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

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

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

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

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

structure Lean.IR.Borrow.BorrowInfCtx : Type

• env : Lean.Environment
• decls : Array Lean.IR.Decl
• currFn : Lean.IR.FunId
• paramSet : Lean.IR.IndexSet

structure Lean.IR.Borrow.BorrowInfState : Type

• owned : Lean.IR.Borrow.OwnedSet

  Set of variables that must be owned.

• modified : Bool
• paramMap : Lean.IR.Borrow.ParamMap

@[inline, reducible]

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

def Lean.IR.Borrow.getCurrFn : Lean.IR.Borrow.M Lean.IR.FunId

def Lean.IR.Borrow.markModified : Lean.IR.Borrow.M Unit

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

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

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

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

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

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

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

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

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

def Lean.IR.Borrow.ownParamsUsingArgs (xs : Array Lean.IR.Arg) (ps : Array Lean.IR.Param) : Lean.IR.Borrow.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 Lean.IR.Arg) : Lean.IR.Borrow.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 : Lean.IR.VarId) : Lean.IR.Expr → Lean.IR.Borrow.M Unit

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

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

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

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

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

Keep executing x until it reaches a fixpoint

def Lean.IR.Borrow.collectDecls : Lean.IR.Borrow.M Lean.IR.Borrow.ParamMap

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

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