bigInt.mli 1.92 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
9
(*                                                                  *)
10
(********************************************************************)
11 12 13 14 15 16 17

type t

val compare : t -> t -> int

(** constants *)
val zero : t
18
val one : t
19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38
val of_int : int -> t

(** basic operations *)
val succ : t -> t
val pred : t -> t
val add_int : int -> t -> t
val mul_int : int -> t -> t
val add : t -> t -> t
val sub : t -> t -> t
val mul : t -> t -> t
val minus : t -> t
val sign : t -> int

(** comparisons *)
val eq : t -> t -> bool
val lt : t -> t -> bool
val gt : t -> t -> bool
val le : t -> t -> bool
val ge : t -> t -> bool

39
(** Division and modulo operators with the convention
40 41 42 43 44 45
that modulo is always non-negative.

It implies that division rounds down when divisor is positive, and
rounds up when divisor is negative.
*)
val euclidean_div_mod : t -> t -> t * t
46 47
val euclidean_div : t -> t -> t
val euclidean_mod : t -> t -> t
48 49 50 51 52

(** "computer" division, i.e division rounds towards zero, and thus [mod
    x y] has the same sign as x
*)
val computer_div_mod : t -> t -> t * t
53 54
val computer_div : t -> t -> t
val computer_mod : t -> t -> t
55

56
(** min, max, abs *)
57 58
val min : t -> t -> t
val max : t -> t -> t
59
val abs : t -> t
60 61 62 63

(** power of small integers. Second arg must be non-negative *)
val pow_int_pos : int -> int -> t

64
(** conversions *)
65 66
val of_string : string -> t
val to_string : t -> string
67
val to_int : t -> int