Lean.Compiler.IR.ElimDeadBranches

source

inductive Lean.IR.UnreachableBranches.Value :

Type

bot: Lean.IR.UnreachableBranches.Value
top: Lean.IR.UnreachableBranches.Value
ctor: Lean.IR.CtorInfo → Array Lean.IR.UnreachableBranches.Value → Lean.IR.UnreachableBranches.Value
choice: List Lean.IR.UnreachableBranches.Value → Lean.IR.UnreachableBranches.Value

source

instance Lean.IR.UnreachableBranches.instReprValue :

Repr Lean.IR.UnreachableBranches.Value

Equations

Lean.IR.UnreachableBranches.instReprValue = { reprPrec := [anonymous] }

source

instance Lean.IR.UnreachableBranches.instInhabitedValue :

Inhabited Lean.IR.UnreachableBranches.Value

Equations

Lean.IR.UnreachableBranches.instInhabitedValue = { default := Lean.IR.UnreachableBranches.Value.bot }

source

partial def Lean.IR.UnreachableBranches.Value.toFormat :

Lean.IR.UnreachableBranches.Value → Lean.Format

source

instance Lean.IR.UnreachableBranches.instToFormatValue :

Lean.ToFormat Lean.IR.UnreachableBranches.Value

Equations

Lean.IR.UnreachableBranches.instToFormatValue = { format := Lean.IR.UnreachableBranches.Value.toFormat }

source

instance Lean.IR.UnreachableBranches.instToStringValue :

ToString Lean.IR.UnreachableBranches.Value

Equations

Lean.IR.UnreachableBranches.instToStringValue = { toString := fun v => toString (Lean.format v) }

source

partial def Lean.IR.UnreachableBranches.Value.beq :

Lean.IR.UnreachableBranches.Value → Lean.IR.UnreachableBranches.Value → Bool

source

instance Lean.IR.UnreachableBranches.Value.instBEqValue :

BEq Lean.IR.UnreachableBranches.Value

Equations

Lean.IR.UnreachableBranches.Value.instBEqValue = { beq := Lean.IR.UnreachableBranches.Value.beq }

source

partial def Lean.IR.UnreachableBranches.Value.addChoice (merge : Lean.IR.UnreachableBranches.Value → Lean.IR.UnreachableBranches.Value → Lean.IR.UnreachableBranches.Value) :

List Lean.IR.UnreachableBranches.Value → Lean.IR.UnreachableBranches.Value → List Lean.IR.UnreachableBranches.Value

source

partial def Lean.IR.UnreachableBranches.Value.merge (v₁ : Lean.IR.UnreachableBranches.Value) (v₂ : Lean.IR.UnreachableBranches.Value) :

Lean.IR.UnreachableBranches.Value

source

partial def Lean.IR.UnreachableBranches.Value.format :

Lean.IR.UnreachableBranches.Value → Lean.Format

source

instance Lean.IR.UnreachableBranches.Value.instToFormatValue :

Lean.ToFormat Lean.IR.UnreachableBranches.Value

Equations

Lean.IR.UnreachableBranches.Value.instToFormatValue = { format := Lean.IR.UnreachableBranches.Value.format }

source

instance Lean.IR.UnreachableBranches.Value.instToStringValue :

ToString Lean.IR.UnreachableBranches.Value

Equations

Lean.IR.UnreachableBranches.Value.instToStringValue = { toString := (fun f => Lean.Format.pretty f) ∘ Lean.IR.UnreachableBranches.Value.format }

source

def Lean.IR.UnreachableBranches.Value.truncateMaxDepth :

Nat

Equations

Lean.IR.UnreachableBranches.Value.truncateMaxDepth = 8

source

def Lean.IR.UnreachableBranches.Value.truncate (env : Lean.Environment) (v : Lean.IR.UnreachableBranches.Value) (s : Lean.NameSet) :

Lean.IR.UnreachableBranches.Value

Equations

