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

Given application f x₁ ... xₙ, perform the following:

• When `isOpaqueRecFun f #[x₁ ... xₙ] ∧ allExplicitParamsAreCtor f #[x₁ ... xₙ]
  • When some auxFun ← unfoldOpaqueFunDef f #[x₁ ... xₙ]
    • When some body ← getFunBody auxFun.getAppFn'
      • return Expr.beta body auxFun.getAppArgs
    • Otherwise:
      • return ⊥
  • Otherwise:
    • return none
• When `isRecursiveFun f ∧ ¬ isOpaqueFunExpr f #[x₁ ... xₙ] ∧ allExplicitParamsAreCtor f #[x₁ ... xₙ]
  • When some body ← getFunBody f:
    • return Expr.beta body #[x₁ ... xₙ]
  • Otherwise:
    • return ⊥
• Otherwise:
  • return none

Equations

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

def Blaster.Optimize.reduceApp?.isOpaqueRecReduction? (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.reduceApp?.isFunRecReduction? (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.reduceApp?.isFunRecReduction? f args = pure none

def Blaster.Optimize.optimizeAppAux (f : Lean.Expr) (args : Array Lean.Expr) : TranslateEnvT Lean.Expr

Perform constant propagation and apply simplification and normalization rules on application expressions.

Equations

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

def Blaster.Optimize.optimizeApp (f : Lean.Expr) (args : Array Lean.Expr) (stack : List OptimizeStack) (skipPropCheck : Bool := false) : TranslateEnvT OptimizeContinuity

Perform the following:

• apply normalization and simplification rrules on the given application expression
• When restart flag is set:
  • add optimized application on continuation stack
• Otherwise:
  • try tp apply function propagation over ite and match:
    • When propagation rules are triggered:
      • add result on continuation stack
    • Otherwise:
      • cache normalized application
      • proceed with stack continuity

NOTE: skipPropCheck is set to true only when it is known beforehand that f is a recursive function for which allExplicitParamsAreCtor f args (funPropagation := true) returns true.

Equations

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

@[inline]

def Blaster.Optimize.optimizeApp.isFunPropagation? (skipPropCheck : Bool) (e : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Equations

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

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

Given application f x₁ ... xₙ,

• When isFunITE f (i.e., f is a Blaster.dite' that return a function)
  • return none
• when isNotfun f
  • return none
• when t₁ → ... → tₘ ← inferType f ∧ n < m:
  • when ∀ i ∈ [1..n], ¬ isExplicit tᵢ:
    • return none
  • otherwise:
    • return etaExpand (mkAppN f args)
• otherwise none

Equations

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

def Blaster.Optimize.normPartialFun?.isFunITE (args : Array Lean.Expr) (e : Lean.Expr) : Bool

Equations

• Blaster.Optimize.normPartialFun?.isFunITE args (Lean.Expr.const `Blaster.dite' us) = decide (args.size > 4)
• Blaster.Optimize.normPartialFun?.isFunITE args e = false

def Blaster.Optimize.normOpaqueAndRecFun (s : OptimizeStack) (xs : List OptimizeStack) : TranslateEnvT OptimizeContinuity

Given application f x₁ ... xₙ perform the following:

• when f corresponds to a recursive definition λ p₁ ... pₙ → body the following actions are performed:
  • params ← getImplicitParameters f #[x₁ ... xₙ]
  • fᵢₙₛ ← getInstApp f params
  • When entry fᵢₙₛ := fdef exists in the instance cache and fdef := fₙ is in the recursive function map.
    • return optimizeRecApp fₙ params
  • when no entry for fᵢₙₛ exists in the instance cache:
    • fbody' ← optimizer (← generalizeRecCall f params (λ p₁ ... pₙ → body))`
    • call storeRecFunDef to update instance cache and check if recursive definition already exists in map, i.e.: fᵢ ← storeRecFunDef fᵢₙₛ fbody'
    • return optimizeRecApp fᵢ params
• when f is not a recursive definition or is already in the recursive visited cache.
  • return optimizeApp f x₁ ... xₙ. Assumes that an entry exists for each opaque recursive function in recFunMap before optimization is performed (see function cacheOpaqueRecFun).

Equations

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

def Blaster.Optimize.normOpaqueAndRecFun.opaqueInstApp (f : Lean.Expr) (args : Array Lean.Expr) (isOpaqueRec : Bool) (instApp : Lean.Expr) : TranslateEnvT Lean.Expr

Given a function application f x₁ ... xₙ, flag isOpaqueRec and default instance application instApp perform the following:

• When isOpaqueRec:
  • return getInstApp (← getImplicitParameters f x₁ ... xₙ)
• Otherwise:
  • return instApp

Equations

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

def Blaster.Optimize.normOpaqueAndRecFun.resolveOpaque (f : Lean.Expr) (args : Array Lean.Expr) (isOpaqueRec : Bool) : TranslateEnvT (Lean.Expr × Array Lean.Expr)

Given a function application f x₁ ... xₙ and flag isOpaqueRec perform the following:

• When isOpaqueRec: let auxApp ← unfoldOpaqueFunDef f x₁ ... xₙ
  • when auxApp := λ α₀ → ... → λ αₖ → fₑ x₀ ... xₙ` (i.e., partially applied opaque relational function)
    • return (fₑ, x₀ ... xₙ₋ₖ)
  • when auxApp := fₑ x₀ ... xₙ` (default case)
    • return (fₑ, x₀ ...xₙ)
• Otherwise:
  • return (f, x₁ ... xₙ)

Equations

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

def Blaster.Optimize.normOpaqueAndRecFun.normRecOpaque (f : Lean.Expr) : Bool

Equations

• Blaster.Optimize.normOpaqueAndRecFun.normRecOpaque (Lean.Expr.const `Nat.beq us) = true
• Blaster.Optimize.normOpaqueAndRecFun.normRecOpaque (Lean.Expr.const `Nat.ble us) = true
• Blaster.Optimize.normOpaqueAndRecFun.normRecOpaque f = false

def Blaster.Optimize.normOpaqueAndRecFun.optimizeRecApp (uf rf : Lean.Expr) (uargs : Array Lean.Expr) (params : ImplicitParameters) (xs : List OptimizeStack) : TranslateEnvT OptimizeContinuity

Given rf a function application instance (see function getInstApp) and params its implicit parameter inffo (see function getImplicitParameters), perform the following: let instanceArgs := [ params[i] | ∀ i ∈ [0..params.size-1] ∧ params[i].isInstance ]

• When params.isEmpty :
  • return rf
• When instanceArgs.isEmpty ∨ f =ₚₜᵣ rf (i.e., non ploymorphic function or rec call in fun body)
  • return optimizeApp rf args
• When rf.isConst (i.e., polymorphic function equivalent to a non-polymorphic one)
  • return optimizeApp rf [params[i] | ∀ i ∈ [0..params.size-1] ∧ ¬ params[i].instance]
• Otherwise: let auxApp := Expr.beta rf (getEffectiveParams params)
  • When auxApp := λ α₀ → ... → λ αₖ → fₑ x₀ ... xₙ (i.e., partially applied polymorphic function)
    • return optimizeApp fₑ x₀ ...xₙ₋ₖ
  • When auxApp := fₑ x₀ ... xₙ (default case)
    • return optimizeApp fₑ x₀ ...xₙ

Equations

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