From 70b2ba35cacbfb9b790dd26364da18a39881ee0e Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Thu, 14 Feb 2019 15:47:18 +0000 Subject: [Manual] Document “Register” to kernel namespace --- doc/sphinx/proof-engine/vernacular-commands.rst | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index a98a46ba21..1eacb95131 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1227,3 +1227,15 @@ Exposing constants to OCaml libraries 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. -- cgit v1.2.3 From 4c48fcace7612e2f1eaf7ffa6e5265282dd0b549 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Thu, 14 Feb 2019 15:54:22 +0000 Subject: [Manual] Document “Register Inline” --- doc/sphinx/proof-engine/vernacular-commands.rst | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 1eacb95131..001bacc9ec 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1239,3 +1239,14 @@ Exposing constants to OCaml libraries 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. + +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. + + 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. -- cgit v1.2.3 From a27d9d43a8e1c1a1629cc72c87e582c323b503c7 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Mon, 18 Feb 2019 13:55:09 +0000 Subject: [Manual] Document the “Primitive” command --- doc/sphinx/proof-engine/vernacular-commands.rst | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 001bacc9ec..342425567e 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1250,3 +1250,17 @@ Inlining hints for the fast reduction machines 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. + +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). + + 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. -- cgit v1.2.3 From 43b2ddf9db407f6e5481974a626ac5c91d74910f Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Thu, 14 Feb 2019 16:39:12 +0000 Subject: [Manual] Document primitive integers --- doc/sphinx/language/gallina-extensions.rst | 49 +++++++++++++++++++++++++ doc/sphinx/proof-engine/vernacular-commands.rst | 2 + 2 files changed, 51 insertions(+) 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 342425567e..6c0290321d 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1240,6 +1240,8 @@ Exposing constants to OCaml libraries 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 ---------------------------------------------------------------- -- cgit v1.2.3 From e4c70510979209760956dc63f0aa15f969c8cf18 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Mon, 25 Feb 2019 10:04:53 +0000 Subject: [Manual] Refactor documentation of internal registration commands --- doc/sphinx/proof-engine/vernacular-commands.rst | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 6c0290321d..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,9 +1234,6 @@ 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: @@ -1243,18 +1249,15 @@ Exposing constants to OCaml libraries .. 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. - 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. - Registering primitive operations --------------------------------- +```````````````````````````````` .. cmd:: Primitive @ident__1 := #@ident__2. @@ -1263,6 +1266,3 @@ Registering primitive operations 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). - - 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. -- cgit v1.2.3