aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/byterun/coq_fix_code.c2
-rw-r--r--kernel/byterun/coq_float64.h12
-rw-r--r--kernel/byterun/coq_interp.c27
-rw-r--r--kernel/cPrimitives.ml10
-rw-r--r--kernel/cPrimitives.mli3
-rw-r--r--kernel/cemitcodes.ml3
-rw-r--r--kernel/float64.ml9
-rw-r--r--kernel/float64.mli6
-rw-r--r--kernel/genOpcodeFiles.ml5
-rw-r--r--kernel/nativevalues.ml21
-rw-r--r--kernel/nativevalues.mli12
-rw-r--r--kernel/primred.ml9
12 files changed, 119 insertions, 0 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 3fe77afc2d..931b509f48 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -44,6 +44,7 @@ void init_arity () {
arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]=
arity[ACCUMULATE]=arity[STOP]=arity[MAKEPROD]=
arity[ADDINT63]=arity[SUBINT63]=arity[LTINT63]=arity[LEINT63]=
+ arity[LTFLOAT]=arity[LEFLOAT]=
arity[ISINT]=arity[AREINT2]=0;
/* instruction with one operand */
arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]=
@@ -64,6 +65,7 @@ void init_arity () {
arity[CHECKLSLINT63CONST1]=arity[CHECKLSRINT63CONST1]=
arity[CHECKEQINT63]=arity[CHECKLTINT63]=arity[CHECKLEINT63]=
arity[CHECKCOMPAREINT63]=arity[CHECKHEAD0INT63]=arity[CHECKTAIL0INT63]=
+ arity[CHECKEQFLOAT]=arity[CHECKLTFLOAT]=arity[CHECKLEFLOAT]=
arity[CHECKOPPFLOAT]=arity[CHECKABSFLOAT]=arity[CHECKCOMPAREFLOAT]=
arity[CHECKCLASSIFYFLOAT]=
arity[CHECKADDFLOAT]=arity[CHECKSUBFLOAT]=arity[CHECKMULFLOAT]=
diff --git a/kernel/byterun/coq_float64.h b/kernel/byterun/coq_float64.h
index 9fc390bd33..c41079c8ff 100644
--- a/kernel/byterun/coq_float64.h
+++ b/kernel/byterun/coq_float64.h
@@ -3,6 +3,15 @@
#include <math.h>
+#define DECLARE_FREL(name, e) \
+ int coq_##name(double x, double y) { \
+ return e; \
+ } \
+ \
+ value coq_##name##_byte(value x, value y) { \
+ return coq_##name(Double_val(x), Double_val(y)); \
+ }
+
#define DECLARE_FBINOP(name, e) \
double coq_##name(double x, double y) { \
return e; \
@@ -21,6 +30,9 @@
return caml_copy_double(coq_##name(Double_val(x))); \
}
+DECLARE_FREL(feq, x == y)
+DECLARE_FREL(flt, x < y)
+DECLARE_FREL(fle, x <= y)
DECLARE_FBINOP(fmul, x * y)
DECLARE_FBINOP(fadd, x + y)
DECLARE_FBINOP(fsub, x - y)
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 6e6adb1293..c21aeecb16 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -1545,6 +1545,33 @@ value coq_interprete
Next;
}
+ Instruct (CHECKEQFLOAT) {
+ print_instr("CHECKEQFLOAT");
+ CheckFloat2();
+ accu = coq_feq(Double_val(accu), Double_val(*sp++)) ? coq_true : coq_false;
+ Next;
+ }
+
+ Instruct (CHECKLTFLOAT) {
+ print_instr("CHECKLTFLOAT");
+ CheckFloat2();
+ }
+ Instruct (LTFLOAT) {
+ print_instr("LTFLOAT");
+ accu = coq_flt(Double_val(accu), Double_val(*sp++)) ? coq_true : coq_false;
+ Next;
+ }
+
+ Instruct (CHECKLEFLOAT) {
+ print_instr("CHECKLEFLOAT");
+ CheckFloat2();
+ }
+ Instruct (LEFLOAT) {
+ print_instr("LEFLOAT");
+ accu = coq_fle(Double_val(accu), Double_val(*sp++)) ? coq_true : coq_false;
+ Next;
+ }
+
Instruct (CHECKCOMPAREFLOAT) {
double x, y;
print_instr("CHECKCOMPAREFLOAT");
diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml
index 342cc29a22..9ff7f69203 100644
--- a/kernel/cPrimitives.ml
+++ b/kernel/cPrimitives.ml
@@ -35,6 +35,9 @@ type t =
| Int63compare
| Float64opp
| Float64abs
+ | Float64eq
+ | Float64lt
+ | Float64le
| Float64compare
| Float64classify
| Float64add
@@ -92,6 +95,9 @@ let hash = function
| Float64ldshiftexp -> 37
| Float64next_up -> 38
| Float64next_down -> 39
+ | Float64eq -> 40
+ | Float64lt -> 41
+ | Float64le -> 42
(* Should match names in nativevalues.ml *)
let to_string = function
@@ -121,6 +127,9 @@ let to_string = function
| Int63compare -> "compare"
| Float64opp -> "fopp"
| Float64abs -> "fabs"
+ | Float64eq -> "feq"
+ | Float64lt -> "flt"
+ | Float64le -> "fle"
| Float64compare -> "fcompare"
| Float64classify -> "fclassify"
| Float64add -> "fadd"
@@ -176,6 +185,7 @@ let types =
| Float64ofInt63 -> [int_ty; float_ty]
| Float64normfr_mantissa -> [float_ty; int_ty]
| Float64frshiftexp -> [float_ty; PITT_ind (PIT_pair, (PT_float64, PT_int63))]
+ | Float64eq | Float64lt | Float64le -> [float_ty; float_ty; PITT_ind (PIT_bool, ())]
| Float64compare -> [float_ty; float_ty; PITT_ind (PIT_f_cmp, ())]
| Float64classify -> [float_ty; PITT_ind (PIT_f_class, ())]
| Float64add | Float64sub | Float64mul
diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli
index 3cb210233d..be65ba5305 100644
--- a/kernel/cPrimitives.mli
+++ b/kernel/cPrimitives.mli
@@ -35,6 +35,9 @@ type t =
| Int63compare
| Float64opp
| Float64abs
+ | Float64eq
+ | Float64lt
+ | Float64le
| Float64compare
| Float64classify
| Float64add
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 908f84293c..5e82cef810 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -236,6 +236,9 @@ let check_prim_op = function
| Int63compare -> opCHECKCOMPAREINT63
| Float64opp -> opCHECKOPPFLOAT
| Float64abs -> opCHECKABSFLOAT
+ | Float64eq -> opCHECKEQFLOAT
+ | Float64lt -> opCHECKLTFLOAT
+ | Float64le -> opCHECKLEFLOAT
| Float64compare -> opCHECKCOMPAREFLOAT
| Float64classify -> opCHECKCLASSIFYFLOAT
| Float64add -> opCHECKADDFLOAT
diff --git a/kernel/float64.ml b/kernel/float64.ml
index 55ad472ea9..86b14c5cd2 100644
--- a/kernel/float64.ml
+++ b/kernel/float64.ml
@@ -42,6 +42,15 @@ let abs = abs_float
type float_comparison = FEq | FLt | FGt | FNotComparable
+let eq x y = x = y
+[@@ocaml.inline always]
+
+let lt x y = x < y
+[@@ocaml.inline always]
+
+let le x y = x <= y
+[@@ocaml.inline always]
+
(* inspired by lib/util.ml; see also #10471 *)
let pervasives_compare = compare
diff --git a/kernel/float64.mli b/kernel/float64.mli
index 78dc1a7bd7..2aa9796526 100644
--- a/kernel/float64.mli
+++ b/kernel/float64.mli
@@ -34,6 +34,12 @@ val abs : t -> t
type float_comparison = FEq | FLt | FGt | FNotComparable
+val eq : t -> t -> bool
+
+val lt : t -> t -> bool
+
+val le : t -> t -> bool
+
(** The IEEE 754 float comparison.
* NotComparable is returned if there is a NaN in the arguments *)
val compare : t -> t -> float_comparison
diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml
index 52b7a822e3..82bb2b584d 100644
--- a/kernel/genOpcodeFiles.ml
+++ b/kernel/genOpcodeFiles.ml
@@ -139,6 +139,11 @@ let opcodes =
"AREINT2";
"CHECKOPPFLOAT";
"CHECKABSFLOAT";
+ "CHECKEQFLOAT";
+ "CHECKLTFLOAT";
+ "LTFLOAT";
+ "CHECKLEFLOAT";
+ "LEFLOAT";
"CHECKCOMPAREFLOAT";
"CHECKCLASSIFYFLOAT";
"CHECKADDFLOAT";
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 6b9d49052d..e4a8344eaf 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -539,6 +539,27 @@ let fabs accu x =
if is_float x then no_check_fabs x
else accu x
+let no_check_feq x y =
+ mk_bool (Float64.eq (to_float x) (to_float y))
+
+let feq accu x y =
+ if is_float x && is_float y then no_check_feq x y
+ else accu x y
+
+let no_check_flt x y =
+ mk_bool (Float64.lt (to_float x) (to_float y))
+
+let flt accu x y =
+ if is_float x && is_float y then no_check_flt x y
+ else accu x y
+
+let no_check_fle x y =
+ mk_bool (Float64.le (to_float x) (to_float y))
+
+let fle accu x y =
+ if is_float x && is_float y then no_check_fle x y
+ else accu x y
+
type coq_fcmp =
| CFcmpAccu of t
| CFcmpEq
diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli
index d19877c121..815ef3e98e 100644
--- a/kernel/nativevalues.mli
+++ b/kernel/nativevalues.mli
@@ -261,6 +261,9 @@ val is_float : t -> bool
val fopp : t -> t -> t
val fabs : t -> t -> t
+val feq : t -> t -> t -> t
+val flt : t -> t -> t -> t
+val fle : t -> t -> t -> t
val fcompare : t -> t -> t -> t
val fclassify : t -> t -> t
val fadd : t -> t -> t -> t
@@ -282,6 +285,15 @@ val no_check_fopp : t -> t
val no_check_fabs : t -> t
[@@ocaml.inline always]
+val no_check_feq : t -> t -> t
+[@@ocaml.inline always]
+
+val no_check_flt : t -> t -> t
+[@@ocaml.inline always]
+
+val no_check_fle : t -> t -> t
+[@@ocaml.inline always]
+
val no_check_fcompare : t -> t -> t
[@@ocaml.inline always]
diff --git a/kernel/primred.ml b/kernel/primred.ml
index 2766793005..c475828cb3 100644
--- a/kernel/primred.ml
+++ b/kernel/primred.ml
@@ -261,6 +261,15 @@ struct
let f = get_float1 evd args in E.mkFloat env (Float64.opp f)
| Float64abs ->
let f = get_float1 evd args in E.mkFloat env (Float64.abs f)
+ | Float64eq ->
+ let i1, i2 = get_float2 evd args in
+ E.mkBool env (Float64.eq i1 i2)
+ | Float64lt ->
+ let i1, i2 = get_float2 evd args in
+ E.mkBool env (Float64.lt i1 i2)
+ | Float64le ->
+ let i1, i2 = get_float2 evd args in
+ E.mkBool env (Float64.le i1 i2)
| Float64compare ->
let f1, f2 = get_float2 evd args in
(match Float64.compare f1 f2 with
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:22:43 +0000