package dolmen
A parser library for automated deduction
Install
Dune Dependency
Authors
Maintainers
Sources
dolmen-0.8.1.tbz
sha256=80fc33ae81817a79c6e6b2f6c01c4cfcc0af02bfe4d2d1b87cf70b84cdde3928
sha512=3a44a99bce871161bc70cf909c813e9e6c91c590873cbc163c69b2ec90ab5be65bf0bf45430bc8d00d85d75cf0af004b06b8f5f1c9d4d47c8a30ab9f28762c04
doc/src/dolmen.std/misc.ml.html
Source file misc.ml
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 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210
(* This file is free software, part of dolmen. See file "LICENSE" for more information. *) (* Extensions *) (* ************************************************************************* *) let get_extension s = let rec aux s i = if i <= 0 then "" else match s.[i] with | '.' -> String.sub s i (String.length s - i) | _ -> aux s (i - 1) in aux s (String.length s - 1) let replicate n x = let rec aux x acc i = if i <= 0 then acc else aux x (x :: acc) (i - 1) in aux x [] n let split_on_char sep s = let r = ref [] in let j = ref (String.length s) in for i = String.length s - 1 downto 0 do if String.unsafe_get s i = sep then begin r := String.sub s (i + 1) (!j - i - 1) :: !r; j := i end done; String.sub s 0 !j :: !r (* Hashs *) (* ************************************************************************* *) (* Taken from containres's CCHash, cf https://github.com/c-cube/ocaml-containers/blob/master/src/core/CCHash.ml *) let fnv_offset_basis = 0xcbf29ce484222325L let fnv_prime = 0x100000001b3L (* hash an integer *) let hash_int n = let h = ref fnv_offset_basis in for k = 0 to 7 do h := Int64.(mul !h fnv_prime); h := Int64.(logxor !h (of_int ((n lsr (k * 8)) land 0xff))); done; (Int64.to_int !h) land max_int (* truncate back to int and remove sign *) let hash_string (x:string) = let h = ref fnv_offset_basis in for i = 0 to String.length x - 1 do h := Int64.(mul !h fnv_prime); let byte = Char.code (String.unsafe_get x i) in h := Int64.(logxor !h (of_int byte)); done; Int64.to_int !h land max_int let hash2 a b = let h = ref fnv_offset_basis in (* we only do one loop, where we mix bytes of [a] and [b], so as to simplify control flow *) for k = 0 to 7 do h := Int64.(mul !h fnv_prime); h := Int64.(logxor !h (of_int ((a lsr (k * 8)) land 0xff))); h := Int64.(mul !h fnv_prime); h := Int64.(logxor !h (of_int ((b lsr (k * 8)) land 0xff))); done; Int64.to_int !h land max_int let hash3 a b c = let h = ref fnv_offset_basis in (* we only do one loop, where we mix bytes of [a] [b] and [c], so as to simplify control flow *) for k = 0 to 7 do h := Int64.(mul !h fnv_prime); h := Int64.(logxor !h (of_int ((a lsr (k * 8)) land 0xff))); h := Int64.(mul !h fnv_prime); h := Int64.(logxor !h (of_int ((b lsr (k * 8)) land 0xff))); h := Int64.(mul !h fnv_prime); h := Int64.(logxor !h (of_int ((c lsr (k * 8)) land 0xff))); done; Int64.to_int !h land max_int let hash4 a b c d = let h = ref fnv_offset_basis in for k = 0 to 7 do h := Int64.(mul !h fnv_prime); h := Int64.(logxor !h (of_int ((a lsr (k * 8)) land 0xff))); h := Int64.(mul !h fnv_prime); h := Int64.(logxor !h (of_int ((b lsr (k * 8)) land 0xff))); h := Int64.(mul !h fnv_prime); h := Int64.(logxor !h (of_int ((c lsr (k * 8)) land 0xff))); h := Int64.(mul !h fnv_prime); h := Int64.(logxor !h (of_int ((d lsr (k * 8)) land 0xff))); done; Int64.to_int !h land max_int let[@inline] hash_combine f s x = hash2 s (f x) let hash_list f l = List.fold_left (hash_combine f) 0x42 l (* Comparisons *) (* ************************************************************************* *) (* Useful shorthand for chaining comparisons *) let (<?>) i (cmp, x, y) = match i with | 0 -> cmp x y | _ -> i (* lexicographic comparison *) let lexicographic cmp l l' = let rec aux l l' = match l, l' with | [], [] -> 0 | _ :: _, [] -> 1 | [], _ :: _ -> -1 | x :: r, x' :: r' -> begin match cmp x x' with | 0 -> aux r r' | res -> res end in aux l l' (* Options *) (* ************************************************************************* *) let opt_map o f = match o with | None -> None | Some x -> Some (f x) let opt_bind o f = match o with | None -> None | Some x -> f x let pp_opt ?(none="<none>") pp b = function | Some t -> pp b t | None -> Printf.bprintf b "%s" none let print_opt ?(none="<none>") print fmt = function | Some t -> print fmt t | None -> Format.fprintf fmt "%s" none (* Lists *) (* ************************************************************************* *) let rec pp_list ~pp_sep ~sep ~pp b = function | [] -> () | [h] -> pp b h | h :: r -> Printf.bprintf b "%a%a%a" pp h pp_sep sep (pp_list ~pp_sep ~sep ~pp) r let rec print_list ~print_sep ~sep ~print fmt = function | [] -> () | [h] -> print fmt h | h :: r -> Format.fprintf fmt "%a%a%a" print h print_sep sep (print_list ~print_sep ~sep ~print) r (* Lexbufs *) (* ************************************************************************* *) let set_file buf filename = let open Lexing in buf.lex_curr_p <- {buf.lex_curr_p with pos_fname=filename;}; () let filename_of_input = function | `Contents (file, _) -> file | `File file -> file | `Stdin -> "<stdin>" let filename_of_input_source = function | `Raw (file, _) -> file | `File file -> file | `Stdin -> "<stdin>" let mk_lexbuf i = let filename = filename_of_input i in match i with | `Contents (_, s) -> let buf = Lexing.from_string s in set_file buf filename; buf, (fun () -> ()) | `Stdin -> let ch, cl = stdin, (fun () -> ()) in let buf = Lexing.from_channel ch in set_file buf filename; buf, cl | `File s -> let ch = open_in s in let cl = (fun () -> close_in ch) in let buf = Lexing.from_channel ch in set_file buf filename; buf, cl
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>