diff options
Diffstat (limited to 'kernel/uint63_31.ml')
| -rw-r--r-- | kernel/uint63_31.ml | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml index b8eccd19fb..e38389ca13 100644 --- a/kernel/uint63_31.ml +++ b/kernel/uint63_31.ml @@ -26,6 +26,13 @@ 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*) @@ -213,4 +220,8 @@ let () = Callback.register "uint63 one" one; Callback.register "uint63 sub" sub; Callback.register "uint63 subcarry" subcarry; - Callback.register "uint63 tail0" tail0 + Callback.register "uint63 tail0" tail0; + Callback.register "uint63 of_float" of_float; + Callback.register "uint63 to_float" to_float; + Callback.register "uint63 of_int" of_int; + Callback.register "uint63 to_int_min" to_int_min |