inductive Lean.Compiler.LCNF.UnreachableBranches.Value : Type

The abstract domain of the interpreter. Representing sets of values of a certain type.

• bot: Lean.Compiler.LCNF.UnreachableBranches.Value

  Undefined, could be anything we have no information.

• top: Lean.Compiler.LCNF.UnreachableBranches.Value

  All values are possible.

• ctor: Lean.Name → Array Lean.Compiler.LCNF.UnreachableBranches.Value → Lean.Compiler.LCNF.UnreachableBranches.Value

  A certain constructor with a certain sets of parameters is possible.

• choice: List Lean.Compiler.LCNF.UnreachableBranches.Value → Lean.Compiler.LCNF.UnreachableBranches.Value

  A set of values are possible.

instance Lean.Compiler.LCNF.UnreachableBranches.instInhabitedValue : Inhabited Lean.Compiler.LCNF.UnreachableBranches.Value

Equations

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

instance Lean.Compiler.LCNF.UnreachableBranches.instReprValue : Repr Lean.Compiler.LCNF.UnreachableBranches.Value

Equations

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

def Lean.Compiler.LCNF.UnreachableBranches.Value.maxValueDepth : Nat

partial def Lean.Compiler.LCNF.UnreachableBranches.Value.beq : Lean.Compiler.LCNF.UnreachableBranches.Value → Lean.Compiler.LCNF.UnreachableBranches.Value → Bool

instance Lean.Compiler.LCNF.UnreachableBranches.Value.instBEq : BEq Lean.Compiler.LCNF.UnreachableBranches.Value

Equations

• Lean.Compiler.LCNF.UnreachableBranches.Value.instBEq = { beq := Lean.Compiler.LCNF.UnreachableBranches.Value.beq }

partial def Lean.Compiler.LCNF.UnreachableBranches.Value.addChoice (vs : List Lean.Compiler.LCNF.UnreachableBranches.Value) (v : Lean.Compiler.LCNF.UnreachableBranches.Value) : List Lean.Compiler.LCNF.UnreachableBranches.Value

Fuse v into vs. That is do not only append but if we see that v is a constructor that is already contained within vs try to detect the difference between these values and merge them accordingly into a choice node further down the tree.

partial def Lean.Compiler.LCNF.UnreachableBranches.Value.merge (v1 v2 : Lean.Compiler.LCNF.UnreachableBranches.Value) : Lean.Compiler.LCNF.UnreachableBranches.Value

Merge two values into one. bot is the neutral element, top the annihilator.

def Lean.Compiler.LCNF.UnreachableBranches.Value.truncate (env : Lean.Environment) (v : Lean.Compiler.LCNF.UnreachableBranches.Value) : Lean.Compiler.LCNF.UnreachableBranches.Value

Make sure constructors of recursive inductive datatypes can only occur once in each path. Values at depth > maxValueDepth are also approximated at top. We use 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.Compiler.LCNF.UnreachableBranches.Value.truncate.go (env : Lean.Environment) (v : Lean.Compiler.LCNF.UnreachableBranches.Value) (forbiddenTypes : Lean.NameSet) (remainingDepth : Nat) : Lean.Compiler.LCNF.UnreachableBranches.Value

def Lean.Compiler.LCNF.UnreachableBranches.Value.widening (env : Lean.Environment) (v1 v2 : Lean.Compiler.LCNF.UnreachableBranches.Value) : Lean.Compiler.LCNF.UnreachableBranches.Value

Widening operator that guarantees termination in our abstract interpreter.

Equations

• Lean.Compiler.LCNF.UnreachableBranches.Value.widening env v1 v2 = Lean.Compiler.LCNF.UnreachableBranches.Value.truncate env (v1.merge v2)

partial def Lean.Compiler.LCNF.UnreachableBranches.Value.containsCtor : Lean.Compiler.LCNF.UnreachableBranches.Value → Lean.Name → Bool

Check whether a certain constructor is part of a Value by name. Note that both top and bot will always true here. For bot this is because we have no information about the Value so just to be sure we don't claim the absence of a certain constructor.

