(* Machine arithmetic for the functions of PeanoNat.Nat, as ExtrOcamlNatInt gives it to those of Init.Nat;
   the values extracted stay far below 2^62. *)
From Stdlib Require Import Arith Extraction ExtrOcamlBasic ExtrOcamlNatInt.

Extract Inlined Constant PeanoNat.Nat.add => "(+)".
Extract Inlined Constant PeanoNat.Nat.mul => "( * )".
Extract Inlined Constant PeanoNat.Nat.sub => "(fun n m -> if n > m then n - m else 0)".
Extract Inlined Constant PeanoNat.Nat.pred => "(fun n -> if n > 0 then n - 1 else 0)".
Extract Inlined Constant PeanoNat.Nat.div => "(fun x y -> if y = 0 then 0 else x / y)".
Extract Inlined Constant PeanoNat.Nat.modulo => "(fun x y -> if y = 0 then x else x mod y)".
Extract Inlined Constant PeanoNat.Nat.div2 => "(fun n -> n / 2)".
Extract Inlined Constant PeanoNat.Nat.even => "(fun n -> n land 1 = 0)".
Extract Inlined Constant PeanoNat.Nat.odd => "(fun n -> n land 1 = 1)".
Extract Inlined Constant PeanoNat.Nat.testbit => "(fun a n -> n < 62 && (a lsr n) land 1 = 1)".
Extract Inlined Constant PeanoNat.Nat.max => "(fun n m -> if n < m then m else n)".
Extract Inlined Constant PeanoNat.Nat.min => "(fun n m -> if n < m then n else m)".
Extract Inlined Constant PeanoNat.Nat.eqb => "(=)".
Extract Inlined Constant PeanoNat.Nat.leb => "(<=)".
Extract Inlined Constant PeanoNat.Nat.ltb => "(<)".
Extract Constant PeanoNat.Nat.pow => "(fun n m -> let rec p k = if k = 0 then 1 else n * p (k - 1) in p m)".
Extract Constant PeanoNat.Nat.log2 =>
  "(fun n -> let rec g k x = if x <= 1 then k else g (k + 1) (x lsr 1) in if n <= 0 then 0 else g 0 n)".
Extract Constant PeanoNat.Nat.log2_up =>
  "(fun a -> let rec g k x = if x = 0 then k else g (k + 1) (x lsr 1) in if a <= 1 then 0 else g 0 (a - 1))".