From 8b18c0da053e069b5a2d9fbf06f45eae2f05a029 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 7 Sep 2023 15:28:06 +0200 Subject: Map some globals like u32::MAX to standard definitions --- backends/lean/Base/Primitives/Scalar.lean | 42 +++++++++++++++++++++++++++++++ 1 file changed, 42 insertions(+) (limited to 'backends/lean/Base/Primitives/Scalar.lean') diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean index ffc969f3..fa5a63cd 100644 --- a/backends/lean/Base/Primitives/Scalar.lean +++ b/backends/lean/Base/Primitives/Scalar.lean @@ -230,6 +230,20 @@ def Scalar.cMax (ty : ScalarTy) : Int := | .Usize => Scalar.max .U32 | _ => Scalar.max ty +theorem Scalar.min_lt_max (ty : ScalarTy) : Scalar.min ty < Scalar.max ty := by + cases ty <;> simp [Scalar.min, Scalar.max] + . simp [Isize.min, Isize.max] + have h1 := Isize.refined_min.property + have h2 := Isize.refined_max.property + cases h1 <;> cases h2 <;> simp [*] + . simp [Usize.max] + have h := Usize.refined_max.property + cases h <;> simp [*] + +theorem Scalar.min_le_max (ty : ScalarTy) : Scalar.min ty ≤ Scalar.max ty := by + have := Scalar.min_lt_max ty + int_tac + theorem Scalar.cMin_bound ty : Scalar.min ty ≤ Scalar.cMin ty := by cases ty <;> simp [Scalar.min, Scalar.max, Scalar.cMin, Scalar.cMax] at * have h := Isize.refined_min.property @@ -395,6 +409,34 @@ def Scalar.cast {src_ty : ScalarTy} (tgt_ty : ScalarTy) (x : Scalar src_ty) : Re @[reducible] def U64 := Scalar .U64 @[reducible] def U128 := Scalar .U128 +-- TODO: reducible? +@[reducible] def isize_min : Isize := Scalar.ofInt Isize.min (by simp [Scalar.min, Scalar.max]; apply (Scalar.min_le_max .Isize)) +@[reducible] def isize_max : Isize := Scalar.ofInt Isize.max (by simp [Scalar.min, Scalar.max]; apply (Scalar.min_le_max .Isize)) +@[reducible] def i8_min : I8 := Scalar.ofInt I8.min +@[reducible] def i8_max : I8 := Scalar.ofInt I8.max +@[reducible] def i16_min : I16 := Scalar.ofInt I16.min +@[reducible] def i16_max : I16 := Scalar.ofInt I16.max +@[reducible] def i32_min : I32 := Scalar.ofInt I32.min +@[reducible] def i32_max : I32 := Scalar.ofInt I32.max +@[reducible] def i64_min : I64 := Scalar.ofInt I64.min +@[reducible] def i64_max : I64 := Scalar.ofInt I64.max +@[reducible] def i128_min : I128 := Scalar.ofInt I128.min +@[reducible] def i128_max : I128 := Scalar.ofInt I128.max + +-- TODO: reducible? +@[reducible] def usize_min : Usize := Scalar.ofInt Usize.min +@[reducible] def usize_max : Usize := Scalar.ofInt Usize.max (by simp [Scalar.min, Scalar.max]; apply (Scalar.min_le_max .Usize)) +@[reducible] def u8_min : U8 := Scalar.ofInt U8.min +@[reducible] def u8_max : U8 := Scalar.ofInt U8.max +@[reducible] def u16_min : U16 := Scalar.ofInt U16.min +@[reducible] def u16_max : U16 := Scalar.ofInt U16.max +@[reducible] def u32_min : U32 := Scalar.ofInt U32.min +@[reducible] def u32_max : U32 := Scalar.ofInt U32.max +@[reducible] def u64_min : U64 := Scalar.ofInt U64.min +@[reducible] def u64_max : U64 := Scalar.ofInt U64.max +@[reducible] def u128_min : U128 := Scalar.ofInt U128.min +@[reducible] def u128_max : U128 := Scalar.ofInt U128.max + -- TODO: below: not sure this is the best way. -- Should we rather overload operations like +, -, etc.? -- Also, it is possible to automate the generation of those definitions -- cgit v1.2.3 From 1181aecddbcb3232c21b191fbde59c2e9596846a Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 7 Sep 2023 16:02:43 +0200 Subject: Fix some issues --- backends/lean/Base/Primitives/Scalar.lean | 48 +++++++++++++++---------------- 1 file changed, 24 insertions(+), 24 deletions(-) (limited to 'backends/lean/Base/Primitives/Scalar.lean') diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean index fa5a63cd..6e7733a7 100644 --- a/backends/lean/Base/Primitives/Scalar.lean +++ b/backends/lean/Base/Primitives/Scalar.lean @@ -410,32 +410,32 @@ def Scalar.cast {src_ty : ScalarTy} (tgt_ty : ScalarTy) (x : Scalar src_ty) : Re @[reducible] def U128 := Scalar .U128 -- TODO: reducible? -@[reducible] def isize_min : Isize := Scalar.ofInt Isize.min (by simp [Scalar.min, Scalar.max]; apply (Scalar.min_le_max .Isize)) -@[reducible] def isize_max : Isize := Scalar.ofInt Isize.max (by simp [Scalar.min, Scalar.max]; apply (Scalar.min_le_max .Isize)) -@[reducible] def i8_min : I8 := Scalar.ofInt I8.min -@[reducible] def i8_max : I8 := Scalar.ofInt I8.max -@[reducible] def i16_min : I16 := Scalar.ofInt I16.min -@[reducible] def i16_max : I16 := Scalar.ofInt I16.max -@[reducible] def i32_min : I32 := Scalar.ofInt I32.min -@[reducible] def i32_max : I32 := Scalar.ofInt I32.max -@[reducible] def i64_min : I64 := Scalar.ofInt I64.min -@[reducible] def i64_max : I64 := Scalar.ofInt I64.max -@[reducible] def i128_min : I128 := Scalar.ofInt I128.min -@[reducible] def i128_max : I128 := Scalar.ofInt I128.max +@[reducible] def core_isize_min : Isize := Scalar.ofInt Isize.min (by simp [Scalar.min, Scalar.max]; apply (Scalar.min_le_max .Isize)) +@[reducible] def core_isize_max : Isize := Scalar.ofInt Isize.max (by simp [Scalar.min, Scalar.max]; apply (Scalar.min_le_max .Isize)) +@[reducible] def core_i8_min : I8 := Scalar.ofInt I8.min +@[reducible] def core_i8_max : I8 := Scalar.ofInt I8.max +@[reducible] def core_i16_min : I16 := Scalar.ofInt I16.min +@[reducible] def core_i16_max : I16 := Scalar.ofInt I16.max +@[reducible] def core_i32_min : I32 := Scalar.ofInt I32.min +@[reducible] def core_i32_max : I32 := Scalar.ofInt I32.max +@[reducible] def core_i64_min : I64 := Scalar.ofInt I64.min +@[reducible] def core_i64_max : I64 := Scalar.ofInt I64.max +@[reducible] def core_i128_min : I128 := Scalar.ofInt I128.min +@[reducible] def core_i128_max : I128 := Scalar.ofInt I128.max -- TODO: reducible? -@[reducible] def usize_min : Usize := Scalar.ofInt Usize.min -@[reducible] def usize_max : Usize := Scalar.ofInt Usize.max (by simp [Scalar.min, Scalar.max]; apply (Scalar.min_le_max .Usize)) -@[reducible] def u8_min : U8 := Scalar.ofInt U8.min -@[reducible] def u8_max : U8 := Scalar.ofInt U8.max -@[reducible] def u16_min : U16 := Scalar.ofInt U16.min -@[reducible] def u16_max : U16 := Scalar.ofInt U16.max -@[reducible] def u32_min : U32 := Scalar.ofInt U32.min -@[reducible] def u32_max : U32 := Scalar.ofInt U32.max -@[reducible] def u64_min : U64 := Scalar.ofInt U64.min -@[reducible] def u64_max : U64 := Scalar.ofInt U64.max -@[reducible] def u128_min : U128 := Scalar.ofInt U128.min -@[reducible] def u128_max : U128 := Scalar.ofInt U128.max +@[reducible] def core_usize_min : Usize := Scalar.ofInt Usize.min +@[reducible] def core_usize_max : Usize := Scalar.ofInt Usize.max (by simp [Scalar.min, Scalar.max]; apply (Scalar.min_le_max .Usize)) +@[reducible] def core_u8_min : U8 := Scalar.ofInt U8.min +@[reducible] def core_u8_max : U8 := Scalar.ofInt U8.max +@[reducible] def core_u16_min : U16 := Scalar.ofInt U16.min +@[reducible] def core_u16_max : U16 := Scalar.ofInt U16.max +@[reducible] def core_u32_min : U32 := Scalar.ofInt U32.min +@[reducible] def core_u32_max : U32 := Scalar.ofInt U32.max +@[reducible] def core_u64_min : U64 := Scalar.ofInt U64.min +@[reducible] def core_u64_max : U64 := Scalar.ofInt U64.max +@[reducible] def core_u128_min : U128 := Scalar.ofInt U128.min +@[reducible] def core_u128_max : U128 := Scalar.ofInt U128.max -- TODO: below: not sure this is the best way. -- Should we rather overload operations like +, -, etc.? -- cgit v1.2.3 From cbb2d05e0db6bedf9d6844f29ee25b95429b994c Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 16 Oct 2023 11:06:46 +0200 Subject: Improve formatting of scalars in Lean --- backends/lean/Base/Primitives/Scalar.lean | 15 +++++++++++++++ 1 file changed, 15 insertions(+) (limited to 'backends/lean/Base/Primitives/Scalar.lean') diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean index 6e7733a7..9e65d3c0 100644 --- a/backends/lean/Base/Primitives/Scalar.lean +++ b/backends/lean/Base/Primitives/Scalar.lean @@ -764,6 +764,21 @@ def U32.ofInt := @Scalar.ofInt .U32 def U64.ofInt := @Scalar.ofInt .U64 def U128.ofInt := @Scalar.ofInt .U128 +postfix:74 "%isize" => Isize.ofInt +postfix:74 "%i8" => I8.ofInt +postfix:74 "%i16" => I16.ofInt +postfix:74 "%i32" => I32.ofInt +postfix:74 "%i64" => I64.ofInt +postfix:74 "%i128" => I128.ofInt +postfix:74 "%usize" => Usize.ofInt +postfix:74 "%u8" => U8.ofInt +postfix:74 "%u16" => U16.ofInt +postfix:74 "%u32" => U32.ofInt +postfix:74 "%u64" => U64.ofInt +postfix:74 "%u128" => U128.ofInt + +example : Result U32 := 1%u32 + 2%u32 + -- TODO: factor those lemmas out @[simp] theorem Scalar.ofInt_val_eq {ty} (h : Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty) : (Scalar.ofInt x h).val = x := by simp [Scalar.ofInt, Scalar.ofIntCore] -- cgit v1.2.3