Cleanup a bit the HOL4 backend and implement eval_conv

1 files changed, 104 insertions, 0 deletions

diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig
index 3b029c05..3e82565c 100644
--- a/backends/hol4/primitivesTheory.sig
+++ b/backends/hol4/primitivesTheory.sig
@@ -225,30 +225,35 @@ sig
     val i128_neg_eq : thm
     val i128_rem_eq : thm
     val i128_sub_eq : thm
+    val i128_to_int_int_to_i128_unfold : thm
     val i16_add_eq : thm
     val i16_div_eq : thm
     val i16_mul_eq : thm
     val i16_neg_eq : thm
     val i16_rem_eq : thm
     val i16_sub_eq : thm
+    val i16_to_int_int_to_i16_unfold : thm
     val i32_add_eq : thm
     val i32_div_eq : thm
     val i32_mul_eq : thm
     val i32_neg_eq : thm
     val i32_rem_eq : thm
     val i32_sub_eq : thm
+    val i32_to_int_int_to_i32_unfold : thm
     val i64_add_eq : thm
     val i64_div_eq : thm
     val i64_mul_eq : thm
     val i64_neg_eq : thm
     val i64_rem_eq : thm
     val i64_sub_eq : thm
+    val i64_to_int_int_to_i64_unfold : thm
     val i8_add_eq : thm
     val i8_div_eq : thm
     val i8_mul_eq : thm
     val i8_neg_eq : thm
     val i8_rem_eq : thm
     val i8_sub_eq : thm
+    val i8_to_int_int_to_i8_unfold : thm
     val index_update_diff : thm
     val index_update_same : thm
     val isize_add_eq : thm
@@ -257,6 +262,7 @@ sig
     val isize_neg_eq : thm
     val isize_rem_eq : thm
     val isize_sub_eq : thm
+    val isize_to_int_int_to_isize_unfold : thm
     val num2error_11 : thm
     val num2error_ONTO : thm
     val num2error_error2num : thm
@@ -273,26 +279,31 @@ sig
     val u128_mul_eq : thm
     val u128_rem_eq : thm
     val u128_sub_eq : thm
+    val u128_to_int_int_to_u128_unfold : thm
     val u16_add_eq : thm
     val u16_div_eq : thm
     val u16_mul_eq : thm
     val u16_rem_eq : thm
     val u16_sub_eq : thm
+    val u16_to_int_int_to_u16_unfold : thm
     val u32_add_eq : thm
     val u32_div_eq : thm
     val u32_mul_eq : thm
     val u32_rem_eq : thm
     val u32_sub_eq : thm
+    val u32_to_int_int_to_u32_unfold : thm
     val u64_add_eq : thm
     val u64_div_eq : thm
     val u64_mul_eq : thm
     val u64_rem_eq : thm
     val u64_sub_eq : thm
+    val u64_to_int_int_to_u64_unfold : thm
     val u8_add_eq : thm
     val u8_div_eq : thm
     val u8_mul_eq : thm
     val u8_rem_eq : thm
     val u8_sub_eq : thm
+    val u8_to_int_int_to_u8_unfold : thm
     val update_len : thm
     val update_spec : thm
     val usize_add_eq : thm
@@ -300,6 +311,7 @@ sig
     val usize_mul_eq : thm
     val usize_rem_eq : thm
     val usize_sub_eq : thm
+    val usize_to_int_int_to_usize_unfold : thm
     val vec_insert_back_spec : thm
     val vec_len_spec : thm
     val vec_to_list_int_bounds : thm