Lean.IR.UnreachableBranches.Value.truncate env v s = (fun go => go v s Lean.IR.UnreachableBranches.Value.truncateMaxDepth) (Lean.IR.UnreachableBranches.Value.truncate.go env)

source

partial def Lean.IR.UnreachableBranches.Value.truncate.go (env : Lean.Environment) (v : Lean.IR.UnreachableBranches.Value) (s : Lean.NameSet) (depth : Nat) :

Lean.IR.UnreachableBranches.Value

source

def Lean.IR.UnreachableBranches.Value.widening (env : Lean.Environment) (v₁ : Lean.IR.UnreachableBranches.Value) (v₂ : Lean.IR.UnreachableBranches.Value) :

Lean.IR.UnreachableBranches.Value

Equations

Lean.IR.UnreachableBranches.Value.widening env v₁ v₂ = Lean.IR.UnreachableBranches.Value.truncate env (Lean.IR.UnreachableBranches.Value.merge v₁ v₂) ∅

source

@[inline]

abbrev Lean.IR.UnreachableBranches.FunctionSummaries :

Type

Equations

Lean.IR.UnreachableBranches.FunctionSummaries = Lean.SMap Lean.IR.FunId Lean.IR.UnreachableBranches.Value

source

constant Lean.IR.UnreachableBranches.functionSummariesExt :

Lean.SimplePersistentEnvExtension (Lean.IR.FunId × Lean.IR.UnreachableBranches.Value) Lean.IR.UnreachableBranches.FunctionSummaries

source

def Lean.IR.UnreachableBranches.addFunctionSummary (env : Lean.Environment) (fid : Lean.IR.FunId) (v : Lean.IR.UnreachableBranches.Value) :

Lean.Environment

Equations

Lean.IR.UnreachableBranches.addFunctionSummary env fid v = Lean.PersistentEnvExtension.addEntry Lean.IR.UnreachableBranches.functionSummariesExt env (fid, v)

source

def Lean.IR.UnreachableBranches.getFunctionSummary? (env : Lean.Environment) (fid : Lean.IR.FunId) :

Option Lean.IR.UnreachableBranches.Value

Equations

Lean.IR.UnreachableBranches.getFunctionSummary? env fid = Lean.SMap.find? (Lean.SimplePersistentEnvExtension.getState Lean.IR.UnreachableBranches.functionSummariesExt env) fid

source

@[inline]

abbrev Lean.IR.UnreachableBranches.Assignment :

Type

Equations

Lean.IR.UnreachableBranches.Assignment = Std.HashMap Lean.IR.VarId Lean.IR.UnreachableBranches.Value

source

structure Lean.IR.UnreachableBranches.InterpContext :

Type

currFnIdx : Nat
decls : Array Lean.IR.Decl
env : Lean.Environment
lctx : Lean.IR.LocalContext

source

structure Lean.IR.UnreachableBranches.InterpState :

Type

assignments : Array Lean.IR.UnreachableBranches.Assignment
funVals : Std.PArray Lean.IR.UnreachableBranches.Value

source

@[inline]

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

Type

Equations

Lean.IR.UnreachableBranches.M = ReaderT Lean.IR.UnreachableBranches.InterpContext (StateM Lean.IR.UnreachableBranches.InterpState)

source

def Lean.IR.UnreachableBranches.findVarValue (x : Lean.IR.VarId) :

Lean.IR.UnreachableBranches.M Lean.IR.UnreachableBranches.Value

Equations

Lean.IR.UnreachableBranches.findVarValue x = do let ctx ← read let s ← get let assignment : Lean.IR.UnreachableBranches.Assignment := Array.getOp s.assignments ctx.currFnIdx pure (Std.HashMap.findD assignment x Lean.IR.UnreachableBranches.Value.bot)

source

def Lean.IR.UnreachableBranches.findArgValue (arg : Lean.IR.Arg) :

Lean.IR.UnreachableBranches.M Lean.IR.UnreachableBranches.Value

Equations

