Make 'a signed word have a different name than 'a word

Signed-off-by: Simon Winwood <simonjwinwood@gmail.com>

Author: Simon Winwood

tools/autocorres/TypHeapSimple.thy

@@ -807,7 +807,8 @@ lemmas simple_lift_simps =
   simple_lift_field_update_t
   c_guard_array_field
   nat_to_bin_string_simps
-
+  signed_or_unsigned
+  
 (* Old name for the above simpset. *)
 lemmas typ_simple_heap_simps = simple_lift_simps
 

tools/c-parser/UMM_Proofs.ML

@@ -545,8 +545,8 @@ fun umm_struct_calculation ((recname, flds), st, thy) = let
       Simplifier.asm_full_rewrite
           ((thy2ctxt thy) addsimps
                       [tag_def_thm, typtag_thm,
-                       @{thm "pad_typ_name_def"}, @{thm "insert_commute"},
-                       @{thm "nat_to_bin_string.simps"}])
+                       @{thm "pad_typ_name_def"}, @{thm "insert_commute"}] @ 
+                       @{thms "signed_or_unsigned"} @ @{thms "nat_to_bin_string.simps"})
           (Thm.cterm_of (thy2ctxt thy) (mk_td_names typtag_lhs)) |> Drule.export_without_context
 
   (* Declare the td_names (typ_info_t ..) = ... and add it to the simpset *)

tools/c-parser/umm_heap/AARCH64/Word_Mem_Encoding.thy

