diff options
| author | Pierre Roux | 2019-10-10 20:11:02 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-11-01 10:21:35 +0100 |
| commit | d39fab9a7c39d8da868c4481b96cf1086c21b1a4 (patch) | |
| tree | 4d544f1407d0a082c5c60740a6f456aa250fd593 /kernel/uint63_31.ml | |
| parent | 40df8d4c451a09e82a5da29a2c3309dedebc64de (diff) | |
Fix ldshiftexp
* Fix the implementations and add tests
* Change shift from int63 to Z (was always used as a Z)
* Update FloatLemmas.v accordingly
Co-authored-by: Erik Martin-Dorel <erik.martin-dorel@irit.fr>
Diffstat (limited to 'kernel/uint63_31.ml')
| -rw-r--r-- | kernel/uint63_31.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml index a5646e87c3..e38389ca13 100644 --- a/kernel/uint63_31.ml +++ b/kernel/uint63_31.ml @@ -27,9 +27,8 @@ 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_saturate i = - let r = if Int64.(equal (logand i maxuint31) i) then i else maxuint31 in - Int64.to_int r +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 @@ -225,4 +224,4 @@ let () = 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_saturate" to_int_saturate + Callback.register "uint63 to_int_min" to_int_min |