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