From e65dca0c66e3a58c1b295bc0029f519a3eda333d Mon Sep 17 00:00:00 2001
From: Jon French
Date: Mon, 21 May 2018 15:20:59 +0100
Subject: further RISCV mapping: all extant non-compressed instructions done

---
 src/gen_lib/sail_string.lem | 10 ++++++++++
 src/sail_lib.ml             | 10 ++++++++++
 2 files changed, 20 insertions(+)

(limited to 'src')

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 ()
-- 
cgit v1.2.3