From fb6ae3d50279005f75deb273de1d0067a5fa089a Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 15 Jun 2010 14:28:05 +0000
Subject: 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
---
 plugins/extraction/ExtrOcamlZInt.v | 78 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 78 insertions(+)
 create mode 100644 plugins/extraction/ExtrOcamlZInt.v

(limited to 'plugins/extraction/ExtrOcamlZInt.v')

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 *)
+
+
-- 
cgit v1.2.3