@[inline]

def Blaster.Optimize.mapTranslateEnvT {m : Type → Type u_1} {β : Sort u_2} [MonadControlT TranslateEnvT m] [Monad m] (f : {α : Type} → (β → TranslateEnvT α) → TranslateEnvT α) {α : Type} (k : β → m α) : m α

Equations

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

@[inline]

def Blaster.Optimize.map2TranslateEnvT {m : Type → Type u_1} {β : Sort u_2} {γ : Sort u_3} [MonadControlT TranslateEnvT m] [Monad m] (f : {α : Type} → (β → γ → TranslateEnvT α) → TranslateEnvT α) {α : Type} (k : β → γ → m α) : m α

Equations

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

@[inline]

def Blaster.Optimize.isClassConstraint? (n : Lean.Name) : TranslateEnvT (Option Lean.Name)

Return some className if n corresponds to a class or is transitively an abbrevation to a class definition (e.g., DecidableEq, DecidableLT, DecidableRel, etc).

Equations

• Blaster.Optimize.isClassConstraint? n = do let __do_lift ← Blaster.Optimize.isClassConstraint n if __do_lift = true then pure (some n) else pure none

@[inline]

def Blaster.Optimize.isClassConstraintExpr? (e : Lean.Expr) : TranslateEnvT (Option Lean.Name)

Return true if e corresponds to a class constraint expression (see function isClassConstraint).

Equations

• Blaster.Optimize.isClassConstraintExpr? e = match e.getAppFn' with | Lean.Expr.const n us => Blaster.Optimize.isClassConstraint? n | x => pure none

structure Blaster.Optimize.TelescopeEnv : Type

• lctx : Lean.LocalContext
• localInsts : Lean.LocalInstances
• fvars : Array Lean.Expr

@[reducible, inline]

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

Equations

• Blaster.Optimize.TelescopeEnvT = StateRefT' IO.RealWorld Blaster.Optimize.TelescopeEnv Blaster.Optimize.TranslateEnvT

@[inline]

def Blaster.Optimize.forallTelescope {n : Type → Type u_1} [MonadControlT TranslateEnvT n] [Monad n] {α : Type} (type : Lean.Expr) (k : Array Lean.Expr → Lean.Expr → n α) : n α

Given type of the form forall xs, A, execute k xs A. This combinator will declare local declarations, create free variables for them, execute k with updated local context, and make sure the cache is restored after executing k.

Equations

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

@[inline]

def Blaster.Optimize.forallBoundedTelescope {n : Type → Type u_1} [MonadControlT TranslateEnvT n] [Monad n] {α : Type} (type : Lean.Expr) (maxFVars : Nat) (k : Array Lean.Expr → Lean.Expr → n α) : n α

Similar to forallTelescope, stops constructing the telescope when it reaches size maxFVars.

Equations

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

@[inline]

def Blaster.Optimize.lambdaTelescope {n : Type → Type u_1} [MonadControlT TranslateEnvT n] [Monad n] {α : Type} (e : Lean.Expr) (k : Array Lean.Expr → Lean.Expr → n α) : n α

Given e of the form fun ..xs => A, execute k xs A. This combinator will declare local declarations, create free variables for them, execute k with updated local context, and make sure the cache is restored after executing k.

Equations

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

@[inline]

def Blaster.Optimize.lambdaBoundedTelescope {n : Type → Type u_1} [MonadControlT TranslateEnvT n] [Monad n] {α : Type} (e : Lean.Expr) (maxFVars : Nat) (k : Array Lean.Expr → Lean.Expr → n α) : n α

Given e of the form fun ..xs ..ys => A, execute k xs (fun ..ys => A) where xs.size ≤ maxFVars. This combinator will declare local declarations, create free variables for them, execute k with updated local context, and make sure the cache is restored after executing k.

Equations

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

@[inline]

def Blaster.Optimize.withLocalDecl' {n : Type → Type u_1} [MonadControlT TranslateEnvT n] [Monad n] {α : Type} (name : Lean.Name) (bi : Lean.BinderInfo) (type : Lean.Expr) (k : Lean.Expr → n α) : n α

Same as default withLocalDecl but rests heartbeats.

Equations

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

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

Eta expand the given expression. Example:

etaExpand (mkConst ``Nat.add)

produces fun x y => Nat.add x y

Equations

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

@[inline]

def Blaster.Optimize.applyOnLambdaBody (e : Lean.Expr) (f : Lean.Expr → TranslateEnvT Lean.Expr) : TranslateEnvT Lean.Expr

Given e of the form λ (a₁ : α₁) → ... → λ (aₙ : αₙ) → b, return λ (a₁ : α₁) → ... → λ (aₙ : αₙ) → f b. NOTE: This function can be used only it is guaranteed the modifications induced by f will not break the de-bruijn indices. E.g.,

• f b ===> b * 2
• f b ===> b x₁ ... xₙ s.t., x₁ .. xₙ don't have any bounded variables.
• etc

Equations

• Blaster.Optimize.applyOnLambdaBody e f = Blaster.Optimize.applyOnLambdaBodyImp✝ e none f

@[inline]

def Blaster.Optimize.applyOnLambdaBoundedBody (e : Lean.Expr) (maxBinders : Nat) (f : Lean.Expr → TranslateEnvT Lean.Expr) : TranslateEnvT Lean.Expr

