Rename some functions in vector_dec library file to avoid clashes with functions in mips spec in prepartion for using this file in mips prelude. Also modify tests that use this header. We should consider prefixing library builtins to avoid name clashes. overload can then be used to provide aliases if desired.

4 files changed, 11 insertions, 11 deletions

diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
index 864d2107..05c7e35b 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -25,15 +25,15 @@ val vector_length = {
 
 overload length = {bitvector_length, vector_length}
 
-val "zeros" : forall 'n. atom('n) -> bits('n)
+val sail_zeros = "zeros" : forall 'n. atom('n) -> bits('n)
 
 val "print_bits" : forall 'n. (string, bits('n)) -> unit
 
 val "prerr_bits" : forall 'n. (string, bits('n)) -> unit
 
-val "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), atom('m)) -> bits('m)
 
-val "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), atom('m)) -> bits('m)
 
 val truncate = {
   ocaml: "vector_truncate",
@@ -42,11 +42,11 @@ val truncate = {
   c: "truncate"
 } : forall 'm 'n, 'm >= 0 & 'm <= 'n. (vector('n, dec, bit), atom('m)) -> vector('m, dec, bit)
 
-val 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. (atom('len), vector('v, dec, bit)) -> vector('len, dec, bit)
 
-function mask(len, v) = if len <= length(v) then truncate(v, len) else zero_extend(v, len)
+function sail_mask(len, v) = if len <= length(v) then truncate(v, len) else sail_zero_extend(v, len)
 
-overload operator ^ = {mask}
+overload operator ^ = {sail_mask}
 
 val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append"} : forall ('n : Int) ('m : Int).
   (bits('n), bits('m)) -> bits('n + 'm)
diff --git a/test/c/bitvector.sail b/test/c/bitvector.sail
index 5311caff..8a80234e 100644
--- a/test/c/bitvector.sail
+++ b/test/c/bitvector.sail
@@ -13,10 +13,10 @@ function test (x, y)  = {
 val main : unit -> unit
 
 function main () = {
-  if test(0xBEEF, zeros(200)) then () else ();
+  if test(0xBEEF, sail_zeros(200)) then () else ();
   let z = 0xCAFE;
   print_bits("z = ", z);
-  print_bits("zero_extend(z) = ", zero_extend(z, 32));
+  print_bits("zero_extend(z) = ", sail_zero_extend(z, 32));
   let q = 0xAB_FEED_DEAD_BEEF_CAFE;
   print_bits("q = ", q);
   let k = 0xFF;
diff --git a/test/ocaml/lsl/lsl.sail b/test/ocaml/lsl/lsl.sail
index 74d2b8e5..ce270c4e 100644
--- a/test/ocaml/lsl/lsl.sail
+++ b/test/ocaml/lsl/lsl.sail
@@ -4,7 +4,7 @@ val lslc : forall ('n : Int) ('shift : Int), 'n >= 1.
 
 function lslc (vec, shift) = {
   assert(constraint('shift >= 1), "shift must be positive");
-  extended : bits('shift + 'n) = vec @ zeros(shift);
+  extended : bits('shift + 'n) = vec @ sail_zeros(shift);
   result : bits('n) = extended[sizeof('n - 1) .. 0];
   c : bit = extended['n];
   return((result, c))
diff --git a/test/ocaml/vec_32_64/vec_32_64.sail b/test/ocaml/vec_32_64/vec_32_64.sail
index ac44d9ae..5dc58cc3 100644
--- a/test/ocaml/vec_32_64/vec_32_64.sail
+++ b/test/ocaml/vec_32_64/vec_32_64.sail
@@ -12,12 +12,12 @@ val main : unit -> unit
 
 function main () = {
   let 'len = get_size ();
-  let xs = zeros(len);
+  let xs = sail_zeros(len);
   if (len == 32) then {
     ()
   } else {
     only64(xs)
   };
   print_bits("xs = ", xs);
-  print_bits("zeros(64) = ", zeros(64))
+  print_bits("zeros(64) = ", sail_zeros(64))
 }
\ No newline at end of file