diff options
-rw-r--r-- | plugins/extraction/ExtrOcamlBigIntConv.v | 76 | ||||
-rw-r--r-- | plugins/extraction/ExtrOcamlNatBigInt.v | 60 | ||||
-rw-r--r-- | plugins/extraction/ExtrOcamlZBigInt.v | 85 | ||||
-rw-r--r-- | plugins/extraction/ExtrOcamlZInt.v | 78 | ||||
-rw-r--r-- | plugins/extraction/big.ml | 154 | ||||
-rw-r--r-- | plugins/extraction/vo.itarget | 2 |
6 files changed, 390 insertions, 65 deletions
diff --git a/plugins/extraction/ExtrOcamlBigIntConv.v b/plugins/extraction/ExtrOcamlBigIntConv.v index 9f80812db..b4490545c 100644 --- a/plugins/extraction/ExtrOcamlBigIntConv.v +++ b/plugins/extraction/ExtrOcamlBigIntConv.v @@ -8,7 +8,10 @@ (** Extraction to Ocaml: conversion from/to [big_int] *) -(** The extracted code should be linked with [nums.(cma|cmxa)] *) +(** 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. @@ -18,11 +21,11 @@ Parameter bigint_succ : bigint -> bigint. Parameter bigint_opp : bigint -> bigint. Parameter bigint_twice : bigint -> bigint. -Extract Inlined Constant bigint => "Big_int.big_int". -Extract Inlined Constant bigint_zero => "Big_int.zero_big_int". -Extract Inlined Constant bigint_succ => "Big_int.succ_big_int". -Extract Inlined Constant bigint_opp => "Big_int.minus_big_int". -Extract Inlined Constant bigint_twice => "Big_int.mult_int_big_int 2". +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 := @@ -56,43 +59,50 @@ Fixpoint bigint_of_n n := non-positive inputs. *) Parameter bigint_natlike_rec : forall A, A -> (A->A) -> bigint -> A. -Extract Constant bigint_natlike_rec => -"fun fO fS -> - let rec loop acc i = if Big_int.sign_big_int i <= 0 then acc - else loop (fS acc) (Big_int.pred_big_int i) - in loop fO". +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 => -"fun f1 f2x f2x1 -> - let rec loop i = if Big_int.le_big_int i Big_int.unit_big_int then f1 - else - let (q,r) = Big_int.quomod_big_int i (Big_int.big_int_of_int 2) in - if Big_int.sign_big_int r = 0 then f2x (loop q) else f2x1 (loop q) - in loop". +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 _ xH xO xI. +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 => -"fun f0 fpos fneg i -> - let sgn = Big_int.sign_big_int i in - if sgn = 0 then f0 else if sgn>0 then fpos i - else fneg (Big_int.minus_big_int i)". +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)). + (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). -(* -Extraction "/tmp/test.ml" - nat_of_bigint bigint_of_nat - pos_of_bigint bigint_of_pos - z_of_bigint bigint_of_z - n_of_bigint bigint_of_n. +(* 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 *)
\ No newline at end of file diff --git a/plugins/extraction/ExtrOcamlNatBigInt.v b/plugins/extraction/ExtrOcamlNatBigInt.v index 22c3a133b..e2051e110 100644 --- a/plugins/extraction/ExtrOcamlNatBigInt.v +++ b/plugins/extraction/ExtrOcamlNatBigInt.v @@ -11,7 +11,10 @@ Require Import Arith Even Div2 EqNat Euclid. Require Import ExtrOcamlBasic. -(** NB: The extracted code should be linked with [nums.(cma|cmxa)]. *) +(** 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 [nat] into [big_int] isn't necessarily a good idea. @@ -22,52 +25,45 @@ Require Import ExtrOcamlBasic. (** Mapping of [nat] into [big_int]. The last string corresponds to a [nat_case], see documentation of [Extract Inductive]. *) -Extract Inductive nat => "Big_int.big_int" - [ "Big_int.zero_big_int" "Big_int.succ_big_int" ] - "(fun fO fS n -> if Big_int.sign_big_int n = 0 then fO () else fS (Big_int.pred_big_int n))". +Extract Inductive nat => "Big.big_int" [ "Big.zero" "Big.succ" ] + "Big.nat_case". (** Efficient (but uncertified) versions for usual [nat] functions *) -Extract Constant plus => "Big_int.add_big_int". -Extract Constant mult => "Big_int.mult_big_int". -Extract Constant pred => - "fun n -> Big_int.max_big_int Big_int.zero_big_int (Big_int.pred_big_int n)". -Extract Constant minus => - "fun n m -> Big_int.max_big_int Big_int.zero_big_int (Big_int.sub_big_int n m)". -Extract Constant max => "Big_int.max_big_int". -Extract Constant min => "Big_int.min_big_int". -Extract Constant nat_beq => "Big_int.eq_big_int". -Extract Constant EqNat.beq_nat => "Big_int.eq_big_int". -Extract Constant EqNat.eq_nat_decide => "Big_int.eq_big_int". +Extract Constant plus => "Big.add". +Extract Constant mult => "Big.mult". +Extract Constant pred => "fun n -> Big.max Big.zero (Big.pred n)". +Extract Constant minus => "fun n m -> Big.max Big.zero (Big.sub n m)". +Extract Constant max => "Big.max". +Extract Constant min => "Big.min". +Extract Constant nat_beq => "Big.eq". +Extract Constant EqNat.beq_nat => "Big.eq". +Extract Constant EqNat.eq_nat_decide => "Big.eq". -Extract Inlined Constant Peano_dec.eq_nat_dec => "Big_int.eq_big_int". +Extract Constant Peano_dec.eq_nat_dec => "Big.eq". Extract Constant Compare_dec.nat_compare => -"fun n m -> - let s = Big_int.compare_big_int n m in - if s=0 then Eq else if s<0 then Lt else Gt". + "Big.compare_case Eq Lt Gt". -Extract Inlined Constant Compare_dec.leb => "Big_int.le_big_int". -Extract Inlined Constant Compare_dec.le_lt_dec => "Big_int.le_big_int". +Extract Constant Compare_dec.leb => "Big.le". +Extract Constant Compare_dec.le_lt_dec => "Big.le". Extract Constant Compare_dec.lt_eq_lt_dec => -"fun n m -> - let s = Big_int.sign_big_int n m in - if s>0 then None else Some (s<0)". + "Big.compare_case (Some false) (Some true) None". Extract Constant Even.even_odd_dec => - "fun n -> Big_int.sign_big_int (Big_int.mod_big_int n (Big_int.big_int_of_int 2)) = 0". -Extract Constant Div2.div2 => - "fun n -> Big_int.div_big_int n (Big_int.big_int_of_int 2)". + "fun n -> Big.sign (Big.mod n Big.two) = 0". +Extract Constant Div2.div2 => "fun n -> Big.div n Big.two". -Extract Inductive Euclid.diveucl => "(Big_int.big_int * Big_int.big_int)" [""]. -Extract Constant Euclid.eucl_dev => "fun n m -> Big_int.quomod_big_int m n". -Extract Constant Euclid.quotient => "fun n m -> Big_int.div_big_int m n". -Extract Constant Euclid.modulo => "fun n m -> Big_int.mod_big_int m n". +Extract Inductive Euclid.diveucl => "(Big.big_int * Big.big_int)" [""]. +Extract Constant Euclid.eucl_dev => "fun n m -> Big.quomod m n". +Extract Constant Euclid.quotient => "fun n m -> Big.div m n". +Extract Constant Euclid.modulo => "fun n m -> Big.modulo m n". (* +Require Import Euclid. Definition test n m (H:m>0) := let (q,r,_,_) := eucl_dev m H n in nat_compare n (q*m+r). -Recursive Extraction test fact. +Extraction "/tmp/test.ml" test fact pred minus max min Div2.div2. *) diff --git a/plugins/extraction/ExtrOcamlZBigInt.v b/plugins/extraction/ExtrOcamlZBigInt.v new file mode 100644 index 000000000..8b05ca290 --- /dev/null +++ b/plugins/extraction/ExtrOcamlZBigInt.v @@ -0,0 +1,85 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \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 Pplus => "Big.add". +Extract Constant Psucc => "Big.succ". +Extract Constant Ppred => "fun n -> Big.max Big.one (Big.pred n)". +Extract Constant Pminus => "fun n m -> Big.max Big.one (Big.sub n m)". +Extract Constant Pmult => "Big.mult". +Extract Constant Pmin => "Big.min". +Extract Constant Pmax => "Big.max". +Extract Constant Pcompare => + "fun x y c -> Big.compare_case c Lt Gt x y". + +Extract Constant Nplus => "Big.add". +Extract Constant Nsucc => "Big.succ". +Extract Constant Npred => "fun n -> Big.max Big.zero (Big.pred n)". +Extract Constant Nminus => "fun n m -> Big.max Big.zero (Big.sub n m)". +Extract Constant Nmult => "Big.mult". +Extract Constant Nmin => "Big.min". +Extract Constant Nmax => "Big.max". +Extract Constant Ndiv => + "fun a b -> if Big.eq b Big.zero then Big.zero else Big.div a b". +Extract Constant Nmod => + "fun a b -> if Big.eq b Big.zero then Big.zero else Big.modulo a b". +Extract Constant Ncompare => "Big.compare_case Eq Lt Gt". + +Extract Constant Zplus => "Big.add". +Extract Constant Zsucc => "Big.succ". +Extract Constant Zpred => "Big.pred". +Extract Constant Zminus => "Big.sub". +Extract Constant Zmult => "Big.mult". +Extract Constant Zopp => "Big.opp". +Extract Constant Zabs => "Big.abs". +Extract Constant Zmin => "Big.min". +Extract Constant Zmax => "Big.max". +Extract Constant Zcompare => "Big.compare_case Eq Lt Gt". + +Extract Constant Z_of_N => "fun p -> p". +Extract Constant Zabs_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. +*) diff --git a/plugins/extraction/ExtrOcamlZInt.v b/plugins/extraction/ExtrOcamlZInt.v new file mode 100644 index 000000000..f96572120 --- /dev/null +++ b/plugins/extraction/ExtrOcamlZInt.v @@ -0,0 +1,78 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \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 [int] *) + +Require Import ZArith NArith. +Require Import ExtrOcamlBasic. + +(** Disclaimer: trying to obtain efficient certified programs + by extracting [Z] into [int] is definitively *not* a good idea. + See the Disclaimer in [ExtrOcamlNatInt]. *) + +(** Mapping of [positive], [Z], [N] into [int]. The last strings + emulate the matching, see documentation of [Extract Inductive]. *) + +Extract Inductive positive => int +[ "(fun p->1+2*p)" "(fun p->2*p)" "1" ] +"(fun f2p1 f2p f1 p -> + if p<=1 then f1 () else if p mod 2 = 0 then f2p (p/2) else f2p1 (p/2))". + +Extract Inductive Z => int [ "0" "" "(~-)" ] +"(fun f0 fp fn z -> if z=0 then f0 () else if z>0 then fp z else fn (-z))". + +Extract Inductive N => int [ "0" "" ] +"(fun f0 fp n -> if n=0 then f0 () else fp n)". + +(** Nota: the "" above is used as an identity function "(fun p->p)" *) + +(** Efficient (but uncertified) versions for usual functions *) + +Extract Constant Pplus => "(+)". +Extract Constant Psucc => "succ". +Extract Constant Ppred => "fun n -> max 1 (n-1)". +Extract Constant Pminus => "fun n m -> max 1 (n-m)". +Extract Constant Pmult => "( * )". +Extract Constant Pmin => "min". +Extract Constant Pmax => "max". +Extract Constant Pcompare => + "fun x y c -> if x=y then c else if x<y then Lt else Gt". + + +Extract Constant Nplus => "(+)". +Extract Constant Nsucc => "succ". +Extract Constant Npred => "fun n -> max 0 (n-1)". +Extract Constant Nminus => "fun n m -> max 0 (n-m)". +Extract Constant Nmult => "( * )". +Extract Constant Nmin => "min". +Extract Constant Nmax => "max". +Extract Constant Ndiv => "fun a b -> if b=0 then 0 else a/b". +Extract Constant Nmod => "fun a b -> if b=0 then a else a mod b". +Extract Constant Ncompare => + "fun x y -> if x=y then Eq else if x<y then Lt else Gt". + + +Extract Constant Zplus => "(+)". +Extract Constant Zsucc => "succ". +Extract Constant Zpred => "pred". +Extract Constant Zminus => "(-)". +Extract Constant Zmult => "( * )". +Extract Constant Zopp => "(~-)". +Extract Constant Zabs => "abs". +Extract Constant Zmin => "min". +Extract Constant Zmax => "max". +Extract Constant Zcompare => + "fun x y -> if x=y then Eq else if x<y then Lt else Gt". + +Extract Constant Z_of_N => "fun p -> p". +Extract Constant Zabs_N => "abs". + +(** Zdiv and Zmod are quite complex to define in terms of (/) and (mod). + For the moment we don't even try *) + + diff --git a/plugins/extraction/big.ml b/plugins/extraction/big.ml new file mode 100644 index 000000000..9a5bf56bc --- /dev/null +++ b/plugins/extraction/big.ml @@ -0,0 +1,154 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** [Big] : a wrapper around ocaml [Big_int] with nicer names, + and a few extraction-specific constructions *) + +(** To be linked with [nums.(cma|cmxa)] *) + +open Big_int + +type big_int = Big_int.big_int + (** The type of big integers. *) + +let zero = zero_big_int + (** The big integer [0]. *) +let one = unit_big_int + (** The big integer [1]. *) +let two = big_int_of_int 2 + (** The big integer [2]. *) + +(** {6 Arithmetic operations} *) + +let opp = minus_big_int + (** Unary negation. *) +let abs = abs_big_int + (** Absolute value. *) +let add = add_big_int + (** Addition. *) +let succ = succ_big_int + (** Successor (add 1). *) +let add_int = add_int_big_int + (** Addition of a small integer to a big integer. *) +let sub = sub_big_int + (** Subtraction. *) +let pred = pred_big_int + (** Predecessor (subtract 1). *) +let mult = mult_big_int + (** Multiplication of two big integers. *) +let mult_int = mult_int_big_int + (** Multiplication of a big integer by a small integer *) +let square = square_big_int + (** Return the square of the given big integer *) +let sqrt = sqrt_big_int + (** [sqrt_big_int a] returns the integer square root of [a], + that is, the largest big integer [r] such that [r * r <= a]. + Raise [Invalid_argument] if [a] is negative. *) +let quomod = quomod_big_int + (** Euclidean division of two big integers. + The first part of the result is the quotient, + the second part is the remainder. + Writing [(q,r) = quomod_big_int a b], we have + [a = q * b + r] and [0 <= r < |b|]. + Raise [Division_by_zero] if the divisor is zero. *) +let div = div_big_int + (** Euclidean quotient of two big integers. + This is the first result [q] of [quomod_big_int] (see above). *) +let modulo = mod_big_int + (** Euclidean modulus of two big integers. + This is the second result [r] of [quomod_big_int] (see above). *) +let gcd = gcd_big_int + (** Greatest common divisor of two big integers. *) +let power = power_big_int_positive_big_int + (** Exponentiation functions. Return the big integer + representing the first argument [a] raised to the power [b] + (the second argument). Depending + on the function, [a] and [b] can be either small integers + or big integers. Raise [Invalid_argument] if [b] is negative. *) + +(** {6 Comparisons and tests} *) + +let sign = sign_big_int + (** Return [0] if the given big integer is zero, + [1] if it is positive, and [-1] if it is negative. *) +let compare = compare_big_int + (** [compare_big_int a b] returns [0] if [a] and [b] are equal, + [1] if [a] is greater than [b], and [-1] if [a] is smaller + than [b]. *) +let eq = eq_big_int +let le = le_big_int +let ge = ge_big_int +let lt = lt_big_int +let gt = gt_big_int + (** Usual boolean comparisons between two big integers. *) +let max = max_big_int + (** Return the greater of its two arguments. *) +let min = min_big_int + (** Return the smaller of its two arguments. *) + +(** {6 Conversions to and from strings} *) + +let to_string = string_of_big_int + (** Return the string representation of the given big integer, + in decimal (base 10). *) +let of_string = big_int_of_string + (** Convert a string to a big integer, in decimal. + The string consists of an optional [-] or [+] sign, + followed by one or several decimal digits. *) + +(** {6 Conversions to and from other numerical types} *) + +let of_int = big_int_of_int + (** Convert a small integer to a big integer. *) +let is_int = is_int_big_int + (** Test whether the given big integer is small enough to + be representable as a small integer (type [int]) + without loss of precision. On a 32-bit platform, + [is_int_big_int a] returns [true] if and only if + [a] is between 2{^30} and 2{^30}-1. On a 64-bit platform, + [is_int_big_int a] returns [true] if and only if + [a] is between -2{^62} and 2{^62}-1. *) +let to_int = int_of_big_int + (** Convert a big integer to a small integer (type [int]). + Raises [Failure "int_of_big_int"] if the big integer + is not representable as a small integer. *) + +(** Functions used by extraction *) + +let double x = mult_int 2 x +let doubleplusone x = succ (double x) + +let nat_case fO fS n = if sign n <= 0 then fO () else fS (pred n) + +let positive_case f2p1 f2p f1 p = + if le p one then f1 () else + let (q,r) = quomod p two in if eq r zero then f2p q else f2p1 q + +let n_case fO fp n = if sign n <= 0 then fO () else fp n + +let z_case fO fp fn z = + let s = sign z in + if s = 0 then fO () else if s > 0 then fp z else fn (opp z) + +let compare_case e l g x y = + let s = compare x y in if s = 0 then e else if s<0 then l else g + +let nat_rec fO fS = + let rec loop acc n = + if sign n <= 0 then acc else loop (fS acc) (pred n) + in loop fO + +let positive_rec f2p1 f2p f1 = + let rec loop n = + if le n one then f1 + else + let (q,r) = quomod n two in + if eq r zero then f2p (loop q) else f2p1 (loop q) + in loop + +let z_rec fO fp fn = z_case (fun _ -> fO) fp fn diff --git a/plugins/extraction/vo.itarget b/plugins/extraction/vo.itarget index 338b27684..1fe09f6fa 100644 --- a/plugins/extraction/vo.itarget +++ b/plugins/extraction/vo.itarget @@ -3,4 +3,6 @@ ExtrOcamlIntConv.vo ExtrOcamlBigIntConv.vo ExtrOcamlNatInt.vo ExtrOcamlNatBigInt.vo +ExtrOcamlZInt.vo +ExtrOcamlZBigInt.vo ExtrOcamlString.vo
\ No newline at end of file |