Extract modules from Gallina ext.

1 files changed, 1 insertions, 569 deletions

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 5b78280edc..ca045dc082 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1,288 +1,4 @@
-.. _extensionsofgallina:
-
-Extensions of |Gallina|
-=======================
-
-|Gallina| is the kernel language of |Coq|. We describe here extensions of
-|Gallina|’s syntax.
-
-Variants and extensions of :g:`match`
--------------------------------------
-
-.. _mult-match:
-
-Multiple and nested pattern matching
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-The basic version of :g:`match` allows pattern matching on simple
-patterns. As an extension, multiple nested patterns or disjunction of
-patterns are allowed, as in ML-like languages.
-
-The extension just acts as a macro that is expanded during parsing
-into a sequence of match on simple patterns. Especially, a
-construction defined using the extended match is generally printed
-under its expanded form (see :flag:`Printing Matching`).
-
-.. seealso:: :ref:`extendedpatternmatching`.
-
-.. _if-then-else:
-
-Pattern-matching on boolean values: the if expression
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-.. insertprodn term_if term_if
-
-.. prodn::
-   term_if ::= if @term {? {? as @name } return @term100 } then @term else @term
-
-For inductive types with exactly two constructors and for pattern matching
-expressions that do not depend on the arguments of the constructors, it is possible
-to use a ``if … then … else`` notation. For instance, the definition
-
-.. coqtop:: all
-
-   Definition not (b:bool) :=
-   match b with
-   | true => false
-   | false => true
-   end.
-
-can be alternatively written
-
-.. coqtop:: reset all
-
-   Definition not (b:bool) := if b then false else true.
-
-More generally, for an inductive type with constructors :n:`@ident__1`
-and :n:`@ident__2`, the following terms are equal:
-
-:n:`if @term__0 {? {? as @name } return @term } then @term__1 else @term__2`
-
-:n:`match @term__0 {? {? as @name } return @term } with | @ident__1 {* _ } => @term__1 | @ident__2 {* _ } => @term__2 end`
-
-.. example::
-
-  .. coqtop:: all
-
-     Check (fun x (H:{x=0}+{x<>0}) =>
-     match H with
-     | left _ => true
-     | right _ => false
-     end).
-
-Notice that the printing uses the :g:`if` syntax because :g:`sumbool` is
-declared as such (see :ref:`controlling-match-pp`).
-
-.. _irrefutable-patterns:
-
-Irrefutable patterns: the destructuring let variants
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-Pattern-matching on terms inhabiting inductive type having only one
-constructor can be alternatively written using :g:`let … in …`
-constructions. There are two variants of them.
-
-
-First destructuring let syntax
-++++++++++++++++++++++++++++++
-
-The expression :n:`let ( {*, @ident__i } ) := @term__0 in @term__1`
-performs case analysis on :n:`@term__0` whose type must be an
-inductive type with exactly one constructor.  The number of variables
-:n:`@ident__i` must correspond to the number of arguments of this
-contrustor.  Then, in :n:`@term__1`, these variables are bound to the
-arguments of the constructor in :n:`@term__0`.  For instance, the
-definition
-
-.. coqtop:: reset all
-
-   Definition fst (A B:Set) (H:A * B) := match H with
-   | pair x y => x
-   end.
-
-can be alternatively written
-
-.. coqtop:: reset all
-
-   Definition fst (A B:Set) (p:A * B) := let (x, _) := p in x.
-
-Notice that reduction is different from regular :g:`let … in …`
-construction since it happens only if :n:`@term__0` is in constructor form.
-Otherwise, the reduction is blocked.
-
-The pretty-printing of a definition by matching on a irrefutable
-pattern can either be done using :g:`match` or the :g:`let` construction
-(see Section :ref:`controlling-match-pp`).
-
-If term inhabits an inductive type with one constructor `C`, we have an
-equivalence between
-
-::
-
-   let (ident₁, …, identₙ) [dep_ret_type] := term in term'
-
-and
-
-::
-
-   match term [dep_ret_type] with
-   C ident₁ … identₙ => term'
-   end
-
-
-Second destructuring let syntax
-+++++++++++++++++++++++++++++++
-
-Another destructuring let syntax is available for inductive types with
-one constructor by giving an arbitrary pattern instead of just a tuple
-for all the arguments. For example, the preceding example can be
-written:
-
-.. coqtop:: reset all
-
-   Definition fst (A B:Set) (p:A*B) := let 'pair x _ := p in x.
-
-This is useful to match deeper inside tuples and also to use notations
-for the pattern, as the syntax :g:`let ’p := t in b` allows arbitrary
-patterns to do the deconstruction. For example:
-
-.. coqtop:: all
-
-   Definition deep_tuple (A:Set) (x:(A*A)*(A*A)) : A*A*A*A :=
-   let '((a,b), (c, d)) := x in (a,b,c,d).
-
-   Notation " x 'With' p " := (exist _ x p) (at level 20).
-
-   Definition proj1_sig' (A:Set) (P:A->Prop) (t:{ x:A | P x }) : A :=
-   let 'x With p := t in x.
-
-When printing definitions which are written using this construct it
-takes precedence over let printing directives for the datatype under
-consideration (see Section :ref:`controlling-match-pp`).
-
-
-.. _controlling-match-pp:
-
-Controlling pretty-printing of match expressions
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-The following commands give some control over the pretty-printing
-of :g:`match` expressions.
-
-Printing nested patterns
-+++++++++++++++++++++++++
-
-.. flag:: Printing Matching
-
-   The Calculus of Inductive Constructions knows pattern matching only
-   over simple patterns. It is however convenient to re-factorize nested
-   pattern matching into a single pattern matching over a nested
-   pattern.
-
-   When this flag is on (default), |Coq|’s printer tries to do such
-   limited re-factorization.
-   Turning it off tells |Coq| to print only simple pattern matching problems
-   in the same way as the |Coq| kernel handles them.
-
-
-Factorization of clauses with same right-hand side
-++++++++++++++++++++++++++++++++++++++++++++++++++
-
-.. flag:: Printing Factorizable Match Patterns
-
-   When several patterns share the same right-hand side, it is additionally
-   possible to share the clauses using disjunctive patterns. Assuming that the
-   printing matching mode is on, this flag (on by default) tells |Coq|'s
-   printer to try to do this kind of factorization.
-
-Use of a default clause
-+++++++++++++++++++++++
-
-.. flag:: Printing Allow Match Default Clause
-
-   When several patterns share the same right-hand side which do not depend on the
-   arguments of the patterns, yet an extra factorization is possible: the
-   disjunction of patterns can be replaced with a `_` default clause. Assuming that
-   the printing matching mode and the factorization mode are on, this flag (on by
-   default) tells |Coq|'s printer to use a default clause when relevant.
-
-Printing of wildcard patterns
-++++++++++++++++++++++++++++++
-
-.. flag:: Printing Wildcard
-
-   Some variables in a pattern may not occur in the right-hand side of
-   the pattern matching clause. When this flag is on (default), the
-   variables having no occurrences in the right-hand side of the
-   pattern matching clause are just printed using the wildcard symbol
-   “_”.
-
-
-Printing of the elimination predicate
-+++++++++++++++++++++++++++++++++++++
-
-.. flag:: Printing Synth
-
-   In most of the cases, the type of the result of a matched term is
-   mechanically synthesizable. Especially, if the result type does not
-   depend of the matched term. When this flag is on (default),
-   the result type is not printed when |Coq| knows that it can re-
-   synthesize it.
-
-
-Printing matching on irrefutable patterns
-++++++++++++++++++++++++++++++++++++++++++
-
-If an inductive type has just one constructor, pattern matching can be
-written using the first destructuring let syntax.
-
-.. table:: Printing Let @qualid
-   :name: Printing Let
-
-   Specifies a set of qualids for which pattern matching is displayed using a let expression.
-   Note that this only applies to pattern matching instances entered with :g:`match`.
-   It doesn't affect pattern matching explicitly entered with a destructuring
-   :g:`let`.
-   Use the :cmd:`Add` and :cmd:`Remove` commands to update this set.
-
-
-Printing matching on booleans
-+++++++++++++++++++++++++++++
-
-If an inductive type is isomorphic to the boolean type, pattern matching
-can be written using ``if`` … ``then`` … ``else`` ….  This table controls
-which types are written this way:
-
-.. table:: Printing If @qualid
-   :name: Printing If
-
-   Specifies a set of qualids for which pattern matching is displayed using
-   ``if`` … ``then`` … ``else`` ….  Use the :cmd:`Add` and :cmd:`Remove`
-   commands to update this set.
-
-This example emphasizes what the printing settings offer.
-
-.. example::
-
-     .. coqtop:: all
-
-       Definition snd (A B:Set) (H:A * B) := match H with
-       | pair x y => y
-       end.
-
-       Test Printing Let for prod.
-
-       Print snd.
-
-       Remove Printing Let prod.
-
-       Unset Printing Synth.
-
-       Unset Printing Wildcard.
-
-       Print snd.
-
-Module system
+Using modules
 -------------
 
 The module system provides a way of packaging related elements
