<commit_before>(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(* Invariant: the msb should be 0 *)
type t = Int64.t

let _ = assert (Sys.word_size = 32)

let uint_size = 63

let maxuint63 = 0x7FFF_FFFF_FFFF_FFFFL
let maxuint31 = 0x7FFF_FFFFL

let zero = Int64.zero
let one = Int64.one

    (* conversion from an int *)
let mask63 i = Int64.logand i maxuint63
let of_int i = Int64.of_int i
let to_int2 i = (Int64.to_int (Int64.shift_right_logical i 31), Int64.to_int i)
let of_int64 i = i

let to_int_min n m =
  if Int64.(compare n (of_int m)) < 0 then Int64.to_int n else m

let of_float f = mask63 (Int64.of_float f)
let to_float = Int64.to_float

let hash i =
  let (h,l) = to_int2 i in
  (*Hashset.combine h l*)
  h * 65599 + l

    (* conversion of an uint63 to a string *)
let to_string i = Int64.to_string i

let of_string s =
  let i64 = Int64.of_string s in
  if Int64.compare Int64.zero i64 <= 0
      && Int64.compare i64 maxuint63 <= 0
  then i64
  else raise (Failure "Int63.of_string")

(* Compiles an unsigned int to OCaml code *)
let compile i = Printf.sprintf "Uint63.of_int64 (%LiL)" i

    (* comparison *)
let lt x y =
  Int64.compare x y < 0

let le x y =
  Int64.compare x y <= 0

    (* logical shift *)
let l_sl x y =
  if le 0L y && lt y 63L then mask63 (Int64.shift_left x (Int64.to_int y)) else 0L

let l_sr x y =
  if le 0L y && lt y 63L then Int64.shift_right x (Int64.to_int y) else 0L

let l_and x y = Int64.logand x y
let l_or x y = Int64.logor x y
let l_xor x y = Int64.logxor x y

    (* addition of int63 *)
let add x y = mask63 (Int64.add x y)

let addcarry x y = add (add x y) Int64.one

    (* subtraction *)
let sub x y = mask63 (Int64.sub x y)

let subcarry x y = sub (sub x y) Int64.one

    (* multiplication *)
let mul x y = mask63 (Int64.mul x y)

    (* division *)
let div x y =
  if y = 0L then 0L else Int64.div x y

    (* modulo *)
let rem x y =
  if y = 0L then 0L else Int64.rem x y

let diveucl x y = (div x y, rem x y)

let addmuldiv p x y =
  l_or (l_sl x p) (l_sr y Int64.(sub (of_int uint_size) p))

    (* division of two numbers by one *)
(* precondition: xh < y *)
(* outputs: q, r s.t. x = q * y + r, r < y *)
let div21 xh xl y =
  let nh = ref xh in
  let nl = ref xl in
  let q = ref 0L in
  for _i = 0 to 62 do
    (* invariants: 0 <= nh < y, nl = (xl*2^i) % 2^64,
       (q*y + nh) * 2^(63-i) + (xl % 2^(63-i)) = (xh%y) * 2^63 + xl *)
    nl := Int64.shift_left !nl 1;
    nh := Int64.logor (Int64.shift_left !nh 1) (Int64.shift_right_logical !nl 63);
    q := Int64.shift_left !q 1;
    (* TODO: use "Int64.unsigned_compare !nh y >= 0",
       once OCaml 4.08 becomes the minimal required version *)
    if Int64.compare !nh 0L < 0 || Int64.compare !nh y >= 0 then
      begin q := Int64.logor !q 1L; nh := Int64.sub !nh y; end
  done;
  !q, !nh

let div21 xh xl y =
  if Int64.compare y xh <= 0 then zero, zero else div21 xh xl y

     (* exact multiplication *)
let mulc x y =
  let lx = ref (Int64.logand x maxuint31) in
  let ly = ref (Int64.logand y maxuint31) in
  let hx = Int64.shift_right x 31 in
  let hy = Int64.shift_right y 31 in
  let hr = ref (Int64.mul hx hy) in
  let lr = ref (Int64.logor (Int64.mul !lx !ly) (Int64.shift_left !hr 62)) in
  hr := (Int64.shift_right_logical !hr 1);
  lx := Int64.mul !lx hy;
  ly := Int64.mul hx !ly;
  hr := Int64.logor !hr (Int64.add (Int64.shift_right !lx 32) (Int64.shift_right !ly 32));
  lr := Int64.add !lr (Int64.shift_left !lx 31);
  hr := Int64.add !hr (Int64.shift_right_logical !lr 63);
  lr := Int64.add (Int64.shift_left !ly 31) (mask63 !lr);
  hr := Int64.add !hr (Int64.shift_right_logical !lr 63);
  if Int64.logand !lr Int64.min_int <> 0L
  then Int64.(sub !hr one, mask63 !lr)
  else (!hr, !lr)

let equal x y = mask63 x = mask63 y
<commit_msg>Simplify equality of 63-bit integers.<commit_after>(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(* Invariant: the msb should be 0 *)
type t = Int64.t

let _ = assert (Sys.word_size = 32)

let uint_size = 63

let maxuint63 = 0x7FFF_FFFF_FFFF_FFFFL
let maxuint31 = 0x7FFF_FFFFL

let zero = Int64.zero
let one = Int64.one

    (* conversion from an int *)
let mask63 i = Int64.logand i maxuint63
let of_int i = Int64.of_int i
let to_int2 i = (Int64.to_int (Int64.shift_right_logical i 31), Int64.to_int i)
let of_int64 i = i

let to_int_min n m =
  if Int64.(compare n (of_int m)) < 0 then Int64.to_int n else m

let of_float f = mask63 (Int64.of_float f)
let to_float = Int64.to_float

let hash i =
  let (h,l) = to_int2 i in
  (*Hashset.combine h l*)
  h * 65599 + l

    (* conversion of an uint63 to a string *)
let to_string i = Int64.to_string i

let of_string s =
  let i64 = Int64.of_string s in
  if Int64.compare Int64.zero i64 <= 0
      && Int64.compare i64 maxuint63 <= 0
  then i64
  else raise (Failure "Int63.of_string")

(* Compiles an unsigned int to OCaml code *)
let compile i = Printf.sprintf "Uint63.of_int64 (%LiL)" i

    (* comparison *)
let lt x y =
  Int64.compare x y < 0

let le x y =
  Int64.compare x y <= 0

    (* logical shift *)
let l_sl x y =
  if le 0L y && lt y 63L then mask63 (Int64.shift_left x (Int64.to_int y)) else 0L

let l_sr x y =
  if le 0L y && lt y 63L then Int64.shift_right x (Int64.to_int y) else 0L

let l_and x y = Int64.logand x y
let l_or x y = Int64.logor x y
let l_xor x y = Int64.logxor x y

    (* addition of int63 *)
let add x y = mask63 (Int64.add x y)

let addcarry x y = add (add x y) Int64.one

    (* subtraction *)
let sub x y = mask63 (Int64.sub x y)

let subcarry x y = sub (sub x y) Int64.one

    (* multiplication *)
let mul x y = mask63 (Int64.mul x y)

    (* division *)
let div x y =
  if y = 0L then 0L else Int64.div x y

    (* modulo *)
let rem x y =
  if y = 0L then 0L else Int64.rem x y

let diveucl x y = (div x y, rem x y)

let addmuldiv p x y =
  l_or (l_sl x p) (l_sr y Int64.(sub (of_int uint_size) p))

    (* division of two numbers by one *)
(* precondition: xh < y *)
(* outputs: q, r s.t. x = q * y + r, r < y *)
let div21 xh xl y =
  let nh = ref xh in
  let nl = ref xl in
  let q = ref 0L in
  for _i = 0 to 62 do
    (* invariants: 0 <= nh < y, nl = (xl*2^i) % 2^64,
       (q*y + nh) * 2^(63-i) + (xl % 2^(63-i)) = (xh%y) * 2^63 + xl *)
    nl := Int64.shift_left !nl 1;
    nh := Int64.logor (Int64.shift_left !nh 1) (Int64.shift_right_logical !nl 63);
    q := Int64.shift_left !q 1;
    (* TODO: use "Int64.unsigned_compare !nh y >= 0",
       once OCaml 4.08 becomes the minimal required version *)
    if Int64.compare !nh 0L < 0 || Int64.compare !nh y >= 0 then
      begin q := Int64.logor !q 1L; nh := Int64.sub !nh y; end
  done;
  !q, !nh

let div21 xh xl y =
  if Int64.compare y xh <= 0 then zero, zero else div21 xh xl y

     (* exact multiplication *)
let mulc x y =
  let lx = ref (Int64.logand x maxuint31) in
  let ly = ref (Int64.logand y maxuint31) in
  let hx = Int64.shift_right x 31 in
  let hy = Int64.shift_right y 31 in
  let hr = ref (Int64.mul hx hy) in
  let lr = ref (Int64.logor (Int64.mul !lx !ly) (Int64.shift_left !hr 62)) in
  hr := (Int64.shift_right_logical !hr 1);
  lx := Int64.mul !lx hy;
  ly := Int64.mul hx !ly;
  hr := Int64.logor !hr (Int64.add (Int64.shift_right !lx 32) (Int64.shift_right !ly 32));
  lr := Int64.add !lr (Int64.shift_left !lx 31);
  hr := Int64.add !hr (Int64.shift_right_logical !lr 63);
  lr := Int64.add (Int64.shift_left !ly 31) (mask63 !lr);
  hr := Int64.add !hr (Int64.shift_right_logical !lr 63);
  if Int64.logand !lr Int64.min_int <> 0L
  then Int64.(sub !hr one, mask63 !lr)
  else (!hr, !lr)

let equal (x : t) y = x = y

{'fraction_non_alphanumeric': 0.1617613764998868, 'fraction_numerical': 0.06701381027846955, 'mean_word_length': 2.7420584498094027, 'pattern_counts': {'":': 0, '<': 29, '<?xml version=': 0, '>': 9, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1414341', 'n_tokens_mistral': 3800, 'n_tokens_neox': 3328, 'n_words': 1245}