- Documentation des nouvelles options d'implicites (Set Strongly Strict

  Implicit, Set Maximal Implicit Insertion, Set Reversible Pattern
  Implicit, Set Printing Implicit Defensive).
- Changement de la sémantique de Set Strongly Strict Implicit : il
  contient maintenant Set Strict Implicit.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10520 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 161 insertions, 38 deletions

diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 6cbd06eae..47409b984 100755
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -172,6 +172,7 @@
 \newcommand{\localdecls}{\textrm{\textsl{local\_decls}}}
 \newcommand{\ident}{\textrm{\textsl{ident}}}
 \newcommand{\accessident}{\textrm{\textsl{access\_ident}}}
+\newcommand{\possiblybracketedident}{\textrm{\textsl{possibly\_bracketed\_ident}}}
 \newcommand{\inductivebody}{\textrm{\textsl{ind\_body}}}
 \newcommand{\inductive}{\textrm{\textsl{inductive}}}
 \newcommand{\naturalnumber}{\textrm{\textsl{natural}}}
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 00eb5c6d2..01a0e9cad 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -335,7 +335,7 @@ $\equiv$~
 
 \subsubsection{{\tt let} pattern}
 
-Another destructuring {\tt let} syntax is available for inductives with
+Another destructuring {\tt 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:
 \begin{coq_eval}
@@ -431,14 +431,14 @@ to print wildcard for useless variables.
 \comindex{Test Printing Synth}}
 
 In most of the cases, the type of the result of a matched term is
-mechanically synthesisable. Especially, if the result type does not
+mechanically synthesizable. Especially, if the result type does not
 depend of the matched term.
 
 \begin{quote}
 {\tt Set Printing Synth.}
 \end{quote}
 The result type is not printed when {\Coq} knows that it can
-re-synthesise it.
+re-synthesize it.
 
 \begin{quote}
 {\tt Unset Printing Synth.}
@@ -448,8 +448,8 @@ This forces the result type to be always printed.
 \begin{quote}
 {\tt Test Printing Synth.}
 \end{quote}
-This tells if the non-printing of synthesisable types is on or off.
-The default is to not print synthesisable types.
+This tells if the non-printing of synthesizable types is on or off.
+The default is to not print synthesizable types.
 
 \subsubsection{Printing matching on irrefutable pattern
 \comindex{Add Printing Let {\ident}}
@@ -784,7 +784,7 @@ subgoals belonging to a Lemma {\ident}{\tt\_tcc}. % These subgoals are independe
 \index{Sections}
 \label{Section}}
 
-The sectioning mechanism allows to organise a proof in structured
+The sectioning mechanism allows to organize a proof in structured
 sections. Then local declarations become available (see
 Section~\ref{Simpl-definitions}). 
 
@@ -805,7 +805,7 @@ This command is used to open a section named {\ident}.
 This command closes the section named {\ident}. When a section is
 closed, all local declarations (variables and local definitions) are
 {\em discharged}. This means that all global objects defined in the
-section are generalised with respect to all variables and local
+section are generalized with respect to all variables and local
 definitions it depends on in the section.  None of the local
 declarations (considered as autonomous declarations) survive the end
 of the section.
@@ -831,7 +831,7 @@ inside section {\tt s1} and outside.
 
 \begin{Remarks}
 \item Most commands, like {\tt Hint}, {\tt Notation}, option management, ...
-which appear inside a section are cancelled when the
+which appear inside a section are canceled when the
 section is closed.
 % see Section~\ref{LongNames}
 %\item Usually all identifiers must be distinct. 
@@ -855,7 +855,7 @@ section is closed.
 \paragraph{Libraries}
 
 The theories developed in {\Coq} are stored in {\em libraries}.  A
-library is characterised by a name called {\it root} of the
+library is characterized by a name called {\it root} of the
 library. The standard library of {\Coq} has root name {\tt Coq} and is
 known by default when a {\Coq} session starts.
 
@@ -999,12 +999,23 @@ and {\tt coqc} by using option~\verb=-R=.
 \label{Implicit Arguments}}
 
 An implicit argument of a function is an argument which can be
