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.

60 files changed, 321 insertions, 260 deletions

diff --git a/editors/sail-mode.el b/editors/sail-mode.el
index a0d98429..e65d9428 100644
--- a/editors/sail-mode.el
+++ b/editors/sail-mode.el
@@ -40,7 +40,7 @@
     "exmem" "undef" "unspec" "nondet" "escape" "configuration"))
 
 (defconst sail2-types
-  '("vector" "int" "nat" "atom" "range" "unit" "bit" "real" "list" "bool" "string" "bits" "option"
+  '("vector" "bitvector" "int" "nat" "atom" "range" "unit" "bit" "real" "list" "bool" "string" "bits" "option"
     "uint64_t" "int64_t" "bv_t" "mpz_t"))
 
 (defconst sail2-special
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)
 
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 70845468..014d50d0 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -397,6 +397,11 @@ let vector_typ n ord typ =
                     mk_typ_arg (A_order ord);
                     mk_typ_arg (A_typ typ)]))
 
+let bitvector_typ n ord =
+  mk_typ (Typ_app (mk_id "bitvector",
+                   [mk_typ_arg (A_nexp (nexp_simp n));
+                    mk_typ_arg (A_order ord)]))
+
 let exc_typ = mk_id_typ (mk_id "exception")
 
 let nconstant c = Nexp_aux (Nexp_constant c, Parse_ast.Unknown)
@@ -1264,6 +1269,8 @@ let typ_app_args_of = function
 let rec vector_typ_args_of typ = match typ_app_args_of typ with
   | ("vector", [A_nexp len; A_order ord; A_typ etyp], l) ->
      (nexp_simp len, ord, etyp)
+  | ("bitvector", [A_nexp len; A_order ord], l) ->
+     (nexp_simp len, ord, bit_typ)
   | ("register", [A_typ rtyp], _) -> vector_typ_args_of rtyp
   | (_, _, l) ->
      raise (Reporting.err_typ l
@@ -1286,11 +1293,11 @@ let is_bit_typ = function
   | Typ_aux (Typ_id (Id_aux (Id "bit", _)), _) -> true
   | _ -> false
 
-let is_bitvector_typ typ =
-  if is_vector_typ typ then
-    let (_,_,etyp) = vector_typ_args_of typ in
-    is_bit_typ etyp
-  else false
+let rec is_bitvector_typ = function
+  | Typ_aux (Typ_app (Id_aux (Id "bitvector", _), [_;_]), _) -> true
+  | Typ_aux (Typ_app (Id_aux (Id "register",_), [A_aux (A_typ rtyp,_)]), _) ->
+    is_bitvector_typ rtyp
+  | _ -> false
 
 let has_effect (Effect_aux (eff,_)) searched_for = match eff with
   | Effect_set effs ->
diff --git a/src/ast_util.mli b/src/ast_util.mli
index c8f3cc5c..ee8fdf13 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -157,6 +157,7 @@ val unit_typ : typ
 val string_typ : typ
 val real_typ : typ
 val vector_typ : nexp -> order -> typ -> typ
+val bitvector_typ : nexp -> order -> typ
 val list_typ : typ -> typ
 val exc_typ : typ
 val tuple_typ : typ list -> typ
diff --git a/src/bitfield.ml b/src/bitfield.ml
index feda4602..5b0a73b0 100644
--- a/src/bitfield.ml
+++ b/src/bitfield.ml
@@ -55,7 +55,7 @@ open Ast
 open Ast_util
 
 let bitvec size order =
-  Printf.sprintf "vector(%i, %s, bit)" size (string_of_order order)
+  Printf.sprintf "bitvector(%i, %s)" size (string_of_order order)
 
 let rec combine = function
   | [] -> Defs []
@@ -65,12 +65,12 @@ let rec combine = function
 
 let newtype name size order =
   let chunks_64 =
-    Util.list_init (size / 64) (fun i -> Printf.sprintf "%s_chunk_%i : vector(64, %s, bit)" name i (string_of_order order))
+    Util.list_init (size / 64) (fun i -> Printf.sprintf "%s_chunk_%i : bitvector(64, %s)" name i (string_of_order order))
   in
   let chunks =
     if size mod 64 = 0 then chunks_64 else
       let chunk_rem =
-        Printf.sprintf "%s_chunk_%i : vector(%i, %s, bit)" name (List.length chunks_64) (size mod 64) (string_of_order order)
+        Printf.sprintf "%s_chunk_%i : bitvector(%i, %s)" name (List.length chunks_64) (size mod 64) (string_of_order order)
       in
       chunk_rem :: List.rev chunks_64
   in
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 522faab7..1f15d054 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -859,6 +859,7 @@ let initial_ctx = {
           ("list", [K_type]);
           ("register", [K_type]);
           ("range", [K_int; K_int]);
+          ("bitvector", [K_int; K_order]);
           ("vector", [K_int; K_order; K_type]);
           ("atom", [K_int]);
           ("implicit", [K_int]);
@@ -925,7 +926,7 @@ let undefined_builtin_val_specs =
    extern_of_string (mk_id "undefined_range") "forall 'n 'm. (atom('n), atom('m)) -> range('n,'m) effect {undef}";
    extern_of_string (mk_id "undefined_vector") "forall 'n ('a:Type) ('ord : Order). (atom('n), 'a) -> vector('n, 'ord,'a) effect {undef}";
    (* Only used with lem_mwords *)
-   extern_of_string (mk_id "undefined_bitvector") "forall 'n. atom('n) -> vector('n, dec, bit) effect {undef}";
+   extern_of_string (mk_id "undefined_bitvector") "forall 'n. atom('n) -> bitvector('n, dec) effect {undef}";
    extern_of_string (mk_id "undefined_unit") "unit -> unit effect {undef}"]
 
 let generate_undefineds vs_ids (Defs defs) =
diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml
index b98c53c4..2c9c11ee 100644
--- a/src/jib/c_backend.ml
+++ b/src/jib/c_backend.ml
@@ -148,9 +148,8 @@ let rec ctyp_of_typ ctx typ =
      - If the length is less than 64, then use a small bits type, sbits.
      - If the length may be larger than 64, use a large bits type lbits. *)
   | Typ_app (id, [A_aux (A_nexp n, _);
-                  A_aux (A_order ord, _);
-                  A_aux (A_typ (Typ_aux (Typ_id vtyp_id, _)), _)])
-       when string_of_id id = "vector" && string_of_id vtyp_id = "bit" ->
+                  A_aux (A_order ord, _)])
+       when string_of_id id = "bitvector" ->
      let direction = match ord with Ord_aux (Ord_dec, _) -> true | Ord_aux (Ord_inc, _) -> false | _ -> assert false in
      begin match nexp_simp n with
      | Nexp_aux (Nexp_constant n, _) when Big_int.less_equal n (Big_int.of_int 64) -> CT_fbits (Big_int.to_int n, direction)
@@ -1429,8 +1428,8 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
           end
        | "internal_vector_update", _ -> Printf.sprintf "internal_vector_update_%s" (sgen_ctyp_name ctyp)
        | "internal_vector_init", _ -> Printf.sprintf "internal_vector_init_%s" (sgen_ctyp_name ctyp)
-       | "undefined_vector", CT_fbits _ -> "UNDEFINED(fbits)"
-       | "undefined_vector", CT_lbits _ -> "UNDEFINED(lbits)"
+       | "undefined_bitvector", CT_fbits _ -> "UNDEFINED(fbits)"
+       | "undefined_bitvector", CT_lbits _ -> "UNDEFINED(lbits)"
        | "undefined_bit", _ -> "UNDEFINED(fbits)"
        | "undefined_vector", _ -> Printf.sprintf "UNDEFINED(vector_%s)" (sgen_ctyp_name ctyp)
        | fname, _ -> fname
diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml
index f8cb3bcd..90c0022d 100644
--- a/src/jib/jib_compile.ml
+++ b/src/jib/jib_compile.ml
@@ -310,10 +310,10 @@ let rec compile_aval l ctx = function
      begin
        let bitstring = List.map value_of_aval_bit avals in
        let len = List.length avals in
-       match destruct_vector ctx.tc_env typ with
-       | Some (_, Ord_aux (Ord_inc, _), _) ->
+       match destruct_bitvector ctx.tc_env typ with
+       | Some (_, Ord_aux (Ord_inc, _)) ->
           [], V_lit (VL_bits (bitstring, false), CT_fbits (len, false)), []
-       | Some (_, Ord_aux (Ord_dec, _), _) ->
+       | Some (_, Ord_aux (Ord_dec, _)) ->
           [], V_lit (VL_bits (bitstring, true), CT_fbits (len, true)), []
        | Some _ ->
           raise (Reporting.err_general l "Encountered order polymorphic bitvector literal")
