@[inline]

def Blaster.Optimize.isCstMatchProp (p : Lean.Expr) : TranslateEnvT Bool

Return true only when isConstructor p ∨g ( p := Blaster.dite' c (fun h : c => e₁) (fun h : ¬ c => e₂) ∧ isCstMatchProp e₁ ∧ isCstMatchProp e₂ ) ∨ ( p := match e₁, ..., eₙ with | p₍₁₎₍₁₎, ..., p₍₁₎₍ₙ₎ => t₁ ... | p₍ₘ₎₍₁₎, ..., p₍ₘ₎₍ₙ₎ => tₘ ∧ ∀ i ∈ [1..m], isCstMatchProp t₁ )

Equations

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

@[inline]

def Blaster.Optimize.allExplicitParamsAreCtor (f : Lean.Expr) (args : Array Lean.Expr) (funPropagation : Bool := false) : TranslateEnvT Bool

Given f x₁ ... xₙ return true when the following conditions are satisfied:

• ∃ i ∈ [1..n], isExplicit xᵢ ∧
• ∀ i ∈ [1..n], isExplicit xᵢ → isCstProp xᵢ ∨ isPropFunType f xₓ with
• isCstProp e := isCstMatchProp e IF funpropagaton isCstProp e := isConstructor e Otherwise
• isPropFunType e := isProp e.Type ∨ isFunType' e.Type NOTE: constructors may contain free variables.

Equations

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

partial def Blaster.Optimize.allExplicitParamsAreCtor.loop (args : Array Lean.Expr) (funPropagation : Bool) (pInfo : FunEnvInfo) (i stop pInfoSize : Nat) (atLeastOneExplicitCstr : Bool := false) : TranslateEnvT Bool

@[inline]

def Blaster.Optimize.allExplicitParamsAreCtor.isFunExpr (e : Lean.Expr) : TranslateEnvT Bool

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Optimize.allExplicitParamsAreCtor.isFunExpr (Lean.Expr.lam binderName binderType body binderInfo) = pure true
• Blaster.Optimize.allExplicitParamsAreCtor.isFunExpr (Lean.Expr.fvar fv) = do let __do_lift ← liftM fv.getType pure (Blaster.Optimize.isFunType' __do_lift)
• Blaster.Optimize.allExplicitParamsAreCtor.isFunExpr (Lean.Expr.const n us) = do let cInfo ← Blaster.Optimize.getConstEnvInfo n pure (Blaster.Optimize.isFunType' cInfo.type)
• Blaster.Optimize.allExplicitParamsAreCtor.isFunExpr e = pure false

@[inline]

def Blaster.Optimize.allExplicitParamsAreCtor.isPropFunType (p : ParamInfo) (e : Lean.Expr) : TranslateEnvT Bool

Equations

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

def Blaster.Optimize.reduceMatch? (f : Lean.Expr) (args : Array Lean.Expr) (mInfo : MatchInfo) : TranslateEnvT (Option Lean.Expr)

Given m := f x₁ ... xₙ with f corresponding to a match function and mInfo the corresponding matcher info, perform the following:

• When ¬ allMatchDiscrsAreCtor x₁ ... xₙ minfo:
  • return none
• When m := b is already in the weak head cache
  • return b
• Otherwise:
• When .reduced e ← reduceMatcher? m
  • update cache with m := some e
  • return some e
• Otherwise
  • update cache with m := none
  • return none Assume that m is a match expression.

Equations

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

@[irreducible]

def Blaster.Optimize.reduceMatch?.allMatchDiscrsAreCtor (args : Array Lean.Expr) (idx stop : Nat) : TranslateEnvT Bool

Equations

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

@[inline]

def Blaster.Optimize.reduceMatch?.commonMatchReduction? (mInfo : MatchInfo) (auxApp : Lean.Expr) (args hs : Array Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Equations

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

def Blaster.Optimize.reduceMatch?.tryReduction? (mInfo : MatchInfo) (args : Array Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Equations

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

def Blaster.Optimize.constMatchPropagation? (cm : Lean.Expr) (cargs : Array Lean.Expr) (mInfo : MatchInfo) : TranslateEnvT (Option Lean.Expr)

Apply the following constant propagation rules on match expressions, such that: Given match₁ e₁, ..., eₙ with | p₍₁₎₍₁₎, ..., p₍₁₎₍ₙ₎ => t₁ ... | p₍ₘ₎₍₁₎, ..., p₍ₘ₎₍ₙ₎ => tₘ

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

• When ∀ i ∈ [1..n], isCstMatchProp eᵢ ∧ ∃ j ∈ [1..n], eⱼ := match₂ f₁, ..., fₚ with | fp₍₁₎₍₁₎, ..., fp₍₁₎₍ₚ₎ => t₁ ... | fp₍ₘ₎₍₁₎, ..., fp₍ₘ₎₍ₚ₎ => tₘ ∧

       ∀ k ∈ [1..m],
        (i ≠ j → g₍ₖ₎₍ᵢ₎ = eᵢ) ∧ (i = j → g₍ₖ₎₍ᵢ₎ = tₖ)
  

  Return match₂ f₁, ..., fₚ with | fp₍₁₎₍₁₎, ..., fp₍₁₎₍ₚ₎ => match₁ g₍₁₎₍₁₎, ..., g₍₁₎₍ₙ₎ with ... ... | fp₍ₘ₎₍₁₎, ..., fp₍ₘ₎₍ₚ₎ => match₁ g₍ₘ₎₍₁₎, ..., g₍ₘ₎₍ₙ₎ with ...

Equations

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

@[irreducible]

def Blaster.Optimize.constMatchPropagation?.loop (cm : Lean.Expr) (cargs : Array Lean.Expr) (mInfo : MatchInfo) (idx stop : Nat) : TranslateEnvT (Option Lean.Expr)

Equations

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

@[irreducible]

def Blaster.Optimize.constMatchPropagation?.allDiscrsAreCstMatch (cargs : Array Lean.Expr) (idx stop : Nat) : TranslateEnvT Bool

Equations

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

def Blaster.Optimize.constMatchPropagation?.pushMatchInLambda (mInfo : MatchInfo) (f : Lean.Expr) (args : Array Lean.Expr) (idxDiscr : Nat) (e : Lean.Expr) : TranslateEnvT Lean.Expr

Equations

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

def Blaster.Optimize.constMatchPropagation?.pushMatchInDIteExpr (mInfo : MatchInfo) (f : Lean.Expr) (args : Array Lean.Expr) (idxDiscr : Nat) (e : Lean.Expr) : TranslateEnvT Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Optimize.constMatchPropagation?.pushMatchInDIteExpr mInfo f args idxDiscr e = Blaster.Optimize.throwEnvError (Lean.toMessageData "pushMatchInDIteExpr: lambda term expected !!!")

@[inline]

def Blaster.Optimize.constMatchPropagation?.isDiteArg (cm : Lean.Expr) (cargs : Array Lean.Expr) (mInfo : MatchInfo) (idx : Nat) : TranslateEnvT (Option Lean.Expr)

Equations

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

@[inline]

def Blaster.Optimize.constMatchPropagation?.isMatchArg (cm : Lean.Expr) (cargs : Array Lean.Expr) (mInfo : MatchInfo) (idx : Nat) : TranslateEnvT (Option Lean.Expr)

Equations

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

@[inline]

def Blaster.Optimize.matchReduction? (f : Lean.Expr) (args : Array Lean.Expr) (mInfo : MatchInfo) : TranslateEnvT (Option Lean.Expr)

Given a match expression try reduceMatch? first and afterwards try constMatchpropagation?.

Equations

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

def Blaster.Optimize.isFVarPattern (e : Lean.Expr) : Bool

Equations

• Blaster.Optimize.isFVarPattern (Lean.Expr.fvar fvarId) = true
• Blaster.Optimize.isFVarPattern (((((Lean.Expr.const `namedPattern us).app _t).app _n).app pe).app _h) = Blaster.Optimize.isFVarPattern pe
• Blaster.Optimize.isFVarPattern e = false

@[inline]

def Blaster.Optimize.optimizeMatchAlt (args : Array Lean.Expr) (mInfo : MatchInfo) (altIdx : Nat) (rhs : Lean.Expr) (stack : List OptimizeStack) : TranslateEnvT (List OptimizeStack)

Given match info mInfo and args the arguments of a match expression of the form: match₁ e₁, ..., eₙ with | p₍₁₎₍₁₎, ..., p₍₁₎₍ₙ₎ => t₁ ... | p₍ₘ₎₍₁₎, ..., p₍ₘ₎₍ₙ₎ => tₘ

Given rhs the current match alternative to be optimized, i.e., p₍ᵢ₎₍₁₎, ..., p₍₁₎₍ₙ₎ => tᵢ and altIdx its index in args, perform the following actions:

• let h := (← get).optEnv.options.matchInContext
• let h1 := h ∪ [ eⱼ := pmᵢ ∪ p₍ᵢ₎₍ⱼ₎ := EqPattern (retrieveAltsArgs #[p₍ᵢ₎₍ⱼ₎]) | j ∈ [1..n] ∧ (h[eⱼ]? = some pmᵢ ∨ pmᵢ = []) ]
• let h2 := h1 ∪ [ eⱼ := pmⱼ ∪ p₍ₖ₎₍ⱼ₎ := NotEqPattern | k ∈ [1..i-1] ∧ ∃! j ∈ [1..n], (h1[eⱼ]? = some pmᵢ ∨ pmᵢ = []) ∧ ¬ isFVarPattern p₍ₖ₎₍ⱼ₎ ]
• let se₁ ... seₚ := [eⱼ | j ∈ [1..n] ∧ isFVar p₍ᵢ₎₍ⱼ₎ ]
• let sp₁ ... spₚ := [p₍ᵢ₎₍ⱼ₎ | j ∈ [1..n] ∧ isFVar p₍ᵢ₎₍ⱼ₎ ]
• withMatchContext h2 $ optimizer tᵢ[sp₁/seᵢ] ... [spₚ/seₚ]

Equations

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

@[irreducible]

def Blaster.Optimize.optimizeMatchAlt.onlyOnePattern (lhs : Array Lean.Expr) (idx : Nat) (onlyOne : Bool) : TranslateEnvT Bool

Equations

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

@[irreducible]

def Blaster.Optimize.optimizeMatchAlt.updateNotEqContext (h : MatchContextMap) (idx start stop : Nat) (args lhs xs : Array Lean.Expr) : TranslateEnvT MatchContextMap

Equations

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

@[irreducible]

def Blaster.Optimize.optimizeMatchAlt.addNotEqPatternToContext (args : Array Lean.Expr) (mInfo : MatchInfo) (alts : Array Lean.Expr) (h : MatchContextMap) (idx stopIdx : Nat) : TranslateEnvT MatchContextMap

Equations

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

def Blaster.Optimize.elimMatch? (mInfo : MatchInfo) (args : Array Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Apply the following reduction rules, such that: Given match₁ e₁, ..., eₙ with | p₍₁₎₍₁₎, ..., p₍₁₎₍ₙ₎ => t₁ ... | p₍ₘ₎₍₁₎, ..., p₍ₘ₎₍ₙ₎ => tₘ

• When ∀ i ∈ [1..m], ¬ tᵢ.hasLooseBVars ∧ tᵢ = t₁

  • return some t₁

• When ∃ i ∈ [1..m], ∀ j ∈ [1..n], eⱼ := pm ∈ matchInContext ∧ p₍ᵢ₎₍ⱼ₎ := EqPattern altArgs ∈ pm ∧ ¬ isFVarPattern p₍ᵢ₎₍ⱼ₎

  • return some tᵢ

• When ∀ j ∈ [1..n], isFVar p₍ₘ₎₍ⱼ₎ ∧ ∀ k ∈ [1..m-1], ∃ h ∈ [1..n], ( eₕ := pm ∈ matchInContext ∧ p₍ₖ₎₍ₕ₎ := NotEqPattern ∈ pm ) - return some tₘ

• Otherwise:

  • return none

Equations

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

@[inline]

def Blaster.Optimize.elimMatch?.commonRhs? (mInfo : MatchInfo) (args : Array Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Equations

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

@[inline]

def Blaster.Optimize.elimMatch?.allPatternsInHyp (mInfo : MatchInfo) (args : Array Lean.Expr) (alt : Lean.Expr) (h : MatchContextMap) : TranslateEnvT (Bool × Array Lean.Expr)

Equations

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

@[inline]

def Blaster.Optimize.elimMatch?.matchInHyps? (mInfo : MatchInfo) (args : Array Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Equations

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

@[inline]

def Blaster.Optimize.elimMatch?.allFVarsPatterns (alt : Lean.Expr) : TranslateEnvT Bool

Equations

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

@[inline]

def Blaster.Optimize.elimMatch?.existsNotEqPattern (mInfo : MatchInfo) (args : Array Lean.Expr) (alt : Lean.Expr) (h : MatchContextMap) : TranslateEnvT Bool

Equations

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

@[inline]

def Blaster.Optimize.elimMatch?.lastPatternReduction? (mInfo : MatchInfo) (args : Array Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Equations

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

def Blaster.Optimize.structEqMatch (f : Lean.Expr) (args : Array Lean.Expr) (mInfo : MatchInfo) : TranslateEnvT (Lean.Expr × Array Lean.Expr)

Given a match application expression of the form f.match_n #[p₁, ..., pₙ, rt, d₁, ..., dₖ, pa₍₁₎₍₁₎ → .. → pa₍₁₎₍ₖ₎ → rhs₁, ..., pa₍ₘ₎₍₁₎ → .. → pa₍ₘ₎₍ₖ₎ → rhsₘ], perform the following actions:

• params ← getImplicitParameters f #[p₁, ..., pₙ]
• let genFVars ← retrieveGenericFVars params
• appType ← genericMatchType (λ (α₁ : Type₁) → λ (αₘ : Typeₘ) → mInfo.instApp p₁, ..., pₙ, rt), with α₁ : Type₁, ..., αₘ : Typeₘ = genFVars
• return g.match.n α₁ ..., αₘ, rt, d₁ ... dₖ pa₍₁₎₍₁₎ → .. → pa₍₁₎₍ₖ₎ → rhs₁ ... pa₍ₘ₎₍₁₎ → .. → pa₍ₘ₎₍ₖ₎ → rhsₘ only when appType := λ (α₁ : Type₁) → λ (αₘ : Typeₘ) → g.match.n q₁ ... qₕ exists in match cache.
• Otherwise, perform the following:
  • Add appType := λ (α₁ : Type₁) → λ (αₘ : Typeₘ) → f.match.n p₁ ... pₙ in match cache
  • return f.match.n p₁, ..., pₙ, rt, d₁ ... dₖ pa₍₁₎₍₁₎ → .. → pa₍₁₎₍ₖ₎ → rhs₁ ... pa₍ₘ₎₍₁₎ → .. → pa₍ₘ₎₍ₖ₎ → rhsₘ Where:
• p₁, ..., pₙ: correspond to the arguments instantiating polymorphic params.
• rt : correspond to the match expression's return type
• d₁, ..., dₖ: correspond to the match expresson discriminators
• pa₍₁₎₍₁₎ → .. → pa₍₁₎₍ₖ₎ → rhs₁, ..., pa₍ₘ₎₍₁₎ → .. → pa₍ₘ₎₍ₖ₎ → rhsₘ: correspond to the rhs for each pattern matching.

Equations

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

def Blaster.Optimize.structEqMatch.genericMatchType (genFVars : Array Lean.Expr) (e : Lean.Expr) : TranslateEnvT Lean.Expr

Equations

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

@[inline]

def Blaster.Optimize.optimizeMatch (f : Lean.Expr) (args : Array Lean.Expr) (mInfo : MatchInfo) (xs : List OptimizeStack) : TranslateEnvT OptimizeContinuity

Apply simplification and normalization rules on match expressions. Assumes that f x₁ ... xₙ is a match application

Equations

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