diff options
| author | Brian Campbell | 2018-03-14 15:05:40 +0000 |
|---|---|---|
| committer | Brian Campbell | 2018-03-14 15:05:40 +0000 |
| commit | 00a7076624011f76b5d8dfc41dc8072658a66739 (patch) | |
| tree | 3cc23b0ef9d1fd9997bdd8c539fec1ddcf827322 /src | |
| parent | f5e92e2fa59a672c21d301407cd6f545810e2830 (diff) | |
Machine words extract/update operations arguments are the other way around
Diffstat (limited to 'src')
| -rw-r--r-- | src/gen_lib/sail_operators_mwords.lem | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem index e87f4b7c..16b9a912 100644 --- a/src/gen_lib/sail_operators_mwords.lem +++ b/src/gen_lib/sail_operators_mwords.lem @@ -51,13 +51,13 @@ let update_vec_inc_oracle w i b = let update_vec_inc w i b = maybe_failwith (update_vec_inc_maybe w i b) val subrange_vec_dec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b -let subrange_vec_dec w i j = Machine_word.word_extract (nat_of_int i) (nat_of_int j) w +let subrange_vec_dec w i j = Machine_word.word_extract (nat_of_int j) (nat_of_int i) w val subrange_vec_inc : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b let subrange_vec_inc w i j = subrange_vec_dec w (length w - 1 - i) (length w - 1 - j) val update_subrange_vec_dec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b -> mword 'a -let update_subrange_vec_dec w i j w' = Machine_word.word_update w (nat_of_int i) (nat_of_int j) w' +let update_subrange_vec_dec w i j w' = Machine_word.word_update w (nat_of_int j) (nat_of_int i) w' val update_subrange_vec_inc : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b -> mword 'a let update_subrange_vec_inc w i j w' = update_subrange_vec_dec w (length w - 1 - i) (length w - 1 - j) w' |