diff options
| author | Brian Campbell | 2017-10-25 12:19:08 +0100 |
|---|---|---|
| committer | Brian Campbell | 2017-10-25 12:19:08 +0100 |
| commit | d1d7f0ef16080200187230d9708155668af6edbf (patch) | |
| tree | 505dce3dc7a2f3f4841909422d822b292ca91d9b | |
| parent | 05b00c86ee484a3e7f108f306e77ae200816a8ad (diff) | |
Avoid name clash in generated Lem
(complains due to added val spec)
| -rw-r--r-- | lib/prelude_wrappers.sail | 2 | ||||
| -rw-r--r-- | src/gen_lib/sail_operators.lem | 2 | ||||
| -rw-r--r-- | 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) |