diff options
Diffstat (limited to 'src/gen_lib/sail_string.lem')
| -rw-r--r-- | src/gen_lib/sail_string.lem | 150 |
1 files changed, 0 insertions, 150 deletions
diff --git a/src/gen_lib/sail_string.lem b/src/gen_lib/sail_string.lem deleted file mode 100644 index 07b39ddc..00000000 --- a/src/gen_lib/sail_string.lem +++ /dev/null @@ -1,150 +0,0 @@ -open import Pervasives -open import List -open import List_extra -open import String -open import String_extra - -open import Sail_operators_mwords -open import Sail_values - -val string_sub : string -> ii -> ii -> string -let string_sub str start len = - toString (take (natFromInteger len) (drop (natFromInteger start) (toCharList str))) - -val string_startswith : string -> string -> bool -let string_startswith str1 str2 = - let prefix = string_sub str1 0 (integerFromNat (stringLength str2)) in - (prefix = str2) - -val string_drop : string -> ii -> string -let string_drop str n = - toString (drop (natFromInteger n) (toCharList str)) - -val string_length : string -> ii -let string_length s = integerFromNat (stringLength s) - -let string_append = stringAppend - -(*********************************************** - * Begin stuff that should be in Lem Num_extra * - ***********************************************) - -val maybeIntegerOfString : string -> maybe integer - -declare ocaml target_rep function maybeIntegerOfString = `(fun s -> match int_of_string_opt s with None -> None | Some i -> Nat_big_num.of_int i)` -declare isabelle target_rep function maybeIntegerOfString = `maybeIntegerOfString` (* TODO FIXME *) -declare hol target_rep function maybeIntegerOfString = `maybeIntegerOfString` (* TODO FIXME *) - -(*********************************************** - * end stuff that should be in Lem Num_extra * - ***********************************************) - -let rec maybe_int_of_prefix s = - match s with - | "" -> Nothing - | str -> - let len = string_length str in - match maybeIntegerOfString str with - | Just n -> Just (n, len) - | Nothing -> maybe_int_of_prefix (string_sub str 0 (len - 1)) - end - end - -let maybe_int_of_string = maybeIntegerOfString - -val n_leading_spaces : string -> ii -let rec n_leading_spaces s = - match string_length s with - | 0 -> 0 - | 1 -> match s with - | " " -> 1 - | _ -> 0 - end - | len -> match nth s 0 with - | #' ' -> 1 + (n_leading_spaces (string_sub s 1 (len - 1))) - | _ -> 0 - end - end - -let opt_spc_matches_prefix s = - Just ((), n_leading_spaces s) - -let spc_matches_prefix s = - let n = n_leading_spaces s in - match n with - | 0 -> Nothing - | n -> Just ((), n) - end - -let hex_bits_5_matches_prefix s = - match maybe_int_of_prefix s with - | Nothing -> Nothing - | Just (n, len) -> - if 0 <= n && n < 32 then - Just ((of_int 5 n, len)) - else - Nothing - end - -let hex_bits_6_matches_prefix s = - match maybe_int_of_prefix s with - | Nothing -> Nothing - | Just (n, len) -> - if 0 <= n && n < 64 then - Just ((of_int 6 n, len)) - else - Nothing - end - -let hex_bits_12_matches_prefix s = - match maybe_int_of_prefix s with - | Nothing -> Nothing - | Just (n, len) -> - if 0 <= n && n < 4096 then - Just ((of_int 12 n, len)) - else - Nothing - end - -let hex_bits_13_matches_prefix s = - match maybe_int_of_prefix s with - | Nothing -> Nothing - | Just (n, len) -> - if 0 <= n && n < 8192 then - Just ((of_int 13 n, len)) - else - Nothing - end - -let hex_bits_20_matches_prefix s = - match maybe_int_of_prefix s with - | Nothing -> Nothing - | Just (n, len) -> - if 0 <= n && n < 1048576 then - Just ((of_int 20 n, len)) - else - Nothing - end - -let hex_bits_21_matches_prefix s = - match maybe_int_of_prefix s with - | Nothing -> Nothing - | Just (n, len) -> - if 0 <= n && n < 2097152 then - Just ((of_int 21 n, len)) - else - Nothing - end - -let hex_bits_32_matches_prefix s = - match maybe_int_of_prefix s with - | Nothing -> Nothing - | Just (n, len) -> - if 0 <= n && n < 4294967296 then - Just ((of_int 2147483648 n, len)) - else - Nothing - end - - -let string_of_bits = string_of_vec |