def Lean.Compiler.LCNF.Simp.isJpCases? (decl : Lean.Compiler.LCNF.FunDecl) : Lean.Compiler.LCNF.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.

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Compiler.LCNF.Simp.isJpCases?.go decl small code prefixSize = if prefixSize > small then none else none

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

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

Equations

• Lean.Compiler.LCNF.Simp.instInhabitedJpCasesInfo = { default := { paramIdx := default, ctorNames := default } }

@[reducible, inline]

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

Equations

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

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

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

def Lean.Compiler.LCNF.Simp.collectJpCasesInfo (code : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.Simp.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

Equations

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

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

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

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

@[reducible, 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 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.

partial def Lean.Compiler.LCNF.Simp.simpJpCases?.visit (code : Lean.Compiler.LCNF.Code) : ReaderT Lean.Compiler.LCNF.Simp.JpCasesInfoMap (StateRefT' IO.RealWorld Lean.Compiler.LCNF.Simp.Ctor2JpCasesAlt Lean.Compiler.LCNF.Simp.DiscrM) 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.JpCasesInfoMap (StateRefT' IO.RealWorld Lean.Compiler.LCNF.Simp.Ctor2JpCasesAlt Lean.Compiler.LCNF.Simp.DiscrM) (Option Lean.Compiler.LCNF.Code)

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

Equations

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