Extraction: in support library, more and nicer big_int

 - we use a wrapper file big.ml to have short names about big_int
 and specialized functions for extraction
 - new files : ExtrOcamlZInt for Z==>int and N==>int,
 ExtrOcamlZBigInt for Z==>big_int and N==>big_int

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13137 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 390 insertions, 65 deletions

diff --git a/plugins/extraction/ExtrOcamlBigIntConv.v b/plugins/extraction/ExtrOcamlBigIntConv.v
index 9f80812db..b4490545c 100644
--- a/plugins/extraction/ExtrOcamlBigIntConv.v
+++ b/plugins/extraction/ExtrOcamlBigIntConv.v
@@ -8,7 +8,10 @@
 
 (** Extraction to Ocaml: conversion from/to [big_int] *)
 
-(** The extracted code should be linked with [nums.(cma|cmxa)] *)
+(** NB: The extracted code should be linked with [nums.cm(x)a]
+    from ocaml's stdlib and with the wrapper [big.ml] that
+    simlifies the use of [Big_int] (it could be found in the sources
+    of Coq). *)
 
 Require Import Arith ZArith.
 
@@ -18,11 +21,11 @@ Parameter bigint_succ : bigint -> bigint.
 Parameter bigint_opp : bigint -> bigint.
 Parameter bigint_twice : bigint -> bigint.
 
-Extract Inlined Constant bigint => "Big_int.big_int".
-Extract Inlined Constant bigint_zero => "Big_int.zero_big_int".
-Extract Inlined Constant bigint_succ => "Big_int.succ_big_int".
-Extract Inlined Constant bigint_opp => "Big_int.minus_big_int".
-Extract Inlined Constant bigint_twice => "Big_int.mult_int_big_int 2".
+Extract Inlined Constant bigint => "Big.big_int".
+Extract Inlined Constant bigint_zero => "Big.zero".
+Extract Inlined Constant bigint_succ => "Big.succ".
+Extract Inlined Constant bigint_opp => "Big.opp".
+Extract Inlined Constant bigint_twice => "Big.double".
 
 Definition bigint_of_nat : nat -> bigint :=
  (fix loop acc n :=
@@ -56,43 +59,50 @@ Fixpoint bigint_of_n n :=
     non-positive inputs. *)
 
 Parameter bigint_natlike_rec : forall A, A -> (A->A) -> bigint -> A.
-Extract Constant bigint_natlike_rec =>
-"fun fO fS ->
- let rec loop acc i = if Big_int.sign_big_int i <= 0 then acc
-  else loop (fS acc) (Big_int.pred_big_int i)
- in loop fO".
+Extract Constant bigint_natlike_rec => "Big.nat_rec".
 
 Definition nat_of_bigint : bigint -> nat := bigint_natlike_rec _ O S.
 
-Parameter bigint_poslike_rec : forall A, A -> (A->A) -> (A->A) -> bigint -> A.
-Extract Constant bigint_poslike_rec =>
-"fun f1 f2x f2x1 ->
- let rec loop i = if Big_int.le_big_int i Big_int.unit_big_int then f1
- else
-  let (q,r) = Big_int.quomod_big_int i (Big_int.big_int_of_int 2) in
-  if Big_int.sign_big_int r = 0 then f2x (loop q) else f2x1 (loop q)
- in loop".
+Parameter bigint_poslike_rec : forall A, (A->A) -> (A->A) -> A -> bigint -> A.
+Extract Constant bigint_poslike_rec => "Big.positive_rec".
 
-Definition pos_of_bigint : bigint -> positive := bigint_poslike_rec _ xH xO xI.
+Definition pos_of_bigint : bigint -> positive := bigint_poslike_rec _ xI xO xH.
 
