From dcf8d012c689ab17df29be33fbb087e2da2f3440 Mon Sep 17 00:00:00 2001
From: Tim Hutt <timothy.hutt@codasip.com>
Date: Wed, 12 Jun 2024 11:19:21 +0100
Subject: [PATCH] Use bool <-> bit mappings from riscv_types.sail

Use these mappings and change the other functions to be aliases of them.
---
 model/prelude.sail     | 26 ++++++++++++++++++--------
 model/riscv_types.sail | 10 ----------
 2 files changed, 18 insertions(+), 18 deletions(-)

diff --git a/model/prelude.sail b/model/prelude.sail
index ae1cafc3a..45d49c0ed 100644
--- a/model/prelude.sail
+++ b/model/prelude.sail
@@ -99,18 +99,28 @@ overload zeros = {zeros_implicit}
 val ones : forall 'n, 'n >= 0 . implicit('n) -> bits('n)
 function ones (n) = sail_ones (n)
 
-val bool_to_bit : bool -> bit
-function bool_to_bit x = if x then bitone else bitzero
+mapping bool_bit : bool <-> bit = {
+  true <-> bitone,
+  false <-> bitzero,
+}
 
-val bool_to_bits : bool -> bits(1)
-function bool_to_bits x = [bool_to_bit(x)]
+mapping bool_bits : bool <-> bits(1) = {
+  true   <-> 0b1,
+  false  <-> 0b0,
+}
 
-val bit_to_bool : bit -> bool
-function bit_to_bool b = match b {
-  bitone  => true,
-  bitzero => false
+mapping bool_not_bits : bool <-> bits(1) = {
+  true   <-> 0b0,
+  false  <-> 0b1,
 }
 
+// These aliases make the conversion direction a bit clearer.
+function bool_to_bit(x : bool) -> bit = bool_bit(x)
+function bit_to_bool(x : bit) -> bool = bool_bit(x)
+function bool_to_bits(x : bool) -> bits(1) = bool_bits(x)
+function bits_to_bool(x : bits(1)) -> bool = bool_bits(x)
+
+
 val to_bits : forall 'l, 'l >= 0.(int('l), int) -> bits('l)
 function to_bits (l, n) = get_slice_int(l, n, 0)
 
diff --git a/model/riscv_types.sail b/model/riscv_types.sail
index 61e0089ac..f6e2d1ced 100644
--- a/model/riscv_types.sail
+++ b/model/riscv_types.sail
@@ -356,16 +356,6 @@ enum extop_zbb = {RISCV_SEXTB, RISCV_SEXTH, RISCV_ZEXTH}
 
 enum zicondop = {RISCV_CZERO_EQZ, RISCV_CZERO_NEZ}
 
-mapping bool_bits : bool <-> bits(1) = {
-  true   <-> 0b1,
-  false  <-> 0b0
-}
-
-mapping bool_not_bits : bool <-> bits(1) = {
-  true   <-> 0b0,
-  false  <-> 0b1
-}
-
 // Get the bit encoding of word_width.
 mapping size_enc : word_width <-> bits(2) = {
   BYTE   <-> 0b00,