Merge PR #9578: Document primitive integers

Reviewed-by: Zimmi48
Reviewed-by: maximedenes

2 files changed, 91 insertions, 3 deletions

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 25f983ac1e..f1733a5ebf 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -2260,3 +2260,52 @@ expression as described in :ref:`ltac`.
 This construction is useful when one wants to define complicated terms
 using highly automated tactics without resorting to writing the proof-term
 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
+(excerpt from the :g:`Int63` module):
+
+.. coqdoc::
+
+   Primitive int := #int63_type.
+
+This type is equipped with a few operators, that must be similarly declared.
+For instance, equality of two primitive integers can be decided using the :g:`Int63.eqb` function,
+declared and specified as follows:
+
+.. coqdoc::
+
+   Primitive eqb := #int63_eq.
+   Notation "m '==' n" := (eqb m n) (at level 70, no associativity) : int63_scope.
+
+   Axiom eqb_correct : forall i j, (i == j)%int63 = true -> i = j.
+
+The complete set of such operators can be obtained looking at the :g:`Int63` module.
+
+These primitive declarations are regular axioms. As such, they must be trusted and are listed by the
+:g:`Print Assumptions` command, as in the following example.
+
+.. coqtop:: in reset
+
+   From Coq Require Import Int63.
+   Lemma one_minus_one_is_zero : (1 - 1 = 0)%int63.
+   Proof. apply eqb_correct; vm_compute; reflexivity. Qed.
+
+.. coqtop:: all
+
+   Print Assumptions one_minus_one_is_zero.
+
+The reduction machines (:tacn:`vm_compute`, :tacn:`native_compute`) implement
+dedicated, efficient, rules to reduce the applications of these primitive
+operations.
+
+These primitives, when extracted to OCaml (see :ref:`extraction`), are mapped to
+types and functions of a :g:`Uint63` 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.
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index a98a46ba21..3e8dd25ee0 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1213,10 +1213,19 @@ Controlling the locality of commands
      occurs in a section.  The :cmd:`Set` and :cmd:`Unset` commands belong to this
      category.
 
+.. _internal-registration-commands:
+
+Internal registration commands
+--------------------------------
+
+Due to their internal nature, the commands that are presented in this section
+are not for general use. They are meant to appear only in standard libraries and
+in support libraries of plug-ins.
+
 .. _exposing-constants-to-ocaml-libraries:
 
 Exposing constants to OCaml libraries
-----------------------------------------------------------------
+````````````````````````````````````````````````````````````````
 
 .. cmd:: Register @qualid__1 as @qualid__2
 
@@ -1225,5 +1234,35 @@ Exposing constants to OCaml libraries
    calling :n:`Coqlib.lib_ref "@qualid__2"`; i.e., there is no need to known
    where is the constant defined (file, module, library, etc.).
 
-   Due to its internal nature, this command is not for general use. It is meant
-   to appear only in standard libraries and in support libraries of plug-ins.
+   As a special case, when the first segment of :n:`@qualid__2` is :g:`kernel`,
+   the constant is exposed to the kernel. For instance, the `Int63` module
+   features the following declaration:
+
+   .. coqdoc::
+
+      Register bool as kernel.ind_bool.
+
+   This makes the kernel aware of what is the type of boolean values. This
+   information is used for instance to define the return type of the
+   :g:`#int63_eq` primitive.
+
+   .. seealso:: :ref:`primitive-integers`
+
+Inlining hints for the fast reduction machines
+````````````````````````````````````````````````````````````````
+
+.. cmd:: Register Inline @qualid
+
+   This command gives as a hint to the reduction machines (VM and native) that
+   the body of the constant :n:`@qualid` should be inlined in the generated code.
+
+Registering primitive operations
+````````````````````````````````
+
+.. cmd:: Primitive @ident__1 := #@ident__2.
+
+   Declares :n:`@ident__1` as the primitive operator :n:`#@ident__2`. When
+   running this command, the type of the primitive should be already known by
+   the kernel (this is achieved through this command for primitive types and
+   through the :cmd:`Register` command with the :g:`kernel` name-space for other
+   types).