diff options
Diffstat (limited to 'powerpc/Nan.v')
| -rw-r--r-- | powerpc/Nan.v | 38 |
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. |