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_63.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_63.ml')
| -rw-r--r-- | kernel/uint63_63.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/kernel/uint63_63.ml b/kernel/uint63_63.ml index 1776f904d6..85b44528a7 100644 --- a/kernel/uint63_63.ml +++ b/kernel/uint63_63.ml @@ -27,8 +27,6 @@ let to_int2 i = (0,i) let of_int64 _i = assert false -let to_int_saturate i = i - let of_float = int_of_float external to_float : int -> (float [@unboxed]) @@ -104,6 +102,10 @@ let le (x : int) (y : int) = (x lxor 0x4000000000000000) <= (y lxor 0x4000000000000000) [@@ocaml.inline always] +let to_int_min n m = + if lt n m then n else m +[@@ocaml.inline always] + (* division of two numbers by one *) (* precondition: xh < y *) (* outputs: q, r s.t. x = q * y + r, r < y *) |