Make some potentially non-terminating library functions terminate

1 files changed, 6 insertions, 5 deletions

diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 48d728bf..97f13c33 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -41,7 +41,7 @@ let list_append (l, r) = l ++ r
 
 val repeat : forall 'a. list 'a -> integer -> list 'a
 let rec repeat xs n =
-  if n = 0 then []
+  if n <= 0 then []
   else xs ++ repeat xs (n-1)
 
 let duplicate_to_list (bit, length) = repeat [bit] length
@@ -167,6 +167,7 @@ let get_dir (Vector _ _ ord) = ord
 let get_start (Vector _ s _) = s
 let get_elems (Vector elems _ _) = elems
 let length (Vector bs _ _) = integerFromNat (length bs)
+let vector_length = length
 
 instance forall 'a. Show 'a => (Show (vector 'a))
   let show = showVector
@@ -566,17 +567,17 @@ let internal_mem_value direction bytes =
 val foreach_inc :  forall 'vars. (integer * integer * integer) -> 'vars ->
                    (integer -> 'vars -> 'vars) -> 'vars
 let rec foreach_inc (i,stop,by) vars body =
-  if i <= stop
+  if (by > 0 && i <= stop) || (by < 0 && stop <= i)
   then let vars = body i vars in
        foreach_inc (i + by,stop,by) vars body
   else vars
 
 val foreach_dec : forall 'vars. (integer * integer * integer) -> 'vars ->
                   (integer -> 'vars -> 'vars) -> 'vars
-let rec foreach_dec (i,stop,by) vars body =
-  if i >= stop
+let rec foreach_dec (stop,i,by) vars body =
+  if (by > 0 && i >= stop) || (by < 0 && stop >= i)
   then let vars = body i vars in
-       foreach_dec (i - by,stop,by) vars body
+       foreach_dec (stop,i - by,by) vars body
   else vars
 
 let assert' b msg_opt =