structure Blaster.Optimize.HypsStackContext : Type

• newHCtx : UpdatedHypContext
• oldHCtx : Option HypothesisContext
• oldCache : Option RewriteCacheMap

structure Blaster.Optimize.MatchStackContext : Type

• oldMatchCtx : MatchContextMap
• oldCache : RewriteCacheMap

structure Blaster.Optimize.LocalDeclStackContext : Type

• newCtx : LocalDeclContext
• oldCtx : LocalDeclContext

instance Blaster.Optimize.instReprHypsStackContext : Repr HypsStackContext

Equations

• Blaster.Optimize.instReprHypsStackContext = { reprPrec := fun (x : Blaster.Optimize.HypsStackContext) (x : Nat) => Std.Format.text "<HypsStackContext>" }

instance Blaster.Optimize.instReprMatchStackContext : Repr MatchStackContext

Equations

• Blaster.Optimize.instReprMatchStackContext = { reprPrec := fun (x : Blaster.Optimize.MatchStackContext) (x : Nat) => Std.Format.text "<MatchStackContext>" }

instance Blaster.Optimize.instReprLocalDeclContext : Repr LocalDeclContext

Equations

• Blaster.Optimize.instReprLocalDeclContext = { reprPrec := fun (x : Blaster.Optimize.LocalDeclContext) (x : Nat) => Std.Format.text "<LocalDeclContext>" }

instance Blaster.Optimize.instReprLocalContext_blaster : Repr Lean.LocalContext

Equations

• Blaster.Optimize.instReprLocalContext_blaster = { reprPrec := fun (x : Lean.LocalContext) (x : Nat) => Std.Format.text "<LocalContext>" }

inductive Blaster.Optimize.OptimizeStack : Type

• InitOptimizeExpr (e : Lean.Expr) : OptimizeStack
• InitOptimizeReturn (e : Lean.Expr) (isGlobal : Bool) : OptimizeStack
• InitOpaqueRecExpr (f : Lean.Expr) (args : Array Lean.Expr) : OptimizeStack
• RecFunDefWaitForStorage (args : Array Lean.Expr) (instApp subsInts : Lean.Expr) (params : ImplicitParameters) : OptimizeStack
• RecFunDefStorage (args : Array Lean.Expr) (instApp subsInts : Lean.Expr) (params : ImplicitParameters) (optBody : Lean.Expr) : OptimizeStack
• ForallWaitForType (n : Lean.Name) (bi : Lean.BinderInfo) (body : Lean.Expr) : OptimizeStack
• ForallWaitForBody (x t : Lean.Expr) (hctx : HypsStackContext) (lctx : LocalDeclContext) : OptimizeStack
• AppWaitForConst (args : Array Lean.Expr) : OptimizeStack
• OptimizeMatchInfoWaitForInst (f : Lean.Expr) (args : Array Lean.Expr) (startArgIdx : Nat) (pInfo : FunEnvInfo) (mInfo : MatcherRecInfo) : OptimizeStack
• AppOptimizeImplicitArgs (f : Lean.Expr) (args : Array Lean.Expr) (idx startArgIdx stopIdx : Nat) (pInfo : FunEnvInfo) : OptimizeStack
• AppOptimizeExplicitArgs (f : Lean.Expr) (args : Array Lean.Expr) (idx stopIdx : Nat) (pInfo : FunEnvInfo) (mInfo : Option MatchInfo) : OptimizeStack
• DiteChoiceWaitForCond (f : Lean.Expr) (args : Array Lean.Expr) (pInfo : FunEnvInfo) (startArgIdx : Nat) : OptimizeStack
• MatchChoiceOptimizeDiscrs (f : Lean.Expr) (args : Array Lean.Expr) (pInfo : FunEnvInfo) (startArgIdx idx : Nat) (mInfo : MatchInfo) : OptimizeStack
• LambdaWaitForType (n : Lean.Name) (bi : Lean.BinderInfo) (body : Lean.Expr) (inDite : Bool) : OptimizeStack
• LambdaWaitForBody (x : Lean.Expr) (lctx : LocalDeclContext) (hctx : Option HypsStackContext) : OptimizeStack
• MatchRhsLambdaWaitForType (n : Lean.Name) (bi : Lean.BinderInfo) (body : Lean.Expr) : OptimizeStack
• MatchRhsLambdaNext (e : Lean.Expr) : OptimizeStack
• MatchRhsLambdaWaitForBody (x : Lean.Expr) (lctx : LocalDeclContext) : OptimizeStack
• MatchAltWaitForExpr (params : Array Lean.Expr) (lctx : LocalDeclContext) (mctx : MatchStackContext) : OptimizeStack
• LetWaitForValue (body : Lean.Expr) : OptimizeStack
• MDataRecCallWaitForExpr (data : Lean.MData) : OptimizeStack
• ProjWaitForExpr (n : Lean.Name) (idx : Nat) : OptimizeStack

