1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
|
open import Pervasives
open import List
open import List_extra
open import String
open import String_extra
open import Sail2_operators_mwords
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_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_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
| 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
| 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_16_matches_prefix s =
match maybe_int_of_prefix s with
| Nothing -> Nothing
| Just (n, len) ->
if 0 <= n && n < 65536 then
Just ((of_int 16 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 hex_bits_32_matches_prefix s =
match maybe_int_of_prefix s with
| Nothing -> Nothing
| Just (n, len) ->
if 0 <= n && n < 4294967296 then
Just ((of_int 2147483648 n, len))
else
Nothing
end
let string_of_bits = string_of_vec
|
