1 files changed, 30 insertions, 14 deletions

diff --git a/powerpc/Archi.v b/powerpc/Archi.v
index 5d11aad1..10f38391 100644
--- a/powerpc/Archi.v
+++ b/powerpc/Archi.v
@@ -16,9 +16,9 @@
 
 (** Architecture-dependent parameters for PowerPC *)
 
-Require Import ZArith.
-Require Import Fappli_IEEE.
-Require Import Fappli_IEEE_bits.
+Require Import ZArith List.
+(*From Flocq*)
+Require Import Binary Bits.
 
 Definition ptr64 := false.
 
@@ -30,6 +30,10 @@ Definition align_float64 := 8%Z.
 (** Can we use the 64-bit extensions to the PowerPC architecture? *)
 Parameter ppc64 : bool.
 
+(** Should single-precision FP arguments passed on stack be passed 
+    as singles or use double FP format. *)
+Parameter single_passed_as_single : bool.
+
 Definition splitlong := negb ppc64.
 
 Lemma splitlong_ptr32: splitlong = true -> ptr64 = false.
@@ -37,21 +41,33 @@ Proof.
   reflexivity.
 Qed.
 
-Program Definition default_pl_64 : bool * nan_pl 53 :=
-  (false, iter_nat 51 _ xO xH).
+Definition default_nan_64 := (false, iter_nat 51 _ xO xH).
+Definition default_nan_32 := (false, iter_nat 22 _ xO xH).
+
+(* Always choose the first NaN argument, if any *)
+
+Definition choose_nan_64 (l: list (bool * positive)) : bool * positive :=
+  match l with nil => default_nan_64 | n :: _ => n end.
+
+Definition choose_nan_32 (l: list (bool * positive)) : bool * positive :=
+  match l with nil => default_nan_32 | n :: _ => n end.
+
+Lemma choose_nan_64_idem: forall n,
+  choose_nan_64 (n :: n :: nil) = choose_nan_64 (n :: nil).
+Proof. auto. Qed.
 
-Definition choose_binop_pl_64 (s1: bool) (pl1: nan_pl 53) (s2: bool) (pl2: nan_pl 53) :=
-  false.                        (**r always choose first NaN *)
+Lemma choose_nan_32_idem: forall n,
+  choose_nan_32 (n :: n :: nil) = choose_nan_32 (n :: nil).
+Proof. auto. Qed.
 
-Program Definition default_pl_32 : bool * nan_pl 24 :=
-  (false, iter_nat 22 _ xO xH).
+Definition fma_order {A: Type} (x y z: A) := (x, z, y).
 
-Definition choose_binop_pl_32 (s1: bool) (pl1: nan_pl 24) (s2: bool) (pl2: nan_pl 24) :=
-  false.                        (**r always choose first NaN *)
+Definition fma_invalid_mul_is_nan := false.
 
 Definition float_of_single_preserves_sNaN := true.
 
 Global Opaque ptr64 big_endian splitlong
-              default_pl_64 choose_binop_pl_64
-              default_pl_32 choose_binop_pl_32
-              float_of_single_preserves_sNaN.
\ No newline at end of file
+              default_nan_64 choose_nan_64
+              default_nan_32 choose_nan_32
+              fma_order fma_invalid_mul_is_nan
+              float_of_single_preserves_sNaN.