diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/gen_lib/sail_string.lem | 129 | ||||
| -rw-r--r-- | src/process_file.ml | 1 | ||||
| -rw-r--r-- | src/rewrites.ml | 3 | ||||
| -rw-r--r-- | src/sail_lib.ml | 9 |
4 files changed, 141 insertions, 1 deletions
diff --git a/src/gen_lib/sail_string.lem b/src/gen_lib/sail_string.lem new file mode 100644 index 00000000..f31e612b --- /dev/null +++ b/src/gen_lib/sail_string.lem @@ -0,0 +1,129 @@ +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_spaces_matches_prefix s = + Just ((), n_leading_spaces s) + +let spaces_matches_prefix s = + let n = n_leading_spaces s in + match n with + | 0 -> Nothing + | n -> Just ((), n) + 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 string_of_bits = string_of_vec diff --git a/src/process_file.ml b/src/process_file.ml index 1bf8eee9..7cab1266 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -295,6 +295,7 @@ let output_lem filename libs defs = "Pervasives_extra"; "Sail_instr_kinds"; "Sail_values"; + "Sail_string"; operators_module ] @ monad_modules in diff --git a/src/rewrites.ml b/src/rewrites.ml index 34cb327a..6772d78c 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -711,6 +711,7 @@ let remove_vector_concat_pat pat = let p_vector_concat pats = let rec aux ((P_aux (p,((l,_) as a))) as pat) = match p with | P_vector _ -> P_aux (P_as (pat,fresh_id_v l),a) + | P_lit _ -> P_aux (P_as (pat, fresh_id_v l), a) | P_id id -> P_aux (P_id id,a) | P_as (p,id) -> P_aux (P_as (p,id),a) | P_typ (typ, pat) -> P_aux (P_typ (typ, aux pat),a) @@ -3900,7 +3901,7 @@ let rewrite_defs_lem = [ ("remove_mapping_valspecs", remove_mapping_valspecs); ("pat_string_append", rewrite_defs_pat_string_append); ("mapping_builtins", rewrite_defs_mapping_patterns); - (* ("pat_lits", rewrite_defs_pat_lits); *) + ("pat_lits", rewrite_defs_pat_lits); ("vector_concat_assignments", rewrite_vector_concat_assignments); ("tuple_assignments", rewrite_tuple_assignments); ("simple_assignments", rewrite_simple_assignments); diff --git a/src/sail_lib.ml b/src/sail_lib.ml index 81685bec..6e2deff7 100644 --- a/src/sail_lib.ml +++ b/src/sail_lib.ml @@ -644,6 +644,15 @@ let spaces_matches_prefix s = | 0 -> ZNone () | n -> ZSome ((), Big_int.of_int n) +let hex_bits_6_matches_prefix s = + match maybe_int_of_prefix s with + | ZNone () -> ZNone () + | ZSome (n, len) -> + let n = Big_int.to_int n in + if 0 <= n && n < 64 then + ZSome ((bits_of_int 32 n, len)) + else + ZNone () let hex_bits_12_matches_prefix s = match maybe_int_of_prefix s with |