Constant folding for primitives that have special runtime support.

def Lean.Compiler.mkLcProof (p : Lean.Expr) : Lean.Expr

Equations

• Lean.Compiler.mkLcProof p = Lean.mkApp (Lean.mkConst `lcProof) p

@[reducible, inline]

abbrev Lean.Compiler.BinFoldFn : Type

Equations

• Lean.Compiler.BinFoldFn = (Bool → Lean.Expr → Lean.Expr → Option Lean.Expr)

@[reducible, inline]

abbrev Lean.Compiler.UnFoldFn : Type

Equations

• Lean.Compiler.UnFoldFn = (Bool → Lean.Expr → Option Lean.Expr)

def Lean.Compiler.mkUIntTypeName (nbytes : Nat) : Lake.Name

Equations

• Lean.Compiler.mkUIntTypeName nbytes = Lean.Name.mkSimple ("UInt" ++ toString nbytes)

structure Lean.Compiler.NumScalarTypeInfo : Type

• nbits : Nat
• id : Lake.Name
• ofNatFn : Lake.Name
• toNatFn : Lake.Name
• size : Nat

def Lean.Compiler.numScalarTypes : List Lean.Compiler.NumScalarTypeInfo

Equations

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

def Lean.Compiler.isOfNat (fn : Lake.Name) : Bool

Equations

• Lean.Compiler.isOfNat fn = Lean.Compiler.numScalarTypes.any fun (info : Lean.Compiler.NumScalarTypeInfo) => info.ofNatFn == fn

def Lean.Compiler.isToNat (fn : Lake.Name) : Bool

Equations

• Lean.Compiler.isToNat fn = Lean.Compiler.numScalarTypes.any fun (info : Lean.Compiler.NumScalarTypeInfo) => info.toNatFn == fn

def Lean.Compiler.getInfoFromFn (fn : Lake.Name) : List Lean.Compiler.NumScalarTypeInfo → Option Lean.Compiler.NumScalarTypeInfo

Equations

• Lean.Compiler.getInfoFromFn fn [] = none
• Lean.Compiler.getInfoFromFn fn (info :: infos) = if (info.ofNatFn == fn) = true then some info else Lean.Compiler.getInfoFromFn fn infos

def Lean.Compiler.getInfoFromVal : Lean.Expr → Option Lean.Compiler.NumScalarTypeInfo

Equations

• Lean.Compiler.getInfoFromVal ((Lean.Expr.const fn us).app arg) = Lean.Compiler.getInfoFromFn fn Lean.Compiler.numScalarTypes
• Lean.Compiler.getInfoFromVal x = none

@[export lean_get_num_lit]

def Lean.Compiler.getNumLit : Lean.Expr → Option Nat

Equations

• Lean.Compiler.getNumLit (Lean.Expr.lit (Lean.Literal.natVal n)) = some n
• Lean.Compiler.getNumLit ((Lean.Expr.const fn us).app a) = if Lean.Compiler.isOfNat fn = true then Lean.Compiler.getNumLit a else none
• Lean.Compiler.getNumLit x = none

def Lean.Compiler.mkUIntLit (info : Lean.Compiler.NumScalarTypeInfo) (n : Nat) : Lean.Expr

Equations

• Lean.Compiler.mkUIntLit info n = Lean.mkApp (Lean.mkConst info.ofNatFn) (Lean.mkRawNatLit (n % info.size))

def Lean.Compiler.mkUInt32Lit (n : Nat) : Lean.Expr

Equations

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

def Lean.Compiler.foldBinUInt (fn : Lean.Compiler.NumScalarTypeInfo → Bool → Nat → Nat → Nat) (beforeErasure : Bool) (a₁ : Lean.Expr) (a₂ : Lean.Expr) : Option Lean.Expr

Equations

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

def Lean.Compiler.foldUIntAdd (beforeErasure : Bool) (a₁ : Lean.Expr) (a₂ : Lean.Expr) : Option Lean.Expr

Equations

• Lean.Compiler.foldUIntAdd = Lean.Compiler.foldBinUInt fun (x : Lean.Compiler.NumScalarTypeInfo) (x : Bool) => Add.add

def Lean.Compiler.foldUIntMul (beforeErasure : Bool) (a₁ : Lean.Expr) (a₂ : Lean.Expr) : Option Lean.Expr

Equations

• Lean.Compiler.foldUIntMul = Lean.Compiler.foldBinUInt fun (x : Lean.Compiler.NumScalarTypeInfo) (x : Bool) => Mul.mul

def Lean.Compiler.foldUIntDiv (beforeErasure : Bool) (a₁ : Lean.Expr) (a₂ : Lean.Expr) : Option Lean.Expr

Equations

• Lean.Compiler.foldUIntDiv = Lean.Compiler.foldBinUInt fun (x : Lean.Compiler.NumScalarTypeInfo) (x : Bool) => Div.div

def Lean.Compiler.foldUIntMod (beforeErasure : Bool) (a₁ : Lean.Expr) (a₂ : Lean.Expr) : Option Lean.Expr

Equations

• Lean.Compiler.foldUIntMod = Lean.Compiler.foldBinUInt fun (x : Lean.Compiler.NumScalarTypeInfo) (x : Bool) => Mod.mod

def Lean.Compiler.foldUIntSub (beforeErasure : Bool) (a₁ : Lean.Expr) (a₂ : Lean.Expr) : Option Lean.Expr

Equations

• Lean.Compiler.foldUIntSub = Lean.Compiler.foldBinUInt fun (info : Lean.Compiler.NumScalarTypeInfo) (x : Bool) (a b : Nat) => a + (info.size - b)

def Lean.Compiler.preUIntBinFoldFns : List (Lake.Name × Lean.Compiler.BinFoldFn)

Equations

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

def Lean.Compiler.uintBinFoldFns : List (Lake.Name × Lean.Compiler.BinFoldFn)

Equations

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

def Lean.Compiler.foldNatBinOp (fn : Nat → Nat → Nat) (a₁ : Lean.Expr) (a₂ : Lean.Expr) : Option Lean.Expr

Equations

• Lean.Compiler.foldNatBinOp fn a₁ a₂ = do let n₁ ← Lean.Compiler.getNumLit a₁ let n₂ ← Lean.Compiler.getNumLit a₂ pure (Lean.mkRawNatLit (fn n₁ n₂))

def Lean.Compiler.foldNatAdd : Bool → Lean.Expr → Lean.Expr → Option Lean.Expr

Equations

• Lean.Compiler.foldNatAdd x = Lean.Compiler.foldNatBinOp Add.add

def Lean.Compiler.foldNatMul : Bool → Lean.Expr → Lean.Expr → Option Lean.Expr

Equations

• Lean.Compiler.foldNatMul x = Lean.Compiler.foldNatBinOp Mul.mul

def Lean.Compiler.foldNatDiv : Bool → Lean.Expr → Lean.Expr → Option Lean.Expr

Equations

• Lean.Compiler.foldNatDiv x = Lean.Compiler.foldNatBinOp Div.div

def Lean.Compiler.foldNatMod : Bool → Lean.Expr → Lean.Expr → Option Lean.Expr

Equations

• Lean.Compiler.foldNatMod x = Lean.Compiler.foldNatBinOp Mod.mod

def Lean.Compiler.natPowThreshold : Nat

Equations

• Lean.Compiler.natPowThreshold = 256

def Lean.Compiler.foldNatPow : Bool → Lean.Expr → Lean.Expr → Option Lean.Expr

Equations

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

def Lean.Compiler.mkNatEq (a : Lean.Expr) (b : Lean.Expr) : Lean.Expr

Equations

• Lean.Compiler.mkNatEq a b = Lean.mkAppN (Lean.mkConst `Eq [Lean.levelOne]) #[Lean.mkConst `Nat, a, b]

