diff options
author | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
commit | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch) | |
tree | 97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /plugins/extraction/ExtrOcamlZInt.v | |
parent | 300293c119981054c95182a90c829058530a6b6f (diff) |
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'plugins/extraction/ExtrOcamlZInt.v')
-rw-r--r-- | plugins/extraction/ExtrOcamlZInt.v | 66 |
1 files changed, 34 insertions, 32 deletions
diff --git a/plugins/extraction/ExtrOcamlZInt.v b/plugins/extraction/ExtrOcamlZInt.v index a7046626..55ba0ca1 100644 --- a/plugins/extraction/ExtrOcamlZInt.v +++ b/plugins/extraction/ExtrOcamlZInt.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,7 +8,7 @@ (** Extraction of [positive], [N] and [Z] into Ocaml's [int] *) -Require Import ZArith NArith ZOdiv_def. +Require Import ZArith NArith. Require Import ExtrOcamlBasic. (** Disclaimer: trying to obtain efficient certified programs @@ -33,44 +33,46 @@ Extract Inductive N => int [ "0" "" ] (** 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 => +Extract Constant Pos.add => "(+)". +Extract Constant Pos.succ => "succ". +Extract Constant Pos.pred => "fun n -> max 1 (n-1)". +Extract Constant Pos.sub => "fun n m -> max 1 (n-m)". +Extract Constant Pos.mul => "( * )". +Extract Constant Pos.min => "min". +Extract Constant Pos.max => "max". +Extract Constant Pos.compare => + "fun x y -> if x=y then Eq else if x<y then Lt else Gt". +Extract Constant Pos.compare_cont => "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 => +Extract Constant N.add => "(+)". +Extract Constant N.succ => "succ". +Extract Constant N.pred => "fun n -> max 0 (n-1)". +Extract Constant N.sub => "fun n m -> max 0 (n-m)". +Extract Constant N.mul => "( * )". +Extract Constant N.min => "min". +Extract Constant N.max => "max". +Extract Constant N.div => "fun a b -> if b=0 then 0 else a/b". +Extract Constant N.modulo => "fun a b -> if b=0 then a else a mod b". +Extract Constant N.compare => "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 => +Extract Constant Z.add => "(+)". +Extract Constant Z.succ => "succ". +Extract Constant Z.pred => "pred". +Extract Constant Z.sub => "(-)". +Extract Constant Z.mul => "( * )". +Extract Constant Z.opp => "(~-)". +Extract Constant Z.abs => "abs". +Extract Constant Z.min => "min". +Extract Constant Z.max => "max". +Extract Constant Z.compare => "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". +Extract Constant Z.of_N => "fun p -> p". +Extract Constant Z.abs_N => "abs". (** Zdiv and Zmod are quite complex to define in terms of (/) and (mod). For the moment we don't even try *) |