From 7a614ea53948423b0266eefd98ea5714559c3cfc Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Thu, 28 Jun 2012 11:23:52 +0000
Subject: Changelog: updated driver/Interp.ml: clean up dead code
 lib/Integers.v: add shifted_or_is_add lib/Floats.v: add from_words_eq
 .depend: updated

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1940 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 lib/Floats.v   | 14 ++++++++++++++
 lib/Integers.v | 40 ++++++++++++++++++++++++++++++++++++++++
 2 files changed, 54 insertions(+)

(limited to 'lib')

diff --git a/lib/Floats.v b/lib/Floats.v
index e7a7aa0..edb6d6b 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -189,6 +189,20 @@ Definition from_words (hi lo: int) : float :=
     (Int64.or (Int64.shl (Int64.repr (Int.unsigned hi)) (Int64.repr 32))
               (Int64.repr (Int.unsigned lo))).
 
+Lemma from_words_eq:
+  forall lo hi,
+  from_words hi lo =
+  double_of_bits (Int64.repr (Int.unsigned hi * two_p 32 + Int.unsigned lo)).
+Proof.
+  intros. unfold from_words. decEq.
+  rewrite Int64.shifted_or_is_add.
+  apply Int64.eqm_samerepr. auto with ints.
+  change (Z_of_nat Int64.wordsize) with 64. omega.
+  generalize (Int.unsigned_range lo). intros [A B]. 
+  rewrite Int64.unsigned_repr. assumption. 
+  assert (Int.modulus < Int64.max_unsigned). compute; auto. omega.
+Qed.
+
 (** Below are the only properties of floating-point arithmetic that we
   rely on in the compiler proof. *)
 
diff --git a/lib/Integers.v b/lib/Integers.v
index 0dc7997..8dc5b6f 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -1224,6 +1224,24 @@ Proof.
   rewrite inj_S in H. omega. rewrite inj_S in H. omega.
 Qed.
 
+Lemma bits_of_Z_greater:
+  forall n x i,
+  0 <= x < two_p i -> bits_of_Z n x i = false.
+Proof.
+  induction n; intros.
+  auto.
+  destruct (zlt i 0). apply bits_of_Z_below. auto.
+  simpl. 
+  destruct (Z_bin_decomp x) as [b x1]_eqn.
+  destruct (zeq i 0).
+  subst i. simpl in H. assert (x = 0) by omega. subst x. simpl in Heqp. congruence.
+  apply IHn. 
+  rewrite <- (Z_shift_add_bin_decomp x) in H. rewrite Heqp in H. simpl in H.
+  replace i with (Zsucc (i-1)) in H by omega. rewrite two_p_S in H. 
+  unfold Z_shift_add in H. destruct b; omega. 
+  omega.
+Qed.
+
 Lemma bits_of_Z_of_bits_gen':
   forall n f i j,
   bits_of_Z n (Z_of_bits n f j) i =
@@ -2283,6 +2301,28 @@ Proof.
   auto.
 Qed.
 
+Theorem shifted_or_is_add:
+  forall x y n,
+  0 <= n < Z_of_nat wordsize ->
+  unsigned y < two_p n ->
+  or (shl x (repr n)) y = repr(unsigned x * two_p n + unsigned y).
+Proof.
+  intros. rewrite <- add_is_or. 
+  rewrite shl_mul_two_p. rewrite unsigned_repr.
+  unfold add. apply eqm_samerepr. unfold mul. auto with ints. 
+  generalize wordsize_max_unsigned; omega.
+  unfold and, shl, bitwise_binop. unfold zero. decEq. apply Z_of_bits_false. intros.
+  rewrite unsigned_repr; auto with ints. rewrite bits_of_Z_of_bits_gen.
+  rewrite unsigned_repr. apply andb_false_iff.  
+  destruct (zlt j n).
+  left. apply bits_of_Z_below. omega. 
+  right. apply bits_of_Z_greater. 
+  split. generalize (unsigned_range y); omega.
+  assert (two_p n <= two_p j). apply two_p_monotone. omega. omega.
+  generalize wordsize_max_unsigned; omega.
+  omega.
+Qed.
+
 (** Unsigned right shifts and unsigned divisions by powers of 2. *)
 
 Lemma Z_of_bits_shift_right:
-- 
cgit v1.2.3