def Lean.Compiler.mkNatLt (a : Lean.Expr) (b : Lean.Expr) : Lean.Expr

Equations

• Lean.Compiler.mkNatLt a b = Lean.mkAppN (Lean.mkConst `LT.lt [Lean.levelZero]) #[Lean.mkConst `Nat, Lean.mkConst `Nat.lt, a, b]

def Lean.Compiler.mkNatLe (a : Lean.Expr) (b : Lean.Expr) : Lean.Expr

Equations

• Lean.Compiler.mkNatLe a b = Lean.mkAppN (Lean.mkConst `LE.le [Lean.levelZero]) #[Lean.mkConst `Nat, Lean.mkConst `Nat.le, a, b]

def Lean.Compiler.toDecidableExpr (beforeErasure : Bool) (pred : Lean.Expr) (r : Bool) : Lean.Expr

Equations

• Lean.Compiler.toDecidableExpr false pred true = Lean.mkConst `Bool.true
• Lean.Compiler.toDecidableExpr false pred false = Lean.mkConst `Bool.false
• Lean.Compiler.toDecidableExpr true pred true = Lean.mkDecIsTrue pred (Lean.Compiler.mkLcProof pred)
• Lean.Compiler.toDecidableExpr true pred false = Lean.mkDecIsFalse pred (Lean.Compiler.mkLcProof pred)

