1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(** 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
simlifies the use of [Big_int] (it could be found in the sources
of Coq). *)
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).
(* Tests:
Definition small := 1234%nat.
Definition big := 12345678901234567890%positive.
Definition nat_0 := nat_of_bigint (bigint_of_nat 0).
Definition nat_1 := nat_of_bigint (bigint_of_nat small).
Definition pos_1 := pos_of_bigint (bigint_of_pos 1).
Definition pos_2 := pos_of_bigint (bigint_of_pos big).
Definition n_0 := n_of_bigint (bigint_of_n 0).
Definition n_1 := n_of_bigint (bigint_of_n 1).
Definition n_2 := n_of_bigint (bigint_of_n (Npos big)).
Definition z_0 := z_of_bigint (bigint_of_z 0).
Definition z_1 := z_of_bigint (bigint_of_z 1).
Definition z_2 := z_of_bigint (bigint_of_z (Zpos big)).
Definition z_m1 := z_of_bigint (bigint_of_z (-1)).
Definition z_m2 := z_of_bigint (bigint_of_z (Zneg big)).
Definition test :=
(nat_0, nat_1, pos_1, pos_2, n_0, n_1, n_2, z_0, z_1, z_2, z_m1, z_m2).
Definition check :=
(O, small, xH, big, 0%N, 1%N, Npos big, 0%Z, 1%Z, Zpos big, (-1)%Z, Zneg big).
Extraction "/tmp/test.ml" check test.
... and we check that test=check
*)
|
