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.

4 files changed, 33 insertions, 33 deletions

diff --git a/lib/sail.c b/lib/sail.c
index 5530b462..d501fb0e 100644
--- a/lib/sail.c
+++ b/lib/sail.c
@@ -578,7 +578,7 @@ sbits CONVERT_OF(sbits, lbits)(const lbits op, const bool direction)
   return rop;
 }
 
-void UNDEFINED(lbits)(lbits *rop, const sail_int len, const fbits bit)
+void UNDEFINED(lbits)(lbits *rop, const sail_int len)
 {
   zeros(rop, len);
 }
diff --git a/lib/sail.h b/lib/sail.h
index b50a5a4c..39b9723e 100644
--- a/lib/sail.h
+++ b/lib/sail.h
@@ -223,7 +223,7 @@ void CONVERT_OF(lbits, sbits)(lbits *, const sbits, const bool);
 sbits CONVERT_OF(sbits, fbits)(const fbits, const uint64_t, const bool);
 sbits CONVERT_OF(sbits, lbits)(const lbits, const bool);
 
-void UNDEFINED(lbits)(lbits *, const sail_int len, const fbits bit);
+void UNDEFINED(lbits)(lbits *, const sail_int len);
 fbits UNDEFINED(fbits)(const unit);
 
 sbits undefined_sbits(void);
diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
index ee84087e..4e4a099f 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -3,7 +3,7 @@ $define _VECTOR_DEC
 
 $include <flow.sail>
 
-type bits ('n : Int) = vector('n, dec, bit)
+type bits ('n : Int) = bitvector('n, dec)
 
 val eq_bits = {
   ocaml: "eq_list",
@@ -11,7 +11,7 @@ val eq_bits = {
   lem: "eq_vec",
   c: "eq_bits",
   coq: "eq_vec"
-} : forall 'n. (vector('n, dec, bit), vector('n, dec, bit)) -> bool
+} : forall 'n. (bits('n), bits('n)) -> bool
 
 overload operator == = {eq_bit, eq_bits}
 
@@ -19,13 +19,13 @@ val neq_bits = {
   lem: "neq_vec",
   c: "neq_bits",
   coq: "neq_vec"
-} : forall 'n. (vector('n, dec, bit), vector('n, dec, bit)) -> bool
+} : forall 'n. (bits('n), bits('n)) -> bool
 
 function neq_bits(x, y) = not_bool(eq_bits(x, y))
 
 overload operator != = {neq_bits}
 
-val bitvector_length = {coq: "length_mword", _:"length"} : forall 'n. bits('n) -> atom('n)
+val bitvector_length = {coq: "length_mword", _:"length"} : forall 'n. bits('n) -> int('n)
 
 val vector_length = {
   ocaml: "length",
@@ -33,7 +33,7 @@ val vector_length = {
   lem: "length_list",
   c: "length",
   coq: "vec_length"
-} : forall 'n ('a : Type). vector('n, dec, 'a) -> atom('n)
+} : forall 'n ('a : Type). vector('n, dec, 'a) -> int('n)
 
 overload length = {bitvector_length, vector_length}
 
@@ -41,9 +41,9 @@ val "print_bits" : forall 'n. (string, bits('n)) -> unit
 
 val "prerr_bits" : forall 'n. (string, bits('n)) -> unit
 