Given e of the form λ (a₁ : α₁) → ... → λ (aₙ : αₙ) → b, return λ (a₁ : α₁) → f λ (aₖ : αₖ → ... → λ (aₙ : αₙ) where k < maxBinders NOTE: This function can be used only it is guaranteed the modifications induced by f will not break the de-bruijn indices. E.g.,

• f b ===> b * 2
• f b ===> b x₁ ... xₙ s.t., x₁ .. xₙ don't have any bounded variables.
• etc

Equations

• Blaster.Optimize.applyOnLambdaBoundedBody e maxBinders f = Blaster.Optimize.applyOnLambdaBodyImp✝ e (some maxBinders) f

@[inline]

def Blaster.Optimize.getLambdaBoundedBinderTypes (e : Lean.Expr) (maxTypes : Nat) : Array Lean.Expr

Given a sequence of nested lambdas (a₁ : α₁) → ... → (aₙ : αₙ) → _, perform the following:

• let k = maxTypes
• return #[α₁ ... αₖ] Note: Dependent types are instantiated (whenever necessary).

Equations

• Blaster.Optimize.getLambdaBoundedBinderTypes e maxTypes = Blaster.Optimize.getLambdaBinderTypesImp✝ e (some maxTypes)

@[inline]

def Blaster.Optimize.getLambdaBinderTypes (e : Lean.Expr) : Array Lean.Expr

Given a sequence of nested lambdas (a₁ : α₁) → ... → (aₙ : αₙ) → _, return #[α₁ ... αₙ]. Note: Dependent types are instantiated (whenever necessary).

Equations

• Blaster.Optimize.getLambdaBinderTypes e = Blaster.Optimize.getLambdaBinderTypesImp✝ e none

@[inline]

def Blaster.Optimize.ParamInfo.isExplicit (p : ParamInfo) : Bool

Equations

• p.isExplicit = p.binderInfo.isExplicit

def Blaster.Optimize.getFunEnvInfo (f : Lean.Expr) : TranslateEnvT FunEnvInfo

Return pInfo when f := pInfo ∈ getFunEnvInfoCache. Otherwise, performing the following

• Let v₁ : t₁ → .. → vₙ : tₙ := inferTypeEnv f
• Let p := #[ { binderInfo := declᵢ.binderInfo, isProp := ← isProp declᵢ.type } | ∀ i ∈ [1..n-1], declᵢ ← getFVarLocalDecl vᵢ ]
• Let pInfo := { paramsInfo := p, type := v₁ : t₁ → .. → vₙ : tₙ }
• add f := pInfo to getFunEnvInfoCache
• return pInfo

Equations

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

def Blaster.Optimize.inferFunType (t : Lean.Expr) (args : Array Lean.Expr) : Lean.Expr

Given t := ∀ α₀ → ∀ α₂ → ... → αₙ corresponding to function type and x₁ ... xₘ the function's applied arguments, determine the instantiated fun type by properly instantiating the implicit arguments.

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

Equations

• Blaster.Optimize.inferFunType t args = Blaster.Optimize.inferFunType.visit args 0 args.size t

partial def Blaster.Optimize.inferFunType.visit (args : Array Lean.Expr) (idx stop : Nat) (e : Lean.Expr) : Lean.Expr

def Blaster.Optimize.inferAppType (t : Lean.Expr) (args : Array Lean.Expr) : Lean.Expr

Given t := ∀ α₀ → ∀ α₂ → ... → αₙ corresponding to function type and x₁ ... xₘ the function's applied arguments, determine the application type by properly instantiating the implicit arguments.

Equations

• Blaster.Optimize.inferAppType t args = Blaster.Optimize.inferAppType.visit args 0 args.size t

partial def Blaster.Optimize.inferAppType.visit (args : Array Lean.Expr) (idx stop : Nat) (t : Lean.Expr) : Lean.Expr

def Blaster.Optimize.hasImplicitArgs (f : Lean.Expr) : TranslateEnvT Bool

Given a f : Expr.const n l a function name expression, return true if f has at least one implicit argument.

Equations

• Blaster.Optimize.hasImplicitArgs f = do let fInfo ← Blaster.Optimize.getFunEnvInfo f pure (fInfo.paramsInfo.any fun (p : Blaster.Optimize.ParamInfo) => !p.isExplicit)

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

Given application f x₀ ... xₙ, return the following sequence: let A := [x₀ ... xₙ] let instanceArgs := [ { implicitArg := A[i], isInstance := ¬ isExplicit A[i], isGeneric := isGenericParam A[i], idxArg := i} | i ∈ [0..n] ] return instanceArgs NOTE: It is also assumed that args does not contain any meta or bounded variables.

Equations

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

def Blaster.Optimize.getInstApp (f : Lean.Expr) (params : ImplicitParameters) : TranslateEnvT Lean.Expr

Given function f and params its implicit parameter info (see getImplicitParameters), perform the following: let instanceArgs := [ params[i] | i ∈ [0..params.size-1] ∧ params[i].isInstance ] let genFVars ← retrieveGenericFVars params

• When instanceArgs.isEmpty
  • return f
• Otherwise:
  • When instanceArgs.size == params.size (i.e., only implicit arguments provided)
    • return mkLambdaFVars genFVars f
  • Otherwise:
    • return mkLambdaFVars genFVars (specializeLambda (← etaExpand f) params)

Equations

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