Map some globals like u32::MAX to standard definitions

1 files changed, 42 insertions, 0 deletions

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