Experiment with making vector and bitvector distinct types

Only change that should be needed for 99.9% of uses is to change
vector('n, 'ord, bit) to bitvector('n, 'ord), and adding

$ifndef FEATURE_BITVECTOR_TYPE
type bitvector('n, dec) = vector('n, dec, bit)
$endif

for to support any Sail before this

Currently I have all C, Typechecking, and SMT tests passing, as well
as the RISC-V spec building OCaml and C completely unmodified.

1 files changed, 5 insertions, 0 deletions

diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index 13ed491b..40f5cecf 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -106,6 +106,11 @@ let rec undefined_vector (len, item) =
   then []
   else item :: undefined_vector (Big_int.sub len (Big_int.of_int 1), item)
 
+let rec undefined_bitvector len =
+  if Big_int.equal len Big_int.zero
+  then []
+  else B0 :: undefined_vector (Big_int.sub len (Big_int.of_int 1), B0)
+
 let undefined_string () = ""
 
 let undefined_unit () = ()