@@ -828,287 +544,3 @@ subdirectories of path). See the command :cmd:`Declare ML Module` in
 
 See :ref:`command-line-options` for a more general view over the |Coq| command
 line options.
-
-.. _Coercions:
-
-Coercions
----------
-
-Coercions can be used to implicitly inject terms from one *class* in
-which they reside into another one. A *class* is either a sort
-(denoted by the keyword ``Sortclass``), a product type (denoted by the
-keyword ``Funclass``), or a type constructor (denoted by its name), e.g.
-an inductive type or any constant with a type of the form
-:n:`forall {+ @binder }, @sort`.
-
-Then the user is able to apply an object that is not a function, but
-can be coerced to a function, and more generally to consider that a
-term of type ``A`` is of type ``B`` provided that there is a declared coercion
-between ``A`` and ``B``.
-
-More details and examples, and a description of the commands related
-to coercions are provided in :ref:`implicitcoercions`.
-
-.. _printing_constructions_full:
-
-Printing constructions in full
-------------------------------
-
-.. flag:: Printing All
-
-   Coercions, implicit arguments, the type of pattern matching, but also
-   notations (see :ref:`syntax-extensions-and-notation-scopes`) can obfuscate the behavior of some
-   tactics (typically the tactics applying to occurrences of subterms are
-   sensitive to the implicit arguments). Turning this flag on
-   deactivates all high-level printing features such as coercions,
-   implicit arguments, returned type of pattern matching, notations and
-   various syntactic sugar for pattern matching or record projections.
-   Otherwise said, :flag:`Printing All` includes the effects of the flags
-   :flag:`Printing Implicit`, :flag:`Printing Coercions`, :flag:`Printing Synth`,
-   :flag:`Printing Projections`, and :flag:`Printing Notations`. To reactivate
-   the high-level printing features, use the command ``Unset Printing All``.
-
-   .. note:: In some cases, setting :flag:`Printing All` may display terms
-      that are so big they become very hard to read.  One technique to work around
-      this is use :cmd:`Undelimit Scope` and/or :cmd:`Close Scope` to turn off the
-      printing of notations bound to particular scope(s).  This can be useful when
-      notations in a given scope are getting in the way of understanding
-      a goal, but turning off all notations with :flag:`Printing All` would make
-      the goal unreadable.
-
-      .. see a contrived example here: https://github.com/coq/coq/pull/11718#discussion_r415481854
-
-.. _printing-universes:
-
-Printing universes
-------------------
-
-.. flag:: Printing Universes
-
-   Turn this flag on to activate the display of the actual level of each
-   occurrence of :g:`Type`. See :ref:`Sorts` for details. This wizard flag, in
-   combination with :flag:`Printing All` can help to diagnose failures to unify
-   terms apparently identical but internally different in the Calculus of Inductive
-   Constructions.
-
-.. cmd:: Print {? Sorted } Universes {? Subgraph ( {* @qualid } ) } {? @string }
-   :name: Print Universes
-
-   This command can be used to print the constraints on the internal level
-   of the occurrences of :math:`\Type` (see :ref:`Sorts`).
-
-   The :n:`Subgraph` clause limits the printed graph to the requested names (adjusting
-   constraints to preserve the implied transitive constraints between
-   kept universes).
-
-   The :n:`Sorted` clause makes each universe
-   equivalent to a numbered label reflecting its level (with a linear
-   ordering) in the universe hierarchy.
-
-   :n:`@string` is an optional output filename.
-   If :n:`@string` ends in ``.dot`` or ``.gv``, the constraints are printed in the DOT
-   language, and can be processed by Graphviz tools. The format is
-   unspecified if `string` doesn’t end in ``.dot`` or ``.gv``.
-
-.. _existential-variables:
-
-Existential variables
----------------------
-
-.. insertprodn term_evar term_evar
-
-.. prodn::
-   term_evar ::= _
-   | ?[ @ident ]
-   | ?[ ?@ident ]
-   | ?@ident {? @%{ {+; @ident := @term } %} }
-
-|Coq| terms can include existential variables which represents unknown
-subterms to eventually be replaced by actual subterms.
-
-Existential variables are generated in place of unsolvable implicit
-arguments or “_” placeholders when using commands such as ``Check`` (see
-Section :ref:`requests-to-the-environment`) or when using tactics such as
-:tacn:`refine`, as well as in place of unsolvable instances when using
-tactics such that :tacn:`eapply`. An existential
-variable is defined in a context, which is the context of variables of
-the placeholder which generated the existential variable, and a type,
-which is the expected type of the placeholder.
-
-As a consequence of typing constraints, existential variables can be
-duplicated in such a way that they possibly appear in different
-contexts than their defining context. Thus, any occurrence of a given
-existential variable comes with an instance of its original context.
-In the simple case, when an existential variable denotes the
-placeholder which generated it, or is used in the same context as the
-one in which it was generated, the context is not displayed and the
-existential variable is represented by “?” followed by an identifier.
-
-.. coqtop:: all
-
-   Parameter identity : forall (X:Set), X -> X.
-
-   Check identity _ _.
-
-   Check identity _ (fun x => _).
-
-In the general case, when an existential variable :n:`?@ident` appears
-outside of its context of definition, its instance, written under the
-form :n:`{ {*; @ident := @term} }` is appending to its name, indicating
-how the variables of its defining context are instantiated.
-The variables of the context of the existential variables which are
-instantiated by themselves are not written, unless the :flag:`Printing Existential Instances` flag
-is on (see Section :ref:`explicit-display-existentials`), and this is why an
-existential variable used in the same context as its context of definition is written with no instance.
-
-.. coqtop:: all
-
-   Check (fun x y => _) 0 1.
-
-   Set Printing Existential Instances.
-
-   Check (fun x y => _) 0 1.
-
-Existential variables can be named by the user upon creation using
-the syntax :n:`?[@ident]`. This is useful when the existential
-variable needs to be explicitly handled later in the script (e.g.
-with a named-goal selector, see :ref:`goal-selectors`).
-
-.. _explicit-display-existentials:
-
-Explicit displaying of existential instances for pretty-printing
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-.. flag:: Printing Existential Instances
-
-   This flag (off by default) activates the full display of how the
-   context of an existential variable is instantiated at each of the
-   occurrences of the existential variable.
-
-.. _tactics-in-terms:
-
-Solving existential variables using tactics
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-Instead of letting the unification engine try to solve an existential
-variable by itself, one can also provide an explicit hole together
-with a tactic to solve it. Using the syntax ``ltac:(``\ `tacexpr`\ ``)``, the user
-can put a tactic anywhere a term is expected. The order of resolution
-is not specified and is implementation-dependent. The inner tactic may
-use any variable defined in its scope, including repeated alternations
-between variables introduced by term binding as well as those
-introduced by tactic binding. The expression `tacexpr` can be any tactic
-expression as described in :ref:`ltac`.
-
-.. coqtop:: all
-
-   Definition foo (x : nat) : nat := ltac:(exact x).
-
-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.
-
-The extraction of these primitives can be customized similarly to the extraction
-of regular axioms (see :ref:`extraction`). Nonetheless, the :g:`ExtrOCamlInt63`
-module can be used when extracting to OCaml: it maps the Coq primitives to types
-and functions of a :g:`Uint63` 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 (at type :g:`Int63.int`) are extracted to literal OCaml values
-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.
-
-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)`.