diff options
Diffstat (limited to 'checklink/Library.ml')
| -rw-r--r-- | checklink/Library.ml | 171 |
1 files changed, 0 insertions, 171 deletions
diff --git a/checklink/Library.ml b/checklink/Library.ml deleted file mode 100644 index 54bca411..00000000 --- a/checklink/Library.ml +++ /dev/null @@ -1,171 +0,0 @@ -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))) |