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
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.
ctorNameis in the set if there is a jump to the join point where the parameterparamIdxis a constructor application.
Instances For
Equations
- Lean.Compiler.LCNF.Simp.instInhabitedJpCasesInfo = { default := { paramIdx := default, ctorNames := default } }
Return true if the collected information suggests opportunities for the JpCases optimization.
Equations
- info.isCandidate = Lean.RBMap.any info fun (x : Lean.FVarId) (s : Lean.Compiler.LCNF.Simp.JpCasesInfo) => !Lean.RBTree.isEmpty s.ctorNames
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
Instances For
- decl : Lean.Compiler.LCNF.FunDecl
- default : Bool
- dependsOnDiscr : Bool
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.