From f93684a412f067622a5026c406bc76032c30b6e9 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 2 Apr 2019 22:39:32 +0200 Subject: Declare type of primitives in CPrimitives Rather than in typeops --- kernel/cPrimitives.mli | 22 +++++++++++++++------- 1 file changed, 15 insertions(+), 7 deletions(-) (limited to 'kernel/cPrimitives.mli') diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli index 6913371caf..3c825a8018 100644 --- a/kernel/cPrimitives.mli +++ b/kernel/cPrimitives.mli @@ -53,18 +53,26 @@ val kind : t -> args_red (** Special Entries for Register **) -type prim_ind = - | PIT_bool - | PIT_carry - | PIT_pair - | PIT_cmp - type prim_type = | PT_int63 +type 'a prim_ind = + | PIT_bool : unit prim_ind + | PIT_carry : prim_type prim_ind + | PIT_pair : (prim_type * prim_type) prim_ind + | PIT_cmp : unit prim_ind + +type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex + type op_or_type = | OT_op of t | OT_type of prim_type -val prim_ind_to_string : prim_ind -> string +val prim_ind_to_string : 'a prim_ind -> string val op_or_type_to_string : op_or_type -> string + +type ind_or_type = + | PITT_ind : 'a prim_ind * 'a -> ind_or_type + | PITT_type : prim_type -> ind_or_type + +val types : t -> ind_or_type list -- cgit v1.2.3 From b0b3cc67e01b165272588b2d8bc178840ba83945 Mon Sep 17 00:00:00 2001 From: Guillaume Bertholon Date: Fri, 13 Jul 2018 16:22:35 +0200 Subject: Add primitive float computation in Coq kernel Beware of 0. = -0. issue for primitive floats The IEEE 754 declares that 0. and -0. are treated equal but we cannot say that this is true with Leibniz equality. Therefore we must patch the equality and the total comparison inside the kernel to prevent inconsistency. --- kernel/cPrimitives.mli | 14 ++++++++++++++ 1 file changed, 14 insertions(+) (limited to 'kernel/cPrimitives.mli') diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli index 3c825a8018..f9424fb09d 100644 --- a/kernel/cPrimitives.mli +++ b/kernel/cPrimitives.mli @@ -33,6 +33,18 @@ type t = | Int63lt | Int63le | Int63compare + | Float64opp + | Float64abs + | Float64compare + | Float64add + | Float64sub + | Float64mul + | Float64div + | Float64sqrt + | Float64ofInt63 + | Float64normfr_mantissa + | Float64frshiftexp + | Float64ldshiftexp val equal : t -> t -> bool @@ -55,12 +67,14 @@ val kind : t -> args_red type prim_type = | PT_int63 + | PT_float64 type 'a prim_ind = | PIT_bool : unit 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 type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex -- cgit v1.2.3 From 79605dabb10e889ae998bf72c8483f095277e693 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 28 Aug 2018 14:31:37 +0200 Subject: Change return type of primitive float comparison Replace `option comparison` with `float_comparison` (:= `FEq | FLt | FGt | FNotComparable`) as suggested by Guillaume Melquiond to avoid boxing and an extra match when using primitive float comparison. --- kernel/cPrimitives.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/cPrimitives.mli') 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 -- cgit v1.2.3 From d18b928154a48ff8d90aaff69eca7d6eb3dfa0ab Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 28 Aug 2018 18:56:07 +0200 Subject: Implement classify on primitive float --- kernel/cPrimitives.mli | 2 ++ 1 file changed, 2 insertions(+) (limited to 'kernel/cPrimitives.mli') diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli index 3e6ec8dbcc..af95f6c6d7 100644 --- a/kernel/cPrimitives.mli +++ b/kernel/cPrimitives.mli @@ -36,6 +36,7 @@ type t = | Float64opp | Float64abs | Float64compare + | Float64classify | Float64add | Float64sub | Float64mul @@ -75,6 +76,7 @@ type 'a prim_ind = | PIT_pair : (prim_type * prim_type) prim_ind | PIT_cmp : unit prim_ind | PIT_f_cmp : unit prim_ind + | PIT_f_class : unit prim_ind type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex -- cgit v1.2.3 From 5f1270242f71a0a1da7c868967e1071d28ed83fb Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 28 Aug 2018 23:37:49 +0200 Subject: Add next_{up,down} primitive float functions --- kernel/cPrimitives.mli | 2 ++ 1 file changed, 2 insertions(+) (limited to 'kernel/cPrimitives.mli') diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli index af95f6c6d7..3cb210233d 100644 --- a/kernel/cPrimitives.mli +++ b/kernel/cPrimitives.mli @@ -46,6 +46,8 @@ type t = | Float64normfr_mantissa | Float64frshiftexp | Float64ldshiftexp + | Float64next_up + | Float64next_down val equal : t -> t -> bool -- cgit v1.2.3 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 --- kernel/cPrimitives.mli | 3 +++ 1 file changed, 3 insertions(+) (limited to 'kernel/cPrimitives.mli') 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 -- cgit v1.2.3