diff options
Diffstat (limited to 'backends/lean/Base/Primitives')
-rw-r--r-- | backends/lean/Base/Primitives/Alloc.lean | 2 | ||||
-rw-r--r-- | backends/lean/Base/Primitives/ArraySlice.lean | 2 | ||||
-rw-r--r-- | backends/lean/Base/Primitives/CoreConvertNum.lean | 263 | ||||
-rw-r--r-- | backends/lean/Base/Primitives/Scalar.lean | 239 |
4 files changed, 265 insertions, 241 deletions
diff --git a/backends/lean/Base/Primitives/Alloc.lean b/backends/lean/Base/Primitives/Alloc.lean index 15fe1ff9..1b15d36d 100644 --- a/backends/lean/Base/Primitives/Alloc.lean +++ b/backends/lean/Base/Primitives/Alloc.lean @@ -1,6 +1,6 @@ import Lean import Base.Primitives.Base -import Base.Primitives.CoreOps +import Base.Primitives.Core open Primitives open Result diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean index 91ca7284..157f9df1 100644 --- a/backends/lean/Base/Primitives/ArraySlice.lean +++ b/backends/lean/Base/Primitives/ArraySlice.lean @@ -6,7 +6,7 @@ import Mathlib.Tactic.Linarith import Base.IList import Base.Primitives.Scalar import Base.Primitives.Range -import Base.Primitives.CoreOps +import Base.Primitives.Core import Base.Arith import Base.Progress.Base diff --git a/backends/lean/Base/Primitives/CoreConvertNum.lean b/backends/lean/Base/Primitives/CoreConvertNum.lean new file mode 100644 index 00000000..d76fba37 --- /dev/null +++ b/backends/lean/Base/Primitives/CoreConvertNum.lean @@ -0,0 +1,263 @@ +import Lean +import Lean.Meta.Tactic.Simp +import Init.Data.List.Basic +import Mathlib.Tactic.Linarith +import Base.IList +import Base.Primitives.Scalar +import Base.Primitives.ArraySlice +import Base.Arith +import Base.Progress.Base + +namespace Primitives + +open Result Error + +namespace core.convert + +namespace num -- core.convert.num + +-- Conversions +def FromUsizeBool.from (b : Bool) : Usize := + if b then 1#usize else 0#usize + +def FromU8Bool.from (b : Bool) : U8 := + if b then 1#u8 else 0#u8 + +def FromU16Bool.from (b : Bool) : U16 := + if b then 1#u16 else 0#u16 + +def FromU32Bool.from (b : Bool) : U32 := + if b then 1#u32 else 0#u32 + +def FromU64Bool.from (b : Bool) : U64 := + if b then 1#u64 else 0#u64 + +def FromU128Bool.from (b : Bool) : U128 := + if b then 1#u128 else 0#u128 + +def FromIsizeBool.from (b : Bool) : Isize := + if b then 1#isize else 0#isize + +def FromI8Bool.from (b : Bool) : I8 := + if b then 1#i8 else 0#i8 + +def FromI16Bool.from (b : Bool) : I16 := + if b then 1#i16 else 0#i16 + +def FromI32Bool.from (b : Bool) : I32 := + if b then 1#i32 else 0#i32 + +def FromI64Bool.from (b : Bool) : I64 := + if b then 1#i64 else 0#i64 + +def FromI128Bool.from (b : Bool) : I128 := + if b then 1#i128 else 0#i128 + +def FromUsizeU8.from (x : U8) : Usize := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ + +def FromUsizeU16.from (x : U16) : Usize := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromUsizeU32.from (x : U32) : Usize := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromUsizeUsize.from (x : Usize) : Usize := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ + +def FromU8U8.from (x : U8) : U8 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ + +def FromU16U8.from (x : U8) : U16 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromU16U16.from (x : U16) : U16 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ + +def FromU32U8.from (x : U8) : U32 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromU32U16.from (x : U16) : U32 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromU32U32.from (x : U32) : U32 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ + +def FromU64U8.from (x : U8) : U64 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromU64U16.from (x : U16) : U64 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromU64U32.from (x : U32) : U64 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromU64U64.from (x : U64) : U64 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ + +def FromU128U8.from (x : U8) : U128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromU128U16.from (x : U16) : U128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromU128U32.from (x : U32) : U128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromU128U64.from (x : U64) : U128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromU128U128.from (x : U128) : U128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ + +def FromIsizeI8.from (x : I8) : Isize := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromIsizeI16.from (x : I16) : Isize := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromIsizeI32.from (x : I32) : Isize := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromIsizeIsize.from (x : Isize) : Isize := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ + +def FromI8I8.from (x : I8) : I8 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ + +def FromI16I8.from (x : I8) : I16 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromI16I16.from (x : I16) : I16 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ + +def FromI32I8.from (x : I8) : I32 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromI32I16.from (x : I16) : I32 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromI32I32.from (x : I32) : I32 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ + +def FromI64I8.from (x : I8) : I64 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromI64I16.from (x : I16) : I64 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromI64I32.from (x : I32) : I64 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromI64I64.from (x : I64) : I64 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ + +def FromI128I8.from (x : I8) : I128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromI128I16.from (x : I16) : I128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromI128I32.from (x : I32) : I128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromI128I64.from (x : I64) : I128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ +def FromI128I128.from (x : I128) : I128 := ⟨ x.val, by scalar_tac, by scalar_tac ⟩ + +end num -- core.convert.num + +def FromUsizeU8 : core.convert.From Usize U8 := { + from_ := fun x => ok (num.FromUsizeU8.from x) +} + +def FromUsizeU16 : core.convert.From Usize U16 := { + from_ := fun x => ok (num.FromUsizeU16.from x) +} + +def FromUsizeU32 : core.convert.From Usize U32 := { + from_ := fun x => ok (num.FromUsizeU32.from x) +} + +def FromUsizeUsize : core.convert.From Usize Usize := { + from_ := fun x => ok (num.FromUsizeUsize.from x) +} + +def FromU8U8 : core.convert.From U8 U8 := { + from_ := fun x => ok (num.FromU8U8.from x) +} + +def FromU16U8 : core.convert.From U16 U8 := { + from_ := fun x => ok (num.FromU16U8.from x) +} + +def FromU16U16 : core.convert.From U16 U16 := { + from_ := fun x => ok (num.FromU16U16.from x) +} + +def FromU32U8 : core.convert.From U32 U8 := { + from_ := fun x => ok (num.FromU32U8.from x) +} + +def FromU32U16 : core.convert.From U32 U16 := { + from_ := fun x => ok (num.FromU32U16.from x) +} + +def FromU32U32 : core.convert.From U32 U32 := { + from_ := fun x => ok (num.FromU32U32.from x) +} + +def FromU64U8 : core.convert.From U64 U8 := { + from_ := fun x => ok (num.FromU64U8.from x) +} + +def FromU64U16 : core.convert.From U64 U16 := { + from_ := fun x => ok (num.FromU64U16.from x) +} + +def FromU64U32 : core.convert.From U64 U32 := { + from_ := fun x => ok (num.FromU64U32.from x) +} + +def FromU64U64 : core.convert.From U64 U64 := { + from_ := fun x => ok (num.FromU64U64.from x) +} + +def FromU128U8 : core.convert.From U128 U8 := { + from_ := fun x => ok (num.FromU128U8.from x) +} + +def FromU128U16 : core.convert.From U128 U16 := { + from_ := fun x => ok (num.FromU128U16.from x) +} + +def FromU128U32 : core.convert.From U128 U32 := { + from_ := fun x => ok (num.FromU128U32.from x) +} + +def FromU128U64 : core.convert.From U128 U64 := { + from_ := fun x => ok (num.FromU128U64.from x) +} + +def FromU128U128 : core.convert.From U128 U128 := { + from_ := fun x => ok (num.FromU128U128.from x) +} + +def FromIsizeI8 : core.convert.From Isize I8 := { + from_ := fun x => ok (num.FromIsizeI8.from x) +} + +def FromIsizeI16 : core.convert.From Isize I16 := { + from_ := fun x => ok (num.FromIsizeI16.from x) +} + +def FromIsizeI32 : core.convert.From Isize I32 := { + from_ := fun x => ok (num.FromIsizeI32.from x) +} + +def FromIsizeIsize : core.convert.From Isize Isize := { + from_ := fun x => ok (num.FromIsizeIsize.from x) +} + +def FromI8I8 : core.convert.From I8 I8 := { + from_ := fun x => ok (num.FromI8I8.from x) +} + +def FromI16I8 : core.convert.From I16 I8 := { + from_ := fun x => ok (num.FromI16I8.from x) +} + +def FromI16I16 : core.convert.From I16 I16 := { + from_ := fun x => ok (num.FromI16I16.from x) +} + +def FromI32I8 : core.convert.From I32 I8 := { + from_ := fun x => ok (num.FromI32I8.from x) +} + +def FromI32I16 : core.convert.From I32 I16 := { + from_ := fun x => ok (num.FromI32I16.from x) +} + +def FromI32I32 : core.convert.From I32 I32 := { + from_ := fun x => ok (num.FromI32I32.from x) +} + +def FromI64I8 : core.convert.From I64 I8 := { + from_ := fun x => ok (num.FromI64I8.from x) +} + +def FromI64I16 : core.convert.From I64 I16 := { + from_ := fun x => ok (num.FromI64I16.from x) +} + +def FromI64I32 : core.convert.From I64 I32 := { + from_ := fun x => ok (num.FromI64I32.from x) +} + +def FromI64I64 : core.convert.From I64 I64 := { + from_ := fun x => ok (num.FromI64I64.from x) +} + +def FromI128I8 : core.convert.From I128 I8 := { + from_ := fun x => ok (num.FromI128I8.from x) +} + +def FromI128I16 : core.convert.From I128 I16 := { + from_ := fun x => ok (num.FromI128I16.from x) +} + +def FromI128I32 : core.convert.From I128 I32 := { + from_ := fun x => ok (num.FromI128I32.from x) +} + +def FromI128I64 : core.convert.From I128 I64 := { + from_ := fun x => ok (num.FromI128I64.from x) +} + +def FromI128I128 : core.convert.From I128 I128 := { + from_ := fun x => ok (num.FromI128I128.from x) +} + +end core.convert + +end Primitives diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean index 0ba538b7..9eb5a794 100644 --- a/backends/lean/Base/Primitives/Scalar.lean +++ b/backends/lean/Base/Primitives/Scalar.lean @@ -1394,245 +1394,6 @@ instance (ty : ScalarTy) : DecidableEq (Scalar ty) := @[simp] theorem Scalar.neq_to_neq_val {ty} : ∀ {i j : Scalar ty}, (¬ i = j) ↔ ¬ i.val = j.val := by simp [eq_equiv] --- Conversions -def core.convert.num.FromUsizeBool.from (b : Bool) : Usize := - if b then 1#usize else 0#usize - -def core.convert.num.FromU8Bool.from (b : Bool) : U8 := - if b then 1#u8 else 0#u8 - -def core.convert.num.FromU16Bool.from (b : Bool) : U16 := - if b then 1#u16 else 0#u16 - -def core.convert.num.FromU32Bool.from (b : Bool) : U32 := - if b then 1#u32 else 0#u32 - -def core.convert.num.FromU64Bool.from (b : Bool) : U64 := - if b then 1#u64 else 0#u64 - -def core.convert.num.FromU128Bool.from (b : Bool) : U128 := - if b then 1#u128 else 0#u128 - -def core.convert.num.FromIsizeBool.from (b : Bool) : Isize := - if b then 1#isize else 0#isize - -def core.convert.num.FromI8Bool.from (b : Bool) : I8 := - if b then 1#i8 else 0#i8 - -def core.convert.num.FromI16Bool.from (b : Bool) : I16 := - if b then 1#i16 else 0#i16 - -def core.convert.num.FromI32Bool.from (b : Bool) : I32 := - if b then 1#i32 else 0#i32 - -def core.convert.num.FromI64Bool.from (b : Bool) : I64 := - if b then 1#i64 else 0#i64 - -def core.convert.num.FromI128Bool.from (b : Bool) : I128 := - if b then 1#i128 else 0#i128 - -def core.convert.num.FromUsizeU8.from (x : U8) : Usize := sorry -def core.convert.num.FromUsizeU16.from (x : U16) : Usize := sorry -def core.convert.num.FromUsizeU32.from (x : U32) : Usize := sorry -def core.convert.num.FromUsizeUsize.from (x : Usize) : Usize := sorry - -def core.convert.num.FromU8U8.from (x : U8) : U8 := sorry - -def core.convert.num.FromU16U8.from (x : U8) : U16 := sorry -def core.convert.num.FromU16U16.from (x : U16) : U16 := sorry - -def core.convert.num.FromU32U8.from (x : U8) : U32 := sorry -def core.convert.num.FromU32U16.from (x : U16) : U32 := sorry -def core.convert.num.FromU32U32.from (x : U32) : U32 := sorry - -def core.convert.num.FromU64U8.from (x : U8) : U64 := sorry -def core.convert.num.FromU64U16.from (x : U16) : U64 := sorry -def core.convert.num.FromU64U32.from (x : U32) : U64 := sorry -def core.convert.num.FromU64U64.from (x : U64) : U64 := sorry - -def core.convert.num.FromU128U8.from (x : U8) : U128 := sorry -def core.convert.num.FromU128U16.from (x : U16) : U128 := sorry -def core.convert.num.FromU128U32.from (x : U32) : U128 := sorry -def core.convert.num.FromU128U64.from (x : U64) : U128 := sorry -def core.convert.num.FromU128U128.from (x : U128) : U128 := sorry - -def core.convert.num.FromIsizeI8.from (x : I8) : Isize := sorry -def core.convert.num.FromIsizeI16.from (x : I16) : Isize := sorry -def core.convert.num.FromIsizeI32.from (x : I32) : Isize := sorry -def core.convert.num.FromIsizeIsize.from (x : Isize) : Isize := sorry - -def core.convert.num.FromI8I8.from (x : I8) : I8 := sorry - -def core.convert.num.FromI16I8.from (x : I8) : I16 := sorry -def core.convert.num.FromI16I16.from (x : I16) : I16 := sorry - -def core.convert.num.FromI32I8.from (x : I8) : I32 := sorry -def core.convert.num.FromI32I16.from (x : I16) : I32 := sorry -def core.convert.num.FromI32I32.from (x : I32) : I32 := sorry - -def core.convert.num.FromI64I8.from (x : I8) : I64 := sorry -def core.convert.num.FromI64I16.from (x : I16) : I64 := sorry -def core.convert.num.FromI64I32.from (x : I32) : I64 := sorry -def core.convert.num.FromI64I64.from (x : I64) : I64 := sorry - -def core.convert.num.FromI128I8.from (x : I8) : I128 := sorry -def core.convert.num.FromI128I16.from (x : I16) : I128 := sorry -def core.convert.num.FromI128I32.from (x : I32) : I128 := sorry -def core.convert.num.FromI128I64.from (x : I64) : I128 := sorry -def core.convert.num.FromI128I128.from (x : I128) : I128 := sorry - -def core.convert.FromUsizeU8 : core.convert.From Usize U8 := { - from_ := fun x => ok (core.convert.num.FromUsizeU8.from x) -} - -def core.convert.FromUsizeU16 : core.convert.From Usize U16 := { - from_ := fun x => ok (core.convert.num.FromUsizeU16.from x) -} - -def core.convert.FromUsizeU32 : core.convert.From Usize U32 := { - from_ := fun x => ok (core.convert.num.FromUsizeU32.from x) -} - -def core.convert.FromUsizeUsize : core.convert.From Usize Usize := { - from_ := fun x => ok (core.convert.num.FromUsizeUsize.from x) -} - -def core.convert.FromU8U8 : core.convert.From U8 U8 := { - from_ := fun x => ok (core.convert.num.FromU8U8.from x) -} - -def core.convert.FromU16U8 : core.convert.From U16 U8 := { - from_ := fun x => ok (core.convert.num.FromU16U8.from x) -} - -def core.convert.FromU16U16 : core.convert.From U16 U16 := { - from_ := fun x => ok (core.convert.num.FromU16U16.from x) -} - -def core.convert.FromU32U8 : core.convert.From U32 U8 := { - from_ := fun x => ok (core.convert.num.FromU32U8.from x) -} - -def core.convert.FromU32U16 : core.convert.From U32 U16 := { - from_ := fun x => ok (core.convert.num.FromU32U16.from x) -} - -def core.convert.FromU32U32 : core.convert.From U32 U32 := { - from_ := fun x => ok (core.convert.num.FromU32U32.from x) -} - -def core.convert.FromU64U8 : core.convert.From U64 U8 := { - from_ := fun x => ok (core.convert.num.FromU64U8.from x) -} - -def core.convert.FromU64U16 : core.convert.From U64 U16 := { - from_ := fun x => ok (core.convert.num.FromU64U16.from x) -} - -def core.convert.FromU64U32 : core.convert.From U64 U32 := { - from_ := fun x => ok (core.convert.num.FromU64U32.from x) -} - -def core.convert.FromU64U64 : core.convert.From U64 U64 := { - from_ := fun x => ok (core.convert.num.FromU64U64.from x) -} - -def core.convert.FromU128U8 : core.convert.From U128 U8 := { - from_ := fun x => ok (core.convert.num.FromU128U8.from x) -} - -def core.convert.FromU128U16 : core.convert.From U128 U16 := { - from_ := fun x => ok (core.convert.num.FromU128U16.from x) -} - -def core.convert.FromU128U32 : core.convert.From U128 U32 := { - from_ := fun x => ok (core.convert.num.FromU128U32.from x) -} - -def core.convert.FromU128U64 : core.convert.From U128 U64 := { - from_ := fun x => ok (core.convert.num.FromU128U64.from x) -} - -def core.convert.FromU128U128 : core.convert.From U128 U128 := { - from_ := fun x => ok (core.convert.num.FromU128U128.from x) -} - -def core.convert.FromIsizeI8 : core.convert.From Isize I8 := { - from_ := fun x => ok (core.convert.num.FromIsizeI8.from x) -} - -def core.convert.FromIsizeI16 : core.convert.From Isize I16 := { - from_ := fun x => ok (core.convert.num.FromIsizeI16.from x) -} - -def core.convert.FromIsizeI32 : core.convert.From Isize I32 := { - from_ := fun x => ok (core.convert.num.FromIsizeI32.from x) -} - -def core.convert.FromIsizeIsize : core.convert.From Isize Isize := { - from_ := fun x => ok (core.convert.num.FromIsizeIsize.from x) -} - -def core.convert.FromI8I8 : core.convert.From I8 I8 := { - from_ := fun x => ok (core.convert.num.FromI8I8.from x) -} - -def core.convert.FromI16I8 : core.convert.From I16 I8 := { - from_ := fun x => ok (core.convert.num.FromI16I8.from x) -} - -def core.convert.FromI16I16 : core.convert.From I16 I16 := { - from_ := fun x => ok (core.convert.num.FromI16I16.from x) -} - -def core.convert.FromI32I8 : core.convert.From I32 I8 := { - from_ := fun x => ok (core.convert.num.FromI32I8.from x) -} - -def core.convert.FromI32I16 : core.convert.From I32 I16 := { - from_ := fun x => ok (core.convert.num.FromI32I16.from x) -} - -def core.convert.FromI32I32 : core.convert.From I32 I32 := { - from_ := fun x => ok (core.convert.num.FromI32I32.from x) -} - -def core.convert.FromI64I8 : core.convert.From I64 I8 := { - from_ := fun x => ok (core.convert.num.FromI64I8.from x) -} - -def core.convert.FromI64I16 : core.convert.From I64 I16 := { - from_ := fun x => ok (core.convert.num.FromI64I16.from x) -} - -def core.convert.FromI64I32 : core.convert.From I64 I32 := { - from_ := fun x => ok (core.convert.num.FromI64I32.from x) -} - -def core.convert.FromI64I64 : core.convert.From I64 I64 := { - from_ := fun x => ok (core.convert.num.FromI64I64.from x) -} - -def core.convert.FromI128I8 : core.convert.From I128 I8 := { - from_ := fun x => ok (core.convert.num.FromI128I8.from x) -} - -def core.convert.FromI128I16 : core.convert.From I128 I16 := { - from_ := fun x => ok (core.convert.num.FromI128I16.from x) -} - -def core.convert.FromI128I32 : core.convert.From I128 I32 := { - from_ := fun x => ok (core.convert.num.FromI128I32.from x) -} - -def core.convert.FromI128I64 : core.convert.From I128 I64 := { - from_ := fun x => ok (core.convert.num.FromI128I64.from x) -} - -def core.convert.FromI128I128 : core.convert.From I128 I128 := { - from_ := fun x => ok (core.convert.num.FromI128I128.from x) -} - -- Leading zeros def core.num.Usize.leading_zeros (x : Usize) : U32 := sorry def core.num.U8.leading_zeros (x : U8) : U32 := sorry |