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

Return true if n corresponds to an unsafe definition (e.g, partial recursive function, partial inductive predicate, etc).

Equations

• Blaster.Optimize.isUnsafeDef n = do let __do_lift ← Blaster.Optimize.getConstEnvInfo n pure __do_lift.isUnsafe

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

Return true if e corresponds to an enumerator constructor (i.e., constructor without any parameters).

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Optimize.isEnumConst e = pure false

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

Return true if e corresponds to a nullary constructor or a fully applied parametric constructor.

Equations

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

@[inline]

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

Return true if e corresponds to a constructor that may contain free or bounded variables.

Equations

• Blaster.Optimize.isConstructor e = if e.isLit = true then pure true else Blaster.Optimize.isEnumConst e <||> Blaster.Optimize.isFullyAppliedConst e

@[inline]

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

Return true if e corresponds to a constructor applied to only constant values (e.g., no free or bounded variables).

Equations

• Blaster.Optimize.isConstant e = (Blaster.Optimize.isConstructor e <&&> pure !Blaster.Optimize.hasVars e)

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

Return true if c corresponds to a nullary constructor.

Equations

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

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

Return true if t is not a Prop and corresponds to one of the following:

• is a sort type; or
• is a class constraint; or
• is an inductive type for which either at least one nullary constructor or an Inhabited instance exists. TODO: extends check to also consider parametric constructor for which each parameter type satisfy isSortOrInhabited.

Equations

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

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

Return ! e when b = false. Otherwise return e.

Equations

• Blaster.Optimize.toBoolNotExpr b e = if b = true then pure e else do let __do_lift ← Blaster.Optimize.mkBoolNotOp pure (Lean.mkApp __do_lift e)

inductive Blaster.Optimize.NatCstOpInfo : Type

Inductive type used to characterize Nat binary operators when at least one operand is a constant. This type is exclusively used by function toNatCstOpExpr?

• NatAddExpr (n : Nat) (e : Lean.Expr) : NatCstOpInfo

  Nat.add N e info.

• NatSubLeftExpr (n : Nat) (e : Lean.Expr) : NatCstOpInfo

  Nat.sub N e info.

• NatSubRightExpr (e : Lean.Expr) (n : Nat) : NatCstOpInfo

  Nat.sub e N info.

• NatMulExpr (n : Nat) (e : Lean.Expr) : NatCstOpInfo

  Nat.mul N e info.

• NatDivLeftExpr (n : Nat) (e : Lean.Expr) : NatCstOpInfo

  Nat.div N e info.

• NatDivRightExpr (e : Lean.Expr) (n : Nat) : NatCstOpInfo

  Nat.div e N info.

• NatModLeftExpr (n : Nat) (e : Lean.Expr) : NatCstOpInfo

  Nat.mod N e info.

• NatModRightExpr (e : Lean.Expr) (n : Nat) : NatCstOpInfo

  Nat.mod e N info.

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

Return a NatCstOpInfo for e according to the following rules:

• NatAddExpr N n (if e := Nat.add N n)
• NatSubLeftExpr N n (if e := Nat.sub N n)
• NatSubRightExpr n N (if e := Nat.sub n N)
• NatMulExpr N n (if e := Nat.mul N n)
• NatDivLeftExpr N n (if e := Nat.div N n)
• NatDivLeftExpr n N (if e := Nat.div n N)
• NatModLeftExpr N n (if e := Nat.mod N n)
• NatModRightExpr n N (if e := Nat.mod n N)

Return none when e is not a full applied Nat binary operator. Assume that operands have already been reordered for commutative operators.

Equations

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

inductive Blaster.Optimize.IntCstOpInfo : Type

Inductive type used to characterize Int binary operators when at least one operand is a constant. This type is exclusively used by function toIntCstOpExpr?

• IntAddExpr (n : Int) (e : Lean.Expr) : IntCstOpInfo

  Int.add N e info.

• IntMulExpr (n : Int) (e : Lean.Expr) : IntCstOpInfo

  Int.mul N e info.

• IntTDivLeftExpr (n : Int) (e : Lean.Expr) : IntCstOpInfo

  Int.tdiv N e info.

• IntTDivRightExpr (e : Lean.Expr) (n : Int) : IntCstOpInfo

  Int.tdiv e N info.

