Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: ExtrOcamlNatBigInt.v Sprache: Coq

Original von: Coq^©

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(** Extraction of [nat] into Ocaml's [big_int] *)

Require Coq.extraction.Extraction.

Require Import Arith Even Div2 EqNat Euclid.
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
    simplifies the use of [Big_int] (it can 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.
    See comments in [ExtrOcamlNatInt.v].
*)

(** Mapping of [nat] into [big_int]. The last string corresponds to
    a [nat_case], see documentation of [Extract Inductive]. *)

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.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 Constant Peano_dec.eq_nat_dec => "Big.eq".

Extract Constant Nat.compare =>
"Big.compare_case Eq Lt Gt".

Extract Constant Compare_dec.leb => "Big.le".
Extract Constant Compare_dec.le_lt_dec => "Big.le".
Extract Constant Compare_dec.lt_eq_lt_dec =>
"Big.compare_case (Some false) (Some true) None".

Extract Constant Even.even_odd_dec =>
"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.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).

Extraction "/tmp/test.ml" test fact pred minus max min Div2.div2.
*)

¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.