From 1dc7c1c7984d8a5bd2750f88a249f33fdebb498b Mon Sep 17 00:00:00 2001
From: Christopher Pulte
Date: Wed, 26 Oct 2016 11:49:55 +0100
Subject: shallow embedding fixes

---
 src/gen_lib/sail_values.lem | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'src/gen_lib')

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
 
-- 
cgit v1.2.3