• IntTModLeftExpr (n : Int) (e : Lean.Expr) : IntCstOpInfo

  Int.tmod N e info.

• IntTModRightExpr (e : Lean.Expr) (n : Int) : IntCstOpInfo

  Int.tmod e N info.

• IntEDivLeftExpr (n : Int) (e : Lean.Expr) : IntCstOpInfo

  Int.ediv N e info.

• IntEDivRightExpr (e : Lean.Expr) (n : Int) : IntCstOpInfo

  Int.ediv e N info.

• IntEModLeftExpr (n : Int) (e : Lean.Expr) : IntCstOpInfo

  Int.emod N e info.

• IntEModRightExpr (e : Lean.Expr) (n : Int) : IntCstOpInfo

  Int.emod e N info.

• IntFDivLeftExpr (n : Int) (e : Lean.Expr) : IntCstOpInfo

  Int.fdiv N e info.

• IntFDivRightExpr (e : Lean.Expr) (n : Int) : IntCstOpInfo

  Int.fdiv e N info.

• IntFModLeftExpr (n : Int) (e : Lean.Expr) : IntCstOpInfo

  Int.fmod N e info.

• IntFModRightExpr (e : Lean.Expr) (n : Int) : IntCstOpInfo

  Int.fmod e N info.

• IntNegAddExpr (n : Int) (e : Lean.Expr) : IntCstOpInfo

  Int.neg (Int.add N e).

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

Return a IntCstOpInfo for e according to the following rules:

• IntAddExpr N n (if e := Int.add N n)
• IntMulExpr N n (if e := Int.mul N n)
• IntTDivLeftExpr N n (if e := Int.tdiv N n)
• IntTDivLeftExpr n N (if e := Int.tdiv n N)
• IntTModLeftExpr N n (if e := Int.tmod N n)
• IntTModRightExpr n N (if e := Int.tmod n N)
• IntEDivLeftExpr N n (if e := Int.ediv N n)
• IntEDivLeftExpr n N (if e := Int.ediv n N)
• IntEModLeftExpr N n (if e := Int.emod N n)
• IntEModRightExpr n N (if e := Int.emod n N)
• IntFDivLeftExpr N n (if e := Int.fdiv N n)
• IntFDivLeftExpr n N (if e := Int.fdiv n N)
• IntFModLeftExpr N n (if e := Int.fmod N n)
• IntFModRightExpr n N (if e := Int.fmod n N)
• IntNegAddExpr N n (if e := Int.neg (Int.add N n))

Return none when e is not a full applied Int binary operator. Assume that operands have already been reordered for commutative operators.

Equations

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

@[inline]

def Blaster.Optimize.swapOnCond (cond : Bool) (e1 e2 : Lean.Expr) : Lean.Expr × Lean.Expr

Equations

• Blaster.Optimize.swapOnCond cond e1 e2 = if cond = true then (e2, e1) else (e1, e2)

@[inline]

def Blaster.Optimize.reorderBoolOp (args : Array Lean.Expr) : Lean.Expr × Lean.Expr

Reorder operands for commutative Bool operators as follows:

• #[``false, _] ===> args
• #[e,false] ===> #[false, e]
• #[``true, _] ===> args
• #[e true] ===> #[true, e]
• #[fvar id1, fvar id2] ===> #[fvar id2, fvar id1] (if id2.name < id1.name)
• #[fvar _, _] ===> args
• #[e, fvar id] ===> #[fvar id, e]
• #[e1, e2] ===> #[e2, e1] (if isTaggedRecursiveCall e1 ∧ ¬ (isTaggedRecursiveCall e2))
• #[e1, e2] ===> #[e2, e1] (if e2 < e1)
• #[not e, e] ===> #[e, not e]
• #[e1, e2] ===> args Assume that args.size = 2

Equations

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

@[inline]

def Blaster.Optimize.reorderPropOp (args : Array Lean.Expr) : Lean.Expr × Lean.Expr

Reorder operands for commutative Prop operators as follows:

