From 157bee13827f9a616b6c82be4af110c8f2464c64 Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 5 May 2011 15:12:23 +0000 Subject: Modularization of BinNat + fixes of stdlib A sub-module N in BinNat now contains functions add (ex-Nplus), mul (ex-Nmult), ... and properties. In particular, this sub-module N directly instantiates NAxiomsSig and includes all derived properties NProp. Files Ndiv_def and co are now obsolete and kept only for compat git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14100 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/extraction/ExtrOcamlZBigInt.v | 20 ++++++++++---------- plugins/extraction/ExtrOcamlZInt.v | 20 ++++++++++---------- 2 files changed, 20 insertions(+), 20 deletions(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/ExtrOcamlZBigInt.v b/plugins/extraction/ExtrOcamlZBigInt.v index fd8ad6d77..c73451e5c 100644 --- a/plugins/extraction/ExtrOcamlZBigInt.v +++ b/plugins/extraction/ExtrOcamlZBigInt.v @@ -48,18 +48,18 @@ Extract Constant Pos.compare => Extract Constant Pos.compare_cont => "fun x y c -> Big.compare_case c Lt Gt x y". -Extract Constant Nplus => "Big.add". -Extract Constant Nsucc => "Big.succ". -Extract Constant Npred => "fun n -> Big.max Big.zero (Big.pred n)". -Extract Constant Nminus => "fun n m -> Big.max Big.zero (Big.sub n m)". -Extract Constant Nmult => "Big.mult". -Extract Constant Nmin => "Big.min". -Extract Constant Nmax => "Big.max". -Extract Constant Ndiv => +Extract Constant N.add => "Big.add". +Extract Constant N.succ => "Big.succ". +Extract Constant N.pred => "fun n -> Big.max Big.zero (Big.pred n)". +Extract Constant N.sub => "fun n m -> Big.max Big.zero (Big.sub n m)". +Extract Constant N.mul => "Big.mult". +Extract Constant N.min => "Big.min". +Extract Constant N.max => "Big.max". +Extract Constant N.div => "fun a b -> if Big.eq b Big.zero then Big.zero else Big.div a b". -Extract Constant Nmod => +Extract Constant N.modulo => "fun a b -> if Big.eq b Big.zero then Big.zero else Big.modulo a b". -Extract Constant Ncompare => "Big.compare_case Eq Lt Gt". +Extract Constant N.compare => "Big.compare_case Eq Lt Gt". Extract Constant Zplus => "Big.add". Extract Constant Zsucc => "Big.succ". diff --git a/plugins/extraction/ExtrOcamlZInt.v b/plugins/extraction/ExtrOcamlZInt.v index 013695772..4f6332d3d 100644 --- a/plugins/extraction/ExtrOcamlZInt.v +++ b/plugins/extraction/ExtrOcamlZInt.v @@ -46,16 +46,16 @@ Extract Constant Pos.compare_cont => "fun x y c -> if x=y then c else if x "(+)". -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