summaryrefslogtreecommitdiff
path: root/powerpc/Nan.v
diff options
context:
space:
mode:
Diffstat (limited to 'powerpc/Nan.v')
-rw-r--r--powerpc/Nan.v38
1 files changed, 18 insertions, 20 deletions
diff --git a/powerpc/Nan.v b/powerpc/Nan.v
index 77a752e..c230789 100644
--- a/powerpc/Nan.v
+++ b/powerpc/Nan.v
@@ -1,28 +1,26 @@
+(* *********************************************************************)
+(* *)
+(* The Compcert verified compiler *)
+(* *)
+(* Xavier Leroy, INRIA Paris-Rocquencourt *)
+(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *)
+(* *)
+(* Copyright Institut National de Recherche en Informatique et en *)
+(* Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the GNU General Public License as published by *)
+(* the Free Software Foundation, either version 2 of the License, or *)
+(* (at your option) any later version. This file is also distributed *)
+(* under the terms of the INRIA Non-Commercial License Agreement. *)
+(* *)
+(* *********************************************************************)
+
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, _ => (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; reflexivity.
-Qed.
-
-Theorem binop_propagate2: Float.binop_propagate2_prop binop_pl.
-Proof.
- repeat intro. destruct f1, f2, f3; try discriminate; simpl; reflexivity.
-Qed.
+Definition choose_binop_pl (s1: bool) (pl1: nan_pl 53) (s2: bool) (pl2: nan_pl 53) :=
+ false.