# 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.
Equations
• Parameter index returned by isJpCases?. This parameter is the one the join point is performing the case-split.

paramIdx : Nat
• 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.

ctorNames : Lean.NameSet

Information for join points that satisfy isJpCases?

Instances For
Equations

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

Equations

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

Try to optimize jpCases join points. We say a join point is a jpCases when it satifies 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.
Equations
• One or more equations did not get rendered due to their size.