def Lean.Compiler.LCNF.UnreachableBranches.Value.getCtorArgs : Lean.Compiler.LCNF.UnreachableBranches.Value → Lean.Name → Option (Array Lean.Compiler.LCNF.UnreachableBranches.Value)

Obtain the arguments of a certain constructor within the Value.

def Lean.Compiler.LCNF.UnreachableBranches.Value.ofNat (n : Nat) : Lean.Compiler.LCNF.UnreachableBranches.Value

partial def Lean.Compiler.LCNF.UnreachableBranches.Value.ofNat.goBig (orig curr : Nat) : Lean.Compiler.LCNF.UnreachableBranches.Value

partial def Lean.Compiler.LCNF.UnreachableBranches.Value.ofNat.goSmall : Nat → Lean.Compiler.LCNF.UnreachableBranches.Value

def Lean.Compiler.LCNF.UnreachableBranches.Value.ofLCNFLit : Lean.Compiler.LCNF.LitValue → Lean.Compiler.LCNF.UnreachableBranches.Value

Equations

• Lean.Compiler.LCNF.UnreachableBranches.Value.ofLCNFLit (Lean.Compiler.LCNF.LitValue.natVal n) = Lean.Compiler.LCNF.UnreachableBranches.Value.ofNat n
• Lean.Compiler.LCNF.UnreachableBranches.Value.ofLCNFLit (Lean.Compiler.LCNF.LitValue.strVal val) = Lean.Compiler.LCNF.UnreachableBranches.Value.top

partial def Lean.Compiler.LCNF.UnreachableBranches.Value.proj : Lean.Compiler.LCNF.UnreachableBranches.Value → Nat → Lean.Compiler.LCNF.UnreachableBranches.Value

partial def Lean.Compiler.LCNF.UnreachableBranches.Value.isLiteral : Lean.Compiler.LCNF.UnreachableBranches.Value → Bool

We say that a Value is a literal iff it is only a tree of Value.ctor nodes.

def Lean.Compiler.LCNF.UnreachableBranches.Value.getLiteral (v : Lean.Compiler.LCNF.UnreachableBranches.Value) : Lean.Compiler.LCNF.CompilerM (Option (Array Lean.Compiler.LCNF.CodeDecl × Lean.FVarId))

Attempt to turn a Value that is representing a literal into a set of auxiliary declarations + the final FVarId of the declaration that contains the actual literal. If it is not a literal return none.

Equations

• v.getLiteral = if v.isLiteral = true then do let literal ← Lean.Compiler.LCNF.UnreachableBranches.Value.getLiteral.go v pure (some literal) else pure none

partial def Lean.Compiler.LCNF.UnreachableBranches.Value.getLiteral.go : Lean.Compiler.LCNF.UnreachableBranches.Value → Lean.Compiler.LCNF.CompilerM (Array Lean.Compiler.LCNF.CodeDecl × Lean.FVarId)

partial def Lean.Compiler.LCNF.UnreachableBranches.Value.getLiteral.getNatConstant : Lean.Compiler.LCNF.UnreachableBranches.Value → Nat

@[reducible, inline]

abbrev Lean.Compiler.LCNF.UnreachableBranches.FunctionSummaries : Type

A map from function names to the Value that the abstract interpreter produced for them.

Equations

• Lean.Compiler.LCNF.UnreachableBranches.FunctionSummaries = Lean.PHashMap Lean.Name Lean.Compiler.LCNF.UnreachableBranches.Value

opaque Lean.Compiler.LCNF.UnreachableBranches.functionSummariesExt : Lean.SimplePersistentEnvExtension (Lean.Name × Lean.Compiler.LCNF.UnreachableBranches.Value) Lean.Compiler.LCNF.UnreachableBranches.FunctionSummaries

Storing FunctionSummaries for all functions in a .olean.

def Lean.Compiler.LCNF.UnreachableBranches.addFunctionSummary (env : Lean.Environment) (fid : Lean.Name) (v : Lean.Compiler.LCNF.UnreachableBranches.Value) : Lean.Environment

