aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-11-01Pretty-printing primitive float constantsErik Martin-Dorel
* map special floats to registered CRef's * kernel/float64.mli: add {is_infinity, is_neg_infinity} functions * kernel/float64.ml: Replace string_of_float with a safe pretty-printing function Namely: let to_string_raw f = Printf.sprintf "%.17g" f let to_string f = if is_nan f then "nan" else to_string_raw f Summary: * printing a binary64 float in 17 decimal places and parsing it again will yield the same float, e.g.: let f1 = 1. +. (0x1p-53 +. 0x1p-105) let f2 = float_of_string (to_string f1) f1 = f2 * OCaml's string_of_float gives a sign to nan values which shouldn't be displayed as all NaNs are considered equal here.
2019-11-01Parsing primitive float constantsPierre Roux
2019-11-01Add primitive floats to checkerPierre Roux
2019-11-01Add tests for primitive floats with 'native_compute'Pierre Roux
Tests are updated to include native computations.
2019-11-01Add primitive floats to 'native_compute'Pierre Roux
* Float added to is_value/get_value to avoid stack overflows (cf. #7646) * beware of the use of Array.map with floats (cf. comment in the makeblock function) NB: From here one, the configure option "-native-compiler no" is no longer needed.
2019-11-01Add next_{up,down} primitive float functionsPierre Roux
2019-11-01Implement classify on primitive floatPierre Roux
2019-11-01Change return type of primitive float comparisonPierre Roux
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.
2019-11-01Put axioms on ldshiftexp and frshiftexpGuillaume Bertholon
Axioms on ldexp and frexp are replaced by proofs inside FloatLemmas. The shift value has been increased to 2 * emax + prec because in ldexp we want to be able to transform the smallest denormalized to the biggest float value in one call.
2019-11-01Add tests for primitive floats with 'vm_compute'Guillaume Bertholon
Tests are updated to include VM computations and check for double rounding.
2019-11-01Add primitive floats to 'vm_compute'Guillaume Bertholon
* This commit add float instructions to the VM, their encoding in bytecode and the interpretation of primitive float values after the reduction. * The flag '-std=c99' could be added to the C compiler flags to ensure that float computation strictly follows the norm (ie. i387 80-bits format is not used as an optimization). Actually, we use '-fexcess-precision=standard' instead of '-std=c99' because the latter would disable GNU asm used in the VM.
2019-11-01Add tests for primitive floatsGuillaume Bertholon
Add utility ldexp and frexp functions to prevent dealing with the shift of ldshiftexp and frshiftexp everywhere. Also move primitive integer tests to place all primitive tests in the same directory.
2019-11-01Add Floats to standard libraryGuillaume Bertholon
All supported floating point operations are defined on specification floats. Then we register the primitive type and functions, and add conversion functions to and from the specification type. Finally we put axioms to state that primitive operations behave exactly the same as specification operations. CREDITS: Most of the code inside SpecFloat is adapted from the Flocq library. NOTE: For the moment this code will not compile if native compilation is enabled in the configuration phase. This will be resolved later when native_compute will be supported by primitive floats. So please use option "-native-compiler no" in ./configure currently.
2019-11-01Add primitive floats to Ltac2Pierre Roux
2019-11-01Add primitive float computation in Coq kernelGuillaume Bertholon
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.
2019-11-01Declare type of primitives in CPrimitivesPierre Roux
Rather than in typeops
2019-10-31Merge PR #11021: Fix build in masterPierre-Marie Pédrot
2019-10-31lra: use “lia” rather than “omega”Vincent Laporte
2019-10-31Merge PR #10983: QArith, Lia: depend on ZArith_base rather than on ZArithPierre-Marie Pédrot
Ack-by: fajb Reviewed-by: ppedrot
2019-10-31Merge PR #10985: Print argument info as an Arguments command in AboutEmilio Jesus Gallego Arias
Ack-by: Zimmi48 Ack-by: cpitclaudel Reviewed-by: ejgallego
2019-10-31[prettyp] remove `mod_ops` and `indirect_accessor` parametersGaëtan Gilbert
`Prettyp` is now late enough in linking to refer to them.
2019-10-31Merge PR #10994: Numbers.Cyclic: use “lia” rather than “omega”Pierre-Marie Pédrot
2019-10-31Merge PR #10937: [stdlib]Reals: use “lia” rather than “omega”Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-10-31Merge PR #11000: make: guard cp calls with rm -f on executablesPierre-Marie Pédrot
Reviewed-by: gares
2019-10-31Merge PR #9883: Add support for Sorts in numeral notationsVincent Laporte
Ack-by: SkySkimmer Ack-by: proux01 Reviewed-by: vbgl
2019-10-31Merge PR #10997: Implement the unsupported attribute error using the warning ↵Emilio Jesus Gallego Arias
system Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2019-10-31lia: depend only on ZArith_baseVincent Laporte
2019-10-31QArith: only depend on ZArith_baseVincent Laporte
2019-10-31Zdigits: use “lia” rather than “omega”Vincent Laporte
2019-10-31Zquot: use “lia” rather than “omega”Vincent Laporte
2019-10-31Zpow_facts: use “lia” rather than “omega”Vincent Laporte
2019-10-31Zwf: use “lia” rather than “omega”Vincent Laporte
2019-10-31Zgcd_alt: use “lia” rather than “omega”Vincent Laporte
2019-10-31restore red behaviour printingGaëtan Gilbert
2019-10-31changelog for #10985Gaëtan Gilbert
2019-10-31Fix output testsGaëtan Gilbert
2019-10-31ppvernac: bidi hints use & not |Gaëtan Gilbert
2019-10-31Print argument info as an Arguments command in AboutGaëtan Gilbert
Close #10961
2019-10-31Move prettyp (Print implementation) to vernac/Gaëtan Gilbert
2019-10-31Doc: index command Arguments with assertGaëtan Gilbert
2019-10-31Move Arguments implementation to its own file (from vernacentries)Gaëtan Gilbert
2019-10-31Merge PR #10861: Fix #10615: Notation substitution for Ltac2 terms.Gaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: jfehrle
2019-10-31Merge PR #11009: Rename the 2 local type_cstr nonterminals to give them ↵Pierre-Marie Pédrot
unique names Reviewed-by: ppedrot
2019-10-31Merge PR #10995: add test for #4502 (fixed by unknown commit)Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-10-31Merge PR #10933: Add clarification in make-changelog.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-10-30Merge PR #10953: [declare] Remove declare_scheme hook in DeclarePierre-Marie Pédrot
Reviewed-by: ppedrot
2019-10-30Merge PR #11004: [test-suite] Test section-local mutual Fixpoint.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-10-30Rename the 2 local type_cstr nonterminals to give them unique namesJim Fehrle
2019-10-30Merge PR #10999: [refman] Give an example of contradiction when positivity ↵Clément Pit-Claudel
checking is disabled. Reviewed-by: cpitclaudel
2019-10-30[test-suite] Test section-local mutual Fixpoint.Emilio Jesus Gallego Arias
Noticed by coverage, test code by Gäetan Gilbert. Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 00:54:55 +0000