blob: d66d6ec11d8c741539d70f712cbd7626ea14a428 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
|
Require Import Fappli_IEEE.
Require Import Fappli_IEEE_bits.
Require Import Floats.
Require Import ZArith.
Require Import Integers.
(* Needed to break a circular reference after extraction *)
Definition transform_quiet_pl :=
Eval unfold Float.transform_quiet_pl in Float.transform_quiet_pl.
Program Definition default_pl : bool * nan_pl 53 := (false, nat_iter 51 xO xH).
Definition binop_pl (pl1 pl2:binary64) : bool*nan_pl 53 :=
match pl1, pl2 with
| B754_nan s1 pl1, B754_nan s2 pl2 =>
if (Pos.testbit (proj1_sig pl1) 51 && (* pl2 is sNan but pl1 is qNan *)
negb (Pos.testbit (proj1_sig pl2) 51))%bool
then (s2, transform_quiet_pl pl2)
else (s1, transform_quiet_pl pl1)
| B754_nan s1 pl1, _ => (s1, transform_quiet_pl pl1)
| _, B754_nan s2 pl2 => (s2, transform_quiet_pl pl2)
| _, _ => default_pl
end.
Theorem binop_propagate1: Float.binop_propagate1_prop binop_pl.
Proof.
repeat intro. destruct f1, f2; try discriminate; simpl;
destruct Pos.testbit; reflexivity.
Qed.
Theorem binop_propagate2: Float.binop_propagate2_prop binop_pl.
Proof.
repeat intro. destruct f1, f2, f3; try discriminate; simpl; reflexivity.
Qed.
|