def Blaster.Optimize.instReprOptimizeStack.repr : OptimizeStack → Nat → Std.Format

Equations

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

instance Blaster.Optimize.instReprOptimizeStack : Repr OptimizeStack

Equations

• Blaster.Optimize.instReprOptimizeStack = { reprPrec := Blaster.Optimize.instReprOptimizeStack.repr }

@[reducible, inline]

abbrev Blaster.Optimize.OptimizeContinuity : Type

Equations

• Blaster.Optimize.OptimizeContinuity = (List Blaster.Optimize.OptimizeStack ⊕ Lean.Expr)

@[inline]

def Blaster.Optimize.mkHypStackContext (h : UpdatedHypContext) : TranslateEnvT HypsStackContext

Equations

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

@[inline]

def Blaster.Optimize.resetHypContext (h : HypsStackContext) : TranslateEnvT Unit

Equations

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

@[inline]

def Blaster.Optimize.mkMatchStackContext (h : MatchContextMap) : TranslateEnvT MatchStackContext

Equations

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

@[inline]

def Blaster.Optimize.resetMatchContext (h : MatchStackContext) : TranslateEnvT Unit

Equations

• Blaster.Optimize.resetMatchContext h = Blaster.Optimize.updateMatchContext h.oldMatchCtx h.oldCache

@[inline]

def Blaster.Optimize.mkLocalDeclStackContext (newCtx : LocalDeclContext) : TranslateEnvT LocalDeclContext

Equations

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

@[inline]

def Blaster.Optimize.resetLocalDeclContext (oldCtx : LocalDeclContext) : TranslateEnvT Unit

Equations

• Blaster.Optimize.resetLocalDeclContext oldCtx = Blaster.Optimize.updateLocalContext oldCtx

def Blaster.Optimize.stackContinuity (stack : List OptimizeStack) (optExpr : Lean.Expr) (skipCache : Bool := false) : TranslateEnvT OptimizeContinuity

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Optimize.stackContinuity [] optExpr skipCache = pure (Sum.inr optExpr)

@[inline]

def Blaster.Optimize.stackContinuity.hasUnOptMatchInfo? (f : Lean.Expr) : TranslateEnvT (Option (MatcherRecInfo × Lean.Expr))

Given a function f := Expr const n l perform the following:

• When n := mInfo ∈ isMatcherCache (i.e., match info already optimized)
  • return none
• When let some mInfo ← getMatcherRecInfo? n l (i.e., f's generic instance not optimized)
  • return some $ Sum.inr (mInfo, matchFun)
• Otherwise none

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Optimize.stackContinuity.hasUnOptMatchInfo? f = do let __do_lift ← Blaster.Optimize.isMatcher? f if __do_lift.isSome = true then pure none else pure none

@[inline]

def Blaster.Optimize.mkOptimizeContinuity (e : Lean.Expr) (stack : List OptimizeStack) : TranslateEnvT OptimizeContinuity

Equations

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

@[inline]

def Blaster.Optimize.optimizeIfThenElse? (f : Lean.Expr) (args : Array Lean.Expr) (stack : List OptimizeStack) : TranslateEnvT OptimizeContinuity

Apply simplification/normalization rules on Blaster.dite' expressions. Assume that f = Expr.const ``Blaster.dite'.

Equations

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

@[inline]

def Blaster.Optimize.isInOptimizeEnvCache (a : Lean.Expr) (stack : List OptimizeStack) : TranslateEnvT (List OptimizeStack ⊕ OptimizeContinuity)

Equations

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