-inferred from the knowledge of the type of other arguments of the
-function, or of the type of the surrounding context of the application.
-Especially, an implicit argument corresponds to a parameter
-dependent in the type of the function. Typical implicit
-arguments are the type arguments in polymorphic functions.
-More precisely, there are several kinds of implicit arguments.
+inferred from contextual knowledge. There are different kinds of
+implicit arguments that can be considered implicit in different
+ways. There are also various commands to control the setting or the
+inference of implicit arguments.
+
+\subsection{The different kinds of implicit arguments}
+
+\subsubsection{Implicit arguments inferable from the knowledge of other 
+arguments of a function}
+
+The first kind of implicit arguments covers the arguments that are
+inferable from the knowledge of the type of other arguments of the
+function, or of the type of the surrounding context of the
+application.  Especially, such implicit arguments correspond to 
+parameters dependent in the type of the function. Typical implicit
+arguments are the type arguments in polymorphic functions.  
+There are several kinds of such implicit arguments.
 
 \paragraph{Strict Implicit Arguments.} 
 An implicit argument can be either strict or non strict. An implicit
@@ -1024,12 +1035,12 @@ For instance, the first argument of
 in module {\tt List.v} is strict because {\tt list} is an inductive
 type and {\tt A} will always be inferable from the type {\tt
 list A} of the third argument of {\tt cons}.
-On the opposite, the second argument of a term of type 
+On the contrary, the second argument of a term of type 
 \begin{quote}
 \verb|forall P:nat->Prop, forall n:nat, P n -> ex nat P|
 \end{quote}
 is implicit but not strict, since it can only be inferred from the
-type {\tt P n} of the the third argument and if {\tt P} is e.g. {\tt
+type {\tt P n} of the third argument and if {\tt P} is, e.g., {\tt
 fun \_ => True}, it reduces to an expression where {\tt n} does not
 occur any longer. The first argument {\tt P} is implicit but not
 strict either because it can only be inferred from {\tt P n} and {\tt
@@ -1037,7 +1048,7 @@ P} is not canonically inferable from an arbitrary {\tt n} and the
 normal form of {\tt P n} (consider e.g. that {\tt n} is {\tt 0} and
 the third argument has type {\tt True}, then any {\tt P} of the form
 {\tt fun n => match n with 0 => True | \_ => \mbox{\em anything} end} would
-be a solution of the inference problem.
+be a solution of the inference problem).
 
 \paragraph{Contextual Implicit Arguments.} 
 An implicit argument can be {\em contextual} or not. An implicit
@@ -1053,6 +1064,46 @@ is contextual. Similarly, both arguments of a term of type
 \end{quote}
 are contextual (moreover, {\tt n} is strict and {\tt P} is not).
 
+\paragraph{Reversible-Pattern Implicit Arguments.}
+There is another class of implicit arguments that can be reinferred
+unambiguously if all the types of the remaining arguments are
+known. This is the class of implicit arguments occurring in the type
+of another argument in position of reversible pattern, which means it
+is at the head of an application but applied only to uninstantiated
+distinct variables. Such an implicit argument is called {\em
+reversible-pattern implicit argument}. A typical example is the
+argument {\tt P} of {\tt nat\_rec} in
+\begin{quote}
+{\tt nat\_rec : forall P : nat -> Set,
+       P 0 -> (forall n : nat, P n -> P (S n)) -> forall x : nat, P x}.
+\end{quote}
+({\tt P} is reinferable by abstracting over {\tt n} in the type {\tt P n}).
+
+See Section~\ref{SetReversiblePatternImplicit} for the automatic declaration
+of reversible-pattern implicit arguments.
+
+\subsubsection{Implicit arguments inferable by resolution}
+
+This corresponds to a class of non dependent implicit arguments that
+are solved based on the structure of their type only.
+
+\subsection{Maximal or non maximal insertion of implicit arguments}
+
+In case a function is partially applied, and the next argument to be
+applied is an implicit argument, two disciplines are applicable. In the
+first case, the function is considered to have no arguments furtherly:
+one says that the implicit argument is not maximally inserted. In
+the second case, the function is considered to be implicitly applied
+to the implicit arguments it is waiting for: one says that the
+implicit argument is maximally inserted.
+
+Each implicit argument can be declared to have to be inserted
+maximally or non maximally. This can be governed argument per argument
+by the command {\tt Implicit Arguments} (see~\ref{ImplicitArguments})
+or globally by the command {\tt Set Maximal Implicit Insertion}
+(see~\ref{SetMaximalImplicitInsertion}). See also
+Section~\ref{PrintImplicit}.
+
 \subsection{Casual use of implicit arguments}
 
 In a given expression, if it is clear that some argument of a function
@@ -1070,24 +1121,30 @@ possible, the correct argument will be automatically generated.
 
 \subsection{Declaration of implicit arguments for a constant
 \comindex{Implicit Arguments}}
+\label{ImplicitArguments}
 
 In case one wants that some arguments of a given object (constant,
 inductive types, constructors, assumptions, local or not) are always
 inferred by Coq, one may declare once for all which are the expected
 implicit arguments of this object. The syntax is
 \begin{quote}
-\tt Implicit Arguments {\qualid} [ \nelist{\ident}{} ]
+\tt Implicit Arguments {\qualid} [ \nelist{\possiblybracketedident}{} ]
 \end{quote}
-where the list of {\ident} is the list of parameters to be declared
-implicit. After this, implicit arguments can just (and have to) be
-skipped in any expression involving an application of {\qualid}.
+where the list of {\possiblybracketedident} is the list of parameters
+to be declared implicit, each of the identifier of the list being
+optionally surrounded by square brackets, then meaning that this
+parameter has to be maximally inserted.
+
+After the above declaration is issued, implicit arguments can just (and
+have to) be skipped in any expression involving an application of
+{\qualid}.
 
 \Example
 \begin{coq_eval}
 Reset Initial.
 \end{coq_eval}
 \begin{coq_example*}
-Inductive list (A:Set) : Set :=
+Inductive list (A:Type) : Type :=
  | nil : list A 
  | cons : A -> list A -> list A.
 \end{coq_example*}
@@ -1096,6 +1153,13 @@ Check (cons nat 3 (nil nat)).
 Implicit Arguments cons [A].
 Implicit Arguments nil [A].
 Check (cons 3 nil).
+Fixpoint map (A B:Type) (f:A->B) (l:list A) : list B :=
+  match l with nil => nil | cons a t => cons (f a) (map A B f t) end.
+Fixpoint length (A:Type) (l:list A) : nat :=
+  match l with nil => 0 | cons _ m => S (length A m) end.
+Implicit Arguments map [A B].
+Implicit Arguments length [[A]]. (* A has to be maximally inserted *)
+Check (fun l:list (list nat) => map length l).
 \end{coq_example}
 
 \Rem To know which are the implicit arguments of an object, use command
@@ -1111,9 +1175,11 @@ of a defined object. The command is just
 \begin{quote}
 \tt Implicit Arguments {\qualid}.
 \end{quote}
-The auto-detection is governed by options telling if strict and
-contextual implicit arguments must be considered or not (see
-Sections~\ref{SetStrictImplicit} and~\ref{SetContextualImplicit}). 
+The auto-detection is governed by options telling if strict,
+contextual, or reversible-pattern implicit arguments must be
+considered or not (see
+Sections~\ref{SetStrictImplicit},~\ref{SetContextualImplicit},~\ref{SetReversiblePatternImplicit}
+and also~\ref{SetMaximalImplicitInsertion}).
 
 \Example
 \begin{coq_eval}
@@ -1180,13 +1246,25 @@ contextual implicit arguments have to be considered or not.
 \comindex{Unset Strict Implicit}
 \label{SetStrictImplicit}}
 
