diff options
| author | Guillaume Bertholon | 2018-07-13 16:22:35 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-11-01 10:20:03 +0100 |
| commit | b0b3cc67e01b165272588b2d8bc178840ba83945 (patch) | |
| tree | 0fc62f69eb0b56a3cae6dd81f82ca869dac6fbc9 /vernac | |
| parent | f93684a412f067622a5026c406bc76032c30b6e9 (diff) | |
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.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/auto_ind_decl.ml | 1 | ||||
| -rw-r--r-- | vernac/g_vernac.mlg | 15 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 1 |
3 files changed, 16 insertions, 1 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 98fe436a22..5822a1a586 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -248,6 +248,7 @@ let build_beq_scheme mode kn = | Meta _ -> raise (EqUnknown "meta-variable") | Evar _ -> raise (EqUnknown "existential variable") | Int _ -> raise (EqUnknown "int") + | Float _ -> raise (EqUnknown "float") in aux t in diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 1387ca4675..78e4c89521 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -244,7 +244,8 @@ GRAMMAR EXTEND Gram ; register_type_token: - [ [ "#int63_type" -> { CPrimitives.PT_int63 } ] ] + [ [ "#int63_type" -> { CPrimitives.PT_int63 } + | "#float64_type" -> { CPrimitives.PT_float64 } ] ] ; register_prim_token: @@ -272,6 +273,18 @@ GRAMMAR EXTEND Gram | "#int63_lt" -> { CPrimitives.Int63lt } | "#int63_le" -> { CPrimitives.Int63le } | "#int63_compare" -> { CPrimitives.Int63compare } + | "#float64_opp" -> { CPrimitives.Float64opp } + | "#float64_abs" -> { CPrimitives.Float64abs } + | "#float64_compare" -> { CPrimitives.Float64compare } + | "#float64_add" -> { CPrimitives.Float64add } + | "#float64_sub" -> { CPrimitives.Float64sub } + | "#float64_mul" -> { CPrimitives.Float64mul } + | "#float64_div" -> { CPrimitives.Float64div } + | "#float64_sqrt" -> { CPrimitives.Float64sqrt } + | "#float64_of_int63" -> { CPrimitives.Float64ofInt63 } + | "#float64_normfr_mantissa" -> { CPrimitives.Float64normfr_mantissa } + | "#float64_frshiftexp" -> { CPrimitives.Float64frshiftexp } + | "#float64_ldshiftexp" -> { CPrimitives.Float64ldshiftexp } ] ] ; diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 7aa053e029..ec32c83670 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1847,6 +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) | k -> CErrors.user_err Pp.(str "Register: unknown identifier “" ++ str k ++ str "” in the “kernel” namespace") in match gr with |