def Lean.Compiler.LCNF.Simp.isJpCases (decl : Lean.Compiler.LCNF.FunDecl) : Lean.Compiler.LCNF.CompilerM Bool

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

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

Equations

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

def Lean.Compiler.LCNF.Simp.isJpCases.go (param : Lean.Compiler.LCNF.Param) (small : Nat) (code : Lean.Compiler.LCNF.Code) (prefixSize : Nat) : Bool

Equations

• One or more equations did not get rendered due to their size.
• Lean.Compiler.LCNF.Simp.isJpCases.go param small (Lean.Compiler.LCNF.Code.cases c) prefixSize = (decide (prefixSize ≤ small) && c.discr == param.fvarId)
• Lean.Compiler.LCNF.Simp.isJpCases.go param small code prefixSize = (decide (prefixSize ≤ small) && false)

@[inline]

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

Equations

• Lean.Compiler.LCNF.Simp.JpCasesInfo = Lean.FVarIdMap Lean.NameSet

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

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

Equations

• Lean.Compiler.LCNF.Simp.JpCasesInfo.isCandidate info = Lean.RBMap.any info fun x s => !Lean.RBTree.isEmpty s

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

Return a map containing entries jpFVarId ↦ 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.

Equations

• Lean.Compiler.LCNF.Simp.collectJpCasesInfo code = do let discr ← StateRefT'.run (Lean.Compiler.LCNF.Simp.collectJpCasesInfo.go code) ∅ match discr with | (fst, s) => pure s

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

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

• decl : Lean.Compiler.LCNF.FunDecl
• default : Bool
• dependsOnDiscr : Bool

@[inline]

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

Equations

• Lean.Compiler.LCNF.Simp.Ctor2JpCasesAlt = Lean.FVarIdMap (Lean.NameMap Lean.Compiler.LCNF.Simp.JpCasesAlt)

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

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.

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

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

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

Equations

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