diff options
Diffstat (limited to 'kernel/uint63.mli')
| -rw-r--r-- | kernel/uint63.mli | 28 |
1 files changed, 27 insertions, 1 deletions
diff --git a/kernel/uint63.mli b/kernel/uint63.mli index b5f40ca804..d22ba3468f 100644 --- a/kernel/uint63.mli +++ b/kernel/uint63.mli @@ -1,3 +1,13 @@ +(************************************************************************) +(* * 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) *) +(************************************************************************) + type t val uint_size : int @@ -13,7 +23,7 @@ val of_uint : int -> t val hash : t -> int - (* convertion to a string *) + (* conversion to a string *) val to_string : t -> string val of_string : string -> t @@ -37,9 +47,15 @@ val mul : t -> t -> t val div : t -> t -> t val rem : t -> t -> t +val diveucl : t -> t -> t * t + (* Specific arithmetic operations *) val mulc : t -> t -> t * t val addmuldiv : t -> t -> t -> t + +(** [div21 xh xl y] returns [q % 2^63, r] + s.t. [xh * 2^63 + xl = q * y + r] and [r < y]. + When [y] is [0], returns [0, 0]. *) val div21 : t -> t -> t -> t * t (* comparison *) @@ -53,3 +69,13 @@ val head0 : t -> t val tail0 : t -> t val is_uint63 : Obj.t -> bool + +(* Arithmetic with explicit carries *) + +(* Analog of Numbers.Abstract.Cyclic.carry *) +type 'a carry = C0 of 'a | C1 of 'a + +val addc : t -> t -> t carry +val addcarryc : t -> t -> t carry +val subc : t -> t -> t carry +val subcarryc : t -> t -> t carry |