• #[``False, _] ===> args
• #[e,False] ===> #[False, e]
• #[True, _] ===> args
• #[e True] ===> #[True, e]
• #[fvar id1, fvar id2] ===> #[fvar id2, fvar id1] (if id2.name < id1.name)
• #[fvar _, _] ===> args
• #[e, fvar _] ===> #[fvar _, e]
• #[¬ e, e] ===> #[e, ¬ e]
• #[false = c, true = c] ===> #[true = c, false = c]
• #[e1 -> e2, e1] ===> #[e1, e1 -> e2]
• #[e1, e2] ===> #[e2, e1] (if isTaggedRecursiveCall e1 ∧ ¬ (isTaggedRecursiveCall e2))
• #[e1, e2] ===> #[e2, e1] (if e2 < e1)
• #[e1, e2] ===> args Assume that args.size = 2

Equations

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

@[inline]

def Blaster.Optimize.reorderEq (args : Array Lean.Expr) : TranslateEnvT (Lean.Expr × Lean.Expr)

Reorder operands for Eq operators by applying reorderPropOp first and followed by the rules:

• #[Expr.lit _, _] ===> args
• #[e, Expr.lit l] ===> #[Expr.lit l, e]
• #[e1, e2] ===> args (if isConstructor e1) -- already ordered by reorderPropOp
• #[e1, e2] ===> #[e2, e1] (if isConstructor e2)
• #[e1, e2] ===> args Assume that args.size = 2 NOTE: Precedence is applied according to the order in which the rules have been specified.

Equations

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

@[inline]

def Blaster.Optimize.reorderNatOp (args : Array Lean.Expr) : Lean.Expr × Lean.Expr

Reorder operands for commutative Int operators as follows:

• #[N1, N2] ===> args
• #[N, e] ===> args
• #[e, N] ===> #[N, e]
• #[fvar id1, fvar id2] ===> #[fvar id2, fvar id1] (if id2.name < id1.name)
• #[fvar _, _] ===> args
• #[e, fvar _] ===> #[fvar _, e]
• #[(Nat.sub x y), (Nat.add p q)] ===> #[Nat.add p q, Nat.sub x y]
• #[(Nat.pow x y), e] ===> #[e, Nat.pow x y] if ¬ (isNatPowExpr e)
• #[e1, e2] ===> #[e2, e1] (if isTaggedRecursiveCall e1 ∧ ¬ (isTaggedRecursiveCall e2))
• #[e1, e2] ===> #[e2, e1] (if e2 < e1)
• #[e1, e2] ===> args Assume that args.size = 2

Equations

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

@[inline]

def Blaster.Optimize.reorderIntOp (args : Array Lean.Expr) : Lean.Expr × Lean.Expr

Reorder operands for commutative Int operators as follows:

• #[N1, N2] ===> args
• #[N, e] ===> args
• #[e, N] ===> #[N, e]
• #[fvar id1, fvar id2] ===> #[fvar id2, fvar id1] (if id2.name < id1.name)
• #[fvar _, _] ===> args
• #[e, fvar _] ===> #[fvar _, e]
• #[Int.neg x, x] ===> #[x, Int.neg x]
• #[e1, e2] ===> #[e2, e1] (if isTaggedRecursiveCall e1 ∧ ¬ (isTaggedRecursiveCall e2))
• #[e1, e2] ===> #[e2, e1] (if e2 < e1)
• #[e1, e2] ===> args Assume that args.size = 2

Equations

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

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

Reorder operands for commutative operators

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Optimize.reorderOperands (Lean.Expr.const n us) args = pure args
• Blaster.Optimize.reorderOperands f args = pure args

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

Return true if e corresponds t a casesOn function.

Equations

• Blaster.Optimize.isCasesOnRec (Lean.Expr.const n us) = do let __do_lift ← Lean.getEnv pure (Lean.isCasesOnRecursor __do_lift n)
• Blaster.Optimize.isCasesOnRec e = pure false

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

Return true if e corresponds to a match or casesOn function.

Equations

• Blaster.Optimize.isMatchExpr (Lean.Expr.const n us) = Option.isSome <$> Blaster.Optimize.getMatcherRecInfo? n us
• Blaster.Optimize.isMatchExpr e = pure false

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

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Optimize.getFunBodyAux? (Lean.Expr.lam binderName binderType body binderInfo) = pure (some (Lean.Expr.lam binderName binderType body binderInfo))
• Blaster.Optimize.getFunBodyAux? (Lean.Expr.proj typeName idx struct) = liftM (Lean.Meta.reduceProj? (Lean.Expr.proj typeName idx struct))
• Blaster.Optimize.getFunBodyAux? f = pure none

