bigInt.ml 1.82 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

open Big_int

type t = big_int
let compare = compare_big_int

let zero = zero_big_int
18
let one = unit_big_int
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
let of_int = big_int_of_int

let succ = succ_big_int
let pred = pred_big_int

let add_int = add_int_big_int
let mul_int = mult_int_big_int

let add = add_big_int
let sub = sub_big_int
let mul = mult_big_int
let minus = minus_big_int

let sign = sign_big_int

let eq = eq_big_int
let lt = lt_big_int
let gt = gt_big_int
let le = le_big_int
let ge = ge_big_int

let euclidean_div_mod = quomod_big_int

let euclidean_div x y = fst (euclidean_div_mod x y)

let euclidean_mod x y = snd (euclidean_div_mod x y)

let computer_div_mod x y =
47
  let (q,r) as qr = quomod_big_int x y in
48
  (* we have x = q*y + r with 0 <= r < |y| *)
49
50
  if sign x >= 0 || sign r = 0 then qr
  else
51
    if sign y < 0
52
53
54
55
56
57
58
59
60
    then (pred q, add r y)
    else (succ q, sub r y)

let computer_div x y = fst (computer_div_mod x y)

let computer_mod x y = snd (computer_div_mod x y)

let min = min_big_int
let max = max_big_int
61
let abs = abs_big_int
62
63
64
65
66

let pow_int_pos = power_int_positive_int

let to_string = string_of_big_int
let of_string = big_int_of_string
67
68
let to_int = int_of_big_int