fast bitwise operations (lor,land,lxor) on int31 and BigN

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15727 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 9 insertions, 2 deletions

diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
index 9a8a7691ca..39e086c311 100644
--- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
+++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
@@ -88,7 +88,11 @@ Module ZnZ.
     is_even     : t -> bool;
     (* square root *)
     sqrt2       : t -> t -> t * carry t;
-    sqrt        : t -> t  }.
+    sqrt        : t -> t;
+    (* bitwise operations *)
+    lor         : t -> t -> t;
+    land        : t -> t -> t;
+    lxor        : t -> t -> t }.
 
  Section Specs.
  Context {t : Type}{ops : Ops t}.
@@ -199,7 +203,10 @@ Module ZnZ.
           [||WW x y||] = [|s|] ^ 2 + [+|r|] /\
           [+|r|] <= 2 * [|s|];
     spec_sqrt : forall x,
-       [|sqrt x|] ^ 2 <= [|x|] < ([|sqrt x|] + 1) ^ 2
+       [|sqrt x|] ^ 2 <= [|x|] < ([|sqrt x|] + 1) ^ 2;
+    spec_lor : forall x y, [|lor x y|] = Z.lor [|x|] [|y|];
+    spec_land : forall x y, [|land x y|] = Z.land [|x|] [|y|];
+    spec_lxor : forall x y, [|lxor x y|] = Z.lxor [|x|] [|y|]
   }.
 
  End Specs.