diff options
| author | Erik Martin-Dorel | 2019-11-01 10:00:01 +0100 |
|---|---|---|
| committer | Pierre Roux | 2019-11-01 10:22:07 +0100 |
| commit | acdaab2a8c2ccb63df364bb75de8a515b2cef484 (patch) | |
| tree | fb598f877b4010b1957f134a194cf59bec93da95 | |
| parent | 324072c12a164f98d0ffa8125d319ffb49df87d8 (diff) | |
docs(gallina-extensions.rst): Say more on float literals extraction
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 3f122f122b..54669534c7 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -2500,12 +2500,19 @@ 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 +The extraction of these primitives can be customized similarly to the extraction +of regular axioms (see :ref:`extraction`). Nonetheless, the :g:`ExtrOCamlFloats` +module can be used when extracting to OCaml: it maps the Coq primitives to types +and functions of a :g:`Float64` module. Said OCaml 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. +Literal values (of type :g:`Float64.t`) are extracted to literal OCaml +values (of type :g:`float`) written in hexadecimal notation and +wrapped into the :g:`Float64.of_float` constructor, e.g.: +:g:`Float64.of_float (0x1p+0)`. + Bidirectionality hints ---------------------- |