-val sail_sign_extend = "sign_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
+val sail_sign_extend = "sign_extend" : forall 'n 'm, 'm >= 'n. (bits('n), int('m)) -> bits('m)
 
-val sail_zero_extend = "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
+val sail_zero_extend = "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), int('m)) -> bits('m)
 
 /*!
 THIS`(v, n)` truncates `v`, keeping only the _least_ significant `n` bits.
@@ -54,7 +54,7 @@ val truncate = {
   lem: "vector_truncate",
   coq: "vector_truncate",
   c: "sail_truncate"
-} : forall 'm 'n, 'm >= 0 & 'm <= 'n. (vector('n, dec, bit), atom('m)) -> vector('m, dec, bit)
+} : forall 'm 'n, 'm >= 0 & 'm <= 'n. (bits('n), int('m)) -> bits('m)
 
 /*!
 THIS`(v, n)` truncates `v`, keeping only the _most_ significant `n` bits.
@@ -64,9 +64,9 @@ val truncateLSB = {
   lem: "vector_truncateLSB",
   coq: "vector_truncateLSB",
   c: "sail_truncateLSB"
-} : forall 'm 'n, 'm >= 0 & 'm <= 'n. (vector('n, dec, bit), atom('m)) -> vector('m, dec, bit)
+} : forall 'm 'n, 'm >= 0 & 'm <= 'n. (bits('n), int('m)) -> bits('m)
 
-val sail_mask : forall 'len 'v, 'len >= 0 & 'v >= 0. (atom('len), vector('v, dec, bit)) -> vector('len, dec, bit)
+val sail_mask : forall 'len 'v, 'len >= 0 & 'v >= 0. (int('len), bits('v)) -> bits('len)
 
 function sail_mask(len, v) = if len <= length(v) then truncate(v, len) else sail_zero_extend(v, len)
 
@@ -94,7 +94,7 @@ val plain_vector_access = {
   lem: "access_list_dec",
   coq: "vec_access_dec",
   c: "vector_access"
-} : forall ('n : Int) ('m : Int) ('a : Type), 0 <= 'm < 'n. (vector('n, dec, 'a), atom('m)) -> 'a
+} : forall ('n : Int) ('m : Int) ('a : Type), 0 <= 'm < 'n. (vector('n, dec, 'a), int('m)) -> 'a
 
 overload vector_access = {bitvector_access, plain_vector_access}
 
@@ -104,7 +104,7 @@ val bitvector_update = {
   lem: "update_vec_dec",
   coq: "update_vec_dec",
   c: "vector_update"
-} : forall 'n 'm, 0 <= 'm < 'n. (bits('n), atom('m), bit) -> bits('n)
+} : forall 'n 'm, 0 <= 'm < 'n. (bits('n), int('m), bit) -> bits('n)
 
 val plain_vector_update = {
   ocaml: "update",
@@ -112,7 +112,7 @@ val plain_vector_update = {
   lem: "update_list_dec",
   coq: "vec_update_dec",
   c: "vector_update"
-} : forall 'n 'm ('a : Type), 0 <= 'm < 'n. (vector('n, dec, 'a), atom('m), 'a) -> vector('n, dec, 'a)
+} : forall 'n 'm ('a : Type), 0 <= 'm < 'n. (vector('n, dec, 'a), int('m), 'a) -> vector('n, dec, 'a)
 
 overload vector_update = {bitvector_update, plain_vector_update}
 
@@ -170,7 +170,7 @@ val vector_subrange = {
   c: "vector_subrange",
   coq: "subrange_vec_dec"
 } : forall ('n : Int) ('m : Int) ('o : Int), 0 <= 'o <= 'm < 'n.
-  (bits('n), atom('m), atom('o)) -> bits('m - 'o + 1)
+  (bits('n), int('m), int('o)) -> bits('m - 'o + 1)
 
 val vector_update_subrange = {
   ocaml: "update_subrange",
@@ -178,45 +178,45 @@ val vector_update_subrange = {
   lem: "update_subrange_vec_dec",
   c: "vector_update_subrange",
   coq: "update_subrange_vec_dec"
-} : forall 'n 'm 'o, 0 <= 'o <= 'm < 'n. (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
+} : forall 'n 'm 'o, 0 <= 'o <= 'm < 'n. (bits('n), int('m), int('o), bits('m - ('o - 1))) -> bits('n)
 
 val sail_shiftleft = "shiftl" : forall 'n ('ord : Order).
-    (vector('n, 'ord, bit), int) -> vector('n, 'ord, bit) effect pure
+    (bitvector('n, 'ord), int) -> bitvector('n, 'ord) effect pure
 
 val sail_shiftright = "shiftr" : forall 'n ('ord : Order).
-    (vector('n, 'ord, bit), int) -> vector('n, 'ord, bit) effect pure
+    (bitvector('n, 'ord), int) -> bitvector('n, 'ord) effect pure
 
 val sail_arith_shiftright = "arith_shiftr" : forall 'n ('ord : Order).
-    (vector('n, 'ord, bit), int) -> vector('n, 'ord, bit) effect pure
+    (bitvector('n, 'ord), int) -> bitvector('n, 'ord) effect pure
 
-val sail_zeros = "zeros" : forall 'n, 'n >= 0. atom('n) -> bits('n)
+val sail_zeros = "zeros" : forall 'n, 'n >= 0. int('n) -> bits('n)
 
-val sail_ones : forall 'n, 'n >= 0. atom('n) -> bits('n)
+val sail_ones : forall 'n, 'n >= 0. int('n) -> bits('n)
 
 function sail_ones(n) = not_vec(sail_zeros(n))
 
 // Some ARM specific builtins
 
 val slice = "slice" : forall 'n 'm 'o, 0 <= 'm & 0 <= 'n.
-  (bits('m), atom('o), atom('n)) -> bits('n)
+  (bits('m), int('o), int('n)) -> bits('n)
 
-val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
+val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), int('m)) -> bits('n * 'm)
 
 val slice_mask : forall 'n, 'n >= 0. (implicit('n), int, int) -> bits('n) effect pure
 function slice_mask(n,i,l) =
   if l >= n then {
     sail_ones(n)
   } else {
-    let one : bits('n) = sail_mask(n, [bitone] : bits(1)) in
+    let one : bits('n) = sail_mask(n, 0b1 : bits(1)) in
     sail_shiftleft(sub_bits(sail_shiftleft(one, l), one), i)
   }
 
-val get_slice_int = "get_slice_int" : forall 'w. (atom('w), int, int) -> bits('w)
+val get_slice_int = "get_slice_int" : forall 'w. (int('w), int, int) -> bits('w)
 
-val set_slice_int = "set_slice_int" : forall 'w. (atom('w), int, int, bits('w)) -> int
+val set_slice_int = "set_slice_int" : forall 'w. (int('w), int, int, bits('w)) -> int
 
 val set_slice_bits = "set_slice" : forall 'n 'm.
-  (atom('n), atom('m), bits('n), int, bits('m)) -> bits('n)
+  (int('n), int('m), bits('n), int, bits('m)) -> bits('n)
 
 /*!
 converts a bit vector of length $n$ to an integer in the range $0$ to $2^n - 1$.
@@ -238,6 +238,6 @@ val signed = {
   _: "sint"
 } : forall 'n, 'n > 0. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1)
 
-overload __size = {__id, length}
+overload __size = {__id, bitvector_length}
 
 $endif
diff --git a/lib/vector_inc.sail b/lib/vector_inc.sail
index daba99be..381ae6bc 100644
--- a/lib/vector_inc.sail
+++ b/lib/vector_inc.sail
@@ -3,7 +3,7 @@ $define _VECTOR_INC
 
 $include <flow.sail>
 
-type bits ('n : Int) = vector('n, inc, bit)
+type bits ('n : Int) = bitvector('n, inc)
 
 val "eq_bit" : (bit, bit) -> bool
 
@@ -13,7 +13,7 @@ val eq_bits = {
   lem: "eq_vec",
   c: "eq_bits",
   coq: "eq_vec"
-} : forall 'n. (vector('n, inc, bit), vector('n, inc, bit)) -> bool
+} : forall 'n. (bits('n), bits('n)) -> bool
 
 overload operator == = {eq_bit, eq_bits}
 
@@ -43,9 +43,9 @@ val truncate = {
   lem: "vector_truncate",
   coq: "vector_truncate",
   c: "truncate"
-} : forall 'm 'n, 'm >= 0 & 'm <= 'n. (vector('n, inc, bit), atom('m)) -> vector('m, inc, bit)
+} : forall 'm 'n, 'm >= 0 & 'm <= 'n. (bits('n), atom('m)) -> bits('m)
 
-val mask : forall 'len 'v, 'len >= 0 & 'v >= 0. (atom('len), vector('v, inc, bit)) -> vector('len, inc, bit)
+val mask : forall 'len 'v, 'len >= 0 & 'v >= 0. (atom('len), bits('v)) -> bits('len)
 
 function mask(len, v) = if len <= length(v) then truncate(v, len) else zero_extend(v, len)