Add a Value for a function name.

Equations

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

def Lean.Compiler.LCNF.UnreachableBranches.getFunctionSummary? (env : Lean.Environment) (fid : Lean.Name) : Option Lean.Compiler.LCNF.UnreachableBranches.Value

Obtain the Value for a function name if possible.

Equations

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

@[reducible, inline]

abbrev Lean.Compiler.LCNF.UnreachableBranches.Assignment : Type

A map from variable identifiers to the Value produced by the abstract interpreter for them.

structure Lean.Compiler.LCNF.UnreachableBranches.InterpContext : Type

The context of InterpM.

• decls : Array Lean.Compiler.LCNF.Decl

  The list of Decls we are operating on in InterpM. This can be a single declaration or a mutual block of declarations where their analysis might influence each other as we approach the fixpoint.

• currFnIdx : Nat

  The index of the function we are currently operating on in decls.

structure Lean.Compiler.LCNF.UnreachableBranches.InterpState : Type

• assignments : Array Lean.Compiler.LCNF.UnreachableBranches.Assignment

  Assignments of functions in the InterpContext.

• funVals : Lean.PArray Lean.Compiler.LCNF.UnreachableBranches.Value

  Values of functions in the InterpContext use during computation of the fixpoint. Afterwards they are stored into the Environment.

@[reducible, inline]

abbrev Lean.Compiler.LCNF.UnreachableBranches.InterpM (α : Type) : Type

The monad which powers the abstract interpreter.

def Lean.Compiler.LCNF.UnreachableBranches.getAssignment : Lean.Compiler.LCNF.UnreachableBranches.InterpM Lean.Compiler.LCNF.UnreachableBranches.Assignment

Get the variable Assignment of the current function.

Equations

• Lean.Compiler.LCNF.UnreachableBranches.getAssignment = do let __do_lift ← get let __do_lift_1 ← read pure __do_lift.assignments[__do_lift_1.currFnIdx]!

def Lean.Compiler.LCNF.UnreachableBranches.getFunVal (funIdx : Nat) : Lean.Compiler.LCNF.UnreachableBranches.InterpM Lean.Compiler.LCNF.UnreachableBranches.Value

Get the Value of a certain function in the current block by index.

def Lean.Compiler.LCNF.UnreachableBranches.findFunVal? (declName : Lean.Name) : Lean.Compiler.LCNF.UnreachableBranches.InterpM (Option Lean.Compiler.LCNF.UnreachableBranches.Value)

def Lean.Compiler.LCNF.UnreachableBranches.modifyAssignment (f : Lean.Compiler.LCNF.UnreachableBranches.Assignment → Lean.Compiler.LCNF.UnreachableBranches.Assignment) : Lean.Compiler.LCNF.UnreachableBranches.InterpM Unit

Run f on the variable Assignment of the current function.

def Lean.Compiler.LCNF.UnreachableBranches.findVarValue (var : Lean.FVarId) : Lean.Compiler.LCNF.UnreachableBranches.InterpM Lean.Compiler.LCNF.UnreachableBranches.Value

Obtain the Value associated with var from the context of InterpM. If none is available return Value.bot.

Equations

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

def Lean.Compiler.LCNF.UnreachableBranches.findArgValue (arg : Lean.Compiler.LCNF.Arg) : Lean.Compiler.LCNF.UnreachableBranches.InterpM Lean.Compiler.LCNF.UnreachableBranches.Value

Find the value of arg using the logic of findVarValue.

Equations

• Lean.Compiler.LCNF.UnreachableBranches.findArgValue (Lean.Compiler.LCNF.Arg.fvar fvarId) = Lean.Compiler.LCNF.UnreachableBranches.findVarValue fvarId
• Lean.Compiler.LCNF.UnreachableBranches.findArgValue arg = pure Lean.Compiler.LCNF.UnreachableBranches.Value.top

