@[inline]

def Blaster.Optimize.getMatchAlts (args : Array Lean.Expr) (mInfo : MatchInfo) : Array Lean.Expr

Equations

• Blaster.Optimize.getMatchAlts args mInfo = Blaster.Optimize.getLambdaBoundedBinderTypes (mInfo.instApp.beta (args.take mInfo.getFirstAltPos)) mInfo.numAlts

def Blaster.Optimize.isCstLiteral (p : Lean.Expr) : Bool

Return true is p is a nat, integer or string literal expression.

Equations

• Blaster.Optimize.isCstLiteral p = ((Blaster.Optimize.isNatValue? p).isSome || (Blaster.Optimize.isIntValue? p).isSome || (Blaster.Optimize.isStrValue? p).isSome)

def Blaster.Optimize.betaReduceRhs (alt : Lean.Expr) (altArgs : Array Lean.Expr) : Lean.Expr

Given a match alternative alt and its corresponding effective arguments altArgs perform beta reduction such that:

• When altArgs.isEmpty
  • return getLambdaBody alt (i.e., no free variables in match pattern)
• otherwise
  • return Expr.beta alt altArgs

Equations

• Blaster.Optimize.betaReduceRhs alt altArgs = if (altArgs.size == 0) = true then Blaster.Optimize.getLambdaBody alt else alt.beta altArgs

structure Blaster.Optimize.AltArgsCache : Type

• patternFreeVars : Array Lean.Expr

  Sequence of named pattern and free variables appearing in each match pattern. The order of appearance for named pattern and free variables are preserved.

• namedPatternEqs : Array Lean.Expr

  Sequence of named pattern equation appearing in each match pattern. The order of appearance is preserved. This sequence is appended to patternFreeVars is reset once a pattern match for a specific match descriminator has been considered.

• nbNamedPatterns : Nat

  Number of named pattern encountered in the match patten.

instance Blaster.Optimize.instInhabitedAltArgsCache : Inhabited AltArgsCache

Equations

• Blaster.Optimize.instInhabitedAltArgsCache = { default := Blaster.Optimize.instInhabitedAltArgsCache.default }

def Blaster.Optimize.instInhabitedAltArgsCache.default : AltArgsCache

Equations

• Blaster.Optimize.instInhabitedAltArgsCache.default = { patternFreeVars := default, namedPatternEqs := default, nbNamedPatterns := default }

@[reducible, inline]

abbrev Blaster.Optimize.AltArgsEnv (α : Type) : Type

Equations

• Blaster.Optimize.AltArgsEnv = StateRefT' IO.RealWorld Blaster.Optimize.AltArgsCache Blaster.Optimize.TranslateEnvT

def Blaster.Optimize.updatePatternVars (fv : Lean.Expr) : AltArgsEnv Unit

Adds fv to patternFreeVars

Equations

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

def Blaster.Optimize.updatePatternEqs (peq : Lean.Expr) : AltArgsEnv Unit

Adds peq to namedPatternEq

Equations

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

def Blaster.Optimize.flushPatternEqs : AltArgsEnv Unit

Performs the following actions:

• Append patternFreeVars with namedPatternEqs
• Increment nbNamedPatterns with namedPatternsEq.size
• Reset namedPatternEqs (i.e., set to empty Array)

Equations

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

structure Blaster.Optimize.AltArgsResult : Type

• altArgs : Array Lean.Expr

  Sequence of named pattern labels, named pattern equations and free variables appearing in each match pattern. The order of appearance for named pattern and free variables are preserved. (see function retrieveAltsArgs).

• nbNamedPatterns : Nat

  Number of named pattern encountered in the match patten.

def Blaster.Optimize.instInhabitedAltArgsResult.default : AltArgsResult

Equations

• Blaster.Optimize.instInhabitedAltArgsResult.default = { altArgs := default, nbNamedPatterns := default }

instance Blaster.Optimize.instInhabitedAltArgsResult : Inhabited AltArgsResult