@@ -337,8 +337,8 @@ let rec compile_aval l ctx = function
      [iclear (CT_lbits true) gs]
 
   (* If we have a bitvector value, that isn't a literal then we need to set bits individually. *)
-  | AV_vector (avals, Typ_aux (Typ_app (id, [_; A_aux (A_order ord, _); A_aux (A_typ (Typ_aux (Typ_id bit_id, _)), _)]), _))
-       when string_of_id bit_id = "bit" && string_of_id id = "vector" && List.length avals <= 64 ->
+  | AV_vector (avals, Typ_aux (Typ_app (id, [_; A_aux (A_order ord, _)]), _))
+       when string_of_id id = "bitvector" && List.length avals <= 64 ->
      let len = List.length avals in
      let direction = match ord with
        | Ord_aux (Ord_inc, _) -> false
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 897c685a..0d70695b 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -1147,10 +1147,8 @@ let rec ctyp_of_typ ctx typ =
      CT_list (ctyp_of_typ ctx typ)
 
   (* Note that we have to use lbits for zero-length bitvectors because they are not allowed by SMTLIB *)
-  | Typ_app (id, [A_aux (A_nexp n, _);
-                  A_aux (A_order ord, _);
-                  A_aux (A_typ (Typ_aux (Typ_id vtyp_id, _)), _)])
-       when string_of_id id = "vector" && string_of_id vtyp_id = "bit" ->
+  | Typ_app (id, [A_aux (A_nexp n, _); A_aux (A_order ord, _)])
+       when string_of_id id = "bitvector"  ->
      let direction = match ord with Ord_aux (Ord_dec, _) -> true | Ord_aux (Ord_inc, _) -> false | _ -> assert false in
      begin match nexp_simp n with
      | Nexp_aux (Nexp_constant n, _) when Big_int.equal n Big_int.zero -> CT_lbits direction
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 89830d38..d28a2b6e 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -69,7 +69,7 @@ type context = {
   top_env : Env.t
 }
 let empty_ctxt = { early_ret = false; bound_nexps = NexpSet.empty; top_env = Env.empty }
-              
+
 let print_to_from_interp_value = ref false
 let langlebar = string "<|"
 let ranglebar = string "|>"
diff --git a/src/process_file.ml b/src/process_file.ml
index ae79d5c3..1672663b 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -94,6 +94,7 @@ let default_symbols =
   List.fold_left (fun set str -> StringSet.add str set) StringSet.empty
     [ "FEATURE_IMPLICITS";
       "FEATURE_CONSTANT_TYPES";
+      "FEATURE_BITVECTOR_TYPE";
     ]
 
 let symbols = ref default_symbols
diff --git a/src/rewrites.ml b/src/rewrites.ml
index c10d931d..41319b45 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -570,7 +570,7 @@ let remove_vector_concat_pat pat =
         let eff = effect_of_annot (snd annot) in
         let (l,_) = annot in
         let wild _ = P_aux (P_wild,(gen_loc l, mk_tannot env bit_typ eff)) in
-        if is_vector_typ typ then
+        if is_vector_typ typ || is_bitvector_typ typ then
           match p, vector_typ_args_of typ with
           | P_vector ps,_ -> acc @ ps
           | _, (Nexp_aux (Nexp_constant length,_),_,_) ->
@@ -1990,11 +1990,13 @@ let rewrite_undefined_if_gen always_bitvector env defs =
   then rewrite_undefined (always_bitvector || !Pretty_print_lem.opt_mwords) env defs
   else defs
 
-let rec simple_typ (Typ_aux (typ_aux, l) as typ) = Typ_aux (simple_typ_aux typ_aux, l)
-and simple_typ_aux = function
+let rec simple_typ (Typ_aux (typ_aux, l) as typ) = Typ_aux (simple_typ_aux l typ_aux, l)
+and simple_typ_aux l = function
   | Typ_id id -> Typ_id id
   | Typ_app (id, [_; _; A_aux (A_typ typ, l)]) when Id.compare id (mk_id "vector") = 0 ->
      Typ_app (mk_id "list", [A_aux (A_typ (simple_typ typ), l)])
+  | Typ_app (id, [_; _]) when Id.compare id (mk_id "bitvector") = 0 ->
+     Typ_app (mk_id "list", [A_aux (A_typ bit_typ, gen_loc l)])
   | Typ_app (id, [_]) when Id.compare id (mk_id "atom") = 0 ->
      Typ_id (mk_id "int")
   | Typ_app (id, [_; _]) when Id.compare id (mk_id "range") = 0 ->
@@ -2004,7 +2006,7 @@ and simple_typ_aux = function
   | Typ_app (id, args) -> Typ_app (id, List.concat (List.map simple_typ_arg args))
   | Typ_fn (arg_typs, ret_typ, effs) -> Typ_fn (List.map simple_typ arg_typs, simple_typ ret_typ, effs)
   | Typ_tup typs -> Typ_tup (List.map simple_typ typs)
-  | Typ_exist (_, _, Typ_aux (typ, l)) -> simple_typ_aux typ
+  | Typ_exist (_, _, Typ_aux (typ, l)) -> simple_typ_aux l typ
   | typ_aux -> typ_aux
 and simple_typ_arg (A_aux (typ_arg_aux, l)) =
   match typ_arg_aux with
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 () = ()
diff --git a/src/type_check.ml b/src/type_check.ml
index 2be68ade..fabcd7b4 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -543,6 +543,7 @@ end = struct
         ("atom", [K_int]);
         ("implicit", [K_int]);
         ("vector", [K_int; K_order; K_type]);
+        ("bitvector", [K_int; K_order]);
         ("register", [K_type]);
         ("bit", []);
         ("unit", []);
@@ -1330,6 +1331,7 @@ let default_order_error_string =
   "No default Order (if you have set a default Order, move it earlier in the specification)"
 
 let dvector_typ env n typ = vector_typ n (Env.get_default_order env) typ
+let bits_typ env n = bitvector_typ n (Env.get_default_order env)
 
 let add_existential l kopts nc env =
   let env = List.fold_left (fun env kopt -> Env.add_typ_var l kopt env) env kopts in
@@ -1388,6 +1390,15 @@ let destruct_vector env typ =
   in
   destruct_vector' (Env.expand_synonyms env typ)
 
+let destruct_bitvector env typ =
+  let destruct_bitvector' = function
+    | Typ_aux (Typ_app (id, [A_aux (A_nexp n1, _);
+                             A_aux (A_order o, _)]
+                       ), _) when string_of_id id = "bitvector" -> Some (nexp_simp n1, o)
+    | typ -> None
+  in
+  destruct_bitvector' (Env.expand_synonyms env typ)
+
 let rec is_typ_monomorphic (Typ_aux (typ, l)) =
   match typ with
   | Typ_id _ -> true
@@ -2174,7 +2185,7 @@ let rec rewrite_sizeof' env (Nexp_aux (aux, l) as nexp) =
        | Typ_app (id, [A_aux (A_nexp n, _)]) when string_of_id id = "atom" ->
           prove __POS__ env (nc_eq (nvar v) n)
 
-       | Typ_app (id, [A_aux (A_nexp (Nexp_aux (Nexp_var v', _)), _); _; _]) when string_of_id id = "vector" ->
+       | Typ_app (id, [A_aux (A_nexp (Nexp_aux (Nexp_var v', _)), _); _]) when string_of_id id = "bitvector" ->
           Kid.compare v v' = 0
 
        | _ ->
@@ -2355,14 +2366,14 @@ let infer_lit env (L_aux (lit_aux, l) as lit) =
      begin
        match Env.get_default_order env with
        | Ord_aux (Ord_inc, _) | Ord_aux (Ord_dec, _) ->
-          dvector_typ env (nint (String.length str)) (mk_typ (Typ_id (mk_id "bit")))
+          bits_typ env (nint (String.length str))
        | Ord_aux (Ord_var _, _) -> typ_error env l default_order_error_string
      end
   | L_hex str ->
      begin
        match Env.get_default_order env with
        | Ord_aux (Ord_inc, _) | Ord_aux (Ord_dec, _) ->
-          dvector_typ env (nint (String.length str * 4)) (mk_typ (Typ_id (mk_id "bit")))
+          bits_typ env (nint (String.length str * 4))
        | Ord_aux (Ord_var _, _) -> typ_error env l default_order_error_string
      end
   | L_undef -> typ_error env l "Cannot infer the type of undefined"
@@ -2409,16 +2420,41 @@ let instantiate_simple_equations =
        inst_from_eq quants
 in inst_from_eq
 
-let destruct_vec_typ l env typ =
-  let destruct_vec_typ' l = function
+type destructed_vector =
+  | Destruct_vector of nexp * order * typ
+  | Destruct_bitvector of nexp * order
+
+let destruct_any_vector_typ l env typ =
+  let destruct_any_vector_typ' l = function
+    | Typ_aux (Typ_app (id, [A_aux (A_nexp n1, _);
+                             A_aux (A_order o, _)]
+                       ), _) when string_of_id id = "bitvector" -> Destruct_bitvector (n1, o)
     | Typ_aux (Typ_app (id, [A_aux (A_nexp n1, _);
                              A_aux (A_order o, _);
                              A_aux (A_typ vtyp, _)]
-                       ), _) when string_of_id id = "vector" -> (n1, o, vtyp)
+                       ), _) when string_of_id id = "vector" -> Destruct_vector (n1, o, vtyp)
+    | typ -> typ_error env l ("Expected vector or bitvector type, got " ^ string_of_typ typ)
+  in
+  destruct_any_vector_typ' l (Env.expand_synonyms env typ)
+
+let destruct_vector_typ l env typ =
+  let destruct_vector_typ' l = function
+    | Typ_aux (Typ_app (id, [A_aux (A_nexp n1, _);
+                             A_aux (A_order o, _);
+                             A_aux (A_typ vtyp, _)]
+                       ), _) when string_of_id id = "vector" -> n1, o, vtyp
     | typ -> typ_error env l ("Expected vector type, got " ^ string_of_typ typ)
   in
-  destruct_vec_typ' l (Env.expand_synonyms env typ)
+  destruct_vector_typ' l (Env.expand_synonyms env typ)
 
+let destruct_bitvector_typ l env typ =
+  let destruct_bitvector_typ' l = function
+    | Typ_aux (Typ_app (id, [A_aux (A_nexp n1, _);
+                             A_aux (A_order o, _)]
+                       ), _) when string_of_id id = "bitvector" -> n1, o
+    | typ -> typ_error env l ("Expected bitvector type, got " ^ string_of_typ typ)
+  in
+  destruct_bitvector_typ' l (Env.expand_synonyms env typ)
 
 let env_of_annot (l, tannot) = match tannot with
   | Some t -> t.env
@@ -2894,7 +2930,10 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
      let checked_body = crule check_exp env body typ in
      annot_exp (E_internal_plet (tpat, bind_exp, checked_body)) typ
   | E_vector vec, _ ->
-     let (len, ord, vtyp) = destruct_vec_typ l env typ in
+     let len, ord, vtyp = match destruct_any_vector_typ l env typ with
+       | Destruct_vector (len, ord, vtyp) -> len, ord, vtyp
+       | Destruct_bitvector (len, ord) -> len, ord, bit_typ
+     in
      let checked_items = List.map (fun i -> crule check_exp env i vtyp) vec in
      if prove __POS__ env (nc_eq (nint (List.length vec)) (nexp_simp len)) then annot_exp (E_vector checked_items) typ
      else typ_error env l "List length didn't match" (* FIXME: improve error message *)
@@ -3327,8 +3366,9 @@ and infer_pat env (P_aux (pat_aux, (l, ())) as pat) =
      let pats, env, guards = List.fold_left fold_pats ([], env, []) (pat :: pats) in
      let len = nexp_simp (nint (List.length pats)) in
      let etyp = typ_of_pat (List.hd pats) in
+     (* BVS TODO: Non-bitvector P_vector *)
      List.iter (fun pat -> typ_equality l env etyp (typ_of_pat pat)) pats;
-     annot_pat (P_vector pats) (dvector_typ env len etyp), env, guards
+     annot_pat (P_vector pats) (bits_typ env len), env, guards
   | P_vector_concat (pat :: pats) ->
      let fold_pats (pats, env, guards) pat =
        let inferred_pat, env, guards' = infer_pat env pat in
@@ -3336,14 +3376,23 @@ and infer_pat env (P_aux (pat_aux, (l, ())) as pat) =
      in
      let inferred_pats, env, guards =
        List.fold_left fold_pats ([], env, []) (pat :: pats) in
-     let (len, _, vtyp) = destruct_vec_typ l env (typ_of_pat (List.hd inferred_pats)) in
-     let fold_len len pat =
-       let (len', _, vtyp') = destruct_vec_typ l env (typ_of_pat pat) in
-       typ_equality l env vtyp vtyp';
-       nsum len len'
-     in
-     let len = nexp_simp (List.fold_left fold_len len (List.tl inferred_pats)) in
-     annot_pat (P_vector_concat inferred_pats) (dvector_typ env len vtyp), env, guards
+     begin match destruct_any_vector_typ l env (typ_of_pat (List.hd inferred_pats)) with
+     | Destruct_vector (len, _, vtyp) ->
+        let fold_len len pat =
+          let (len', _, vtyp') = destruct_vector_typ l env (typ_of_pat pat) in
+          typ_equality l env vtyp vtyp';
+          nsum len len'
+        in
+        let len = nexp_simp (List.fold_left fold_len len (List.tl inferred_pats)) in
+        annot_pat (P_vector_concat inferred_pats) (dvector_typ env len vtyp), env, guards
+     | Destruct_bitvector (len, _) ->
+        let fold_len len pat =
+          let (len', _) = destruct_bitvector_typ l env (typ_of_pat pat) in
+          nsum len len'
+        in
+        let len = nexp_simp (List.fold_left fold_len len (List.tl inferred_pats)) in
+        annot_pat (P_vector_concat inferred_pats) (bits_typ env len), env, guards
+     end
   | P_string_append pats ->
      let fold_pats (pats, env, guards) pat =
        let inferred_pat, env, guards' = infer_pat env pat in
@@ -3545,8 +3594,7 @@ and infer_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) =
        let inferred_v_lexp = infer_lexp env v_lexp in
        let (Typ_aux (v_typ_aux, _) as v_typ) = Env.expand_synonyms env (lexp_typ_of inferred_v_lexp) in
        match v_typ_aux with
-       | Typ_app (id, [A_aux (A_nexp len, _); A_aux (A_order ord, _); A_aux (A_typ elem_typ, _)])
-            when Id.compare id (mk_id "vector") = 0 ->
+       | Typ_app (id, [A_aux (A_nexp len, _); A_aux (A_order ord, _)]) when Id.compare id (mk_id "bitvector") = 0 ->
           let inferred_exp1 = infer_exp env exp1 in
           let inferred_exp2 = infer_exp env exp2 in
           let nexp1, env = bind_numeric l (typ_of inferred_exp1) env in
@@ -3554,10 +3602,10 @@ and infer_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) =
           begin match ord with
           | Ord_aux (Ord_inc, _) when !opt_no_lexp_bounds_check || prove __POS__ env (nc_lteq nexp1 nexp2) ->
              let len = nexp_simp (nsum (nminus nexp2 nexp1) (nint 1)) in
-             annot_lexp (LEXP_vector_range (inferred_v_lexp, inferred_exp1, inferred_exp2)) (vector_typ len ord elem_typ)
+             annot_lexp (LEXP_vector_range (inferred_v_lexp, inferred_exp1, inferred_exp2)) (bitvector_typ len ord)
           | Ord_aux (Ord_dec, _) when !opt_no_lexp_bounds_check || prove __POS__ env (nc_gteq nexp1 nexp2) ->
              let len = nexp_simp (nsum (nminus nexp1 nexp2) (nint 1)) in
-             annot_lexp (LEXP_vector_range (inferred_v_lexp, inferred_exp1, inferred_exp2)) (vector_typ len ord elem_typ)
+             annot_lexp (LEXP_vector_range (inferred_v_lexp, inferred_exp1, inferred_exp2)) (bitvector_typ len ord)
           | _ -> typ_error env l ("Could not infer length of vector slice assignment " ^ string_of_lexp lexp)
           end
        | _ -> typ_error env l "Cannot assign slice of non vector type"
@@ -3575,12 +3623,20 @@ and infer_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) =
             annot_lexp (LEXP_vector (inferred_v_lexp, inferred_exp)) elem_typ
           else
             typ_error env l ("Vector assignment not provably in bounds " ^ string_of_lexp lexp)
+       | Typ_app (id, [A_aux (A_nexp len, _); A_aux (A_order ord, _)])
+            when Id.compare id (mk_id "bitvector") = 0 ->
+          let inferred_exp = infer_exp env exp in
+          let nexp, env = bind_numeric l (typ_of inferred_exp) env in
+          if !opt_no_lexp_bounds_check || prove __POS__ env (nc_and (nc_lteq (nint 0) nexp) (nc_lteq nexp (nexp_simp (nminus len (nint 1))))) then
+            annot_lexp (LEXP_vector (inferred_v_lexp, inferred_exp)) bit_typ
+          else
+            typ_error env l ("Vector assignment not provably in bounds " ^ string_of_lexp lexp)
        | _ -> typ_error env l "Cannot assign vector element of non vector type"
      end
   | LEXP_vector_concat [] -> typ_error env l "Cannot have empty vector concatenation l-expression"
   | LEXP_vector_concat (v_lexp :: v_lexps) ->
      begin
-       let sum_lengths first_ord first_elem_typ acc (Typ_aux (v_typ_aux, _) as v_typ) =
+       let sum_vector_lengths first_ord first_elem_typ acc (Typ_aux (v_typ_aux, _) as v_typ) =
          match v_typ_aux with
          | Typ_app (id, [A_aux (A_nexp len, _); A_aux (A_order ord, _); A_aux (A_typ elem_typ, _)])
               when Id.compare id (mk_id "vector") = 0 && ord_identical ord first_ord ->
@@ -3588,6 +3644,13 @@ and infer_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) =
             nsum acc len
          | _ -> typ_error env l "Vector concatentation l-expression must only contain vector types of the same order"
        in
+       let sum_bitvector_lengths first_ord acc (Typ_aux (v_typ_aux, _) as v_typ) =
+         match v_typ_aux with
+         | Typ_app (id, [A_aux (A_nexp len, _); A_aux (A_order ord, _)])
+              when Id.compare id (mk_id "bitvector") = 0 && ord_identical ord first_ord ->
+            nsum acc len
+         | _ -> typ_error env l "Bitvector concatentation l-expression must only contain bitvector types of the same order"
+       in
        let inferred_v_lexp = infer_lexp env v_lexp in
        let inferred_v_lexps = List.map (infer_lexp env) v_lexps in
        let (Typ_aux (v_typ_aux, _) as v_typ) = Env.expand_synonyms env (lexp_typ_of inferred_v_lexp) in
@@ -3595,9 +3658,13 @@ and infer_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) =
        match v_typ_aux with
        | Typ_app (id, [A_aux (A_nexp len, _); A_aux (A_order ord, _); A_aux (A_typ elem_typ, _)])
             when Id.compare id (mk_id "vector") = 0 ->
-          let len = List.fold_left (sum_lengths ord elem_typ) len v_typs in
+          let len = List.fold_left (sum_vector_lengths ord elem_typ) len v_typs in
           annot_lexp (LEXP_vector_concat (inferred_v_lexp :: inferred_v_lexps)) (vector_typ (nexp_simp len) ord elem_typ)
-       | _ -> typ_error env l ("Vector concatentation l-expression must only contain vector types, found " ^ string_of_typ v_typ)
+       | Typ_app (id, [A_aux (A_nexp len, _); A_aux (A_order ord, _)])
+            when Id.compare id (mk_id "bitvector") = 0 ->
+          let len = List.fold_left (sum_bitvector_lengths ord) len v_typs in
+          annot_lexp (LEXP_vector_concat (inferred_v_lexp :: inferred_v_lexps)) (bitvector_typ (nexp_simp len) ord)
+       | _ -> typ_error env l ("Vector concatentation l-expression must only contain bitvector or vector types, found " ^ string_of_typ v_typ)
      end
   | LEXP_field (LEXP_aux (LEXP_id v, _), fid) ->
      (* FIXME: will only work for ASL *)
@@ -3795,8 +3862,14 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
   | E_vector ((item :: items) as vec) ->
      let inferred_item = irule infer_exp env item in
      let checked_items = List.map (fun i -> crule check_exp env i (typ_of inferred_item)) items in
-     let vec_typ = dvector_typ env (nint (List.length vec)) (typ_of inferred_item) in
-     annot_exp (E_vector (inferred_item :: checked_items)) vec_typ
+     begin match typ_of inferred_item with
+     | Typ_aux (Typ_id id, _) when string_of_id id = "bit" ->
+        let bitvec_typ = bits_typ env (nint (List.length vec)) in
+        annot_exp (E_vector (inferred_item :: checked_items)) bitvec_typ
+     | _ ->
+        let vec_typ = dvector_typ env (nint (List.length vec)) (typ_of inferred_item) in
+        annot_exp (E_vector (inferred_item :: checked_items)) vec_typ
+     end
   | E_assert (test, msg) ->
      let msg = assert_msg msg in
      let checked_test = crule check_exp env test bool_typ in
@@ -4255,14 +4328,23 @@ and infer_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat)
      if allow_unknown && List.exists (fun mpat -> is_unknown_type (typ_of_mpat mpat)) inferred_mpats then
        annot_mpat (MP_vector_concat inferred_mpats) unknown_typ, env, guards (* hack *)
      else
-       let (len, _, vtyp) = destruct_vec_typ l env (typ_of_mpat (List.hd inferred_mpats)) in
-       let fold_len len mpat =
-         let (len', _, vtyp') = destruct_vec_typ l env (typ_of_mpat mpat) in
-         typ_equality l env vtyp vtyp';
-         nsum len len'
-       in
-       let len = nexp_simp (List.fold_left fold_len len (List.tl inferred_mpats)) in
-       annot_mpat (MP_vector_concat inferred_mpats) (dvector_typ env len vtyp), env, guards
+       begin match destruct_any_vector_typ l env (typ_of_mpat (List.hd inferred_mpats)) with
+       | Destruct_vector (len, _, vtyp) ->
+          let fold_len len mpat =
+            let (len', _, vtyp') = destruct_vector_typ l env (typ_of_mpat mpat) in
+            typ_equality l env vtyp vtyp';
+            nsum len len'
+          in
+          let len = nexp_simp (List.fold_left fold_len len (List.tl inferred_mpats)) in
+          annot_mpat (MP_vector_concat inferred_mpats) (dvector_typ env len vtyp), env, guards
+       | Destruct_bitvector (len, _) ->
+          let fold_len len mpat =
+            let (len', _) = destruct_bitvector_typ l env (typ_of_mpat mpat) in
+            nsum len len'
+          in
+          let len = nexp_simp (List.fold_left fold_len len (List.tl inferred_mpats)) in
+          annot_mpat (MP_vector_concat inferred_mpats) (bits_typ env len), env, guards
+       end
   | MP_string_append mpats ->
      let fold_pats (pats, env, guards) pat =
        let inferred_pat, env, guards' = infer_mpat allow_unknown other_env env pat in
@@ -4988,9 +5070,8 @@ let rec check_typedef : 'a. Env.t -> 'a type_def -> (tannot def) list * Env.t =
        match typ with
        (* The type of a bitfield must be a constant-width bitvector *)
        | Typ_aux (Typ_app (v, [A_aux (A_nexp (Nexp_aux (Nexp_constant size, _)), _);
-                               A_aux (A_order order, _);
-                               A_aux (A_typ (Typ_aux (Typ_id b, _)), _)]), _)
-            when string_of_id v = "vector" && string_of_id b = "bit" ->
+                               A_aux (A_order order, _)]), _)
+            when string_of_id v = "bitvector" ->
           let size = Big_int.to_int size in
           let eval_index_nexp env nexp =
             int_of_nexp_opt (nexp_simp (Env.expand_nexp_synonyms env nexp)) in
diff --git a/src/type_check.mli b/src/type_check.mli
index dcedcc90..711f2411 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -398,6 +398,7 @@ val destruct_range : Env.t -> typ -> (kid list * n_constraint * nexp * nexp) opt
 val destruct_numeric : ?name:string option -> typ -> (kid list * n_constraint * nexp) option
 
 val destruct_vector : Env.t -> typ -> (nexp * order * typ) option
+val destruct_bitvector : Env.t -> typ -> (nexp * order) option
 
 (** Construct an existential type with a guaranteed fresh
    identifier. *)
diff --git a/test/c/bitvector.sail b/test/c/bitvector.sail
index 8a80234e..ba23b2cc 100644
--- a/test/c/bitvector.sail
+++ b/test/c/bitvector.sail
@@ -2,7 +2,7 @@ default Order dec
 
 $include <vector_dec.sail>
 
-val test : (vector(16, dec, bit), vector(200, dec, bit)) -> bool
+val test : (bitvector(16, dec), bitvector(200, dec)) -> bool
 
 function test (x, y)  = {
   print_bits("x = ", x);
diff --git a/test/c/bv_literal.sail b/test/c/bv_literal.sail
index 1955b5dd..73f1133c 100644
--- a/test/c/bv_literal.sail
+++ b/test/c/bv_literal.sail
@@ -1,12 +1,12 @@
 
 default Order dec
 
-val "print_bits" : forall 'n. (string, vector('n, dec, bit)) -> unit
+val "print_bits" : forall 'n. (string, bitvector('n, dec)) -> unit
 
 val main : unit -> unit
 
 function main () = {
   let x : bit = bitone;
-  let y : vector(4, dec, bit) = [x, bitone, bitzero, x];
+  let y : bitvector(4, dec) = [x, bitone, bitzero, x];
   print_bits("y = ", y);
 }
