def Blaster.Optimize.getAppliedMatchType (t : Lean.Expr) (nbArgs : Nat) : Lean.Expr

Given,

• t := λ β₁ => ... => βₘ => ∀ α₁ → ∀ α₂ → ... → αₙ corresponding to a match expression returning functions as rhs; and
• nbArgs ∈ [0..n] corresponding to the number of extra arguments applied to the match expression; and
• α'₁, ..., α'ₘ := [ αᵢ | i ∈ [nbArgs, n] ] Return:
• ∀ α'₁ → ∀ α'₂ → ... → α'ₘ Note that the returned type will correspond to αₙ when nbArgs = n.

Equations

• Blaster.Optimize.getAppliedMatchType t nbArgs = Lean.Expr.getForallBodyMaxDepth nbArgs (Blaster.Optimize.getLambdaBody t)

def Blaster.Optimize.normChoiceApplication? (f : Lean.Expr) (args : Array Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Given application f x₁ ... xₙ, apply the following normalization rules:

• When f := Blaster.dite' c (fun h : c => t₁) (fun h : ¬ c => t₂) Return Blaster.dite' c (fun h : c => t₁ x₁ ... xₙ) (fun h : ¬ c => t₂ x₁ ... xₙ)

• When f := match₁ e₁, ..., eₙ with | p₍₁₎₍₁₎, ..., p₍₁₎₍ₙ₎ => t₁ ... | p₍ₘ₎₍₁₎, ..., p₍ₘ₎₍ₙ₎ => tₘ Return match₁ e₁, ..., eₙ with | p₍₁₎₍₁₎, ..., p₍₁₎₍ₙ₎ => t₁ x₁ ... xₙ ... | p₍ₘ₎₍₁₎, ..., p₍ₘ₎₍ₙ₎ => tₘ x₁ ... xₙ

Equations

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

def Blaster.Optimize.normChoiceApplication?.mkAppInDIteExpr (extra_args : Array Lean.Expr) (ite_cond ite_e : Lean.Expr) : TranslateEnvT Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Optimize.normChoiceApplication?.mkAppInDIteExpr extra_args ite_cond (Lean.Expr.lam n t body bi) = pure (Lean.Expr.lam n t (Lean.mkAppN body extra_args) bi)

def Blaster.Optimize.normChoiceApplication?.normDIteApp? (f : Lean.Expr) (args : Array Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Optimize.normChoiceApplication?.normDIteApp? f args = pure none

def Blaster.Optimize.normChoiceApplication?.mkAppInRhs (extra_args lhs : Array Lean.Expr) (rhs : Lean.Expr) : TranslateEnvT Lean.Expr

Equations

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

def Blaster.Optimize.normChoiceApplication?.normMatchApp? (f : Lean.Expr) (args : Array Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Equations

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

def Blaster.Optimize.funPropagation? (cf : Lean.Expr) (cargs : Array Lean.Expr) (skipPropCheck reorderArgs : Bool := false) : TranslateEnvT (Option Lean.Expr)

Apply the following propagation rules on any function application fn e₁ ... eₙ only when fn := Expr.const n l ∧ n ≠ Blaster.dite' ∧ ¬ isNotFun fn ∧ propagate fn e₁ ... eₙ

• When ∃ i ∈ [1..n], eᵢ := Blaster.dite' c (fun h : c => d₁) (fun h : ¬ c => d₂) ∧ ∀ j ∈ [1..n], (i ≠ j → gⱼ = eⱼ) ∧ (i = j → gⱼ = d₁) ∧ (i ≠ j → hⱼ = eⱼ) ∧ (i = j → hⱼ = d₂) Return Blaster.dite' c then (fun h : c => fn g₁ ... gₙ) (fun h : ¬ c => fn h₁ ... hₙ)

• When ∃ i ∈ [1..n], eᵢ := match₂ f₁, ..., fₚ with | p₍₁₎₍₁₎, ..., p₍₁₎₍ₚ₎ => t₁ ... | p₍ₘ₎₍₁₎, ..., p₍ₘ₎₍ₚ₎ => tₘ ∧ ∀ k ∈ [1..m], ∀ j ∈ [1..n], (i ≠ j → g₍ₖ₎₍ⱼ₎ = eⱼ) ∧ (i = j → g₍ₖ₎₍ⱼ₎ = tₖ) Return match₂ f₁, ..., fₚ with | p₍₁₎₍₁₎, ..., p₍₁₎₍ₚ₎ => fn g₍₁₎₍₁₎, ..., g₍₁₎₍ₙ₎ ... | p₍ₘ₎₍₁₎, ..., p₍ₘ₎₍ₚ₎ => fn g₍ₘ₎₍₁₎, ..., g₍ₘ₎₍ₙ₎

with: propagate fn e₁ ... eₙ := isCtorExpr fn ∨ allExplicitParamsAreCtor fn e₁ ... eₙ (funPropagation := true) ∨ (fn = Eq ∧ n = 3 ∧ (isBoolValue? e₂).isSome ) NOTE: skipPropCheck is set to true only when it is known beforehand that cf is a recursive function for which allExplicitParamsAreCtor cf cargs (funPropagation := true) returns true. NOTE: reorderArgs is set to true only when funPropagation? is called before optimizeApp.

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Optimize.funPropagation? cf cargs skipPropCheck reorderArgs = Blaster.Optimize.withLocalContext (pure none)

@[irreducible]

def Blaster.Optimize.funPropagation?.loop (cf : Lean.Expr) (idx : Nat) (args : Array Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Equations

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

def Blaster.Optimize.funPropagation?.propagate (f : Lean.Expr) (n : Lean.Name) (args : Array Lean.Expr) : TranslateEnvT Bool

Equations

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

def Blaster.Optimize.funPropagation?.pushFunInDIteExpr (f : Lean.Expr) (args : Array Lean.Expr) (idxField : Nat) (ite_cond ite_e : Lean.Expr) : TranslateEnvT Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Optimize.funPropagation?.pushFunInDIteExpr f args idxField ite_cond (Lean.Expr.lam n t body bi) = pure (Lean.Expr.lam n t (Lean.mkAppN f (args.set! idxField body)) bi)

def Blaster.Optimize.funPropagation?.diteCstProp? (f : Lean.Expr) (args : Array Lean.Expr) (idxArg : Nat) : TranslateEnvT (Option Lean.Expr)

Implements dite over ctor rule

Equations

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

def Blaster.Optimize.funPropagation?.updateRhsWithFun (f : Lean.Expr) (args : Array Lean.Expr) (idxField : Nat) (lhs : Array Lean.Expr) (rhs : Lean.Expr) : TranslateEnvT Lean.Expr

Equations

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

def Blaster.Optimize.funPropagation?.matchCstProp? (f : Lean.Expr) (args : Array Lean.Expr) (idxArg : Nat) : TranslateEnvT (Option Lean.Expr)

Implements match over ctor rule

Equations

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