From be4d6e42dfa287b93b1a35ec820ab2a5aaf8c7ec Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 19 May 2013 09:54:40 +0000 Subject: 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 --- lib/Floats.v | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) (limited to 'lib') 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 -- cgit v1.2.3