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

Equations

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

instance Lean.IR.UnreachableBranches.instReprValue : Repr Value

Equations

• Lean.IR.UnreachableBranches.instReprValue = { reprPrec := Lean.IR.UnreachableBranches.reprValue✝ }

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

instance Lean.IR.UnreachableBranches.instToFormatValue : ToFormat Value

Equations

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

instance Lean.IR.UnreachableBranches.instToStringValue : ToString Value

Equations

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

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

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

Equations

• Lean.IR.UnreachableBranches.Value.instBEq = { beq := Lean.IR.UnreachableBranches.Value.beq }

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.

Equations

• Lean.IR.UnreachableBranches.Value.truncateMaxDepth = 8

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.

Equations

• Lean.IR.UnreachableBranches.Value.truncate env v s = Lean.IR.UnreachableBranches.Value.truncate.go env v s Lean.IR.UnreachableBranches.Value.truncateMaxDepth

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.

Equations

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

@[reducible, inline]

abbrev Lean.IR.UnreachableBranches.FunctionSummaries : Type

Equations

• Lean.IR.UnreachableBranches.FunctionSummaries = Lean.PHashMap Lean.IR.FunId Lean.IR.UnreachableBranches.Value

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

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

Equations

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

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

Equations

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

@[reducible, inline]

abbrev Lean.IR.UnreachableBranches.Assignment : Type

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.IR.UnreachableBranches.findArgValue (Lean.IR.Arg.var x) = Lean.IR.UnreachableBranches.findVarValue x
• Lean.IR.UnreachableBranches.findArgValue arg = pure Lean.IR.UnreachableBranches.Value.top

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

Equations

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

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

Equations

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

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

Equations

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

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

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.IR.UnreachableBranches.interpExpr (Lean.IR.Expr.proj i x_1) = do let __do_lift ← Lean.IR.UnreachableBranches.findVarValue x_1 pure (Lean.IR.UnreachableBranches.projValue __do_lift i)
• Lean.IR.UnreachableBranches.interpExpr x✝ = pure Lean.IR.UnreachableBranches.Value.top

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

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

Equations

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

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

Equations

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

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.

Equations

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

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

def Lean.IR.UnreachableBranches.inferStep : M Bool

Equations

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

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

Equations

• Lean.IR.UnreachableBranches.elimDead assignment (Lean.IR.Decl.fdecl f xs type b info) = (Lean.IR.Decl.fdecl f xs type b info).updateBody! (Lean.IR.UnreachableBranches.elimDeadAux assignment b)
• Lean.IR.UnreachableBranches.elimDead assignment d = d

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

Equations

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