summaryrefslogtreecommitdiff
path: root/backends/hol4
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--backends/hol4/primitivesScript.sml26
-rw-r--r--backends/hol4/primitivesTheory.sig120
2 files changed, 146 insertions, 0 deletions
diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml
index 82da4de9..916988be 100644
--- a/backends/hol4/primitivesScript.sml
+++ b/backends/hol4/primitivesScript.sml
@@ -555,6 +555,32 @@ Proof
QED
val _ = evalLib.add_unfold_thm "mk_isize_unfold"
+(** Constants *)
+val core_i8_min_def = Define ‘core_i8_min = int_to_i8 i8_min’
+val core_i8_max_def = Define ‘core_i8_max = int_to_i8 i8_max’
+val core_i16_min_def = Define ‘core_i16_min = int_to_i16 i16_min’
+val core_i16_max_def = Define ‘core_i16_max = int_to_i16 i16_max’
+val core_i32_min_def = Define ‘core_i32_min = int_to_i32 i32_min’
+val core_i32_max_def = Define ‘core_i32_max = int_to_i32 i32_max’
+val core_i64_min_def = Define ‘core_i64_min = int_to_i64 i64_min’
+val core_i64_max_def = Define ‘core_i64_max = int_to_i64 i64_max’
+val core_i128_min_def = Define ‘core_i128_min = int_to_i128 i128_min’
+val core_i128_max_def = Define ‘core_i128_max = int_to_i128 i128_max’
+val core_isize_min_def = Define ‘core_isize_min = int_to_isize isize_min’
+val core_isize_max_def = Define ‘core_isize_max = int_to_isize isize_max’
+val core_u8_min_def = Define ‘core_u8_min = int_to_u8 0’
+val core_u8_max_def = Define ‘core_u8_max = int_to_u8 u8_max’
+val core_u16_min_def = Define ‘core_u16_min = int_to_u16 0’
+val core_u16_max_def = Define ‘core_u16_max = int_to_u16 u16_max’
+val core_u32_min_def = Define ‘core_u32_min = int_to_u32 0’
+val core_u32_max_def = Define ‘core_u32_max = int_to_u32 u32_max’
+val core_u64_min_def = Define ‘core_u64_min = int_to_u64 0’
+val core_u64_max_def = Define ‘core_u64_max = int_to_u64 u64_max’
+val core_u128_min_def = Define ‘core_u128_min = int_to_u128 0’
+val core_u128_max_def = Define ‘core_u128_max = int_to_u128 u128_max’
+val core_usize_min_def = Define ‘core_usize_min = int_to_usize 0’
+val core_usize_max_def = Define ‘core_usize_max = int_to_usize usize_max’
+
val isize_neg_def = Define ‘isize_neg x = mk_isize (- (isize_to_int x))’
val i8_neg_def = Define ‘i8_neg x = mk_i8 (- (i8_to_int x))’
val i16_neg_def = Define ‘i16_neg x = mk_i16 (- (i16_to_int x))’
diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig
index 6660b02d..4ae6bb3e 100644
--- a/backends/hol4/primitivesTheory.sig
+++ b/backends/hol4/primitivesTheory.sig
@@ -46,6 +46,30 @@ sig
(* Definitions *)
val bind_def : thm
+ val core_i128_max_def : thm
+ val core_i128_min_def : thm
+ val core_i16_max_def : thm
+ val core_i16_min_def : thm
+ val core_i32_max_def : thm
+ val core_i32_min_def : thm
+ val core_i64_max_def : thm
+ val core_i64_min_def : thm
+ val core_i8_max_def : thm
+ val core_i8_min_def : thm
+ val core_isize_max_def : thm
+ val core_isize_min_def : thm
+ val core_u128_max_def : thm
+ val core_u128_min_def : thm
+ val core_u16_max_def : thm
+ val core_u16_min_def : thm
+ val core_u32_max_def : thm
+ val core_u32_min_def : thm
+ val core_u64_max_def : thm
+ val core_u64_min_def : thm
+ val core_u8_max_def : thm
+ val core_u8_min_def : thm
+ val core_usize_max_def : thm
+ val core_usize_min_def : thm
val error_BIJ : thm
val error_CASE : thm
val error_TY_DEF : thm
@@ -566,6 +590,102 @@ sig
monad_bind x f =
case x of Return y => f y | Fail e => Fail e | Diverge => Diverge
+ [core_i128_max_def] Definition
+
+ ⊢ core_i128_max = int_to_i128 i128_max
+
+ [core_i128_min_def] Definition
+
+ ⊢ core_i128_min = int_to_i128 i128_min
+
+ [core_i16_max_def] Definition
+
+ ⊢ core_i16_max = int_to_i16 i16_max
+
+ [core_i16_min_def] Definition
+
+ ⊢ core_i16_min = int_to_i16 i16_min
+
+ [core_i32_max_def] Definition
+
+ ⊢ core_i32_max = int_to_i32 i32_max
+
+ [core_i32_min_def] Definition
+
+ ⊢ core_i32_min = int_to_i32 i32_min
+
+ [core_i64_max_def] Definition
+
+ ⊢ core_i64_max = int_to_i64 i64_max
+
+ [core_i64_min_def] Definition
+
+ ⊢ core_i64_min = int_to_i64 i64_min
+
+ [core_i8_max_def] Definition
+
+ ⊢ core_i8_max = int_to_i8 i8_max
+
+ [core_i8_min_def] Definition
+
+ ⊢ core_i8_min = int_to_i8 i8_min
+
+ [core_isize_max_def] Definition
+
+ ⊢ core_isize_max = int_to_isize isize_max
+
+ [core_isize_min_def] Definition
+
+ ⊢ core_isize_min = int_to_isize isize_min
+
+ [core_u128_max_def] Definition
+
+ ⊢ core_u128_max = int_to_u128 u128_max
+
+ [core_u128_min_def] Definition
+
+ ⊢ core_u128_min = int_to_u128 0
+
+ [core_u16_max_def] Definition
+
+ ⊢ core_u16_max = int_to_u16 u16_max
+
+ [core_u16_min_def] Definition
+
+ ⊢ core_u16_min = int_to_u16 0
+
+ [core_u32_max_def] Definition
+
+ ⊢ core_u32_max = int_to_u32 u32_max
+
+ [core_u32_min_def] Definition
+
+ ⊢ core_u32_min = int_to_u32 0
+
+ [core_u64_max_def] Definition
+
+ ⊢ core_u64_max = int_to_u64 u64_max
+
+ [core_u64_min_def] Definition
+
+ ⊢ core_u64_min = int_to_u64 0
+
+ [core_u8_max_def] Definition
+
+ ⊢ core_u8_max = int_to_u8 u8_max
+
+ [core_u8_min_def] Definition
+
+ ⊢ core_u8_min = int_to_u8 0
+
+ [core_usize_max_def] Definition
+
+ ⊢ core_usize_max = int_to_usize usize_max
+
+ [core_usize_min_def] Definition
+
+ ⊢ core_usize_min = int_to_usize 0
+
[error_BIJ] Definition
⊢ (∀a. num2error (error2num a) = a) ∧