lib/Integers.v: revised and extended, faster implementation based on

  bit-level operations provided by ZArith in Coq 8.4.
Other modules: adapted accordingly.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2110 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

2 files changed, 24 insertions, 23 deletions

diff --git a/common/Memdata.v b/common/Memdata.v
index 5f06d2c..8afe752 100644
--- a/common/Memdata.v
+++ b/common/Memdata.v
@@ -190,7 +190,7 @@ Opaque Byte.wordsize.
   replace (Zsucc (Z_of_nat n) * 8) with (Z_of_nat n * 8 + 8) by omega.
   rewrite two_p_is_exp; try omega. 
   rewrite Zmod_recombine. rewrite IHn. rewrite Zplus_comm. 
-  rewrite Byte.Z_mod_two_p_eq. reflexivity. 
+  rewrite Byte.Z_mod_modulus_eq. reflexivity. 
   apply two_p_gt_ZERO. omega. apply two_p_gt_ZERO. omega.
 Qed.
 
@@ -214,7 +214,7 @@ Lemma decode_encode_int_1:
 Proof.
   intros. rewrite decode_encode_int. 
   rewrite <- (Int.repr_unsigned (Int.zero_ext 8 x)).
-  decEq. symmetry. apply Int.zero_ext_mod. compute; auto. 
+  decEq. symmetry. apply Int.zero_ext_mod. compute. intuition congruence. 
 Qed.
 
 Lemma decode_encode_int_2:
@@ -222,7 +222,7 @@ Lemma decode_encode_int_2:
 Proof.
   intros. rewrite decode_encode_int. 
   rewrite <- (Int.repr_unsigned (Int.zero_ext 16 x)).
-  decEq. symmetry. apply Int.zero_ext_mod. compute; auto. 
+  decEq. symmetry. apply Int.zero_ext_mod. compute; intuition congruence.
 Qed.
 
 Lemma decode_encode_int_4:
@@ -419,14 +419,14 @@ Opaque inj_pointer.
   destruct v; destruct chunk1; simpl; try (apply decode_val_undef);
   destruct chunk2; unfold decode_val; auto; try (rewrite proj_inj_bytes).
   (* int-int *)
-  rewrite decode_encode_int_1. decEq. apply Int.sign_ext_zero_ext. compute; auto.
-  rewrite decode_encode_int_1. decEq. apply Int.zero_ext_idem. compute; auto.
-  rewrite decode_encode_int_1. decEq. apply Int.sign_ext_zero_ext. compute; auto.
-  rewrite decode_encode_int_1. decEq. apply Int.zero_ext_idem. compute; auto.
-  rewrite decode_encode_int_2. decEq. apply Int.sign_ext_zero_ext. compute; auto.
-  rewrite decode_encode_int_2. decEq. apply Int.zero_ext_idem. compute; auto.
-  rewrite decode_encode_int_2. decEq. apply Int.sign_ext_zero_ext. compute; auto.
-  rewrite decode_encode_int_2. decEq. apply Int.zero_ext_idem. compute; auto.
+  rewrite decode_encode_int_1. decEq. apply Int.sign_ext_zero_ext. omega.
+  rewrite decode_encode_int_1. decEq. apply Int.zero_ext_idem. omega.
+  rewrite decode_encode_int_1. decEq. apply Int.sign_ext_zero_ext. omega.
+  rewrite decode_encode_int_1. decEq. apply Int.zero_ext_idem. omega.
+  rewrite decode_encode_int_2. decEq. apply Int.sign_ext_zero_ext. omega.
+  rewrite decode_encode_int_2. decEq. apply Int.zero_ext_idem. omega.
+  rewrite decode_encode_int_2. decEq. apply Int.sign_ext_zero_ext. omega.
+  rewrite decode_encode_int_2. decEq. apply Int.zero_ext_idem. omega.
   rewrite decode_encode_int_4. auto.
   rewrite decode_encode_int_4. auto.
   rewrite decode_encode_int_4. auto.
@@ -482,7 +482,8 @@ Qed.
 Lemma encode_val_int8_zero_ext:
   forall n, encode_val Mint8unsigned (Vint (Int.zero_ext 8 n)) = encode_val Mint8unsigned (Vint n).
 Proof.
