From c532c4dc18b881086bba2644b92905bce96ab2a3 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 30 Aug 2018 15:48:51 +0100
Subject: Coq: correct endianness reversal bug

---
 snapshots/coq-riscv/sail/lib/coq/Sail2_values.v | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

(limited to 'snapshots')

diff --git a/snapshots/coq-riscv/sail/lib/coq/Sail2_values.v b/snapshots/coq-riscv/sail/lib/coq/Sail2_values.v
index 9c1173f1..def6e248 100644
--- a/snapshots/coq-riscv/sail/lib/coq/Sail2_values.v
+++ b/snapshots/coq-riscv/sail/lib/coq/Sail2_values.v
@@ -857,17 +857,21 @@ val make_the_value : forall n. Z -> itself n
 Definition inline make_the_value x := the_value
 *)
 
-Fixpoint bitlistFromWord {n} w :=
+Fixpoint bitlistFromWord_rev {n} w :=
 match w with
 | WO => []
-| WS b w => b :: bitlistFromWord w
+| WS b w => b :: bitlistFromWord_rev w
 end.
+Definition bitlistFromWord {n} w :=
+  List.rev (@bitlistFromWord_rev n w).
 
-Fixpoint wordFromBitlist l : word (length l) :=
+Fixpoint wordFromBitlist_rev l : word (length l) :=
 match l with
 | [] => WO
-| b::t => WS b (wordFromBitlist t)
+| b::t => WS b (wordFromBitlist_rev t)
 end.
+Definition wordFromBitlist l : word (length l) :=
+  nat_cast _ (List.rev_length l) (wordFromBitlist_rev (List.rev l)).
 
 Local Open Scope nat.
 
-- 
cgit v1.2.3