docs: Add refman+stdlib documentation

2 files changed, 145 insertions, 2 deletions

diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index ac75240cfb..cad5e4e67e 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -756,6 +756,7 @@ subdirectories:
   * **Sets** : Sets (classical, constructive, finite, infinite, power set, etc.) 
   * **FSets** : Specification and implementations of finite sets and finite maps (by lists and by AVL trees)
   * **Reals** : Axiomatization of real numbers (classical, basic functions, integer part, fractional part, limit, derivative, Cauchy series, power series and results,...)
+  * **Floats** : Machine implementation of floating-point arithmetic (for the binary64 format)
   * **Relations** : Relations (definitions and basic results)
   * **Sorting** : Sorted list (basic definitions and heapsort correctness)
   * **Strings** : 8-bits characters and strings
@@ -768,7 +769,7 @@ are directly accessible with the command ``Require`` (see
 Section :ref:`compiled-files`).
 
 The different modules of the |Coq| standard library are documented
-online at http://coq.inria.fr/stdlib.
+online at https://coq.inria.fr/stdlib.
 
 Peano’s arithmetic (nat)
 ~~~~~~~~~~~~~~~~~~~~~~~~
@@ -988,6 +989,106 @@ Notation    Interpretation  Precedence  Associativity
 ``_ :: _``  ``cons``        60          right
 ==========  ==============  ==========  =============
 
+.. _floats_library:
+
+Floats library
+~~~~~~~~~~~~~~
+
+The library of primitive floating-point arithmetic can be loaded by
+requiring module ``Floats``:
+
+.. coqtop:: in
+
+  Require Import Floats.
+
+It exports the module ``PrimFloat`` that provides a primitive type
+named ``float``, defined in the kernel (see section :ref:`primitive-floats`),
+as well as two variant types ``float_comparison`` and ``float_class``:
+
+
+.. coqtop:: all
+
+  Print float.
+  Print float_comparison.
+  Print float_class.
+
+It then defines the primitive operators below, using the processor
+floating-point operators for binary64 in rounding-to-nearest even:
+
+* ``abs``
+* ``opp``
+* ``sub``
+* ``add``
+* ``mul``
+* ``div``
+* ``sqrt``
+* ``compare`` : compare two floats and return a ``float_comparison``
+* ``classify`` : analyze a float and return a ``float_class``
+* ``of_int63`` : round a primitive integer and convert it into a float
+* ``normfr_mantissa`` : take a float in ``[0.5; 1.0)`` and return its mantissa
+* ``frshiftexp`` : convert a float to fractional part in ``[0.5; 1.0)`` and integer part
+* ``ldshiftexp`` : multiply a float by an integral power of ``2``
+* ``next_up`` : return the next float towards positive infinity
+* ``next_down`` : return the next float towards negative infinity
+
+For special floating-point values, the following constants are also
+defined:
+
+* ``zero``
+* ``neg_zero``
+* ``one``
+* ``two``
+* ``infinity``
+* ``neg_infinity``
+* ``nan`` : Not a Number (assumed to be unique: the "payload" of NaNs is ignored)
+
+The following table shows the notations available when opening scope
+``float_scope``.
+
+===========  ==============
+Notation     Interpretation
+===========  ==============
+``- _``      ``opp``
+``_ - _``    ``sub``
+``_ + _``    ``add``
+``_ * _``    ``mul``
+``_ / _``    ``div``
+``_ == _``   ``eqb``
+``_ < _``    ``ltb``
+``_ <= _``   ``leb``
+``_ ?= _``   ``compare``
+===========  ==============
+
+Floating-point constants are parsed and pretty-printed as (17-digit)
+decimal constants. This ensures that the composition
+:math:`\text{parse} \circ \text{print}` amounts to the identity.
+
+.. example::
+
+  .. coqtop:: all
+
+    Open Scope float_scope.
+    Eval compute in 1 + 0.5.
+    Eval compute in 1 / 0.
+    Eval compute in 1 / -0.
+    Eval compute in 0 / 0.
+    Eval compute in 0 ?= -0.
+    Eval compute in nan ?= nan.
+    Eval compute in next_down (-1).
+
+The primitive operators are specified with respect to their Gallina
+counterpart, using the variant type ``spec_float``, and the injection
+``Prim2SF``:
+
+.. coqtop:: all
+
+  Print spec_float.
+  Check Prim2SF.
+  Check mul_spec.
+
+For more details on the available definitions and lemmas, see the
+online documentation of the ``Floats`` library.
+
 .. _userscontributions:
 
 Users’ contributions
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index f50cf9340c..3f122f122b 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -2411,7 +2411,7 @@ by means of the interactive proof engine.
 .. _primitive-integers:
 
 Primitive Integers
---------------------------------
+------------------
 
 The language of terms features 63-bit machine integers as values. The type of
 such a value is *axiomatized*; it is declared through the following sentence
@@ -2464,6 +2464,48 @@ wrapped into the :g:`Uint63.of_int` (resp. :g:`Uint63.of_int64`) constructor on
 64-bit (resp. 32-bit) platforms. Currently, this cannot be customized (see the
 function :g:`Uint63.compile` from the kernel).
 
+.. _primitive-floats:
+
+Primitive Floats
+----------------
+
+The language of terms features Binary64 floating-point numbers as values.
+The type of such a value is *axiomatized*; it is declared through the
+following sentence (excerpt from the :g:`PrimFloat` module):
+
+.. coqdoc::
+
+   Primitive float := #float64_type.
+
+This type is equipped with a few operators, that must be similarly declared.
+For instance, the product of two primitive floats can be computed using the
+:g:`PrimFloat.mul` function, declared and specified as follows:
+
+.. coqdoc::
+
+   Primitive mul := #float64_mul.
+   Notation "x * y" := (mul x y) : float_scope.
+
+   Axiom mul_spec : forall x y, Prim2SF (x * y)%float = SF64mul (Prim2SF x) (Prim2SF y).
+
+where :g:`Prim2SF` is defined in the :g:`FloatOps` module.
+
+The set of such operators is described in section :ref:`floats_library`.
+
+These primitive declarations are regular axioms. As such, they must be trusted, and are listed by the
+:g:`Print Assumptions` command.
+
+The reduction machines (:tacn:`vm_compute`, :tacn:`native_compute`) implement
+dedicated, efficient rules to reduce the applications of these primitive
+operations, using the floating-point processor operators that are assumed
+to comply with the IEEE 754 standard for floating-point arithmetic.
+
+These primitives, when extracted to OCaml (see :ref:`extraction`), are mapped to
+types and functions of a :g:`Float64` module. Said module is not produced by
+extraction. Instead, it has to be provided by the user (if they want to compile
+or execute the extracted code). For instance, an implementation of this module
+can be taken from the kernel of Coq.
+
 Bidirectionality hints
 ----------------------