blob: 54bca411ef00e431a3ac2819ff6b7712ef62e6e5 (
plain)
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
162
163
164
165
166
167
168
169
170
171
|
open Camlcoq
type bitstring = Bitstring.bitstring
module IntMap = Map.Make(struct type t = int let compare = compare end)
module StringMap = Map.Make (String)
module StringSet = Set.Make (String)
let is_some: 'a option -> bool = function
| Some(_) -> true
| None -> false
let from_some: 'a option -> 'a = function
| Some(x) -> x
| None -> raise Not_found
let filter_some (l: 'a option list): 'a list =
List.(map from_some (filter is_some l))
type 'a or_err =
| OK of 'a
| ERR of string
let is_ok: 'a or_err -> bool = function
| OK(_) -> true
| ERR(_) -> false
let is_err x = not (is_ok x)
let from_ok: 'a or_err -> 'a = function
| OK(x) -> x
| ERR(_) -> assert false
let from_err: 'a or_err -> string = function
| OK(_) -> assert false
| ERR(s) -> s
let filter_ok (l: 'a or_err list): 'a list =
List.(map from_ok (filter is_ok l))
let filter_err (l: 'a or_err list): string list =
List.(map from_err (filter is_err l))
external id : 'a -> 'a = "%identity"
(** [a; a + 1; ... ; b - 1; b] *)
let list_ab (a: int) (b: int): int list =
let rec list_ab_aux a b res =
if b < a
then res
else list_ab_aux a (b - 1) (b :: res)
in list_ab_aux a b []
(** [0; 1; ...; n - 1] *)
let list_n (n: int): int list =
list_ab 0 (n - 1)
(** Checks for existence of an array element satisfying a condition, and returns
its index if it exists.
*)
let array_exists (cond: 'a -> bool) (arr: 'a array): int option =
let rec array_exists_aux ndx =
if ndx < 0
then None
else if cond arr.(ndx)
then Some ndx
else array_exists_aux (ndx - 1)
in array_exists_aux (Array.length arr - 1)
exception IntOverflow
exception Int32Overflow
(* Can only return positive numbers 0 <= res < 2^31 *)
let positive_int32 p =
let rec positive_int32_unsafe = function
| P.Coq_xI(p) -> Int32.(add (shift_left (positive_int32_unsafe p) 1) 1l)
| P.Coq_xO(p) -> Int32.(shift_left (positive_int32_unsafe p) 1)
| P.Coq_xH -> 1l
in
let res = positive_int32_unsafe p in
if res >= 0l
then res
else raise IntOverflow
(* This allows for 1 bit of overflow, effectively returning a negative *)
let rec positive_int32_lax = function
| P.Coq_xI(p) ->
let acc = positive_int32_lax p in
if acc < 0l
then raise Int32Overflow
else Int32.(add (shift_left acc 1) 1l)
| P.Coq_xO(p) ->
let acc = positive_int32_lax p in
if acc < 0l
then raise Int32Overflow
else Int32.shift_left acc 1
| P.Coq_xH -> 1l
let z_int32 = function
| Z.Z0 -> 0l
| Z.Zpos(p) -> positive_int32 p
| Z.Zneg(p) -> Int32.neg (positive_int32 p)
let z_int32_lax = function
| Z.Z0 -> 0l
| Z.Zpos(p) -> positive_int32_lax p
| Z.Zneg(_) -> raise Int32Overflow
let z_int z = Safe32.to_int (z_int32 z)
let z_int_lax z = Safe32.to_int (z_int32_lax z)
let z_int64 = Camlcoq.Z.to_int64
(* Some more printers *)
let string_of_ffloat f = string_of_float (camlfloat_of_coqfloat f)
let string_of_ffloat32 f = string_of_float (camlfloat_of_coqfloat32 f)
let string_of_array string_of_elt sep a =
let b = Buffer.create 1024 in
Buffer.add_string b "[\n";
Array.iteri
(fun ndx elt ->
if ndx > 0 then Buffer.add_string b sep;
Buffer.add_string b (string_of_int ndx);
Buffer.add_string b ": ";
Buffer.add_string b (string_of_elt elt)
) a;
Buffer.add_string b "\n]";
Buffer.contents b
let string_of_list string_of_elt sep l =
String.concat sep (List.map string_of_elt l)
let string_of_bitstring bs =
let rec string_of_bitset_aux bs =
bitmatch bs with
| { bit : 1 : int ;
rest : -1 : bitstring } ->
(if bit then "1" else "0") ^ (string_of_bitset_aux rest)
| { _ } -> ""
in string_of_bitset_aux bs
(* To print addresses/offsets *)
let string_of_int32 = Printf.sprintf "0x%08lx"
let string_of_int64 = Printf.sprintf "0x%08Lx"
(* To print counts/indices *)
let string_of_int32i = Int32.to_string
let string_of_int64i = Int64.to_string
let string_of_positive p = string_of_int32i (positive_int32 p)
let string_of_z z = string_of_int32 (z_int32 z)
let sorted_lookup (compare: 'a -> 'b -> int) (arr: 'a array) (v: 'b): 'a option =
let rec sorted_lookup_aux (i_from: int) (i_to: int): 'a option =
if i_from > i_to
then None
else
let i_mid = (i_from + i_to) / 2 in
let comp = compare arr.(i_mid) v in
if comp < 0 (* v_mid < v *)
then sorted_lookup_aux (i_mid + 1) i_to
else if comp > 0
then sorted_lookup_aux i_from (i_mid - 1)
else Some(arr.(i_mid))
in sorted_lookup_aux 0 (Array.length arr - 1)
let list_false_indices a =
filter_some (Array.(to_list (mapi (fun ndx b -> if b then None else Some(ndx)) a)))
|
