1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
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
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <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) *)
(************************************************************************)
(** [Big] : a wrapper around ocaml [Big_int] with nicer names,
and a few extraction-specific constructions *)
(** To be linked with [nums.(cma|cmxa)] *)
open Big_int
type big_int = Big_int.big_int
(** The type of big integers. *)
let zero = zero_big_int
(** The big integer [0]. *)
let one = unit_big_int
(** The big integer [1]. *)
let two = big_int_of_int 2
(** The big integer [2]. *)
(** {6 Arithmetic operations} *)
let opp = minus_big_int
(** Unary negation. *)
let abs = abs_big_int
(** Absolute value. *)
let add = add_big_int
(** Addition. *)
let succ = succ_big_int
(** Successor (add 1). *)
let add_int = add_int_big_int
(** Addition of a small integer to a big integer. *)
let sub = sub_big_int
(** Subtraction. *)
let pred = pred_big_int
(** Predecessor (subtract 1). *)
let mult = mult_big_int
(** Multiplication of two big integers. *)
let mult_int = mult_int_big_int
(** Multiplication of a big integer by a small integer *)
let square = square_big_int
(** Return the square of the given big integer *)
let sqrt = sqrt_big_int
(** [sqrt_big_int a] returns the integer square root of [a],
that is, the largest big integer [r] such that [r * r <= a].
Raise [Invalid_argument] if [a] is negative. *)
let quomod = quomod_big_int
(** Euclidean division of two big integers.
The first part of the result is the quotient,
the second part is the remainder.
Writing [(q,r) = quomod_big_int a b], we have
[a = q * b + r] and [0 <= r < |b|].
Raise [Division_by_zero] if the divisor is zero. *)
let div = div_big_int
(** Euclidean quotient of two big integers.
This is the first result [q] of [quomod_big_int] (see above). *)
let modulo = mod_big_int
(** Euclidean modulus of two big integers.
This is the second result [r] of [quomod_big_int] (see above). *)
let gcd = gcd_big_int
(** Greatest common divisor of two big integers. *)
let power = power_big_int_positive_big_int
(** Exponentiation functions. Return the big integer
representing the first argument [a] raised to the power [b]
(the second argument). Depending
on the function, [a] and [b] can be either small integers
or big integers. Raise [Invalid_argument] if [b] is negative. *)
(** {6 Comparisons and tests} *)
let sign = sign_big_int
(** Return [0] if the given big integer is zero,
[1] if it is positive, and [-1] if it is negative. *)
let compare = compare_big_int
(** [compare_big_int a b] returns [0] if [a] and [b] are equal,
[1] if [a] is greater than [b], and [-1] if [a] is smaller
than [b]. *)
let eq = eq_big_int
let le = le_big_int
let ge = ge_big_int
let lt = lt_big_int
let gt = gt_big_int
(** Usual boolean comparisons between two big integers. *)
let max = max_big_int
(** Return the greater of its two arguments. *)
let min = min_big_int
(** Return the smaller of its two arguments. *)
(** {6 Conversions to and from strings} *)
let to_string = string_of_big_int
(** Return the string representation of the given big integer,
in decimal (base 10). *)
let of_string = big_int_of_string
(** Convert a string to a big integer, in decimal.
The string consists of an optional [-] or [+] sign,
followed by one or several decimal digits. *)
(** {6 Conversions to and from other numerical types} *)
let of_int = big_int_of_int
(** Convert a small integer to a big integer. *)
let is_int = is_int_big_int
(** Test whether the given big integer is small enough to
be representable as a small integer (type [int])
without loss of precision. On a 32-bit platform,
[is_int_big_int a] returns [true] if and only if
[a] is between 2{^30} and 2{^30}-1. On a 64-bit platform,
[is_int_big_int a] returns [true] if and only if
[a] is between -2{^62} and 2{^62}-1. *)
let to_int = int_of_big_int
(** Convert a big integer to a small integer (type [int]).
Raises [Failure "int_of_big_int"] if the big integer
is not representable as a small integer. *)
(** Functions used by extraction *)
let double x = mult_int 2 x
let doubleplusone x = succ (double x)
let nat_case fO fS n = if sign n <= 0 then fO () else fS (pred n)
let positive_case f2p1 f2p f1 p =
if le p one then f1 () else
let (q,r) = quomod p two in if eq r zero then f2p q else f2p1 q
let n_case fO fp n = if sign n <= 0 then fO () else fp n
let z_case fO fp fn z =
let s = sign z in
if s = 0 then fO () else if s > 0 then fp z else fn (opp z)
let compare_case e l g x y =
let s = compare x y in if s = 0 then e else if s<0 then l else g
let nat_rec fO fS =
let rec loop acc n =
if sign n <= 0 then acc else loop (fS acc) (pred n)
in loop fO
let positive_rec f2p1 f2p f1 =
let rec loop n =
if le n one then f1
else
let (q,r) = quomod n two in
if eq r zero then f2p (loop q) else f2p1 (loop q)
in loop
let z_rec fO fp fn = z_case (fun _ -> fO) fp fn
|
