diff options
Diffstat (limited to 'src/gen_lib')
| -rw-r--r-- | src/gen_lib/sail_operators.lem | 8 | ||||
| -rw-r--r-- | src/gen_lib/sail_operators_mwords.lem | 2 | ||||
| -rw-r--r-- | src/gen_lib/sail_values.lem | 7 |
3 files changed, 11 insertions, 6 deletions
diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem index f14ef2e4..b94257f0 100644 --- a/src/gen_lib/sail_operators.lem +++ b/src/gen_lib/sail_operators.lem @@ -5,7 +5,7 @@ open import Sail_values (*** Bit vector operations *) -let bvlength = length +let bitvector_length = length let set_bitvector_start = set_vector_start let reset_bitvector_start = reset_vector_start @@ -25,8 +25,10 @@ let vector_subrange_bl_dec = vector_subrange_bl let bitvector_access_inc = vector_access_inc let bitvector_access_dec = vector_access_dec -let bitvector_update_pos_dec = update_pos -let bitvector_update_subrange_dec = vector_update_dec +let bitvector_update_pos_inc = vector_update_pos_inc +let bitvector_update_pos_dec = vector_update_pos_dec +let bitvector_update_subrange_inc = vector_update_subrange_inc +let bitvector_update_subrange_dec = vector_update_subrange_dec let extract_only_bit = extract_only_element diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem index 4d1cc713..a1fc1fd7 100644 --- a/src/gen_lib/sail_operators_mwords.lem +++ b/src/gen_lib/sail_operators_mwords.lem @@ -5,7 +5,7 @@ open import Sail_values (*** Bit vector operations *) -let bvlength bs = integerFromNat (word_length bs) +let bitvector_length bs = integerFromNat (word_length bs) (*val set_bitvector_start : forall 'a. (integer * bitvector 'a) -> bitvector 'a let set_bitvector_start (new_start, Bitvector bs _ is_inc) = diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index 95a61eca..48d728bf 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -246,8 +246,8 @@ val update : forall 'a. vector 'a -> integer -> integer -> vector 'a -> vector ' let update (Vector bs start is_inc) i j (Vector bs' _ _) = Vector (update_aux is_inc start bs i j bs') start is_inc -let vector_update_inc (start, v, i, j, v') = update v i j v' -let vector_update_dec (start, v, i, j, v') = update v i j v' +let vector_update_subrange_inc (start, v, i, j, v') = update v i j v' +let vector_update_subrange_dec (start, v, i, j, v') = update v i j v' val access_aux : forall 'a. bool -> integer -> list 'a -> integer -> 'a let access_aux is_inc start xs n = @@ -264,6 +264,9 @@ val update_pos : forall 'a. vector 'a -> integer -> 'a -> vector 'a let update_pos v n b = update v n n (Vector [b] 0 false) +let vector_update_pos_inc (start, v, i, x) = update_pos v i x +let vector_update_pos_dec (start, v, i, x) = update_pos v i x + let extract_only_element (Vector elems _ _) = match elems with | [] -> failwith "extract_only_element called for empty vector" | [e] -> e |