\ No newline at end of file
diff --git a/test/c/eq_struct.sail b/test/c/eq_struct.sail
index 9da12aae..2f6d4453 100644
--- a/test/c/eq_struct.sail
+++ b/test/c/eq_struct.sail
@@ -17,7 +17,7 @@ function neq(x, y) = ~(eq(x, y))
 
 struct S = {
   field1: int,
-  field2: vector(8, dec, bit)
+  field2: bitvector(8, dec)
 }
 
 val "print" : string -> unit
diff --git a/test/c/gvector.sail b/test/c/gvector.sail
index 3e452985..3d6e2bef 100644
--- a/test/c/gvector.sail
+++ b/test/c/gvector.sail
@@ -5,7 +5,7 @@ $include <vector_dec.sail>
 
 val "print_int" : (string, int) -> unit
 
-register R : vector(32, dec, vector(32, dec, bit))
+register R : vector(32, dec, bitvector(32, dec))
 
 register T : vector(32, dec, int)
 
diff --git a/test/c/option.sail b/test/c/option.sail
index aedde8ef..8041e8aa 100644
--- a/test/c/option.sail
+++ b/test/c/option.sail
@@ -5,7 +5,7 @@ $include <flow.sail>
 val print = "print_endline" : string -> unit
 
 val "print_int" : (string, int) -> unit
