summaryrefslogtreecommitdiff
path: root/plugins/extraction/ExtrOcamlNatBigInt.v
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
commit5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch)
tree631ad791a7685edafeb1fb2e8faeedc8379318ae /plugins/extraction/ExtrOcamlNatBigInt.v
parentda178a880e3ace820b41d38b191d3785b82991f5 (diff)
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'plugins/extraction/ExtrOcamlNatBigInt.v')
-rw-r--r--plugins/extraction/ExtrOcamlNatBigInt.v69
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.
+*)