diff options
| author | Pierre Roux | 2019-02-20 18:00:04 +0100 |
|---|---|---|
| committer | Pierre Roux | 2019-11-01 10:20:51 +0100 |
| commit | 6133877fc097412233a60740fdf94374abb79559 (patch) | |
| tree | 26655b276f177cc77f108524278eb620e03c97c1 /kernel | |
| parent | f0bf1511e59e528e090a87cfcc220f93c2431ecd (diff) | |
Add primitive floats to checker
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/float64.ml | 11 | ||||
| -rw-r--r-- | kernel/float64.mli | 3 |
2 files changed, 12 insertions, 2 deletions
diff --git a/kernel/float64.ml b/kernel/float64.ml index c0611f37a0..72f0d83359 100644 --- a/kernel/float64.ml +++ b/kernel/float64.ml @@ -35,6 +35,9 @@ let abs = abs_float type float_comparison = FEq | FLt | FGt | FNotComparable +(* inspired by lib/util.ml; see also #10471 *) +let pervasives_compare = compare + let compare x y = if x < y then FLt else @@ -137,5 +140,9 @@ let hash = let total_compare f1 f2 = (* pervasives_compare considers all NaNs as equal, which is fine here, but also considers -0. and +0. as equal *) - if f1 = 0. && f2 = 0. then Util.pervasives_compare (1. /. f1) (1. /. f2) - else Util.pervasives_compare f1 f2 + if f1 = 0. && f2 = 0. then pervasives_compare (1. /. f1) (1. /. f2) + else pervasives_compare f1 f2 + +let is_float64 t = + Obj.tag t = Obj.double_tag +[@@ocaml.inline always] diff --git a/kernel/float64.mli b/kernel/float64.mli index 1e6ea8bb96..927594115e 100644 --- a/kernel/float64.mli +++ b/kernel/float64.mli @@ -87,3 +87,6 @@ val hash : t -> int (** Total order relation over float values. Behaves like [Pervasives.compare].*) val total_compare : t -> t -> int + +val is_float64 : Obj.t -> bool +[@@ocaml.inline always] |