Coq: reverse_endianness

2 files changed, 22 insertions, 9 deletions

diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v
index 3ecaca12..224ab18d 100644
--- a/lib/coq/Sail2_operators_mwords.v
+++ b/lib/coq/Sail2_operators_mwords.v
@@ -2,7 +2,7 @@ Require Import Sail2_values.
 Require Import Sail2_operators.
 Require Import Sail2_prompt_monad.
 Require Import Sail2_prompt.
-Require bbv.Word.
+Require Import bbv.Word.
 Require Import Arith.
 Require Import ZArith.
 Require Import Omega.
@@ -366,4 +366,18 @@ Definition sgteq_vec := sgteq_bv.
 
 *)
 
+Program Fixpoint reverse_endianness_word {n} (bits : word n) : word n :=
+  match n with
+  | S (S (S (S (S (S (S (S m))))))) =>
+    combine
+      (reverse_endianness_word (split2 8 m bits))
+      (split1 8 m bits)
+  | _ => bits
+  end.
+Next Obligation.
+omega.
+Qed.
+
+Definition reverse_endianness {n} (bits : mword n) := with_word (P := id) reverse_endianness_word bits.
+
 Definition get_slice_int {a} `{ArithFact (a >= 0)} : Z -> Z -> Z -> mword a := get_slice_int_bv.
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index c3acbbcb..23e7f486 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -939,7 +939,7 @@ Definition mem_bytes_of_bits (bs : a) := option_map (@rev (list bitU)) (bytes_of
 Definition bits_of_mem_bytes (bs : list memory_byte) := bits_of_bytes (List.rev bs).
 
 End BytesBits.
-(*
+
 (*val bitv_of_byte_lifteds : list Sail_impl_base.byte_lifted -> list bitU
 Definition bitv_of_byte_lifteds v :=
   foldl (fun x (Byte_lifted y) => x ++ (List.map bitU_of_bit_lifted y)) [] v
@@ -983,13 +983,12 @@ Definition address_of_bitv v :=
   let bytes := bytes_of_bitv v in
   address_of_byte_list bytes*)
 
-Fixpoint reverse_endianness_list bits :=
-  if List.length bits <= 8 then bits else
-    reverse_endianness_list (drop_list 8 bits) ++ take_list 8 bits
-
-val reverse_endianness : forall a. Bitvector a => a -> a
-Definition reverse_endianness v := of_bits (reverse_endianness_list (bits_of v))
-*)
+Fixpoint reverse_endianness_list (bits : list bitU) :=
+  match bits with
+  | _ :: _ :: _ :: _ :: _ :: _ :: _ :: _ :: t =>
+    reverse_endianness_list t ++ firstn 8 bits
+  | _ => bits
+  end.
 
 (*** Registers *)