-  intros; unfold encode_val. decEq. apply encode_int_8_mod. apply Int.eqmod_zero_ext. compute; auto.
+  intros; unfold encode_val. decEq. apply encode_int_8_mod. apply Int.eqmod_zero_ext. 
+  compute; intuition congruence.
 Qed.
 
 Lemma encode_val_int8_sign_ext:
@@ -494,7 +495,7 @@ Qed.
 Lemma encode_val_int16_zero_ext:
   forall n, encode_val Mint16unsigned (Vint (Int.zero_ext 16 n)) = encode_val Mint16unsigned (Vint n).
 Proof.
-  intros; unfold encode_val. decEq. apply encode_int_16_mod. apply Int.eqmod_zero_ext. compute; auto.
+  intros; unfold encode_val. decEq. apply encode_int_16_mod. apply Int.eqmod_zero_ext. compute; intuition congruence.
 Qed.
 
 Lemma encode_val_int16_sign_ext:
@@ -516,10 +517,10 @@ Lemma decode_val_cast:
   end.
 Proof.
   unfold decode_val; intros; destruct chunk; auto; destruct (proj_bytes l); auto.
-  unfold Val.sign_ext. rewrite Int.sign_ext_idem; auto. compute; auto.
-  unfold Val.zero_ext. rewrite Int.zero_ext_idem; auto. compute; auto.
-  unfold Val.sign_ext. rewrite Int.sign_ext_idem; auto. compute; auto.
-  unfold Val.zero_ext. rewrite Int.zero_ext_idem; auto. compute; auto.
+  unfold Val.sign_ext. rewrite Int.sign_ext_idem; auto. omega.
+  unfold Val.zero_ext. rewrite Int.zero_ext_idem; auto. omega. 
+  unfold Val.sign_ext. rewrite Int.sign_ext_idem; auto. omega.
+  unfold Val.zero_ext. rewrite Int.zero_ext_idem; auto. omega.
   simpl. rewrite Float.singleoffloat_of_bits. auto.
 Qed.
 
diff --git a/common/Values.v b/common/Values.v
index 177cd93..f02fa70 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -428,14 +428,14 @@ Theorem cast8unsigned_and:
   forall x, zero_ext 8 x = and x (Vint(Int.repr 255)).
 Proof.
   destruct x; simpl; auto. decEq. 
-  change 255 with (two_p 8 - 1). apply Int.zero_ext_and. vm_compute; auto.
+  change 255 with (two_p 8 - 1). apply Int.zero_ext_and. omega. 
 Qed.
 
 Theorem cast16unsigned_and:
   forall x, zero_ext 16 x = and x (Vint(Int.repr 65535)).
 Proof.
   destruct x; simpl; auto. decEq. 
-  change 65535 with (two_p 16 - 1). apply Int.zero_ext_and. vm_compute; auto.
+  change 65535 with (two_p 16 - 1). apply Int.zero_ext_and. omega.
 Qed.
 
 Theorem bool_of_val_of_bool:
@@ -600,7 +600,7 @@ Theorem mul_pow2:
   mul x (Vint n) = shl x (Vint logn).
 Proof.
   intros; destruct x; simpl; auto.
-  change 32 with (Z_of_nat Int.wordsize).
+  change 32 with Int.zwordsize.
   rewrite (Int.is_power2_range _ _ H). decEq. apply Int.mul_pow2. auto.
 Qed.  
 
@@ -929,17 +929,17 @@ Qed.
 
 Lemma zero_ext_and:
   forall n v, 
-  0 < n < Z_of_nat Int.wordsize ->
+  0 < n < Int.zwordsize ->
   Val.zero_ext n v = Val.and v (Vint (Int.repr (two_p n - 1))).
 Proof.
-  intros. destruct v; simpl; auto. decEq. apply Int.zero_ext_and; auto.
+  intros. destruct v; simpl; auto. decEq. apply Int.zero_ext_and; auto. omega.
 Qed.
 
 Lemma rolm_lt_zero:
   forall v, rolm v Int.one Int.one = cmp Clt v (Vint Int.zero).
 Proof.
   intros. unfold cmp, cmp_bool; destruct v; simpl; auto.
-  transitivity (Vint (Int.shru i (Int.repr (Z_of_nat Int.wordsize - 1)))).
+  transitivity (Vint (Int.shru i (Int.repr (Int.zwordsize - 1)))).
   decEq. symmetry. rewrite Int.shru_rolm. auto. auto. 
   rewrite Int.shru_lt_zero. destruct (Int.lt i Int.zero); auto. 
 Qed.