diff options
Diffstat (limited to 'lib/Floats.v')
-rw-r--r-- | lib/Floats.v | 25 |
1 files changed, 3 insertions, 22 deletions
diff --git a/lib/Floats.v b/lib/Floats.v index 50712af2..f6af7bf0 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 |