Documentation

Lean.Compiler.IR.ElimDeadBranches

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

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 := [anonymous] }

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 => toString (Lean.format v) }

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

Equations

Lean.IR.UnreachableBranches.Value.instBEqValue = { 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.instToFormatValue:

Lean.ToFormat Lean.IR.UnreachableBranches.Value

Equations

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

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 }

def Lean.IR.UnreachableBranches.Value.truncateMaxDepth:

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 (Lean.IR.UnreachableBranches.Value.merge v₁ v₂) ∅

@[inline]

abbrev Lean.IR.UnreachableBranches.FunctionSummaries:

Type

Equations

Lean.IR.UnreachableBranches.FunctionSummaries = Lean.SMap 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 (fid, v)

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

@[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

structure Lean.IR.UnreachableBranches.InterpState:

Type

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

@[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) :

Equations

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

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.