Documentation

Lean.Compiler.LCNF.Simp.JpCases

Given the function declaration decl, return some idx if it is of the form

f y :=
  ... /- This part is not bigger than smallThreshold. -/
  cases y
  | ... => ...
  ...

idx is the index of the parameter used in the cases statement.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[irreducible]
    Equations
    Instances For

      Information for join points that satisfy isJpCases?

      • paramIdx : Nat

        Parameter index returned by isJpCases?. This parameter is the one the join point is performing the case-split.

      • ctorNames : Lean.NameSet

        Set of constructor names s.t. ctorName is in the set if there is a jump to the join point where the parameter paramIdx is a constructor application.

      Instances For

        Return true if the collected information suggests opportunities for the JpCases optimization.

        Equations
        Instances For

          Return a map containing entries jpFVarId ↦ { paramIdx, ctorNames } where jpFVarId is the id of join point in code that satisfies isJpCases, and ctorNames is a set of constructor names such that there is a jump .jmp jpFVarId #[..., x, ...] in code and x is a constructor application. paramIdx is the index of the parameter

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

              Try to optimize jpCases join points. We say a join point is a jpCases when it satisfies the predicate isJpCases. If we have a jump to jpCases with a constructor, then we can optimize the code by creating an new join point for the constructor. Example: suppose we have

              jp _jp.1 y :=
                let x.1 := true
                cases y
                | nil => let x.2 := g x.1; return x.2
                | cons h t => let x.3 := h x.1; return x.3
              ...
              cases x.4
              | ctor1 =>
                let x.5 := cons z.1 z.2
                jmp _jp.1 x.5
              | ctor2 =>
                let x.6 := f x.4
                jmp _jp.1 x.6
              

              This simpJpCases? converts it to

              jp _jp.2 h t :=
                let x.1 := true
                let x.3 := h x.1
                return x.3
              jp _jp.1 y :=
                let x.1 := true
                cases y
                | nil => let x.2 := g x.1; return x.2
                | cons h t => jmp _jp.2 h t
              ...
              cases x.4
              | ctor1 =>
                -- The constructor has been eliminated here
                jmp _jp.2 z.1 z.2
              | ctor2 =>
                let x.6 := f x.4
                jmp _jp.1 x.6
              

              Note that if all jumps to the join point are with constructors, then the join point is eliminated as dead code.

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