@[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 : Lean.IR.Borrow.OwnedSet.Key → Lean.IR.Borrow.OwnedSet.Key → Bool

Equations

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

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

Equations

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

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

Equations

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

instance Lean.IR.Borrow.OwnedSet.instHashableKey : Hashable Lean.IR.Borrow.OwnedSet.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 : Lean.IR.Borrow.OwnedSet) (k : Lean.IR.Borrow.OwnedSet.Key) : Lean.IR.Borrow.OwnedSet

Equations

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

def Lean.IR.Borrow.OwnedSet.contains (s : Lean.IR.Borrow.OwnedSet) (k : Lean.IR.Borrow.OwnedSet.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: 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

Equations

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

def Lean.IR.Borrow.ParamMap.getHash : Lean.IR.Borrow.ParamMap.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 Lean.IR.Borrow.ParamMap.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 : Lean.IR.Borrow.ParamMap) : Lean.Format

Equations

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

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

Equations

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

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

Equations

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

def Lean.IR.Borrow.InitParamMap.initBorrow (ps : Array Lean.IR.Param) : Array Lean.IR.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 Lean.IR.Param) : Array Lean.IR.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 : 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

Equations

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

def Lean.IR.Borrow.mkInitParamMap (env : Lean.Environment) (decls : Array Lean.IR.Decl) : Lean.IR.Borrow.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 : 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

Equations

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

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

Equations

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

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

@[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 : Lean.IR.Borrow.M Lean.IR.FunId

Equations

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

def Lean.IR.Borrow.markModified : Lean.IR.Borrow.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 : Lean.IR.VarId) : Lean.IR.Borrow.M Unit

Equations

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

def Lean.IR.Borrow.ownArg (x : Lean.IR.Arg) : Lean.IR.Borrow.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 Lean.IR.Arg) : Lean.IR.Borrow.M Unit

Equations

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

def Lean.IR.Borrow.isOwned (x : Lean.IR.VarId) : Lean.IR.Borrow.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 : Lean.IR.Borrow.ParamMap.Key) : Lean.IR.Borrow.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 : Lean.IR.Borrow.ParamMap.Key) : Lean.IR.Borrow.M (Array Lean.IR.Param)

Equations

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

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.

Equations

• Lean.IR.Borrow.ownArgsUsingParams xs ps = xs.size.forM fun (i : Nat) => let x := xs[i]!; let p := ps[i]!; if p.borrow = true then pure PUnit.unit else Lean.IR.Borrow.ownArg x

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.

Equations

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

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

Equations

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

def Lean.IR.Borrow.collectExpr (z : Lean.IR.VarId) : Lean.IR.Expr → Lean.IR.Borrow.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 : Lean.IR.VarId) (v : Lean.IR.Expr) (b : Lean.IR.FnBody) : Lean.IR.Borrow.M Unit

Equations

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

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

Equations

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

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

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 : 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

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 : Lean.Environment) (decls : Array Lean.IR.Decl) : Lean.IR.Borrow.ParamMap

Equations

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

def Lean.IR.inferBorrow (decls : Array Lean.IR.Decl) : Lean.IR.CompilerM (Array Lean.IR.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)