diff options
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/big.ml | 76 | ||||
| -rw-r--r-- | plugins/extraction/dune | 2 |
2 files changed, 38 insertions, 40 deletions
diff --git a/plugins/extraction/big.ml b/plugins/extraction/big.ml index 19055fd425..7228f709f1 100644 --- a/plugins/extraction/big.ml +++ b/plugins/extraction/big.ml @@ -8,63 +8,61 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** [Big] : a wrapper around ocaml [Big_int] with nicer names, +(** [Big] : a wrapper around ocaml [ZArith] with nicer names, and a few extraction-specific constructions *) -(** To be linked with [nums.(cma|cmxa)] *) +(** To be linked with [zarith] *) -open Big_int - -type big_int = Big_int.big_int +type big_int = Z.t (** The type of big integers. *) -let zero = zero_big_int +let zero = Z.zero (** The big integer [0]. *) -let one = unit_big_int +let one = Z.one (** The big integer [1]. *) -let two = big_int_of_int 2 +let two = Z.of_int 2 (** The big integer [2]. *) (** {6 Arithmetic operations} *) -let opp = minus_big_int +let opp = Z.neg (** Unary negation. *) -let abs = abs_big_int +let abs = Z.abs (** Absolute value. *) -let add = add_big_int +let add = Z.add (** Addition. *) -let succ = succ_big_int - (** Successor (add 1). *) +let succ = Z.succ +(** Successor (add 1). *) -let add_int = add_int_big_int +let add_int = Z.add (** Addition of a small integer to a big integer. *) -let sub = sub_big_int +let sub = Z.sub (** Subtraction. *) -let pred = pred_big_int +let pred = Z.pred (** Predecessor (subtract 1). *) -let mult = mult_big_int +let mult = Z.mul (** Multiplication of two big integers. *) -let mult_int = mult_int_big_int +let mult_int x y = Z.mul (Z.of_int x) y (** Multiplication of a big integer by a small integer *) -let square = square_big_int +let square x = Z.mul x x (** Return the square of the given big integer *) -let sqrt = sqrt_big_int +let sqrt = Z.sqrt (** [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 +let quomod = Z.div_rem (** Euclidean division of two big integers. The first part of the result is the quotient, the second part is the remainder. @@ -72,18 +70,18 @@ let quomod = quomod_big_int [a = q * b + r] and [0 <= r < |b|]. Raise [Division_by_zero] if the divisor is zero. *) -let div = div_big_int +let div = Z.div (** Euclidean quotient of two big integers. This is the first result [q] of [quomod_big_int] (see above). *) -let modulo = mod_big_int +let modulo = Z.(mod) (** Euclidean modulus of two big integers. This is the second result [r] of [quomod_big_int] (see above). *) -let gcd = gcd_big_int +let gcd = Z.gcd (** Greatest common divisor of two big integers. *) -let power = power_big_int_positive_big_int +let power = Z.pow (** Exponentiation functions. Return the big integer representing the first argument [a] raised to the power [b] (the second argument). Depending @@ -92,45 +90,45 @@ let power = power_big_int_positive_big_int (** {6 Comparisons and tests} *) -let sign = sign_big_int +let sign = Z.sign (** 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 +let compare = Z.compare (** [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 +let eq = Z.equal +let le = Z.leq +let ge = Z.geq +let lt = Z.lt +let gt = Z.gt (** Usual boolean comparisons between two big integers. *) -let max = max_big_int +let max = Z.max (** Return the greater of its two arguments. *) -let min = min_big_int +let min = Z.min (** Return the smaller of its two arguments. *) (** {6 Conversions to and from strings} *) -let to_string = string_of_big_int +let to_string = Z.to_string (** Return the string representation of the given big integer, in decimal (base 10). *) -let of_string = big_int_of_string +let of_string = Z.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 +let of_int = Z.of_int (** Convert a small integer to a big integer. *) -let is_int = is_int_big_int +let is_int = Z.fits_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, @@ -139,7 +137,7 @@ let is_int = is_int_big_int [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 +let to_int = Z.to_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. *) diff --git a/plugins/extraction/dune b/plugins/extraction/dune index 0c01dcd488..d9d675fe6a 100644 --- a/plugins/extraction/dune +++ b/plugins/extraction/dune @@ -2,6 +2,6 @@ (name extraction_plugin) (public_name coq.plugins.extraction) (synopsis "Coq's extraction plugin") - (libraries num coq.plugins.ltac)) + (libraries coq.plugins.ltac)) (coq.pp (modules g_extraction)) |