Library Coq.extraction.ExtrOcamlBigIntConv


Extraction to Ocaml: conversion from/to big_int
NB: The extracted code should be linked with nums.cm(x)a from ocaml's stdlib and with the wrapper big.ml that simplifies the use of Big_int (it can be found in the sources of Coq).

Require Coq.extraction.Extraction.

Require Import Arith ZArith.

Parameter bigint : Type.
Parameter bigint_zero : bigint.
Parameter bigint_succ : bigint -> bigint.
Parameter bigint_opp : bigint -> bigint.
Parameter bigint_twice : bigint -> bigint.

Extract Inlined Constant bigint => "Big.big_int".
Extract Inlined Constant bigint_zero => "Big.zero".
Extract Inlined Constant bigint_succ => "Big.succ".
Extract Inlined Constant bigint_opp => "Big.opp".
Extract Inlined Constant bigint_twice => "Big.double".

Definition bigint_of_nat : nat -> bigint :=
 (fix loop acc n :=
  match n with
   | O => acc
   | S n => loop (bigint_succ acc) n
  end) bigint_zero.

Fixpoint bigint_of_pos p :=
 match p with
  | xH => bigint_succ bigint_zero
  | xO p => bigint_twice (bigint_of_pos p)
  | xI p => bigint_succ (bigint_twice (bigint_of_pos p))
 end.

Fixpoint bigint_of_z z :=
 match z with
  | Z0 => bigint_zero
  | Zpos p => bigint_of_pos p
  | Zneg p => bigint_opp (bigint_of_pos p)
 end.

Fixpoint bigint_of_n n :=
 match n with
  | N0 => bigint_zero
  | Npos p => bigint_of_pos p
 end.

NB: as for pred or minus, nat_of_bigint, n_of_bigint and pos_of_bigint are total and return zero (resp. one) for non-positive inputs.

Parameter bigint_natlike_rec : forall A, A -> (A->A) -> bigint -> A.
Extract Constant bigint_natlike_rec => "Big.nat_rec".

Definition nat_of_bigint : bigint -> nat := bigint_natlike_rec _ O S.

Parameter bigint_poslike_rec : forall A, (A->A) -> (A->A) -> A -> bigint -> A.
Extract Constant bigint_poslike_rec => "Big.positive_rec".

Definition pos_of_bigint : bigint -> positive := bigint_poslike_rec _ xI xO xH.

Parameter bigint_zlike_case :
 forall A, A -> (bigint->A) -> (bigint->A) -> bigint -> A.
Extract Constant bigint_zlike_case => "Big.z_rec".

Definition z_of_bigint : bigint -> Z :=
 bigint_zlike_case _ Z0 (fun i => Zpos (pos_of_bigint i))
                        (fun i => Zneg (pos_of_bigint i)).

Definition n_of_bigint : bigint -> N :=
 bigint_zlike_case _ N0 (fun i => Npos (pos_of_bigint i)) (fun _ => N0).