@[implemented_by _private.Blaster.Optimize.Expr.0.Blaster.Optimize.exprEqUnsafe]

def Blaster.Optimize.exprEq (op1 op2 : Lean.Expr) : Bool

Safe implementation of physically equivalence for Expr.

Equations

• Blaster.Optimize.exprEq op1 op2 = (op1 == op2)

@[inline]

def Blaster.Optimize.instantiate1' (e subst : Lean.Expr) : Lean.Expr

Equations

• Blaster.Optimize.instantiate1' e subst = if e.hasLooseBVars = true then e.instantiate1 subst else e

@[inline]

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

Return true if e contains free / bounded variables.

Equations

• Blaster.Optimize.hasVars e = (e.hasFVar || e.hasLooseBVars)

structure Blaster.Optimize.stkEntry : Type

• prev : Lean.Expr
• next : Lean.Expr

instance Blaster.Optimize.instInhabitedStkEntry : Inhabited stkEntry

Equations

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

def Blaster.Optimize.instInhabitedStkEntry.default : stkEntry

Equations

• Blaster.Optimize.instInhabitedStkEntry.default = { prev := default, next := default }

@[inline]

unsafe def Blaster.Optimize.containsFVarImp (e : Lean.Expr) (v : Lean.FVarId) : Bool

Return true iff e contains a free variable v.

Equations

• Blaster.Optimize.containsFVarImp e v = Blaster.Optimize.containsFVarImp.visit v e (Array.emptyWithCapacity e.approxDepth.toNat) Std.HashSet.emptyWithCapacity

unsafe def Blaster.Optimize.containsFVarImp.visit (v : Lean.FVarId) (e : Lean.Expr) (stk : Array stkEntry) (cache : Std.HashSet Lean.Expr) : Bool

Equations

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

@[implemented_by Blaster.Optimize.containsFVarImp]

def Blaster.Optimize.containsFVar (e : Lean.Expr) (v : Lean.FVarId) : Bool

Equations

• Blaster.Optimize.containsFVar e v = e.containsFVar v

@[inline]

def Blaster.Optimize.fVarInExpr (v : Lean.FVarId) (e : Lean.Expr) : Bool

Return true if v occurs at least once in e.

Equations

• Blaster.Optimize.fVarInExpr v e = if e.hasFVar = true then Blaster.Optimize.containsFVar e v else false

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

If the e is a sequence of lambda fun x₁ => fun x₂ => ... fun xₙ => b, return b. Otherwise return e.

Equations

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

@[inline]

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

Determine if e is a boolean not expression and return its corresponding argument. Otherwise return none.

Equations

• Blaster.Optimize.boolNot? ((Lean.Expr.const `Bool.not us).app n) = some n
• Blaster.Optimize.boolNot? e = none

@[inline]

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

Determine if e is a boolean and expression and return its corresponding argument. Otherwise return none.

Equations

• Blaster.Optimize.boolAnd? (((Lean.Expr.const `Bool.and us).app op1).app op2) = some (op1, op2)
• Blaster.Optimize.boolAnd? e = none

@[inline]

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

Determine if e is a boolean or expression and return its corresponding argument. Otherwise return none.

Equations

