inductive Lean.IR.UnreachableBranches.Value : Type

Value used in the abstract interpreter

• bot : Value
• top : Value
• ctor (i : CtorInfo) (vs : Array Value) : Value
• choice (vs : List Value) : Value

instance Lean.IR.UnreachableBranches.instInhabitedValue : Inhabited Value

instance Lean.IR.UnreachableBranches.instReprValue : Repr Value

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

instance Lean.IR.UnreachableBranches.instToFormatValue : ToFormat Value

instance Lean.IR.UnreachableBranches.instToStringValue : ToString Value

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

instance Lean.IR.UnreachableBranches.Value.instBEq : BEq Value

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

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

def Lean.IR.UnreachableBranches.Value.truncateMaxDepth : Nat

In truncate, we approximate a value as top if depth > truncateMaxDepth. TODO: add option to control this parameter.

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

Make sure constructors of recursive inductive datatypes can only occur once in each path. Values at depth > truncateMaxDepth are also approximated at top. We use this function this function to implement a simple widening operation for our abstract interpreter. Recall the widening functions is used to ensure termination in abstract interpreters.

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

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

Widening operator that guarantees termination in our abstract interpreter.

@[reducible, inline]

abbrev Lean.IR.UnreachableBranches.FunctionSummaries : Type

opaque Lean.IR.UnreachableBranches.functionSummariesExt : SimplePersistentEnvExtension (FunId × Value) FunctionSummaries

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

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

@[reducible, inline]

abbrev Lean.IR.UnreachableBranches.Assignment : Type

structure Lean.IR.UnreachableBranches.InterpContext : Type

• currFnIdx : Nat
• decls : Array Decl
• env : Environment
• lctx : LocalContext

structure Lean.IR.UnreachableBranches.InterpState : Type

• assignments : Array Assignment
• funVals : PArray Value
• visitedJps : Array (Std.HashSet JoinPointId)

@[reducible, inline]

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

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

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

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

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

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

partial def Lean.IR.UnreachableBranches.projValue : Value → Nat → Value

def Lean.IR.UnreachableBranches.interpExpr : Expr → M Value

partial def Lean.IR.UnreachableBranches.containsCtor : Value → CtorInfo → Bool

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

def Lean.IR.UnreachableBranches.markJPVisited (j : JoinPointId) : M Bool

def Lean.IR.UnreachableBranches.updateJPParamsAssignment (j : JoinPointId) (ys : Array Param) (xs : Array Arg) : M Bool

Return true if the assignment of at least one parameter has been updated.

partial def Lean.IR.UnreachableBranches.interpFnBody : FnBody → M Unit

def Lean.IR.UnreachableBranches.inferStep : M Bool

partial def Lean.IR.UnreachableBranches.inferMain : M Unit

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

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

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