structure Blaster.Optimize.IndTypeDeclaration : Type

Type to cache inductive datatype instances and quantified functions that have already been translated.

• instName : Smt.SmtSymbol

  Unique name generated for datatype instance/quantified functions.

  • E.g., Given datatype instances List T1 and List T2, names List_<id1> and List_<id2> will respectively be generated,

  • E.g., Given two quantified functions f1 : Int → Bool and f2 : Nat -> Bool, names Fun_<id1> and Fun_<id2> will respectively be generated. where <idX> is a Nat literal.

  This unique name is mainly used when generating the corresponding smt predicate qualifier for the datatype instance/quantified functions, that is required to specify the expected domain values for quantified variables.

  NOTE: Two (or more) polymorphic instances for an inductive datatype will generate the same name (see function getIndInst in Translate.Qualifier).

  • E.g., List α and List β will both have the same predicate qualifier name.

  NOTE: Two (or more) polymorphic quantified function will generate the same name (see function getFunInstDecl in Translate.Qualifier).

  • E.g., f1 : α → Nat and f2 : β → Nat will both have the same predicate qualifier name.

  NOTE: Polymorphic instances are detected transitively,

  • E.g., List (Option α) and List (Option β) will both generate the same predicate qualifier name.
  • E.g., f1 : Term (List α) → Nat and f2 : Term (List β) → Nat will both generate the same predicate qualifier name.
• instSort : Smt.SortExpr

  Corresponding Smt instantiated sort for the inductive datatype instance, E.g., (List Int) for instance List Int.

• applyInstName : Option Smt.SmtSymbol

  unique @apply function generated for each HOF/quantified function or lambda term.

def Blaster.Optimize.instInhabitedIndTypeDeclaration.default : IndTypeDeclaration

Equations

• Blaster.Optimize.instInhabitedIndTypeDeclaration.default = { instName := default, instSort := default, applyInstName := default }

instance Blaster.Optimize.instInhabitedIndTypeDeclaration : Inhabited IndTypeDeclaration

Equations

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

instance Blaster.Optimize.instReprIndTypeDeclaration : Repr IndTypeDeclaration

Equations

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

structure Blaster.Optimize.OptimizeOptions : Type

• normalizeFunCall : Bool

  Flag to activate function normalization, e.g., Nat.beq x y to BEq.beq Nat instBEqNat x y. This flag is set to false when optimizing the recursive function body.

• inFunApp : Bool

  Flag set to true only when optimizing function name f in expression f x₁ ... xₙ. This is to avoid applying optimization twice on the body of non-recursive functions.

• mcDepth : Nat

  Keep track of the analysis Step reached for bmc and k-induction.

• solverOptions : Options.BlasterOptions

  Options passed to the #solve command.

instance Blaster.Optimize.instInhabitedOptimizeOptions : Inhabited OptimizeOptions

Equations

• Blaster.Optimize.instInhabitedOptimizeOptions = { default := { mcDepth := 0, solverOptions := default } }

inductive Blaster.Optimize.MatchEntry : Type

• EqPattern (altArgs : Array Lean.Expr) : MatchEntry

  instanitated alternative arguments for current match pattern when discriminator matches pattern

• NotEqPattern : MatchEntry

  Constructor used when discriminator does not match current pattern in match context

instance Blaster.Optimize.instReprMatchEntry : Repr MatchEntry

Equations

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

def Blaster.Optimize.instReprMatchEntry.repr : MatchEntry → Nat → Std.Format

Equations

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

@[reducible, inline]

abbrev Blaster.Optimize.HypothesisMap : Type

Equations

• Blaster.Optimize.HypothesisMap = Std.HashMap Lean.Expr Lean.Expr

@[reducible, inline]

abbrev Blaster.Optimize.RewriteCacheMap : Type

Equations

• Blaster.Optimize.RewriteCacheMap = Std.HashMap Lean.Expr Lean.Expr

@[reducible, inline]

abbrev Blaster.Optimize.MatchEntryMap : Type

Equations

• Blaster.Optimize.MatchEntryMap = Std.HashMap Lean.Expr Blaster.Optimize.MatchEntry

@[reducible, inline]

abbrev Blaster.Optimize.MatchContextMap : Type

Equations

• Blaster.Optimize.MatchContextMap = Std.HashMap Lean.Expr Blaster.Optimize.MatchEntryMap

@[reducible, inline]

abbrev Blaster.Optimize.EqualityMap : Type

Equations

• Blaster.Optimize.EqualityMap = Std.HashMap Lean.Expr Lean.Expr

structure Blaster.Optimize.HypothesisContext : Type

Type to keep hypothesis context

• hypothesisMap : HypothesisMap

  Map keeping track of hypotheses introduced by implications/ite. Given an implication of the form h : a → b, the following entries are introduced in this map:

  • a := h ∈ hypothesisMap
  • When a := e₁ ∧ e₂
    • e₁ := Blaster.and_left e₁ e₂ h ∈ hypothesisMap
    • e₂ := Blaster.and_right e₁ e₂ h ∈ hypothesisMap The Map is populated only when Type(a) = Prop. The updated Map is considered only when optimizing b, which may also be an implication. (see addHypotheses function and optimizeForall rule).
• equalityMap : EqualityMap

  Map keeping track of equality introduced by implications/ite. An entry in this map is expected to be one of the following forms:

  • fv := Expr
  • Expr := C
  • Expr := C x₁ ... xₙ Any occurrence of the key for a given context is replaced by the rhs value.

instance Blaster.Optimize.instReprHypothesisContext : Repr HypothesisContext

Equations

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

def Blaster.Optimize.instReprHypothesisContext.repr : HypothesisContext → Nat → Std.Format

Equations

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

instance Blaster.Optimize.instInhabitedHypothesisContext : Inhabited HypothesisContext

Equations

• Blaster.Optimize.instInhabitedHypothesisContext = { default := { hypothesisMap := Std.HashMap.emptyWithCapacity, equalityMap := Std.HashMap.emptyWithCapacity } }

structure Blaster.Optimize.ParamInfo : Type

Type to keep parameter info for a given function

• binderInfo : Lean.BinderInfo

  The binder annotation for the parameter.

• isProp : Bool

  Flag set to true when parameter type is a Prop

def Blaster.Optimize.instInhabitedParamInfo.default : ParamInfo

Equations

• Blaster.Optimize.instInhabitedParamInfo.default = { binderInfo := default, isProp := default }

instance Blaster.Optimize.instInhabitedParamInfo : Inhabited ParamInfo

Equations

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

def Blaster.Optimize.instReprParamInfo.repr : ParamInfo → Nat → Std.Format

Equations

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

instance Blaster.Optimize.instReprParamInfo : Repr ParamInfo

Equations

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

structure Blaster.Optimize.FunEnvInfo : Type

• paramsInfo : Array ParamInfo

  Parameters Info for current function

• type : Lean.Expr

  Generic Function Type

def Blaster.Optimize.instInhabitedFunEnvInfo.default : FunEnvInfo

Equations

• Blaster.Optimize.instInhabitedFunEnvInfo.default = { paramsInfo := default, type := default }

instance Blaster.Optimize.instInhabitedFunEnvInfo : Inhabited FunEnvInfo

Equations

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

instance Blaster.Optimize.instReprFunEnvInfo : Repr FunEnvInfo

Equations

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

def Blaster.Optimize.instReprFunEnvInfo.repr : FunEnvInfo → Nat → Std.Format

Equations

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

structure Blaster.Optimize.MemoizeEnv : Type

Type defining the memoization cache for internally demanding functions.

• isRecFunCache : Std.HashMap Lean.Name Bool

  Cache memoizing the isRecursiveFun result

• isInstanceCache : Std.HashMap Lean.Name Bool

  Cache memoizing the isInstance result

• isClassCache : Std.HashMap Lean.Name Bool

  Cache memoizing the isClassConstraint result

• isInductiveCache : Std.HashMap Lean.Name Bool

  Cache memoizing the isInductiveType result

• isResolvableCache : Std.HashMap Lean.Expr Bool

  Cache memoizing the isResolvableType result

• getMatcherCache : Std.HashMap Lean.Name (Option MatcherRecInfo)

  Cache memoizing the getMatcherRecInfo? result

• getConstInfoCache : Std.HashMap Lean.Name Lean.ConstantInfo

  Cache memoizing the getConstInfo result

• inferTypeCache : Std.HashMap Lean.Expr Lean.Expr

  Cache memoizing the inferType result

• isMatcherCache : Std.HashMap Lean.Name MatchInfo

  Cache memoizing MatchInfo

• isPartialCache : Std.HashMap Lean.Name Bool

  Cache memoizing isPartialDef

• getFunEnvInfoCache : Std.HashMap Lean.Expr FunEnvInfo

  Cache memoizing getFunEnvInfo result

• isCstMatchPropCache : Std.HashMap Lean.Expr Bool

  Cache memoizing isCstMatchProp result

• getFunBodyCache : Std.HashMap Lean.Expr (Option Lean.Expr)

  Cache memoizing getFunBody result