Equations

• Blaster.Optimize.instInhabitedAltArgsResult = { default := Blaster.Optimize.instInhabitedAltArgsResult.default }

def Blaster.Optimize.retrieveAltsArgs (lhs : Array Lean.Expr) : TranslateEnvT AltArgsResult

Given a sequence of match pattern p₁, ..., pₙ such that each pᵢ may contain named patterns of the form: (namedPattern t₍₁₎₍₁₎ l₍₁₎₍₁₎ (.. (namedPattern t₍₁₎₍ₖ₋₁₎ l₍₁₎₍ₖ₋₁₎ (namedPattern t₍₁₎₍ₖ₎ l₍₁₎₍ₖ₎ e₍₁₎₍ₖ₎ h₍₁₎₍ₖ₎) h₍₁₎₍ₖ₋₁₎) h₍₁₎₍₂₎) h₍₁₎₍₁₎), ..., (namedPattern t₍ₙ₎₍₁₎ l₍ₙ₎₍₁₎ (.. (namedPattern t₍ₙ₎₍ₖ₋₁₎ l₍ₙ₎₍ₖ₋₁₎ (namedPattern t₍ₙ₎₍ₖ₎ l₍ₙ₎₍ₖ₎ e₍ₙ₎₍ₖ₎ h₍ₙ₎₍ₖ₎) h₍ₙ₎₍ₖ₋₁₎) h₍ₙ₎₍₂₎) h₍ₙ₎₍₁₎) with ∀ i ∈ [1..n], ∀ j ∈ [1..k]

• t₍ᵢ₎₍ⱼ₎: corresponding to sort type of the named pattern.
• l₍ᵢ₎₍ⱼ₎: corresponding to the label of the named pattern.
• e₍ᵢ₎₍ⱼ₎: corresponding to the expression of the named pattern that may contain free variables v₍ᵢ₎₍ⱼ₎₍₁₎, ..., v₍ᵢ₎₍ⱼ₎₍ₘ₎.
• h₍ᵢ₎₍ⱼ₎: corresponding to the equality equation of the named pattern. return the following sequence of free variables #[l₍₁₎₍₁₎, v₍₁₎₍₁₎₍₁₎, ..., v₍₁₎₍₁₎₍ₘ₎, l₍₁₎₍₂₎, v₍₁₎₍₂₎₍₁₎, ..., v₍₁₎₍₂₎₍ₘ₎, ..., l₍₁₎₍ₖ₎, v₍₁₎₍ₖ₎₍₁₎, ..., v₍₁₎₍ₖ₎₍ₘ₎, h₍₁₎₍₁₎, ..., h₍₁₎₍ₖ₎, ..., l₍ₙ₎₍₁₎, v₍ₙ₎₍₁₎₍₁₎, ..., v₍ₙ₎₍₁₎₍ₘ₎, l₍ₙ₎₍₂₎, v₍ₙ₎₍₂₎₍₁₎, ..., v₍ₙ₎₍₂₎₍ₘ₎, ..., l₍ₙ₎₍ₖ₎, v₍ₙ₎₍ₖ₎₍₁₎, ..., v₍ₙ₎₍ₖ₎₍ₘ₎, h₍ₙ₎₍₁₎, ..., h₍ₙ₎₍ₖ₎]

Trigger an error if at least one pᵢ does not correspond to:

• A nullary constructor;
• A String/Nat literal;
• A constructor/function application; or
• A named pattern; or
• A free variable.

TODO: change function to pure tail rec call using stack-based approach

Equations

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

partial def Blaster.Optimize.retrieveAltsArgs.visit (e : Lean.Expr) : AltArgsEnv Unit

partial def Blaster.Optimize.removeNamedPatternExpr (p : Lean.Expr) : TranslateEnvT Lean.Expr

Remove all namedPattern expression in p and apply optimizePattern whenever necessary. TODO: change function to pure tail rec call using stack-based approach

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

Equations

