Extraction: start of a support library

 - ExtrOcamlBasic: mapping of basic types to ocaml's ones
 - ExtrOcamlIntConv: conversion between int and coq's numerical types
 - ExtrOcamlBigIntConv: same with big_int (no overflow)
 - ExtrOcamlNatInt: realizes nat by int (unsafe)

more to come: Haskell, handling of stings, more stuff in ExtrOcamlNatInt,
etc etc...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13050 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 268 insertions, 0 deletions

diff --git a/plugins/extraction/ExtrOcamlBasic.v b/plugins/extraction/ExtrOcamlBasic.v
new file mode 100644
index 000000000..1fcdfd655
--- /dev/null
+++ b/plugins/extraction/ExtrOcamlBasic.v
@@ -0,0 +1,33 @@
+(************************************************************************)
+(*  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 to Ocaml : use of basic Ocaml types *)
+
+Extract Inductive bool => bool [ true false ].
+Extract Inductive option => option [ Some None ].
+Extract Inductive prod => "( * )" [ "" ].
+ (* The "" above is a hack, but produce nicer code than with "(,)" *)
+Extract Inductive unit => unit [ "()" ].
+Extract Inductive list => list [ "[]" "( :: )" ].
+
+(** We could also map sumbool to bool, sumor to option, but
+    this isn't always a gain in clarity. We leave it to the user...
+
+Extract Inductive sumbool => bool [ true false ].
+Extract Inductive sumor => option [ Some None ].
+*)
+
+(** Restore lazyness of andb, orb.
+    NB: without these Extract Constant, andb/orb would be inlined
+    by extraction in order to have lazyness, producing inelegant
+    (if ... then ... else false) and (if ... then true else ...).
+*)
+
+Extract Inlined Constant andb => "(&&)".
+Extract Inlined Constant orb => "(||)".
+
diff --git a/plugins/extraction/ExtrOcamlBigIntConv.v b/plugins/extraction/ExtrOcamlBigIntConv.v
new file mode 100644
index 000000000..9f80812db
--- /dev/null
+++ b/plugins/extraction/ExtrOcamlBigIntConv.v
@@ -0,0 +1,98 @@
+(************************************************************************)
+(*  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 to Ocaml: conversion from/to [big_int] *)
+
+(** The extracted code should be linked with [nums.(cma|cmxa)] *)
+
+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_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".
+
+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 =>
+"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".
+
+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".
+
+Definition pos_of_bigint : bigint -> positive := bigint_poslike_rec _ xH xO xI.
+
+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)".
+
+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).
+
+(*
+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.
+*)
\ No newline at end of file
diff --git a/plugins/extraction/ExtrOcamlIntConv.v b/plugins/extraction/ExtrOcamlIntConv.v
new file mode 100644
index 000000000..e729d9ca0
--- /dev/null
+++ b/plugins/extraction/ExtrOcamlIntConv.v
@@ -0,0 +1,97 @@
+(************************************************************************)
+(*  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 to Ocaml: conversion from/to [int]
+
+    Nota: no check that [int] values aren't generating overflows *)
+
+Require Import Arith ZArith.
+
+Parameter int : Type.
+Parameter int_zero : int.
+Parameter int_succ : int -> int.
+Parameter int_opp : int -> int.
+Parameter int_twice : int -> int.
+
+Extract Inlined Constant int => int.
+Extract Inlined Constant int_zero => "0".
+Extract Inlined Constant int_succ => "succ".
+Extract Inlined Constant int_opp => "-".
+Extract Inlined Constant int_twice => "2 *".
+
+Definition int_of_nat : nat -> int :=
+ (fix loop acc n :=
+  match n with
+   | O => acc
+   | S n => loop (int_succ acc) n
+  end) int_zero.
+
+Fixpoint int_of_pos p :=
+ match p with
+  | xH => int_succ int_zero
+  | xO p => int_twice (int_of_pos p)
+  | xI p => int_succ (int_twice (int_of_pos p))
+ end.
+
+Fixpoint int_of_z z :=
+ match z with
+  | Z0 => int_zero
+  | Zpos p => int_of_pos p
+  | Zneg p => int_opp (int_of_pos p)
+ end.
+
+Fixpoint int_of_n n :=
+ match n with
+  | N0 => int_zero
+  | Npos p => int_of_pos p
+ end.
+
+(** NB: as for [pred] or [minus], [nat_of_int], [n_of_int] and
+    [pos_of_int] are total and return zero (resp. one) for
+    non-positive inputs. *)
+
+Parameter int_natlike_rec : forall A, A -> (A->A) -> int -> A.
+Extract Constant int_natlike_rec =>
+"fun fO fS ->
+ let rec loop acc i = if i <= 0 then acc else loop (fS acc) (i-1)
+ in loop fO".
+
+Definition nat_of_int : int -> nat := int_natlike_rec _ O S.
+
+Parameter int_poslike_rec : forall A, A -> (A->A) -> (A->A) -> int -> A.
+Extract Constant int_poslike_rec =>
+"fun f1 f2x f2x1 ->
+ let rec loop i = if i <= 1 then f1 else
+  if i land 1 = 0 then f2x (loop (i lsr 1)) else f2x1 (loop (i lsr 1))
+ in loop".
+
+Definition pos_of_int : int -> positive := int_poslike_rec _ xH xO xI.
+
+Parameter int_zlike_case : forall A, A -> (int->A) -> (int->A) -> int -> A.
+Extract Constant int_zlike_case =>
+"fun f0 fpos fneg i ->
+ if i = 0 then f0 else if i>0 then fpos i else fneg (-i)".
+
+Definition z_of_int : int -> Z :=
+ int_zlike_case _ Z0 (fun i => Zpos (pos_of_int i))
+                     (fun i => Zneg (pos_of_int i)).
+
+Definition n_of_int : int -> N :=
+ int_zlike_case _ N0 (fun i => Npos (pos_of_int i)) (fun _ => N0).
+
+(** Warning: [z_of_int] is currently wrong for Ocaml's [min_int],
+    since [min_int] has no positive opposite ([-min_int = min_int]).
+*)
+
+(*
+Extraction "/tmp/test.ml"
+  nat_of_int int_of_nat
+  pos_of_int int_of_pos
+  z_of_int int_of_z
+  n_of_int int_of_n.
+*)
\ No newline at end of file
diff --git a/plugins/extraction/ExtrOcamlNatInt.v b/plugins/extraction/ExtrOcamlNatInt.v
new file mode 100644
index 000000000..580d1fbea
--- /dev/null
+++ b/plugins/extraction/ExtrOcamlNatInt.v
@@ -0,0 +1,36 @@
+(************************************************************************)
+(*  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 [nat] into Ocaml's [int] *)
+
+(** Nota: this is potentially unsafe since [int] is bounded
+    while [nat] isn't, so you should make sure that no overflow
+    occurs in your programs... *)
+
+Require Import Arith Compare_dec ExtrOcamlBasic.
+
+Extract Inductive sumbool => bool [ true false ].
+
+Extract Inductive nat => int [ "0" "succ" ]
+ "(*nat_case*) (fun fO fS n => if n=0 then fO () else fS (n-1))".
+
+Extract Constant plus => "(+)".
+Extract Constant pred => "fun n => max 0 (n-1)".
+Extract Constant minus => "fun n m => max 0 (n-p)".
+Extract Constant mult => "( * )".
+Extract Constant nat_compare =>
+ "fun n m => if n=m then Eq else if n<m then Lt else Gt".
+
+Extract Constant leb => "(<=)".
+Extract Constant nat_beq => "(=)".
+
+Extraction fact.
+
+(* Div2.div2 *)
+(* Even.even_odd_dec *)
+(* beq_nat ?? eq_nat_dec le_lt_dec, etc *)
diff --git a/plugins/extraction/vo.itarget b/plugins/extraction/vo.itarget
new file mode 100644
index 000000000..03554a164
--- /dev/null
+++ b/plugins/extraction/vo.itarget
@@ -0,0 +1,4 @@
+ExtrOcamlBasic.vo
+ExtrOcamlBigIntConv.vo
+ExtrOcamlIntConv.vo
+ExtrOcamlNatInt.vo