From d1d7f0ef16080200187230d9708155668af6edbf Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Wed, 25 Oct 2017 12:19:08 +0100
Subject: Avoid name clash in generated Lem (complains due to added val spec)

---
 lib/prelude_wrappers.sail             | 2 +-
 src/gen_lib/sail_operators.lem        | 2 +-
 src/gen_lib/sail_operators_mwords.lem | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/lib/prelude_wrappers.sail b/lib/prelude_wrappers.sail
index b36dcf9c..7fd6eac6 100644
--- a/lib/prelude_wrappers.sail
+++ b/lib/prelude_wrappers.sail
@@ -78,5 +78,5 @@ function forall Num 'n, Num 'l. (vector<'n,'l,inc,bit>) cast_0_vec_inc i = to_ve
 function forall Num 'n, Num 'l. (vector<'n,'l,inc,bit>) cast_1_vec_inc i = to_vec_inc (sizeof 'n, sizeof 'l, i)
 function forall Num 'n, Num 'l. (vector<'n,'l,inc,bit>) cast_01_vec_inc i = to_vec_inc (sizeof 'n, sizeof 'l, i)
 
-val extern forall Num 'n, Num 'm, 'n >= 'm - 1, 'm >= 1. ([:'n:], [:'m:], bit) -> vector<'n,'m,dec,bit> effect pure cast_bit_vec' = "cast_bit_vec"
+val extern forall Num 'n, Num 'm, 'n >= 'm - 1, 'm >= 1. ([:'n:], [:'m:], bit) -> vector<'n,'m,dec,bit> effect pure cast_bit_vec' = "cast_bit_vec_basic"
 function forall Num 'n, Num 'm, 'n >= 'm - 1, 'm >= 1. (vector<'n,'m,dec,bit>) cast_bit_vec b = cast_bit_vec' (sizeof 'n, sizeof 'm, b)
diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
index d9bf8454..524d7ef6 100644
--- a/src/gen_lib/sail_operators.lem
+++ b/src/gen_lib/sail_operators.lem
@@ -36,7 +36,7 @@ let norm_dec = reset_vector_start
 let adjust_start_index (start, v) = set_vector_start (start, v)
 
 let cast_vec_bool v = bitU_to_bool (extract_only_element v)
-let cast_bit_vec (start, len, b) = Vector (repeat [b] len) start false
+let cast_bit_vec_basic (start, len, b) = Vector (repeat [b] len) start false
 let cast_boolvec_bitvec (Vector bs start inc) =
   Vector (List.map bool_to_bitU bs) start inc
 
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem
index 8fb158de..d4dca80c 100644
--- a/src/gen_lib/sail_operators_mwords.lem
+++ b/src/gen_lib/sail_operators_mwords.lem
@@ -97,7 +97,7 @@ let norm_dec v = v (*reset_bitvector_start*)
 let adjust_start_index (start, v) = v (*set_bitvector_start (start, v)*)
 
 let cast_vec_bool v = bitU_to_bool (extract_only_bit v)
-let cast_bit_vec (start, len, b) = vec_to_bvec (Vector [b] start false)
+let cast_bit_vec_basic (start, len, b) = vec_to_bvec (Vector [b] start false)
 let cast_boolvec_bitvec (Vector bs start inc) =
   vec_to_bvec (Vector (List.map bool_to_bitU bs) start inc)
 
-- 
cgit v1.2.3