@[reducible, inline]

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

Equations

• Lean.IR.Borrow.OwnedSet.Key = (Lean.IR.FunId × Lean.IR.Index)

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

Equations

• Lean.IR.Borrow.OwnedSet.beq (f₁, x₁) (f₂, x₂) = (f₁ == f₂ && x₁ == x₂)

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

Equations

• Lean.IR.Borrow.OwnedSet.instBEqKey = { beq := Lean.IR.Borrow.OwnedSet.beq }

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

Equations

• Lean.IR.Borrow.OwnedSet.getHash (f, x_1) = mixHash (hash f) (hash x_1)

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

Equations

• Lean.IR.Borrow.OwnedSet.instHashableKey = { hash := Lean.IR.Borrow.OwnedSet.getHash }

@[reducible, inline]

abbrev Lean.IR.Borrow.OwnedSet : Type

Equations

• Lean.IR.Borrow.OwnedSet = Std.HashMap Lean.IR.Borrow.OwnedSet.Key Unit

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

Equations

• s.insert k = Std.HashMap.insert s k ()

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

Equations

• s.contains k = Std.HashMap.contains s k

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

Equations

• Lean.IR.Borrow.ParamMap.instBEqKey = { beq := Lean.IR.Borrow.ParamMap.beqKey✝ }

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

Equations

• Lean.IR.Borrow.ParamMap.getHash (Lean.IR.Borrow.ParamMap.Key.decl n) = hash n
• Lean.IR.Borrow.ParamMap.getHash (Lean.IR.Borrow.ParamMap.Key.jp n id) = mixHash (hash n) (hash id)

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

Equations

• Lean.IR.Borrow.ParamMap.instHashableKey = { hash := Lean.IR.Borrow.ParamMap.getHash }

@[reducible, inline]

abbrev Lean.IR.Borrow.ParamMap : Type

Equations

• Lean.IR.Borrow.ParamMap = Std.HashMap Lean.IR.Borrow.ParamMap.Key (Array Lean.IR.Param)

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

Equations

• One or more equations did not get rendered due to their size.

instance Lean.IR.Borrow.instToFormatParamMap : ToFormat ParamMap

Equations

• Lean.IR.Borrow.instToFormatParamMap = { format := Lean.IR.Borrow.ParamMap.fmt }

instance Lean.IR.Borrow.instToStringParamMap : ToString ParamMap

Equations

• Lean.IR.Borrow.instToStringParamMap = { toString := fun (m : Lean.IR.Borrow.ParamMap) => (Std.format m).pretty }

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

Mark parameters that take a reference as borrow

Equations

• Lean.IR.Borrow.InitParamMap.initBorrow ps = Array.map (fun (p : Lean.IR.Param) => { x := p.x, borrow := p.ty.isObj, ty := p.ty }) ps

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.

Equations

• Lean.IR.Borrow.InitParamMap.initBorrowIfNotExported exported ps = if exported = true then ps else Lean.IR.Borrow.InitParamMap.initBorrow ps

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.IR.Borrow.mkInitParamMap env decls = StateT.run' (Lean.IR.Borrow.InitParamMap.visitDecls env decls *> get) ∅

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.IR.Borrow.applyParamMap decls map = Lean.IR.Borrow.ApplyParamMap.visitDecls decls map

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

Equations

• Lean.IR.Borrow.M = ReaderT Lean.IR.Borrow.BorrowInfCtx (StateM Lean.IR.Borrow.BorrowInfState)

def Lean.IR.Borrow.getCurrFn : M FunId

Equations

• Lean.IR.Borrow.getCurrFn = do let ctx ← read pure ctx.currFn

def Lean.IR.Borrow.markModified : M Unit

Equations

• Lean.IR.Borrow.markModified = modify fun (s : Lean.IR.Borrow.BorrowInfState) => { owned := s.owned, modified := true, paramMap := s.paramMap }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.IR.Borrow.ownArg (Lean.IR.Arg.var x_2) = Lean.IR.Borrow.ownVar x_2
• Lean.IR.Borrow.ownArg x = pure ()

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

Equations

• Lean.IR.Borrow.ownArgs xs = Array.forM Lean.IR.Borrow.ownArg xs

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

Equations

• Lean.IR.Borrow.isOwned x = do let currFn ← Lean.IR.Borrow.getCurrFn let s ← get pure (s.owned.contains (currFn, x.idx))

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.IR.Borrow.collectExpr z (Lean.IR.Expr.reset n x_1) = Lean.IR.Borrow.ownVar z *> Lean.IR.Borrow.ownVar x_1
• Lean.IR.Borrow.collectExpr z (Lean.IR.Expr.reuse x_1 i updtHeader ys) = Lean.IR.Borrow.ownVar z *> Lean.IR.Borrow.ownVar x_1 *> Lean.IR.Borrow.ownArgsIfParam ys
• Lean.IR.Borrow.collectExpr z (Lean.IR.Expr.ctor i xs) = Lean.IR.Borrow.ownVar z *> Lean.IR.Borrow.ownArgsIfParam xs
• Lean.IR.Borrow.collectExpr z (Lean.IR.Expr.ap x_1 ys) = Lean.IR.Borrow.ownVar z *> Lean.IR.Borrow.ownVar x_1 *> Lean.IR.Borrow.ownArgs ys
• Lean.IR.Borrow.collectExpr z (Lean.IR.Expr.pap c xs) = Lean.IR.Borrow.ownVar z *> Lean.IR.Borrow.ownArgs xs
• Lean.IR.Borrow.collectExpr z x✝ = pure ()

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.IR.Borrow.collectDecl x✝ = pure ()

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

Equations

• Lean.IR.Borrow.collectDecls = do let __do_lift ← read Lean.IR.Borrow.whileModifing (Array.forM Lean.IR.Borrow.collectDecl __do_lift.decls) let s ← get pure s.paramMap

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

Equations

• Lean.IR.Borrow.infer env decls = StateT.run' (Lean.IR.Borrow.collectDecls { env := env, decls := decls }) { paramMap := Lean.IR.Borrow.mkInitParamMap env decls }

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

Equations

• Lean.IR.inferBorrow decls = do let env ← Lean.IR.getEnv let paramMap : Lean.IR.Borrow.ParamMap := Lean.IR.Borrow.infer env decls pure (Lean.IR.Borrow.applyParamMap decls paramMap)