-By default, {\Coq} automatically set implicit only the strict implicit
-arguments. To relax this constraint, use command 
+When the mode for automatic declaration of implicit arguments is on,
+the default is to automatically set implicit only the strict implicit
+arguments plus, for historical reasons, a small subset of the non
+strict implicit arguments. To relax this constraint and to
+set implicit all non strict implicit arguments by default, use the command
 \begin{quote}
 \tt Unset Strict Implicit.
 \end{quote}
-Conversely, use command {\tt Set Strict Implicit} to
-restore the strict implicit mode.
+Conversely, use the command {\tt Set Strict Implicit} to
+restore the original mode that declares implicit only the strict implicit arguments plus a small subset of the non strict implicit arguments.
+
+In the other way round, to capture exactly the strict implicit arguments and no more than the strict implicit arguments, use the command:
+\comindex{Set Strongly Strict Implicit}
+\comindex{Unset Strongly Strict Implicit}
+\begin{quote}
+\tt Set Strongly Strict Implicit.
+\end{quote}
+Conversely, use the command {\tt Unset Strongly Strict Implicit} to
+let the option ``{\tt Strict Implicit}'' decide what to do.
 
 \Rem In versions of {\Coq} prior to version 8.0, the default was to
 declare the strict implicit arguments as implicit.
@@ -1205,8 +1283,40 @@ argument, use command
 Conversely, use command {\tt Unset Contextual Implicit} to
 unset the contextual implicit mode.
 
