diff --git a/src/Init/Data/SInt/Basic.lean b/src/Init/Data/SInt/Basic.lean index 84189c7c77..7df1da3981 100644 --- a/src/Init/Data/SInt/Basic.lean +++ b/src/Init/Data/SInt/Basic.lean @@ -148,6 +148,9 @@ instance : ShiftLeft Int8 := ⟨Int8.shiftLeft⟩ instance : ShiftRight Int8 := ⟨Int8.shiftRight⟩ instance : DecidableEq Int8 := Int8.decEq +@[extern "lean_bool_to_int8"] +def Bool.toInt8 (b : Bool) : Int8 := if b then 1 else 0 + @[extern "lean_int8_dec_lt"] def Int8.decLt (a b : Int8) : Decidable (a < b) := inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec)) @@ -249,6 +252,9 @@ instance : ShiftLeft Int16 := ⟨Int16.shiftLeft⟩ instance : ShiftRight Int16 := ⟨Int16.shiftRight⟩ instance : DecidableEq Int16 := Int16.decEq +@[extern "lean_bool_to_int16"] +def Bool.toInt16 (b : Bool) : Int16 := if b then 1 else 0 + @[extern "lean_int16_dec_lt"] def Int16.decLt (a b : Int16) : Decidable (a < b) := inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec)) @@ -354,6 +360,9 @@ instance : ShiftLeft Int32 := ⟨Int32.shiftLeft⟩ instance : ShiftRight Int32 := ⟨Int32.shiftRight⟩ instance : DecidableEq Int32 := Int32.decEq +@[extern "lean_bool_to_int32"] +def Bool.toInt32 (b : Bool) : Int32 := if b then 1 else 0 + @[extern "lean_int32_dec_lt"] def Int32.decLt (a b : Int32) : Decidable (a < b) := inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec)) @@ -463,6 +472,9 @@ instance : ShiftLeft Int64 := ⟨Int64.shiftLeft⟩ instance : ShiftRight Int64 := ⟨Int64.shiftRight⟩ instance : DecidableEq Int64 := Int64.decEq +@[extern "lean_bool_to_int64"] +def Bool.toInt64 (b : Bool) : Int64 := if b then 1 else 0 + @[extern "lean_int64_dec_lt"] def Int64.decLt (a b : Int64) : Decidable (a < b) := inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec)) @@ -574,6 +586,9 @@ instance : ShiftLeft ISize := ⟨ISize.shiftLeft⟩ instance : ShiftRight ISize := ⟨ISize.shiftRight⟩ instance : DecidableEq ISize := ISize.decEq +@[extern "lean_bool_to_isize"] +def Bool.toISize (b : Bool) : ISize := if b then 1 else 0 + @[extern "lean_isize_dec_lt"] def ISize.decLt (a b : ISize) : Decidable (a < b) := inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec)) diff --git a/src/Init/Data/UInt/Basic.lean b/src/Init/Data/UInt/Basic.lean index f1f19f3fc0..263a9919ec 100644 --- a/src/Init/Data/UInt/Basic.lean +++ b/src/Init/Data/UInt/Basic.lean @@ -56,6 +56,9 @@ instance : Xor UInt8 := ⟨UInt8.xor⟩ instance : ShiftLeft UInt8 := ⟨UInt8.shiftLeft⟩ instance : ShiftRight UInt8 := ⟨UInt8.shiftRight⟩ +@[extern "lean_bool_to_uint8"] +def Bool.toUInt8 (b : Bool) : UInt8 := if b then 1 else 0 + @[extern "lean_uint8_dec_lt"] def UInt8.decLt (a b : UInt8) : Decidable (a < b) := inferInstanceAs (Decidable (a.toBitVec < b.toBitVec)) @@ -116,6 +119,9 @@ instance : Xor UInt16 := ⟨UInt16.xor⟩ instance : ShiftLeft UInt16 := ⟨UInt16.shiftLeft⟩ instance : ShiftRight UInt16 := ⟨UInt16.shiftRight⟩ +@[extern "lean_bool_to_uint16"] +def Bool.toUInt16 (b : Bool) : UInt16 := if b then 1 else 0 + set_option bootstrap.genMatcherCode false in @[extern "lean_uint16_dec_lt"] def UInt16.decLt (a b : UInt16) : Decidable (a < b) := @@ -174,6 +180,9 @@ instance : Xor UInt32 := ⟨UInt32.xor⟩ instance : ShiftLeft UInt32 := ⟨UInt32.shiftLeft⟩ instance : ShiftRight UInt32 := ⟨UInt32.shiftRight⟩ +@[extern "lean_bool_to_uint32"] +def Bool.toUInt32 (b : Bool) : UInt32 := if b then 1 else 0 + @[extern "lean_uint64_add"] def UInt64.add (a b : UInt64) : UInt64 := ⟨a.toBitVec + b.toBitVec⟩ @[extern "lean_uint64_sub"] @@ -278,5 +287,8 @@ instance : Xor USize := ⟨USize.xor⟩ instance : ShiftLeft USize := ⟨USize.shiftLeft⟩ instance : ShiftRight USize := ⟨USize.shiftRight⟩ +@[extern "lean_bool_to_usize"] +def Bool.toUSize (b : Bool) : USize := if b then 1 else 0 + instance : Max USize := maxOfLe instance : Min USize := minOfLe diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h index 652ba744ac..5ac680164c 100644 --- a/src/include/lean/lean.h +++ b/src/include/lean/lean.h @@ -1617,7 +1617,16 @@ static inline uint8_t lean_int_dec_nonneg(b_lean_obj_arg a) { /* Bool */ -static inline uint64_t lean_bool_to_uint64(uint8_t a) { return ((uint64_t)a); } +static inline uint8_t lean_bool_to_uint8(uint8_t a) { return a; } +static inline uint16_t lean_bool_to_uint16(uint8_t a) { return (uint16_t)a; } +static inline uint32_t lean_bool_to_uint32(uint8_t a) { return (uint32_t)a; } +static inline uint64_t lean_bool_to_uint64(uint8_t a) { return (uint64_t)a; } +static inline size_t lean_bool_to_usize(uint8_t a) { return (size_t)a; } +static inline uint8_t lean_bool_to_int8(uint8_t a) { return (uint8_t)(int8_t)a; } +static inline uint16_t lean_bool_to_int16(uint8_t a) { return (uint16_t)(int16_t)a; } +static inline uint32_t lean_bool_to_int32(uint8_t a) { return (uint32_t)(int32_t)a; } +static inline uint64_t lean_bool_to_int64(uint8_t a) { return (uint64_t)(int64_t)a; } +static inline size_t lean_bool_to_isize(uint8_t a) { return (size_t)(ptrdiff_t)a; } /* UInt8 */ diff --git a/tests/lean/bool2int.lean b/tests/lean/bool2int.lean new file mode 100644 index 0000000000..64aee5583f --- /dev/null +++ b/tests/lean/bool2int.lean @@ -0,0 +1,20 @@ +#eval Bool.toUInt8 false = 0 +#eval Bool.toUInt8 true = 1 +#eval Bool.toUInt16 false = 0 +#eval Bool.toUInt16 true = 1 +#eval Bool.toUInt32 false = 0 +#eval Bool.toUInt32 true = 1 +#eval Bool.toUInt64 false = 0 +#eval Bool.toUInt64 true = 1 +#eval Bool.toUSize false = 0 +#eval Bool.toUSize true = 1 +#eval Bool.toInt8 false = 0 +#eval Bool.toInt8 true = 1 +#eval Bool.toInt16 false = 0 +#eval Bool.toInt16 true = 1 +#eval Bool.toInt32 false = 0 +#eval Bool.toInt32 true = 1 +#eval Bool.toInt64 false = 0 +#eval Bool.toInt64 true = 1 +#eval Bool.toISize false = 0 +#eval Bool.toISize true = 1 diff --git a/tests/lean/bool2int.lean.expected.out b/tests/lean/bool2int.lean.expected.out new file mode 100644 index 0000000000..9a531b2b13 --- /dev/null +++ b/tests/lean/bool2int.lean.expected.out @@ -0,0 +1,20 @@ +true +true +true +true +true +true +true +true +true +true +true +true +true +true +true +true +true +true +true +true