Merge branch 'sail2' into union_barrier

1 files changed, 448 insertions, 0 deletions

diff --git a/src/gen_lib/0.11/sail2_string.lem b/src/gen_lib/0.11/sail2_string.lem
new file mode 100644
index 00000000..33a665a0
--- /dev/null
+++ b/src/gen_lib/0.11/sail2_string.lem
@@ -0,0 +1,448 @@
+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