diff options
| author | Erik Martin-Dorel | 2019-07-03 15:08:44 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-11-01 10:21:16 +0100 |
| commit | f155ba664a782f000e278d97ee5666e2e7d2adea (patch) | |
| tree | c7d9ddacde2059e4fa4745ce32395b9150764a1e /kernel/cPrimitives.ml | |
| parent | f8fdc27f922694edf74a7b608de1596e0a1ac0e3 (diff) | |
Add "==", "<", "<=" in PrimFloat.v
* Add a related test-suite in compare.v (generated by a bash script)
Co-authored-by: Pierre Roux <pierre.roux@onera.fr>
Diffstat (limited to 'kernel/cPrimitives.ml')
| -rw-r--r-- | kernel/cPrimitives.ml | 10 |
1 files changed, 10 insertions, 0 deletions
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 |