@@ -308,6 +320,8 @@ sig
 (*
    [ilist] Parent theory of "primitives"
    
+   [string] Parent theory of "primitives"
+   
    [isize_bounds]  Axiom
       
       [oracles: ] [axioms: isize_bounds] []
@@ -1390,6 +1404,14 @@ sig
           ∃z. i128_sub x y = Return z ∧
               i128_to_int z = i128_to_int x − i128_to_int y
    
+   [i128_to_int_int_to_i128_unfold]  Theorem
+      
+      [oracles: DISK_THM]
+      [axioms: usize_bounds, i128_to_int_int_to_i128, isize_bounds] []
+      ⊢ ∀n. i128_to_int (int_to_i128 n) =
+            if i128_min ≤ n ∧ n ≤ i128_max then n
+            else i128_to_int (int_to_i128 n)
+   
    [i16_add_eq]  Theorem
       
       [oracles: DISK_THM]
@@ -1451,6 +1473,14 @@ sig
           ∃z. i16_sub x y = Return z ∧
               i16_to_int z = i16_to_int x − i16_to_int y
    
+   [i16_to_int_int_to_i16_unfold]  Theorem
+      
+      [oracles: DISK_THM]
+      [axioms: usize_bounds, i16_to_int_int_to_i16, isize_bounds] []
+      ⊢ ∀n. i16_to_int (int_to_i16 n) =
+            if i16_min ≤ n ∧ n ≤ i16_max then n
+            else i16_to_int (int_to_i16 n)
+   
    [i32_add_eq]  Theorem
       
       [oracles: DISK_THM]
@@ -1512,6 +1542,14 @@ sig
           ∃z. i32_sub x y = Return z ∧
               i32_to_int z = i32_to_int x − i32_to_int y
    
+   [i32_to_int_int_to_i32_unfold]  Theorem
+      
+      [oracles: DISK_THM]
+      [axioms: usize_bounds, i32_to_int_int_to_i32, isize_bounds] []
+      ⊢ ∀n. i32_to_int (int_to_i32 n) =
+            if i32_min ≤ n ∧ n ≤ i32_max then n
+            else i32_to_int (int_to_i32 n)
+   
    [i64_add_eq]  Theorem
       
       [oracles: DISK_THM]
@@ -1573,6 +1611,14 @@ sig
           ∃z. i64_sub x y = Return z ∧
               i64_to_int z = i64_to_int x − i64_to_int y
    
+   [i64_to_int_int_to_i64_unfold]  Theorem
+      
+      [oracles: DISK_THM]
+      [axioms: usize_bounds, i64_to_int_int_to_i64, isize_bounds] []
+      ⊢ ∀n. i64_to_int (int_to_i64 n) =
+            if i64_min ≤ n ∧ n ≤ i64_max then n
+            else i64_to_int (int_to_i64 n)
+   
    [i8_add_eq]  Theorem
       
       [oracles: DISK_THM]
@@ -1634,6 +1680,13 @@ sig
           ∃z. i8_sub x y = Return z ∧
               i8_to_int z = i8_to_int x − i8_to_int y
    
+   [i8_to_int_int_to_i8_unfold]  Theorem
+      
+      [oracles: DISK_THM]
+      [axioms: usize_bounds, i8_to_int_int_to_i8, isize_bounds] []
+      ⊢ ∀n. i8_to_int (int_to_i8 n) =
+            if i8_min ≤ n ∧ n ≤ i8_max then n else i8_to_int (int_to_i8 n)
+   
    [index_update_diff]  Theorem
       
       ⊢ ∀ls i j y. 0 ≤ i ⇒ i < len ls ⇒ index i (update ls i y) = y
@@ -1723,6 +1776,14 @@ sig
           ∃z. isize_sub x y = Return z ∧
               isize_to_int z = isize_to_int x − isize_to_int y
    
+   [isize_to_int_int_to_isize_unfold]  Theorem
+      
+      [oracles: DISK_THM]
+      [axioms: usize_bounds, isize_to_int_int_to_isize, isize_bounds] []
+      ⊢ ∀n. isize_to_int (int_to_isize n) =
+            if i16_min ≤ n ∧ n ≤ i16_max then n
+            else isize_to_int (int_to_isize n)
+   
    [num2error_11]  Theorem
       
       ⊢ ∀r r'. r < 1 ⇒ r' < 1 ⇒ (num2error r = num2error r' ⇔ r = r')
@@ -1826,6 +1887,13 @@ sig
           ∃z. u128_sub x y = Return z ∧
               u128_to_int z = u128_to_int x − u128_to_int y
    
+   [u128_to_int_int_to_u128_unfold]  Theorem
+      
+      [oracles: DISK_THM]
+      [axioms: usize_bounds, u128_to_int_int_to_u128, isize_bounds] []
+      ⊢ ∀n. u128_to_int (int_to_u128 n) =
+            if 0 ≤ n ∧ n ≤ u128_max then n else u128_to_int (int_to_u128 n)
+   
    [u16_add_eq]  Theorem
       
       [oracles: DISK_THM]
@@ -1876,6 +1944,13 @@ sig
           ∃z. u16_sub x y = Return z ∧
               u16_to_int z = u16_to_int x − u16_to_int y
    
+   [u16_to_int_int_to_u16_unfold]  Theorem
+      
+      [oracles: DISK_THM]
+      [axioms: usize_bounds, u16_to_int_int_to_u16, isize_bounds] []
+      ⊢ ∀n. u16_to_int (int_to_u16 n) =
+            if 0 ≤ n ∧ n ≤ u16_max then n else u16_to_int (int_to_u16 n)
+   
    [u32_add_eq]  Theorem
       
       [oracles: DISK_THM]
@@ -1926,6 +2001,13 @@ sig
           ∃z. u32_sub x y = Return z ∧
               u32_to_int z = u32_to_int x − u32_to_int y
    
+   [u32_to_int_int_to_u32_unfold]  Theorem
+      
+      [oracles: DISK_THM]
+      [axioms: usize_bounds, u32_to_int_int_to_u32, isize_bounds] []
+      ⊢ ∀n. u32_to_int (int_to_u32 n) =
+            if 0 ≤ n ∧ n ≤ u32_max then n else u32_to_int (int_to_u32 n)
+   
    [u64_add_eq]  Theorem
       
       [oracles: DISK_THM]
@@ -1976,6 +2058,13 @@ sig
           ∃z. u64_sub x y = Return z ∧
               u64_to_int z = u64_to_int x − u64_to_int y
    
+   [u64_to_int_int_to_u64_unfold]  Theorem
+      
+      [oracles: DISK_THM]
+      [axioms: usize_bounds, u64_to_int_int_to_u64, isize_bounds] []
+      ⊢ ∀n. u64_to_int (int_to_u64 n) =
+            if 0 ≤ n ∧ n ≤ u64_max then n else u64_to_int (int_to_u64 n)
+   
    [u8_add_eq]  Theorem
       
       [oracles: DISK_THM]
@@ -2026,6 +2115,13 @@ sig
           ∃z. u8_sub x y = Return z ∧
               u8_to_int z = u8_to_int x − u8_to_int y
    
+   [u8_to_int_int_to_u8_unfold]  Theorem
+      
+      [oracles: DISK_THM]
+      [axioms: usize_bounds, u8_to_int_int_to_u8, isize_bounds] []
+      ⊢ ∀n. u8_to_int (int_to_u8 n) =
+            if 0 ≤ n ∧ n ≤ u8_max then n else u8_to_int (int_to_u8 n)
+   
    [update_len]  Theorem
       
       ⊢ ∀ls i y. len (update ls i y) = len ls
@@ -2090,6 +2186,14 @@ sig
           ∃z. usize_sub x y = Return z ∧
               usize_to_int z = usize_to_int x − usize_to_int y
    
+   [usize_to_int_int_to_usize_unfold]  Theorem
+      
+      [oracles: DISK_THM]
+      [axioms: usize_bounds, usize_to_int_int_to_usize, isize_bounds] []
+      ⊢ ∀n. usize_to_int (int_to_usize n) =
+            if 0 ≤ n ∧ n ≤ u16_max then n
+            else usize_to_int (int_to_usize n)
+   
    [vec_insert_back_spec]  Theorem
       
       [oracles: DISK_THM]