Commit 65c353c6 authored by François Bobot's avatar François Bobot
Browse files

Fix is_subnormal

parent 0bef17d9
-R ../_build/default/farith2/thry Farith2
-R ../_build/default/farith2/thry Farith
(coq.extraction
(prelude extraction)
(extracted_modules BinNums Bool Qextended Utils Binary BinPosDef Datatypes Round Zaux BinarySingleNaN
BinPos Interval SpecFloat Zbool BinInt Bits Specif Zpower Assert GenericFloat Version
BinPos Interval SpecFloat FloatClass Zbool BinInt Bits Specif Zpower Assert GenericFloat Version
Defs Operations Op)
(theories Farith2))
(theories Farith))
From Flocq Require Import Core.Zaux IEEE754.BinarySingleNaN IEEE754.Bits Version.
From Farith2 Require Import Qextended GenericFloat.
From Farith Require Import Qextended GenericFloat.
From Coq Require Import Extraction Lia Arith.Wf_nat ZArith.
(* Goal (Beqb (B32.add mode_NE (B32.of_q mode_NE Qx_half) (B32.of_q mode_NE Qx_half)) (B32.of_q mode_NE Qx_one) = true). *)
......@@ -265,7 +265,7 @@ Extract Inlined Constant Qextended.Qx_classify => "Q.classify".
Extract Inductive Qx_kind => "Q.kind" [ "Q.INF" "Q.MINF" "Q.UNDEF" "Q.ZERO" "Q.NZERO" ].
Extract Inlined Constant Qx_classify => "Q.classify".
Extract Inductive mode => "Farith_Big.mode" [
Extract Inductive mode => "Farith_Big.mode" [
"Farith_Big.NE" "Farith_Big.ZR" "Farith_Big.DN" "Farith_Big.UP" "Farith_Big.NA"
].
......
type float_class =
| PNormal
| NNormal
| PSubn
| NSubn
| PZero
| NZero
| PInf
| NInf
| NaN
type float_class =
| PNormal
| NNormal
| PSubn
| NSubn
| PZero
| NZero
| PInf
| NInf
| NaN
......@@ -3,6 +3,7 @@ open Binary
open BinarySingleNaN
open Bits
open Datatypes
open FloatClass
open Interval
open Op
open Qextended
......@@ -339,6 +340,22 @@ module GenericFloat =
let inf mw0 ew0 b =
(fun x f -> assert x; f ()) (check_param mw0 ew0) (fun _ ->
mk_generic mw0 ew0 (fun _ _ _ _ -> B754_infinity b))
(** val classify : binary_float coq_Generic -> float_class **)
let classify f =
match f.value with
| B754_zero s -> if s then NZero else PZero
| B754_infinity s -> if s then NInf else PInf
| B754_nan -> NaN
| B754_finite (s, m, _) ->
if s
then if Farith_Big.eq (digits2_pos m) (Z.to_pos (prec f))
then NNormal
else NSubn
else if Farith_Big.eq (digits2_pos m) (Z.to_pos (prec f))
then PNormal
else PSubn
end
module GenericInterval =
......
......@@ -3,6 +3,7 @@ open Binary
open BinarySingleNaN
open Bits
open Datatypes
open FloatClass
open Interval
open Op
open Qextended
......@@ -125,6 +126,8 @@ module GenericFloat :
val zero : Farith_Big.big_int -> Farith_Big.big_int -> bool -> t
val inf : Farith_Big.big_int -> Farith_Big.big_int -> bool -> t
val classify : binary_float coq_Generic -> float_class
end
module GenericInterval :
......
......@@ -20,11 +20,13 @@
(rule (action (copy ../extract/BinPos.ml BinPos.ml)) (mode promote))
(rule (action (copy ../extract/Interval.ml Interval.ml)) (mode promote))
(rule (action (copy ../extract/SpecFloat.ml SpecFloat.ml)) (mode promote))
(rule (action (copy ../extract/FloatClass.ml FloatClass.ml)) (mode promote))
(rule (action (copy ../extract/Zbool.ml Zbool.ml)) (mode promote))
(rule (action (copy ../extract/BinarySingleNaN.mli BinarySingleNaN.mli)) (mode promote))
(rule (action (copy ../extract/BinPos.mli BinPos.mli)) (mode promote))
(rule (action (copy ../extract/Interval.mli Interval.mli)) (mode promote))
(rule (action (copy ../extract/SpecFloat.mli SpecFloat.mli)) (mode promote))
(rule (action (copy ../extract/FloatClass.mli FloatClass.mli)) (mode promote))
(rule (action (copy ../extract/Zbool.mli Zbool.mli)) (mode promote))
(rule (action (copy ../extract/BinInt.ml BinInt.ml)) (mode promote))
(rule (action (copy ../extract/Bits.ml Bits.ml)) (mode promote))
......
......@@ -19,7 +19,6 @@
(* *)
(**************************************************************************)
open Base
module Format = Stdlib.Format
module Z = struct
......@@ -28,14 +27,24 @@ module Z = struct
let hash_fold_t s t = Base.Hash.fold_int s (hash t)
end
type mode = Farith_Big.mode = NE | ZR | DN | UP | NA
[@@deriving eq, ord, hash]
module Mode = struct
type t = Farith_Big.mode = NE | ZR | DN | UP | NA
[@@deriving eq, ord, hash, show]
end
type classify = Farith_Big.classify =
| Zero of bool
| Infinity of bool
| NaN
| Finite of bool * Z.t * Z.t
module Classify = struct
type t = FloatClass.float_class =
| PNormal
| NNormal
| PSubn
| NSubn
| PZero
| NZero
| PInf
| NInf
| NaN
[@@deriving eq, ord, hash, show]
end
type 'v generic = 'v GenericFloat.coq_Generic = {
mw : Z.t;
......@@ -77,13 +86,14 @@ module F = struct
Format.fprintf fmt "%a%ap%a" pp_sign b Z.pp_print m Z.pp_print e
let pp fmt t = pp_binary_float fmt t.value
let show = Format.asprintf "%a" pp
(** lexer for finite float *)
let lex_float s =
match String.index s 'p' with
| Some k ->
let m = String.sub s ~pos:0 ~len:k in
let e = String.sub s (Int.succ k) (String.length s - k - 1) in
let e = String.sub s ~pos:(Int.succ k) ~len:(String.length s - k - 1) in
(Z.of_string m, Z.of_string e)
| None -> (Z.of_string s, Z.zero)
......@@ -93,46 +103,42 @@ module F = struct
let nan ~mw ~ew = nan (Z.of_int mw) (Z.of_int ew)
let zero ~mw ~ew b = zero (Z.of_int mw) (Z.of_int ew) b
let inf ~mw ~ew b = inf (Z.of_int mw) (Z.of_int ew) b
let round ~mw ~ew mode (f : t) : t =
match f.value with
| B754_zero _ | B754_infinity _ | B754_nan ->
{ mw = Z.of_int mw; ew = Z.of_int ew; value = f.value }
| B754_finite (_, _, _) -> of_q ~mw ~ew mode (to_q f)
let of_float f =
of_bits ~mw:52 ~ew:11 @@ Z.extract (Z.of_int64 (Int64.bits_of_float f)) 0 64
let to_float mode f =
round ~mw:52 ~ew:11 mode f |> to_bits |> fun z ->
Z.signed_extract z 0 64 |> Z.to_int64 |> Int64.float_of_bits
let is_zero t = match t.value with B754_zero _ -> true | _ -> false
let is_infinite t = match t.value with B754_infinity _ -> true | _ -> false
let is_nan t = match t.value with B754_nan -> true | _ -> false
let round ~mw ~ew mode (f:t) : t =
(match f.value with
| B754_zero _
| B754_infinity _
| B754_nan -> { mw = Z.of_int mw; ew = Z.of_int ew; value = f.value }
| B754_finite (_, _, _) ->
(of_q ~mw ~ew mode (to_q f))
)
let of_float f = of_bits ~mw:52 ~ew:11
@@ Z.extract (Z.of_int64 (Int64.bits_of_float f)) 0 64
let to_float mode f = round ~mw:52 ~ew:11 mode f
|> to_bits
|> fun z -> Z.signed_extract z 0 64
|> Z.to_int64
|> Int64.float_of_bits
let is_negative t =
match t.value with
| B754_zero true | B754_finite (true, _, _) -> true
| _ -> false
| B754_infinity b | B754_zero b | B754_finite (b, _, _) -> b
| B754_nan -> false
let is_positive t =
match t.value with
| B754_zero false | B754_finite (false, _, _) -> true
| _ -> false
| B754_infinity b | B754_zero b | B754_finite (b, _, _) -> not b
| B754_nan -> false
let is_normal t =
match t.value with
| B754_zero _ -> true
| B754_finite (_, e, _) when Z.sign e <> 0 -> true
match classify t with
| FloatClass.PNormal | FloatClass.NNormal -> true
| _ -> false
let is_subnormal t =
match t.value with
| B754_finite (_, e, _) when Z.sign e = 0 -> true
match classify t with
| FloatClass.PSubn | FloatClass.NSubn -> true
| _ -> false
end
......
......@@ -21,125 +21,96 @@
(** Float Arithmetics (based on [Flocq] extraction) *)
(** Supported rounding modes *)
type mode =
| NE (** Nearest to even *)
| ZR (** Toward zero *)
| DN (** Toward minus infinity *)
| UP (** Toward plus infinity *)
| NA (** Nearest away from zero *)
[@@deriving eq, ord, hash]
module Mode : sig
(** Supported rounding modes *)
type t =
| NE (** Nearest to even *)
| ZR (** Toward zero *)
| DN (** Toward minus infinity *)
| UP (** Toward plus infinity *)
| NA (** Nearest away from zero *)
[@@deriving eq, ord, hash, show]
end
(** Type used for classifying floating points *)
type classify =
| Zero of bool
| Infinity of bool
| NaN
| Finite of bool * Z.t * Z.t
module Classify : sig
(** Type used for classifying floating points *)
type t =
| PNormal
| NNormal
| PSubn
| NSubn
| PZero
| NZero
| PInf
| NInf
| NaN
[@@deriving eq, ord, hash, show]
end
module F : sig
type t [@@deriving eq, ord, hash]
type t [@@deriving eq, ord, hash, show]
val ew : t -> int
val mw : t -> int
val pp : Format.formatter -> t -> unit
val of_q : mw:int -> ew:int -> mode -> Q.t -> t
val of_q : mw:int -> ew:int -> Mode.t -> Q.t -> t
val to_q : t -> Q.t
val add : mode -> t -> t -> t
val sub : mode -> t -> t -> t
val mul : mode -> t -> t -> t
val div : mode -> t -> t -> t
val fma : mode -> t -> t -> t -> t
val sqrt : mode -> t -> t
val add : Mode.t -> t -> t -> t
val sub : Mode.t -> t -> t -> t
val mul : Mode.t -> t -> t -> t
val div : Mode.t -> t -> t -> t
val fma : Mode.t -> t -> t -> t -> t
val sqrt : Mode.t -> t -> t
val abs : t -> t
val neg : t -> t
val pred : t -> t
val succ : t -> t
val of_bits : mw:int -> ew:int -> Z.t -> t
val to_bits : t -> Z.t
val of_float : float -> t
val to_float : mode -> t -> float
val round: mw:int -> ew:int -> mode -> t -> t
val to_float : Mode.t -> t -> float
val round : mw:int -> ew:int -> Mode.t -> t -> t
val ge : t -> t -> bool
val gt : t -> t -> bool
val le : t -> t -> bool
val lt : t -> t -> bool
val eq : t -> t -> bool
val nan : mw:int -> ew:int -> t
val zero : mw:int -> ew:int -> bool -> t
(** [zero false] is positive zero and [zero true] is negative zero *)
val inf : mw:int -> ew:int -> bool -> t
val is_zero : t -> bool
val is_infinite : t -> bool
val is_nan : t -> bool
val is_negative : t -> bool
val is_positive : t -> bool
val is_normal : t -> bool
val is_subnormal : t -> bool
val classify : t -> Classify.t
end
module I : sig
type t [@@deriving eq, ord, hash]
val ew : t -> int
val mw : t -> int
val pp : Format.formatter -> t -> unit
val top : mw:int -> ew:int -> t
val inter : t -> t -> t option
val add : mode -> t -> t -> t
val add : Mode.t -> t -> t -> t
val ge : t -> t option
val gt : t -> t option
val le : t -> t option
val lt : t -> t option
val singleton : F.t -> t
val is_singleton : t -> F.t option
end
val flocq_version: Z.t
val flocq_version : Z.t
(* (\** {2 Generic Version } *\)
*
......@@ -167,11 +138,11 @@ val flocq_version: Z.t
* (\** {2 Floating point operations} *\)
*
* val opp : 't conf -> 't -> 't
* val add : 't conf -> mode -> 't -> 't -> 't
* val sub : 't conf -> mode -> 't -> 't -> 't
* val mul : 't conf -> mode -> 't -> 't -> 't
* val div : 't conf -> mode -> 't -> 't -> 't
* val sqrt : 't conf -> mode -> 't -> 't
* val add : 't conf -> Mode.t -> 't -> 't -> 't
* val sub : 't conf -> Mode.t -> 't -> 't -> 't
* val mul : 't conf -> Mode.t -> 't -> 't -> 't
* val div : 't conf -> Mode.t -> 't -> 't -> 't
* val sqrt : 't conf -> Mode.t -> 't -> 't
* val abs : 't conf -> 't -> 't
*
* (\** {2 Conversions} *\)
......@@ -184,23 +155,23 @@ val flocq_version: Z.t
* val to_bits : 't conf -> 't -> Z.t
* (\** Convert the floating point to its bitvector representation *\)
*
* val of_z : 't conf -> mode -> Z.t -> 't
* val of_z : 't conf -> Mode.t -> Z.t -> 't
* (\** Convert the integer to the nearest representable integer *\)
*
* val of_q : 't conf -> mode -> Q.t -> 't
* val of_q : 't conf -> Mode.t -> Q.t -> 't
* (\** Convert the rational to the nearest representable integer. *\)
*
* val to_q : 't conf -> 't -> Q.t
* (\** Convert the floating-point to its rational representation. *\)
*
* val conv : 't1 conf -> 't2 conf -> mode -> 't1 -> 't2
* val conv : 't1 conf -> 't2 conf -> Mode.t -> 't1 -> 't2
* (\** Convert the floating point to the nearest representable floating point
* having another mantissa and exponent size. *\)
*
* val roundq : mw:int -> ew:int -> mode -> Q.t -> Q.t
* val roundq : mw:int -> ew:int -> Mode.t -> Q.t -> Q.t
* (\** Round the given rational to the nearest representable floating
* point with the mantissa width [mw] and exponent width [ew] using
* the rounding mode [mode].
* the rounding Mode.t [Mode.t].
* *\)
*
* (\** {2 Floating point constants} *\)
......@@ -225,8 +196,8 @@ val flocq_version: Z.t
*
* val default_nan: 't conf -> 't
*
* val finite: 't conf -> mode -> Z.t -> Z.t -> 't
* (\** [finite conf mode m e] return the rounded floating point
* val finite: 't conf -> Mode.t -> Z.t -> Z.t -> 't
* (\** [finite conf Mode.t m e] return the rounded floating point
* corresponding to m*2^e. Beware of the result can be classified
* not only as finite but also as infinite or zero because of the
* rounding.
......@@ -278,11 +249,11 @@ val flocq_version: Z.t
* (\** {2 Floating point operations} *\)
*
* val opp : t -> t
* val add : mode -> t -> t -> t
* val sub : mode -> t -> t -> t
* val mul : mode -> t -> t -> t
* val div : mode -> t -> t -> t
* val sqrt : mode -> t -> t
* val add : Mode.t -> t -> t -> t
* val sub : Mode.t -> t -> t -> t
* val mul : Mode.t -> t -> t -> t
* val div : Mode.t -> t -> t -> t
* val sqrt : Mode.t -> t -> t
* val abs : t -> t
*
* (\** {2 conversions} *\)
......@@ -295,16 +266,16 @@ val flocq_version: Z.t
* val to_bits : t -> Z.t
* (\** Convert the floating point to its bitvector representation *\)
*
* val of_z : mode -> Z.t -> t
* val of_z : Mode.t -> Z.t -> t
* (\** Convert the integer to the nearest representable integer *\)
*
* val of_q : mode -> Q.t -> t
* val of_q : Mode.t -> Q.t -> t
* (\** Convert the rational to the nearest representable integer. *\)
*
* val to_q : t -> Q.t
* (\** Convert the floating-point to its rational representation. *\)
*
* val conv : 't D.conf -> mode -> t -> 't
* val conv : 't D.conf -> Mode.t -> t -> 't
* (\** Convert the floating point to the nearest representable floating point
* having another mantissa and exponent size. *\)
*
......@@ -330,8 +301,8 @@ val flocq_version: Z.t
*
* val default_nan: t
*
* val finite: mode -> Z.t -> Z.t -> t
* (\** [finite conf mode m e] return the rounded floating point
* val finite: Mode.t -> Z.t -> Z.t -> t
* (\** [finite conf Mode.t m e] return the rounded floating point
* corresponding to m*2^e. Beware of the result can be classified
* not only as finite but also as infinite or zero because of the
* rounding. *\)
......@@ -365,7 +336,7 @@ val flocq_version: Z.t
* val pp : Format.formatter -> t -> unit
*
*
* val of_string: mode -> string -> t
* val of_string: Mode.t -> string -> t
* (\** convert string of the shape "[-+][0-9]+p[-+][0-9]+" or "[-+][0-9]+"
* to a floating point using the given rounding *\)
* end
......
From Flocq Require Import Core.Core IEEE754.BinarySingleNaN IEEE754.Bits.
From Coq Require Import Program ZArith Bool Lia Reals Qreals ZBits.
From Coq Require Import Program ZArith Bool Lia Reals Qreals ZBits SpecFloat FloatClass.
Require Import Assert Utils Interval Qextended Rextended Op.
Definition cprec mw := (Z.succ mw)%Z.
......@@ -423,7 +423,24 @@ Module GenericFloat.
Definition inf mw ew b : t :=
AssertF.assert (check_param mw ew) (fun H => mk_generic mw ew H (fun _ _ _ _ => B754_infinity b)).
(** SFclassify is currently false:
https://github.com/coq/coq/issues/16096
*)
Definition classify f : float_class :=
match value f with
| B754_nan => FloatClass.NaN
| B754_infinity false => PInf
| B754_infinity true => NInf
| B754_zero false => PZero
| B754_zero true => NZero
| B754_finite false m _ _ =>
if (digits2_pos m =? Z.to_pos (prec f))%positive then PNormal
else PSubn
| B754_finite true m _ _ =>
if (digits2_pos m =? Z.to_pos (prec f))%positive then NNormal
else NSubn
end.
End GenericFloat.
Module GenericInterval.
......
(coq.theory
(name Farith2)
; (package farith2)
(name Farith)
(synopsis "Manipulation of float with arbitrary precision extracted from the Flocq library")
; (modules <ordered_set_lang>)
; (theories Flocq)
)
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment