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

1 files changed, 28 insertions, 32 deletions

diff --git a/plugins/extraction/ExtrOcamlNatBigInt.v b/plugins/extraction/ExtrOcamlNatBigInt.v
index 22c3a133b8..e2051e1107 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.
 *)