Library Coq.extraction.ExtrOcamlNatInt
Extraction of nat into Ocaml's int
Require Coq.extraction.Extraction.
Require Import Arith Even Div2 EqNat Euclid.
Require Import ExtrOcamlBasic.
Disclaimer: trying to obtain efficient certified programs
by extracting nat into int is definitively *not* a good idea:
Mapping of nat into int. The last string corresponds to
a nat_case, see documentation of Extract Inductive.
- This is just a syntactic adaptation, many things can go wrong,
Extract Inductive nat => int [ "0" "Stdlib.Int.succ" ]
"(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 -> Stdlib.max 0 (n-1)".
Extract Constant minus => "fun n m -> Stdlib.max 0 (n-m)".
Extract Constant mult => "( * )".
Extract Inlined Constant max => "Stdlib.max".
Extract Inlined Constant min => "Stdlib.min".
Extract Inlined Constant Nat.eqb => "(=)".
Extract Inlined Constant EqNat.eq_nat_decide => "(=)".
Extract Inlined Constant Peano_dec.eq_nat_dec => "(=)".
Extract Constant 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 Inlined Constant Compare_dec.lt_dec => "(<)".
Extract Constant Compare_dec.lt_eq_lt_dec =>
"fun n m -> if n>m then None else Some (n<m)".
Extract Constant Nat.Even_or_Odd => "fun n -> n mod 2 = 0".
Extract Constant Nat.div2 => "fun n -> n/2".
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".