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/safe_typing.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/safe_typing.ml') diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index e846b17aa0..52bd9a6ada 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -1327,7 +1327,7 @@ let register_inline kn senv = let cb = {cb with const_inline_code = true} in let env = add_constant kn cb env in { senv with env} -let check_register_ind ind r env = +let check_register_ind (type t) ind (r : t CPrimitives.prim_ind) env = let (mb,ob as spec) = Inductive.lookup_mind_specif env ind in let check_if b msg = if not b then -- 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/safe_typing.ml | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) (limited to 'kernel/safe_typing.ml') diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 52bd9a6ada..000f6125a6 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -1403,6 +1403,27 @@ 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 let register_inductive ind prim senv = check_register_ind ind prim senv.env; -- 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/safe_typing.ml | 31 ++++++++++--------------------- 1 file changed, 10 insertions(+), 21 deletions(-) (limited to 'kernel/safe_typing.ml') 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; -- 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/safe_typing.ml | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) (limited to 'kernel/safe_typing.ml') diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 241ee8ada3..d3cffd1546 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -1413,6 +1413,26 @@ let check_register_ind (type t) ind (r : t CPrimitives.prim_ind) env = check_type_cte 2; check_name 3 "FNotComparable"; check_type_cte 3 + | CPrimitives.PIT_f_class -> + check_nconstr 9; + check_name 0 "PNormal"; + check_type_cte 0; + check_name 1 "NNormal"; + check_type_cte 1; + check_name 2 "PSubn"; + check_type_cte 2; + check_name 3 "NSubn"; + check_type_cte 3; + check_name 4 "PZero"; + check_type_cte 4; + check_name 5 "NZero"; + check_type_cte 5; + check_name 6 "PInf"; + check_type_cte 6; + check_name 7 "NInf"; + check_type_cte 7; + check_name 8 "NaN"; + check_type_cte 8 let register_inductive ind prim senv = check_register_ind ind prim senv.env; -- cgit v1.2.3