def Lean.Compiler.foldNatBinPred (mkPred : Lean.Expr → Lean.Expr → Lean.Expr) (fn : Nat → Nat → Bool) (beforeErasure : Bool) (a₁ : Lean.Expr) (a₂ : Lean.Expr) : Option Lean.Expr

Equations

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

def Lean.Compiler.foldNatDecEq (beforeErasure : Bool) (a₁ : Lean.Expr) (a₂ : Lean.Expr) : Option Lean.Expr

Equations

• Lean.Compiler.foldNatDecEq = Lean.Compiler.foldNatBinPred Lean.Compiler.mkNatEq fun (a b : Nat) => decide (a = b)

def Lean.Compiler.foldNatDecLt (beforeErasure : Bool) (a₁ : Lean.Expr) (a₂ : Lean.Expr) : Option Lean.Expr

Equations

• Lean.Compiler.foldNatDecLt = Lean.Compiler.foldNatBinPred Lean.Compiler.mkNatLt fun (a b : Nat) => decide (a < b)

def Lean.Compiler.foldNatDecLe (beforeErasure : Bool) (a₁ : Lean.Expr) (a₂ : Lean.Expr) : Option Lean.Expr

Equations

• Lean.Compiler.foldNatDecLe = Lean.Compiler.foldNatBinPred Lean.Compiler.mkNatLe fun (a b : Nat) => decide (a ≤ b)

def Lean.Compiler.foldNatBinBoolPred (fn : Nat → Nat → Bool) (a₁ : Lean.Expr) (a₂ : Lean.Expr) : Option Lean.Expr

Equations

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

def Lean.Compiler.foldNatBeq : Bool → Lean.Expr → Lean.Expr → Option Lean.Expr

Equations

• Lean.Compiler.foldNatBeq x = Lean.Compiler.foldNatBinBoolPred fun (a b : Nat) => a == b

def Lean.Compiler.foldNatBle : Bool → Lean.Expr → Lean.Expr → Option Lean.Expr

Equations

• Lean.Compiler.foldNatBle x = Lean.Compiler.foldNatBinBoolPred fun (a b : Nat) => decide (a < b)

def Lean.Compiler.foldNatBlt : Bool → Lean.Expr → Lean.Expr → Option Lean.Expr

Equations

• Lean.Compiler.foldNatBlt x = Lean.Compiler.foldNatBinBoolPred fun (a b : Nat) => decide (a ≤ b)

def Lean.Compiler.natFoldFns : List (Lake.Name × Lean.Compiler.BinFoldFn)

