Module Archi

From Flocq Require Import Binary Bits.
Require Import ZArith List.

Definition ptr64 := false.

Definition big_endian := true.

Definition align_int64 := 8%Z.
Definition align_float64 := 8%Z.

Parameter ppc64 : bool.

Parameter single_passed_as_single : bool.

Definition splitlong := negb ppc64.

Lemma splitlong_ptr32: splitlong = true -> ptr64 = false.

Definition default_nan_64 := (false, iter_nat 51 _ xO xH).
Definition default_nan_32 := (false, iter_nat 22 _ xO xH).


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).

Lemma choose_nan_32_idem: forall n,
  choose_nan_32 (n :: n :: nil) = choose_nan_32 (n :: nil).

Definition fma_order {A: Type} (x y z: A) := (x, z, y).

Definition fma_invalid_mul_is_nan := false.

Definition float_of_single_preserves_sNaN := true.

Definition float_conversion_default_nan := false.

Global Opaque ptr64 big_endian splitlong
              default_nan_64 choose_nan_64
              default_nan_32 choose_nan_32
              fma_order fma_invalid_mul_is_nan
              float_of_single_preserves_sNaN
              float_conversion_default_nan.