Lean.IR.UnreachableBranches.findArgValue arg = match arg with | Lean.IR.Arg.var x => Lean.IR.UnreachableBranches.findVarValue x | x => pure Lean.IR.UnreachableBranches.Value.top

source

def Lean.IR.UnreachableBranches.updateVarAssignment (x : Lean.IR.VarId) (v : Lean.IR.UnreachableBranches.Value) :

Lean.IR.UnreachableBranches.M Unit

Equations

Lean.IR.UnreachableBranches.updateVarAssignment x v = do let v' ← Lean.IR.UnreachableBranches.findVarValue x let ctx ← read modify fun s => { assignments := Array.modify s.assignments ctx.currFnIdx fun a => Std.HashMap.insert a x (Lean.IR.UnreachableBranches.Value.merge v v'), funVals := s.funVals }

source

def Lean.IR.UnreachableBranches.resetVarAssignment (x : Lean.IR.VarId) :

Lean.IR.UnreachableBranches.M Unit

Equations

Lean.IR.UnreachableBranches.resetVarAssignment x = do let ctx ← read modify fun s => { assignments := Array.modify s.assignments ctx.currFnIdx fun a => Std.HashMap.insert a x Lean.IR.UnreachableBranches.Value.bot, funVals := s.funVals }

source

def Lean.IR.UnreachableBranches.resetParamAssignment (y : Lean.IR.Param) :

Lean.IR.UnreachableBranches.M Unit

Equations

Lean.IR.UnreachableBranches.resetParamAssignment y = Lean.IR.UnreachableBranches.resetVarAssignment y.x

source

partial def Lean.IR.UnreachableBranches.projValue :

Lean.IR.UnreachableBranches.Value → Nat → Lean.IR.UnreachableBranches.Value

source

def Lean.IR.UnreachableBranches.interpExpr :

Lean.IR.Expr → Lean.IR.UnreachableBranches.M Lean.IR.UnreachableBranches.Value

Equations

Lean.IR.UnreachableBranches.interpExpr x = match x with | Lean.IR.Expr.ctor i ys => do let a ← Array.mapM (fun y => Lean.IR.UnreachableBranches.findArgValue y) ys pure (Lean.IR.UnreachableBranches.Value.ctor i a) | Lean.IR.Expr.proj i x => do let a ← Lean.IR.UnreachableBranches.findVarValue x pure (Lean.IR.UnreachableBranches.projValue a i) | Lean.IR.Expr.fap fid ys => do let ctx ← read match Lean.IR.UnreachableBranches.getFunctionSummary? ctx.env fid with | some v => pure v | none => do let s ← get match Array.findIdx? ctx.decls fun decl => Lean.IR.Decl.name decl == fid with | some idx => pure (Std.PersistentArray.getOp s.funVals idx) | none => pure Lean.IR.UnreachableBranches.Value.top | x => pure Lean.IR.UnreachableBranches.Value.top

source

partial def Lean.IR.UnreachableBranches.containsCtor :

Lean.IR.UnreachableBranches.Value → Lean.IR.CtorInfo → Bool

source

def Lean.IR.UnreachableBranches.updateCurrFnSummary (v : Lean.IR.UnreachableBranches.Value) :

Lean.IR.UnreachableBranches.M Unit

Equations

Lean.IR.UnreachableBranches.updateCurrFnSummary v = do let ctx ← read let currFnIdx : Nat := ctx.currFnIdx modify fun s => { assignments := s.assignments, funVals := Std.PersistentArray.modify s.funVals currFnIdx fun v' => Lean.IR.UnreachableBranches.Value.widening ctx.env v v' }

source

def Lean.IR.UnreachableBranches.updateJPParamsAssignment (ys : Array Lean.IR.Param) (xs : Array Lean.IR.Arg) :

Lean.IR.UnreachableBranches.M Bool

Equations