• Blaster.Optimize.removeNamedPatternExpr.optimizePattern (Lean.Expr.const `Nat.add us) args = Blaster.Optimize.optimizeNatAdd (Lean.Expr.const `Nat.add us) args
• Blaster.Optimize.removeNamedPatternExpr.optimizePattern (Lean.Expr.const `Int.neg us) args = Blaster.Optimize.optimizeIntNeg (Lean.Expr.const `Int.neg us) args
• Blaster.Optimize.removeNamedPatternExpr.optimizePattern f args = pure (Lean.mkAppN f args)

def Blaster.Optimize.withModifyFVarValue {α : Type} (fv : Lean.FVarId) (v : Lean.Expr) (k : TranslateEnvT α) : TranslateEnvT α

Assign fv to v in the local context and execute k s.t.,

• When fv has a lambda free variable declaration (i.e., LocalDecl.cdecl)
  • replace it with a let free variable declaration (i.e., LocalDecl.ldecl with value set to v)
• When fv is a let free variable declaration only replace the let bind value with v

Equations

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

def Blaster.Optimize.withModifyFVarValue.declModifier (v : Lean.Expr) (d : Lean.LocalDecl) : Lean.LocalDecl

Equations

• Blaster.Optimize.withModifyFVarValue.declModifier v (Lean.LocalDecl.cdecl idx fvarId userName type bi kind) = Lean.LocalDecl.ldecl idx fvarId userName type v false kind
• Blaster.Optimize.withModifyFVarValue.declModifier v (Lean.LocalDecl.ldecl idx fvarId userName type _v nonDep kind) = Lean.LocalDecl.ldecl idx fvarId userName type v nonDep kind

def Blaster.Optimize.isCtorPattern (p : Lean.Expr) : TranslateEnvT (Option (Lean.Name × Array Lean.Expr))

