Extraction: finish ExtrOcamlNatInt, add similar translation nat==>big_int

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

4 files changed, 135 insertions, 22 deletions

diff --git a/plugins/extraction/ExtrOcamlBasic.v b/plugins/extraction/ExtrOcamlBasic.v
index 1fcdfd655..f01352212 100644
--- a/plugins/extraction/ExtrOcamlBasic.v
+++ b/plugins/extraction/ExtrOcamlBasic.v
@@ -10,17 +10,17 @@
 
 Extract Inductive bool => bool [ true false ].
 Extract Inductive option => option [ Some None ].
-Extract Inductive prod => "( * )" [ "" ].
- (* The "" above is a hack, but produce nicer code than with "(,)" *)
 Extract Inductive unit => unit [ "()" ].
 Extract Inductive list => list [ "[]" "( :: )" ].
+Extract Inductive prod => "( * )" [ "" ].
 
-(** We could also map sumbool to bool, sumor to option, but
-    this isn't always a gain in clarity. We leave it to the user...
+(** NB: The "" above is a hack, but produce nicer code than "(,)" *)
+
+(** Mapping sumbool to bool and sumor to option is not always nicer,
+    but it helps when realizing stuff like [lt_eq_lt_dec] *)
 
 Extract Inductive sumbool => bool [ true false ].
 Extract Inductive sumor => option [ Some None ].
-*)
 
 (** Restore lazyness of andb, orb.
     NB: without these Extract Constant, andb/orb would be inlined
diff --git a/plugins/extraction/ExtrOcamlNatBigInt.v b/plugins/extraction/ExtrOcamlNatBigInt.v
new file mode 100644
index 000000000..22c3a133b
--- /dev/null
+++ b/plugins/extraction/ExtrOcamlNatBigInt.v
@@ -0,0 +1,73 @@
+(************************************************************************)
+(*  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 [nat] into Ocaml's [big_int] *)
+
+Require Import Arith Even Div2 EqNat Euclid.
+Require Import ExtrOcamlBasic.
+
+(** NB: The extracted code should be linked with [nums.(cma|cmxa)]. *)
+
+(** Disclaimer: trying to obtain efficient certified programs
+    by extracting [nat] into [big_int] isn't necessarily a good idea.
+    See comments in [ExtrOcamlNatInt.v].
+*)
+
+
+(** 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))".
+
+(** 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 Inlined Constant Peano_dec.eq_nat_dec => "Big_int.eq_big_int".
+
+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".
+
+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.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)".
+
+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)".
+
+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".
+
+(*
+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.
+*)
diff --git a/plugins/extraction/ExtrOcamlNatInt.v b/plugins/extraction/ExtrOcamlNatInt.v
index 580d1fbea..d0791da32 100644
--- a/plugins/extraction/ExtrOcamlNatInt.v
+++ b/plugins/extraction/ExtrOcamlNatInt.v
@@ -8,29 +8,68 @@
 
 (** Extraction of [nat] into Ocaml's [int] *)
 
-(** Nota: this is potentially unsafe since [int] is bounded
-    while [nat] isn't, so you should make sure that no overflow
-    occurs in your programs... *)
+Require Import Arith Even Div2 EqNat Euclid.
+Require Import ExtrOcamlBasic.
 
-Require Import Arith Compare_dec ExtrOcamlBasic.
+(** Disclaimer: trying to obtain efficient certified programs
+    by extracting [nat] into [int] is definitively *not* a good idea:
 
-Extract Inductive sumbool => bool [ true false ].
+    - Since [int] is bounded while [nat] is (theoretically) infinite,
+    you have to make sure by yourself that your program will not
+    manipulate numbers greater than [max_int]. Otherwise you should
+    consider the translation of [nat] into [big_int].
+
+    - Moreover, the mere translation of [nat] into [int] does not
+    change the complexity of functions. For instance, [mult] stays
+    quadratic. To mitigate this, we propose here a few efficient (but
+    uncertified) realizers for some common functions over [nat].
+
+    This file is hence provided mainly for testing / prototyping
+    purpose. For serious use of numbers in extracted programs,
+    you are advised to use either coq advanced representations
+    (positive, Z, N, BigN, BigZ) or modular/axiomatic representation.
+*)
+
+
+(** Mapping of [nat] into [int]. The last string corresponds to
+    a [nat_case], see documentation of [Extract Inductive]. *)
 
 Extract Inductive nat => int [ "0" "succ" ]
- "(*nat_case*) (fun fO fS n => if n=0 then fO () else fS (n-1))".
+ "(fun fO fS n -> if n=0 then fO () else fS (n-1))".
+
+(** Efficient (but uncertified) versions for usual [nat] functions *)
 
 Extract Constant plus => "(+)".
-Extract Constant pred => "fun n => max 0 (n-1)".
-Extract Constant minus => "fun n m => max 0 (n-p)".
+Extract Constant pred => "fun n -> max 0 (n-1)".
+Extract Constant minus => "fun n m -> max 0 (n-m)".
 Extract Constant mult => "( * )".
-Extract Constant nat_compare =>
- "fun n m => if n=m then Eq else if n<m then Lt else Gt".
+Extract Inlined Constant max => max.
+Extract Inlined Constant min => min.
+Extract Inlined Constant nat_beq => "(=)".
+Extract Inlined Constant EqNat.beq_nat => "(=)".
+Extract Inlined Constant EqNat.eq_nat_decide => "(=)".
+
+Extract Inlined Constant Peano_dec.eq_nat_dec => "(=)".
+
+Extract Constant Compare_dec.nat_compare =>
+ "fun n m -> if n=m then Eq else if n<m then Lt else Gt".
+Extract Inlined Constant Compare_dec.leb => "(<=)".
+Extract Inlined Constant Compare_dec.le_lt_dec => "(<=)".
+Extract Constant Compare_dec.lt_eq_lt_dec =>
+ "fun n m -> if n>m then None else Some (n<m)".
+
+Extract Constant Even.even_odd_dec => "fun n -> n mod 2 = 0".
+Extract Constant Div2.div2 => "fun n -> n/2".
 
-Extract Constant leb => "(<=)".
-Extract Constant nat_beq => "(=)".
+Extract Inductive Euclid.diveucl => "(int * int)" [ "" ].
+Extract Constant Euclid.eucl_dev => "fun n m -> (m/n, m mod n)".
+Extract Constant Euclid.quotient => "fun n m -> m/n".
+Extract Constant Euclid.modulo => "fun n m -> m mod n".
 
-Extraction fact.
+(*
+Definition test n m (H:m>0) :=
+ let (q,r,_,_) := eucl_dev m H n in
+ nat_compare n (q*m+r).
 
-(* Div2.div2 *)
-(* Even.even_odd_dec *)
-(* beq_nat ?? eq_nat_dec le_lt_dec, etc *)
+Recursive Extraction test fact.
+*)
\ No newline at end of file
diff --git a/plugins/extraction/vo.itarget b/plugins/extraction/vo.itarget
index 03554a164..f7168ff40 100644
--- a/plugins/extraction/vo.itarget
+++ b/plugins/extraction/vo.itarget
@@ -1,4 +1,5 @@
 ExtrOcamlBasic.vo
-ExtrOcamlBigIntConv.vo
 ExtrOcamlIntConv.vo
+ExtrOcamlBigIntConv.vo
 ExtrOcamlNatInt.vo
+ExtrOcamlNatBigInt.vo