Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 69 insertions, 0 deletions

diff --git a/plugins/extraction/ExtrOcamlNatBigInt.v b/plugins/extraction/ExtrOcamlNatBigInt.v
new file mode 100644
index 00000000..491e0258
--- /dev/null
+++ b/plugins/extraction/ExtrOcamlNatBigInt.v
@@ -0,0 +1,69 @@
+(************************************************************************)
+(*  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 MinMax Euclid.
+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 [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.big_int" [ "Big.zero" "Big.succ" ]
+ "Big.nat_case".
+
+(** Efficient (but uncertified) versions for usual [nat] functions *)
+
+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 Constant Peano_dec.eq_nat_dec => "Big.eq".
+
+Extract Constant Compare_dec.nat_compare =>
+ "Big.compare_case Eq Lt Gt".
+
+Extract Constant Compare_dec.leb => "Big.le".
+Extract Constant Compare_dec.le_lt_dec => "Big.le".
+Extract Constant Compare_dec.lt_eq_lt_dec =>
+ "Big.compare_case (Some false) (Some true) None".
+
+Extract Constant Even.even_odd_dec =>
+ "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.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).
+
+Extraction "/tmp/test.ml" test fact pred minus max min Div2.div2.
+*)