coq/test-suite/primitive/float, branch master The formal proof system Add more explicit tests for next_up and next_down. 2020-11-18T13:36:45+00:00 Pierre Roux 2020-11-18T13:36:45+00:00 9815b5947a5c02ba9189a447f5b58d5bb81e4f93 






Bring Float notations in line with stdlib
2020-08-09T22:16:37+00:00

Jason Gross

2020-06-21T03:35:53+00:00

fcc3db46303d97e0696a1685619301be3622f4e9

This is a companion to #12479 as per
https://github.com/coq/coq/pull/12479#issuecomment-641336039 that
changes some of the PrimFloat notations:
- `m == n` into `m =? n` to correspond with the eqb notations elsewhere
- `m < n` into `m <? n` to correspond with the ltb notations elsewhere
- `m <= n` into `m <=? n` to correspond with the leb notations elsewhere

We also put them in a module, so users can `Require PrimFloat. Import
PrimFloat.PrimFloatNotations` without needing to unqualify the
primitives.

Fixes the part of #12454 about floats





This is a companion to #12479 as per
https://github.com/coq/coq/pull/12479#issuecomment-641336039 that
changes some of the PrimFloat notations:
- `m == n` into `m =? n` to correspond with the eqb notations elsewhere
- `m < n` into `m <? n` to correspond with the ltb notations elsewhere
- `m <= n` into `m <=? n` to correspond with the leb notations elsewhere

We also put them in a module, so users can `Require PrimFloat. Import
PrimFloat.PrimFloatNotations` without needing to unqualify the
primitives.

Fixes the part of #12454 about floats







Fix ldshiftexp
2019-11-01T09:21:35+00:00

Pierre Roux

2019-10-10T18:11:02+00:00

d39fab9a7c39d8da868c4481b96cf1086c21b1a4

* Fix the implementations and add tests
* Change shift from int63 to Z (was always used as a Z)
* Update FloatLemmas.v accordingly

Co-authored-by: Erik Martin-Dorel <erik.martin-dorel@irit.fr>





* Fix the implementations and add tests
* Change shift from int63 to Z (was always used as a Z)
* Update FloatLemmas.v accordingly

Co-authored-by: Erik Martin-Dorel <erik.martin-dorel@irit.fr>







Add "==", "<", "<=" in PrimFloat.v
2019-11-01T09:21:16+00:00

Erik Martin-Dorel

2019-07-03T13:08:44+00:00

f155ba664a782f000e278d97ee5666e2e7d2adea

* Add a related test-suite in compare.v (generated by a bash script)

Co-authored-by: Pierre Roux <pierre.roux@onera.fr>





* Add a related test-suite in compare.v (generated by a bash script)

Co-authored-by: Pierre Roux <pierre.roux@onera.fr>







Make primitive float work on x86_32
2019-11-01T09:21:03+00:00

Pierre Roux

2019-04-03T22:14:47+00:00

dca0135a263717b3a1a1d7c4f054f039dc08109e

Flag -fexcess-precision=standard is not enough on x86_32
where -msse2 -mfpmath=sse is required (-msse is not enough)
to avoid double rounding issues in the VM.

Most floating-point operation are now implemented in C because OCaml
is suffering double rounding issues on x86_32 with 80 bits extended
precision registers used for floating-point values, causing double
rounding making floating-point arithmetic incorrect with respect to
its specification.

Add a runtime test for double roundings.





Flag -fexcess-precision=standard is not enough on x86_32
where -msse2 -mfpmath=sse is required (-msse is not enough)
to avoid double rounding issues in the VM.

Most floating-point operation are now implemented in C because OCaml
is suffering double rounding issues on x86_32 with 80 bits extended
precision registers used for floating-point values, causing double
rounding making floating-point arithmetic incorrect with respect to
its specification.

Add a runtime test for double roundings.







Parsing primitive float constants
2019-11-01T09:20:55+00:00

Pierre Roux

2018-10-20T21:43:07+00:00

fdfcadc111fb5618a8e4a769c50607dc920b7dec












Add tests for primitive floats with 'native_compute'
2019-11-01T09:20:47+00:00

Pierre Roux

2019-06-09T08:41:10+00:00

f0bf1511e59e528e090a87cfcc220f93c2431ecd

Tests are updated to include native computations.





Tests are updated to include native computations.







Add next_{up,down} primitive float functions
2019-11-01T09:20:39+00:00

Pierre Roux

2018-08-28T21:37:49+00:00

5f1270242f71a0a1da7c868967e1071d28ed83fb












Implement classify on primitive float
2019-11-01T09:20:35+00:00

Pierre Roux

2018-08-28T16:56:07+00:00

d18b928154a48ff8d90aaff69eca7d6eb3dfa0ab












Change return type of primitive float comparison
2019-11-01T09:20:31+00:00

Pierre Roux

2018-08-28T12:31:37+00:00

79605dabb10e889ae998bf72c8483f095277e693

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.





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.