diff options
Diffstat (limited to 'src/gen_lib')
| -rw-r--r-- | src/gen_lib/sail_values.lem | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index 186dddc3..6f5dfb28 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -38,6 +38,16 @@ let get_dir (Vector _ _ ord) = ord let get_start (Vector _ s _) = s let length (Vector bs _ _) = integerFromNat (length bs) +val set_vector_start : forall 'a. integer -> vector 'a -> vector 'a +let set_vector_start new_start (Vector bs _ is_inc) = + Vector bs new_start is_inc + +let copy v = + set_vector_start (if (get_dir v) then 0 else (length v - 1)) v + +let set_vector_start_to_length v = + set_vector_start (length v - 1) v + let vector_concat (Vector bs start is_inc) (Vector bs' _ _) = Vector (bs ++ bs') start is_inc |