aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/byterun/coq_interp.c11
-rw-r--r--kernel/byterun/coq_values.h6
-rw-r--r--kernel/cClosure.ml55
-rw-r--r--kernel/cPrimitives.ml6
-rw-r--r--kernel/cPrimitives.mli2
-rw-r--r--kernel/float64.ml10
-rw-r--r--kernel/float64.mli2
-rw-r--r--kernel/primred.ml30
-rw-r--r--kernel/primred.mli8
-rw-r--r--kernel/retroknowledge.ml6
-rw-r--r--kernel/retroknowledge.mli4
-rw-r--r--kernel/safe_typing.ml31
-rw-r--r--kernel/typeops.ml12
-rw-r--r--pretyping/cbv.ml24
-rw-r--r--pretyping/reductionops.ml24
-rw-r--r--test-suite/primitive/float/double_rounding.v12
-rw-r--r--theories/Floats/FloatAxioms.v11
-rw-r--r--theories/Floats/PrimFloat.v17
-rw-r--r--vernac/vernacentries.ml2
19 files changed, 151 insertions, 122 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 55b973dcdb..74edd79872 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -1551,19 +1551,16 @@ value coq_interprete
x = Double_val(accu);
y = Double_val(*sp++);
if(x < y) {
- Alloc_small(accu, 1, coq_tag_Some);
- Field(accu, 0) = coq_Lt;
+ accu = coq_FLt;
}
else if(x > y) {
- Alloc_small(accu, 1, coq_tag_Some);
- Field(accu, 0) = coq_Gt;
+ accu = coq_FGt;
}
else if(x == y) {
- Alloc_small(accu, 1, coq_tag_Some);
- Field(accu, 0) = coq_Eq;
+ accu = coq_FEq;
}
else { // nan value
- accu = coq_None;
+ accu = coq_FNotComparable;
}
Next;
}
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index fa51b2d31f..c79a8f1b4f 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -42,8 +42,10 @@
#define coq_Eq Val_int(0)
#define coq_Lt Val_int(1)
#define coq_Gt Val_int(2)
-#define coq_tag_Some 1
-#define coq_None Val_int(0)
+#define coq_FEq Val_int(0)
+#define coq_FLt Val_int(1)
+#define coq_FGt Val_int(2)
+#define coq_FNotComparable Val_int(3)
#define FLOAT_EXP_SHIFT (2101) /* 2*emax + prec */
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 5f0da5da65..77352595f1 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -1052,17 +1052,22 @@ module FNativeEntries =
fcmp := { mark = mark Norm KnownR; term = FInd (Univ.in_punivs icmp) }
| None -> defined_cmp := false
- let defined_option = ref false
- let fSome = ref dummy
- let fNone = ref dummy
-
- let init_option retro =
- match retro.Retroknowledge.retro_option with
- | Some (cSome, cNone) ->
- defined_option := true;
- fSome := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cSome) };
- fNone := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cNone) }
- | None -> defined_option := false
+ let defined_f_cmp = ref false
+ let fFEq = ref dummy
+ let fFLt = ref dummy
+ let fFGt = ref dummy
+ let fFNotComparable = ref dummy
+
+ let init_f_cmp retro =
+ match retro.Retroknowledge.retro_f_cmp with
+ | Some (cFEq, cFLt, cFGt, cFNotComparable) ->
+ defined_f_cmp := true;
+ fFEq := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cFEq) };
+ fFLt := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cFLt) };
+ fFGt := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cFGt) };
+ fFNotComparable :=
+ { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cFNotComparable) };
+ | None -> defined_f_cmp := false
let defined_refl = ref false
@@ -1083,7 +1088,7 @@ module FNativeEntries =
init_carry !current_retro;
init_pair !current_retro;
init_cmp !current_retro;
- init_option !current_retro;
+ init_f_cmp !current_retro;
init_refl !current_retro
let check_env env =
@@ -1113,9 +1118,9 @@ module FNativeEntries =
check_env env;
assert (!defined_cmp)
- let check_option env =
+ let check_f_cmp env =
check_env env;
- assert (!defined_option)
+ assert (!defined_f_cmp)
let mkInt env i =
check_int env;
@@ -1155,15 +1160,21 @@ module FNativeEntries =
check_cmp env;
!fGt
- let mkSomeCmp env v =
- check_cmp env;
- check_option env;
- { mark = mark Cstr KnownR; term = FApp(!fSome, [|!fcmp;v|]) }
+ let mkFLt env =
+ check_f_cmp env;
+ !fFLt
- let mkNoneCmp env =
- check_cmp env;
- check_option env;
- { mark = mark Cstr KnownR; term = FApp(!fNone, [|!fcmp|]) }
+ let mkFEq env =
+ check_f_cmp env;
+ !fFEq
+
+ let mkFGt env =
+ check_f_cmp env;
+ !fFGt
+
+ let mkFNotComparable env =
+ check_f_cmp env;
+ !fFNotComparable
end
module FredNative = RedNative(FNativeEntries)
diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml
index 3154ee8c75..d5ed2c1a06 100644
--- a/kernel/cPrimitives.ml
+++ b/kernel/cPrimitives.ml
@@ -135,7 +135,7 @@ type 'a prim_ind =
| PIT_carry : prim_type prim_ind
| PIT_pair : (prim_type * prim_type) prim_ind
| PIT_cmp : unit prim_ind
- | PIT_option : unit prim_ind
+ | PIT_f_cmp : unit prim_ind
type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex
@@ -165,7 +165,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))]
- | Float64compare -> [float_ty; float_ty; PITT_ind (PIT_option, ())]
+ | Float64compare -> [float_ty; float_ty; PITT_ind (PIT_f_cmp, ())]
| Float64add | Float64sub | Float64mul
| Float64div -> [float_ty; float_ty; float_ty]
| Float64ldshiftexp -> [float_ty; int_ty; float_ty]
@@ -197,7 +197,7 @@ let prim_ind_to_string (type a) (p : a prim_ind) = match p with
| PIT_carry -> "carry"
| PIT_pair -> "pair"
| PIT_cmp -> "cmp"
- | PIT_option -> "option"
+ | PIT_f_cmp -> "f_cmp"
let prim_type_to_string = function
| PT_int63 -> "int63_type"
diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli
index f9424fb09d..3e6ec8dbcc 100644
--- a/kernel/cPrimitives.mli
+++ b/kernel/cPrimitives.mli
@@ -74,7 +74,7 @@ type 'a prim_ind =
| PIT_carry : prim_type prim_ind
| PIT_pair : (prim_type * prim_type) prim_ind
| PIT_cmp : unit prim_ind
- | PIT_option : unit prim_ind
+ | PIT_f_cmp : unit prim_ind
type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex
diff --git a/kernel/float64.ml b/kernel/float64.ml
index a625c0f551..eebc8f35ef 100644
--- a/kernel/float64.ml
+++ b/kernel/float64.ml
@@ -24,17 +24,17 @@ let of_float f = f
let opp = ( ~-. )
let abs = abs_float
-type float_comparison = Eq | Lt | Gt | NotComparable
+type float_comparison = FEq | FLt | FGt | FNotComparable
let compare x y =
- if x < y then Lt
+ if x < y then FLt
else
(
- if x > y then Gt
+ if x > y then FGt
else
(
- if x = y then Eq
- else NotComparable (* NaN case *)
+ if x = y then FEq
+ else FNotComparable (* NaN case *)
)
)
diff --git a/kernel/float64.mli b/kernel/float64.mli
index 7ced535dc0..c82f1d84da 100644
--- a/kernel/float64.mli
+++ b/kernel/float64.mli
@@ -24,7 +24,7 @@ val of_float : float -> t
val opp : t -> t
val abs : t -> t
-type float_comparison = Eq | Lt | Gt | NotComparable
+type float_comparison = FEq | FLt | FGt | FNotComparable
(** The IEEE 754 float comparison.
* NotComparable is returned if there is a NaN in the arguments *)
diff --git a/kernel/primred.ml b/kernel/primred.ml
index 1b9badfca9..5fe700cb9a 100644
--- a/kernel/primred.ml
+++ b/kernel/primred.ml
@@ -49,12 +49,12 @@ let add_retroknowledge env action =
| None -> ((ind,1), (ind,2), (ind,3))
| Some (((ind',_),_,_) as t) -> assert (eq_ind ind ind'); t in
{ retro with retro_cmp = Some r }
- | PIT_option ->
+ | PIT_f_cmp ->
let r =
- match retro.retro_option with
- | None -> ((ind,1), (ind,2))
- | Some (((ind',_),_) as t) -> assert (eq_ind ind ind'); t in
- { retro with retro_option = Some r }
+ match retro.retro_f_cmp with
+ | 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 }
in
set_retroknowledge env retro
@@ -94,10 +94,10 @@ let get_cmp_constructors env =
| Some r -> r
| None -> anomaly Pp.(str"Reduction of primitive: cmp not registered")
-let get_option_constructors env =
- match env.retroknowledge.retro_option with
+let get_f_cmp_constructors env =
+ match env.retroknowledge.retro_f_cmp with
| Some r -> r
- | None -> anomaly Pp.(str"Reduction of primitive: option not registered")
+ | None -> anomaly Pp.(str"Reduction of primitive: fcmp not registered")
exception NativeDestKO
@@ -119,8 +119,10 @@ module type RedNativeEntries =
val mkLt : env -> elem
val mkEq : env -> elem
val mkGt : env -> elem
- val mkSomeCmp : env -> elem -> elem
- val mkNoneCmp : env -> elem
+ val mkFLt : env -> elem
+ val mkFEq : env -> elem
+ val mkFGt : env -> elem
+ val mkFNotComparable : env -> elem
end
module type RedNative =
@@ -239,10 +241,10 @@ struct
| Float64compare ->
let f1, f2 = get_float2 evd args in
(match Float64.compare f1 f2 with
- | Float64.Eq -> E.mkSomeCmp env (E.mkEq env)
- | Float64.Lt -> E.mkSomeCmp env (E.mkLt env)
- | Float64.Gt -> E.mkSomeCmp env (E.mkGt env)
- | Float64.NotComparable -> E.mkNoneCmp env)
+ | Float64.FEq -> E.mkFEq env
+ | Float64.FLt -> E.mkFLt env
+ | Float64.FGt -> E.mkFGt env
+ | Float64.FNotComparable -> E.mkFNotComparable 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 b2c9ebc6ea..5531c81550 100644
--- a/kernel/primred.mli
+++ b/kernel/primred.mli
@@ -11,7 +11,7 @@ val get_bool_constructors : env -> constructor * constructor
val get_carry_constructors : env -> constructor * constructor
val get_pair_constructor : env -> constructor
val get_cmp_constructors : env -> constructor * constructor * constructor
-val get_option_constructors : env -> constructor * constructor
+val get_f_cmp_constructors : env -> constructor * constructor * constructor * constructor
exception NativeDestKO (* Should be raised by get_* functions on failure *)
@@ -33,8 +33,10 @@ module type RedNativeEntries =
val mkLt : env -> elem
val mkEq : env -> elem
val mkGt : env -> elem
- val mkSomeCmp : env -> elem -> elem
- val mkNoneCmp : env -> elem
+ val mkFLt : env -> elem
+ val mkFEq : env -> elem
+ val mkFGt : env -> elem
+ val mkFNotComparable : env -> elem
end
module type RedNative =
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index a84353bdc6..e897be6141 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -24,7 +24,9 @@ type retroknowledge = {
retro_pair : constructor option;
retro_cmp : (constructor * constructor * constructor) option;
(* Eq, Lt, Gt *)
- retro_option : (constructor * constructor) option; (* Some, None *)
+ retro_f_cmp : (constructor * constructor * constructor * constructor)
+ option;
+ (* FEq, FLt, FGt, FNotComparable *)
retro_refl : constructor option;
}
@@ -35,7 +37,7 @@ let empty = {
retro_carry = None;
retro_pair = None;
retro_cmp = None;
- retro_option = None;
+ retro_f_cmp = None;
retro_refl = None;
}
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index 0aca296d29..7aaf14e176 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -18,7 +18,9 @@ type retroknowledge = {
retro_pair : constructor option;
retro_cmp : (constructor * constructor * constructor) option;
(* Eq, Lt, Gt *)
- retro_option : (constructor * constructor) option; (* Some, None *)
+ retro_f_cmp : (constructor * constructor * constructor * constructor)
+ option;
+ (* FEq, FLt, FGt, FNotComparable *)
retro_refl : constructor option;
}
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 000f6125a6..241ee8ada3 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -1403,27 +1403,16 @@ let check_register_ind (type t) ind (r : t CPrimitives.prim_ind) env =
check_type_cte 1;
check_name 2 "Gt";
check_type_cte 2
- | CPrimitives.PIT_option ->
- check_nconstr 2;
- check_name 0 "Some";
- let cSome = ob.mind_user_lc.(0) in
- let s = Pp.str "the first option constructor (Some) has a wrong type" in
- begin match Term.decompose_prod cSome with
- | ([_,v;_,_V], codom) ->
- check_if (is_Type _V) s;
- check_if (Constr.equal v (mkRel 1)) s;
- check_if (Constr.equal codom (mkApp (mkRel 3, [|mkRel 2|]))) s
- | _ -> check_if false s
- end;
- check_name 1 "None";
- let cNone = ob.mind_user_lc.(1) in
- let s = Pp.str "the second option constructor (None) has a wrong type" in
- begin match Term.decompose_prod cNone with
- | ([_,_V], codom) ->
- check_if (is_Type _V) s;
- check_if (Constr.equal codom (mkApp (mkRel 2, [|mkRel 1|]))) s
- | _ -> check_if false s
- end
+ | CPrimitives.PIT_f_cmp ->
+ check_nconstr 4;
+ check_name 0 "FEq";
+ check_type_cte 0;
+ check_name 1 "FLt";
+ check_type_cte 1;
+ check_name 2 "FGt";
+ check_type_cte 2;
+ check_name 3 "FNotComparable";
+ check_type_cte 3
let register_inductive ind prim senv =
check_register_ind ind prim senv.env;
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index a9913772f2..3e79b174b8 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -241,16 +241,16 @@ let type_of_prim env t =
| Some ((ind,_),_,_) -> Constr.mkInd ind
| None -> CErrors.user_err Pp.(str"The type compare must be registered before this primitive.")
in
+ let f_compare_ty () =
+ match env.retroknowledge.Retroknowledge.retro_f_cmp with
+ | Some ((ind,_),_,_,_) -> Constr.mkInd ind
+ | None -> CErrors.user_err Pp.(str"The type float_comparison 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|])
| None -> CErrors.user_err Pp.(str"The type pair must be registered before this primitive.")
in
- let option_ty ty =
- match env.retroknowledge.Retroknowledge.retro_option with
- | Some ((ind,_),_) -> Constr.mkApp(Constr.mkInd ind, [|ty|])
- | None -> CErrors.user_err Pp.(str"The type option must be registered before this primitive.")
- in
let carry_ty int_ty =
match env.retroknowledge.Retroknowledge.retro_carry with
| Some ((ind,_),_) -> Constr.mkApp(Constr.mkInd ind, [|int_ty|])
@@ -265,7 +265,7 @@ 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_option, () -> option_ty (compare_ty ()) in
+ | PIT_f_cmp, () -> f_compare_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 520bcd6b41..bac13a0bd7 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -241,8 +241,6 @@ module VNativeEntries =
let float_ty env = VAL(0, mkConst @@ get_float_type env)
- let cmp_ty env = VAL(0, mkConst @@ get_cmp_type env)
-
let mkCarry env b e =
let (c0,c1) = get_carry_constructors env in
CONSTR(Univ.in_punivs (if b then c1 else c0), [|int_ty env;e|])
@@ -270,15 +268,21 @@ module VNativeEntries =
let (_eq,_lt,gt) = get_cmp_constructors env in
CONSTR(Univ.in_punivs gt, [||])
- let mkSomeCmp env v =
- let cmp_ty = cmp_ty env in
- let (some,_none) = get_option_constructors env in
- CONSTR(Univ.in_punivs some, [|cmp_ty;v|])
+ let mkFLt env =
+ let (_eq,lt,_gt,_nc) = get_f_cmp_constructors env in
+ CONSTR(Univ.in_punivs lt, [||])
+
+ let mkFEq env =
+ let (eq,_lt,_gt,_nc) = get_f_cmp_constructors env in
+ CONSTR(Univ.in_punivs eq, [||])
+
+ let mkFGt env =
+ let (_eq,_lt,gt,_nc) = get_f_cmp_constructors env in
+ CONSTR(Univ.in_punivs gt, [||])
- let mkNoneCmp env =
- let cmp_ty = cmp_ty env in
- let (_some,none) = get_option_constructors env in
- CONSTR(Univ.in_punivs none, [|cmp_ty|])
+ let mkFNotComparable env =
+ let (_eq,_lt,_gt,nc) = get_f_cmp_constructors env in
+ CONSTR(Univ.in_punivs nc, [||])
end
module VredNative = RedNative(VNativeEntries)
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 12419c04bc..321c64e411 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -891,15 +891,21 @@ struct
let (_eq, _lt, gt) = get_cmp_constructors env in
mkConstruct gt
- let mkSomeCmp env v =
- let cmp_ty = mkConst @@ get_cmp_type env in
- let (some, _none) = get_option_constructors env in
- mkApp(mkConstruct some, [|cmp_ty;v|])
-
- let mkNoneCmp env =
- let cmp_ty = mkConst @@ get_cmp_type env in
- let (_some, none) = get_option_constructors env in
- mkApp(mkConstruct none, [|cmp_ty|])
+ let mkFLt env =
+ let (_eq, lt, _gt, _nc) = get_f_cmp_constructors env in
+ mkConstruct lt
+
+ let mkFEq env =
+ let (eq, _lt, _gt, _nc) = get_f_cmp_constructors env in
+ mkConstruct eq
+
+ let mkFGt env =
+ let (_eq, _lt, gt, _nc) = get_f_cmp_constructors env in
+ mkConstruct gt
+
+ let mkFNotComparable env =
+ let (_eq, _lt, _gt, nc) = get_f_cmp_constructors env in
+ mkConstruct nc
end
module CredNative = RedNative(CNativeEntries)
diff --git a/test-suite/primitive/float/double_rounding.v b/test-suite/primitive/float/double_rounding.v
index 04c91cd56a..8aa9b4ca45 100644
--- a/test-suite/primitive/float/double_rounding.v
+++ b/test-suite/primitive/float/double_rounding.v
@@ -7,8 +7,8 @@ Definition small_cbn := Eval cbn in (one + ldexp one (-52)%Z)%float.
Definition result_cbn := Eval cbn in (big_cbn + small_cbn)%float.
Definition check_cbn := Eval cbn in (big_cbn + one)%float.
-Check (eq_refl : (result_cbn ?= big_cbn)%float = Some Gt).
-Check (eq_refl : (check_cbn ?= big_cbn)%float = Some Eq).
+Check (eq_refl : (result_cbn ?= big_cbn)%float = FGt).
+Check (eq_refl : (check_cbn ?= big_cbn)%float = FEq).
Definition big_cbv := Eval cbv in ldexp one (53)%Z.
@@ -16,8 +16,8 @@ Definition small_cbv := Eval cbv in (one + ldexp one (-52)%Z)%float.
Definition result_cbv := Eval cbv in (big_cbv + small_cbv)%float.
Definition check_cbv := Eval cbv in (big_cbv + one)%float.
-Check (eq_refl : (result_cbv ?= big_cbv)%float = Some Gt).
-Check (eq_refl : (check_cbv ?= big_cbv)%float = Some Eq).
+Check (eq_refl : (result_cbv ?= big_cbv)%float = FGt).
+Check (eq_refl : (check_cbv ?= big_cbv)%float = FEq).
Definition big_vm := Eval vm_compute in ldexp one (53)%Z.
@@ -25,5 +25,5 @@ Definition small_vm := Eval vm_compute in (one + ldexp one (-52)%Z)%float.
Definition result_vm := Eval vm_compute in (big_vm + small_vm)%float.
Definition check_vm := Eval vm_compute in (big_vm + one)%float.
-Check (eq_refl : (result_vm ?= big_vm)%float = Some Gt).
-Check (eq_refl : (check_vm ?= big_vm)%float = Some Eq).
+Check (eq_refl : (result_vm ?= big_vm)%float = FGt).
+Check (eq_refl : (check_vm ?= big_vm)%float = FEq).
diff --git a/theories/Floats/FloatAxioms.v b/theories/Floats/FloatAxioms.v
index d057d641da..d835e87ee0 100644
--- a/theories/Floats/FloatAxioms.v
+++ b/theories/Floats/FloatAxioms.v
@@ -22,7 +22,16 @@ Qed.
Axiom opp_spec : forall x, Prim2SF (-x)%float = SFopp (Prim2SF x).
Axiom abs_spec : forall x, Prim2SF (abs x) = SFabs (Prim2SF x).
-Axiom compare_spec : forall x y, (x ?= y)%float = SFcompare (Prim2SF x) (Prim2SF y).
+
+Definition flatten_cmp_opt c :=
+ match c with
+ | None => FNotComparable
+ | Some Eq => FEq
+ | Some Lt => FLt
+ | Some Gt => FGt
+ end.
+Axiom compare_spec : forall x y, (x ?= y)%float = flatten_cmp_opt (SFcompare (Prim2SF x) (Prim2SF y)).
+
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/PrimFloat.v b/theories/Floats/PrimFloat.v
index 21a1be8708..13763a39d1 100644
--- a/theories/Floats/PrimFloat.v
+++ b/theories/Floats/PrimFloat.v
@@ -1,5 +1,9 @@
Require Import Int63.
+Inductive float_comparison : Set := FEq | FLt | FGt | FNotComparable.
+
+Register float_comparison as kernel.ind_f_cmp.
+
Primitive float := #float64_type.
Declare Scope float_scope.
@@ -11,7 +15,6 @@ Notation "- x" := (opp x) : float_scope.
Primitive abs := #float64_abs.
-Register option as kernel.ind_option.
Primitive compare := #float64_compare.
Notation "x ?= y" := (compare x y) (at level 70, no associativity) : float_scope.
@@ -58,21 +61,21 @@ Definition two := Eval compute in (of_int63 2).
Definition is_nan f :=
match f ?= f with
- | None => true
+ | FNotComparable => true
| _ => false
end.
Definition is_zero f :=
match f ?= zero with
- | Some Eq => true (* note: 0 == -0 with floats *)
+ | FEq => true (* note: 0 == -0 with floats *)
| _ => false
end.
Definition is_infinity f :=
match f ?= infinity with
- | Some Eq => true
- | Some Lt => match f ?= neg_infinity with
- | Some Eq => true
+ | FEq => true
+ | FLt => match f ?= neg_infinity with
+ | FEq => true
| _ => false
end
| _ => false
@@ -81,7 +84,7 @@ Definition is_infinity f :=
Definition get_sign f := (* + => false, - => true *)
let f := if is_zero f then one / f else f in
match f ?= zero with
- | Some Gt => false
+ | FGt => false
| _ => true
end.
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index ec32c83670..c86b70c78e 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1847,7 +1847,7 @@ let vernac_register qid r =
| "ind_carry" -> CPrimitives.(PIE PIT_carry)
| "ind_pair" -> CPrimitives.(PIE PIT_pair)
| "ind_cmp" -> CPrimitives.(PIE PIT_cmp)
- | "ind_option" -> CPrimitives.(PIE PIT_option)
+ | "ind_f_cmp" -> CPrimitives.(PIE PIT_f_cmp)
| 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 14:20:57 +0000