Lean.IR.UnreachableBranches.updateJPParamsAssignment ys xs = do let ctx ← read let currFnIdx : Nat := ctx.currFnIdx Nat.foldM (fun i r => let y := Array.getOp ys i; let x := Array.getOp xs i; do let yVal ← Lean.IR.UnreachableBranches.findVarValue y.x let xVal ← Lean.IR.UnreachableBranches.findArgValue x let newVal : Lean.IR.UnreachableBranches.Value := Lean.IR.UnreachableBranches.Value.merge yVal xVal if (newVal == yVal) = true then pure r else do modify fun s => { assignments := Array.modify s.assignments currFnIdx fun a => Std.HashMap.insert a y.x newVal, funVals := s.funVals } pure true) false (Array.size ys)

source

partial def Lean.IR.UnreachableBranches.interpFnBody :

Lean.IR.FnBody → Lean.IR.UnreachableBranches.M Unit

source

def Lean.IR.UnreachableBranches.inferStep :

Lean.IR.UnreachableBranches.M Bool

Equations

Lean.IR.UnreachableBranches.inferStep = do let ctx ← read modify fun s => { assignments := Array.map (fun x => ∅) ctx.decls, funVals := s.funVals } Nat.foldM (fun idx modified => match Array.getOp ctx.decls idx with | Lean.IR.Decl.fdecl x ys x_1 b x_2 => do let s ← get let currVals : Lean.IR.UnreachableBranches.Value := Std.PersistentArray.getOp s.funVals idx withReader (fun ctx => { currFnIdx := idx, decls := ctx.decls, env := ctx.env, lctx := ctx.lctx }) do Array.forM (fun y => Lean.IR.UnreachableBranches.updateVarAssignment y.x Lean.IR.UnreachableBranches.Value.top) ys 0 (Array.size ys) Lean.IR.UnreachableBranches.interpFnBody b let s ← get let newVals : Lean.IR.UnreachableBranches.Value := Std.PersistentArray.getOp s.funVals idx pure (modified || currVals != newVals) | Lean.IR.Decl.extern x x_1 x_2 x_3 => pure modified) false (Array.size ctx.decls)

source

partial def Lean.IR.UnreachableBranches.inferMain :

Lean.IR.UnreachableBranches.M Unit

source

partial def Lean.IR.UnreachableBranches.elimDeadAux (assignment : Lean.IR.UnreachableBranches.Assignment) :

Lean.IR.FnBody → Lean.IR.FnBody

source

def Lean.IR.UnreachableBranches.elimDead (assignment : Lean.IR.UnreachableBranches.Assignment) (d : Lean.IR.Decl) :

Lean.IR.Decl

Equations

Lean.IR.UnreachableBranches.elimDead assignment d = match d with | Lean.IR.Decl.fdecl x x_1 x_2 b x_3 => Lean.IR.Decl.updateBody! d (Lean.IR.UnreachableBranches.elimDeadAux assignment b) | other => other

source

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

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

Equations

Lean.IR.elimDeadBranches decls = do let s ← get let env : Lean.Environment := s.env let assignments : Array Lean.IR.UnreachableBranches.Assignment := Array.map (fun x => ∅) decls let funVals : Std.PArray Lean.IR.UnreachableBranches.Value := Std.mkPArray (Array.size decls) Lean.IR.UnreachableBranches.Value.bot let ctx : Lean.IR.UnreachableBranches.InterpContext := { currFnIdx := 0, decls := decls, env := env, lctx := ∅ } let s : Lean.IR.UnreachableBranches.InterpState := { assignments := assignments, funVals := funVals } let x : Id (Unit × Lean.IR.UnreachableBranches.InterpState) := StateT.run (Lean.IR.UnreachableBranches.inferMain ctx) s match x with | (x, s) => let funVals := s.funVals; let assignments := s.assignments; do modify fun s => let env := Nat.fold (fun i env => Lean.IR.UnreachableBranches.addFunctionSummary env (Lean.IR.Decl.name (Array.getOp decls i)) (Std.PersistentArray.getOp funVals i)) (Array.size decls) s.env; { env := env, log := s.log } pure (Array.mapIdx decls fun i decl => Lean.IR.UnreachableBranches.elimDead (Array.getOp assignments i.val) decl)