Documentation

Lean.Compiler.LCNF.Simp.SimpM

source
structure Lean.Compiler.LCNF.Simp.Context :
Type

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

    declName : Lean.Name
  • config : Lean.Compiler.LCNF.Simp.Config

  • Stack of global declarations being recursively inlined.

    inlineStack : List Lean.Name

  • Mapping from declaration names to number of occurrences at inlineStack

    inlineStackOccs : Lean.PHashMap Lean.Name Nat
Instances For
    source
    structure Lean.Compiler.LCNF.Simp.State :
    Type

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

      subst : Lean.Compiler.LCNF.FVarSubst

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

      used : Lean.Compiler.LCNF.UsedLocalDecls

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

      binderRenaming : Lean.Compiler.LCNF.Renaming

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

      funDeclInfoMap : Lean.Compiler.LCNF.Simp.FunDeclInfoMap

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

      simplified : Bool

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

      visited : Nat

    • Number of definitions inlined. This is a performance counter.

      inline : Nat

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

      inlineLocal : Nat
    Instances For
      source
      @[inline]
      abbrev Lean.Compiler.LCNF.Simp.SimpM (α : Type) :
      Type
      Equations
      source
      @[always_inline]
      instance Lean.Compiler.LCNF.Simp.instMonadSimpM :
      Monad Lean.Compiler.LCNF.Simp.SimpM
      Equations
      source
      instance Lean.Compiler.LCNF.Simp.instMonadFVarSubstSimpMFalse :
      Lean.Compiler.LCNF.MonadFVarSubst Lean.Compiler.LCNF.Simp.SimpM false
      Equations
      source
      instance Lean.Compiler.LCNF.Simp.instMonadFVarSubstStateSimpM :
      Lean.Compiler.LCNF.MonadFVarSubstState Lean.Compiler.LCNF.Simp.SimpM
      Equations
      • One or more equations did not get rendered due to their size.
      source
      def Lean.Compiler.LCNF.Simp.markSimplified :
      Lean.Compiler.LCNF.Simp.SimpM Unit

      Set the simplified flag to true.

      Equations
      • One or more equations did not get rendered due to their size.
      source
      def Lean.Compiler.LCNF.Simp.incVisited :
      Lean.Compiler.LCNF.Simp.SimpM Unit

      Increment visited performance counter.

      Equations
      • One or more equations did not get rendered due to their size.
      source
      def Lean.Compiler.LCNF.Simp.incInline :
      Lean.Compiler.LCNF.Simp.SimpM Unit

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

      Equations
      • One or more equations did not get rendered due to their size.
      source
      def Lean.Compiler.LCNF.Simp.incInlineLocal :
      Lean.Compiler.LCNF.Simp.SimpM Unit

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

      Equations
      • One or more equations did not get rendered due to their size.
      source
      def Lean.Compiler.LCNF.Simp.addMustInline (fvarId : Lean.FVarId) :
      Lean.Compiler.LCNF.Simp.SimpM Unit

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

      Equations
      • One or more equations did not get rendered due to their size.
      source
      def Lean.Compiler.LCNF.Simp.addFunOcc (fvarId : Lean.FVarId) :
      Lean.Compiler.LCNF.Simp.SimpM Unit

      Add a new occurrence of local function fvarId.

      Equations
      • One or more equations did not get rendered due to their size.
      source
      def Lean.Compiler.LCNF.Simp.addFunHoOcc (fvarId : Lean.FVarId) :
      Lean.Compiler.LCNF.Simp.SimpM Unit

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

      Equations
      • One or more equations did not get rendered due to their size.
      source
      def Lean.Compiler.LCNF.Simp.updateFunDeclInfo (code : Lean.Compiler.LCNF.Code) (mustInline : optParam Bool false) :
      Lean.Compiler.LCNF.Simp.SimpM Unit

      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
      • One or more equations did not get rendered due to their size.
      source
      @[inline]
      def Lean.Compiler.LCNF.Simp.withInlining {α : Type} (value : Lean.Compiler.LCNF.LetValue) (recursive : Bool) (x : Lean.Compiler.LCNF.Simp.SimpM α) :
      Lean.Compiler.LCNF.Simp.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
      • One or more equations did not get rendered due to their size.
      source
      def Lean.Compiler.LCNF.Simp.withInlining.check (recursive : Bool) (declName : Lean.Name) :
      Lean.Compiler.LCNF.Simp.SimpM Nat
      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[inline]
      def Lean.Compiler.LCNF.Simp.withIncRecDepth {α : Type} (x : Lean.Compiler.LCNF.Simp.SimpM α) :
      Lean.Compiler.LCNF.Simp.SimpM α

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

      Equations
      • One or more equations did not get rendered due to their size.
      source
      def Lean.Compiler.LCNF.Simp.withIncRecDepth.throwMaxRecDepth {α : Type} :
      Lean.Compiler.LCNF.Simp.SimpM α
      Equations
      • One or more equations did not get rendered due to their size.
      source
      def Lean.Compiler.LCNF.Simp.withAddMustInline {α : Type} (fvarId : Lean.FVarId) (x : Lean.Compiler.LCNF.Simp.SimpM α) :
      Lean.Compiler.LCNF.Simp.SimpM α

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

      Equations
      • One or more equations did not get rendered due to their size.
      source
      def Lean.Compiler.LCNF.Simp.isOnceOrMustInline (fvarId : Lean.FVarId) :
      Lean.Compiler.LCNF.Simp.SimpM Bool

      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
      • One or more equations did not get rendered due to their size.
      source
      def Lean.Compiler.LCNF.Simp.isSmall (code : Lean.Compiler.LCNF.Code) :
      Lean.Compiler.LCNF.Simp.SimpM Bool

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

      Equations
      source
      def Lean.Compiler.LCNF.Simp.shouldInlineLocal (decl : Lean.Compiler.LCNF.FunDecl) :
      Lean.Compiler.LCNF.Simp.SimpM Bool

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

      Equations
      • One or more equations did not get rendered due to their size.
      source
      def Lean.Compiler.LCNF.Simp.betaReduce (params : Array Lean.Compiler.LCNF.Param) (code : Lean.Compiler.LCNF.Code) (args : Array Lean.Compiler.LCNF.Arg) (mustInline : optParam Bool false) :
      Lean.Compiler.LCNF.Simp.SimpM Lean.Compiler.LCNF.Code

      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
      • One or more equations did not get rendered due to their size.
      source
      def Lean.Compiler.LCNF.Simp.eraseLetDecl (decl : Lean.Compiler.LCNF.LetDecl) :
      Lean.Compiler.LCNF.Simp.SimpM Unit

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

      Equations
      source
      def Lean.Compiler.LCNF.Simp.eraseFunDecl (decl : Lean.Compiler.LCNF.FunDecl) :
      Lean.Compiler.LCNF.Simp.SimpM Unit

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

      Equations
      source
      def Lean.Compiler.LCNF.Simp.addFVarSubst (fvarId : Lean.FVarId) (fvarId' : Lean.FVarId) :
      Lean.Compiler.LCNF.Simp.SimpM Unit

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