+\subsection{Controlling reversible-pattern implicit arguments
+\comindex{Set Reversible Pattern Implicit}
+\comindex{Unset Reversible Pattern Implicit}
+\label{SetReversiblePatternImplicit}}
+
+By default, {\Coq} does not automatically set implicit the reversible-pattern
+implicit arguments. To tell {\Coq} to infer also reversible-pattern implicit
+argument, use command  
+\begin{quote}
+\tt Set Reversible Pattern Implicit. 
+\end{quote}
+Conversely, use command {\tt Unset Reversible Pattern Implicit} to
+unset the reversible-pattern implicit mode.
+
+\subsection{Controlling the insertion of implicit arguments not followed by explicit arguments
+\comindex{Set Maximal Implicit Insertion}
+\comindex{Unset Maximal Implicit Insertion}
+\label{SetMaximalImplicitInsertion}}
+
+Implicit arguments can be declared to be automatically inserted when a
+function is partially applied and the next argument of the function is
+an implicit one. In case the implicit arguments are automatically
+declared (with the command {\tt Set Implicit Arguments}), the command
+\begin{quote}
+\tt Set Maximal Implicit Insertion. 
+\end{quote}
+is used to tell to declare the implicit arguments with a maximal
+insertion status. By default, automatically declared implicit
+arguments are not declared to be insertable maximally.  To restore the
+default mode for maximal insertion, use command {\tt Unset Maximal
+Implicit Insertion}.
+
 \subsection{Explicit applications
-\index{Explicitation of implicit arguments}
+\index{Explicitly given implicit arguments}
 \label{Implicits-explicitation}
 \index{qualid@{\qualid}}}
 
@@ -1215,7 +1325,7 @@ partial applications, the synthesis of implicit arguments may fail, so
 one may have to give explicitly certain implicit arguments of an
 application. The syntax for this is {\tt (\ident:=\term)} where {\ident}
 is the name of the implicit argument and {\term} is its corresponding
-explicit term. Alternatively, one can locally deactivate the hidding of
+explicit term. Alternatively, one can locally deactivate the hiding of
 implicit arguments of a function by using the notation
 {\tt @{\qualid}~{\term}$_1$..{\term}$_n$}. This syntax extension is
 given Figure~\ref{fig:explicitations}.
@@ -1230,7 +1340,7 @@ given Figure~\ref{fig:explicitations}.
 & $|$ & {\tt ({\ident}:={\term})}\\
 \end{tabular}
 \end{centerframe}
-\caption{Syntax for explicitations of implicit arguments}
+\caption{Syntax for explicitly giving implicit arguments}
 \label{fig:explicitations}
 \end{figure}
 
@@ -1244,14 +1354,17 @@ Check (p (x:=a) (y:=b) r1 (z:=c) r2).
 \comindex{Print Implicit}
 \label{PrintImplicit}}
 
-To display the implicit arguments associated to an object use command
+To display the implicit arguments associated to an object, and to know
+if each of them is to be used maximally or not, use the command
 \begin{quote}
 \tt Print Implicit {\qualid}.
 \end{quote}
 
-\subsection{Explicitation of implicit arguments for pretty-printing
+\subsection{Explicit displaying of implicit arguments for pretty-printing
 \comindex{Set Printing Implicit}
-\comindex{Unset Printing Implicit}}
+\comindex{Unset Printing Implicit}
+\comindex{Set Printing Implicit Defensive}
+\comindex{Unset Printing Implicit Defensive}}
 
 By default the basic pretty-printing rules hide the inferable implicit
 arguments of an application. To force printing all implicit arguments,
@@ -1259,11 +1372,20 @@ use command
 \begin{quote}
 {\tt Set Printing Implicit.}
 \end{quote}
-Conversely, to restore the hidding of implicit arguments, use command
+Conversely, to restore the hiding of implicit arguments, use command
 \begin{quote}
 {\tt Unset Printing Implicit.}
 \end{quote}
 
+By default the basic pretty-printing rules display the implicit arguments that are not detected as strict implicit arguments. This ``defensive'' mode can quickly make the display cumbersome so this can be deactivated by using the command
+\begin{quote}
+{\tt Unset Printing Implicit Defensive.}
+\end{quote}
+Conversely, to force the display of non strict arguments, use command
+\begin{quote}
+{\tt Set Printing Implicit Defensive.}
+\end{quote}
+
 \SeeAlso {\tt Set Printing All} in Section~\ref{SetPrintingAll}.
 
 \subsection{Interaction with subtyping}
@@ -1321,7 +1443,7 @@ Canonical Structure nat_setoid.
 \end{coq_example*}
 
 Thanks to \texttt{nat\_setoid} declared as canonical, the implicit
-arguments {\tt A} and {\tt B} can be synthesised in the next statement.
+arguments {\tt A} and {\tt B} can be synthesized in the next statement.
 \begin{coq_example}
 Lemma is_law_S : is_law S.
 \end{coq_example}