• isPropCache : Std.HashMap Lean.Expr Bool

  Cache memoizing isProp result

• isMatchToIte : Std.HashMap Lean.Name Bool

  Cache memoizing match to ite normalization

• isNotFunCache : Std.HashMap Lean.Expr Bool

  Cache memoizing isNotFun result

• isTypeCache : Std.HashMap Lean.Expr Bool

  Cache memoizing isType result.

instance Blaster.Optimize.instInhabitedMemoizeEnv : Inhabited MemoizeEnv

Equations

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

structure Blaster.Optimize.LocalDeclContext : Type

• ctx : Lean.LocalContext

  local lean context updated when optimizing lambda and forall expression

• localInsts : Lean.LocalInstances

  local instances updated when optimizing lambda and forall expression

instance Blaster.Optimize.instInhabitedLocalDeclContext : Inhabited LocalDeclContext

Equations

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

def Blaster.Optimize.instInhabitedLocalDeclContext.default : LocalDeclContext

Equations

• Blaster.Optimize.instInhabitedLocalDeclContext.default = { ctx := default, localInsts := default }

structure Blaster.Optimize.OptimizeEnv : Type

Type defining the environment used when optimizing a lean theorem.

• globalRewriteCache : RewriteCacheMap

  Cache memoizing the normalization and rewriting performed on the lean theorem according to a given context.

• localRewriteCache : RewriteCacheMap
• synthInstanceCache : Std.HashMap Lean.Expr (Option Lean.Expr)

  Cache memoizing synthesized instances for Inhabited/LawfulBEq constraint.

• whnfCache : Std.HashMap Lean.Expr (Option Lean.Expr)

  Cache memoizing the whnf result.