Return some (C, #[xₖ, ..., xₙ]) when p := C x₁ ... xₙ such that:

• C is a ctor name.
• x₁ ... xₖ₋₁ correspond to the polymorphic parameters of the corresponding inductive datatype.

Equations

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

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

Equations

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

def Blaster.Optimize.normMatchExprAux? (idx : Nat) (discrs lhs : Array Lean.Expr) (alt matchType : Lean.Expr) (acc : Option Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Is the accumulator rewriter function to be used with matchExprRewriter when attempting to normalize a match expression to if-then-else (see normMatchExpr?). Asssumes that matchType := λ β₁ => ... => βₘ

Equations

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

def Blaster.Optimize.normMatchExprAux?.removeNamedPatterns (lhs : Array Lean.Expr) : TranslateEnvT (Array Lean.Expr)

Equations

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

def Blaster.Optimize.normMatchExprAux?.isItePattern (discrs : Array Lean.Expr) (argsResult : AltArgsResult) (plhs : Array Lean.Expr) : TranslateEnvT Bool

Return true only when the "match" normalization condition is satisfied, i.e,:

• ∀ i ∈ [1..m], ∀ j ∈ [1..n], ( NoFreeVar(p₍ᵢ₎₍ⱼ₎) ∨ p₍ᵢ₎₍ⱼ₎ = v ∨ isIntNatStrCst(p₍ᵢ₎₍ⱼ₎) ∨ Type(eⱼ) ∈ {Nat, Int} )

Equations

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

def Blaster.Optimize.normMatchExprAux?.mkRhs (discrs 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.normMatchExprAux?.mkIte (matchType : Lean.Expr) (discrs lhs plhs : Array Lean.Expr) (rhs elseExpr : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Equations

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

@[specialize #[]]

def Blaster.Optimize.matchExprRewriter {α : Type} (mInfo : MatchInfo) (args : Array Lean.Expr) (rewriter : Nat → Array Lean.Expr → Array Lean.Expr → Lean.Expr → Lean.Expr → Option α → TranslateEnvT (Option α)) : TranslateEnvT (Option α)

A generic match expression rewriter that given a MatchInfo instance representing a match application, apply the rewriter function on each match pattern. The rewriter function is applied from the last match pattern to the first one. Concretely, given a match expression of the form: match e₁, ..., eₙ with | p₍₁₎₍₁₎, ..., p₍₁₎₍ₙ₎ => t₁ ... | p₍ₘ₎₍₁₎, ..., p₍ₘ₎₍ₙ₎ => tₘ

matchExprRewriter return the following evaluation: rewriter m-1 [e₁, ..., eₙ] [p₍₁₎₍₁₎, ..., p₍₁₎₍ₙ₎] t₁ matchType ... (rewriter 1 [e₁, ..., eₙ] [p₍ₘ₋₁₎₍₁₎, ..., p₍ₘ₋₁₎₍ₙ₎] tₘ₋₁ matchType (rewriter 0 [e₁, ..., eₙ] [p₍ₘ₎₍₁₎, ..., p₍ₘ₎₍ₙ₎] tₘ matchType none)) where,

• matchType := args[mInfo.getFirstDiscrPos - 1]!
• the first application is passed the none accumulator
• the Nat argument corresponding to the traversed index, starting with 0. NOTE: The evaluation stops when at least one of the rewriter invocation return none.

Equations

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

def Blaster.Optimize.matchExprRewriter.commonMatchRewriter {α : Type} (rewriter : Nat → Array Lean.Expr → Array Lean.Expr → Lean.Expr → Lean.Expr → Option α → TranslateEnvT (Option α)) (discrs alts rhs : Array Lean.Expr) (matchType : Lean.Expr) : TranslateEnvT (Option α)

Equations

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

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

Normalize a match expression to if-then-else only when each match pattern is either

• an constructor application that does not contain any free variables (e.g., Nat.zero, some Nat.zero, List.const 0 (List.nil)); or
• a Nat, Int or String literal; or
• a Nat or Int expression; or
• a free variable v

Concretely: match e₁, ..., eₙ with | p₍₁₎₍₁₎, ..., p₍₁₎₍ₙ₎ => t₁ ... | p₍ₘ₎₍₁₎, ..., p₍ₘ₎₍ₙ₎ => tₘ ===> sif h1 : (mkCond e₁ p₍₁₎₍₁₎) ∧ ... ∧ (mkCond eₙ p₍₁₎₍ₙ₎) then (mkRhs [e₁ ... eₙ] [p₍₁₎₍₁₎ ... p₍₁₎₍ₙ₎] t₁) else sif h2 : (mkCond e₁ p₍₂₎₍₁₎) ∧ ... ∧ (mkCond eₙ p₍₂₎₍ₙ₎) then (mkRhs [e₁ ... eₙ] [p₍₂₎₍₁₎ ... p₍₂₎₍ₙ₎] t₂) ... else (mkRhs [e₁ ... eₙ] [p₍ₘ₎₍₁₎ ... p₍ₘ₎₍ₙ₎] tₘ) when:

• ∀ i ∈ [1..m], ∀ j ∈ [1..n], ( NoFreeVar(p₍ᵢ₎₍ⱼ₎) ∨ p₍ᵢ₎₍ⱼ₎ = v ∨ isIntNatStrCst(p₍ᵢ₎₍ⱼ₎) ∨ Type(eⱼ) ∈ {Nat, Int} ) with:

• mkCond e p : let p' ← removeNamedPatternExpr p; := e = p' if (p ≠ v ∧ Type(eᵢ) ∉ {Nat, Int}) ∨ isIntNatStrCst(p) := N ≤ e if p' = N + n ∧ Type(N) = Nat := Int.ofNat 0 ≤ e if p' = Int.ofNat n := (Int.ofNat N ≤ e if p' = Int.ofNat (N + n) := e ≤ -N if p' = Int.Neg (Int.ofNat (N + n)) := True if p' = v := ⊥ otherwise

• mkRhs [e₁ ... eₙ] [p₁ ... pₙ] t : := (mkLet e₁ p₁ ( ... (mkLet eₙ₋₁ ₙ₋₁ (mkLet eₙ pₙ t))))

• mkLet e p t : let t' := t[e/p'] if (isIntNatStrCst(p') ∨ isCtorPattern p') with p' ← (removeNamedPatternExpr p) := t otherwise := let v := e in t' if p = v := t' if p = C (i.e., nullary constructor) := t' if isIntNatStrCst(p) := let n := e in (mkLet n pe t') if p = namedPattern t n pe h ∧ ¬ isIntNatStrCst(pe') ∧ ( Type(eⱼ) ∈ {Nat, Int} ∨ ¬ isCtorPattern pe' ) with pe' ← (removeNamedPatternExpr pe) := let n := pe' in (mkCstLet pe t') if p = namedPattern t n pe h ∧ (isIntNatStrCst(pe') ∨ (Type(eⱼ) ∉ {Nat, Int} ∧ isCtorPattern pe')) with pe' ← (removeNamedPatternExpr pe) := let n := e - N in t' if p = N + n ∧ Type(N) = Nat := let n := e - N in (mkLet n pe t') if p = N + (namedPattern t n pe h) ∧ Type(N) = Nat ∧ ¬ isIntNatStrCst(pe') with pe' ← (removeNamedPatternExpr pe) := let n := pe' in (mkCstLet pe t') if p = N + (namedPattern t n pe h) ∧ Type(N) = Nat ∧ isIntNatStrCst(pe') with pe' ← (removeNamedPatternExpr pe) := let n := Int.toNat e in t' if p = Int.ofNat n := let n := Int.toNat e in (mkLet n pe t') if p = Int.ofNat (namedPattern t n pe t) ∧ ¬ isIntNatStrCst(pe') with pe' ← (removeNamedPatternExpr pe) := let n := pe' in (mkCstLet pe t') if p = Int.ofNat (namedPattern t n pe t) ∧ isIntNatStrCst(pe') with pe' ← (removeNamedPatternExpr pe) := let n := Int.toNat e - N in t' if p = Int.ofNat (N + n) := let n := Int.toNat e - N in (mkLet n pe t') if p = Int.ofNat (N + namedPattern t n pe h) ∧ ¬ isIntNatStrCst(pe') with pe' ← (removeNamedPatternExpr pe) := let n := pe' in (mkCstLet pe t') if p = Int.ofNat (N + namedPattern t n pe h) ∧ isIntNatStrCst(pe') with pe' ← (removeNamedPatternExpr pe) := let n := (Int.toNat (Int.neg e)) - N in t' if p = Int.Neg (Int.ofNat (N + n)) := let n := (Int.toNat (Int.neg e)) - N in (mkLet n pe t') if p = Int.Neg (Int.ofNat (N + namedPattern t n pe h)) ∧ ¬ isIntNatStrCst(pe') with pe' ← (removeNamedPatternExpr pe) := let n := pe' in (mkCstLet n pe t') if p = Int.Neg (Int.ofNat (N + namedPattern t n pe h)) ∧ isIntNatStrCst(pe') with pe' ← (removeNamedPatternExpr pe) := (mkCstLet x₁ (.. (mkCstLet xₖ₋₁ (mkCstLet xₙ t')))) if p = C x₁ ... xₖ := ⊥ otherwise

• mkCstLet e t : := t if e = C := t if isIntNatStrCst(e) := let n := removeNamedPatternExpr pe in (mkCstLet pe t) if e = namedPattern t n pe h := let n := removeNamedPatternExpr pe in (mkCstLet pe t) if e = N + (namedPattern t n pe h) ∧ Type(N) = Nat := (mkCstLet pe t) if e = Int.ofNat pe := (mkCstLet pe t) if e = Int.neg pe := (mkCstLet x₁ (.. (mkCstLet xₖ₋₁ (mkCstLet xₙ t)))) if e = C x₁ ... xₖ := ⊥ otherwise

Equations

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