summaryrefslogtreecommitdiff
path: root/plugins/extraction/ExtrOcamlZBigInt.v
blob: 12607b3ad205f02508c4ff51eb608bc50b14a389 (plain)
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
(************************************************************************)
(*  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 of [positive], [N] and [Z] into Ocaml's [big_int] *)

Require Import ZArith NArith.
Require Import ExtrOcamlBasic.

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

(** Disclaimer: trying to obtain efficient certified programs
    by extracting [Z] into [big_int] isn't necessarily a good idea.
    See the Disclaimer in [ExtrOcamlNatInt]. *)

(** Mapping of [positive], [Z], [N] into [big_int]. The last strings
    emulate the matching, see documentation of [Extract Inductive]. *)

Extract Inductive positive => "Big.big_int"
 [ "Big.doubleplusone" "Big.double" "Big.one" ] "Big.positive_case".

Extract Inductive Z => "Big.big_int"
 [ "Big.zero" "" "Big.opp" ] "Big.z_case".

Extract Inductive N => "Big.big_int"
 [ "Big.zero" "" ] "Big.n_case".

(** Nota: the "" above is used as an identity function "(fun p->p)" *)

(** Efficient (but uncertified) versions for usual functions *)

Extract Constant Pos.add => "Big.add".
Extract Constant Pos.succ => "Big.succ".
Extract Constant Pos.pred => "fun n -> Big.max Big.one (Big.pred n)".
Extract Constant Pos.sub => "fun n m -> Big.max Big.one (Big.sub n m)".
Extract Constant Pos.mul => "Big.mult".
Extract Constant Pos.min => "Big.min".
Extract Constant Pos.max => "Big.max".
Extract Constant Pos.compare =>
 "fun x y -> Big.compare_case Eq Lt Gt x y".
Extract Constant Pos.compare_cont =>
 "fun x y c -> Big.compare_case c Lt Gt x y".

Extract Constant N.add => "Big.add".
Extract Constant N.succ => "Big.succ".
Extract Constant N.pred => "fun n -> Big.max Big.zero (Big.pred n)".
Extract Constant N.sub => "fun n m -> Big.max Big.zero (Big.sub n m)".
Extract Constant N.mul => "Big.mult".
Extract Constant N.min => "Big.min".
Extract Constant N.max => "Big.max".
Extract Constant N.div =>
 "fun a b -> if Big.eq b Big.zero then Big.zero else Big.div a b".
Extract Constant N.modulo =>
 "fun a b -> if Big.eq b Big.zero then Big.zero else Big.modulo a b".
Extract Constant N.compare => "Big.compare_case Eq Lt Gt".

Extract Constant Z.add => "Big.add".
Extract Constant Z.succ => "Big.succ".
Extract Constant Z.pred => "Big.pred".
Extract Constant Z.sub => "Big.sub".
Extract Constant Z.mul => "Big.mult".
Extract Constant Z.opp => "Big.opp".
Extract Constant Z.abs => "Big.abs".
Extract Constant Z.min => "Big.min".
Extract Constant Z.max => "Big.max".
Extract Constant Z.compare => "Big.compare_case Eq Lt Gt".

Extract Constant Z.of_N => "fun p -> p".
Extract Constant Z.abs_N => "Big.abs".

(** Zdiv and Zmod are quite complex to define in terms of (/) and (mod).
    For the moment we don't even try *)

(** Test:
Require Import ZArith NArith.

Extraction "/tmp/test.ml"
 Pplus Ppred Pminus Pmult Pcompare Npred Nminus Ndiv Nmod Ncompare
 Zplus Zmult BinInt.Zcompare Z_of_N Zabs_N Zdiv.Zdiv Zmod.
*)