def Blaster.Optimize.isFunType' (t : Lean.Expr) : Bool

Return true if the given type expression t (e.g., obtained via inferType) satisfy the following:

• t := α₁ → ... → αₙ Assumes that t is not a Prop.

Equations

• Blaster.Optimize.isFunType' t = if t.isForall = true then true else match Blaster.Optimize.autoParam? t with | some (t', _tactic) => t'.isForall | x => false

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

Return true if the given type expression t (e.g., obtained via inferType) satisfy the following:

• ¬ isProp t
• t := α₁ → ... → αₙ

Equations

• Blaster.Optimize.isFunType t = do let __do_lift ← Blaster.Optimize.isPropEnv t if __do_lift = true then pure false else pure (Blaster.Optimize.isFunType' t)

@[inline]

def Blaster.Optimize.getFunBody (f : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Same as getFunBodyAux? but cache result

Equations

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

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

Return true if e corresponds to an undefined type class function application, s.t.:

• e := app (Expr.proj c _ _) ...; and
• c is the name of a type class in the given environment; and
• Expr.proj c _ _ cannot be reduced.

Equations

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

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

Return true only when e := Expr.const n l and one of the following condition is satisfied:

• n := namedPattern; or
• n is a class instance; or
• n is a match expression; or
• n is a class constraint; or
• n is an inductive datatype ∧ n ∉ opaqueFuns;

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Optimize.isNotFunAux e = pure false

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

Same as isNotFunAux but caches the result.

Equations

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

def Blaster.Optimize.isNotFoldable (e : Lean.Expr) (args : Array Lean.Expr) : TranslateEnvT Bool

Return true only when e := Expr.const n l and one of the following condition is satisfied:

• n is not tagged as an opaque definition when flag opaqueCheck is set to true;
• n is not a recursive function when flag recFunCheck is set to true;
• n is a class instance;
• n is an inductive datatype;
• n := namedPattern;
• n is not a match expression; or
• n is not a class constraint.

Equations

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

def Blaster.Optimize.getUnfoldFunDef? (f : Lean.Expr) (args : Array Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Unfold fuction f w.r.t. the effective parameters args only when:

• f is not a constructor
• f is not tagged as an opaque definition
• f is not a recursive function
• f is not a class constraint
• f is not an undefined type class function
• f is not a match application

Equations

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

partial def Blaster.Optimize.unfoldOpaqueFunDef (f : Lean.Expr) (args : Array Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Unfold an opaque relation function up to its base definition Assume that f corresponds to an opaque relation function on first call.

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

Equations

• Blaster.Optimize.unfoldOpaqueFunDef.isFoldable (Lean.Expr.const declName us) args = do let __do_lift ← Blaster.Optimize.isNotFoldable (Lean.Expr.const declName us) args pure !__do_lift
• Blaster.Optimize.unfoldOpaqueFunDef.isFoldable (Lean.Expr.lam binderName binderType body binderInfo) args = pure true
• Blaster.Optimize.unfoldOpaqueFunDef.isFoldable (Lean.Expr.proj typeName idx struct) args = pure true
• Blaster.Optimize.unfoldOpaqueFunDef.isFoldable f args = pure false

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

Return true when the following conditions are satisfied:

• f is an opaque relation function
• f has a sort parameter not in relationalCompatibleTypes
• f is an alias to a well-founded recursive definition.

Equations

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

partial def Blaster.Optimize.hasSorryTheorem (e : Lean.Expr) (msg : Lean.MessageData) : TranslateEnvT Unit

Trigger an error if e contains at least one theorem with sorry demonstration.

partial def Blaster.Optimize.hasSorryTheorem.findSorry (msg : Lean.MessageData) (e : Lean.Expr) : TranslateEnvT Unit

def Blaster.Optimize.updateMatchReturnType (eType pType : Lean.Expr) : TranslateEnvT Lean.Expr

Given pType := λ α₁ → .. → λ αₙ → t returns λ α₁ → .. → λ αₙ → eType This function is expected to be used only when updating a match return type

Equations

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