def Lean.Compiler.LCNF.Simp.isJpCases? (decl : FunDecl) : CompilerM (Option Nat)

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.

def Lean.Compiler.LCNF.Simp.isJpCases?.go (decl : FunDecl) (small : Nat) (code : Code) (prefixSize : Nat) : Option Nat

structure Lean.Compiler.LCNF.Simp.JpCasesInfo : Type

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

instance Lean.Compiler.LCNF.Simp.instInhabitedJpCasesInfo : Inhabited JpCasesInfo

@[reducible, inline]

abbrev Lean.Compiler.LCNF.Simp.JpCasesInfoMap : Type

def Lean.Compiler.LCNF.Simp.JpCasesInfoMap.isCandidate (info : JpCasesInfoMap) : Bool

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

def Lean.Compiler.LCNF.Simp.collectJpCasesInfo (code : Code) : CompilerM JpCasesInfoMap

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

partial def Lean.Compiler.LCNF.Simp.collectJpCasesInfo.go (code : Code) : StateRefT' IO.RealWorld JpCasesInfoMap DiscrM Unit

structure Lean.Compiler.LCNF.Simp.JpCasesAlt : Type

• decl : FunDecl
• default : Bool
• dependsOnDiscr : Bool

@[reducible, inline]

abbrev Lean.Compiler.LCNF.Simp.Ctor2JpCasesAlt : Type

def Lean.Compiler.LCNF.Simp.simpJpCases? (code : Code) : CompilerM (Option Code)

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.

partial def Lean.Compiler.LCNF.Simp.simpJpCases?.visit (code : Code) : ReaderT JpCasesInfoMap (StateRefT' IO.RealWorld Ctor2JpCasesAlt DiscrM) Code

partial def Lean.Compiler.LCNF.Simp.simpJpCases?.visitJp? (decl : FunDecl) (k : Code) : ReaderT JpCasesInfoMap (StateRefT' IO.RealWorld Ctor2JpCasesAlt DiscrM) (Option Code)

def Lean.Compiler.LCNF.Simp.simpJpCases?.visitJmp? (fvarId : FVarId) (args : Array Arg) : ReaderT JpCasesInfoMap (StateRefT' IO.RealWorld Ctor2JpCasesAlt DiscrM) (Option Code)