Merge pull request #44 from AeneasVerif/son_traits_types

Add support for traits

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) ∧