coq - The formal proof system

Age	Commit message (Collapse)	Author
2019-11-01	Fix ldshiftexp	Pierre Roux
	* 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>
2019-11-01	docs: Add refman+stdlib documentation	Erik Martin-Dorel

2019-11-01	Add "==", "<", "<=" in PrimFloat.v	Erik Martin-Dorel
	* Add a related test-suite in compare.v (generated by a bash script) Co-authored-by: Pierre Roux <pierre.roux@onera.fr>
2019-11-01	Pretty-printing primitive float constants	Erik 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-01	Parsing primitive float constants	Pierre Roux

2019-11-01	Add next_{up,down} primitive float functions	Pierre Roux

2019-11-01	Implement classify on primitive float	Pierre Roux

2019-11-01	Change return type of primitive float comparison	Pierre 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-01	Put axioms on ldshiftexp and frshiftexp	Guillaume 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-01	Add Floats to standard library	Guillaume 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.