diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/gen_lib/sail_string.lem | 10 | ||||
| -rw-r--r-- | src/sail_lib.ml | 10 |
2 files changed, 20 insertions, 0 deletions
diff --git a/src/gen_lib/sail_string.lem b/src/gen_lib/sail_string.lem index f31e612b..b1f0fbe3 100644 --- a/src/gen_lib/sail_string.lem +++ b/src/gen_lib/sail_string.lem @@ -76,6 +76,16 @@ let spaces_matches_prefix s = | 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 diff --git a/src/sail_lib.ml b/src/sail_lib.ml index 6e2deff7..3e304796 100644 --- a/src/sail_lib.ml +++ b/src/sail_lib.ml @@ -644,6 +644,16 @@ let spaces_matches_prefix s = | 0 -> ZNone () | n -> ZSome ((), Big_int.of_int n) +let hex_bits_5_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 < 32 then + ZSome ((bits_of_int 16 n, len)) + else + ZNone () + let hex_bits_6_matches_prefix s = match maybe_int_of_prefix s with | ZNone () -> ZNone () |