Lean.Compiler.IR.Borrow

source

@[inline]

abbrev Lean.IR.Borrow.OwnedSet.Key:

Type

Equations

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

source

def Lean.IR.Borrow.OwnedSet.beq:

Lean.IR.Borrow.OwnedSet.Key → Lean.IR.Borrow.OwnedSet.Key → Bool

Equations

Lean.IR.Borrow.OwnedSet.beq _fun_discr _fun_discr = match _fun_discr, _fun_discr with | (f₁, x₁), (f₂, x₂) => f₁ == f₂ && x₁ == x₂

source

instance Lean.IR.Borrow.OwnedSet.instBEqKey:

BEq Lean.IR.Borrow.OwnedSet.Key

Equations

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

source

def Lean.IR.Borrow.OwnedSet.getHash:

Lean.IR.Borrow.OwnedSet.Key → UInt64

Equations

Lean.IR.Borrow.OwnedSet.getHash _fun_discr = match _fun_discr with | (f, x) => mixHash (hash f) (hash x)

source

instance Lean.IR.Borrow.OwnedSet.instHashableKey:

Hashable Lean.IR.Borrow.OwnedSet.Key

Equations

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

source

@[inline]

abbrev Lean.IR.Borrow.OwnedSet:

Type

Equations

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

source

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

Lean.IR.Borrow.OwnedSet

Equations

Lean.IR.Borrow.OwnedSet.insert s k = Std.HashMap.insert s k ()

source

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

Bool

Equations

Lean.IR.Borrow.OwnedSet.contains s k = Std.HashMap.contains s k

source

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

source

instance Lean.IR.Borrow.ParamMap.instBEqKey:

BEq Lean.IR.Borrow.ParamMap.Key

Equations

Lean.IR.Borrow.ParamMap.instBEqKey = { beq := [anonymous] }

source

def Lean.IR.Borrow.ParamMap.getHash:

Lean.IR.Borrow.ParamMap.Key → UInt64

Equations

Lean.IR.Borrow.ParamMap.getHash _fun_discr = match _fun_discr with | Lean.IR.Borrow.ParamMap.Key.decl n => hash n | Lean.IR.Borrow.ParamMap.Key.jp n id => mixHash (hash n) (hash id)

source

instance Lean.IR.Borrow.ParamMap.instHashableKey:

Hashable Lean.IR.Borrow.ParamMap.Key

Equations

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

source

@[inline]

abbrev Lean.IR.Borrow.ParamMap:

Type

Equations

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

source

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.

source

instance Lean.IR.Borrow.instToFormatParamMap:

Lean.ToFormat Lean.IR.Borrow.ParamMap

Equations

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

source

instance Lean.IR.Borrow.instToStringParamMap:

ToString Lean.IR.Borrow.ParamMap

Equations

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

source

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

Array Lean.IR.Param

Equations

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

source

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

Array Lean.IR.Param

Equations

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

source

partial def Lean.IR.Borrow.InitParamMap.visitFnBody (fnid : Lean.IR.FunId) :

Lean.IR.FnBody → StateM Lean.IR.Borrow.ParamMap Unit

source

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.

source

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' (SeqRight.seqRight (Lean.IR.Borrow.InitParamMap.visitDecls env decls) fun x => get) ∅

source

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

Lean.IR.FnBody → Lean.IR.FnBody

source

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.

source

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

source

structure Lean.IR.Borrow.BorrowInfCtx:

Type

source

structure Lean.IR.Borrow.BorrowInfState:

Type

source

@[inline]

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

Type

Equations

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

source

def Lean.IR.Borrow.getCurrFn:

Lean.IR.Borrow.M Lean.IR.FunId

Equations

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

source

def Lean.IR.Borrow.markModified:

Lean.IR.Borrow.M Unit

Equations

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

source

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.

source

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

Lean.IR.Borrow.M Unit

Equations

Lean.IR.Borrow.ownArg x = match x with | Lean.IR.Arg.var x => Lean.IR.Borrow.ownVar x | x => pure ()

source

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 0 (Array.size xs)

source

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 (Lean.IR.Borrow.OwnedSet.contains s.owned (currFn, x.idx))

source

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

Lean.IR.Borrow.M Unit

Equations

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

source

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.

source

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

Lean.IR.Borrow.M Unit

Equations

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

source

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

Lean.IR.Borrow.M Unit

Equations

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

source

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

Lean.IR.Borrow.M Unit

Equations

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

source

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.

source

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.

source

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.

source

partial def Lean.IR.Borrow.collectFnBody:

Lean.IR.FnBody → Lean.IR.Borrow.M Unit

source

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.

source

@[inline]

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

Lean.IR.Borrow.M Unit

source

def Lean.IR.Borrow.collectDecls:

Lean.IR.Borrow.M Lean.IR.Borrow.ParamMap

Equations

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

source

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.

source

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)