def Lean.Compiler.LCNF.UnreachableBranches.updateVarAssignment (var : Lean.FVarId) (newVal : Lean.Compiler.LCNF.UnreachableBranches.Value) : Lean.Compiler.LCNF.UnreachableBranches.InterpM Unit

Update the assignment of var by merging the current value with newVal.

Equations

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

def Lean.Compiler.LCNF.UnreachableBranches.resetVarAssignment (var : Lean.FVarId) : Lean.Compiler.LCNF.UnreachableBranches.InterpM Unit

Set the value of var to bot.

def Lean.Compiler.LCNF.UnreachableBranches.updateCurrFnSummary (v : Lean.Compiler.LCNF.UnreachableBranches.Value) : Lean.Compiler.LCNF.UnreachableBranches.InterpM Unit

Widen the value of the current function by v.

def Lean.Compiler.LCNF.UnreachableBranches.updateFunDeclParamsAssignment (params : Array Lean.Compiler.LCNF.Param) (args : Array Lean.Compiler.LCNF.Arg) : Lean.Compiler.LCNF.UnreachableBranches.InterpM Bool

Return true if the assignment of at least one parameter has been updated. Furthermore if we see that params.size != args.size we know that this is a partial application and set the values of the remaining parameters to top since it is impossible to track what will happen with them from here on.

Equations

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

partial def Lean.Compiler.LCNF.UnreachableBranches.interpCode : Lean.Compiler.LCNF.Code → Lean.Compiler.LCNF.UnreachableBranches.InterpM Unit

The actual abstract interpreter on a block of Code.

partial def Lean.Compiler.LCNF.UnreachableBranches.interpCode.interpLetValue (letVal : Lean.Compiler.LCNF.LetValue) : Lean.Compiler.LCNF.UnreachableBranches.InterpM Lean.Compiler.LCNF.UnreachableBranches.Value

The abstract interpreter on a LetValue.

partial def Lean.Compiler.LCNF.UnreachableBranches.interpCode.handleFunArg (arg : Lean.Compiler.LCNF.Arg) : Lean.Compiler.LCNF.UnreachableBranches.InterpM Unit

partial def Lean.Compiler.LCNF.UnreachableBranches.interpCode.handleFunVar (var : Lean.FVarId) : Lean.Compiler.LCNF.UnreachableBranches.InterpM Unit

If we see a function being passed as an argument to a higher order function we cannot know what arguments it will be passed further down the line. Hence we set all of its arguments to top since anything is possible.

partial def Lean.Compiler.LCNF.UnreachableBranches.interpCode.interpFunCall (funDecl : Lean.Compiler.LCNF.FunDecl) (args : Array Lean.Compiler.LCNF.Arg) : Lean.Compiler.LCNF.UnreachableBranches.InterpM Unit

def Lean.Compiler.LCNF.UnreachableBranches.inferStep : Lean.Compiler.LCNF.UnreachableBranches.InterpM Bool

Rerun the abstract interpreter on all declarations except of the unsafe ones. Return whether any Value got updated in the process.

partial def Lean.Compiler.LCNF.UnreachableBranches.inferMain : Lean.Compiler.LCNF.UnreachableBranches.InterpM Unit

Run inferStep until it reaches a fix point.

def Lean.Compiler.LCNF.UnreachableBranches.elimDead (assignment : Lean.Compiler.LCNF.UnreachableBranches.Assignment) (decl : Lean.Compiler.LCNF.Decl) : Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.Decl

Use the information produced by the abstract interpreter to:

• Eliminate branches that we know cannot be hit
• Eliminate values that we know have to be constants.

partial def Lean.Compiler.LCNF.UnreachableBranches.elimDead.go (assignment : Lean.Compiler.LCNF.UnreachableBranches.Assignment) (code : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.Code

def Lean.Compiler.LCNF.Decl.elimDeadBranches (decls : Array Lean.Compiler.LCNF.Decl) : Lean.Compiler.LCNF.CompilerM (Array Lean.Compiler.LCNF.Decl)

Equations

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

def Lean.Compiler.LCNF.elimDeadBranches : Lean.Compiler.LCNF.Pass

Equations

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