partial def Blaster.Optimize.optimizeExprAux (stack : List OptimizeStack) : TranslateEnvT Lean.Expr

@[inline]

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

Given e := Expr.fVar fv perform the following:

• When some v := fv.getValue? return Sum.inl (.InitOptimizeExpr v :: stack)`
• Otherwise: return stackContinuity stack (← mkExpr e)`

Equations

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

@[inline]

def Blaster.Optimize.optimizeExprAux.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.optimizeExprAux.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.optimizeExprAux.inlineLet (v body : Lean.Expr) (stack : List OptimizeStack) : List OptimizeStack

Equations

• Blaster.Optimize.optimizeExprAux.inlineLet v body stack = Blaster.Optimize.OptimizeStack.InitOptimizeExpr v :: Blaster.Optimize.OptimizeStack.LetWaitForValue body :: stack

@[inline]

def Blaster.Optimize.optimizeExprAux.optimizeLambda (n : Lean.Name) (t b : Lean.Expr) (bi : Lean.BinderInfo) (xs : List OptimizeStack) (inDite : Bool := false) : List OptimizeStack

Equations

• Blaster.Optimize.optimizeExprAux.optimizeLambda n t b bi xs inDite = Blaster.Optimize.OptimizeStack.InitOptimizeExpr t :: Blaster.Optimize.OptimizeStack.LambdaWaitForType n bi b inDite :: xs

@[inline]

def Blaster.Optimize.optimizeExprAux.optimizeDiteArg (e : Lean.Expr) (stack : List OptimizeStack) : List OptimizeStack

Equations

• Blaster.Optimize.optimizeExprAux.optimizeDiteArg (Lean.Expr.lam n t b bi) stack = Blaster.Optimize.optimizeExprAux.optimizeLambda n t b bi stack true
• Blaster.Optimize.optimizeExprAux.optimizeDiteArg e stack = Blaster.Optimize.OptimizeStack.InitOptimizeExpr e :: stack

@[inline]

def Blaster.Optimize.optimizeExprAux.optimizeExplicitArgs (f : Lean.Expr) (args : Array Lean.Expr) (idx stopIdx : Nat) (pInfo : FunEnvInfo) (mInfo : Option MatchInfo) (stack nxtStack : List OptimizeStack) : TranslateEnvT (List OptimizeStack)

Equations

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

@[inline]

def Blaster.Optimize.optimizeExpr (e : Lean.Expr) : TranslateEnvT Lean.Expr

Equations

• Blaster.Optimize.optimizeExpr e = Blaster.Optimize.optimizeExprAux [Blaster.Optimize.OptimizeStack.InitOptimizeExpr e]

@[inline]

def Blaster.Optimize.optimizeExpr' (e : Lean.Expr) : TranslateEnvT Lean.Expr

Same as optimizeExpr but updates local context before optimizing expression

Equations

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

def Blaster.Optimize.cacheOpaqueRecFun : TranslateEnvT Unit

Populate the recFunInstCache with opaque recursive function definition. This function need to be call before performing optimization on a lean expression. NOTE: This function need to be updated each time we are opacifying a new recursive function.

Equations

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

def Blaster.Optimize.cacheOpaqueRecFun.callOptimize (e : Lean.Expr) : TranslateEnvT Unit

Equations

• Blaster.Optimize.cacheOpaqueRecFun.callOptimize e = discard (Blaster.Optimize.optimizeExprAux [Blaster.Optimize.OptimizeStack.InitOpaqueRecExpr e #[]])

def Blaster.Optimize.Optimize.main (e : Lean.Expr) : TranslateEnvT Lean.Expr

Perform the following actions:

• populate the recFunInstCache with default recursive function definitions.
• optimize expression e

Equations

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

def Blaster.Optimize.command (sOpts : Options.BlasterOptions) (e : Lean.Expr) : Lean.MetaM (Lean.Expr × TranslateEnv)

Optimize an expression using the given solver options.

Parameters

• sOpts: The solver options to use for optimization.
• expr: The expression to be optimized.

Returns

• A tuple containing the optimized expression and the optimization environment. NOTE: This function is to be used only by callOptimize in package Test.

Equations

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