• matchCache : Std.HashMap Lean.Expr Lean.Expr

  Cache memoizing type for a match application of the form f.match.n [p₁, ..., pₙ, d₁, ..., dₖ,, pa₍₁₎₍₁₎ → .. → pa₍₁₎₍ₖ₎ → rhs₁, ..., pa₍ₘ₎₍₁₎ → .. → pa₍ₘ₎₍ₖ₎ → rhsₘ], s.t.: An entry in this map is expected to be of the form Type(f.match.n [p₁, ..., pₙ]) := fun.match.n p₁ ... pₙwhere,p₁, ..., pₙcorrespond to the arguments instantiating polymorphic params. This is used to determine equivalence between match functions (see functionstructEqMatch?`).

• recFunInstCache : Std.HashMap Lean.Expr Lean.Expr

  Cache memoizing instances of recursive functions. An entry in this map is expected to be of the form f x₁ ... xₙ := fdef, where:

  • x₁ .. xₙ: correspond to the arguments instantiating the polymorphic parameters of f (if any).
  • fdef: correspond to the recursive function body. TODO: UPDATE SPEC
• recFunCache : Std.HashSet Lean.Expr

  Cache keeping track of visited recursive function. Note that we here keep track of each instantiated polymorphic function.

• recFunMap : Std.HashMap Lean.Expr Lean.Expr

  Map to keep the normalized definition for each recursive function, which is also used to determine structural equivalence between functions (see function storeRecFunDef).

• hypothesisContext : HypothesisContext

  Hypothesis context that is populated whether an implication or ite is encountered. The context is used only when optimization the implication's body or the then/else term of an ite.

• matchInContext : MatchContextMap

  Map keeping track of match patterns when optimizing a match rhs. Given a match expression of the form: match₁ e₁, ..., eₙ with | p₍₁₎₍₁₎, ..., p₍₁₎₍ₙ₎ => t₁ x₁ ... xₙ ... | p₍ₘ₎₍₁₎, ..., p₍ₘ₎₍ₙ₎ => tₘ x₁ ... xₙ The following entries are introduced in this map context for each tᵢ:

  • ∀ j ∈ [1..n], p₍ᵢ₎₍ⱼ₎ = eⱼ := (← retrieveAltsArgs #[p₍ᵢ₎₍ⱼ₎]).altArgs ∈ matchInContext (see optimizeMatchAlt function).

  NOTE: The updated Map context is considered only when optimizing each tᵢ.

• memCache : MemoizeEnv

  Memoization maps (see not on MemoizeEnv)

• options : OptimizeOptions

  Optimization options (see note on OptimizeOptions)

• restart : Bool

  Flag to be set to true when there is a need to apply optimization again on a given expression.

• ctx : LocalDeclContext

  local declaration context

instance Blaster.Optimize.instInhabitedOptimizeEnv : Inhabited OptimizeEnv

Equations

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

structure Blaster.Optimize.TranslateOptions : Type

• typeUniverse : Bool

  Flag set when universe @@Type has already been declared in Smt instance.

• arrowTypeArities : Std.HashMap Nat Smt.SmtSymbol

  Cache keeping track of ArrowTN already declared in Smt instance, with N corresponding to the function arity.

• inPatternMatching : Std.HashSet Lean.FVarId

  Set keeping track of all variables in matched terms, including named patterns. This set is provided only when translating matched terms and match rhs.

• axiomMap : Std.HashMap Lean.Name Smt.SmtSymbol

  Map keeping track of axioms not of type Prop or opaque variables, encountered during translation. This set is used mainly to avoid multiple global declaration in the Smt instance.

instance Blaster.Optimize.instInhabitedTranslateOptions : Inhabited TranslateOptions

Equations

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

@[reducible, inline]

abbrev Blaster.Optimize.TopLevelVars : Type

Equations

• Blaster.Optimize.TopLevelVars = Array (List (Blaster.Smt.SmtSymbol × Lean.Name))

structure Blaster.Optimize.SmtEnv : Type

Type defining the environment used when translating to Smt-Lib.

• translateCache : Std.HashMap Lean.Expr Smt.SmtTerm

  Cache memoizing the translation to Smt-Lib term.

• smtCommands : Array Smt.SmtCommand

  Smt-Lib commands emitted to the backend solver.

• smtProc : Option (IO.Process.Child { stdin := IO.Process.Stdio.piped, stdout := IO.Process.Stdio.piped, stderr := IO.Process.Stdio.piped })

  Backend solver process.

• indTypeVisited : Std.HashSet Lean.Name

  Cache keeping track of visited inductive datatype during translation.

• indTypeInstCache : Std.HashMap Lean.Expr IndTypeDeclaration

  Map to keep inductive datatype instances and quantified functions that has already been translated. An entry in this map may correspond to one of the following:

  • Given d the name of an inductive data type and x₀ ... xₙ its corresponding arguments (if any):

    • When ∀ i ∈ [0..n], ¬ isGenericParam xᵢ, d x₁ ... xₙ := {instName := n, instSort := (sd sx₀ .. sxₙ)} ∈ indTypeInstCache
    • when ∃ i ∈ [0..n], isGenericParam xᵢ, λ b₀ → .. → bₘ → t x₀ ... xₙ := {instName := n, instSort := (sd sx₀ .. sxₙ)}` ∈ indTypeInstCache with
      • b₀ .. bₘ corresponding to the polymorphic arguments (see getIndInst).

  • Given f : α₀ → α₁ ... → αₙ a quantified function:

    • When ∀ i ∈ [0..n], ¬ isGenericParam αᵢ, α₀ → α₁ ... → αₙ := {instName := n, instSort := (Array sα₀ sα₁ ... sαₙ)} ∈ indTypeInstCache
    • When ∃ i ∈ [0..n], isGenericParam αᵢ, λ b₀ → .. → bₘ → α₀ → ... → α := {instName := n, instSort := (Array sα₀ ... sαₙ)} ∈ indTypeInstCache with
      • b₀ .. bₘ corresponding to the polymorphic arguments (see getFunInstDecl). See note on IndTypeDeclaration.
• funInstCache : Std.HashMap Lean.Expr Smt.SmtQualifiedIdent

  Cache keeping track of opaque functions, recursive function instances as well as undefined class functions that have already been translated. An entry in this map is expected to be of the form f x₁ ... xₙ := n, where:

  • x₁ .. xₙ: correspond to the arguments instantiating the polymorphic parameters of f (if any).
  • n corresponds an smt qualified identifier that is expected to be unique for each recursive function or undefined class function instances. TODO: UPDATE SPEC
• sortCache : Std.HashMap Lean.FVarId Smt.SmtSymbol

  Cache keeping track of sort that have already been declared.

• fvarsCache : Std.HashMap Lean.FVarId Nat

  Hash keeping track of all translated fvars. (see function fvarIdToSmtSymbol)

• quantifiedFVars : Std.HashMap Lean.FVarId Bool

  Hash keeping track of quantified fvars. This is essential to detect globally declared variables. The bool flag is set to true for globally declared variables or for top level forall quantifiers.

• topLevelVars : TopLevelVars

  Array list keeping track of globally declared variables and the ones in the top level forall quantifier. This list is used exclusively when retrieving counterexample after a sat result is obtained from the backend smt solver. The Array index indicates the analysis step at which the variables where introduced.

• symbolStrCache : Std.HashMap Smt.SmtSymbol String

  Cache memoizing the string representation for an Smt Symbol

• funCtorCache : Std.HashMap Lean.Name FunEnvInfo

  Hash Map keeping the FunEnvInfo for functions defined as Ctor arguments An entry in this Map will correspond to {ctor}.{idx} := f ∈ funCtorCache Where ctor is the name of the ctor and idx the index label generated at the smt level. Example, Given structure Ratio where numerator : Int denominator : Int The corresponding smt datatype declaration will be:

  • (declare-datatype @Tests.Uplc.Onchain.Ratio ( (Tests.Uplc.Onchain.Ratio.mk (Tests.Uplc.Onchain.Ratio.mk.1 Int) (Tests.Uplc.Onchain.Ratio.mk.2 Int)) ) ) where
  • {ctor} = Tests.Uplc.Onchain.Ratio.mk
  • {idx} ∈ [1, 2]
• options : TranslateOptions

  Translation options (see note on TranslateOptions)

instance Blaster.Optimize.instInhabitedSmtEnv : Inhabited SmtEnv

Equations

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

structure Blaster.Optimize.TranslateEnv : Type

Type defining the environment used when optimizing a lean theorem and translating to Smt-lib.

• smtEnv : SmtEnv

  Environment used when translating to Smt-ling.

• optEnv : OptimizeEnv

  Environment used when optimization a lean expression.

instance Blaster.Optimize.instInhabitedTranslateEnv : Inhabited TranslateEnv

Equations

• Blaster.Optimize.instInhabitedTranslateEnv = { default := { smtEnv := default, optEnv := default } }

@[reducible, inline]

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

Equations

• Blaster.Optimize.TranslateEnvT = StateRefT' IO.RealWorld Blaster.Optimize.TranslateEnv Lean.MetaM

def Blaster.Optimize.getMCtx' : Lean.MetaM Lean.MetavarContext

Equations

• Blaster.Optimize.getMCtx' = do let __do_lift ← get pure __do_lift.mctx

def Blaster.Optimize.modifyMCtx' (f : Lean.MetavarContext → Lean.MetavarContext) : Lean.MetaM Unit

Equations

• Blaster.Optimize.modifyMCtx' f = Lean.modifyMCtx f

instance Blaster.Optimize.instMonadMCtxTranslateEnvT : Lean.MonadMCtx TranslateEnvT

Equations

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

def Blaster.Optimize.throwEnvError {α : Type} (msg : Lean.MessageData) : TranslateEnvT α

Equations

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

def Blaster.Optimize.termThrowEnvError__ : Lean.ParserDescr

macro throwEnvError to avoid applying format on msg before throwEnvError is called

Equations

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

def Blaster.Optimize.getAppFnWithArgsAux : Lean.Expr → Array Lean.Expr → Nat → Lean.Expr × Array Lean.Expr

Equations

• Blaster.Optimize.getAppFnWithArgsAux (f.app a) x✝¹ x✝ = Blaster.Optimize.getAppFnWithArgsAux f (x✝¹.set! x✝ a) (x✝ - 1)
• Blaster.Optimize.getAppFnWithArgsAux x✝² x✝¹ x✝ = (x✝², x✝¹)

@[inline]

def Blaster.Optimize.getAppFnWithArgs (e : Lean.Expr) : Lean.Expr × Array Lean.Expr

Return a function and its arguments

Equations

• Blaster.Optimize.getAppFnWithArgs e = Blaster.Optimize.getAppFnWithArgsAux e (Array.replicate e.getAppNumArgs (Lean.mkSort Lean.levelZero)) (e.getAppNumArgs - 1)

@[inline]

def Blaster.Optimize.getCurrentDepth : TranslateEnvT Nat

Return the current analysis Step

Equations

• Blaster.Optimize.getCurrentDepth = do let __do_lift ← get pure __do_lift.optEnv.options.mcDepth

@[inline]

def Blaster.Optimize.setRestart : TranslateEnvT Unit

set restart flag to true.

Equations

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

@[inline]

def Blaster.Optimize.resetRestart : TranslateEnvT Unit

reset restart flag to false.

Equations

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

@[inline]

def Blaster.Optimize.isRestart : TranslateEnvT Bool

Return the restart flag.

Equations

• Blaster.Optimize.isRestart = do let __do_lift ← get pure __do_lift.optEnv.restart

def Blaster.Optimize.setNormalizeFunCall (b : Bool) : TranslateEnvT Unit

set optimize option normalizeFunCall to b.

Equations

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

def Blaster.Optimize.setInFunApp (b : Bool) : TranslateEnvT Unit

set optimize option inFunApp to b.

Equations

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

@[inline]

def Blaster.Optimize.updateHypothesis (h : HypothesisContext) (localCache : RewriteCacheMap) : TranslateEnvT Unit

Equations

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

@[inline]

def Blaster.Optimize.getMatchContext : TranslateEnvT MatchContextMap

Equations

• Blaster.Optimize.getMatchContext = do let __do_lift ← get pure __do_lift.optEnv.matchInContext

@[inline]

def Blaster.Optimize.updateMatchContext (h : MatchContextMap) (localCache : RewriteCacheMap) : TranslateEnvT Unit

Equations

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

@[inline]

def Blaster.Optimize.updateLocalContext (h : LocalDeclContext) : TranslateEnvT Unit

Equations

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

@[inline]

def Blaster.Optimize.mkLocalContext : Lean.MetaM LocalDeclContext

Equations

• Blaster.Optimize.mkLocalContext = do let __do_lift ← Lean.getLCtx let __do_lift_1 ← Lean.Meta.getLocalInstances pure { ctx := __do_lift, localInsts := __do_lift_1 }

@[inline]

def Blaster.Optimize.withLocalContext {α : Type} (f : TranslateEnvT α) : TranslateEnvT α

Equations

• Blaster.Optimize.withLocalContext f = do let __do_lift ← get have ctx : Blaster.Optimize.LocalDeclContext := __do_lift.optEnv.ctx Lean.Meta.withLCtx ctx.ctx ctx.localInsts f

def Blaster.Optimize.getConstEnvInfo (n : Lean.Name) : TranslateEnvT Lean.ConstantInfo

Same as the default getConstInfo but cache result.

Equations

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

@[inline]

def Blaster.Optimize.isCtorName (c : Lean.Name) : TranslateEnvT Bool

Return true if c corresponds to a constructor.

Equations

• Blaster.Optimize.isCtorName c = do let __do_lift ← Blaster.Optimize.getConstEnvInfo c pure __do_lift.isCtor

@[inline]

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

Return true if e corresponds to a constructor expression.

Equations

• Blaster.Optimize.isCtorExpr (Lean.Expr.const n us) = do let __do_lift ← Blaster.Optimize.getConstEnvInfo n pure __do_lift.isCtor
• Blaster.Optimize.isCtorExpr e = pure false

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

Same as the default isProp but cache result.

Equations

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

def Blaster.Optimize.setInPatternMatching (h : Std.HashSet Lean.FVarId) : TranslateEnvT Unit

set optimize option inPatternMatchin to h.

Equations

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

@[inline]

def Blaster.Optimize.withTranslatePattern {α : Type} (h : Std.HashSet Lean.FVarId) (f : TranslateEnvT α) : TranslateEnvT α

Perform the following actions:

• let s := (← get).smtEnv.options.inPatternMatching
• set inPatternMatching to s ∪ h
• execute f
• set inPatternMatching to s

Equations

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

def Blaster.Optimize.isOptimizeRecCall : TranslateEnvT Bool

Return true if optimize option normalizeFunCall is set to true.

Equations

• Blaster.Optimize.isOptimizeRecCall = do let __do_lift ← get pure __do_lift.optEnv.options.normalizeFunCall

def Blaster.Optimize.isInFunApp : TranslateEnvT Bool

Return true if optimize option inFunApp is set to true.

Equations

• Blaster.Optimize.isInFunApp = do let __do_lift ← get pure __do_lift.optEnv.options.inFunApp

@[inline]

def Blaster.Optimize.findGlobalCache (a : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Equations

• Blaster.Optimize.findGlobalCache a = do let __do_lift ← get pure (Std.HashMap.get? __do_lift.optEnv.globalRewriteCache a)

@[inline]

def Blaster.Optimize.findLocalCache (a : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Equations

• Blaster.Optimize.findLocalCache a = do let __do_lift ← get pure (Std.HashMap.get? __do_lift.optEnv.localRewriteCache a)

def Blaster.Optimize.updateGlobalRewriteCache (a b : Lean.Expr) : TranslateEnvT Unit

Update global rewrite cache with a := b.

Equations

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

def Blaster.Optimize.updateLocalRewriteCache (a b : Lean.Expr) : TranslateEnvT Unit

Update local rewrite cache with a := b.

Equations

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

@[inline]

def Blaster.Optimize.updateSynthCache (a : Lean.Expr) (b : Option Lean.Expr) : TranslateEnvT Unit

Update synthesize decidable instance cache with a := b.

Equations

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

@[inline]

def Blaster.Optimize.withSynthInstanceCache (a : Lean.Expr) (f : Unit → TranslateEnvT (Option Lean.Expr)) : TranslateEnvT (Option Lean.Expr)

Return b if a := b is already in the synthesize cache Otherwise, the following actions are performed:

• execute b ← f ()
• update cache with a := b
• return b

Equations

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

@[inline]

def Blaster.Optimize.mkExpr (a : Lean.Expr) (cacheResult : Bool := true) : TranslateEnvT Lean.Expr

Return a' if a := a' is already in optimization cache. Otherwise, the following actions are performed:

• add a := a in cache only when cacheResult is set to true
• return a

Equations

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

@[inline]

def Blaster.Optimize.isGlobalContext : TranslateEnvT Bool

Return true only when both hypothesisMap and matchInContext are empty and isRefHyp flag is not set

Equations

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

@[inline]

def Blaster.Optimize.updateOptimizeEnvCache (a b : Lean.Expr) (isGlobal : Bool) : TranslateEnvT Unit

Perform the following:

• When isGlobal
  • Add entry a := b to globalRewriteCache
• Otherwise
  • Add entry a := b to localRewriteCache

Equations

• Blaster.Optimize.updateOptimizeEnvCache a b isGlobal = if isGlobal = true then Blaster.Optimize.updateGlobalRewriteCache a b else Blaster.Optimize.updateLocalRewriteCache a b

@[inline]

def Blaster.Optimize.isInOptimizeCache? (a : Lean.Expr) (isGlobal : Bool) : TranslateEnvT (Option Lean.Expr)

Perform the following:

• When isGlobal
  • When a := b ∈ globalRewriteCache
    • return some b
  • Otherwise none
• Otherwise
  • When a := b ∈ localRewriteCache
    • return some b
  • Otherwise none

Equations

• Blaster.Optimize.isInOptimizeCache? a isGlobal = if isGlobal = true then Blaster.Optimize.findGlobalCache a else Blaster.Optimize.findLocalCache a

def Blaster.Optimize.cacheFunName (f : Lean.Expr) : TranslateEnvT Unit

Add an instance recursive application (see function getInstApp) to the visited recursive function cache.

Equations

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

def Blaster.Optimize.uncacheFunName (f : Lean.Expr) : TranslateEnvT Unit

Remove an instance recursive application (see function getInstApp) from the visited recursive function cache.

Equations

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

def Blaster.Optimize.internalRecFun : Lean.Name

Internal generalized rec fun const to be used for in normalized recursive definition kept in recFunMap.

Equations

• Blaster.Optimize.internalRecFun = `_recFun

@[inline]

def Blaster.Optimize.tagAsRecursiveCall (e : Lean.Expr) : Lean.Expr

Tag expression as recursive call. This metadata is used when replacing a recursive call function with internalRecfun.

Equations

• Blaster.Optimize.tagAsRecursiveCall e = Lean.mkAnnotation `_solver.recursivecall e

def Blaster.Optimize.toTaggedRecursiveCall? (e : Lean.Expr) : Option Lean.Expr

Return some b if e := mkAnnotation _solver.recursivecall b'`.

Equations

• Blaster.Optimize.toTaggedRecursiveCall? (Lean.Expr.mdata d b) = if (Lean.KVMap.size d == 1 && Lean.KVMap.getBool d `_solver.recursivecall) = true then some b else none
• Blaster.Optimize.toTaggedRecursiveCall? e = none

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

Return true if e := mkAnnotation _solver.recursivecall b'`.

Equations

• Blaster.Optimize.isTaggedRecursiveCall (Lean.Expr.mdata d b) = (Lean.KVMap.size d == 1 && Lean.KVMap.getBool d `_solver.recursivecall)
• Blaster.Optimize.isTaggedRecursiveCall e = false

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

Return true if f is already in the recursive function cache.

Equations

• Blaster.Optimize.isVisitedRecFun f = do let __do_lift ← get pure (__do_lift.optEnv.recFunCache.contains f)

def Blaster.Optimize.isTheorem (f : Lean.Name) : TranslateEnvT Bool

Return true if f corresponds to a theorem name.

Equations

• Blaster.Optimize.isTheorem f = do let __do_lift ← Blaster.Optimize.getConstEnvInfo f match __do_lift with | Lean.ConstantInfo.thmInfo val => pure true | x => pure false

def Blaster.Optimize.mkBoolType : TranslateEnvT Lean.Expr

Return Bool type and cache result.

Equations

• Blaster.Optimize.mkBoolType = Blaster.Optimize.mkExpr (Lean.mkConst `Bool)

def Blaster.Optimize.mkBoolTrue : TranslateEnvT Lean.Expr

Return true boolean constructor and cache result.

Equations

• Blaster.Optimize.mkBoolTrue = Blaster.Optimize.mkExpr (Lean.mkConst `Bool.true)

def Blaster.Optimize.mkBoolFalse : TranslateEnvT Lean.Expr

Return false boolean constructor and cache result.

Equations

• Blaster.Optimize.mkBoolFalse = Blaster.Optimize.mkExpr (Lean.mkConst `Bool.false)

def Blaster.Optimize.mkBoolLit (b : Bool) : TranslateEnvT Lean.Expr

Given b a boolean value return the corresponding boolean constructor expression and cache result.

Equations

• Blaster.Optimize.mkBoolLit b = if b = true then Blaster.Optimize.mkBoolTrue else Blaster.Optimize.mkBoolFalse

def Blaster.Optimize.mkBoolNotOp : TranslateEnvT Lean.Expr

Return not boolean operator and cache result.

Equations

• Blaster.Optimize.mkBoolNotOp = Blaster.Optimize.mkExpr (Lean.mkConst `Bool.not)

def Blaster.Optimize.mkBoolOrOp : TranslateEnvT Lean.Expr

Return or boolean operator and cache result.

Equations

• Blaster.Optimize.mkBoolOrOp = Blaster.Optimize.mkExpr (Lean.mkConst `Bool.or)

def Blaster.Optimize.mkBoolAndOp : TranslateEnvT Lean.Expr

Return and boolean operator and cache result.

Equations

• Blaster.Optimize.mkBoolAndOp = Blaster.Optimize.mkExpr (Lean.mkConst `Bool.and)

def Blaster.Optimize.mkPropType : TranslateEnvT Lean.Expr

Return Prop type and cache result.

Equations

• Blaster.Optimize.mkPropType = Blaster.Optimize.mkExpr (Lean.mkSort Lean.levelZero)

def Blaster.Optimize.mkPropTrue : TranslateEnvT Lean.Expr

Return True Prop and cache result.

Equations

• Blaster.Optimize.mkPropTrue = Blaster.Optimize.mkExpr (Lean.mkConst `True)

def Blaster.Optimize.mkPropFalse : TranslateEnvT Lean.Expr

Return False Prop and cache result.

Equations

• Blaster.Optimize.mkPropFalse = Blaster.Optimize.mkExpr (Lean.mkConst `False)

def Blaster.Optimize.mkPropLit (b : Bool) : TranslateEnvT Lean.Expr

Given b a boolean value return the corresponding propositional expression and cache result.

Equations

• Blaster.Optimize.mkPropLit b = if b = true then Blaster.Optimize.mkPropTrue else Blaster.Optimize.mkPropFalse

def Blaster.Optimize.mkPropNotOp : TranslateEnvT Lean.Expr

Return Not operator and cache result.

Equations

• Blaster.Optimize.mkPropNotOp = Blaster.Optimize.mkExpr (Lean.mkConst `Not)

def Blaster.Optimize.mkPropOrOp : TranslateEnvT Lean.Expr

Return Or operator and cache result.

Equations

• Blaster.Optimize.mkPropOrOp = Blaster.Optimize.mkExpr (Lean.mkConst `Or)

def Blaster.Optimize.mkPropAndOp : TranslateEnvT Lean.Expr

Return And operator and cache result.

Equations

• Blaster.Optimize.mkPropAndOp = Blaster.Optimize.mkExpr (Lean.mkConst `And)

def Blaster.Optimize.mkBeqOp : TranslateEnvT Lean.Expr

Return BEq.beq operator and cache result.

Equations

• Blaster.Optimize.mkBeqOp = Blaster.Optimize.mkExpr (Lean.mkConst `BEq.beq [Lean.levelZero])

def Blaster.Optimize.mkEqOp : TranslateEnvT Lean.Expr

Return Eq operator and cache result.

Equations

• Blaster.Optimize.mkEqOp = Blaster.Optimize.mkExpr (Lean.mkConst `Eq [Lean.levelOne])

def Blaster.Optimize.mkIteOp : TranslateEnvT Lean.Expr

Return ite operator and cache result.

Equations

• Blaster.Optimize.mkIteOp = Blaster.Optimize.mkExpr (Lean.mkConst `ite [Lean.levelOne])

def Blaster.Optimize.mkDIteOp : TranslateEnvT Lean.Expr

Return dite operator and cache result.

Equations

• Blaster.Optimize.mkDIteOp = Blaster.Optimize.mkExpr (Lean.mkConst `dite [Lean.levelOne])

def Blaster.Optimize.mkBlasterDIteOp : TranslateEnvT Lean.Expr

Return Blaster.dite' operator and cache result.

Equations

• Blaster.Optimize.mkBlasterDIteOp = Blaster.Optimize.mkExpr (Lean.mkConst `Blaster.dite' [Lean.levelOne])

def Blaster.Optimize.mkLeOp : TranslateEnvT Lean.Expr

Return LE.le operator and cache result.

Equations

• Blaster.Optimize.mkLeOp = Blaster.Optimize.mkExpr (Lean.mkConst `LE.le [Lean.levelZero])

def Blaster.Optimize.mkLEConst : TranslateEnvT Lean.Expr

Return LE const expression and cache result.

Equations

• Blaster.Optimize.mkLEConst = Blaster.Optimize.mkExpr (Lean.mkConst `LE [Lean.levelZero])

def Blaster.Optimize.mkLtOp : TranslateEnvT Lean.Expr

Return LT.lt operator and cache result.

Equations

• Blaster.Optimize.mkLtOp = Blaster.Optimize.mkExpr (Lean.mkConst `LT.lt [Lean.levelZero])

def Blaster.Optimize.mkLTConst : TranslateEnvT Lean.Expr

Return LT const expression and cache result.

Equations

• Blaster.Optimize.mkLTConst = Blaster.Optimize.mkExpr (Lean.mkConst `LT [Lean.levelZero])

def Blaster.Optimize.mkDecidableConst : TranslateEnvT Lean.Expr

Return Decidable const expression and cache result.

Equations

• Blaster.Optimize.mkDecidableConst = Blaster.Optimize.mkExpr (Lean.mkConst `Decidable)

def Blaster.Optimize.mkDecidableEqConst : TranslateEnvT Lean.Expr

Return Decidable const expression and cache result.

Equations

• Blaster.Optimize.mkDecidableEqConst = Blaster.Optimize.mkExpr (Lean.mkConst `DecidableEq)

def Blaster.Optimize.mkDecideConst : TranslateEnvT Lean.Expr

Return decide const expression and cache result.

Equations

• Blaster.Optimize.mkDecideConst = Blaster.Optimize.mkExpr (Lean.mkConst `Decidable.decide)

def Blaster.Optimize.mkBlasterDecideConst : TranslateEnvT Lean.Expr

Return Blaster.decide' const expression and cache result.

Equations

• Blaster.Optimize.mkBlasterDecideConst = Blaster.Optimize.mkExpr (Lean.mkConst `Blaster.decide')

def Blaster.Optimize.mkInhabitedConst : TranslateEnvT Lean.Expr

Return Inhabited const expression and cache result.

Equations

• Blaster.Optimize.mkInhabitedConst = Blaster.Optimize.mkExpr (Lean.mkConst `Inhabited [Lean.levelOne])

def Blaster.Optimize.mkBEqConst : TranslateEnvT Lean.Expr

Return BEq const expression and cache result.

Equations

• Blaster.Optimize.mkBEqConst = Blaster.Optimize.mkExpr (Lean.mkConst `BEq [Lean.levelZero])

def Blaster.Optimize.mkLawfulBEqConst : TranslateEnvT Lean.Expr

Return LawfulBEq const expression and cache result.

Equations

• Blaster.Optimize.mkLawfulBEqConst = Blaster.Optimize.mkExpr (Lean.mkConst `LawfulBEq [Lean.levelZero])

def Blaster.Optimize.mkInstBEqOfDecidableEq : TranslateEnvT Lean.Expr

Return instBEqOfDecidableEq const expression and cache result.

Equations

• Blaster.Optimize.mkInstBEqOfDecidableEq = Blaster.Optimize.mkExpr (Lean.mkConst `instBEqOfDecidableEq [Lean.levelZero])

def Blaster.Optimize.mkInstDecidableEqNat : TranslateEnvT Lean.Expr

Return instDecidableEqNat const expression and cache result.

Equations

• Blaster.Optimize.mkInstDecidableEqNat = Blaster.Optimize.mkExpr (Lean.mkConst `instDecidableEqNat)

def Blaster.Optimize.mkTrueIntro : TranslateEnvT Lean.Expr

Return True.intro const expression and cache result.

Equations

• Blaster.Optimize.mkTrueIntro = Blaster.Optimize.mkExpr (Lean.mkConst `True.intro)

def Blaster.Optimize.mkNotFalse : TranslateEnvT Lean.Expr

Return not_false const expression and cache result.

Equations

• Blaster.Optimize.mkNotFalse = Blaster.Optimize.mkExpr (Lean.mkConst `not_false)

def Blaster.Optimize.mkOfDecideEqTrue : TranslateEnvT Lean.Expr

Return of_decide_eq_true const expression and cache result.

Equations

• Blaster.Optimize.mkOfDecideEqTrue = Blaster.Optimize.mkExpr (Lean.mkConst `of_decide_eq_true)

def Blaster.Optimize.mkOfDecideEqFalse : TranslateEnvT Lean.Expr

Return of_decide_eq_false const expression and cache result.

Equations

• Blaster.Optimize.mkOfDecideEqFalse = Blaster.Optimize.mkExpr (Lean.mkConst `of_decide_eq_false)

def Blaster.Optimize.mkEqRefl : TranslateEnvT Lean.Expr

Return Eq.refl const expression and cache result.

Equations

• Blaster.Optimize.mkEqRefl = Blaster.Optimize.mkExpr (Lean.mkConst `Eq.refl [Lean.levelOne])

def Blaster.Optimize.mkNatType : TranslateEnvT Lean.Expr

Return Nat Type and cache result.

Equations

• Blaster.Optimize.mkNatType = Blaster.Optimize.mkExpr (Lean.mkConst `Nat)

def Blaster.Optimize.natAdd : Lean.Expr

Return Nat.add operator

Equations

• Blaster.Optimize.natAdd = Lean.mkConst `Nat.add

def Blaster.Optimize.mkNatAddOp : TranslateEnvT Lean.Expr

Create a Nat.add operator expression and cache result.

Equations

• Blaster.Optimize.mkNatAddOp = Blaster.Optimize.mkExpr Blaster.Optimize.natAdd

def Blaster.Optimize.natSub : Lean.Expr

Return Nat.sub operator

Equations

• Blaster.Optimize.natSub = Lean.mkConst `Nat.sub

def Blaster.Optimize.mkNatSubOp : TranslateEnvT Lean.Expr

Create a Nat.sub operator expression and cache result.

Equations

• Blaster.Optimize.mkNatSubOp = Blaster.Optimize.mkExpr Blaster.Optimize.natSub

def Blaster.Optimize.natMul : Lean.Expr

Return Nat.mul operator

Equations

• Blaster.Optimize.natMul = Lean.mkConst `Nat.mul

def Blaster.Optimize.mkNatMulOp : TranslateEnvT Lean.Expr

Create a Nat.mul operator expression and cache result.

Equations

• Blaster.Optimize.mkNatMulOp = Blaster.Optimize.mkExpr Blaster.Optimize.natMul

def Blaster.Optimize.natDiv : Lean.Expr

Return Nat.div operator

Equations

• Blaster.Optimize.natDiv = Lean.mkConst `Nat.div

def Blaster.Optimize.mkNatDivOp : TranslateEnvT Lean.Expr

Creata a Nat.div operator expression and cache result.

Equations

• Blaster.Optimize.mkNatDivOp = Blaster.Optimize.mkExpr Blaster.Optimize.natDiv

def Blaster.Optimize.natMod : Lean.Expr

Return Nat.mod operator

Equations

• Blaster.Optimize.natMod = Lean.mkConst `Nat.mod

def Blaster.Optimize.mkNatModOp : TranslateEnvT Lean.Expr

Create a Nat.mod operator expression and cache result.

Equations

• Blaster.Optimize.mkNatModOp = Blaster.Optimize.mkExpr Blaster.Optimize.natMod

def Blaster.Optimize.natPow : Lean.Expr

Return Nat.pow operator

Equations

• Blaster.Optimize.natPow = Lean.mkConst `Nat.pow

def Blaster.Optimize.mkNatPowOp : TranslateEnvT Lean.Expr

Create a Nat.pow operator expression and cache result.

Equations

• Blaster.Optimize.mkNatPowOp = Blaster.Optimize.mkExpr Blaster.Optimize.natPow

def Blaster.Optimize.natBeq : Lean.Expr

Return Nat.beq operator

Equations

• Blaster.Optimize.natBeq = Lean.mkConst `Nat.beq

def Blaster.Optimize.natBle : Lean.Expr

Return Nat.ble operator

Equations

• Blaster.Optimize.natBle = Lean.mkConst `Nat.ble

def Blaster.Optimize.mkNatBltOp : TranslateEnvT Lean.Expr

Return Nat.blt operator and cache result.

Equations

• Blaster.Optimize.mkNatBltOp = Blaster.Optimize.mkExpr (Lean.mkConst `Nat.blt)

def Blaster.Optimize.mkIntType : TranslateEnvT Lean.Expr

Return Int Type and cache result.

Equations

• Blaster.Optimize.mkIntType = Blaster.Optimize.mkExpr (Lean.mkConst `Int)

def Blaster.Optimize.mkIntAddOp : TranslateEnvT Lean.Expr

Return Int.add operator and cache result.

Equations

• Blaster.Optimize.mkIntAddOp = Blaster.Optimize.mkExpr (Lean.mkConst `Int.add)

def Blaster.Optimize.mkIntMulOp : TranslateEnvT Lean.Expr

Return Int.mul operator and cache result.

Equations

• Blaster.Optimize.mkIntMulOp = Blaster.Optimize.mkExpr (Lean.mkConst `Int.mul)

def Blaster.Optimize.intPow : Lean.Expr

Return Int.pow operator

Equations

• Blaster.Optimize.intPow = Lean.mkConst `Int.pow

def Blaster.Optimize.mkIntPowOp : TranslateEnvT Lean.Expr

Create an Int.pow operator expression and cache result.

Equations

• Blaster.Optimize.mkIntPowOp = Blaster.Optimize.mkExpr Blaster.Optimize.intPow

def Blaster.Optimize.intEDiv : Lean.Expr

Return Int.ediv operator

Equations

• Blaster.Optimize.intEDiv = Lean.mkConst `Int.ediv

def Blaster.Optimize.mkIntEDivOp : TranslateEnvT Lean.Expr

Create an Int.ediv operator expression and cache result.

Equations

• Blaster.Optimize.mkIntEDivOp = Blaster.Optimize.mkExpr Blaster.Optimize.intEDiv

def Blaster.Optimize.intEMod : Lean.Expr

Return Int.emod operator

Equations

• Blaster.Optimize.intEMod = Lean.mkConst `Int.emod

def Blaster.Optimize.mkIntEModOp : TranslateEnvT Lean.Expr

Create an Int.emod operator expression and cache result.

Equations

• Blaster.Optimize.mkIntEModOp = Blaster.Optimize.mkExpr Blaster.Optimize.intEMod

def Blaster.Optimize.mkIntFDivOp : TranslateEnvT Lean.Expr

Return Int.fdiv operator and cache result.

Equations

• Blaster.Optimize.mkIntFDivOp = Blaster.Optimize.mkExpr (Lean.mkConst `Int.fdiv)

def Blaster.Optimize.mkIntFModOp : TranslateEnvT Lean.Expr

Return Int.fmod operator and cache result.

Equations

• Blaster.Optimize.mkIntFModOp = Blaster.Optimize.mkExpr (Lean.mkConst `Int.fmod)

def Blaster.Optimize.mkIntTDivOp : TranslateEnvT Lean.Expr

Return Int.tdiv operator and cache result.

Equations

• Blaster.Optimize.mkIntTDivOp = Blaster.Optimize.mkExpr (Lean.mkConst `Int.tdiv)

def Blaster.Optimize.mkIntTModOp : TranslateEnvT Lean.Expr

Return Int.tmod operator and cache result.

Equations

• Blaster.Optimize.mkIntTModOp = Blaster.Optimize.mkExpr (Lean.mkConst `Int.tmod)

def Blaster.Optimize.mkIntNegOp : TranslateEnvT Lean.Expr

Return Int.neg operator and cache result.

Equations

• Blaster.Optimize.mkIntNegOp = Blaster.Optimize.mkExpr (Lean.mkConst `Int.neg)

def Blaster.Optimize.mkIntOfNat : TranslateEnvT Lean.Expr

Return Int.ofNat constructor and cache result.

Equations

• Blaster.Optimize.mkIntOfNat = Blaster.Optimize.mkExpr (Lean.mkConst `Int.ofNat)

def Blaster.Optimize.mkIntToNatOp : TranslateEnvT Lean.Expr

Return Int.toNat operator and cache result.

Equations

• Blaster.Optimize.mkIntToNatOp = Blaster.Optimize.mkExpr (Lean.mkConst `Int.toNat)

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

mkAppExpr f #[a₀, ..., aₙ] constructs the application f a₀ ... aₙ and cache the result.

Equations

• Blaster.Optimize.mkAppExpr f args = Blaster.Optimize.mkExpr (Lean.mkAppN f args)

def Blaster.Optimize.mkNatBEqOp : TranslateEnvT Lean.Expr

Return "==" Nat operator and cache result.

Equations

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

def Blaster.Optimize.mkNatLeOp : TranslateEnvT Lean.Expr

Return the ≤ Nat operator and cache result.

Equations

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

def Blaster.Optimize.mkNatLtOp : TranslateEnvT Lean.Expr

Return the < Nat operator and cache result.

Equations

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

def Blaster.Optimize.mkNatDecLeOp : TranslateEnvT Lean.Expr

Return the Nat.decLe operator and cache result.

Equations

• Blaster.Optimize.mkNatDecLeOp = Blaster.Optimize.mkExpr (Lean.mkConst `Nat.decLe)

def Blaster.Optimize.mkNatDecLtOp : TranslateEnvT Lean.Expr

Return the Nat.decLt operator and cache result.

Equations

• Blaster.Optimize.mkNatDecLtOp = Blaster.Optimize.mkExpr (Lean.mkConst `Nat.decLt)

def Blaster.Optimize.mkIntLeOp : TranslateEnvT Lean.Expr

Return the ≤ Int operator and cache result.

Equations

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

def Blaster.Optimize.mkIntLtOp : TranslateEnvT Lean.Expr

Return the < Int operator and cache result.

Equations

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

def Blaster.Optimize.mkForallFVar (n b : Lean.Expr) : Lean.MetaM Lean.Expr

Equations

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

@[inline]

def Blaster.Optimize.mkForallFVars' (fvars : Array Lean.Expr) (b : Lean.Expr) : Lean.MetaM Lean.Expr

Equations

• Blaster.Optimize.mkForallFVars' fvars b = Array.foldrM (fun (v acc : Lean.Expr) => Blaster.Optimize.mkForallFVar v acc) b fvars

@[inline]

def Blaster.Optimize.mkForallExpr (n b : Lean.Expr) : TranslateEnvT Lean.Expr

mkForallExpr n b constructs ∀ n, b and cache result.

Equations

• Blaster.Optimize.mkForallExpr n b = do let __do_lift ← liftM (Blaster.Optimize.mkForallFVar n b) Blaster.Optimize.mkExpr __do_lift

def Blaster.Optimize.mkLambdaFVar (n b : Lean.Expr) : Lean.MetaM Lean.Expr

Equations

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

@[inline]

def Blaster.Optimize.mkLambdaFVars' (fvars : Array Lean.Expr) (b : Lean.Expr) : Lean.MetaM Lean.Expr

Equations

• Blaster.Optimize.mkLambdaFVars' fvars b = Array.foldrM (fun (v acc : Lean.Expr) => Blaster.Optimize.mkLambdaFVar v acc) b fvars

@[inline]

def Blaster.Optimize.mkLambdaExpr (n b : Lean.Expr) : TranslateEnvT Lean.Expr

mkLambdaExpr n b constructs fun n => b and cache result.

Equations

• Blaster.Optimize.mkLambdaExpr n b = do let __do_lift ← liftM (Blaster.Optimize.mkLambdaFVar n b) Blaster.Optimize.mkExpr __do_lift

def Blaster.Optimize.mkNatLitExpr (n : Nat) : TranslateEnvT Lean.Expr

mkNatLitExpr n constructs Expr.lit (Literal.natVal n) and cache result.

Equations

• Blaster.Optimize.mkNatLitExpr n = Blaster.Optimize.mkExpr (Lean.mkRawNatLit n)

def Blaster.Optimize.mkNatEqExpr (a b : Lean.Expr) : TranslateEnvT Lean.Expr

Return Nat a = b but don't cache result.

Equations

• Blaster.Optimize.mkNatEqExpr a b = do let __do_lift ← Blaster.Optimize.mkEqOp let __do_lift_1 ← Blaster.Optimize.mkNatType pure (Lean.mkApp3 __do_lift __do_lift_1 a b)

def Blaster.Optimize.mkNatLtExpr (a b : Lean.Expr) : TranslateEnvT Lean.Expr

Return Nat a < b and don't cache result.

Equations

• Blaster.Optimize.mkNatLtExpr a b = do let __do_lift ← Blaster.Optimize.mkNatLtOp pure (Lean.mkApp2 __do_lift a b)

def Blaster.Optimize.mkNatLeExpr (a b : Lean.Expr) : TranslateEnvT Lean.Expr

Return Nat a ≤ b and don't cache result.

Equations

• Blaster.Optimize.mkNatLeExpr a b = do let __do_lift ← Blaster.Optimize.mkNatLeOp pure (Lean.mkApp2 __do_lift a b)

def Blaster.Optimize.evalBinNatOp (f : Nat → Nat → Nat) (n1 n2 : Nat) : TranslateEnvT Lean.Expr

`evalBinNatOp f n1 n2 perform the following:

• let r := f n1 n2
• construct nat literal for r
• cache result and return r

Equations

• Blaster.Optimize.evalBinNatOp f n1 n2 = Blaster.Optimize.mkNatLitExpr (f n1 n2)

def Blaster.Optimize.mkIntLitExpr (n : Int) : TranslateEnvT Lean.Expr

mkIntLitExpr n constructs and cache an Int literal expression, i.e., either Int.ofNat (Expr.lit (Literal.natVal n) or Int.negSucc (Expr.lit (Literal.natVal n).

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Optimize.mkIntLitExpr (Int.negSucc n_2) = do let __do_lift ← Blaster.Optimize.mkNatLitExpr n_2 Blaster.Optimize.mkExpr (Lean.mkApp (Lean.mkConst `Int.negSucc) __do_lift)

def Blaster.Optimize.mkIntEqExpr (a b : Lean.Expr) : TranslateEnvT Lean.Expr

Return Int a = b and don't cache result.

Equations

• Blaster.Optimize.mkIntEqExpr a b = do let __do_lift ← Blaster.Optimize.mkEqOp let __do_lift_1 ← Blaster.Optimize.mkIntType pure (Lean.mkApp3 __do_lift __do_lift_1 a b)

def Blaster.Optimize.mkIntLtExpr (a b : Lean.Expr) : TranslateEnvT Lean.Expr

Returns Int a < b and don't cache result.

Equations

• Blaster.Optimize.mkIntLtExpr a b = do let __do_lift ← Blaster.Optimize.mkIntLtOp pure (Lean.mkApp2 __do_lift a b)

def Blaster.Optimize.mkIntLeExpr (a b : Lean.Expr) : TranslateEnvT Lean.Expr

Return Int a ≤ b and don't cache result.

Equations

• Blaster.Optimize.mkIntLeExpr a b = do let __do_lift ← Blaster.Optimize.mkIntLeOp pure (Lean.mkApp2 __do_lift a b)

def Blaster.Optimize.mkNatNegExpr (n : Nat) : TranslateEnvT Lean.Expr

mkNatNegExpr n constructs and cache the negation of a Nat literal expression, i.e., Int.negSucc (Expr.lit (Literal.natVal (n - 1))`.

Equations

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

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

Equations

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

@[inline]

def Blaster.Optimize.evalBinIntOp (f : Int → Int → Int) (n1 n2 : Int) : TranslateEnvT Lean.Expr

`evalBinIntOp f n1 n2 perform the following:

• let r := f n1 n2
• construct int literal for r
• cache result and return r

Equations

• Blaster.Optimize.evalBinIntOp f n1 n2 = Blaster.Optimize.mkIntLitExpr (f n1 n2)

def Blaster.Optimize.mkStrLitExpr (s : String) : TranslateEnvT Lean.Expr

mkStrLitExpr s constructs Expr.lit (Literal.strVal s) and cache result.

Equations

• Blaster.Optimize.mkStrLitExpr s = Blaster.Optimize.mkExpr (Lean.mkStrLit s)

def Blaster.Optimize.mkDecidableConstraint (e : Lean.Expr) (cacheDecidableCst : Bool := true) : TranslateEnvT Lean.Expr

mkDecidableConstraint e constructs constraint [Decidable e] and cache the result.

Equations

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

def Blaster.Optimize.trySynthConstraintInstance? (cstr : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Return d if there is already a synthesize instance for cstr in the synthesize cache. Otherwise, the following actions are performed:

• When LOption.some d ← trySynthInstance cstr
  • add cstr := some d to synthesize cache
  • return some d
• When trySynthInstance does not return LOption.some:
  • add cstr := none to synthesize cache
  • return none

Equations

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

def Blaster.Optimize.trySynthDecidableInstance? (e : Lean.Expr) (cacheDecidableCst : Bool := true) : TranslateEnvT (Option Lean.Expr)

Try to find an instance for [Decidable e].

Equations

• Blaster.Optimize.trySynthDecidableInstance? e cacheDecidableCst = do let dCstr ← Blaster.Optimize.mkDecidableConstraint e cacheDecidableCst Blaster.Optimize.trySynthConstraintInstance? dCstr

def Blaster.Optimize.synthDecidableInstance! (e : Lean.Expr) : TranslateEnvT Lean.Expr

Same as trySynthDecidableInstance but throws an error when a decidable instance cannot be found.

Equations

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

def Blaster.Optimize.synthDecidableWithNotFound! (e : Lean.Expr) : TranslateEnvT Lean.Expr

Same as trySynthDecidableInstance but cache and return the queried decidable constraint when no decidable instance cannot be found. In fact, after definitions have been unfolded, it can sometimes be the case that Lean can't infer the proper Decidable instance. In this case, we return the queried decidable instance.

Equations

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

@[inline]

def Blaster.Optimize.hasInhabitedInstance (n : Lean.Expr) : TranslateEnvT Bool

Return true only when an instance for [Inhabited n] can be found. Assume that n is a name expression for an inductive datatype.

Equations

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

@[inline]

def Blaster.Optimize.hasLawfulBEqInstance (t beqInst : Lean.Expr) : TranslateEnvT Bool

Return true only when an instance for [LawfulBEq t beqInst] can be found.

Equations

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

def Blaster.Optimize.mkOfDecideEqProof (c : Lean.Expr) (b : Bool) : TranslateEnvT Lean.Expr

Given an expression c and a boolean value b, perform the following: let d ← synthDecidableWithNotFound! c

• When b is true:
  • return of_decide_eq_true c d (Eq.refl true)
• Otherwise:
  • return of_decide_eq_false c d (Eq.refl true)

Equations

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

def Blaster.Optimize.isOpaqueRelational (f : Lean.Name) (args : Array Lean.Expr) : TranslateEnvT Bool

Given f x₁ ... xₙ, return true only when one of the following conditions is satisfied: - f := BEq.beq with sort parameter that has a LawfulBEq instance - f := LT.lt with sort parameter in relationalCompatibleTypes - f : LE.le with sort parameter in relationalCompatibleTypes

In fact, we can't assume that BEq.beq, LT.lt and LE.le will properly be defined for any user-defined types or parametric inductive types (e.g., List, Option, etc).

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Optimize.isOpaqueRelational f args = pure false

def Blaster.Optimize.isOpaqueFun (f : Lean.Name) (args : Array Lean.Expr) : TranslateEnvT Bool

Return true if function name f is tagged as an opaque definition.

Equations

• Blaster.Optimize.isOpaqueFun f args = do let __do_lift ← Blaster.Optimize.isOpaqueRelational f args pure (Blaster.Optimize.opaqueFuns.contains f || __do_lift)

def Blaster.Optimize.isOpaqueFunExpr (f : Lean.Expr) (args : Array Lean.Expr) : TranslateEnvT Bool

Same as isOpaqueFun expect that f is an expression.

Equations

• Blaster.Optimize.isOpaqueFunExpr (Lean.Expr.const n us) args = Blaster.Optimize.isOpaqueFun n args
• Blaster.Optimize.isOpaqueFunExpr f args = pure false

@[inline]

def Blaster.Optimize.isInstanceClass (f : Lean.Name) : TranslateEnvT Bool

Return true only when f is a class instance.

Equations

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

@[inline]

def Blaster.Optimize.isRecursiveFun (f : Lean.Name) : TranslateEnvT Bool

Return true when f is neither a theorem nor a class instance and is tagged as a well-founded recursive definition.

Equations

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

@[inline]

def Blaster.Optimize.isRecursiveFun.updateIsRec (f : Lean.Name) (b : Bool) : TranslateEnvT Unit

Equations

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

def Blaster.Optimize.getForallLambdaBody (e : Lean.Expr) : Lean.Expr

Return the body in a sequence of forall / lambda.

Equations

• Blaster.Optimize.getForallLambdaBody (Lean.Expr.lam binderName binderType b binderInfo) = Blaster.Optimize.getForallLambdaBody b
• Blaster.Optimize.getForallLambdaBody (Lean.Expr.forallE binderName binderType b binderInfo) = Blaster.Optimize.getForallLambdaBody b
• Blaster.Optimize.getForallLambdaBody e = e

@[inline]

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

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

Equations

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

@[inline]

def Blaster.Optimize.getMatcherRecInfo? (n : Lean.Name) (l : List Lean.Level) : TranslateEnvT (Option MatcherRecInfo)

Same as the default getMatcherInfo in the Lean library but also handles casesOn recursor application.

Equations

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

@[inline]

def Blaster.Optimize.updateIsMatcherCache (n : Lean.Name) (mInfo : MatchInfo) : TranslateEnvT Unit

Add n := mInfo to isMatcherCache

Equations

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

def Blaster.Optimize.isMatcher? (f : Lean.Expr) : TranslateEnvT (Option MatchInfo)

Return some mInfo when f := Expr.const n l ∧ n := mInfo ∈ isMatcherCache. Otherwise none.

Equations

• Blaster.Optimize.isMatcher? (Lean.Expr.const n us) = do let __do_lift ← get pure (__do_lift.optEnv.memCache.isMatcherCache.get? n)
• Blaster.Optimize.isMatcher? f = pure none

@[inline]

def Blaster.Optimize.isPartialDef (n : Lean.Name) : TranslateEnvT Bool

Determine if n corresponds to a partial definition and cache result.

Equations

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

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

Same as the default inferType in the Lean codebase but caches the result.

Equations

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

@[inline]

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

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 false

partial def Blaster.Optimize.isInductiveTypeAux (f : Lean.Name) (us : List Lean.Level) : Lean.MetaM Bool

Return true if f corresponds to an inductive type or is an abbrevation to an inductive type.

@[inline]

def Blaster.Optimize.isInductiveType (f : Lean.Name) (us : List Lean.Level) : TranslateEnvT Bool

Return true if f corresponds to an inductive type or is an abbrevation to an inductive type.

Equations

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

@[inline]

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

Return true if e corresponds to an inductive type or is an abbreviation to an inductive type.

Equations

• Blaster.Optimize.isInductiveTypeExpr e = match e.getAppFn with | Lean.Expr.const n l => Blaster.Optimize.isInductiveType n l | x => pure false

inductive Blaster.Optimize.ResolveTypeStack : Type

• InitExpr (t : Lean.Expr) : ResolveTypeStack
• ArgsExpr (f : Lean.Expr) (args : Array Lean.Expr) (idx stop : Nat) : ResolveTypeStack

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

Same as the default isType but cache result.

Equations

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

def Blaster.Optimize.isResolvableType (t : Lean.Expr) : TranslateEnvT Bool

Return true is t is a potential resolvable type

Equations

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

@[always_inline]

def Blaster.Optimize.resolveTypeAbbrev (t : Lean.Expr) : TranslateEnvT Lean.Expr

Equations

• Blaster.Optimize.resolveTypeAbbrev t = Blaster.Optimize.resolveTypeAbbrevAux✝ [Blaster.Optimize.ResolveTypeStack.InitExpr t]

@[inline]

def Blaster.Optimize.getFVarsInExpr (e : Lean.Expr) : TranslateEnvT (Array Lean.Expr)

Return all fvar expressions in e. The return array preserved dependencies between fvars, i.e., child fvars appear first. TODO: change function to pure tail rec call using stack-based approach

Equations

• Blaster.Optimize.getFVarsInExpr e = Blaster.Optimize.getFVarsInExpr.visit e #[]

@[specialize #[]]

partial def Blaster.Optimize.getFVarsInExpr.visit (e : Lean.Expr) (acc : Array Lean.Expr) : TranslateEnvT (Array Lean.Expr)

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

Return true whenever e satisfies one of the following:

• e is a sort type;
• e is a const or variable of sort type;
• e is an application that transitively has at least one argument of sort type.

structure Blaster.Optimize.ImplicitInfo : Type

Type to represent the parameters instantiating the implicit arguments for a given function. (see function getImplicitParameters)

• effectiveArg : Lean.Expr

  Corresponds to an effective parameter for a given function (implicit or not).

• isInstance : Bool

  Flag set to true when the effective parameter instantiates an implicit parameter.

• isGeneric : Bool

  Flag set to true when the effective parameter instantiates an implicit parameter but is still polymorphic, i.e., predicate isGenericParam is satisfied.

instance Blaster.Optimize.instReprImplicitInfo : Repr ImplicitInfo

Equations

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

def Blaster.Optimize.instReprImplicitInfo.repr : ImplicitInfo → Nat → Std.Format

Equations

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

instance Blaster.Optimize.instInhabitedImplicitInfo : Inhabited ImplicitInfo

Equations

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

def Blaster.Optimize.instInhabitedImplicitInfo.default : ImplicitInfo

Equations

• Blaster.Optimize.instInhabitedImplicitInfo.default = { effectiveArg := default, isInstance := default, isGeneric := default }

@[reducible, inline]

abbrev Blaster.Optimize.ImplicitParameters : Type

Equations

• Blaster.Optimize.ImplicitParameters = Array Blaster.Optimize.ImplicitInfo

def Blaster.Optimize.updateGenericArgs (e : Lean.Expr) (gargs : Array Lean.Expr) (pset : Std.HashSet Lean.Expr) : TranslateEnvT (Array Lean.Expr × Std.HashSet Lean.Expr)

Helper function for retrieveGenericFVars and retrieveGenericArgs -

Equations

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

def Blaster.Optimize.retrieveGenericFVars (params : ImplicitParameters) : TranslateEnvT (Array Lean.Expr)

Given arguments params obtained from getImplicitParameters, perform the following: let V := #[α | i ∈ [0..n] ∧ α ∈ getFVarsInExpr params[i] ∧ params[i].isGeneric] return V

Equations

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

@[inline]

def Blaster.Optimize.getEffectiveParams (params : ImplicitParameters) : TranslateEnvT (Array Lean.Expr)

Given params an implicit parameters perform the following: let genArgs ← retrieveGenericFVars let P := #[ params[i].effectiveArgs | i ∈ [0..params.size-1] ∧ ¬ params[i].isInstance ] return genArgs ++ P

Equations

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

def Blaster.Optimize.specializeLambda (fbody : Lean.Expr) (params : ImplicitParameters) : Lean.Expr

Given a fun body λ α₀ → ... λ αₙ → body and params the implicit parameters info for the corresponding function, perform the following actions:

• let A := [α₀, ..., αₙ]
• let B := [ A[i] | i ∈ [0..n] ∧ ¬ params[i].isInstance ]
• let S := [ A[i] | i ∈ [0..n] ∧ params[i].isInstance ]
• let R := [ params[i].effectiveArg | i ∈ [0..n] ∧ params[i].isInstance ]
• let β₀, .., βₘ = B
• return λ β₀ → ... λ βₘ → body [S[0]/R[0]] ... [S[k]/R[k]] with k = S.size-1

Assume that params.size ≤ n TODO: change function to pure tail rec call using stack-based approach

Equations

• Blaster.Optimize.specializeLambda fbody params = Blaster.Optimize.specializeLambda.visit params 0 (Array.size params) fbody fun (e : Lean.Expr) => e

partial def Blaster.Optimize.specializeLambda.visit (params : ImplicitParameters) (idx stop : Nat) (e : Lean.Expr) (k : Lean.Expr → Lean.Expr) : Lean.Expr

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

Given f a function name expression, params its implicit parameters info (see getImplicitParameters), and fbody corresponding the recursive definition for f, perform the following actions:

• let fbody' be fbody in which the recurisve call is annotated with _solver.recursivecall
• When ∀ i ∈ [0..params.size-1], ¬ params[i].isInstance:
  • return fbody'
• Otherwise:
  • let genFVars ← retrieveGenericFVars params
  • return mkLambdaFVars genFVars (specializeLambda fbody' params) (usedOnly := true) An error is triggered when f is not a name expression.

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Optimize.generalizeRecCall f params fbody = Blaster.Optimize.throwEnvError (Lean.toMessageData "generalizeRecCall: name expression expected but got " ++ Lean.toMessageData (reprStr f))

def Blaster.Optimize.generalizeRecCall.replacePred (n : Lean.Name) (e : Lean.Expr) : Option Lean.Expr

Equations

• Blaster.Optimize.generalizeRecCall.replacePred n e = match e.getAppFn with | Lean.Expr.const rn us => if (rn == n) = true then some (Blaster.Optimize.tagAsRecursiveCall e) else none | x => none

def Blaster.Optimize.updateRecFunInst (f fbody : Lean.Expr) : TranslateEnvT Unit

Given f which is either a function name expression or a fully/partially instantiated polymorphic function (see getInstApp), and fbody corresponding to f's definition, update the recursive instance cache (i.e., recFunInstCache),

Equations

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

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

Return fₙ if body[mkAnnotation _solver.recursivecall _'/_recFun α₁ ... αₖ x₁ ... xₙ] := fₙ` is already in the recursive function map. Otherwise,

• update recursive function map with body[mkAnnotation _solver.recursivecall _'/_recFun α₁ ... αₖ x₁ ... xₙ] := f`
• return f. where:
• α₁ ... αₖcorrespond to the implicit arguments off` that are still polymorphic (if any).
• x₁ ... xₙ correspond to the effective parameters of the recursive call (excluding implicit arguments). NOTE:
• f is also removed from the visiting cache.
• The polymorphic instance cache is updated with f := body[mkAnnotation _solver.recursivecall _'/_recFun α₁ ... αₖ x₁ ... xₙ]` (if required) for all cases. This is essential to avoid performing structural equivalence check again on an already handled recursive function. Assumes that:
• f is either a function name expression or a fully/partially instantiated polymorphic function (see getInstApp)
• an entry exists for each opaque recursive function in recFunMap before optimization is performed (see function cacheOpaqueRecFun).

Equations

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

partial def Blaster.Optimize.storeRecFunDef.replacePred (params : ImplicitParameters) (recFun e : Lean.Expr) : Option Lean.Expr

def Blaster.Optimize.hasRecFunInst? (instApp : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Given instApp corresponding either to a function name expression or to a fully/partially instantiated polymorphic function (see function getInstApp), determine if instApp has already a mapping in recFunInstCache. If so then retrieve the corresponding function application in recFunMap. Otherwise return none. An error is triggered if no corresponding entry can be found in recFunMap.

Equations

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

def Blaster.Optimize.findLocalAxioms : TranslateEnvT (List Lean.Expr)

Returns all axioms only defined in current module.

Equations

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