diff options
-rw-r--r-- | doc/refman/Classes.tex | 41 | ||||
-rw-r--r-- | doc/refman/RefMan-ext.tex | 69 | ||||
-rw-r--r-- | lib/util.ml | 2 | ||||
-rw-r--r-- | parsing/g_vernac.ml4 | 8 | ||||
-rw-r--r-- | theories/Classes/Morphisms.v | 2 |
5 files changed, 90 insertions, 32 deletions
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex index 23b018ee3..0ddbb6d89 100644 --- a/doc/refman/Classes.tex +++ b/doc/refman/Classes.tex @@ -47,6 +47,7 @@ record syntax of \Coq: \end{center} \begin{coq_eval} Reset Initial. + Generalizable All Variables. \end{coq_eval} The $\tele{\alpha_i : \tau_i}$ variables are called the \emph{parameters} @@ -126,36 +127,21 @@ particular support for type classes: class arguments, making derived functions as easy to use as class methods. In the example above, \texttt{A} and \texttt{eqa} should be set maximally implicit. -\item They support implicit quantification on class arguments and - partialy applied type classes (\S \ref{classes:impl-quant}) -\item They support implicit quantification on superclasses (\S \ref{classes:superclasses}) +\item They support implicit quantification on partialy applied type + classes (\S \ref{implicit-generalization}). + Any argument not given as part of a type class binder will be + automatically generalized. +\item They also support implicit quantification on superclasses + (\S \ref{classes:superclasses}) \end{itemize} -\subsection{Implicit quantification} -\label{classes:impl-quant} - -Implicit quantification is an automatic elaboration of a statement with -free variables into a closed statement where these variables are -quantified explicitly. Implicit generalization is done only inside -binders beginning with a backquote \texttt{`} and the codomain of -\texttt{Instance} declarations. - Following the previous example, one can write: \begin{coq_example} Definition neqb_impl `{eqa : EqDec A} (x y : A) := negb (eqb x y). \end{coq_example} Here \texttt{A} is implicitly generalized, and the resulting function -is equivalent to the one above. One must be careful that \emph{all} the -free variables are generalized, which may result in confusing errors in -case of typos. In such cases, the context will probably contain some -unexpected generalized variable. - -The generalizing binders \verb|`{ }| and \verb|`( )| work similarly to -their explicit counterparts, only binding the generalized variables -implicitly, as maximally-inserted arguments. In these binders, -the binding name for the bound object is optional, whereas the type is -mandatory, dually to regular binders. +is equivalent to the one above. \asection{Parameterized Instances} @@ -311,7 +297,7 @@ parameters {\binder$_1$} to {\binder$_n$} and fields {\tt field$_1$} to This variant declares a \emph{singleton} class whose only method is {\tt \ident$_1$}. This singleton class is a so-called definitional class, represented simply as a definition - {\tt \ident \binder$_1$ \ldots \binder$_n$ := \type$_1$} and whose + {\tt {\ident} \binder$_1$ \ldots \binder$_n$ := \type$_1$} and whose instances are themselves objects of this type. Definitional classes are not wrapped inside records, and the trivial projection of an instance of such a class is convertible to the instance itself. This can @@ -340,10 +326,12 @@ priority as for auto hints. \begin{Variants} \item {\tt Instance {\ident} {\binder$_1$ \ldots \binder$_n$} : + forall {\binder$_{n+1}$ \ldots \binder$_m$}, {Class} {t$_1$ \ldots t$_n$} [| \textit{priority}] := \term} - This syntax is used for declaration of singleton class instances. - It does not include curly braces and one need not even mention - the unique field name. + This syntax is used for declaration of singleton class instances or + for directly giving an explicit term of type + {\tt forall {\binder$_{n+1}$ \ldots \binder$_m$}, {Class} {t$_1$ \ldots t$_n$}}. + One need not even mention the unique field name for singleton classes. \item {\tt Global Instance} One can use the \texttt{Global} modifier on instances declared in a section so that their generalization is automatically @@ -409,5 +397,4 @@ based on a variant of eauto. The flags semantics are: %%% Local Variables: %%% mode: latex %%% TeX-master: "Reference-Manual" -%%% compile-command: "BIBINPUTS=\".\" make -C ../.. -f Makefile.stage3 doc/refman/Reference-Manual.pdf" %%% End: diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 3aa42dbd8..42374e368 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -1483,6 +1483,9 @@ but succeeds in Check Prop = nat. \end{coq_example*} + + + \subsection{Canonical structures \comindex{Canonical Structure}} @@ -1584,6 +1587,72 @@ Lemma cons_inj_bool : forall (m n:bool) l, n :: l = m :: l -> n = m. This is useful for declaring the implicit type of a single variable. \end{Variants} + +\subsection{Implicit generalization +\label{implicit-generalization} +\comindex{Generalizable Variables}} + +Implicit generalization is an automatic elaboration of a statement with +free variables into a closed statement where these variables are +quantified explicitly. Implicit generalization is done inside binders +starting with a \verb|`| and terms delimited by \verb|`{ }| and +\verb|`( )|, always introducing maximally inserted implicit arguments for +the generalized variables. Inside implicit generalization +delimiters, free variables in the current context are automatically +quantified using a product or a lambda abstraction to generate a closed +term. In the following statement for example, the variables \texttt{n} +and \texttt{m} are autamatically generalized and become explicit +arguments of the lemma as we are using \verb|`( )|: + +\begin{coq_example} +Generalizable All Variables. +Lemma nat_comm : `(n = n + 0). +\end{coq_example} +\begin{coq_eval} +Abort. +\end{coq_eval} +One can control the set of generalizable identifiers with the +\texttt{Generalizable} vernacular command to avoid unexpected +generalizations when mistyping identifiers. There are three variants of +the command: + +\begin{quote} +{\tt Generalizable (All|No) Variable(s)? ({\ident$_1$ \ident$_n$})?.} +\end{quote} + +\begin{Variants} +\item {\tt Generalizable All Variables.} All variables are candidate for + generalization if they appear free in the context under a + generalization delimiter. This may result in confusing errors in + case of typos. In such cases, the context will probably contain some + unexpected generalized variable. + +\item {\tt Generalizable No Variables.} Disable implicit generalization + entirely. This is the default behavior. + +\item {\tt Generalizable Variable(s)? {\ident$_1$ \ident$_n$}.} + Allow generalization of the given identifiers only. Calling this + command multiple times adds to the allowed identifiers. + +\item {\tt Global Generalizable} Allows to export the choice of + generalizable variables. +\end{Variants} + +One can also use implicit generalization for binders, in which case the +generalized variables are added as binders and set maximally implicit. +\begin{coq_example*} +Definition id `(x : A) : A := x. +\end{coq_example*} +\begin{coq_example} +Print id. +\end{coq_example} + +The generalizing binders \verb|`{ }| and \verb|`( )| work similarly to +their explicit counterparts, only binding the generalized variables +implicitly, as maximally-inserted arguments. In these binders, the +binding name for the bound object is optional, whereas the type is +mandatory, dually to regular binders. + \section{Coercions \label{Coercions} \index{Coercions}} diff --git a/lib/util.ml b/lib/util.ml index 9f29d55bd..5e2a071a9 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -810,7 +810,7 @@ let list_split_at index l = let list_split_when p = let rec split_when_loop x y = match y with - | [] -> ([],[]) + | [] -> (List.rev x,[]) | (a::l) -> if (p a) then (List.rev x,y) else split_when_loop (a::x) l in split_when_loop [] diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index a0ee06683..3bc27965a 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -553,9 +553,11 @@ GEXTEND Gram | IDENT "Implicit"; ["Type" | IDENT "Types"]; idl = LIST1 identref; ":"; c = lconstr -> VernacReserve (idl,c) - | IDENT "Generalizable"; ["Variable" | IDENT "Variables"]; - gen = [ IDENT "none" -> None | IDENT "all" -> Some [] | - idl = LIST1 identref -> Some idl ] -> + | IDENT "Generalizable"; + gen = [IDENT "All"; IDENT "Variables" -> Some [] + | IDENT "No"; IDENT "Variables" -> None + | [IDENT "Variable" | IDENT "Variables"]; + idl = LIST1 identref -> Some idl ] -> VernacGeneralizable (use_non_locality (), gen) ] ] ; implicit_name: diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index ac455415e..f5d08edb4 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -20,7 +20,7 @@ Require Import Coq.Program.Tactics. Require Import Coq.Relations.Relation_Definitions. Require Export Coq.Classes.RelationClasses. -Generalizable Variables all. +Generalizable All Variables. (** * Morphisms. |