diff options
| -rw-r--r-- | lib/vector_dec.sail | 12 | ||||
| -rw-r--r-- | test/c/bitvector.sail | 4 | ||||
| -rw-r--r-- | test/ocaml/lsl/lsl.sail | 2 | ||||
| -rw-r--r-- | test/ocaml/vec_32_64/vec_32_64.sail | 4 |
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 |