diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-15 14:28:05 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-15 14:28:05 +0000 |
commit | fb6ae3d50279005f75deb273de1d0067a5fa089a (patch) | |
tree | 753aab2da5a61fc9bb6942b0dacbd762f6a4ca98 /plugins/extraction/ExtrOcamlZInt.v | |
parent | 94eed81b4fbea5bf05e722280a9338ca607e2f21 (diff) |
Extraction: in support library, more and nicer big_int
- we use a wrapper file big.ml to have short names about big_int
and specialized functions for extraction
- new files : ExtrOcamlZInt for Z==>int and N==>int,
ExtrOcamlZBigInt for Z==>big_int and N==>big_int
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13137 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/extraction/ExtrOcamlZInt.v')
-rw-r--r-- | plugins/extraction/ExtrOcamlZInt.v | 78 |
1 files changed, 78 insertions, 0 deletions
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 *) + + |