aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/byterun/coq_fix_code.c1
-rw-r--r--kernel/byterun/coq_interp.c25
-rw-r--r--kernel/byterun/coq_values.h9
-rw-r--r--kernel/cClosure.ml67
-rw-r--r--kernel/cPrimitives.ml24
-rw-r--r--kernel/cPrimitives.mli2
-rw-r--r--kernel/cemitcodes.ml1
-rw-r--r--kernel/float64.ml11
-rw-r--r--kernel/float64.mli5
-rw-r--r--kernel/genOpcodeFiles.ml1
-rw-r--r--kernel/primred.ml35
-rw-r--r--kernel/primred.mli13
-rw-r--r--kernel/retroknowledge.ml10
-rw-r--r--kernel/retroknowledge.mli9
-rw-r--r--kernel/safe_typing.ml20
-rw-r--r--kernel/typeops.ml8
-rw-r--r--pretyping/cbv.ml46
-rw-r--r--pretyping/reductionops.ml45
-rw-r--r--test-suite/primitive/float/classify.v23
-rw-r--r--theories/Floats/FloatAxioms.v2
-rw-r--r--theories/Floats/FloatClass.v2
-rw-r--r--theories/Floats/Floats.v1
-rw-r--r--theories/Floats/PrimFloat.v5
-rw-r--r--theories/Floats/SpecFloat.v17
-rw-r--r--vernac/g_vernac.mlg1
-rw-r--r--vernac/vernacentries.ml1
26 files changed, 369 insertions, 15 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index bca2cc3bd9..fb39ca8358 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -65,6 +65,7 @@ void init_arity () {
arity[CHECKEQINT63]=arity[CHECKLTINT63]=arity[CHECKLEINT63]=
arity[CHECKCOMPAREINT63]=arity[CHECKHEAD0INT63]=arity[CHECKTAIL0INT63]=
arity[CHECKOPPFLOAT]=arity[CHECKABSFLOAT]=arity[CHECKCOMPAREFLOAT]=
+ arity[CHECKCLASSIFYFLOAT]=
arity[CHECKADDFLOAT]=arity[CHECKSUBFLOAT]=arity[CHECKMULFLOAT]=
arity[CHECKDIVFLOAT]=arity[CHECKSQRTFLOAT]=
arity[CHECKFLOATOFINT63]=arity[CHECKFLOATNORMFRMANTISSA]=
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 74edd79872..b862480fda 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -1565,6 +1565,31 @@ value coq_interprete
Next;
}
+ Instruct (CHECKCLASSIFYFLOAT) {
+ double x;
+ print_instr("CHECKCLASSIFYFLOAT");
+ CheckFloat1();
+ x = Double_val(accu);
+ switch (fpclassify(x)) {
+ case FP_NORMAL:
+ accu = signbit(x) ? coq_NNormal : coq_PNormal;
+ break;
+ case FP_SUBNORMAL:
+ accu = signbit(x) ? coq_NSubn : coq_PSubn;
+ break;
+ case FP_ZERO:
+ accu = signbit(x) ? coq_NZero : coq_PZero;
+ break;
+ case FP_INFINITE:
+ accu = signbit(x) ? coq_NInf : coq_PInf;
+ break;
+ default: /* FP_NAN */
+ accu = coq_NaN;
+ break;
+ }
+ Next;
+ }
+
Instruct (CHECKADDFLOAT) {
print_instr("CHECKADDFLOAT");
CheckFloat2();
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index c79a8f1b4f..b027673ac7 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -46,6 +46,15 @@
#define coq_FLt Val_int(1)
#define coq_FGt Val_int(2)
#define coq_FNotComparable Val_int(3)
+#define coq_PNormal Val_int(0)
+#define coq_NNormal Val_int(1)
+#define coq_PSubn Val_int(2)
+#define coq_NSubn Val_int(3)
+#define coq_PZero Val_int(4)
+#define coq_NZero Val_int(5)
+#define coq_PInf Val_int(6)
+#define coq_NInf Val_int(7)
+#define coq_NaN Val_int(8)
#define FLOAT_EXP_SHIFT (2101) /* 2*emax + prec */
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 77352595f1..72585e5014 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -1069,6 +1069,32 @@ module FNativeEntries =
{ mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cFNotComparable) };
| None -> defined_f_cmp := false
+ let defined_f_class = ref false
+ let fPNormal = ref dummy
+ let fNNormal = ref dummy
+ let fPSubn = ref dummy
+ let fNSubn = ref dummy
+ let fPZero = ref dummy
+ let fNZero = ref dummy
+ let fPInf = ref dummy
+ let fNInf = ref dummy
+ let fNaN = ref dummy
+
+ let init_f_class retro =
+ match retro.Retroknowledge.retro_f_class with
+ | Some (cPNormal, cNNormal, cPSubn, cNSubn, cPZero, cNZero,
+ cPInf, cNInf, cNaN) ->
+ defined_f_class := true;
+ fPNormal := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cPNormal) };
+ fNNormal := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cNNormal) };
+ fPSubn := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cPSubn) };
+ fNSubn := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cNSubn) };
+ fPZero := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cPZero) };
+ fNZero := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cNZero) };
+ fPInf := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cPInf) };
+ fNInf := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cNInf) };
+ fNaN := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cNaN) };
+ | None -> defined_f_class := false
let defined_refl = ref false
let frefl = ref dummy
@@ -1089,6 +1115,7 @@ module FNativeEntries =
init_pair !current_retro;
init_cmp !current_retro;
init_f_cmp !current_retro;
+ init_f_class !current_retro;
init_refl !current_retro
let check_env env =
@@ -1122,6 +1149,10 @@ module FNativeEntries =
check_env env;
assert (!defined_f_cmp)
+ let check_f_class env =
+ check_env env;
+ assert (!defined_f_class)
+
let mkInt env i =
check_int env;
{ mark = mark Cstr KnownR; term = FInt i }
@@ -1175,6 +1206,42 @@ module FNativeEntries =
let mkFNotComparable env =
check_f_cmp env;
!fFNotComparable
+
+ let mkPNormal env =
+ check_f_class env;
+ !fPNormal
+
+ let mkNNormal env =
+ check_f_class env;
+ !fNNormal
+
+ let mkPSubn env =
+ check_f_class env;
+ !fPSubn
+
+ let mkNSubn env =
+ check_f_class env;
+ !fNSubn
+
+ let mkPZero env =
+ check_f_class env;
+ !fPZero
+
+ let mkNZero env =
+ check_f_class env;
+ !fNZero
+
+ let mkPInf env =
+ check_f_class env;
+ !fPInf
+
+ let mkNInf env =
+ check_f_class env;
+ !fNInf
+
+ let mkNaN env =
+ check_f_class env;
+ !fNaN
end
module FredNative = RedNative(FNativeEntries)
diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml
index d5ed2c1a06..02a5351ccf 100644
--- a/kernel/cPrimitives.ml
+++ b/kernel/cPrimitives.ml
@@ -36,6 +36,7 @@ type t =
| Float64opp
| Float64abs
| Float64compare
+ | Float64classify
| Float64add
| Float64sub
| Float64mul
@@ -77,15 +78,16 @@ let hash = function
| Float64opp -> 25
| Float64abs -> 26
| Float64compare -> 27
- | Float64add -> 28
- | Float64sub -> 29
- | Float64mul -> 30
- | Float64div -> 31
- | Float64sqrt -> 32
- | Float64ofInt63 -> 33
- | Float64normfr_mantissa -> 34
- | Float64frshiftexp -> 35
- | Float64ldshiftexp -> 36
+ | Float64classify -> 28
+ | Float64add -> 29
+ | Float64sub -> 30
+ | Float64mul -> 31
+ | Float64div -> 32
+ | Float64sqrt -> 33
+ | Float64ofInt63 -> 34
+ | Float64normfr_mantissa -> 35
+ | Float64frshiftexp -> 36
+ | Float64ldshiftexp -> 37
(* Should match names in nativevalues.ml *)
let to_string = function
@@ -116,6 +118,7 @@ let to_string = function
| Float64opp -> "fopp"
| Float64abs -> "fabs"
| Float64compare -> "fcompare"
+ | Float64classify -> "fclassify"
| Float64add -> "fadd"
| Float64sub -> "fsub"
| Float64mul -> "fmul"
@@ -136,6 +139,7 @@ type 'a prim_ind =
| PIT_pair : (prim_type * prim_type) prim_ind
| PIT_cmp : unit prim_ind
| PIT_f_cmp : unit prim_ind
+ | PIT_f_class : unit prim_ind
type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex
@@ -166,6 +170,7 @@ let types =
| Float64normfr_mantissa -> [float_ty; int_ty]
| Float64frshiftexp -> [float_ty; PITT_ind (PIT_pair, (PT_float64, PT_int63))]
| Float64compare -> [float_ty; float_ty; PITT_ind (PIT_f_cmp, ())]
+ | Float64classify -> [float_ty; PITT_ind (PIT_f_class, ())]
| Float64add | Float64sub | Float64mul
| Float64div -> [float_ty; float_ty; float_ty]
| Float64ldshiftexp -> [float_ty; int_ty; float_ty]
@@ -198,6 +203,7 @@ let prim_ind_to_string (type a) (p : a prim_ind) = match p with
| PIT_pair -> "pair"
| PIT_cmp -> "cmp"
| PIT_f_cmp -> "f_cmp"
+ | PIT_f_class -> "f_class"
let prim_type_to_string = function
| PT_int63 -> "int63_type"
diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli
index 3e6ec8dbcc..af95f6c6d7 100644
--- a/kernel/cPrimitives.mli
+++ b/kernel/cPrimitives.mli
@@ -36,6 +36,7 @@ type t =
| Float64opp
| Float64abs
| Float64compare
+ | Float64classify
| Float64add
| Float64sub
| Float64mul
@@ -75,6 +76,7 @@ type 'a prim_ind =
| PIT_pair : (prim_type * prim_type) prim_ind
| PIT_cmp : unit prim_ind
| PIT_f_cmp : unit prim_ind
+ | PIT_f_class : unit prim_ind
type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 82dd7bd85d..535034d8fa 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -237,6 +237,7 @@ let check_prim_op = function
| Float64opp -> opCHECKOPPFLOAT
| Float64abs -> opCHECKABSFLOAT
| Float64compare -> opCHECKCOMPAREFLOAT
+ | Float64classify -> opCHECKCLASSIFYFLOAT
| Float64add -> opCHECKADDFLOAT
| Float64sub -> opCHECKSUBFLOAT
| Float64mul -> opCHECKMULFLOAT
diff --git a/kernel/float64.ml b/kernel/float64.ml
index eebc8f35ef..7b54fd0c4b 100644
--- a/kernel/float64.ml
+++ b/kernel/float64.ml
@@ -38,6 +38,17 @@ let compare x y =
)
)
+type float_class =
+ | PNormal | NNormal | PSubn | NSubn | PZero | NZero | PInf | NInf | NaN
+
+let classify x =
+ match classify_float x with
+ | FP_normal -> if 0. < x then PNormal else NNormal
+ | FP_subnormal -> if 0. < x then PSubn else NSubn
+ | FP_zero -> if 0. < 1. /. x then PZero else NZero
+ | FP_infinite -> if 0. < x then PInf else NInf
+ | FP_nan -> NaN
+
let mul = ( *. )
let add = ( +. )
let sub = ( -. )
diff --git a/kernel/float64.mli b/kernel/float64.mli
index c82f1d84da..1ad980a691 100644
--- a/kernel/float64.mli
+++ b/kernel/float64.mli
@@ -30,6 +30,11 @@ type float_comparison = FEq | FLt | FGt | FNotComparable
* NotComparable is returned if there is a NaN in the arguments *)
val compare : t -> t -> float_comparison
+type float_class =
+ | PNormal | NNormal | PSubn | NSubn | PZero | NZero | PInf | NInf | NaN
+
+val classify : t -> float_class
+
val mul : t -> t -> t
val add : t -> t -> t
val sub : t -> t -> t
diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml
index 7deffd030b..045a1e361d 100644
--- a/kernel/genOpcodeFiles.ml
+++ b/kernel/genOpcodeFiles.ml
@@ -140,6 +140,7 @@ let opcodes =
"CHECKOPPFLOAT";
"CHECKABSFLOAT";
"CHECKCOMPAREFLOAT";
+ "CHECKCLASSIFYFLOAT";
"CHECKADDFLOAT";
"CHECKSUBFLOAT";
"CHECKMULFLOAT";
diff --git a/kernel/primred.ml b/kernel/primred.ml
index 5fe700cb9a..cfe6c8effe 100644
--- a/kernel/primred.ml
+++ b/kernel/primred.ml
@@ -55,6 +55,15 @@ let add_retroknowledge env action =
| None -> ((ind,1), (ind,2), (ind,3), (ind,4))
| Some (((ind',_),_,_,_) as t) -> assert (eq_ind ind ind'); t in
{ retro with retro_f_cmp = Some r }
+ | PIT_f_class ->
+ let r =
+ match retro.retro_f_class with
+ | None -> ((ind,1), (ind,2), (ind,3), (ind,4),
+ (ind,5), (ind,6), (ind,7), (ind,8),
+ (ind,9))
+ | Some (((ind',_),_,_,_,_,_,_,_,_) as t) ->
+ assert (eq_ind ind ind'); t in
+ { retro with retro_f_class = Some r }
in
set_retroknowledge env retro
@@ -99,6 +108,11 @@ let get_f_cmp_constructors env =
| Some r -> r
| None -> anomaly Pp.(str"Reduction of primitive: fcmp not registered")
+let get_f_class_constructors env =
+ match env.retroknowledge.retro_f_class with
+ | Some r -> r
+ | None -> anomaly Pp.(str"Reduction of primitive: fclass not registered")
+
exception NativeDestKO
module type RedNativeEntries =
@@ -123,6 +137,15 @@ module type RedNativeEntries =
val mkFEq : env -> elem
val mkFGt : env -> elem
val mkFNotComparable : env -> elem
+ val mkPNormal : env -> elem
+ val mkNNormal : env -> elem
+ val mkPSubn : env -> elem
+ val mkNSubn : env -> elem
+ val mkPZero : env -> elem
+ val mkNZero : env -> elem
+ val mkPInf : env -> elem
+ val mkNInf : env -> elem
+ val mkNaN : env -> elem
end
module type RedNative =
@@ -245,6 +268,18 @@ struct
| Float64.FLt -> E.mkFLt env
| Float64.FGt -> E.mkFGt env
| Float64.FNotComparable -> E.mkFNotComparable env)
+ | Float64classify ->
+ let f = get_float1 evd args in
+ (match Float64.classify f with
+ | Float64.PNormal -> E.mkPNormal env
+ | Float64.NNormal -> E.mkNNormal env
+ | Float64.PSubn -> E.mkPSubn env
+ | Float64.NSubn -> E.mkNSubn env
+ | Float64.PZero -> E.mkPZero env
+ | Float64.NZero -> E.mkNZero env
+ | Float64.PInf -> E.mkPInf env
+ | Float64.NInf -> E.mkNInf env
+ | Float64.NaN -> E.mkNaN env)
| Float64add ->
let f1, f2 = get_float2 evd args in E.mkFloat env (Float64.add f1 f2)
| Float64sub ->
diff --git a/kernel/primred.mli b/kernel/primred.mli
index 5531c81550..bbe564d8e7 100644
--- a/kernel/primred.mli
+++ b/kernel/primred.mli
@@ -12,6 +12,10 @@ val get_carry_constructors : env -> constructor * constructor
val get_pair_constructor : env -> constructor
val get_cmp_constructors : env -> constructor * constructor * constructor
val get_f_cmp_constructors : env -> constructor * constructor * constructor * constructor
+val get_f_class_constructors :
+ env -> constructor * constructor * constructor * constructor
+ * constructor * constructor * constructor * constructor
+ * constructor
exception NativeDestKO (* Should be raised by get_* functions on failure *)
@@ -37,6 +41,15 @@ module type RedNativeEntries =
val mkFEq : env -> elem
val mkFGt : env -> elem
val mkFNotComparable : env -> elem
+ val mkPNormal : env -> elem
+ val mkNNormal : env -> elem
+ val mkPSubn : env -> elem
+ val mkNSubn : env -> elem
+ val mkPZero : env -> elem
+ val mkNZero : env -> elem
+ val mkPInf : env -> elem
+ val mkNInf : env -> elem
+ val mkNaN : env -> elem
end
module type RedNative =
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index e897be6141..479fe02295 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -27,7 +27,14 @@ type retroknowledge = {
retro_f_cmp : (constructor * constructor * constructor * constructor)
option;
(* FEq, FLt, FGt, FNotComparable *)
- retro_refl : constructor option;
+ retro_f_class : (constructor * constructor * constructor * constructor
+ * constructor * constructor * constructor * constructor
+ * constructor)
+ option;
+ (* PNormal, NNormal, PSubn, NSubn,
+ PZero, NZero, PInf, NInf,
+ NaN *)
+ retro_refl : constructor option
}
let empty = {
@@ -38,6 +45,7 @@ let empty = {
retro_pair = None;
retro_cmp = None;
retro_f_cmp = None;
+ retro_f_class = None;
retro_refl = None;
}
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index 7aaf14e176..2df8a00465 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -21,7 +21,14 @@ type retroknowledge = {
retro_f_cmp : (constructor * constructor * constructor * constructor)
option;
(* FEq, FLt, FGt, FNotComparable *)
- retro_refl : constructor option;
+ retro_f_class : (constructor * constructor * constructor * constructor
+ * constructor * constructor * constructor * constructor
+ * constructor)
+ option;
+ (* PNormal, NNormal, PSubn, NSubn,
+ PZero, NZero, PInf, NInf,
+ NaN *)
+ retro_refl : constructor option
}
val empty : retroknowledge
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 241ee8ada3..d3cffd1546 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -1413,6 +1413,26 @@ let check_register_ind (type t) ind (r : t CPrimitives.prim_ind) env =
check_type_cte 2;
check_name 3 "FNotComparable";
check_type_cte 3
+ | CPrimitives.PIT_f_class ->
+ check_nconstr 9;
+ check_name 0 "PNormal";
+ check_type_cte 0;
+ check_name 1 "NNormal";
+ check_type_cte 1;
+ check_name 2 "PSubn";
+ check_type_cte 2;
+ check_name 3 "NSubn";
+ check_type_cte 3;
+ check_name 4 "PZero";
+ check_type_cte 4;
+ check_name 5 "NZero";
+ check_type_cte 5;
+ check_name 6 "PInf";
+ check_type_cte 6;
+ check_name 7 "NInf";
+ check_type_cte 7;
+ check_name 8 "NaN";
+ check_type_cte 8
let register_inductive ind prim senv =
check_register_ind ind prim senv.env;
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 3e79b174b8..1cc40a6707 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -246,6 +246,11 @@ let type_of_prim env t =
| Some ((ind,_),_,_,_) -> Constr.mkInd ind
| None -> CErrors.user_err Pp.(str"The type float_comparison must be registered before this primitive.")
in
+ let f_class_ty () =
+ match env.retroknowledge.Retroknowledge.retro_f_class with
+ | Some ((ind,_),_,_,_,_,_,_,_,_) -> Constr.mkInd ind
+ | None -> CErrors.user_err Pp.(str"The type float_class must be registered before this primitive.")
+ in
let pair_ty fst_ty snd_ty =
match env.retroknowledge.Retroknowledge.retro_pair with
| Some (ind,_) -> Constr.mkApp(Constr.mkInd ind, [|fst_ty;snd_ty|])
@@ -265,7 +270,8 @@ let type_of_prim env t =
| PIT_carry, t -> carry_ty (tr_prim_type t)
| PIT_pair, (t1, t2) -> pair_ty (tr_prim_type t1) (tr_prim_type t2)
| PIT_cmp, () -> compare_ty ()
- | PIT_f_cmp, () -> f_compare_ty () in
+ | PIT_f_cmp, () -> f_compare_ty ()
+ | PIT_f_class, () -> f_class_ty () in
let tr_type = function
| PITT_ind (i, a) -> tr_ind i a
| PITT_type t -> tr_prim_type t in
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index bac13a0bd7..c78f791a5a 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -228,7 +228,6 @@ module VNativeEntries =
| _ -> raise Primred.NativeDestKO)
| _ -> raise Primred.NativeDestKO
-
let mkInt env i = VAL(0, mkInt i)
let mkFloat env f = VAL(0, mkFloat f)
@@ -283,6 +282,51 @@ module VNativeEntries =
let mkFNotComparable env =
let (_eq,_lt,_gt,nc) = get_f_cmp_constructors env in
CONSTR(Univ.in_punivs nc, [||])
+
+ let mkPNormal env =
+ let (pNormal,_nNormal,_pSubn,_nSubn,_pZero,_nZero,_pInf,_nInf,_nan) =
+ get_f_class_constructors env in
+ CONSTR(Univ.in_punivs pNormal, [||])
+
+ let mkNNormal env =
+ let (_pNormal,nNormal,_pSubn,_nSubn,_pZero,_nZero,_pInf,_nInf,_nan) =
+ get_f_class_constructors env in
+ CONSTR(Univ.in_punivs nNormal, [||])
+
+ let mkPSubn env =
+ let (_pNormal,_nNormal,pSubn,_nSubn,_pZero,_nZero,_pInf,_nInf,_nan) =
+ get_f_class_constructors env in
+ CONSTR(Univ.in_punivs pSubn, [||])
+
+ let mkNSubn env =
+ let (_pNormal,_nNormal,_pSubn,nSubn,_pZero,_nZero,_pInf,_nInf,_nan) =
+ get_f_class_constructors env in
+ CONSTR(Univ.in_punivs nSubn, [||])
+
+ let mkPZero env =
+ let (_pNormal,_nNormal,_pSubn,_nSubn,pZero,_nZero,_pInf,_nInf,_nan) =
+ get_f_class_constructors env in
+ CONSTR(Univ.in_punivs pZero, [||])
+
+ let mkNZero env =
+ let (_pNormal,_nNormal,_pSubn,_nSubn,_pZero,nZero,_pInf,_nInf,_nan) =
+ get_f_class_constructors env in
+ CONSTR(Univ.in_punivs nZero, [||])
+
+ let mkPInf env =
+ let (_pNormal,_nNormal,_pSubn,_nSubn,_pZero,_nZero,pInf,_nInf,_nan) =
+ get_f_class_constructors env in
+ CONSTR(Univ.in_punivs pInf, [||])
+
+ let mkNInf env =
+ let (_pNormal,_nNormal,_pSubn,_nSubn,_pZero,_nZero,_pInf,nInf,_nan) =
+ get_f_class_constructors env in
+ CONSTR(Univ.in_punivs nInf, [||])
+
+ let mkNaN env =
+ let (_pNormal,_nNormal,_pSubn,_nSubn,_pZero,_nZero,_pInf,_nInf,nan) =
+ get_f_class_constructors env in
+ CONSTR(Univ.in_punivs nan, [||])
end
module VredNative = RedNative(VNativeEntries)
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 321c64e411..2952466fbb 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -906,6 +906,51 @@ struct
let mkFNotComparable env =
let (_eq, _lt, _gt, nc) = get_f_cmp_constructors env in
mkConstruct nc
+
+ let mkPNormal env =
+ let (pNormal,_nNormal,_pSubn,_nSubn,_pZero,_nZero,_pInf,_nInf,_nan) =
+ get_f_class_constructors env in
+ mkConstruct pNormal
+
+ let mkNNormal env =
+ let (_pNormal,nNormal,_pSubn,_nSubn,_pZero,_nZero,_pInf,_nInf,_nan) =
+ get_f_class_constructors env in
+ mkConstruct nNormal
+
+ let mkPSubn env =
+ let (_pNormal,_nNormal,pSubn,_nSubn,_pZero,_nZero,_pInf,_nInf,_nan) =
+ get_f_class_constructors env in
+ mkConstruct pSubn
+
+ let mkNSubn env =
+ let (_pNormal,_nNormal,_pSubn,nSubn,_pZero,_nZero,_pInf,_nInf,_nan) =
+ get_f_class_constructors env in
+ mkConstruct nSubn
+
+ let mkPZero env =
+ let (_pNormal,_nNormal,_pSubn,_nSubn,pZero,_nZero,_pInf,_nInf,_nan) =
+ get_f_class_constructors env in
+ mkConstruct pZero
+
+ let mkNZero env =
+ let (_pNormal,_nNormal,_pSubn,_nSubn,_pZero,nZero,_pInf,_nInf,_nan) =
+ get_f_class_constructors env in
+ mkConstruct nZero
+
+ let mkPInf env =
+ let (_pNormal,_nNormal,_pSubn,_nSubn,_pZero,_nZero,pInf,_nInf,_nan) =
+ get_f_class_constructors env in
+ mkConstruct pInf
+
+ let mkNInf env =
+ let (_pNormal,_nNormal,_pSubn,_nSubn,_pZero,_nZero,_pInf,nInf,_nan) =
+ get_f_class_constructors env in
+ mkConstruct nInf
+
+ let mkNaN env =
+ let (_pNormal,_nNormal,_pSubn,_nSubn,_pZero,_nZero,_pInf,_nInf,nan) =
+ get_f_class_constructors env in
+ mkConstruct nan
end
module CredNative = RedNative(CNativeEntries)
diff --git a/test-suite/primitive/float/classify.v b/test-suite/primitive/float/classify.v
new file mode 100644
index 0000000000..e4373415cb
--- /dev/null
+++ b/test-suite/primitive/float/classify.v
@@ -0,0 +1,23 @@
+Require Import ZArith Floats.
+
+Definition epsilon := Eval compute in ldexp one (-1024)%Z.
+
+Check (eq_refl : classify one = PNormal).
+Check (eq_refl : classify (- one)%float = NNormal).
+Check (eq_refl : classify epsilon = PSubn).
+Check (eq_refl : classify (- epsilon)%float = NSubn).
+Check (eq_refl : classify zero = PZero).
+Check (eq_refl : classify neg_zero = NZero).
+Check (eq_refl : classify infinity = PInf).
+Check (eq_refl : classify neg_infinity = NInf).
+Check (eq_refl : classify nan = NaN).
+
+Check (eq_refl PNormal <: classify one = PNormal).
+Check (eq_refl NNormal <: classify (- one)%float = NNormal).
+Check (eq_refl PSubn <: classify epsilon = PSubn).
+Check (eq_refl NSubn <: classify (- epsilon)%float = NSubn).
+Check (eq_refl PZero <: classify zero = PZero).
+Check (eq_refl NZero <: classify neg_zero = NZero).
+Check (eq_refl PInf <: classify infinity = PInf).
+Check (eq_refl NInf <: classify neg_infinity = NInf).
+Check (eq_refl NaN <: classify nan = NaN).
diff --git a/theories/Floats/FloatAxioms.v b/theories/Floats/FloatAxioms.v
index d835e87ee0..d78e3192e7 100644
--- a/theories/Floats/FloatAxioms.v
+++ b/theories/Floats/FloatAxioms.v
@@ -2,6 +2,7 @@ Require Import ZArith Int63 SpecFloat PrimFloat FloatOps.
Notation valid_binary := (valid_binary prec emax).
+Definition SF64classify := SFclassify prec.
Definition SF64mul := SFmul prec emax.
Definition SF64add := SFadd prec emax.
Definition SF64sub := SFsub prec emax.
@@ -32,6 +33,7 @@ Definition flatten_cmp_opt c :=
end.
Axiom compare_spec : forall x y, (x ?= y)%float = flatten_cmp_opt (SFcompare (Prim2SF x) (Prim2SF y)).
+Axiom classify_spec : forall x, classify x = SF64classify (Prim2SF x).
Axiom mul_spec : forall x y, Prim2SF (x * y)%float = SF64mul (Prim2SF x) (Prim2SF y).
Axiom add_spec : forall x y, Prim2SF (x + y)%float = SF64add (Prim2SF x) (Prim2SF y).
Axiom sub_spec : forall x y, Prim2SF (x - y)%float = SF64sub (Prim2SF x) (Prim2SF y).
diff --git a/theories/Floats/FloatClass.v b/theories/Floats/FloatClass.v
new file mode 100644
index 0000000000..3241035aef
--- /dev/null
+++ b/theories/Floats/FloatClass.v
@@ -0,0 +1,2 @@
+Inductive float_class : Set :=
+ | PNormal | NNormal | PSubn | NSubn | PZero | NZero | PInf | NInf | NaN.
diff --git a/theories/Floats/Floats.v b/theories/Floats/Floats.v
index a1d49e87ee..53dd73f6d0 100644
--- a/theories/Floats/Floats.v
+++ b/theories/Floats/Floats.v
@@ -1,3 +1,4 @@
+Require Export FloatClass.
Require Export SpecFloat.
Require Export PrimFloat.
Require Export FloatOps.
diff --git a/theories/Floats/PrimFloat.v b/theories/Floats/PrimFloat.v
index 13763a39d1..bc5c49d085 100644
--- a/theories/Floats/PrimFloat.v
+++ b/theories/Floats/PrimFloat.v
@@ -1,8 +1,9 @@
-Require Import Int63.
+Require Import Int63 FloatClass.
Inductive float_comparison : Set := FEq | FLt | FGt | FNotComparable.
Register float_comparison as kernel.ind_f_cmp.
+Register float_class as kernel.ind_f_class.
Primitive float := #float64_type.
@@ -18,6 +19,8 @@ Primitive abs := #float64_abs.
Primitive compare := #float64_compare.
Notation "x ?= y" := (compare x y) (at level 70, no associativity) : float_scope.
+Primitive classify := #float64_classify.
+
Primitive mul := #float64_mul.
Notation "x * y" := (mul x y) : float_scope.
diff --git a/theories/Floats/SpecFloat.v b/theories/Floats/SpecFloat.v
index 337c00b20f..fc26ba8cab 100644
--- a/theories/Floats/SpecFloat.v
+++ b/theories/Floats/SpecFloat.v
@@ -1,4 +1,4 @@
-Require Import ZArith.
+Require Import ZArith FloatClass.
Variant spec_float :=
| S754_zero (s : bool)
@@ -183,6 +183,21 @@ Section FloatOps.
end
end.
+ Definition SFclassify f :=
+ match f with
+ | S754_nan => NaN
+ | S754_infinity false => PInf
+ | S754_infinity true => NInf
+ | S754_zero false => NZero
+ | S754_zero true => PZero
+ | S754_finite false m _ =>
+ if (digits2_pos m =? Z.to_pos prec)%positive then PNormal
+ else PSubn
+ | S754_finite true m _ =>
+ if (digits2_pos m =? Z.to_pos prec)%positive then NNormal
+ else NSubn
+ end.
+
Definition SFmul x y :=
match x, y with
| S754_nan, _ | _, S754_nan => S754_nan
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 78e4c89521..aeae86e1f7 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -276,6 +276,7 @@ GRAMMAR EXTEND Gram
| "#float64_opp" -> { CPrimitives.Float64opp }
| "#float64_abs" -> { CPrimitives.Float64abs }
| "#float64_compare" -> { CPrimitives.Float64compare }
+ | "#float64_classify" -> { CPrimitives.Float64classify }
| "#float64_add" -> { CPrimitives.Float64add }
| "#float64_sub" -> { CPrimitives.Float64sub }
| "#float64_mul" -> { CPrimitives.Float64mul }
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index c86b70c78e..c4892736ae 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1848,6 +1848,7 @@ let vernac_register qid r =
| "ind_pair" -> CPrimitives.(PIE PIT_pair)
| "ind_cmp" -> CPrimitives.(PIE PIT_cmp)
| "ind_f_cmp" -> CPrimitives.(PIE PIT_f_cmp)
+ | "ind_f_class" -> CPrimitives.(PIE PIT_f_class)
| k -> CErrors.user_err Pp.(str "Register: unknown identifier “" ++ str k ++ str "” in the “kernel” namespace")
in
match gr with
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:54:05 +0000