inductive Lean.IR.UnreachableBranches.Value : Type

Value used in the abstract interpreter

• 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

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

Equations

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

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

Equations

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

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

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

Equations

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

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

Equations

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

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

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

Equations

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

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.instToFormat : Lean.ToFormat Lean.IR.UnreachableBranches.Value

Equations

• Lean.IR.UnreachableBranches.Value.instToFormat = { format := Lean.IR.UnreachableBranches.Value.format }

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

Equations

• Lean.IR.UnreachableBranches.Value.instToString = { toString := (fun (f : Lean.Format) => f.pretty Std.Format.defWidth 0) ∘ Lean.IR.UnreachableBranches.Value.format }

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 : 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.

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 : 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.

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 : 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

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 : Lean.Environment) (fid : Lean.IR.FunId) : Option Lean.IR.UnreachableBranches.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 = Lean.HashMap Lean.IR.VarId Lean.IR.UnreachableBranches.Value

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

@[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 : Lean.IR.VarId) : Lean.IR.UnreachableBranches.M Lean.IR.UnreachableBranches.Value

Equations

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

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

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

Equations

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

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

Equations

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

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

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

Equations

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

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

Equations

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

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.

Equations

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

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

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

Equations

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

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

Equations

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

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

Equations

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