Library Coq.extraction.ExtrOcamlBigIntConv
Extraction to OCaml: conversion from/to Z.t
NB: The extracted code should be linked with zarith.cm(x)a and with
the big.ml wrapper. The latter 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.
Definition 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.
Definition 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).