From c281c3aed5b00d970c9a48b59eb4b3bc620a28b0 Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Thu, 7 Jun 2018 17:39:01 +0100
Subject: 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.

---
 lib/vector_dec.sail | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'lib')

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)
-- 
cgit v1.2.3