1 files changed, 25 insertions, 0 deletions
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index 47acae88..1f3d0bba 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -1,6 +1,9 @@
 module Big_int = Nat_big_num
 
 type 'a return = { return : 'b . 'a -> 'b }
+type 'za zoption = | ZNone of unit | ZSome of 'za;;
+
+let zint_forwards i = string_of_int (Big_int.to_int i)
 
 let opt_trace = ref false
 
@@ -461,6 +464,28 @@ let debug (str1, n, str2, v) = prerr_endline (str1 ^ Big_int.to_string n ^ str2
 
 let eq_string (str1, str2) = String.compare str1 str2 == 0
 
+let string_startswith (str1, str2) = String.compare (String.sub str1 0 (String.length str2)) str2 == 0
+
+let string_drop (str, n) = let n = Big_int.to_int n in String.sub str n (String.length str - n)
+
+let string_length str = Big_int.of_int (String.length str)
+
+let string_append (s1, s2) = s1 ^ s2
+
+(* highly inefficient recursive implementation *)
+let rec maybe_int_of_prefix = function
+  | "" -> ZNone ()
+  | str ->
+     let len = String.length str in
+     match int_of_string_opt str with
+     | Some n -> ZSome (Big_int.of_int n, Big_int.of_int len)
+     | None -> maybe_int_of_prefix (String.sub str 0 (len - 1))
+
+let maybe_int_of_string str =
+  match int_of_string_opt str with
+  | None -> ZNone ()
+  | Some n -> ZSome (Big_int.of_int n)
+
 let lt_int (x, y) = Big_int.less x y
 
 let set_slice (out_len, slice_len, out, n, slice) =