Documentation

Lean.Compiler.LCNF.Simp.SimpM

  • declName : Name

    Name of the declaration being simplified. We currently use this information because we are generating phase1 declarations on demand, and it may trigger non-termination when trying to access the phase1 declaration.

  • config : Config
  • inlineStack : List Name

    Stack of global declarations being recursively inlined.

  • inlineStackOccs : PHashMap Name Nat

    Mapping from declaration names to number of occurrences at inlineStack

Instances For
    • subst : FVarSubst

      Free variable substitution. We use it to implement inlining and removing redundant variables let _x.i := _x.j

    • Track used local declarations to be able to eliminate dead variables.

    • binderRenaming : Renaming

      Mapping containing free variables ids that need to be renamed (i.e., the binderName). We use this map to preserve user provide names.

    • funDeclInfoMap : FunDeclInfoMap

      Mapping used to decide whether a local function declaration must be inlined or not.

    • simplified : Bool

      true if some simplification was performed in the current simplification pass.

    • visited : Nat

      Number of visited let-declarations and terminal values. This is a performance counter, and currently has no impact on code generation.

    • inline : Nat

      Number of definitions inlined. This is a performance counter.

    • inlineLocal : Nat

      Number of local functions inlined. This is a performance counter.

    Instances For
      @[reducible, inline]
      Equations
        Instances For
          @[always_inline]
          Equations

            Set the simplified flag to true.

            Equations
              Instances For

                Increment visited performance counter.

                Equations
                  Instances For

                    Increment inline performance counter. It is the number of inlined global declarations.

                    Equations
                      Instances For

                        Increment inlineLocal performance counter. It is the number of inlined local function and join point declarations.

                        Equations
                          Instances For

                            Mark the local function declaration or join point with the given id as a "must inline".

                            Equations
                              Instances For

                                Add a new occurrence of local function fvarId.

                                Equations
                                  Instances For

                                    Add a new occurrence of local function fvarId in argument position .

                                    Equations
                                      Instances For

                                        Traverse code and update function occurrence map. This map is used to decide whether we inline local functions or not. If mustInline := true, then all local function declarations occurring in code are tagged as .mustInline. Recall that we use .mustInline for local function declarations occurring in type class instances.

                                        Equations
                                          Instances For
                                            @[inline]
                                            def Lean.Compiler.LCNF.Simp.withInlining {α : Type} (value : LetValue) (recursive : Bool) (x : SimpM α) :

                                            Execute x with an updated inlineStack. If value is of the form const ..., add const to the stack. Otherwise, do not change the inlineStack.

                                            Equations
                                              Instances For
                                                Equations
                                                  Instances For
                                                    @[inline]

                                                    Similar to the default Lean.withIncRecDepth, but include the inlineStack in the error message.

                                                    Equations
                                                      Instances For

                                                        Execute x with fvarId set as mustInline. After execution the original setting is restored.

                                                        Equations
                                                          Instances For

                                                            Return true if the given local function declaration or join point id is marked as once or mustInline. We use this information to decide whether to inline them.

                                                            Equations
                                                              Instances For

                                                                Return true if the given code is considered "small".

                                                                Equations
                                                                  Instances For

                                                                    Return true if the given local function declaration should be inlined.

                                                                    Equations
                                                                      Instances For
                                                                        def Lean.Compiler.LCNF.Simp.betaReduce (params : Array Param) (code : Code) (args : Array Arg) (mustInline : Bool := false) :

                                                                        LCNF "Beta-reduce". The equivalent of (fun params => code) args. If mustInline is true, the local function declarations in the resulting code are marked as .mustInline. See comment at updateFunDeclInfo.

                                                                        Equations
                                                                          Instances For

                                                                            Erase the given let-declaration from the local context, and set the simplified flag to true.

                                                                            Equations
                                                                              Instances For

                                                                                Erase the given local function declaration from the local context, and set the simplified flag to true.

                                                                                Equations
                                                                                  Instances For

                                                                                    Similar to LCNF.addFVarSubst. That is, add the entry fvarId ↦ fvarId' to the free variable substitution. If fvarId has a non-internal binder name n, but fvarId' does not, this method also adds the entry fvarId' ↦ n to the binderRenaming map. The goal is to preserve user provided names.

                                                                                    Equations
                                                                                      Instances For