Documentation

Lean.Compiler.LCNF.ElimDeadBranches

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

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

Instances For
    source
    instance Lean.Compiler.LCNF.UnreachableBranches.instInhabitedValue :
    Inhabited Lean.Compiler.LCNF.UnreachableBranches.Value
    Equations
    source
    instance Lean.Compiler.LCNF.UnreachableBranches.instReprValue :
    Repr Lean.Compiler.LCNF.UnreachableBranches.Value
    Equations
    source
    def Lean.Compiler.LCNF.UnreachableBranches.Value.maxValueDepth :
    Nat
    Equations
    source
    partial def Lean.Compiler.LCNF.UnreachableBranches.Value.beq :
    Lean.Compiler.LCNF.UnreachableBranches.Value → Lean.Compiler.LCNF.UnreachableBranches.Value → Bool
    source
    instance Lean.Compiler.LCNF.UnreachableBranches.Value.instBEqValue :
    BEq Lean.Compiler.LCNF.UnreachableBranches.Value
    Equations
    source
    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.

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

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

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

    Equations
    source
    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
    source
    def Lean.Compiler.LCNF.UnreachableBranches.Value.widening (env : Lean.Environment) (v1 : Lean.Compiler.LCNF.UnreachableBranches.Value) (v2 : Lean.Compiler.LCNF.UnreachableBranches.Value) :
    Lean.Compiler.LCNF.UnreachableBranches.Value

    Widening operator that guarantees termination in our abstract interpreter.

    Equations
    source
    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.

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

    Equations
    • One or more equations did not get rendered due to their size.
    source
    def Lean.Compiler.LCNF.UnreachableBranches.Value.ofNat (n : Nat) :
    Lean.Compiler.LCNF.UnreachableBranches.Value
    Equations
    • One or more equations did not get rendered due to their size.
    source
    partial def Lean.Compiler.LCNF.UnreachableBranches.Value.ofNat.goBig (orig : Nat) (curr : Nat) :
    Lean.Compiler.LCNF.UnreachableBranches.Value
    source
    partial def Lean.Compiler.LCNF.UnreachableBranches.Value.ofNat.goSmall :
    Nat → Lean.Compiler.LCNF.UnreachableBranches.Value
    source
    def Lean.Compiler.LCNF.UnreachableBranches.Value.ofLCNFLit :
    Lean.Compiler.LCNF.LitValue → Lean.Compiler.LCNF.UnreachableBranches.Value
    Equations
    • One or more equations did not get rendered due to their size.
    source
    partial def Lean.Compiler.LCNF.UnreachableBranches.Value.proj :
    Lean.Compiler.LCNF.UnreachableBranches.Value → Nat → Lean.Compiler.LCNF.UnreachableBranches.Value
    source
    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.

    source
    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
    • One or more equations did not get rendered due to their size.
    source
    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)
    source
    partial def Lean.Compiler.LCNF.UnreachableBranches.Value.getLiteral.getNatConstant :
    Lean.Compiler.LCNF.UnreachableBranches.Value → Nat
    source
    @[inline]
    abbrev Lean.Compiler.LCNF.UnreachableBranches.FunctionSummaries :
    Type

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

    Equations
    source
    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.

    source
    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.
    source
    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.
    source
    @[inline]
    abbrev Lean.Compiler.LCNF.UnreachableBranches.Assignment :
    Type

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

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

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

      decls : Array Lean.Compiler.LCNF.Decl

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

      currFnIdx : Nat

    The context of InterpM.

    Instances For
      source
      structure Lean.Compiler.LCNF.UnreachableBranches.InterpState :
      Type
      Instances For
        source
        @[inline]
        abbrev Lean.Compiler.LCNF.UnreachableBranches.InterpM (α : Type) :
        Type

        The monad which powers the abstract interpreter.

        Equations
        • One or more equations did not get rendered due to their size.
        source
        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
        source
        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.

        Equations
        source
        def Lean.Compiler.LCNF.UnreachableBranches.findFunVal? (declName : Lean.Name) :
        Lean.Compiler.LCNF.UnreachableBranches.InterpM (Option Lean.Compiler.LCNF.UnreachableBranches.Value)
        Equations
        • One or more equations did not get rendered due to their size.
        source
        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.

        Equations
        • One or more equations did not get rendered due to their size.
        source
        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.
        source
        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
        • One or more equations did not get rendered due to their size.
        source
        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.
        source
        def Lean.Compiler.LCNF.UnreachableBranches.resetVarAssignment (var : Lean.FVarId) :
        Lean.Compiler.LCNF.UnreachableBranches.InterpM Unit

        Set the value of var to bot.

        Equations
        • One or more equations did not get rendered due to their size.
        source
        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.

        Equations
        • One or more equations did not get rendered due to their size.
        source
        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.
        source
        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.

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

        source
        partial def Lean.Compiler.LCNF.UnreachableBranches.interpCode.handleFunArg (arg : Lean.Compiler.LCNF.Arg) :
        Lean.Compiler.LCNF.UnreachableBranches.InterpM Unit
        source
        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.

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

        Equations
        • One or more equations did not get rendered due to their size.
        source
        partial def Lean.Compiler.LCNF.UnreachableBranches.inferMain :
        Lean.Compiler.LCNF.UnreachableBranches.InterpM Unit

        Run inferStep until it reaches a fix point.

        source
        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 interpeter to:

        • Eliminate branches that we know cannot be hit
        • Eliminate values that we know have to be constants.
        Equations
        • One or more equations did not get rendered due to their size.
        source
        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
        source
        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.
        source
        def Lean.Compiler.LCNF.elimDeadBranches :
        Lean.Compiler.LCNF.Pass
        Equations