From e884946c8788db4eb791fa93761d487b9de13ae4 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Fri, 29 Oct 2010 14:21:59 +0000
Subject: float->int conversions, continued: weaker axiomatization.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1545 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 arm/SelectOpproof.v     |  4 ++--
 extraction/extraction.v |  1 -
 ia32/SelectOpproof.v    |  4 ++--
 lib/Floats.v            | 25 +++----------------------
 powerpc/SelectOpproof.v |  4 ++--
 5 files changed, 9 insertions(+), 29 deletions(-)

diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v
index 87dc63e..cdb21cb 100644
--- a/arm/SelectOpproof.v
+++ b/arm/SelectOpproof.v
@@ -953,8 +953,8 @@ Proof.
   econstructor. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor.
   simpl. auto.
   caseEq (Float.cmp Clt x fm); intros.
-  rewrite Float.intuoffloat_intoffloat_1 in H0; auto.
-  EvalOp. simpl. rewrite H0; auto.
+  exploit Float.intuoffloat_intoffloat_1; eauto. intro EQ.
+  EvalOp. simpl. rewrite EQ; auto.
   exploit Float.intuoffloat_intoffloat_2; eauto. intro EQ.
   replace n with (Int.add (Int.sub n Float.ox8000_0000) Float.ox8000_0000).
   apply eval_addimm. eapply eval_intoffloat; eauto.
diff --git a/extraction/extraction.v b/extraction/extraction.v
index 984bee0..8e3c1aa 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -30,7 +30,6 @@ Extract Inlined Constant Floats.float => "float".
 Extract Constant Floats.Float.zero   => "0.".
 Extract Constant Floats.Float.neg => "( ~-. )".
 Extract Constant Floats.Float.abs => "abs_float".
-Extract Constant Floats.Float.of_Z => "fun x -> assert false".
 Extract Constant Floats.Float.singleoffloat => "Floataux.singleoffloat".
 Extract Constant Floats.Float.intoffloat => "Floataux.intoffloat".
 Extract Constant Floats.Float.intuoffloat => "Floataux.intuoffloat".
diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v
index 4279f29..3d6a667 100644
--- a/ia32/SelectOpproof.v
+++ b/ia32/SelectOpproof.v
@@ -894,8 +894,8 @@ Proof.
   econstructor. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor.
   simpl. auto.
   caseEq (Float.cmp Clt x fm); intros.
-  rewrite Float.intuoffloat_intoffloat_1 in H0; auto.
-  EvalOp. simpl. rewrite H0; auto.
+  exploit Float.intuoffloat_intoffloat_1; eauto. intro EQ.
+  EvalOp. simpl. rewrite EQ; auto.
   exploit Float.intuoffloat_intoffloat_2; eauto. intro EQ.
   replace n with (Int.add (Int.sub n Float.ox8000_0000) Float.ox8000_0000).
   apply eval_addimm. eapply eval_intoffloat; eauto.
diff --git a/lib/Floats.v b/lib/Floats.v
index 50712af..f6af7bf 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -31,8 +31,6 @@ Parameter zero: float.                  (**r the float [+0.0] *)
 
 Axiom eq_dec: forall (f1 f2: float), {f1 = f2} + {f1 <> f2}.
 
-Parameter of_Z: Z -> float.             (**r conversion from exact integers, for specification *)
-
 (** Arithmetic operations *)
 
 Parameter neg: float -> float.          (**r opposite (change sign) *)
@@ -118,18 +116,6 @@ Axiom bits_of_singleoffloat:
 Axiom singleoffloat_of_bits:
   forall b, singleoffloat (single_of_bits b) = single_of_bits b.
 
-(** Range of conversions from floats to ints. *)
-
-Axiom intuoffloat_defined:
-  forall f, 
-  cmp Clt f (of_Z Int.modulus) = true /\ cmp Cge f zero = true
-  <-> exists n, intuoffloat f = Some n.
-
-Axiom intoffloat_defined:
-  forall f, 
-  cmp Clt f (of_Z Int.half_modulus) = true /\ cmp Cgt f (of_Z (- Int.half_modulus - 1)) = true
-  <-> exists n, intoffloat f = Some n.
-
 (** 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
@@ -149,9 +135,10 @@ Axiom floatofintu_floatofint_2:
                       (floatofintu ox8000_0000).
 
 Axiom intuoffloat_intoffloat_1:
-  forall x,
+  forall x n,
   cmp Clt x (floatofintu ox8000_0000) = true ->
-  intuoffloat x = intoffloat x.
+  intuoffloat x = Some n ->
+  intoffloat x = Some n.
 
 Axiom intuoffloat_intoffloat_2:
   forall x n,
@@ -159,12 +146,6 @@ Axiom intuoffloat_intoffloat_2:
   intuoffloat x = Some n ->
   intoffloat (sub x (floatofintu ox8000_0000)) = Some (Int.sub n ox8000_0000).
 
-Axiom intuoffloat_intoffloat_3:
-  forall x n,
-  cmp Clt x (floatofintu ox8000_0000) = false ->
-  intoffloat (sub x (floatofintu ox8000_0000)) = Some n ->
-  intuoffloat x = Some (Int.add n ox8000_0000).
-
 (** Conversions from ints to floats can be defined as bitwise manipulations
   over the in-memory representation.  This is what the PowerPC port does.
   The trick is that [from_words 0x4330_0000 x] is the float
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index 60c11dc..1f2c736 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -871,8 +871,8 @@ Proof.
   econstructor. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor.
   simpl. auto.
   caseEq (Float.cmp Clt x fm); intros.
-  rewrite Float.intuoffloat_intoffloat_1 in H0; auto.
-  EvalOp. simpl. rewrite H0; auto.
+  exploit Float.intuoffloat_intoffloat_1; eauto. intro EQ.
+  EvalOp. simpl. rewrite EQ; auto.
   exploit Float.intuoffloat_intoffloat_2; eauto. intro EQ.
   replace n with (Int.add (Int.sub n Float.ox8000_0000) Float.ox8000_0000).
   apply eval_addimm. eapply eval_intoffloat; eauto.
-- 
cgit v1.2.3