Library Coq.extraction.ExtrOcamlNatBigInt
Extraction of nat into Ocaml's big_int
Require Coq.extraction.Extraction.
Require Import Arith Even Div2 EqNat 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
simplifies the use of Big_int (it can 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.
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 EqNat.beq_nat => "Big.eq".
Extract Constant EqNat.eq_nat_decide => "Big.eq".
Extract Constant Peano_dec.eq_nat_dec => "Big.eq".
Extract Constant 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".