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

Value used in the abstract interpreter

instance Lean.IR.UnreachableBranches.instInhabitedValue : Inhabited Lean.IR.UnreachableBranches.Value

instance Lean.IR.UnreachableBranches.instReprValue : Repr Lean.IR.UnreachableBranches.Value

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

instance Lean.IR.UnreachableBranches.instToFormatValue : Lean.ToFormat Lean.IR.UnreachableBranches.Value

instance Lean.IR.UnreachableBranches.instToStringValue : ToString Lean.IR.UnreachableBranches.Value

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

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

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

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

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

instance Lean.IR.UnreachableBranches.Value.instToFormatValue : Lean.ToFormat Lean.IR.UnreachableBranches.Value

instance Lean.IR.UnreachableBranches.Value.instToStringValue : ToString Lean.IR.UnreachableBranches.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 : Lean.Environment) (v : Lean.IR.UnreachableBranches.Value) (s : Lean.NameSet) : Lean.IR.UnreachableBranches.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 : Lean.Environment) (v : Lean.IR.UnreachableBranches.Value) (s : Lean.NameSet) (depth : Nat) : Lean.IR.UnreachableBranches.Value

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

Widening operator that guarantees termination in our abstract interpreter.

@[inline, reducible]

abbrev Lean.IR.UnreachableBranches.FunctionSummaries : Type

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

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

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

@[inline, reducible]

abbrev Lean.IR.UnreachableBranches.Assignment : Type

structure Lean.IR.UnreachableBranches.InterpContext : Type

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

structure Lean.IR.UnreachableBranches.InterpState : Type

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

@[inline, reducible]

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

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

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

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

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

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

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

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

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

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

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

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

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

def Lean.IR.UnreachableBranches.inferStep : Lean.IR.UnreachableBranches.M Bool

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

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

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

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