@@ -17,6 +17,6 @@ where
                        (len_exp TYPE('a))
                        \<lparr> field_access = \<lambda>v bs. (rev o word_rsplit) v,
                          field_update = \<lambda>bs v. (word_rcat (rev bs)::'a::len8 word) \<rparr>)
-            (''word'' @  nat_to_bin_string (len_of TYPE('a)))"
+            (signed_or_unsigned_as_str TYPE('a) @ ''word'' @ nat_to_bin_string (len_of TYPE('a)))"
 
 end

tools/c-parser/umm_heap/ARM/Word_Mem_Encoding.thy

@@ -12,6 +12,6 @@ begin
 definition
   word_tag :: "'a::len8 word itself \<Rightarrow> 'a word typ_info"
 where
-  "word_tag (w::'a::len8 word itself) \<equiv> TypDesc (TypScalar (len_of TYPE('a) div 8) (len_exp TYPE('a)) \<lparr> field_access = \<lambda>v bs. (rev o word_rsplit) v, field_update = \<lambda>bs v. (word_rcat (rev bs)::'a::len8 word) \<rparr>)  (''word'' @  nat_to_bin_string (len_of TYPE('a)) )"
+  "word_tag (w::'a::len8 word itself) \<equiv> TypDesc (TypScalar (len_of TYPE('a) div 8) (len_exp TYPE('a)) \<lparr> field_access = \<lambda>v bs. (rev o word_rsplit) v, field_update = \<lambda>bs v. (word_rcat (rev bs)::'a::len8 word) \<rparr>)  (signed_or_unsigned_as_str TYPE('a) @ ''word'' @ nat_to_bin_string (len_of TYPE('a)) )"
 
 end

tools/c-parser/umm_heap/ARM_HYP/Word_Mem_Encoding.thy

@@ -12,6 +12,6 @@ begin
 definition
   word_tag :: "'a::len8 word itself \<Rightarrow> 'a word typ_info"
 where
-  "word_tag (w::'a::len8 word itself) \<equiv> TypDesc (TypScalar (len_of TYPE('a) div 8) (len_exp TYPE('a)) \<lparr> field_access = \<lambda>v bs. (rev o word_rsplit) v, field_update = \<lambda>bs v. (word_rcat (rev bs)::'a::len8 word) \<rparr>)  (''word'' @  nat_to_bin_string (len_of TYPE('a)) )"
+  "word_tag (w::'a::len8 word itself) \<equiv> TypDesc (TypScalar (len_of TYPE('a) div 8) (len_exp TYPE('a)) \<lparr> field_access = \<lambda>v bs. (rev o word_rsplit) v, field_update = \<lambda>bs v. (word_rcat (rev bs)::'a::len8 word) \<rparr>)  (signed_or_unsigned_as_str TYPE('a) @  ''word'' @  nat_to_bin_string (len_of TYPE('a)) )"
 
 end

tools/c-parser/umm_heap/RISCV64/Word_Mem_Encoding.thy

@@ -17,6 +17,6 @@ where
                        (len_exp TYPE('a))
                        \<lparr> field_access = \<lambda>v bs. (rev o word_rsplit) v,
                          field_update = \<lambda>bs v. (word_rcat (rev bs)::'a::len8 word) \<rparr>)
-            (''word'' @  nat_to_bin_string (len_of TYPE('a)))"
+            (signed_or_unsigned_as_str TYPE('a) @ ''word'' @ nat_to_bin_string (len_of TYPE('a)))"
 
 end

tools/c-parser/umm_heap/StructSupport.thy

@@ -485,15 +485,15 @@ lemma td_names_ptr [simp]:
 lemma td_names_word8 [simp]:
   fixes x :: "byte itself"
   shows "td_names (typ_info_t x) = {''word00010''}"
- by (simp add: pad_typ_name_def nat_to_bin_string.simps)
+ by (simp add: pad_typ_name_def nat_to_bin_string.simps signed_or_unsigned)
 
 lemma td_names_word32 [simp]:
   "td_names (typ_info_t TYPE(32 word)) = {''word0000010''}"
-  by (simp add: pad_typ_name_def nat_to_bin_string.simps)
+  by (simp add: pad_typ_name_def nat_to_bin_string.simps signed_or_unsigned)
 
 lemma td_names_word64 [simp]:
   "td_names (typ_info_t TYPE(64 word)) = {''word00000010''}"
-  by (simp add: pad_typ_name_def nat_to_bin_string.simps)
+  by (simp add: pad_typ_name_def nat_to_bin_string.simps signed_or_unsigned)
 
 lemma td_names_export_uinfo [simp]:
   "td_names (export_uinfo td) = td_names td"

tools/c-parser/umm_heap/Vanilla32.thy

@@ -9,7 +9,6 @@ theory Vanilla32
 imports Word_Mem_Encoding CTypes
 begin
 
-
 overloading typ_info_word \<equiv> typ_info_t begin
 definition
   typ_info_word: "typ_info_word (w::'a::len8 word itself) \<equiv> word_tag w"
@@ -337,7 +336,7 @@ lemma ptr_typ_name [simp]:
   by simp
 
 lemma word_typ_name [simp]:
-  "typ_name (typ_info_t TYPE('a::len8 word)) = ''word'' @ nat_to_bin_string (len_of TYPE('a))"
+  "typ_name (typ_info_t TYPE('a::len8 word)) = signed_or_unsigned_as_str TYPE('a) @ ''word'' @ nat_to_bin_string (len_of TYPE('a))"  
   by simp
 
 lemma nat_to_bin_string_word_sizes [simp]:
@@ -357,19 +356,19 @@ lemma typ_name_words [simp]:
    "typ_name (typ_info_t  TYPE(16 word)) = ''word000010''"
    "typ_name (typ_info_t  TYPE(32 word)) = ''word0000010''"
    "typ_name (typ_info_t  TYPE(64 word)) = ''word00000010''"
-  by (auto simp: typ_uinfo_t_def)
+  by (auto simp: typ_uinfo_t_def signed_or_unsigned)
 
 lemma typ_name_swords [simp]:
-   "typ_name (typ_uinfo_t TYPE(8 sword))  = ''word00010''"
-   "typ_name (typ_uinfo_t TYPE(16 sword)) = ''word000010''"
-   "typ_name (typ_uinfo_t TYPE(32 sword)) = ''word0000010''"
-   "typ_name (typ_uinfo_t TYPE(64 sword)) = ''word00000010''"
+   "typ_name (typ_uinfo_t TYPE(8 sword))  = ''sword00010''"
+   "typ_name (typ_uinfo_t TYPE(16 sword)) = ''sword000010''"
+   "typ_name (typ_uinfo_t TYPE(32 sword)) = ''sword0000010''"
+   "typ_name (typ_uinfo_t TYPE(64 sword)) = ''sword00000010''"
    (* these do not fire in a simple simp, because typ_info_word takes precedence (innermost term): *)
-   "typ_name (typ_info_t  TYPE(8 sword))  = ''word00010''"
-   "typ_name (typ_info_t  TYPE(16 sword)) = ''word000010''"
-   "typ_name (typ_info_t  TYPE(32 sword)) = ''word0000010''"
-   "typ_name (typ_info_t  TYPE(64 sword)) = ''word00000010''"
-  by (auto simp: typ_uinfo_t_def)
+   "typ_name (typ_info_t  TYPE(8 sword))  = ''sword00010''"
+   "typ_name (typ_info_t  TYPE(16 sword)) = ''sword000010''"
+   "typ_name (typ_info_t  TYPE(32 sword)) = ''sword0000010''"
+   "typ_name (typ_info_t  TYPE(64 sword)) = ''sword00000010''"
+  by (auto simp: typ_uinfo_t_def signed_or_unsigned)
 
 lemma ptr_arith[simp]:
   "(x +\<^sub>p a = y +\<^sub>p a) = ((x::('a::c_type) ptr) = (y::'a ptr))"

tools/c-parser/umm_heap/Vanilla32_Preliminaries.thy

@@ -80,7 +80,74 @@ by (simp add: len_exp_def bogus_log2lessthree_def)
 lemma lx_signed' [simp]: "len_exp (x::('a::len) signed itself) = len_exp (TYPE('a))"
   by (simp add: len_exp_def)
 
-class len8 = len +
+(* Maybe not required, but keeps everything neat *)
+class typ_num 
+
+instantiation num0 and num1 :: typ_num
+begin
+instance ..
+end
+
+instantiation bit0 and bit1 :: (typ_num) typ_num
+begin
+instance ..
+end
+
+class signed_or_unsigned =  
+  fixes signed_or_unsigned_as_str :: "'a itself \<Rightarrow> char list"
+
+instantiation num0 :: signed_or_unsigned
+begin
+
+definition
+  num0_signed_or_unsigned_def: "signed_or_unsigned_as_str (w :: num0 itself) = []" 
+
+instance ..
+end
+
+instantiation num1 :: signed_or_unsigned
+begin
+
+definition
+  num1_signed_or_unsigned_def: "signed_or_unsigned_as_str (w :: num1 itself) = []" 
+
+instance ..
+end
+
+instantiation bit0 :: (type) signed_or_unsigned
+begin
+
+definition
+  bit0_signed_or_unsigned_def: "signed_or_unsigned_as_str (w :: 'a bit0 itself) = []" 
+
+instance ..
+end
+
+instantiation bit1 :: (type) signed_or_unsigned
+begin
+
+definition
+  bit1_signed_or_unsigned_def: "signed_or_unsigned_as_str (w :: 'a bit1 itself) = []" 
+
+instance ..
+end
+
+instantiation signed :: (type) signed_or_unsigned
+begin
+
+definition
+  signed_signed_or_unsigned_def: "signed_or_unsigned_as_str (w :: 'a signed itself) = ''s''" 
+
+instance ..
+end
+
+lemmas signed_or_unsigned = num0_signed_or_unsigned_def 
+                            num1_signed_or_unsigned_def 
+                            bit0_signed_or_unsigned_def 
+                            bit1_signed_or_unsigned_def 
+                            signed_signed_or_unsigned_def 
+
+class len8 = signed_or_unsigned + len +
   (* this constraint gives us (in the most convoluted way possible) that we're only
      interested in words with a length that is divisible by 8 *)
   assumes len8_bytes: "len_of TYPE('a::len) = 8 * (2^len_exp TYPE('a))"

tools/c-parser/umm_heap/X64/Word_Mem_Encoding.thy

@@ -17,6 +17,6 @@ where
                        (len_exp TYPE('a))
                        \<lparr> field_access = \<lambda>v bs. (rev o word_rsplit) v,
                          field_update = \<lambda>bs v. (word_rcat (rev bs)::'a::len8 word) \<rparr>)
-            (''word'' @  nat_to_bin_string (len_of TYPE('a)))"
+            (signed_or_unsigned_as_str TYPE('a) @ ''word'' nat_to_bin_string (len_of TYPE('a)))"
 
 end