• Blaster.Optimize.boolOr? (((Lean.Expr.const `Bool.or us).app op1).app op2) = some (op1, op2)
• Blaster.Optimize.boolOr? e = none

@[inline]

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

Determine if e is a Bool literal expression b and return some b. Otherwise none

Equations

• Blaster.Optimize.isBoolValue? (Lean.Expr.const `Bool.true us) = some true
• Blaster.Optimize.isBoolValue? (Lean.Expr.const `Bool.false us) = some false
• Blaster.Optimize.isBoolValue? e = none

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

Return true only when e is a Bool literal. Otherwise false`

Equations

• Blaster.Optimize.isBoolCtor (Lean.Expr.const `Bool.true us) = true
• Blaster.Optimize.isBoolCtor (Lean.Expr.const `Bool.false us) = true
• Blaster.Optimize.isBoolCtor e = false

@[inline]

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

Determine if e is an boolean == expression and return its corresponding arguments. Otherwise return none.

Equations

• Blaster.Optimize.beq? (((((Lean.Expr.const `BEq.beq us).app psort).app pdecide).app e1).app e2) = some (psort, pdecide, e1, e2)
• Blaster.Optimize.beq? e = none

@[inline]

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

Determine if e is an Eq expression and return its corresponding arguments. Otherwise return none.

Equations

• Blaster.Optimize.eq? ((((Lean.Expr.const `Eq us).app psort).app e1).app e2) = some (psort, e1, e2)
• Blaster.Optimize.eq? e = none

@[inline]

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

Determine if e is an LE.le expression and return its corresponding arguments. Otherwise return none.

Equations

• Blaster.Optimize.le? (((((Lean.Expr.const `LE.le us).app psort).app pinst).app e1).app e2) = some (psort, pinst, e1, e2)
• Blaster.Optimize.le? e = none

@[inline]

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

Determine if e is an LT.lt expression and return its corresponding arguments. Otherwise return none.

Equations

• Blaster.Optimize.lt? (((((Lean.Expr.const `LT.lt us).app psort).app pinst).app e1).app e2) = some (psort, pinst, e1, e2)
• Blaster.Optimize.lt? e = none

@[inline]

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

Determine if e is an Not expression and return its corresponding argument. Otherwise return none.

Equations

• Blaster.Optimize.propNot? ((Lean.Expr.const `Not us).app n) = some n
• Blaster.Optimize.propNot? e = none

@[inline]

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

Determine if e is an And expression and return its corresponding arguments. Otherwise return none.

Equations

• Blaster.Optimize.propAnd? (((Lean.Expr.const `And us).app op1).app op2) = some (op1, op2)
• Blaster.Optimize.propAnd? e = none

@[inline]

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

Determine if e is an Or expression and return its corresponding arguments. Otherwise return none.

Equations

• Blaster.Optimize.propOr? (((Lean.Expr.const `Or us).app op1).app op2) = some (op1, op2)
• Blaster.Optimize.propOr? e = none

def Blaster.Optimize.isNotExprOf (e1 e2 : Lean.Expr) : Bool

Return true when e1 := ¬ ne ∧ ne =ₚₜᵣ e2. Otherwise false.

Equations

• Blaster.Optimize.isNotExprOf e1 e2 = match Blaster.Optimize.propNot? e1 with | some op => Blaster.Optimize.exprEq e2 op | x => false

def Blaster.Optimize.isBoolNotExprOf (e1 e2 : Lean.Expr) : Bool

Return true when e1 := not ne ∧ ne =ₚₜᵣ e2. Otherwise false.

Equations

• Blaster.Optimize.isBoolNotExprOf e1 e2 = match Blaster.Optimize.boolNot? e1 with | some op => Blaster.Optimize.exprEq e2 op | x => false

def Blaster.Optimize.isNegBoolEqOf (e1 e2 : Lean.Expr) : Bool

Return true when e1 := false = c ∧ e2 := true = c.

Equations

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

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

Return true if the given expression is of the form const ``Bool.

Equations

• Blaster.Optimize.isBoolType (Lean.Expr.const `Bool us) = true
• Blaster.Optimize.isBoolType e = false

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

Return true if the given expression is of the form const ``Nat.

Equations

• Blaster.Optimize.isNatType (Lean.Expr.const `Nat us) = true
• Blaster.Optimize.isNatType e = false

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

Return true if the given expression is of the form const ``Int.

Equations

• Blaster.Optimize.isIntType (Lean.Expr.const `Int us) = true
• Blaster.Optimize.isIntType e = false

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

Return true if the given expression is of the form const ``String.

Equations

• Blaster.Optimize.isStringType (Lean.Expr.const `String us) = true
• Blaster.Optimize.isStringType e = false

@[inline]

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

Determine if e is an autoParam expression and return its corresponding arguments. Otherwise return none.

Equations

• Blaster.Optimize.autoParam? (((Lean.Expr.const `autoParam us).app t).app tac) = some (t, tac)
• Blaster.Optimize.autoParam? e = none

@[inline]

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

Return true only when e is a Nat literal expression Expr.lit (Literal.natVal n)

Equations

• Blaster.Optimize.isNatValue (Lean.Expr.lit (Lean.Literal.natVal val)) = true
• Blaster.Optimize.isNatValue e = false

@[inline]

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

Determine if e is a Nat literal expression Expr.lit (Literal.natVal n) and return some n as result. Otherwise return none NOTE: This function is to be used only when it is guaranteed that Nat.zero has been normalized to Expr.lit (Literal.natVal 0).

Equations

• Blaster.Optimize.isNatValue? (Lean.Expr.lit (Lean.Literal.natVal val)) = some val
• Blaster.Optimize.isNatValue? e = none

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

Determine if e is a String literal expression Expr.lit (Literal.strVal s) and return some s as result. Otherwise return none.

Equations

• Blaster.Optimize.isStrValue? (Lean.Expr.lit (Lean.Literal.strVal s)) = some s
• Blaster.Optimize.isStrValue? e = none

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

Determine if e is a UInt32 literal expression UInt32.mk (Fin.mk UInt32.size n isLt) and return some n only when n < UInt32.size. Otherwise return none

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Optimize.isUInt32Value? ((Lean.Expr.const `UInt32.ofBitVec us).app (((Lean.Expr.const `BitVec.ofFin us_1).app arg).app fn2)) = none
• Blaster.Optimize.isUInt32Value? ((Lean.Expr.const `UInt32.ofBitVec us).app fn1) = none
• Blaster.Optimize.isUInt32Value? e = none

@[inline]

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

Determine if e is a Char literal expression Char.mk (UInt32.mk (Fin.mk UInt32.size n isLt) and return some Char.ofNat n) only when Nat.isValidChar n. Otherwise return none

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Optimize.isCharValue? e = none

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

Return true if e := Nat.add e1 e2. Otherwise return false. Note that true is returned only when e is a fully applied `Nat.add expression.

Equations

• Blaster.Optimize.isNatAddExpr (((Lean.Expr.const `Nat.add us).app arg).app arg_1) = true
• Blaster.Optimize.isNatAddExpr e = false

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

Return true if e := Nat.sub e1 e2. Otherwise return false. Note that true is returned only when e is a fully applied `Nat.sub expression.

Equations

• Blaster.Optimize.isNatSubExpr (((Lean.Expr.const `Nat.sub us).app arg).app arg_1) = true
• Blaster.Optimize.isNatSubExpr e = false

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

Return true if e := Nat.pow e1 e2. Otherwise return false. Note that true is returned only when e is a fully applied `Nat.pow expression.

Equations

• Blaster.Optimize.isNatPowExpr (((Lean.Expr.const `Nat.pow us).app arg).app arg_1) = true
• Blaster.Optimize.isNatPowExpr e = false

@[inline]

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

Determine if e is a Nat.mul expression and return its corresponding arguments. Otherwise return none.

Equations

• Blaster.Optimize.natMul? (((Lean.Expr.const `Nat.mul us).app op1).app op2) = some (op1, op2)
• Blaster.Optimize.natMul? e = none

@[inline]

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

Determine if e is a Nat.add expression and return its corresponding arguments. Otherwise return none.

Equations

• Blaster.Optimize.natAdd? (((Lean.Expr.const `Nat.add us).app arg).app arg_1) = some (arg, arg_1)
• Blaster.Optimize.natAdd? e = none

@[inline]

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

Determine if e is a Nat.sub expression and return its corresponding arguments. Otherwise return none.

Equations

• Blaster.Optimize.natSub? (((Lean.Expr.const `Nat.sub us).app arg).app arg_1) = some (arg, arg_1)
• Blaster.Optimize.natSub? e = none

@[inline]

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

Determine if e is a Nat.pow expression and return its corresponding arguments. Otherwise return none.

Equations

• Blaster.Optimize.natPow? (((Lean.Expr.const `Nat.pow us).app arg).app arg_1) = some (arg, arg_1)
• Blaster.Optimize.natPow? e = none

@[inline]

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

Return some (f, op1, op2) when e is a binary operator. Otherwise none.

Equations

• Blaster.Optimize.binOp? ((f.app op1).app op2) = if f.isApp = true then none else some (f, op1, op2)
• Blaster.Optimize.binOp? e = none

@[inline]

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

Determine if e is an Int.neg expression and return its corresponding argument. Otherwise return none.

Equations

• Blaster.Optimize.intNeg? ((Lean.Expr.const `Int.neg us).app n) = some n
• Blaster.Optimize.intNeg? e = none

@[inline]

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

Determine if e is a Int.add expression and return its corresponding arguments. Otherwise return none.

Equations

• Blaster.Optimize.intAdd? (((Lean.Expr.const `Int.add us).app op1).app op2) = some (op1, op2)
• Blaster.Optimize.intAdd? e = none

@[inline]

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

Determine if e is a Int.mul expression and return its corresponding arguments. Otherwise return none.

Equations

• Blaster.Optimize.intMul? (((Lean.Expr.const `Int.mul us).app op1).app op2) = some (op1, op2)
• Blaster.Optimize.intMul? e = none

@[inline]

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

Determine if e is a Int.tdiv expression and return its corresponding arguments. Otherwise return none.

Equations

• Blaster.Optimize.intTDiv? (((Lean.Expr.const `Int.tdiv us).app op1).app op2) = some (op1, op2)
• Blaster.Optimize.intTDiv? e = none

@[inline]

def Blaster.Optimize.isIntNegExprOf (e1 e2 : Lean.Expr) : Bool

Return true when e1 := -ne ∧ ne =ₚₜᵣ e2. Otherwise false.

Equations

• Blaster.Optimize.isIntNegExprOf e1 e2 = match Blaster.Optimize.intNeg? e1 with | some op => Blaster.Optimize.exprEq e2 op | x => false

@[inline]

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

Determine if e is a Blaster.decide' expression and return its corresponding arguments. Otherwise return none.

Equations

• Blaster.Optimize.decide'? ((Lean.Expr.const `Blaster.decide' us).app op) = some op
• Blaster.Optimize.decide'? e = none

@[inline]

def Blaster.Optimize.ite'? (e : Lean.Expr) : Option (Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr)

Determine if e is an Blaster.ite' expression and return its corresponding arguments. Otherwise return none.

Equations

• Blaster.Optimize.ite'? (((((Lean.Expr.const `Blaster.ite' us).app psort).app pcond).app e1).app e2) = some (psort, pcond, e1, e2)
• Blaster.Optimize.ite'? e = none

@[inline]

def Blaster.Optimize.dite'? (e : Lean.Expr) : Option (Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr)

Determine if e is an Blaster.dite' expression and return its corresponding arguments. Otherwise return none.

Equations

• Blaster.Optimize.dite'? (((((Lean.Expr.const `Blaster.dite' us).app psort).app pcond).app e1).app e2) = some (psort, pcond, e1, e2)
• Blaster.Optimize.dite'? e = none

@[inline]

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

Return true only when e := Expr.const ``Blaster.dite' _ Otherwise false.

Equations

• Blaster.Optimize.isBlasterDiteConst (Lean.Expr.const `Blaster.dite' us) = true
• Blaster.Optimize.isBlasterDiteConst e = false

@[inline]

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

Return true only when e is a Int expression corresponding to one of the following:

• Int.ofNat (Expr.lit (Literal.natVal n))
• Int.negSucc (Expr.lit (Literal.natVal n))

Equations

• Blaster.Optimize.isIntValue ((Lean.Expr.const `Int.ofNat us).app a) = if Blaster.Optimize.isNatValue a = true then true else false
• Blaster.Optimize.isIntValue ((Lean.Expr.const `Int.negSucc us).app a) = if Blaster.Optimize.isNatValue a = true then true else false
• Blaster.Optimize.isIntValue (f.app a) = if Blaster.Optimize.isNatValue a = true then false else false
• Blaster.Optimize.isIntValue e = false

@[inline]

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

Determine if e is a Int expression corresponding to one of the following:

• Int.ofNat (Expr.lit (Literal.natVal n))
• Int.negSucc (Expr.lit (Literal.natVal n)) Return either some (Int.ofNat n) or some (Int.negSucc n) as result. Otherwise return none NOTE: This function is to be used only when it is guaranteed that Nat.zero has been normalized to Expr.lit (Literal.natVal 0).

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Optimize.isIntValue? e = none

def Blaster.Optimize.betaForAll (e : Lean.Expr) (args : Array Lean.Expr) : Lean.Expr

Given e of the form ∀ (a₁ : A₁) ... (aₙ : Aₙ), B[a₁, ..., aₙ] and p₁ : A₁, ... pₘ : Aₙ, return B[p₁, ..., pₘ].

Equations

• Blaster.Optimize.betaForAll e args = Blaster.Optimize.betaForAll.visit args 0 e

partial def Blaster.Optimize.betaForAll.visit (args : Array Lean.Expr) (i : Nat) (e : Lean.Expr) : Lean.Expr

@[inline]

def Blaster.Optimize.betaLambda (e : Lean.Expr) (args : Array Lean.Expr) : Lean.Expr

Equations

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

def Blaster.Optimize.betaLambda.visit (args : Array Lean.Expr) (finish : Lean.Expr → Nat → Lean.Expr) (e : Lean.Expr) (i : Nat) : Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Optimize.betaLambda.visit args finish e i = if i < args.size then Lean.mkAppN (finish e i) (args.extract i) else finish e i

def Blaster.Optimize.headBeta' (e : Lean.Expr) : Lean.Expr

(fun x => e) a ==> e[x/a].

Equations

• Blaster.Optimize.headBeta' e = if e.getAppFn'.isLambda = true then Blaster.Optimize.betaLambda e.getAppFn' e.getAppArgs else e

@[inline]

def Blaster.Optimize.isQuantifiedFun (e : Lean.Expr) : Lean.MetaM Bool

Return true only when e is a FVar of type ∀ α₀ → ... → αₙ.

Equations

• Blaster.Optimize.isQuantifiedFun (Lean.Expr.fvar v) = do let __do_lift ← v.getType pure __do_lift.isForall
• Blaster.Optimize.isQuantifiedFun e = pure false