@[inline]

partial def Blaster.Optimize.normLevel (l : Lean.Level) : Lean.Level

Perform the following normalization on l

• When l := .param .. ∨ l := .mvar ..
  • return .succ .zero
• When l := .succ l'
  • return .succ (normLevel l')
• Otherwise
  • return l

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

Given `e := Expr.const n l, apply the following normalization rule:

• When n := Nat.zero return Expr.lit (Literal.natVal 0)

• When n := Nat.pred

  • return λ n => n - 1

• When n := Nat.succ

  • return λ n => 1 + n

• When n := Nat.le

  • return mkNatLeOp

• When n := Nat.ble ∧ (← isOptimizeRecCall):

  • return λ x y => decide' (x ≤ y)

• When n := Nat.beq ∧ (← isOptimizeRecCall):

  • return λ x y => x == y

• When n := Int.negSucc ∧ ¬ (← isInFunApp)

  • return λ n => Int.neg (Int.ofNat (1 + n))

• When n := Int.le

  • return mkIntLeOp

• When n := ite

  • return λ (α : Sort u) (p : Prop) [h : Decidable p] (t e : α) => Blaster.dite' α p (fun _ => t) (fun _ => e)

• When n := dite

  • return λ (α : Sort u) (p : Prop) [h : Decidable p] (t : p → α) (e : ¬ p → α) => Blaster.dite' α p t e

• When n := Decidable.decide

  • return λ (p : Prop) [h : Decidable p] => Blaster.decide' p

• When `¬ (← isInFunApp):

  • When ¬ hasImplicitArgs e:
    • When isRecursiveFun n (i.e., a recursive function passed as argument):
      • return (← normOpaqueAndRecFun e #[] optimizer)
    • When (← getFunBody e).isSome ∧ ¬ isRecursiveFun n ∧ ¬ isNotFoldable e:
      • return optimizer (← getFunBody e)

• When (← isInFunApp) ∧ ¬ isNotFoldable e ∧ ¬ hasImplicitArgs e ∧ (← getFunBody e).isSome:

  • return ← getFunBody e

• Otherwise:

  • When isResolvebleType e :
    • return mkExpr (← resolveTypeAbbrev e)
  • Otherwise
    • return mkExpr e

Equations

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

@[inline]

def Blaster.Optimize.normConst.normConstLevel (n : Lean.Name) (xs : List Lean.Level) : Lean.Expr

Normalizing level in Expr.const due to normalization perform on sort (see normSort in Basic)

Equations

• Blaster.Optimize.normConst.normConstLevel n xs = Lean.Expr.const n (List.map Blaster.Optimize.normLevel xs)

@[inline]

def Blaster.Optimize.normConst.isToNormOpaqueFun (e : Lean.Expr) (stack : List OptimizeStack) (n : Lean.Name) : TranslateEnvT (Option OptimizeContinuity)

Apply the following normalization rules on opaque functions:

• Nat.pred ==> λ n => n - 1
• Nat.succ ==> λ n => 1 + n
• Nat.le ==> ≤
• Nat.ble ==> λ x y => Blaster.decide' (x ≤ y) (if isOptimizeRecCall)
• Nat.beq ==> λ x y => x == y (if isOptimizeRecCall)
• Int.negSucc ==> λ n => Int.neg (Int.ofNat (1 + n)) (if ¬ isInFunApp)
• Int.le ==> ≤
• ite ==> λ (α : Sort u) (p : Prop) [h : Decidable p] (t e : α) => Blaster.dite' α p (fun _ => t) (fun _ => e)
• dite ==> λ (α : Sort u) (p : Prop) [h : Decidable p] (t : p → α) (e : ¬ p → α) => Blaster.dite' α p t e
• Decidable.decide ==> λ (p : Prop) [h : Decidable p] => Blaster.decide' p

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Optimize.normConst.isToNormOpaqueFun e stack `Nat.le = do let __do_lift ← Blaster.Optimize.mkNatLeOp let a ← Blaster.Optimize.stackContinuity stack __do_lift pure (some a)
• Blaster.Optimize.normConst.isToNormOpaqueFun e stack `Int.le = do let __do_lift ← Blaster.Optimize.mkIntLeOp let a ← Blaster.Optimize.stackContinuity stack __do_lift pure (some a)
• Blaster.Optimize.normConst.isToNormOpaqueFun e stack n = pure none

@[inline]

def Blaster.Optimize.normConst.isHOF (stack : List OptimizeStack) (f : Lean.Name) (e : Lean.Expr) : TranslateEnvT (Option OptimizeContinuity)

Equations

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