@[inline]
@[inline]
Equations
- Lean.Compiler.mkUIntTypeName nbytes = Lean.Name.mkSimple ("UInt" ++ toString nbytes)
Equations
- Lean.Compiler.numScalarTypes = [{ nbits := 8, id := Lean.Compiler.mkUIntTypeName 8, ofNatFn := Lean.Name.mkStr (Lean.Compiler.mkUIntTypeName 8) "ofNat", toNatFn := Lean.Name.mkStr (Lean.Compiler.mkUIntTypeName 8) "toNat", size := 2 ^ 8 }, { nbits := 16, id := Lean.Compiler.mkUIntTypeName 16, ofNatFn := Lean.Name.mkStr (Lean.Compiler.mkUIntTypeName 16) "ofNat", toNatFn := Lean.Name.mkStr (Lean.Compiler.mkUIntTypeName 16) "toNat", size := 2 ^ 16 }, { nbits := 32, id := Lean.Compiler.mkUIntTypeName 32, ofNatFn := Lean.Name.mkStr (Lean.Compiler.mkUIntTypeName 32) "ofNat", toNatFn := Lean.Name.mkStr (Lean.Compiler.mkUIntTypeName 32) "toNat", size := 2 ^ 32 }, { nbits := 64, id := Lean.Compiler.mkUIntTypeName 64, ofNatFn := Lean.Name.mkStr (Lean.Compiler.mkUIntTypeName 64) "ofNat", toNatFn := Lean.Name.mkStr (Lean.Compiler.mkUIntTypeName 64) "toNat", size := 2 ^ 64 }, { nbits := System.Platform.numBits, id := `USize, ofNatFn := `USize.ofNat, toNatFn := `USize.toNat, size := 2 ^ System.Platform.numBits }]
Equations
- Lean.Compiler.isOfNat fn = List.any Lean.Compiler.numScalarTypes fun info => info.ofNatFn == fn
Equations
- Lean.Compiler.isToNat fn = List.any Lean.Compiler.numScalarTypes fun info => info.toNatFn == fn
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
Equations
- Lean.Compiler.getInfoFromVal x = match x with | Lean.Expr.app (Lean.Expr.const fn x x_1) x_2 x_3 => Lean.Compiler.getInfoFromFn fn Lean.Compiler.numScalarTypes | x => none
Equations
- Lean.Compiler.mkUIntLit info n = Lean.mkApp (Lean.mkConst info.ofNatFn) (Lean.mkRawNatLit (n % info.size))
Equations
- Lean.Compiler.mkUInt32Lit n = Lean.Compiler.mkUIntLit { nbits := 32, id := Lean.Compiler.mkUIntTypeName 32, ofNatFn := Lean.Name.mkStr (Lean.Compiler.mkUIntTypeName 32) "ofNat", toNatFn := Lean.Name.mkStr (Lean.Compiler.mkUIntTypeName 32) "toNat", size := 2 ^ 32 } n
def
Lean.Compiler.foldBinUInt
(fn : Lean.Compiler.NumScalarTypeInfo → Bool → Nat → Nat → Nat)
(beforeErasure : Bool)
(a₁ : Lean.Expr)
(a₂ : Lean.Expr)
:
Equations
- Lean.Compiler.foldBinUInt fn beforeErasure a₁ a₂ = OptionM.run do let n₁ ← Lean.Compiler.getNumLit a₁ let n₂ ← Lean.Compiler.getNumLit a₂ let info ← Lean.Compiler.getInfoFromVal a₁ pure (Lean.Compiler.mkUIntLit info (fn info beforeErasure n₁ n₂))
Equations
- Lean.Compiler.foldUIntAdd = Lean.Compiler.foldBinUInt fun x x => Add.add
Equations
- Lean.Compiler.foldUIntMul = Lean.Compiler.foldBinUInt fun x x => Mul.mul
Equations
- Lean.Compiler.foldUIntDiv = Lean.Compiler.foldBinUInt fun x x => Div.div
Equations
- Lean.Compiler.foldUIntMod = Lean.Compiler.foldBinUInt fun x x => Mod.mod
Equations
- Lean.Compiler.foldUIntSub = Lean.Compiler.foldBinUInt fun info x a b => a + (info.size - b)
Equations
- Lean.Compiler.preUIntBinFoldFns = [(`add, Lean.Compiler.foldUIntAdd), (`mul, Lean.Compiler.foldUIntMul), (`div, Lean.Compiler.foldUIntDiv), (`mod, Lean.Compiler.foldUIntMod), (`sub, Lean.Compiler.foldUIntSub)]
Equations
- Lean.Compiler.uintBinFoldFns = List.foldl (fun r info => r ++ List.map (fun x => match x with | (suffix, fn) => (info.id ++ suffix, fn)) Lean.Compiler.preUIntBinFoldFns) [] Lean.Compiler.numScalarTypes
Equations
- Lean.Compiler.foldNatBinOp fn a₁ a₂ = OptionM.run do let n₁ ← Lean.Compiler.getNumLit a₁ let n₂ ← Lean.Compiler.getNumLit a₂ pure (Lean.mkRawNatLit (fn n₁ n₂))
Equations
Equations
Equations
Equations
Equations
- Lean.Compiler.foldNatPow x a₁ a₂ = OptionM.run do let n₁ ← Lean.Compiler.getNumLit a₁ let n₂ ← Lean.Compiler.getNumLit a₂ if n₂ < Lean.Compiler.natPowThreshold then pure (Lean.mkRawNatLit (n₁ ^ n₂)) else failure
Equations
- Lean.Compiler.mkNatEq a b = Lean.mkAppN (Lean.mkConst `Eq [Lean.levelOne]) #[Lean.mkConst `Nat, a, b]
Equations
- Lean.Compiler.mkNatLt a b = Lean.mkAppN (Lean.mkConst `LT.lt [Lean.levelZero]) #[Lean.mkConst `Nat, Lean.mkConst `Nat.lt, a, b]
Equations
- Lean.Compiler.mkNatLe a b = Lean.mkAppN (Lean.mkConst `LE.le [Lean.levelZero]) #[Lean.mkConst `Nat, Lean.mkConst `Nat.le, a, b]
Equations
- Lean.Compiler.toDecidableExpr beforeErasure pred r = match beforeErasure, r with | false, true => Lean.mkConst `Bool.true | false, false => Lean.mkConst `Bool.false | true, true => Lean.mkDecIsTrue pred (Lean.Compiler.mkLcProof pred) | true, 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)
:
Equations
- Lean.Compiler.foldNatBinPred mkPred fn beforeErasure a₁ a₂ = OptionM.run do let n₁ ← Lean.Compiler.getNumLit a₁ let n₂ ← Lean.Compiler.getNumLit a₂ pure (Lean.Compiler.toDecidableExpr beforeErasure (mkPred a₁ a₂) (fn n₁ n₂))
Equations
- Lean.Compiler.foldNatDecEq = Lean.Compiler.foldNatBinPred Lean.Compiler.mkNatEq fun a b => decide (a = b)
Equations
- Lean.Compiler.foldNatDecLt = Lean.Compiler.foldNatBinPred Lean.Compiler.mkNatLt fun a b => decide (a < b)
Equations
- Lean.Compiler.foldNatDecLe = Lean.Compiler.foldNatBinPred Lean.Compiler.mkNatLe fun a b => decide (a ≤ b)
Equations
- Lean.Compiler.natFoldFns = [(`Nat.add, Lean.Compiler.foldNatAdd), (`Nat.mul, Lean.Compiler.foldNatMul), (`Nat.div, Lean.Compiler.foldNatDiv), (`Nat.mod, Lean.Compiler.foldNatMod), (`Nat.pow, Lean.Compiler.foldNatPow), (`Nat.decEq, Lean.Compiler.foldNatDecEq), (`Nat.decLt, Lean.Compiler.foldNatDecLt), (`Nat.decLe, Lean.Compiler.foldNatDecLe)]
Equations
- Lean.Compiler.getBoolLit x = match x with | Lean.Expr.const (Lean.Name.str (Lean.Name.str Lean.Name.anonymous "Bool" x_2) "true" x_3) x x_1 => some true | Lean.Expr.const (Lean.Name.str (Lean.Name.str Lean.Name.anonymous "Bool" x_2) "false" x_3) x x_1 => some false | x => none
Equations
- Lean.Compiler.foldStrictAnd x a₁ a₂ = let v₁ := Lean.Compiler.getBoolLit a₁; let v₂ := Lean.Compiler.getBoolLit a₂; match v₁, v₂ with | some true, x => some a₂ | some false, x => some a₁ | x, some true => some a₁ | x, some false => some a₂ | x, x_1 => none
Equations
- Lean.Compiler.foldStrictOr x a₁ a₂ = let v₁ := Lean.Compiler.getBoolLit a₁; let v₂ := Lean.Compiler.getBoolLit a₂; match v₁, v₂ with | some true, x => some a₁ | some false, x => some a₂ | x, some true => some a₂ | x, some false => some a₁ | x, x_1 => none
Equations
- Lean.Compiler.boolFoldFns = [(`strictOr, Lean.Compiler.foldStrictOr), (`strictAnd, Lean.Compiler.foldStrictAnd)]
Equations
- Lean.Compiler.foldNatSucc x a = OptionM.run do let n ← Lean.Compiler.getNumLit a pure (Lean.mkRawNatLit (n + 1))
Equations
- Lean.Compiler.foldCharOfNat beforeErasure a = OptionM.run do guard ((!beforeErasure) = true) let n ← Lean.Compiler.getNumLit a if isValidChar (Nat.toUInt32 n) then pure (Lean.Compiler.mkUInt32Lit n) else pure (Lean.Compiler.mkUInt32Lit 0)
Equations
- Lean.Compiler.foldToNat x a = OptionM.run do let n ← Lean.Compiler.getNumLit a pure (Lean.mkRawNatLit n)
Equations
- Lean.Compiler.uintFoldToNatFns = List.foldl (fun r info => (info.toNatFn, Lean.Compiler.foldToNat) :: r) [] Lean.Compiler.numScalarTypes
Equations
- Lean.Compiler.unFoldFns = [(`Nat.succ, Lean.Compiler.foldNatSucc), (`Char.ofNat, Lean.Compiler.foldCharOfNat)] ++ Lean.Compiler.uintFoldToNatFns
Equations
Equations
def
Lean.Compiler.foldBinOp
(beforeErasure : Bool)
(f : Lean.Expr)
(a : Lean.Expr)
(b : Lean.Expr)
:
Equations
- Lean.Compiler.foldBinOp beforeErasure f a b = OptionM.run (match f with | Lean.Expr.const fn x x_1 => do let foldFn ← Lean.Compiler.findBinFoldFn fn foldFn beforeErasure a b | x => failure)
Equations
- Lean.Compiler.foldUnOp beforeErasure f a = OptionM.run (match f with | Lean.Expr.const fn x x_1 => do let foldFn ← Lean.Compiler.findUnFoldFn fn foldFn beforeErasure a | x => failure)