Library Coq.extraction.ExtrOcamlNatBigInt
Extraction of nat into Zarith's Z.t
Require Coq.extraction.Extraction.
Require Import Arith Even Div2 EqNat Euclid.
Require Import ExtrOcamlBasic.
NB: The extracted code depends on zarith package.
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.
See documentation of Extract Inductive.
Extract Inductive nat => "Big_int_Z.big_int"
[ "Big_int_Z.zero_big_int" "Big_int_Z.succ_big_int" ]
"(fun fO fS n -> if Big_int_Z.sign_big_int n <= 0 then fO () else fS (Big_int_Z.pred_big_int n))".
Efficient (but uncertified) versions for usual nat functions
Extract Constant plus => "Big_int_Z.add_big_int".
Extract Constant mult => "Big_int_Z.mult_big_int".
Extract Constant pred =>
"(fun n -> Big_int_Z.max_big_int Big_int_Z.zero_big_int (Big_int_Z.pred_big_int n))".
Extract Constant minus =>
"(fun n m -> Big_int_Z.max_big_int Big_int_Z.zero_big_int (Big_int_Z.sub_big_int n m))".
Extract Constant max => "Big_int_Z.max_big_int".
Extract Constant min => "Big_int_Z.min_big_int".
Extract Constant Nat.eqb => "Big_int_Z.eq_big_int".
Extract Constant EqNat.eq_nat_decide => "Big_int_Z.eq_big_int".
Extract Constant Peano_dec.eq_nat_dec => "Big_int_Z.eq_big_int".
Extract Constant Nat.compare =>
"(fun x y -> let s = Big_int_Z.compare_big_int x y in if s = 0 then Eq else if s < 0 then Lt else Gt)".
Extract Constant Compare_dec.leb => "Big_int_Z.le_big_int".
Extract Constant Compare_dec.le_lt_dec => "Big_int_Z.le_big_int".
Extract Constant Compare_dec.lt_eq_lt_dec =>
"(fun x y -> let s = Big_int_Z.compare_big_int x y in if s = 0 then (Some false) else if s < 0 then (Some true) else None)".
Extract Constant Nat.Even_or_Odd =>
"(fun n -> Big_int_Z.sign_big_int (Big_int_Z.mod_big_int n (Big_int_Z.big_int_of_int 2)) = 0)".
Extract Constant Nat.div2 => "(fun n -> Big_int_Z.div_big_int n (Big_int_Z.big_int_of_int 2))".
Extract Inductive Euclid.diveucl => "(Big_int_Z.big_int * Big_int_Z.big_int)" [""].
Extract Constant Euclid.eucl_dev => "(fun n m -> Big_int_Z.quomod_big_int m n)".
Extract Constant Euclid.quotient => "(fun n m -> Big_int_Z.div_big_int m n)".
Extract Constant Euclid.modulo => "(fun n m -> Big_int_Z.mod_big_int m n)".