| products/sources/formale Sprachen/Coq/plugins/extraction/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: ExtrOcamlNatBigInt.v Sprache: CoqUntersuchung 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. *) ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.41Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤ |
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
ZieleEntwicklung einer Software für die statische QuellcodeanalyseBot Zugriff |
