# Library MetaCoq.Template.utils.MC_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.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".