From 700f011316e067fa7311ba23d2195a483376a284 Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 2 Jun 2010 15:06:03 +0000 Subject: 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 --- plugins/extraction/ExtrOcamlBasic.v | 33 +++++++++++ plugins/extraction/ExtrOcamlBigIntConv.v | 98 ++++++++++++++++++++++++++++++++ plugins/extraction/ExtrOcamlIntConv.v | 97 +++++++++++++++++++++++++++++++ plugins/extraction/ExtrOcamlNatInt.v | 36 ++++++++++++ plugins/extraction/vo.itarget | 4 ++ 5 files changed, 268 insertions(+) create mode 100644 plugins/extraction/ExtrOcamlBasic.v create mode 100644 plugins/extraction/ExtrOcamlBigIntConv.v create mode 100644 plugins/extraction/ExtrOcamlIntConv.v create mode 100644 plugins/extraction/ExtrOcamlNatInt.v create mode 100644 plugins/extraction/vo.itarget (limited to 'plugins/extraction') 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 *) +(* 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 *) +(* 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 *) +(* 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 *) +(* 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 "(<=)". +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 -- cgit v1.2.3