-val "print_bits" : forall 'n. (string, vector('n, dec, bit)) -> unit
+val "print_bits" : forall 'n. (string, bitvector('n, dec)) -> unit
 
 union option ('a : Type) = {
   None : unit,
@@ -22,7 +22,7 @@ val main : unit -> unit
 function main () = {
   let x : option(int) = Some(5);
   let y : option(int) = None();
-  let z : option(vector(4, dec, bit)) = Some(0xF);
+  let z : option(bitvector(4, dec)) = Some(0xF);
 
   match x {
     Some(a) => print_int("a = ", 5),
@@ -34,7 +34,7 @@ function main () = {
     None()  => print("None")
   };
 
-  let q : soption(vector(4, dec, bit)) = sSome(0xA);
+  let q : soption(bitvector(4, dec)) = sSome(0xA);
 
   match q {
     sSome(c) => print_bits("c = ", c)
diff --git a/test/c/pattern_concat_nest.sail b/test/c/pattern_concat_nest.sail
index 92150e66..df588662 100644
--- a/test/c/pattern_concat_nest.sail
+++ b/test/c/pattern_concat_nest.sail
@@ -1,5 +1,6 @@
 default Order dec
-type bits ('n : Int) = vector('n, dec, bit)
+
+type bits ('n : Int) = bitvector('n, dec)
 
 union option ('a : Type) = {None : unit, Some : 'a}
 
diff --git a/test/c/stack_struct.sail b/test/c/stack_struct.sail
index c5c79a81..5dd0caeb 100644
--- a/test/c/stack_struct.sail
+++ b/test/c/stack_struct.sail
@@ -1,6 +1,6 @@
 default Order dec
 
-type bits ('n : Int) = vector('n, dec, bit)
+type bits ('n : Int) = bitvector('n, dec)
 
 union option ('a : Type) = {
   Some : 'a,
diff --git a/test/c/struct.sail b/test/c/struct.sail
index f3f2b071..21484c6a 100644
--- a/test/c/struct.sail
+++ b/test/c/struct.sail
@@ -1,10 +1,10 @@
 default Order dec
 
-val "print_bits" : forall 'n. (string, vector('n, dec, bit)) -> unit
+val "print_bits" : forall 'n. (string, bitvector('n, dec)) -> unit
 
 struct test = {
-  A : vector(4, dec, bit),
-  B : vector(2, dec, bit),
+  A : bitvector(4, dec),
+  B : bitvector(2, dec),
 }
 
 function main (() : unit) -> unit = {
diff --git a/test/smt/clear_overflow_regression.unsat.sail b/test/smt/clear_overflow_regression.unsat.sail
index b10d7531..272d4be6 100644
--- a/test/smt/clear_overflow_regression.unsat.sail
+++ b/test/smt/clear_overflow_regression.unsat.sail
@@ -1,8 +1,8 @@
+default Order dec
+
 $include <arith.sail>
 $include <vector_dec.sail>
 
-default Order dec
-
 infix 1 >>
 infix 1 <<
 overload operator - = {sub_bits}
diff --git a/test/smt/gvector.unsat.sail b/test/smt/gvector.unsat.sail
index 23054765..af287608 100644
--- a/test/smt/gvector.unsat.sail
+++ b/test/smt/gvector.unsat.sail
@@ -2,7 +2,7 @@ default Order dec
 
 $include <prelude.sail>
 
-register R : vector(32, dec, vector(32, dec, bit))
+register R : vector(32, dec, bitvector(32, dec))
 
 type is_reg('n: Int) -> Bool = 0 <= 'n <= 31
 
@@ -12,4 +12,4 @@ function prop forall 'n, is_reg('n). (n: int('n)) -> bool = {
     R[i] = 0xDEAD_BEEF;
   };
   R[n] == 0xDEAD_BEEF
-}
\ No newline at end of file
+}
diff --git a/test/smt/gvector_trivial.unsat.sail b/test/smt/gvector_trivial.unsat.sail
index 37a4fbed..5aad74d1 100644
--- a/test/smt/gvector_trivial.unsat.sail
+++ b/test/smt/gvector_trivial.unsat.sail
@@ -2,7 +2,7 @@ default Order dec
 
 $include <prelude.sail>
 
-register R : vector(32, dec, vector(32, dec, bit))
+register R : vector(32, dec, bitvector(32, dec))
 
 $property
 function prop() -> bool = {
diff --git a/test/typecheck/pass/Replicate/v1.expect b/test/typecheck/pass/Replicate/v1.expect
index c40aa5ec..5c52861f 100644
--- a/test/typecheck/pass/Replicate/v1.expect
+++ b/test/typecheck/pass/Replicate/v1.expect
@@ -2,7 +2,7 @@ Type error:
 [Replicate/v1.sail]:14:4-30
 14 |    replicate_bits(x, 'N / 'M)
    |    ^------------------------^
-   | Tried performing type coercion from vector(('M * div('N, 'M)), dec, bit) to vector('N, dec, bit) on replicate_bits(x, ediv_int(__id(N), bitvector_length(x)))
+   | Tried performing type coercion from bitvector(('M * div('N, 'M)), dec) to bitvector('N, dec) on replicate_bits(x, ediv_int(__id(N), bitvector_length(x)))
    | Coercion failed because:
    | Mismatched argument types in subtype check
    | 
diff --git a/test/typecheck/pass/Replicate/v2.expect b/test/typecheck/pass/Replicate/v2.expect
index acadd4e2..7d4891f9 100644
--- a/test/typecheck/pass/Replicate/v2.expect
+++ b/test/typecheck/pass/Replicate/v2.expect
@@ -2,7 +2,7 @@ Type error:
 [Replicate/v2.sail]:13:4-30
 13 |    replicate_bits(x, 'N / 'M)
    |    ^------------------------^
-   | Tried performing type coercion from {('ex119# : Int), true. vector(('M * 'ex119#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, tdiv_int(__id(N), bitvector_length(x)))
+   | Tried performing type coercion from {('ex128# : Int), true. bitvector(('M * 'ex128#), dec)} to bitvector('N, dec) on replicate_bits(x, tdiv_int(__id(N), bitvector_length(x)))
    | Coercion failed because:
    | Mismatched argument types in subtype check
    | 
diff --git a/test/typecheck/pass/add_vec_lit.sail b/test/typecheck/pass/add_vec_lit.sail
index 7e5c873a..cf29212f 100644
--- a/test/typecheck/pass/add_vec_lit.sail
+++ b/test/typecheck/pass/add_vec_lit.sail
@@ -1,13 +1,13 @@
 default Order inc
 
 val add_vec = {ocaml: "add_vec", lem: "add_vec"}: forall ('n : Int).
-  (vector('n, inc, bit), vector('n, inc, bit)) -> vector('n, inc, bit)
+  (bitvector('n, inc), bitvector('n, inc)) -> bitvector('n, inc)
 
 val add_range = {ocaml: "add_range", lem: "add_range"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
   (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p)
 
 val cast unsigned : forall ('n : Int).
-  vector('n, inc, bit) -> range(0, 2 ^ 'n - 1)
+  bitvector('n, inc) -> range(0, 2 ^ 'n - 1)
 
 overload operator + = {add_vec, add_range}
 
diff --git a/test/typecheck/pass/arm_FPEXC1.sail b/test/typecheck/pass/arm_FPEXC1.sail
index 2021bf67..3f4b8632 100644
--- a/test/typecheck/pass/arm_FPEXC1.sail
+++ b/test/typecheck/pass/arm_FPEXC1.sail
@@ -1,17 +1,17 @@
 default Order dec
 
 val vector_access = {ocaml: "access", lem: "access_vec_dec", coq: "access_vec_dec"}: forall ('n : Int).
-  (vector('n, dec, bit), int) -> bit
+  (bitvector('n, dec), int) -> bit
 
 val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec", coq: "subrange_vec_dec"}: forall ('n : Int) ('m : Int) ('o : Int), 'm >= 'o & 'o >= 0 & 'n >= 'm + 1.
-  (vector('n, dec, bit), atom('m), atom('o)) -> vector('m - ('o - 1), dec, bit)
+  (bitvector('n, dec), atom('m), atom('o)) -> bitvector('m - ('o - 1), dec)
 
 val vector_update_subrange = {ocaml: "update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o.
-  (vector('n, dec, bit), atom('m), atom('o), vector('m - ('o - 1), dec, bit)) -> vector('n, dec, bit)
+  (bitvector('n, dec), atom('m), atom('o), bitvector('m - ('o - 1), dec)) -> bitvector('n, dec)
 
-register _FPEXC32_EL2 : vector(32, dec, bit)
+register _FPEXC32_EL2 : bitvector(32, dec)
 
-val set_FPEXC32_EL2 : vector(32, dec, bit) -> unit effect {wreg}
+val set_FPEXC32_EL2 : bitvector(32, dec) -> unit effect {wreg}
 
 function set_FPEXC32_EL2 value_name = {
   _FPEXC32_EL2[0 .. 0] = [value_name[0]];
@@ -26,10 +26,10 @@ function set_FPEXC32_EL2 value_name = {
   _FPEXC32_EL2[30 .. 30] = [value_name[30]]
 }
 
-val get_FPEXC32_EL2 : unit -> vector(32, dec, bit) effect {rreg}
+val get_FPEXC32_EL2 : unit -> bitvector(32, dec) effect {rreg}
 
 function get_FPEXC32_EL2 () = {
-  value_name : vector(32, dec, bit) = 0x04000700;
+  value_name : bitvector(32, dec) = 0x04000700;
   value_name[0 .. 0] = [_FPEXC32_EL2[0]];
   value_name[1 .. 1] = [_FPEXC32_EL2[1]];
   value_name[2 .. 2] = [_FPEXC32_EL2[2]];
@@ -44,11 +44,11 @@ function get_FPEXC32_EL2 () = {
   value_name
 }
 
-val set_FPEXC : vector(32, dec, bit) -> unit effect {rreg, wreg}
+val set_FPEXC : bitvector(32, dec) -> unit effect {rreg, wreg}
 
 function set_FPEXC val_name = {
-  r : vector(32, dec, bit) = val_name;
-  __tmp_45 : vector(32, dec, bit) = get_FPEXC32_EL2();
+  r : bitvector(32, dec) = val_name;
+  __tmp_45 : bitvector(32, dec) = get_FPEXC32_EL2();
   __tmp_45[31 .. 0] = r;
   set_FPEXC32_EL2(__tmp_45)
 }
diff --git a/test/typecheck/pass/bitfield_pc.sail b/test/typecheck/pass/bitfield_pc.sail
index 9764289a..889e27ce 100644
--- a/test/typecheck/pass/bitfield_pc.sail
+++ b/test/typecheck/pass/bitfield_pc.sail
@@ -1,6 +1,8 @@
+default Order dec
+
 $include <vector_dec.sail>
 
-bitfield PC_t : vector(16, dec, bit) = {
+bitfield PC_t : bitvector(16, dec) = {
   H : 15 .. 8,
   L :  7 .. 0
 }
diff --git a/test/typecheck/pass/bitvector_param.sail b/test/typecheck/pass/bitvector_param.sail
index 77fe7dc3..784a77f9 100644
--- a/test/typecheck/pass/bitvector_param.sail
+++ b/test/typecheck/pass/bitvector_param.sail
@@ -1,32 +1,7 @@
 default Order dec
 
 $include <flow.sail>
-
-type bits ('n : Int) = vector('n, dec, bit)
-
-val vector_subrange = {
-  ocaml: "subrange",
-  lem: "subrange_vec_dec",
-  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)
-
-val vector_update_subrange_dec = {ocaml: "update_subrange", c: "vector_update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o.
-  (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
-
-val vector_update_subrange_inc = {ocaml: "update_subrange", lem: "update_subrange_vec_inc"} : forall 'n 'm 'o.
-  (vector('n, inc, bit), atom('m), atom('o), vector('o - ('m - 1), inc, bit)) -> vector('n, inc, bit)
-
-overload vector_update_subrange = {vector_update_subrange_dec, vector_update_subrange_inc}
-
-val bitvector_concat = {c: "append", ocaml: "append", lem: "concat_vec", coq: "concat_vec"} : forall ('n : Int) ('m : Int).
-  (bits('n), bits('m)) -> bits('n + 'm)
-
-val vector_concat = {ocaml: "append", lem: "append_list"} : forall ('n : Int) ('m : Int) ('a : Type).
-  (vector('n, dec, 'a), vector('m, dec, 'a)) -> vector('n + 'm, dec, 'a)
-
-overload append = {bitvector_concat, vector_concat}
+$include <vector_dec.sail>
 
 type xlen : Int = 64
 type ylen : Int = 1
diff --git a/test/typecheck/pass/decode_patterns.sail b/test/typecheck/pass/decode_patterns.sail
index d54e9416..6f28ec18 100644
--- a/test/typecheck/pass/decode_patterns.sail
+++ b/test/typecheck/pass/decode_patterns.sail
@@ -2,7 +2,7 @@ default Order dec
 
 $include <prelude.sail>
 
-val decode : vector(16, dec, bit) -> unit
+val decode : bitvector(16, dec) -> unit
 
 scattered function decode
 
@@ -22,11 +22,11 @@ function clause decode 0x00 @ 0b001 @ [b : bit] @ 0x0 =
 
 end decode
 
-val decode2 : vector(16, dec, bit) -> unit
+val decode2 : bitvector(16, dec) -> unit
 
 function decode2 x =
   match x {
-    0x00 @ 0b000 @ [b : bit]  @ 0x0 =>
+    0x00 @ 0b000 @ [b : bit] @ 0x0 =>
       if b == bitone then {
         ()
       } else {
diff --git a/test/typecheck/pass/exist_tlb.sail b/test/typecheck/pass/exist_tlb.sail
index de15edf8..1d0e1d20 100644
--- a/test/typecheck/pass/exist_tlb.sail
+++ b/test/typecheck/pass/exist_tlb.sail
@@ -1,17 +1,17 @@
 $include <flow.sail>
 
 val extz : forall ('n : Int) ('m : Int) ('ord : Order).
-  vector('n, 'ord, bit) -> vector('m, 'ord, bit)
+  bitvector('n, 'ord) -> bitvector('m, 'ord)
 
 val exts : forall ('n : Int) ('m : Int) ('ord : Order).
-  vector('n, 'ord, bit) -> vector('m, 'ord, bit)
+  bitvector('n, 'ord) -> bitvector('m, 'ord)
 
 overload EXTZ = {extz}
 
 overload EXTS = {exts}
 
 val add_vec : forall ('n : Int) ('ord : Order).
-  (vector('n, 'ord, bit), vector('n, 'ord, bit)) -> vector('n, 'ord, bit)
+  (bitvector('n, 'ord), bitvector('n, 'ord)) -> bitvector('n, 'ord)
 
 overload operator + = {add_vec}
 
@@ -21,15 +21,15 @@ overload ~ = {bool_not}
 
 default Order dec
 
-register CP0LLBit : vector(1, dec, bit)
+register CP0LLBit : bitvector(1, dec)
 
-register CP0LLAddr : vector(64, dec, bit)
+register CP0LLAddr : bitvector(64, dec)
 
 enum MemAccessType = {Instruction, LoadData, StoreData}
 
-type regno = vector(5, dec, bit)
+type regno = bitvector(5, dec)
 
-type imm16 = vector(16, dec, bit)
+type imm16 = bitvector(16, dec)
 
 enum Exception = {
   EInt,
@@ -55,12 +55,12 @@ enum Exception = {
 
 enum WordType = {B, H, W, D}
 
-val rGPR : vector(5, dec, bit) -> vector(64, dec, bit) effect {rreg}
+val rGPR : bitvector(5, dec) -> bitvector(64, dec) effect {rreg}
 
-val isAddressAligned : (vector(64, dec, bit), WordType) -> bool
+val isAddressAligned : (bitvector(64, dec), WordType) -> bool
 
 val SignalExceptionBadAddr : forall ('o : Type).
-  (Exception, vector(64, dec, bit)) -> 'o
+  (Exception, bitvector(64, dec)) -> 'o
 
 val wordWidthBytes : WordType -> {|1, 2, 4, 8|}
 
@@ -72,29 +72,29 @@ function wordWidthBytes w = match w {
 }
 
 val MEMr_reserve_wrapper : forall ('n : Int).
-  (vector(64, dec, bit), atom('n)) -> vector(8 * 'n, dec, bit) effect {rmem}
+  (bitvector(64, dec), atom('n)) -> bitvector(8 * 'n, dec) effect {rmem}
 
 val MEMr_wrapper : forall ('n : Int).
-  (vector(64, dec, bit), atom('n)) -> vector(8 * 'n, dec, bit) effect {rmem}
+  (bitvector(64, dec), atom('n)) -> bitvector(8 * 'n, dec) effect {rmem}
 
-val wGPR : (vector(5, dec, bit), vector(64, dec, bit)) -> unit effect {wreg}
+val wGPR : (bitvector(5, dec), bitvector(64, dec)) -> unit effect {wreg}
 
-val addrWrapper : (vector(64, dec, bit), MemAccessType, WordType) -> vector(64, dec, bit)
+val addrWrapper : (bitvector(64, dec), MemAccessType, WordType) -> bitvector(64, dec)
 
-function addrWrapper (addr : vector(64, dec, bit), accessType : MemAccessType, width : WordType) = addr
+function addrWrapper (addr : bitvector(64, dec), accessType : MemAccessType, width : WordType) = addr
 
-val TLBTranslate : (vector(64, dec, bit), MemAccessType) -> vector(64, dec, bit)
+val TLBTranslate : (bitvector(64, dec), MemAccessType) -> bitvector(64, dec)
 
-function TLBTranslate (vAddr : vector(64, dec, bit), accessType : MemAccessType) = vAddr
+function TLBTranslate (vAddr : bitvector(64, dec), accessType : MemAccessType) = vAddr
 
 union ast = {Load : (WordType, bool, bool, regno, regno, imm16)}
 
 val execute : ast -> unit effect {rmem, rreg, wreg}
 
 function execute Load(width, signed, linked, base, rt, offset) = {
-  vAddr : vector(64, dec, bit) = addrWrapper(EXTS(offset) + rGPR(base), LoadData, width);
+  vAddr : bitvector(64, dec) = addrWrapper(EXTS(offset) + rGPR(base), LoadData, width);
   if ~(isAddressAligned(vAddr, width)) then SignalExceptionBadAddr(AdEL, vAddr) else let pAddr = TLBTranslate(vAddr, LoadData) in {
-    memResult : {'t, 't in {1, 2, 4, 8}. vector(8 * 't, dec, bit)} = if linked then {
+    memResult : {'t, 't in {1, 2, 4, 8}. bitvector(8 * 't, dec)} = if linked then {
       CP0LLBit = 0b1;
       CP0LLAddr = pAddr;
       MEMr_reserve_wrapper(pAddr, wordWidthBytes(width))
diff --git a/test/typecheck/pass/existential_ast/v3.expect b/test/typecheck/pass/existential_ast/v3.expect
index 7bb8a4ab..78711c2b 100644
--- a/test/typecheck/pass/existential_ast/v3.expect
+++ b/test/typecheck/pass/existential_ast/v3.expect
@@ -3,5 +3,5 @@ Type error:
 26 |  Some(Ctor1(a, x, c))
    |       ^------------^
    | Could not resolve quantifiers for Ctor1
-   | * datasize('ex196#)
+   | * datasize('ex205#)
    | 
diff --git a/test/typecheck/pass/existential_ast3/v1.expect b/test/typecheck/pass/existential_ast3/v1.expect
index 4b9bd7cc..40657d0c 100644
--- a/test/typecheck/pass/existential_ast3/v1.expect
+++ b/test/typecheck/pass/existential_ast3/v1.expect
@@ -4,17 +4,17 @@ Type error:
    |                                                ^---------------^
    | Tried performing type coercion from (int(33), range(0, (2 ^ 5 - 1))) to {('d : Int) ('n : Int), (datasize('d) & (0 <= 'n & ('n + 1) <= 'd)). (int('d), int('n))} on (33, unsigned(a))
    | Coercion failed because:
-   | (int(33), int('ex158#)) is not a subtype of (int('ex153#), int('ex154#))
+   | (int(33), int('ex167#)) is not a subtype of (int('ex162#), int('ex163#))
    | [existential_ast3/v1.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex153# bound here
+   |    | 'ex162# bound here
    | [existential_ast3/v1.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex154# bound here
+   |    | 'ex163# bound here
    | [existential_ast3/v1.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex158# bound here
+   |    | 'ex167# bound here
    | 
diff --git a/test/typecheck/pass/existential_ast3/v2.expect b/test/typecheck/pass/existential_ast3/v2.expect
index 52eb2f13..8954736e 100644
--- a/test/typecheck/pass/existential_ast3/v2.expect
+++ b/test/typecheck/pass/existential_ast3/v2.expect
@@ -4,17 +4,17 @@ Type error:
    |                                                ^---------------^
    | Tried performing type coercion from (int(31), range(0, (2 ^ 5 - 1))) to {('d : Int) ('n : Int), (datasize('d) & (0 <= 'n & ('n + 1) <= 'd)). (int('d), int('n))} on (31, unsigned(a))
    | Coercion failed because:
-   | (int(31), int('ex158#)) is not a subtype of (int('ex153#), int('ex154#))
+   | (int(31), int('ex167#)) is not a subtype of (int('ex162#), int('ex163#))
    | [existential_ast3/v2.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex153# bound here
+   |    | 'ex162# bound here
    | [existential_ast3/v2.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex154# bound here
+   |    | 'ex163# bound here
    | [existential_ast3/v2.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex158# bound here
+   |    | 'ex167# bound here
    | 
diff --git a/test/typecheck/pass/existential_ast3/v3.expect b/test/typecheck/pass/existential_ast3/v3.expect
index 0e43cd52..d0fcdc06 100644
--- a/test/typecheck/pass/existential_ast3/v3.expect
+++ b/test/typecheck/pass/existential_ast3/v3.expect
@@ -3,5 +3,5 @@ Type error:
 25 |    Some(Ctor(64, unsigned(0b0 @ b @ a)))
    |         ^-----------------------------^
    | Could not resolve quantifiers for Ctor
-   | * (datasize(64) & (0 <= 'ex197# & ('ex197# + 1) <= 64))
+   | * (datasize(64) & (0 <= 'ex206# & ('ex206# + 1) <= 64))
    | 
diff --git a/test/typecheck/pass/if_infer/v1.expect b/test/typecheck/pass/if_infer/v1.expect
index 011ecbdf..e236d4b6 100644
--- a/test/typecheck/pass/if_infer/v1.expect
+++ b/test/typecheck/pass/if_infer/v1.expect
@@ -5,8 +5,7 @@ Type error:
    | No overloading for vector_access, tried:
    | * bitvector_access
    |    Could not resolve quantifiers for bitvector_access
-   |    * (0 <= 'ex115# & ('ex115# + 1) <= 3)
+   |    * (0 <= 'ex124# & ('ex124# + 1) <= 3)
    | * plain_vector_access
-   |    Could not resolve quantifiers for plain_vector_access
-   |    * (0 <= 'ex118# & ('ex118# + 1) <= 3)
+   |    No valid casts resulted in unification
    | 
diff --git a/test/typecheck/pass/if_infer/v2.expect b/test/typecheck/pass/if_infer/v2.expect
index 9a34f688..fa7fb9ff 100644
--- a/test/typecheck/pass/if_infer/v2.expect
+++ b/test/typecheck/pass/if_infer/v2.expect
@@ -5,8 +5,7 @@ Type error:
    | No overloading for vector_access, tried:
    | * bitvector_access
    |    Could not resolve quantifiers for bitvector_access
-   |    * (0 <= 'ex115# & ('ex115# + 1) <= 4)
+   |    * (0 <= 'ex124# & ('ex124# + 1) <= 4)
    | * plain_vector_access
-   |    Could not resolve quantifiers for plain_vector_access
-   |    * (0 <= 'ex118# & ('ex118# + 1) <= 4)
+   |    No valid casts resulted in unification
    | 
diff --git a/test/typecheck/pass/if_infer/v3.expect b/test/typecheck/pass/if_infer/v3.expect
index 7e0e74bb..b7447d0f 100644
--- a/test/typecheck/pass/if_infer/v3.expect
+++ b/test/typecheck/pass/if_infer/v3.expect
@@ -6,5 +6,5 @@ Type error:
    | * bitvector_access
    |    Numeric type is non-simple
    | * plain_vector_access
-   |    Numeric type is non-simple
+   |    No valid casts resulted in unification
    | 
diff --git a/test/typecheck/pass/nexp_synonym/v1.expect b/test/typecheck/pass/nexp_synonym/v1.expect
index 9ba21c2c..2f547747 100644
--- a/test/typecheck/pass/nexp_synonym/v1.expect
+++ b/test/typecheck/pass/nexp_synonym/v1.expect
@@ -2,7 +2,7 @@ Type error:
 [nexp_synonym/v1.sail]:7:20-31
 7 |let v : bits(LEN) = 0xFFFF_FFFF
   |                    ^---------^
-  | Tried performing type coercion from vector(32, dec, bit) to bits(LEN) on 0xFFFFFFFF
+  | Tried performing type coercion from bitvector(32, dec) to bits(LEN) on 0xFFFFFFFF
   | Coercion failed because:
   | Mismatched argument types in subtype check
   | 
diff --git a/test/typecheck/pass/nexp_synonym/v2.expect b/test/typecheck/pass/nexp_synonym/v2.expect
index 68d664f7..c4bd774c 100644
--- a/test/typecheck/pass/nexp_synonym/v2.expect
+++ b/test/typecheck/pass/nexp_synonym/v2.expect
@@ -2,7 +2,7 @@ Type error:
 [nexp_synonym/v2.sail]:7:20-32
 7 |let v : bits(LEN) = 0xFFFF_FFFFF
   |                    ^----------^
-  | Tried performing type coercion from vector(36, dec, bit) to bits(LEN) on 0xFFFFFFFFF
+  | Tried performing type coercion from bitvector(36, dec) to bits(LEN) on 0xFFFFFFFFF
   | Coercion failed because:
   | Mismatched argument types in subtype check
   | 
diff --git a/test/typecheck/pass/nlflow.sail b/test/typecheck/pass/nlflow.sail
index 95d2d280..9c426819 100644
--- a/test/typecheck/pass/nlflow.sail
+++ b/test/typecheck/pass/nlflow.sail
@@ -7,7 +7,7 @@ $include <exception_basic.sail>
 
 val foo : forall 'n, 'n != 8. int('n) -> unit
 
-function test(xs: vector(4, dec, bit)) -> unit = {
+function test(xs: bitvector(4, dec)) -> unit = {
   if xs == 0b1000 then {
     throw(Exception())
   };
diff --git a/test/typecheck/pass/nzcv.sail b/test/typecheck/pass/nzcv.sail
index dc625084..dd1734f6 100644
--- a/test/typecheck/pass/nzcv.sail
+++ b/test/typecheck/pass/nzcv.sail
@@ -1,9 +1,9 @@
 default Order dec
 
 val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec"} : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n.
-  (vector('n, dec, bit), atom('m), atom('o)) -> vector('m - ('o - 1), dec, bit)
+  (bitvector('n, dec), atom('m), atom('o)) -> bitvector('m - ('o - 1), dec)
 
-val test : vector(4, dec, bit) -> unit
+val test : bitvector(4, dec) -> unit
 
 function test nzcv = {
   N = 0b0;
diff --git a/test/typecheck/pass/procstate1.sail b/test/typecheck/pass/procstate1.sail
index 1d7e15b1..02453c72 100644
--- a/test/typecheck/pass/procstate1.sail
+++ b/test/typecheck/pass/procstate1.sail
@@ -2,13 +2,13 @@ default Order dec
 
 infix 4 ==
 
-val operator == = {lem: "eq_vec"} : forall 'n. (vector('n, dec, bit), vector('n, dec, bit)) -> bool
+val operator == = {lem: "eq_vec"} : forall 'n. (bitvector('n, dec), bitvector('n, dec)) -> bool
 
 struct ProcState ('n : Int) = {
-  N : vector('n, dec, bit),
-  Z : vector(1, dec, bit),
-  C : vector(1, dec, bit),
-  V : vector(1, dec, bit)
+  N : bitvector('n, dec),
+  Z : bitvector(1, dec),
+  C : bitvector(1, dec),
+  V : bitvector(1, dec)
 }
 
 register PSTATE : ProcState(1)
diff --git a/test/typecheck/pass/pure_record.sail b/test/typecheck/pass/pure_record.sail
index 15f14a3b..fe324914 100644
--- a/test/typecheck/pass/pure_record.sail
+++ b/test/typecheck/pass/pure_record.sail
@@ -1,24 +1,24 @@
 default Order dec
 
-struct State ('a : Type) = {
-  N : vector(1, dec, 'a),
-  Z : vector(1, dec, bit)
+struct State = {
+  N : bitvector(1, dec),
+  Z : bitvector(1, dec)
 }
 
-val myStateM : unit -> State(bit) effect {undef}
+val myStateM : unit -> State effect {undef}
 
 function myStateM () = {
-  r : State(bit) = undefined;
+  r : State = undefined;
   r.N = 0b1;
   r.Z = 0b1;
   r
 }
 
-let myState : State(bit) = struct { N = 0b1, Z = 0b1 }
+let myState : State = struct { N = 0b1, Z = 0b1 }
 
 val test : unit -> unit effect {undef}
 
 function test () = {
-  myState2 : State(bit) = struct { N = undefined, Z = 0b1 };
-  myState3 : State(bit) = { myState2 with N = 0b0 }
+  myState2 : State = struct { N = undefined, Z = 0b1 };
+  myState3 : State = { myState2 with N = 0b0 }
 }
diff --git a/test/typecheck/pass/pure_record2.sail b/test/typecheck/pass/pure_record2.sail
index 588fd324..fe6651db 100644
--- a/test/typecheck/pass/pure_record2.sail
+++ b/test/typecheck/pass/pure_record2.sail
@@ -1,24 +1,24 @@
 default Order dec
 
-struct State('a: Type, 'n: Int) = {
-  N : vector('n, dec, 'a),
-  Z : vector(1, dec, bit)
+struct State('n: Int) = {
+  N : bitvector('n, dec),
+  Z : bitvector(1, dec)
 }
 
-val myStateM : unit -> State(bit, 1) effect {undef}
+val myStateM : unit -> State(1) effect {undef}
 
 function myStateM () = {
-  r : State(bit, 1) = undefined;
+  r : State(1) = undefined;
   r.N = 0b1;
   r.Z = 0b1;
   r
 }
 
-let myState : State(bit, 1) = struct { N = 0b1, Z = 0b1 }
+let myState : State(1) = struct { N = 0b1, Z = 0b1 }
 
 val test : unit -> unit effect {undef}
 
 function test () = {
-  myState2 : State(bit, 1) = struct { N = undefined, Z = 0b1 };
-  myState3 : State(bit, 1) = { myState2 with N = 0b0 }
+  myState2 : State(1) = struct { N = undefined, Z = 0b1 };
+  myState3 : State(1) = { myState2 with N = 0b0 }
 }
diff --git a/test/typecheck/pass/pure_record3.sail b/test/typecheck/pass/pure_record3.sail
index de388c3e..b1080a1a 100644
--- a/test/typecheck/pass/pure_record3.sail
+++ b/test/typecheck/pass/pure_record3.sail
@@ -1,27 +1,27 @@
 default Order dec
 
-struct State('a: Type, 'n: Int) = {
-  N : vector('n, dec, 'a),
-  Z : vector(1, dec, bit)
+struct State('n: Int) = {
+  N : bitvector('n, dec),
+  Z : bitvector(1, dec)
 }
 
-register procState : State(bit, 1)
+register procState : State(1)
 
-val myStateM : unit -> State(bit, 1) effect {undef}
+val myStateM : unit -> State(1) effect {undef}
 
 function myStateM () = {
-  r : State(bit, 1) = undefined;
+  r : State(1) = undefined;
   r.N = 0b1;
   r.Z = 0b1;
   r
 }
 
-let myState : State(bit, 1) = struct { N = 0b1, Z = 0b1 }
+let myState : State(1) = struct { N = 0b1, Z = 0b1 }
 
 val test : unit -> unit effect {undef}
 
 function test () = {
-  myState1 : State(bit, 1) = undefined;
-  myState2 : State(bit, 1) = struct { N = undefined, Z = 0b1 };
-  myState3 : State(bit, 1) = { myState2 with N = 0b0 }
+  myState1 : State(1) = undefined;
+  myState2 : State(1) = struct { N = undefined, Z = 0b1 };
+  myState3 : State(1) = { myState2 with N = 0b0 }
 }
diff --git a/test/typecheck/pass/reg_32_64/v2.expect b/test/typecheck/pass/reg_32_64/v2.expect
index f007c917..24439bed 100644
--- a/test/typecheck/pass/reg_32_64/v2.expect
+++ b/test/typecheck/pass/reg_32_64/v2.expect
@@ -2,7 +2,7 @@ Type error:
 [reg_32_64/v2.sail]:21:18-22
 21 |  (*R)['d .. 0] = data
    |                  ^--^
-   | Tried performing type coercion from vector('d, dec, bit) to vector((('d - 0) + 1), dec, bit) on data
+   | Tried performing type coercion from bitvector('d, dec) to bitvector((('d - 0) + 1), dec) on data
    | Coercion failed because:
    | Mismatched argument types in subtype check
    | This error occured because of a previous error:
diff --git a/test/typecheck/pass/vec_length/v1.expect b/test/typecheck/pass/vec_length/v1.expect
index ce61cf2a..36bd848e 100644
--- a/test/typecheck/pass/vec_length/v1.expect
+++ b/test/typecheck/pass/vec_length/v1.expect
@@ -7,6 +7,5 @@ Type error:
   |    Could not resolve quantifiers for bitvector_access
   |    * (0 <= 10 & (10 + 1) <= 8)
   | * plain_vector_access
-  |    Could not resolve quantifiers for plain_vector_access
-  |    * (0 <= 10 & (10 + 1) <= 8)
+  |    No valid casts resulted in unification
   | 
diff --git a/test/typecheck/pass/vec_length/v1_inc.expect b/test/typecheck/pass/vec_length/v1_inc.expect
index 3d40cdb0..efbfcc54 100644
--- a/test/typecheck/pass/vec_length/v1_inc.expect
+++ b/test/typecheck/pass/vec_length/v1_inc.expect
@@ -7,6 +7,5 @@ Type error:
   |    Could not resolve quantifiers for bitvector_access
   |    * (0 <= 10 & (10 + 1) <= 8)
   | * plain_vector_access
-  |    Could not resolve quantifiers for plain_vector_access
-  |    * (0 <= 10 & (10 + 1) <= 8)
+  |    No valid casts resulted in unification
   | 
diff --git a/test/typecheck/pass/vec_length/v2.expect b/test/typecheck/pass/vec_length/v2.expect
index c77ecaa7..9ce8f9a2 100644
--- a/test/typecheck/pass/vec_length/v2.expect
+++ b/test/typecheck/pass/vec_length/v2.expect
@@ -7,6 +7,5 @@ Type error:
   |    Could not resolve quantifiers for bitvector_update
   |    * (0 <= 10 & (10 + 1) <= 8)
   | * plain_vector_update
-  |    Could not resolve quantifiers for plain_vector_update
-  |    * (0 <= 10 & (10 + 1) <= 8)
+  |    No valid casts resulted in unification
   | 
diff --git a/test/typecheck/pass/vec_length/v2_inc.expect b/test/typecheck/pass/vec_length/v2_inc.expect
index cff65f62..dba312ea 100644
--- a/test/typecheck/pass/vec_length/v2_inc.expect
+++ b/test/typecheck/pass/vec_length/v2_inc.expect
@@ -7,6 +7,5 @@ Type error:
   |    Could not resolve quantifiers for bitvector_update
   |    * (0 <= 10 & (10 + 1) <= 8)
   | * plain_vector_update
-  |    Could not resolve quantifiers for plain_vector_update
-  |    * (0 <= 10 & (10 + 1) <= 8)
+  |    No valid casts resulted in unification
   | 
diff --git a/test/typecheck/pass/vec_length/v3.expect b/test/typecheck/pass/vec_length/v3.expect
index e3afecee..88e6fa50 100644
--- a/test/typecheck/pass/vec_length/v3.expect
+++ b/test/typecheck/pass/vec_length/v3.expect
@@ -9,6 +9,5 @@ Type error:
    |    Could not resolve quantifiers for bitvector_access
    |    * (0 <= 10 & (10 + 1) <= 8)
    | * plain_vector_access
-   |    Could not resolve quantifiers for plain_vector_access
-   |    * (0 <= 10 & (10 + 1) <= 8)
+   |    No valid casts resulted in unification
    | 
diff --git a/test/typecheck/pass/vec_pat1.sail b/test/typecheck/pass/vec_pat1.sail
index 6de87a8c..e11a8654 100644
--- a/test/typecheck/pass/vec_pat1.sail
+++ b/test/typecheck/pass/vec_pat1.sail
@@ -1,15 +1,15 @@
 default Order inc
 
 val bv_add = {ocaml: "add_vec", lem: "add_vec"}: forall ('n : Int).
-  (vector('n, inc, bit), vector('n, inc, bit)) -> vector('n, inc, bit)
+  (bitvector('n, inc), bitvector('n, inc)) -> bitvector('n, inc)
 
 val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_inc"}: forall ('l : Int) ('m : Int) ('o : Int), 'l >= 0 & 'm <= 'o & 'o <= 'l.
-  (vector('l, inc, bit), atom('m), atom('o)) -> vector('o + 1 - 'm, inc, bit)
+  (bitvector('l, inc), atom('m), atom('o)) -> bitvector('o + 1 - 'm, inc)
 
 val bitvector_concat = {ocaml: "append", lem: "concat_vec"} : forall ('m : Int) ('p : Int).
-  (vector('m, inc, bit), vector('p, inc, bit)) -> vector('m + 'p, inc, bit)
+  (bitvector('m, inc), bitvector('p, inc)) -> bitvector('m + 'p, inc)
 
-val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (vector('n, inc, bit), vector('n, inc, bit)) -> bool
+val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bitvector('n, inc), bitvector('n, inc)) -> bool
 
 infix 4 ==
 overload operator == = {eq_vec}
@@ -18,6 +18,6 @@ overload operator + = {bv_add}
 
 overload append = {bitvector_concat}
 
-val test : (vector(3, inc, bit), vector(3, inc, bit)) -> vector(3, inc, bit)
+val test : (bitvector(3, inc), bitvector(3, inc)) -> bitvector(3, inc)
 
-function test (x : vector(1, inc, bit) @ 0b1 @ 0b0, z) = (x @ 0b11) + z
+function test (x : bitvector(1, inc) @ 0b1 @ 0b0, z) = (x @ 0b11) + z
diff --git a/test/typecheck/pass/vector_subrange_gen.sail b/test/typecheck/pass/vector_subrange_gen.sail
index b82d6c8c..9f7f4e49 100644
--- a/test/typecheck/pass/vector_subrange_gen.sail
+++ b/test/typecheck/pass/vector_subrange_gen.sail
@@ -1,23 +1,17 @@
 
-val vector_access : forall ('l : Int) ('o : Order) ('a : Type), 'l >= 0.
-  (vector('l, 'o, 'a), range(0, 'l - 1)) -> 'a
-
-val vector_append : forall ('l1 : Int) ('l2 : Int) ('o : Order) ('a : Type), 'l1 >= 0 & 'l2 >= 0.
-  (vector('l1, 'o, 'a), vector('l2, 'o, 'a)) -> vector('l1 + 'l2, 'o, 'a)
-
 val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_inc"} : forall ('l : Int) ('m : Int) ('o : Int), 'l >= 0 & 'm <= 'o & 'o <= 'l.
-  (vector('l, inc, bit), atom('m), atom('o)) -> vector('o - 'm + 1, inc, bit)
+  (bitvector('l, inc), atom('m), atom('o)) -> bitvector('o - 'm + 1, inc)
 
 val sub : forall ('n : Int) ('m : Int). (atom('n), atom('m)) -> atom('n - 'm)
 
-val "length" : forall ('n : Int). vector('n, inc, bit) -> atom('n)
+val bitvector_length = "length" : forall ('n : Int). bitvector('n, inc) -> atom('n)
 
-overload __size = {length}
+overload __size = {bitvector_length}
 
 default Order inc
 
 val test : forall 'n 'm, 'n >= 5.
-  vector('n, inc, bit) -> vector('n - 1, inc, bit)
+  bitvector('n, inc) -> bitvector('n - 1, inc)
 
 function test v = {
   z = vector_subrange(v, 0, sub('n, 2));