diff options
Diffstat (limited to 'src/gen_lib/0.11/sail2_string.lem')
| -rw-r--r-- | src/gen_lib/0.11/sail2_string.lem | 448 |
1 files changed, 0 insertions, 448 deletions
diff --git a/src/gen_lib/0.11/sail2_string.lem b/src/gen_lib/0.11/sail2_string.lem deleted file mode 100644 index 33a665a0..00000000 --- a/src/gen_lib/0.11/sail2_string.lem +++ /dev/null @@ -1,448 +0,0 @@ -open import Pervasives -open import List -open import List_extra -open import String -open import String_extra - -open import Sail2_operators -open import Sail2_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_take : string -> ii -> string -let string_take str n = - toString (take (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 -let maybeIntegerOfString _ = Nothing (* TODO FIXME *) -declare ocaml target_rep function maybeIntegerOfString = `(fun s -> match int_of_string s with i -> Some (Nat_big_num.of_int i) | exception Failure _ -> None )` - -(*********************************************** - * 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 = - let len = string_length s in - if len = 0 then 0 else - if len = 1 then - match s with - | " " -> 1 - | _ -> 0 - end - else - (* Isabelle generation for pattern matching on characters - is currently broken, so use an if-expression *) - if nth s 0 = #' ' - then 1 + (n_leading_spaces (string_sub s 1 (len - 1))) - else 0 - (* 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 *) - if n = 0 then Nothing else - (* | n -> *) Just ((), n) - (* end *) - -(* Python: -f = """let hex_bits_{0}_matches_prefix s = - match maybe_int_of_prefix s with - | Nothing -> Nothing - | Just (n, len) -> - if 0 <= n && n < (2 ** {0}) then - Just ((of_int {0} n, len)) - else - Nothing - end -""" - -for i in list(range(1, 34)) + [48, 64]: - print(f.format(i)) -*) -let hex_bits_1_matches_prefix s = - match maybe_int_of_prefix s with - | Nothing -> Nothing - | Just (n, len) -> - if 0 <= n && n < (2 ** 1) then - Just ((of_int 1 n, len)) - else - Nothing - end - -let hex_bits_2_matches_prefix s = - match maybe_int_of_prefix s with - | Nothing -> Nothing - | Just (n, len) -> - if 0 <= n && n < (2 ** 2) then - Just ((of_int 2 n, len)) - else - Nothing - end - -let hex_bits_3_matches_prefix s = - match maybe_int_of_prefix s with - | Nothing -> Nothing - | Just (n, len) -> - if 0 <= n && n < (2 ** 3) then - Just ((of_int 3 n, len)) - else - Nothing - end - -let hex_bits_4_matches_prefix s = - match maybe_int_of_prefix s with - | Nothing -> Nothing - | Just (n, len) -> - if 0 <= n && n < (2 ** 4) then - Just ((of_int 4 n, len)) - else - Nothing - end - -let hex_bits_5_matches_prefix s = - match maybe_int_of_prefix s with - | Nothing -> Nothing - | Just (n, len) -> - if 0 <= n && n < (2 ** 5) 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 < (2 ** 6) then - Just ((of_int 6 n, len)) - else - Nothing - end - -let hex_bits_7_matches_prefix s = - match maybe_int_of_prefix s with - | Nothing -> Nothing - | Just (n, len) -> - if 0 <= n && n < (2 ** 7) then - Just ((of_int 7 n, len)) - else - Nothing - end - -let hex_bits_8_matches_prefix s = - match maybe_int_of_prefix s with - | Nothing -> Nothing - | Just (n, len) -> - if 0 <= n && n < (2 ** 8) then - Just ((of_int 8 n, len)) - else - Nothing - end - -let hex_bits_9_matches_prefix s = - match maybe_int_of_prefix s with - | Nothing -> Nothing - | Just (n, len) -> - if 0 <= n && n < (2 ** 9) then - Just ((of_int 9 n, len)) - else - Nothing - end - -let hex_bits_10_matches_prefix s = - match maybe_int_of_prefix s with - | Nothing -> Nothing - | Just (n, len) -> - if 0 <= n && n < (2 ** 10) then - Just ((of_int 10 n, len)) - else - Nothing - end - -let hex_bits_11_matches_prefix s = - match maybe_int_of_prefix s with - | Nothing -> Nothing - | Just (n, len) -> - if 0 <= n && n < (2 ** 11) then - Just ((of_int 11 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 < (2 ** 12) 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 < (2 ** 13) then - Just ((of_int 13 n, len)) - else - Nothing - end - -let hex_bits_14_matches_prefix s = - match maybe_int_of_prefix s with - | Nothing -> Nothing - | Just (n, len) -> - if 0 <= n && n < (2 ** 14) then - Just ((of_int 14 n, len)) - else - Nothing - end - -let hex_bits_15_matches_prefix s = - match maybe_int_of_prefix s with - | Nothing -> Nothing - | Just (n, len) -> - if 0 <= n && n < (2 ** 15) then - Just ((of_int 15 n, len)) - else - Nothing - end - -let hex_bits_16_matches_prefix s = - match maybe_int_of_prefix s with - | Nothing -> Nothing - | Just (n, len) -> - if 0 <= n && n < (2 ** 16) then - Just ((of_int 16 n, len)) - else - Nothing - end - -let hex_bits_17_matches_prefix s = - match maybe_int_of_prefix s with - | Nothing -> Nothing - | Just (n, len) -> - if 0 <= n && n < (2 ** 17) then - Just ((of_int 17 n, len)) - else - Nothing - end - -let hex_bits_18_matches_prefix s = - match maybe_int_of_prefix s with - | Nothing -> Nothing - | Just (n, len) -> - if 0 <= n && n < (2 ** 18) then - Just ((of_int 18 n, len)) - else - Nothing - end - -let hex_bits_19_matches_prefix s = - match maybe_int_of_prefix s with - | Nothing -> Nothing - | Just (n, len) -> - if 0 <= n && n < (2 ** 19) then - Just ((of_int 19 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 < (2 ** 20) 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 < (2 ** 21) then - Just ((of_int 21 n, len)) - else - Nothing - end - -let hex_bits_22_matches_prefix s = - match maybe_int_of_prefix s with - | Nothing -> Nothing - | Just (n, len) -> - if 0 <= n && n < (2 ** 22) then - Just ((of_int 22 n, len)) - else - Nothing - end - -let hex_bits_23_matches_prefix s = - match maybe_int_of_prefix s with - | Nothing -> Nothing - | Just (n, len) -> - if 0 <= n && n < (2 ** 23) then - Just ((of_int 23 n, len)) - else - Nothing - end - -let hex_bits_24_matches_prefix s = - match maybe_int_of_prefix s with - | Nothing -> Nothing - | Just (n, len) -> - if 0 <= n && n < (2 ** 24) then - Just ((of_int 24 n, len)) - else - Nothing - end - -let hex_bits_25_matches_prefix s = - match maybe_int_of_prefix s with - | Nothing -> Nothing - | Just (n, len) -> - if 0 <= n && n < (2 ** 25) then - Just ((of_int 25 n, len)) - else - Nothing - end - -let hex_bits_26_matches_prefix s = - match maybe_int_of_prefix s with - | Nothing -> Nothing - | Just (n, len) -> - if 0 <= n && n < (2 ** 26) then - Just ((of_int 26 n, len)) - else - Nothing - end - -let hex_bits_27_matches_prefix s = - match maybe_int_of_prefix s with - | Nothing -> Nothing - | Just (n, len) -> - if 0 <= n && n < (2 ** 27) then - Just ((of_int 27 n, len)) - else - Nothing - end - -let hex_bits_28_matches_prefix s = - match maybe_int_of_prefix s with - | Nothing -> Nothing - | Just (n, len) -> - if 0 <= n && n < (2 ** 28) then - Just ((of_int 28 n, len)) - else - Nothing - end - -let hex_bits_29_matches_prefix s = - match maybe_int_of_prefix s with - | Nothing -> Nothing - | Just (n, len) -> - if 0 <= n && n < (2 ** 29) then - Just ((of_int 29 n, len)) - else - Nothing - end - -let hex_bits_30_matches_prefix s = - match maybe_int_of_prefix s with - | Nothing -> Nothing - | Just (n, len) -> - if 0 <= n && n < (2 ** 30) then - Just ((of_int 30 n, len)) - else - Nothing - end - -let hex_bits_31_matches_prefix s = - match maybe_int_of_prefix s with - | Nothing -> Nothing - | Just (n, len) -> - if 0 <= n && n < (2 ** 31) then - Just ((of_int 31 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 < (2 ** 32) then - Just ((of_int 32 n, len)) - else - Nothing - end - -let hex_bits_33_matches_prefix s = - match maybe_int_of_prefix s with - | Nothing -> Nothing - | Just (n, len) -> - if 0 <= n && n < (2 ** 33) then - Just ((of_int 33 n, len)) - else - Nothing - end - -let hex_bits_48_matches_prefix s = - match maybe_int_of_prefix s with - | Nothing -> Nothing - | Just (n, len) -> - if 0 <= n && n < (2 ** 48) then - Just ((of_int 48 n, len)) - else - Nothing - end - -let hex_bits_64_matches_prefix s = - match maybe_int_of_prefix s with - | Nothing -> Nothing - | Just (n, len) -> - if 0 <= n && n < (2 ** 64) then - Just ((of_int 64 n, len)) - else - Nothing - end |