Convert nat to big_int in extraction of Coq to Ocaml

Question

I am doing extraction convert nat to big_int

When I used the library: ExtrOcamlNatBigInt, it does not return the correct type for big_int in Ocaml

So I modify it (the file ExtrOcamlNatBigInt), but I cannot find the way to define function nat_case because in the libary Big_int of Ocaml they do not have function nat_case.

Extract Inductive nat => "Big_int.big_int"
  [ "Big_int.zero_big_int" "Big_int.succ_big_int" ] "Big_int.nat_case".

I try to define a second definition for nat_case by :

Extract Inductive nat => "Big_int.big_int"
  [ "Big_int.zero_big_int" "Big_int.succ_big_int" ] "(fun fO fS n ->
    let one = Big_int.unit_big_int in
    if n = Big_int.zero_big_int then fO () else fS (n - one))".

Here is a result after using the second definition:

(** val nat_rect :
    'a1 -> (Big_int.big_int -> 'a1 -> 'a1) -> Big_int.big_int -> 'a1 **)

let rec nat_rect f f0 n =
  let one = Big_int.unit_big_int in
    if n = Big_int.zero_big_int then f () else f0 (n - one)
    (fun _ ->
    f)
    (fun n0 ->
    f0 n0 (nat_rect f f0 n0)) n

I got an error at n of line else f0 (n - one):

File "Datatypes.ml", line 68, characters 51-52: Error: This expression has type Big_int.big_int but an expression was expected of type int

I think it is because of the minus (-)

I also modify the minus extraction :

Extract Constant minus => "fun n m -> Big_int.max_big_int Big_int.zero_big_int 
   (Big_int.sub_big_int n m)".

Could you please help me to define the function nat_case for Big_int? Thank you very much.

Answer 1

(-) is reserved to integer operation, you can't use the same operator for big_int. Replace

(n - one)

by :

Big_int.sub_big_int n one