Merge of the float32 branch:

- added RTL type "Tsingle"
- ABI-compatible passing of single-precision floats on ARM and x86


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

1 files changed, 28 insertions, 0 deletions

diff --git a/lib/Floats.v b/lib/Floats.v
index 02ff25c..3edf39c 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -319,6 +319,28 @@ Proof.
   intros; unfold singleoffloat; rewrite binary32offloatofbinary32; reflexivity.
 Qed.
 
+Definition is_single (f: float) : Prop := exists s, f = floatofbinary32 s.
+
+Theorem singleoffloat_is_single:
+  forall f, is_single (singleoffloat f).
+Proof.
+  intros. exists (binary32offloat f); auto.
+Qed.
+
+Theorem singleoffloat_of_single:
+  forall f, is_single f -> singleoffloat f = f.
+Proof.
+  intros. destruct H as [s EQ]. subst f. unfold singleoffloat. 
+  rewrite binary32offloatofbinary32; reflexivity.
+Qed.
+
+Theorem is_single_dec: forall f, {is_single f} + {~is_single f}.
+Proof.
+  intros. case (eq_dec (singleoffloat f) f); intros.
+  unfold singleoffloat in e. left. exists (binary32offloat f). auto.
+  right; red; intros; elim n. apply singleoffloat_of_single; auto.
+Defined.
+
 (** Properties of comparisons. *)
 
 Theorem order_float_finite_correct:
@@ -470,6 +492,12 @@ Proof.
   intro; unfold singleoffloat, single_of_bits; rewrite binary32offloatofbinary32; reflexivity.
 Qed.
 
+Theorem single_of_bits_is_single:
+  forall b, is_single (single_of_bits b).
+Proof.
+  intros. exists (b32_of_bits (Int.unsigned b)); auto.
+Qed.
+
 (** Conversions between floats and unsigned ints can be defined
   in terms of conversions between floats and signed ints.
   (Most processors provide only the latter, forcing the compiler