Lean.Compiler.IR.RC

Lean.IR.ExplicitRC.getDecl ctx fid = match Lean.IR.findEnvDecl' ctx.env fid ctx.decls with | some decl => decl | none => panicWithPosWithDecl "Lean.Compiler.IR.RC" "Lean.IR.ExplicitRC.getDecl" 34 17 "unreachable code has been reached"

source

def Lean.IR.ExplicitRC.getVarInfo (ctx : Lean.IR.ExplicitRC.Context) (x : Lean.IR.VarId) :

Lean.IR.ExplicitRC.VarInfo

Equations

Lean.IR.ExplicitRC.getVarInfo ctx x = match Std.RBMap.find? ctx.varMap x with | some info => info | none => panicWithPosWithDecl "Lean.Compiler.IR.RC" "Lean.IR.ExplicitRC.getVarInfo" 39 17 "unreachable code has been reached"

source

def Lean.IR.ExplicitRC.getJPParams (ctx : Lean.IR.ExplicitRC.Context) (j : Lean.IR.JoinPointId) :

Array Lean.IR.Param

Equations

Lean.IR.ExplicitRC.getJPParams ctx j = match Lean.IR.LocalContext.getJPParams ctx.localCtx j with | some ps => ps | none => panicWithPosWithDecl "Lean.Compiler.IR.RC" "Lean.IR.ExplicitRC.getJPParams" 44 15 "unreachable code has been reached"

source

def Lean.IR.ExplicitRC.getJPLiveVars (ctx : Lean.IR.ExplicitRC.Context) (j : Lean.IR.JoinPointId) :

Lean.IR.LiveVarSet

Equations

Lean.IR.ExplicitRC.getJPLiveVars ctx j = match Std.RBMap.find? ctx.jpLiveVarMap j with | some s => s | none => ∅

source

def Lean.IR.ExplicitRC.mustConsume (ctx : Lean.IR.ExplicitRC.Context) (x : Lean.IR.VarId) :

Bool

Equations

Lean.IR.ExplicitRC.mustConsume ctx x = let info := Lean.IR.ExplicitRC.getVarInfo ctx x; info.ref && info.consume

source

@[inline]

def Lean.IR.ExplicitRC.addInc (ctx : Lean.IR.ExplicitRC.Context) (x : Lean.IR.VarId) (b : Lean.IR.FnBody) (n : optParam Nat 1) :

Lean.IR.FnBody

Equations

Lean.IR.ExplicitRC.addInc ctx x b n = let info := Lean.IR.ExplicitRC.getVarInfo ctx x; if (n == 0) = true then b else Lean.IR.FnBody.inc x n true info.persistent b

source

@[inline]

def Lean.IR.ExplicitRC.addDec (ctx : Lean.IR.ExplicitRC.Context) (x : Lean.IR.VarId) (b : Lean.IR.FnBody) :

Lean.IR.FnBody

Equations

Lean.IR.ExplicitRC.addDec ctx x b = let info := Lean.IR.ExplicitRC.getVarInfo ctx x; Lean.IR.FnBody.dec x 1 true info.persistent b

source

def Lean.IR.ExplicitRC.updateVarInfoWithParams (ctx : Lean.IR.ExplicitRC.Context) (ps : Array Lean.IR.Param) :

Lean.IR.ExplicitRC.Context

Equations

Lean.IR.ExplicitRC.updateVarInfoWithParams ctx ps = let m := Array.foldl (fun m p => Std.RBMap.insert m p.x { ref := Lean.IR.IRType.isObj p.ty, persistent := false, consume := !p.borrow }) ctx.varMap ps 0 (Array.size ps); { env := ctx.env, decls := ctx.decls, varMap := m, jpLiveVarMap := ctx.jpLiveVarMap, localCtx := ctx.localCtx }

source

partial def Lean.IR.ExplicitRC.visitFnBody :

Lean.IR.FnBody → Lean.IR.ExplicitRC.Context → Lean.IR.FnBody × Lean.IR.LiveVarSet

source

def Lean.IR.ExplicitRC.visitDecl (env : Lean.Environment) (decls : Array Lean.IR.Decl) (d : Lean.IR.Decl) :

Lean.IR.Decl

Equations

Lean.IR.ExplicitRC.visitDecl env decls d = match d with | Lean.IR.Decl.fdecl x xs x_1 b x_2 => let ctx := { env := env, decls := decls, varMap := ∅, jpLiveVarMap := ∅, localCtx := ∅ }; let ctx := Lean.IR.ExplicitRC.updateVarInfoWithParams ctx xs; let x := Lean.IR.ExplicitRC.visitFnBody b ctx; match x with | (b, bLiveVars) => let b := Lean.IR.ExplicitRC.addDecForDeadParams ctx xs b bLiveVars; Lean.IR.Decl.updateBody! d b | other => other

source

def Lean.IR.explicitRC (decls : Array Lean.IR.Decl) :

Lean.IR.CompilerM (Array Lean.IR.Decl)

Equations

Lean.IR.explicitRC decls = do let env ← Lean.IR.getEnv pure (Array.map (Lean.IR.ExplicitRC.visitDecl env decls) decls)