Equations

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

def Lean.Compiler.getBoolLit : Lean.Expr → Option Bool

Equations

• Lean.Compiler.getBoolLit (Lean.Expr.const `Bool.true us) = some true
• Lean.Compiler.getBoolLit (Lean.Expr.const `Bool.false us) = some false
• Lean.Compiler.getBoolLit x = none

def Lean.Compiler.foldStrictAnd : Bool → Lean.Expr → Lean.Expr → Option Lean.Expr

Equations

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

def Lean.Compiler.foldStrictOr : Bool → Lean.Expr → Lean.Expr → Option Lean.Expr

Equations

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

def Lean.Compiler.boolFoldFns : List (Lake.Name × Lean.Compiler.BinFoldFn)

Equations

• Lean.Compiler.boolFoldFns = [(`strictOr, Lean.Compiler.foldStrictOr), (`strictAnd, Lean.Compiler.foldStrictAnd)]

def Lean.Compiler.binFoldFns : List (Lake.Name × Lean.Compiler.BinFoldFn)

Equations

• Lean.Compiler.binFoldFns = Lean.Compiler.boolFoldFns ++ Lean.Compiler.uintBinFoldFns ++ Lean.Compiler.natFoldFns

def Lean.Compiler.foldNatSucc : Bool → Lean.Expr → Option Lean.Expr

Equations

• Lean.Compiler.foldNatSucc x a = do let n ← Lean.Compiler.getNumLit a pure (Lean.mkRawNatLit (n + 1))

def Lean.Compiler.foldCharOfNat (beforeErasure : Bool) (a : Lean.Expr) : Option Lean.Expr

Equations

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

def Lean.Compiler.foldToNat (size : Nat) : Bool → Lean.Expr → Option Lean.Expr

Equations

• Lean.Compiler.foldToNat size x a = do let n ← Lean.Compiler.getNumLit a pure (Lean.mkRawNatLit (n % size))

def Lean.Compiler.uintFoldToNatFns : List (Lake.Name × Lean.Compiler.UnFoldFn)

Equations

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

def Lean.Compiler.unFoldFns : List (Lake.Name × Lean.Compiler.UnFoldFn)

Equations

• Lean.Compiler.unFoldFns = [(`Nat.succ, Lean.Compiler.foldNatSucc), (`Char.ofNat, Lean.Compiler.foldCharOfNat)] ++ Lean.Compiler.uintFoldToNatFns

def Lean.Compiler.findBinFoldFn (fn : Lake.Name) : Option Lean.Compiler.BinFoldFn

Equations

• Lean.Compiler.findBinFoldFn fn = List.lookup fn Lean.Compiler.binFoldFns

def Lean.Compiler.findUnFoldFn (fn : Lake.Name) : Option Lean.Compiler.UnFoldFn

Equations

• Lean.Compiler.findUnFoldFn fn = List.lookup fn Lean.Compiler.unFoldFns

@[export lean_fold_bin_op]

def Lean.Compiler.foldBinOp (beforeErasure : Bool) (f : Lean.Expr) (a : Lean.Expr) (b : Lean.Expr) : Option Lean.Expr

Equations

• Lean.Compiler.foldBinOp beforeErasure (Lean.Expr.const fn us) a b = do let foldFn ← Lean.Compiler.findBinFoldFn fn foldFn beforeErasure a b
• Lean.Compiler.foldBinOp beforeErasure f a b = failure

@[export lean_fold_un_op]

def Lean.Compiler.foldUnOp (beforeErasure : Bool) (f : Lean.Expr) (a : Lean.Expr) : Option Lean.Expr

Equations

• Lean.Compiler.foldUnOp beforeErasure (Lean.Expr.const fn us) a = do let foldFn ← Lean.Compiler.findUnFoldFn fn foldFn beforeErasure a
• Lean.Compiler.foldUnOp beforeErasure f a = failure