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).