From 9ca7e769b62173a79a1c7d12a363205dd608b519 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 1 Dec 2020 18:28:43 +0100
Subject: Make the code clearer and faster by calling mask63 explicitly at the
 end.

Before this commit, function mask63 was called implicitly at each step.
---
 kernel/uint63_31.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/uint63_31.ml')

diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml
index 5b2d934b5d..696efacb32 100644
--- a/kernel/uint63_31.ml
+++ b/kernel/uint63_31.ml
@@ -72,12 +72,12 @@ 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
+let addcarry x y = mask63 Int64.(add (add x y) one)
 
     (* subtraction *)
 let sub x y = mask63 (Int64.sub x y)
 
-let subcarry x y = sub (sub x y) Int64.one
+let subcarry x y = mask63 Int64.(sub (sub x y) one)
 
     (* multiplication *)
 let mul x y = mask63 (Int64.mul x y)
-- 
cgit v1.2.3


From 2422d7dee3fda9ac5e65636db937d3d98c85e576 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 1 Dec 2020 21:03:18 +0100
Subject: Greatly simplify the conversion functions between Z.t and Uint63.t.

---
 kernel/uint63_31.ml | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

(limited to 'kernel/uint63_31.ml')

diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml
index 696efacb32..3517f51bfc 100644
--- a/kernel/uint63_31.ml
+++ b/kernel/uint63_31.ml
@@ -26,6 +26,7 @@ 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_int64 i = i
 
 let to_int_min n m =
   if Int64.(compare n (of_int m)) < 0 then Int64.to_int n else m
@@ -41,13 +42,6 @@ let hash i =
     (* 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
 
-- 
cgit v1.2.3


From f4dcd1d9f696972e7cbdaa8d70e5abb1a18820ef Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 2 Dec 2020 06:44:10 +0100
Subject: Make sure the msb is clear.

This is presumably not usable from the surface language. But an ML module
could easily create a proof of false by passing a negative number to
Const.mkInt.
---
 kernel/uint63_31.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/uint63_31.ml')

diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml
index 3517f51bfc..988611df3e 100644
--- a/kernel/uint63_31.ml
+++ b/kernel/uint63_31.ml
@@ -23,9 +23,9 @@ let one = Int64.one
 
     (* conversion from an int *)
 let mask63 i = Int64.logand i maxuint63
-let of_int i = Int64.of_int i
+let of_int i = mask63 (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 of_int64 = mask63
 let to_int64 i = i
 
 let to_int_min n m =
-- 
cgit v1.2.3