From f155ba664a782f000e278d97ee5666e2e7d2adea Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Wed, 3 Jul 2019 15:08:44 +0200 Subject: Add "==", "<", "<=" in PrimFloat.v * Add a related test-suite in compare.v (generated by a bash script) Co-authored-by: Pierre Roux --- checker/values.ml | 2 +- kernel/byterun/coq_fix_code.c | 2 + kernel/byterun/coq_float64.h | 12 + kernel/byterun/coq_interp.c | 27 +++ kernel/cPrimitives.ml | 10 + kernel/cPrimitives.mli | 3 + kernel/cemitcodes.ml | 3 + kernel/float64.ml | 9 + kernel/float64.mli | 6 + kernel/genOpcodeFiles.ml | 5 + kernel/nativevalues.ml | 21 ++ kernel/nativevalues.mli | 12 + kernel/primred.ml | 9 + test-suite/primitive/float/compare.v | 385 ++++++++++++++++++++++++++++++ test-suite/primitive/float/gen_compare.sh | 65 +++++ theories/Floats/FloatAxioms.v | 4 + theories/Floats/PrimFloat.v | 46 ++-- theories/Floats/SpecFloat.v | 18 ++ vernac/g_vernac.mlg | 3 + 19 files changed, 613 insertions(+), 29 deletions(-) create mode 100644 test-suite/primitive/float/compare.v create mode 100755 test-suite/primitive/float/gen_compare.sh diff --git a/checker/values.ml b/checker/values.ml index 0cd63566d7..3882f88391 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -228,7 +228,7 @@ let v_pol_arity = v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|] let v_primitive = - v_enum "primitive" 41 (* Number of "Primitive" in Int63.v and PrimFloat.v *) + v_enum "primitive" 44 (* Number of "Primitive" in Int63.v and PrimFloat.v *) let v_cst_def = v_sum "constant_def" 0 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 +#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 diff --git a/test-suite/primitive/float/compare.v b/test-suite/primitive/float/compare.v new file mode 100644 index 0000000000..23d1e5bbae --- /dev/null +++ b/test-suite/primitive/float/compare.v @@ -0,0 +1,385 @@ +(* DO NOT EDIT THIS FILE: automatically generated by ./gen_compare.sh *) +Require Import ZArith Floats. +Local Open Scope float_scope. + +Definition min_denorm := Eval compute in ldexp one (-1074)%Z. + +Definition min_norm := Eval compute in ldexp one (-1024)%Z. + +Check (eq_refl false : nan == nan = false). +Check (eq_refl false : nan == nan = false). +Check (eq_refl false : nan < nan = false). +Check (eq_refl false : nan < nan = false). +Check (eq_refl false : nan <= nan = false). +Check (eq_refl false : nan <= nan = false). +Check (eq_refl FNotComparable : nan ?= nan = FNotComparable). +Check (eq_refl FNotComparable : nan ?= nan = FNotComparable). + +Check (eq_refl false <: nan == nan = false). +Check (eq_refl false <: nan == nan = false). +Check (eq_refl false <: nan < nan = false). +Check (eq_refl false <: nan < nan = false). +Check (eq_refl false <: nan <= nan = false). +Check (eq_refl false <: nan <= nan = false). +Check (eq_refl FNotComparable <: nan ?= nan = FNotComparable). +Check (eq_refl FNotComparable <: nan ?= nan = FNotComparable). + +Check (eq_refl false <<: nan == nan = false). +Check (eq_refl false <<: nan == nan = false). +Check (eq_refl false <<: nan < nan = false). +Check (eq_refl false <<: nan < nan = false). +Check (eq_refl false <<: nan <= nan = false). +Check (eq_refl false <<: nan <= nan = false). +Check (eq_refl FNotComparable <<: nan ?= nan = FNotComparable). +Check (eq_refl FNotComparable <<: nan ?= nan = FNotComparable). + +Check (eq_refl false : nan == - nan = false). +Check (eq_refl false : - nan == nan = false). +Check (eq_refl false : nan < - nan = false). +Check (eq_refl false : - nan < nan = false). +Check (eq_refl false : nan <= - nan = false). +Check (eq_refl false : - nan <= nan = false). +Check (eq_refl FNotComparable : nan ?= - nan = FNotComparable). +Check (eq_refl FNotComparable : - nan ?= nan = FNotComparable). + +Check (eq_refl false <: nan == - nan = false). +Check (eq_refl false <: - nan == nan = false). +Check (eq_refl false <: nan < - nan = false). +Check (eq_refl false <: - nan < nan = false). +Check (eq_refl false <: nan <= - nan = false). +Check (eq_refl false <: - nan <= nan = false). +Check (eq_refl FNotComparable <: nan ?= - nan = FNotComparable). +Check (eq_refl FNotComparable <: - nan ?= nan = FNotComparable). + +Check (eq_refl false <<: nan == - nan = false). +Check (eq_refl false <<: - nan == nan = false). +Check (eq_refl false <<: nan < - nan = false). +Check (eq_refl false <<: - nan < nan = false). +Check (eq_refl false <<: nan <= - nan = false). +Check (eq_refl false <<: - nan <= nan = false). +Check (eq_refl FNotComparable <<: nan ?= - nan = FNotComparable). +Check (eq_refl FNotComparable <<: - nan ?= nan = FNotComparable). + +Check (eq_refl true : one == one = true). +Check (eq_refl true : one == one = true). +Check (eq_refl false : one < one = false). +Check (eq_refl false : one < one = false). +Check (eq_refl true : one <= one = true). +Check (eq_refl true : one <= one = true). +Check (eq_refl FEq : one ?= one = FEq). +Check (eq_refl FEq : one ?= one = FEq). + +Check (eq_refl true <: one == one = true). +Check (eq_refl true <: one == one = true). +Check (eq_refl false <: one < one = false). +Check (eq_refl false <: one < one = false). +Check (eq_refl true <: one <= one = true). +Check (eq_refl true <: one <= one = true). +Check (eq_refl FEq <: one ?= one = FEq). +Check (eq_refl FEq <: one ?= one = FEq). + +Check (eq_refl true <<: one == one = true). +Check (eq_refl true <<: one == one = true). +Check (eq_refl false <<: one < one = false). +Check (eq_refl false <<: one < one = false). +Check (eq_refl true <<: one <= one = true). +Check (eq_refl true <<: one <= one = true). +Check (eq_refl FEq <<: one ?= one = FEq). +Check (eq_refl FEq <<: one ?= one = FEq). + +Check (eq_refl true : zero == zero = true). +Check (eq_refl true : zero == zero = true). +Check (eq_refl false : zero < zero = false). +Check (eq_refl false : zero < zero = false). +Check (eq_refl true : zero <= zero = true). +Check (eq_refl true : zero <= zero = true). +Check (eq_refl FEq : zero ?= zero = FEq). +Check (eq_refl FEq : zero ?= zero = FEq). + +Check (eq_refl true <: zero == zero = true). +Check (eq_refl true <: zero == zero = true). +Check (eq_refl false <: zero < zero = false). +Check (eq_refl false <: zero < zero = false). +Check (eq_refl true <: zero <= zero = true). +Check (eq_refl true <: zero <= zero = true). +Check (eq_refl FEq <: zero ?= zero = FEq). +Check (eq_refl FEq <: zero ?= zero = FEq). + +Check (eq_refl true <<: zero == zero = true). +Check (eq_refl true <<: zero == zero = true). +Check (eq_refl false <<: zero < zero = false). +Check (eq_refl false <<: zero < zero = false). +Check (eq_refl true <<: zero <= zero = true). +Check (eq_refl true <<: zero <= zero = true). +Check (eq_refl FEq <<: zero ?= zero = FEq). +Check (eq_refl FEq <<: zero ?= zero = FEq). + +Check (eq_refl true : zero == - zero = true). +Check (eq_refl true : - zero == zero = true). +Check (eq_refl false : zero < - zero = false). +Check (eq_refl false : - zero < zero = false). +Check (eq_refl true : zero <= - zero = true). +Check (eq_refl true : - zero <= zero = true). +Check (eq_refl FEq : zero ?= - zero = FEq). +Check (eq_refl FEq : - zero ?= zero = FEq). + +Check (eq_refl true <: zero == - zero = true). +Check (eq_refl true <: - zero == zero = true). +Check (eq_refl false <: zero < - zero = false). +Check (eq_refl false <: - zero < zero = false). +Check (eq_refl true <: zero <= - zero = true). +Check (eq_refl true <: - zero <= zero = true). +Check (eq_refl FEq <: zero ?= - zero = FEq). +Check (eq_refl FEq <: - zero ?= zero = FEq). + +Check (eq_refl true <<: zero == - zero = true). +Check (eq_refl true <<: - zero == zero = true). +Check (eq_refl false <<: zero < - zero = false). +Check (eq_refl false <<: - zero < zero = false). +Check (eq_refl true <<: zero <= - zero = true). +Check (eq_refl true <<: - zero <= zero = true). +Check (eq_refl FEq <<: zero ?= - zero = FEq). +Check (eq_refl FEq <<: - zero ?= zero = FEq). + +Check (eq_refl true : - zero == - zero = true). +Check (eq_refl true : - zero == - zero = true). +Check (eq_refl false : - zero < - zero = false). +Check (eq_refl false : - zero < - zero = false). +Check (eq_refl true : - zero <= - zero = true). +Check (eq_refl true : - zero <= - zero = true). +Check (eq_refl FEq : - zero ?= - zero = FEq). +Check (eq_refl FEq : - zero ?= - zero = FEq). + +Check (eq_refl true <: - zero == - zero = true). +Check (eq_refl true <: - zero == - zero = true). +Check (eq_refl false <: - zero < - zero = false). +Check (eq_refl false <: - zero < - zero = false). +Check (eq_refl true <: - zero <= - zero = true). +Check (eq_refl true <: - zero <= - zero = true). +Check (eq_refl FEq <: - zero ?= - zero = FEq). +Check (eq_refl FEq <: - zero ?= - zero = FEq). + +Check (eq_refl true <<: - zero == - zero = true). +Check (eq_refl true <<: - zero == - zero = true). +Check (eq_refl false <<: - zero < - zero = false). +Check (eq_refl false <<: - zero < - zero = false). +Check (eq_refl true <<: - zero <= - zero = true). +Check (eq_refl true <<: - zero <= - zero = true). +Check (eq_refl FEq <<: - zero ?= - zero = FEq). +Check (eq_refl FEq <<: - zero ?= - zero = FEq). + +Check (eq_refl true : infinity == infinity = true). +Check (eq_refl true : infinity == infinity = true). +Check (eq_refl false : infinity < infinity = false). +Check (eq_refl false : infinity < infinity = false). +Check (eq_refl true : infinity <= infinity = true). +Check (eq_refl true : infinity <= infinity = true). +Check (eq_refl FEq : infinity ?= infinity = FEq). +Check (eq_refl FEq : infinity ?= infinity = FEq). + +Check (eq_refl true <: infinity == infinity = true). +Check (eq_refl true <: infinity == infinity = true). +Check (eq_refl false <: infinity < infinity = false). +Check (eq_refl false <: infinity < infinity = false). +Check (eq_refl true <: infinity <= infinity = true). +Check (eq_refl true <: infinity <= infinity = true). +Check (eq_refl FEq <: infinity ?= infinity = FEq). +Check (eq_refl FEq <: infinity ?= infinity = FEq). + +Check (eq_refl true <<: infinity == infinity = true). +Check (eq_refl true <<: infinity == infinity = true). +Check (eq_refl false <<: infinity < infinity = false). +Check (eq_refl false <<: infinity < infinity = false). +Check (eq_refl true <<: infinity <= infinity = true). +Check (eq_refl true <<: infinity <= infinity = true). +Check (eq_refl FEq <<: infinity ?= infinity = FEq). +Check (eq_refl FEq <<: infinity ?= infinity = FEq). + +Check (eq_refl true : - infinity == - infinity = true). +Check (eq_refl true : - infinity == - infinity = true). +Check (eq_refl false : - infinity < - infinity = false). +Check (eq_refl false : - infinity < - infinity = false). +Check (eq_refl true : - infinity <= - infinity = true). +Check (eq_refl true : - infinity <= - infinity = true). +Check (eq_refl FEq : - infinity ?= - infinity = FEq). +Check (eq_refl FEq : - infinity ?= - infinity = FEq). + +Check (eq_refl true <: - infinity == - infinity = true). +Check (eq_refl true <: - infinity == - infinity = true). +Check (eq_refl false <: - infinity < - infinity = false). +Check (eq_refl false <: - infinity < - infinity = false). +Check (eq_refl true <: - infinity <= - infinity = true). +Check (eq_refl true <: - infinity <= - infinity = true). +Check (eq_refl FEq <: - infinity ?= - infinity = FEq). +Check (eq_refl FEq <: - infinity ?= - infinity = FEq). + +Check (eq_refl true <<: - infinity == - infinity = true). +Check (eq_refl true <<: - infinity == - infinity = true). +Check (eq_refl false <<: - infinity < - infinity = false). +Check (eq_refl false <<: - infinity < - infinity = false). +Check (eq_refl true <<: - infinity <= - infinity = true). +Check (eq_refl true <<: - infinity <= - infinity = true). +Check (eq_refl FEq <<: - infinity ?= - infinity = FEq). +Check (eq_refl FEq <<: - infinity ?= - infinity = FEq). + +Check (eq_refl false : min_denorm == min_norm = false). +Check (eq_refl false : min_norm == min_denorm = false). +Check (eq_refl true : min_denorm < min_norm = true). +Check (eq_refl false : min_norm < min_denorm = false). +Check (eq_refl true : min_denorm <= min_norm = true). +Check (eq_refl false : min_norm <= min_denorm = false). +Check (eq_refl FLt : min_denorm ?= min_norm = FLt). +Check (eq_refl FGt : min_norm ?= min_denorm = FGt). + +Check (eq_refl false <: min_denorm == min_norm = false). +Check (eq_refl false <: min_norm == min_denorm = false). +Check (eq_refl true <: min_denorm < min_norm = true). +Check (eq_refl false <: min_norm < min_denorm = false). +Check (eq_refl true <: min_denorm <= min_norm = true). +Check (eq_refl false <: min_norm <= min_denorm = false). +Check (eq_refl FLt <: min_denorm ?= min_norm = FLt). +Check (eq_refl FGt <: min_norm ?= min_denorm = FGt). + +Check (eq_refl false <<: min_denorm == min_norm = false). +Check (eq_refl false <<: min_norm == min_denorm = false). +Check (eq_refl true <<: min_denorm < min_norm = true). +Check (eq_refl false <<: min_norm < min_denorm = false). +Check (eq_refl true <<: min_denorm <= min_norm = true). +Check (eq_refl false <<: min_norm <= min_denorm = false). +Check (eq_refl FLt <<: min_denorm ?= min_norm = FLt). +Check (eq_refl FGt <<: min_norm ?= min_denorm = FGt). + +Check (eq_refl false : min_denorm == one = false). +Check (eq_refl false : one == min_denorm = false). +Check (eq_refl true : min_denorm < one = true). +Check (eq_refl false : one < min_denorm = false). +Check (eq_refl true : min_denorm <= one = true). +Check (eq_refl false : one <= min_denorm = false). +Check (eq_refl FLt : min_denorm ?= one = FLt). +Check (eq_refl FGt : one ?= min_denorm = FGt). + +Check (eq_refl false <: min_denorm == one = false). +Check (eq_refl false <: one == min_denorm = false). +Check (eq_refl true <: min_denorm < one = true). +Check (eq_refl false <: one < min_denorm = false). +Check (eq_refl true <: min_denorm <= one = true). +Check (eq_refl false <: one <= min_denorm = false). +Check (eq_refl FLt <: min_denorm ?= one = FLt). +Check (eq_refl FGt <: one ?= min_denorm = FGt). + +Check (eq_refl false <<: min_denorm == one = false). +Check (eq_refl false <<: one == min_denorm = false). +Check (eq_refl true <<: min_denorm < one = true). +Check (eq_refl false <<: one < min_denorm = false). +Check (eq_refl true <<: min_denorm <= one = true). +Check (eq_refl false <<: one <= min_denorm = false). +Check (eq_refl FLt <<: min_denorm ?= one = FLt). +Check (eq_refl FGt <<: one ?= min_denorm = FGt). + +Check (eq_refl false : min_norm == one = false). +Check (eq_refl false : one == min_norm = false). +Check (eq_refl true : min_norm < one = true). +Check (eq_refl false : one < min_norm = false). +Check (eq_refl true : min_norm <= one = true). +Check (eq_refl false : one <= min_norm = false). +Check (eq_refl FLt : min_norm ?= one = FLt). +Check (eq_refl FGt : one ?= min_norm = FGt). + +Check (eq_refl false <: min_norm == one = false). +Check (eq_refl false <: one == min_norm = false). +Check (eq_refl true <: min_norm < one = true). +Check (eq_refl false <: one < min_norm = false). +Check (eq_refl true <: min_norm <= one = true). +Check (eq_refl false <: one <= min_norm = false). +Check (eq_refl FLt <: min_norm ?= one = FLt). +Check (eq_refl FGt <: one ?= min_norm = FGt). + +Check (eq_refl false <<: min_norm == one = false). +Check (eq_refl false <<: one == min_norm = false). +Check (eq_refl true <<: min_norm < one = true). +Check (eq_refl false <<: one < min_norm = false). +Check (eq_refl true <<: min_norm <= one = true). +Check (eq_refl false <<: one <= min_norm = false). +Check (eq_refl FLt <<: min_norm ?= one = FLt). +Check (eq_refl FGt <<: one ?= min_norm = FGt). + +Check (eq_refl false : one == infinity = false). +Check (eq_refl false : infinity == one = false). +Check (eq_refl true : one < infinity = true). +Check (eq_refl false : infinity < one = false). +Check (eq_refl true : one <= infinity = true). +Check (eq_refl false : infinity <= one = false). +Check (eq_refl FLt : one ?= infinity = FLt). +Check (eq_refl FGt : infinity ?= one = FGt). + +Check (eq_refl false <: one == infinity = false). +Check (eq_refl false <: infinity == one = false). +Check (eq_refl true <: one < infinity = true). +Check (eq_refl false <: infinity < one = false). +Check (eq_refl true <: one <= infinity = true). +Check (eq_refl false <: infinity <= one = false). +Check (eq_refl FLt <: one ?= infinity = FLt). +Check (eq_refl FGt <: infinity ?= one = FGt). + +Check (eq_refl false <<: one == infinity = false). +Check (eq_refl false <<: infinity == one = false). +Check (eq_refl true <<: one < infinity = true). +Check (eq_refl false <<: infinity < one = false). +Check (eq_refl true <<: one <= infinity = true). +Check (eq_refl false <<: infinity <= one = false). +Check (eq_refl FLt <<: one ?= infinity = FLt). +Check (eq_refl FGt <<: infinity ?= one = FGt). + +Check (eq_refl false : - infinity == infinity = false). +Check (eq_refl false : infinity == - infinity = false). +Check (eq_refl true : - infinity < infinity = true). +Check (eq_refl false : infinity < - infinity = false). +Check (eq_refl true : - infinity <= infinity = true). +Check (eq_refl false : infinity <= - infinity = false). +Check (eq_refl FLt : - infinity ?= infinity = FLt). +Check (eq_refl FGt : infinity ?= - infinity = FGt). + +Check (eq_refl false <: - infinity == infinity = false). +Check (eq_refl false <: infinity == - infinity = false). +Check (eq_refl true <: - infinity < infinity = true). +Check (eq_refl false <: infinity < - infinity = false). +Check (eq_refl true <: - infinity <= infinity = true). +Check (eq_refl false <: infinity <= - infinity = false). +Check (eq_refl FLt <: - infinity ?= infinity = FLt). +Check (eq_refl FGt <: infinity ?= - infinity = FGt). + +Check (eq_refl false <<: - infinity == infinity = false). +Check (eq_refl false <<: infinity == - infinity = false). +Check (eq_refl true <<: - infinity < infinity = true). +Check (eq_refl false <<: infinity < - infinity = false). +Check (eq_refl true <<: - infinity <= infinity = true). +Check (eq_refl false <<: infinity <= - infinity = false). +Check (eq_refl FLt <<: - infinity ?= infinity = FLt). +Check (eq_refl FGt <<: infinity ?= - infinity = FGt). + +Check (eq_refl false : - infinity == one = false). +Check (eq_refl false : one == - infinity = false). +Check (eq_refl true : - infinity < one = true). +Check (eq_refl false : one < - infinity = false). +Check (eq_refl true : - infinity <= one = true). +Check (eq_refl false : one <= - infinity = false). +Check (eq_refl FLt : - infinity ?= one = FLt). +Check (eq_refl FGt : one ?= - infinity = FGt). + +Check (eq_refl false <: - infinity == one = false). +Check (eq_refl false <: one == - infinity = false). +Check (eq_refl true <: - infinity < one = true). +Check (eq_refl false <: one < - infinity = false). +Check (eq_refl true <: - infinity <= one = true). +Check (eq_refl false <: one <= - infinity = false). +Check (eq_refl FLt <: - infinity ?= one = FLt). +Check (eq_refl FGt <: one ?= - infinity = FGt). + +Check (eq_refl false <<: - infinity == one = false). +Check (eq_refl false <<: one == - infinity = false). +Check (eq_refl true <<: - infinity < one = true). +Check (eq_refl false <<: one < - infinity = false). +Check (eq_refl true <<: - infinity <= one = true). +Check (eq_refl false <<: one <= - infinity = false). +Check (eq_refl FLt <<: - infinity ?= one = FLt). +Check (eq_refl FGt <<: one ?= - infinity = FGt). diff --git a/test-suite/primitive/float/gen_compare.sh b/test-suite/primitive/float/gen_compare.sh new file mode 100755 index 0000000000..cd87eb4e5b --- /dev/null +++ b/test-suite/primitive/float/gen_compare.sh @@ -0,0 +1,65 @@ +#!/bin/bash +# -*- compile-command: "mv -f compare.v{,~} && ./gen_compare.sh" -*- +set -e + +exec > compare.v + +cat <&2 "genTest expects 10 arguments" + fi + TACTICS=(":" "<:" "<<:") + OPS=("==" "<" "<=" "?=") + x="$1" + y="$2" + OPS1=("$3" "$4" "$5" "$6") # for x y + OPS2=("$7" "$8" "$9" "${10}") # for y x + for tac in "${TACTICS[@]}"; do + for i in {0..3}; do + op="${OPS[$i]}" + op1="${OPS1[$i]}" + op2="${OPS2[$i]}" + echo "Check (eq_refl $op1 $tac $x $op $y = $op1)." + echo "Check (eq_refl $op2 $tac $y $op $x = $op2)." + done + echo + done +} + +genTest nan nan \ + false false false FNotComparable \ + false false false FNotComparable +genTest nan "- nan" \ + false false false FNotComparable \ + false false false FNotComparable + +EQ=(true false true FEq \ + true false true FEq) + +genTest one one "${EQ[@]}" +genTest zero zero "${EQ[@]}" +genTest zero "- zero" "${EQ[@]}" +genTest "- zero" "- zero" "${EQ[@]}" +genTest infinity infinity "${EQ[@]}" +genTest "- infinity" "- infinity" "${EQ[@]}" + +LT=(false true true FLt \ + false false false FGt) + +genTest min_denorm min_norm "${LT[@]}" +genTest min_denorm one "${LT[@]}" +genTest min_norm one "${LT[@]}" +genTest one infinity "${LT[@]}" +genTest "- infinity" infinity "${LT[@]}" +genTest "- infinity" one "${LT[@]}" diff --git a/theories/Floats/FloatAxioms.v b/theories/Floats/FloatAxioms.v index 142883171e..d094032805 100644 --- a/theories/Floats/FloatAxioms.v +++ b/theories/Floats/FloatAxioms.v @@ -26,6 +26,10 @@ Qed. Axiom opp_spec : forall x, Prim2SF (-x)%float = SFopp (Prim2SF x). Axiom abs_spec : forall x, Prim2SF (abs x) = SFabs (Prim2SF x). +Axiom eqb_spec : forall x y, (x == y)%float = SFeqb (Prim2SF x) (Prim2SF y). +Axiom ltb_spec : forall x y, (x < y)%float = SFltb (Prim2SF x) (Prim2SF y). +Axiom leb_spec : forall x y, (x <= y)%float = SFleb (Prim2SF x) (Prim2SF y). + Definition flatten_cmp_opt c := match c with | None => FNotComparable diff --git a/theories/Floats/PrimFloat.v b/theories/Floats/PrimFloat.v index bdd78ea544..24e4ac2da2 100644 --- a/theories/Floats/PrimFloat.v +++ b/theories/Floats/PrimFloat.v @@ -18,6 +18,15 @@ Notation "- x" := (opp x) : float_scope. Primitive abs := #float64_abs. +Primitive eqb := #float64_eq. +Notation "x == y" := (eqb x y) (at level 70, no associativity) : float_scope. + +Primitive ltb := #float64_lt. +Notation "x < y" := (ltb x y) (at level 70, no associativity) : float_scope. + +Primitive leb := #float64_le. +Notation "x <= y" := (leb x y) (at level 70, no associativity) : float_scope. + Primitive compare := #float64_compare. Notation "x ?= y" := (compare x y) (at level 70, no associativity) : float_scope. @@ -72,33 +81,14 @@ Definition zero := Eval compute in (of_int63 0). Definition neg_zero := Eval compute in (-zero). Definition two := Eval compute in (of_int63 2). -Definition is_nan f := - match f ?= f with - | FNotComparable => true - | _ => false - end. - -Definition is_zero f := - match f ?= zero with - | FEq => true (* note: 0 == -0 with floats *) - | _ => false - end. - -Definition is_infinity f := - match f ?= infinity with - | FEq => true - | FLt => match f ?= neg_infinity with - | FEq => true - | _ => false - end - | _ => false - end. - -Definition get_sign f := (* + => false, - => true *) - let f := if is_zero f then one / f else f in - match f ?= zero with - | FGt => false - | _ => true - end. +Definition is_nan f := negb (f == f)%float. + +Definition is_zero f := (f == zero)%float. (* note: 0 == -0 with floats *) + +Definition is_infinity f := (abs f == infinity)%float. Definition is_finite (x : float) := negb (is_nan x || is_infinity x). + +Definition get_sign f := + let f := if is_zero f then (one / f)%float else f in + (f < zero)%float. diff --git a/theories/Floats/SpecFloat.v b/theories/Floats/SpecFloat.v index 900739812a..8708782e39 100644 --- a/theories/Floats/SpecFloat.v +++ b/theories/Floats/SpecFloat.v @@ -183,6 +183,24 @@ Section FloatOps. end end. + Definition SFeqb f1 f2 := + match SFcompare f1 f2 with + | Some Eq => true + | _ => false + end. + + Definition SFltb f1 f2 := + match SFcompare f1 f2 with + | Some Lt => true + | _ => false + end. + + Definition SFleb f1 f2 := + match SFcompare f1 f2 with + | Some Le => true + | _ => false + end. + Definition SFclassify f := match f with | S754_nan => NaN diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 635b9b2c88..b4c0a33585 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -275,6 +275,9 @@ GRAMMAR EXTEND Gram | "#int63_compare" -> { CPrimitives.Int63compare } | "#float64_opp" -> { CPrimitives.Float64opp } | "#float64_abs" -> { CPrimitives.Float64abs } + | "#float64_eq" -> { CPrimitives.Float64eq } + | "#float64_lt" -> { CPrimitives.Float64lt } + | "#float64_le" -> { CPrimitives.Float64le } | "#float64_compare" -> { CPrimitives.Float64compare } | "#float64_classify" -> { CPrimitives.Float64classify } | "#float64_add" -> { CPrimitives.Float64add } -- cgit v1.2.3