-Parameter bigint_zlike_case : forall A, A -> (bigint->A) -> (bigint->A) -> bigint -> A.
-Extract Constant bigint_zlike_case =>
-"fun f0 fpos fneg i ->
-  let sgn = Big_int.sign_big_int i in
-  if sgn = 0 then f0 else if sgn>0 then fpos i
-  else fneg (Big_int.minus_big_int i)".
+Parameter bigint_zlike_case :
+ forall A, A -> (bigint->A) -> (bigint->A) -> bigint -> A.
+Extract Constant bigint_zlike_case => "Big.z_rec".
 
 Definition z_of_bigint : bigint -> Z :=
  bigint_zlike_case _ Z0 (fun i => Zpos (pos_of_bigint i))
-                     (fun i => Zneg (pos_of_bigint i)).
+                        (fun i => Zneg (pos_of_bigint i)).
 
 Definition n_of_bigint : bigint -> N :=
  bigint_zlike_case _ N0 (fun i => Npos (pos_of_bigint i)) (fun _ => N0).
 
-(*
-Extraction "/tmp/test.ml"
-  nat_of_bigint bigint_of_nat
-  pos_of_bigint bigint_of_pos
-  z_of_bigint bigint_of_z
-  n_of_bigint bigint_of_n.
+(* Tests:
+
+Definition small := 1234%nat.
+Definition big := 12345678901234567890%positive.
+
+Definition nat_0 := nat_of_bigint (bigint_of_nat 0).
+Definition nat_1 := nat_of_bigint (bigint_of_nat small).
+Definition pos_1 := pos_of_bigint (bigint_of_pos 1).
+Definition pos_2 := pos_of_bigint (bigint_of_pos big).
+Definition n_0 := n_of_bigint (bigint_of_n 0).
+Definition n_1 := n_of_bigint (bigint_of_n 1).
+Definition n_2 := n_of_bigint (bigint_of_n (Npos big)).
+Definition z_0 := z_of_bigint (bigint_of_z 0).
+Definition z_1 := z_of_bigint (bigint_of_z 1).
+Definition z_2 := z_of_bigint (bigint_of_z (Zpos big)).
+Definition z_m1 := z_of_bigint (bigint_of_z (-1)).
+Definition z_m2 := z_of_bigint (bigint_of_z (Zneg big)).
+
+Definition test :=
+ (nat_0, nat_1, pos_1, pos_2, n_0, n_1, n_2, z_0, z_1, z_2, z_m1, z_m2).
+Definition check :=
+ (O, small, xH, big, 0%N, 1%N, Npos big, 0%Z, 1%Z, Zpos big, (-1)%Z, Zneg big).
+
+Extraction "/tmp/test.ml" check test.
+
+... and we check that test=check
 *)
\ No newline at end of file
diff --git a/plugins/extraction/ExtrOcamlNatBigInt.v b/plugins/extraction/ExtrOcamlNatBigInt.v
index 22c3a133b..e2051e110 100644
--- a/plugins/extraction/ExtrOcamlNatBigInt.v
+++ b/plugins/extraction/ExtrOcamlNatBigInt.v
@@ -11,7 +11,10 @@
 Require Import Arith Even Div2 EqNat Euclid.
 Require Import ExtrOcamlBasic.
 
-(** NB: The extracted code should be linked with [nums.(cma|cmxa)]. *)
+(** NB: The extracted code should be linked with [nums.cm(x)a]
+    from ocaml's stdlib and with the wrapper [big.ml] that
+    simlifies the use of [Big_int] (it could be found in the sources
+    of Coq). *)
 
 (** Disclaimer: trying to obtain efficient certified programs
     by extracting [nat] into [big_int] isn't necessarily a good idea.
@@ -22,52 +25,45 @@ Require Import ExtrOcamlBasic.
 (** Mapping of [nat] into [big_int]. The last string corresponds to
     a [nat_case], see documentation of [Extract Inductive]. *)
 
-Extract Inductive nat => "Big_int.big_int"
- [ "Big_int.zero_big_int" "Big_int.succ_big_int" ]
- "(fun fO fS n -> if Big_int.sign_big_int n = 0 then fO () else fS (Big_int.pred_big_int n))".
+Extract Inductive nat => "Big.big_int" [ "Big.zero" "Big.succ" ]
+ "Big.nat_case".
 
 (** Efficient (but uncertified) versions for usual [nat] functions *)
 
-Extract Constant plus => "Big_int.add_big_int".
-Extract Constant mult => "Big_int.mult_big_int".
-Extract Constant pred =>
- "fun n -> Big_int.max_big_int Big_int.zero_big_int (Big_int.pred_big_int n)".
-Extract Constant minus =>
- "fun n m -> Big_int.max_big_int Big_int.zero_big_int (Big_int.sub_big_int n m)".
-Extract Constant max => "Big_int.max_big_int".
-Extract Constant min => "Big_int.min_big_int".
-Extract Constant nat_beq => "Big_int.eq_big_int".
-Extract Constant EqNat.beq_nat => "Big_int.eq_big_int".
-Extract Constant EqNat.eq_nat_decide => "Big_int.eq_big_int".
+Extract Constant plus => "Big.add".
+Extract Constant mult => "Big.mult".
+Extract Constant pred => "fun n -> Big.max Big.zero (Big.pred n)".
+Extract Constant minus => "fun n m -> Big.max Big.zero (Big.sub n m)".
+Extract Constant max => "Big.max".
+Extract Constant min => "Big.min".
+Extract Constant nat_beq => "Big.eq".
+Extract Constant EqNat.beq_nat => "Big.eq".
+Extract Constant EqNat.eq_nat_decide => "Big.eq".
 
-Extract Inlined Constant Peano_dec.eq_nat_dec => "Big_int.eq_big_int".
+Extract Constant Peano_dec.eq_nat_dec => "Big.eq".
 
 Extract Constant Compare_dec.nat_compare =>
-"fun n m ->
- let s = Big_int.compare_big_int n m in
- if s=0 then Eq else if s<0 then Lt else Gt".
+ "Big.compare_case Eq Lt Gt".
 
-Extract Inlined Constant Compare_dec.leb => "Big_int.le_big_int".
-Extract Inlined Constant Compare_dec.le_lt_dec => "Big_int.le_big_int".
+Extract Constant Compare_dec.leb => "Big.le".
+Extract Constant Compare_dec.le_lt_dec => "Big.le".
 Extract Constant Compare_dec.lt_eq_lt_dec =>
-"fun n m ->
- let s = Big_int.sign_big_int n m in
- if s>0 then None else Some (s<0)".
+ "Big.compare_case (Some false) (Some true) None".
 
 Extract Constant Even.even_odd_dec =>
- "fun n -> Big_int.sign_big_int (Big_int.mod_big_int n (Big_int.big_int_of_int 2)) = 0".
-Extract Constant Div2.div2 =>
- "fun n -> Big_int.div_big_int n (Big_int.big_int_of_int 2)".
+ "fun n -> Big.sign (Big.mod n Big.two) = 0".
+Extract Constant Div2.div2 => "fun n -> Big.div n Big.two".
 
-Extract Inductive Euclid.diveucl => "(Big_int.big_int * Big_int.big_int)" [""].
-Extract Constant Euclid.eucl_dev => "fun n m -> Big_int.quomod_big_int m n".
-Extract Constant Euclid.quotient => "fun n m -> Big_int.div_big_int m n".
-Extract Constant Euclid.modulo => "fun n m -> Big_int.mod_big_int m n".
+Extract Inductive Euclid.diveucl => "(Big.big_int * Big.big_int)" [""].
+Extract Constant Euclid.eucl_dev => "fun n m -> Big.quomod m n".
+Extract Constant Euclid.quotient => "fun n m -> Big.div m n".
+Extract Constant Euclid.modulo => "fun n m -> Big.modulo m n".
 
 (*
+Require Import Euclid.
 Definition test n m (H:m>0) :=
  let (q,r,_,_) := eucl_dev m H n in
  nat_compare n (q*m+r).
 
-Recursive Extraction test fact.
+Extraction "/tmp/test.ml" test fact pred minus max min Div2.div2.
 *)
diff --git a/plugins/extraction/ExtrOcamlZBigInt.v b/plugins/extraction/ExtrOcamlZBigInt.v
new file mode 100644
index 000000000..8b05ca290
--- /dev/null
+++ b/plugins/extraction/ExtrOcamlZBigInt.v
@@ -0,0 +1,85 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Extraction of [positive], [N] and [Z] into Ocaml's [big_int] *)
+
+Require Import ZArith NArith.
+Require Import ExtrOcamlBasic.
+
+(** NB: The extracted code should be linked with [nums.cm(x)a]
+    from ocaml's stdlib and with the wrapper [big.ml] that
+    simlifies the use of [Big_int] (it could be found in the sources
+    of Coq). *)
+
+(** Disclaimer: trying to obtain efficient certified programs
+    by extracting [Z] into [big_int] isn't necessarily a good idea.
+    See the Disclaimer in [ExtrOcamlNatInt]. *)
+
+(** Mapping of [positive], [Z], [N] into [big_int]. The last strings
+    emulate the matching, see documentation of [Extract Inductive]. *)
+
+Extract Inductive positive => "Big.big_int"
+ [ "Big.doubleplusone" "Big.double" "Big.one" ] "Big.positive_case".
+
+Extract Inductive Z => "Big.big_int"
+ [ "Big.zero" "" "Big.opp" ] "Big.z_case".
+
+Extract Inductive N => "Big.big_int"
+ [ "Big.zero" "" ] "Big.n_case".
+
+(** Nota: the "" above is used as an identity function "(fun p->p)" *)
+
+(** Efficient (but uncertified) versions for usual functions *)
+
+Extract Constant Pplus => "Big.add".
+Extract Constant Psucc => "Big.succ".
+Extract Constant Ppred => "fun n -> Big.max Big.one (Big.pred n)".
+Extract Constant Pminus => "fun n m -> Big.max Big.one (Big.sub n m)".
+Extract Constant Pmult => "Big.mult".
+Extract Constant Pmin => "Big.min".
+Extract Constant Pmax => "Big.max".
+Extract Constant Pcompare =>
+ "fun x y c -> Big.compare_case c Lt Gt x y".
+
+Extract Constant Nplus => "Big.add".
+Extract Constant Nsucc => "Big.succ".
+Extract Constant Npred => "fun n -> Big.max Big.zero (Big.pred n)".
+Extract Constant Nminus => "fun n m -> Big.max Big.zero (Big.sub n m)".
+Extract Constant Nmult => "Big.mult".
+Extract Constant Nmin => "Big.min".
+Extract Constant Nmax => "Big.max".
+Extract Constant Ndiv =>
+ "fun a b -> if Big.eq b Big.zero then Big.zero else Big.div a b".
+Extract Constant Nmod =>
+ "fun a b -> if Big.eq b Big.zero then Big.zero else Big.modulo a b".
+Extract Constant Ncompare => "Big.compare_case Eq Lt Gt".
+
+Extract Constant Zplus => "Big.add".
+Extract Constant Zsucc => "Big.succ".
+Extract Constant Zpred => "Big.pred".
+Extract Constant Zminus => "Big.sub".
+Extract Constant Zmult => "Big.mult".
+Extract Constant Zopp => "Big.opp".
+Extract Constant Zabs => "Big.abs".
+Extract Constant Zmin => "Big.min".
+Extract Constant Zmax => "Big.max".
+Extract Constant Zcompare => "Big.compare_case Eq Lt Gt".
+
+Extract Constant Z_of_N => "fun p -> p".
+Extract Constant Zabs_N => "Big.abs".
+
+(** Zdiv and Zmod are quite complex to define in terms of (/) and (mod).
+    For the moment we don't even try *)
+
+(** Test:
+Require Import ZArith NArith.
+
+Extraction "/tmp/test.ml"
+ Pplus Ppred Pminus Pmult Pcompare Npred Nminus Ndiv Nmod Ncompare
+ Zplus Zmult BinInt.Zcompare Z_of_N Zabs_N Zdiv.Zdiv Zmod.
+*)
diff --git a/plugins/extraction/ExtrOcamlZInt.v b/plugins/extraction/ExtrOcamlZInt.v
new file mode 100644
index 000000000..f96572120
--- /dev/null
+++ b/plugins/extraction/ExtrOcamlZInt.v
@@ -0,0 +1,78 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Extraction of [positive], [N] and [Z] into Ocaml's [int] *)
+
+Require Import ZArith NArith.
+Require Import ExtrOcamlBasic.
+
+(** Disclaimer: trying to obtain efficient certified programs
+    by extracting [Z] into [int] is definitively *not* a good idea.
+    See the Disclaimer in [ExtrOcamlNatInt]. *)
+
+(** Mapping of [positive], [Z], [N] into [int]. The last strings
+    emulate the matching, see documentation of [Extract Inductive]. *)
+
+Extract Inductive positive => int
+[ "(fun p->1+2*p)" "(fun p->2*p)" "1" ]
+"(fun f2p1 f2p f1 p ->
+  if p<=1 then f1 () else if p mod 2 = 0 then f2p (p/2) else f2p1 (p/2))".
+
+Extract Inductive Z => int [ "0" "" "(~-)" ]
+"(fun f0 fp fn z -> if z=0 then f0 () else if z>0 then fp z else fn (-z))".
+
+Extract Inductive N => int [ "0" "" ]
+"(fun f0 fp n -> if n=0 then f0 () else fp n)".
+
+(** Nota: the "" above is used as an identity function "(fun p->p)" *)
+
+(** Efficient (but uncertified) versions for usual functions *)
+
+Extract Constant Pplus => "(+)".
+Extract Constant Psucc => "succ".
+Extract Constant Ppred => "fun n -> max 1 (n-1)".
+Extract Constant Pminus => "fun n m -> max 1 (n-m)".
+Extract Constant Pmult => "( * )".
+Extract Constant Pmin => "min".
+Extract Constant Pmax => "max".
+Extract Constant Pcompare =>
+ "fun x y c -> if x=y then c else if x<y then Lt else Gt".
+
+
+Extract Constant Nplus => "(+)".
+Extract Constant Nsucc => "succ".
+Extract Constant Npred => "fun n -> max 0 (n-1)".
+Extract Constant Nminus => "fun n m -> max 0 (n-m)".
+Extract Constant Nmult => "( * )".
+Extract Constant Nmin => "min".
+Extract Constant Nmax => "max".
+Extract Constant Ndiv => "fun a b -> if b=0 then 0 else a/b".
+Extract Constant Nmod => "fun a b -> if b=0 then a else a mod b".
+Extract Constant Ncompare =>
+ "fun x y -> if x=y then Eq else if x<y then Lt else Gt".
+
+
+Extract Constant Zplus => "(+)".
+Extract Constant Zsucc => "succ".
+Extract Constant Zpred => "pred".
+Extract Constant Zminus => "(-)".
+Extract Constant Zmult => "( * )".
+Extract Constant Zopp => "(~-)".
+Extract Constant Zabs => "abs".
+Extract Constant Zmin => "min".
+Extract Constant Zmax => "max".
+Extract Constant Zcompare =>
+ "fun x y -> if x=y then Eq else if x<y then Lt else Gt".
+
+Extract Constant Z_of_N => "fun p -> p".
+Extract Constant Zabs_N => "abs".
+
+(** Zdiv and Zmod are quite complex to define in terms of (/) and (mod).
+    For the moment we don't even try *)
+
+
diff --git a/plugins/extraction/big.ml b/plugins/extraction/big.ml
new file mode 100644
index 000000000..9a5bf56bc
--- /dev/null
+++ b/plugins/extraction/big.ml
@@ -0,0 +1,154 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** [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
diff --git a/plugins/extraction/vo.itarget b/plugins/extraction/vo.itarget
index 338b27684..1fe09f6fa 100644
--- a/plugins/extraction/vo.itarget
+++ b/plugins/extraction/vo.itarget
@@ -3,4 +3,6 @@ ExtrOcamlIntConv.vo
 ExtrOcamlBigIntConv.vo
 ExtrOcamlNatInt.vo
 ExtrOcamlNatBigInt.vo
+ExtrOcamlZInt.vo
+ExtrOcamlZBigInt.vo
 ExtrOcamlString.vo
\ No newline at end of file