diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-21 18:54:25 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-21 18:54:25 +0000 |
commit | 86133a9fbf0397d8722368ef3068990f7ae0f689 (patch) | |
tree | dec41006d692cc958aa165b574f97901b52454c7 | |
parent | 5592007ae13ad8a6d4658dd8702c5627e0423d51 (diff) |
Diverses MAJ V7.1 autour des qualid
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8221 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | doc/RefMan-ext.tex | 161 | ||||
-rw-r--r-- | doc/RefMan-gal.tex | 46 | ||||
-rw-r--r-- | doc/RefMan-oth.tex | 134 | ||||
-rw-r--r-- | doc/RefMan-tac.tex | 48 | ||||
-rwxr-xr-x | doc/macros.tex | 2 |
5 files changed, 277 insertions, 114 deletions
diff --git a/doc/RefMan-ext.tex b/doc/RefMan-ext.tex index 0ed20012e..c2bafac0f 100644 --- a/doc/RefMan-ext.tex +++ b/doc/RefMan-ext.tex @@ -19,7 +19,7 @@ construction allows to define ``signatures''. \hline {\sentence} & ::= & {\record}\\ & & \\ -{\record} & ::= & {\tt Record} {\ident} {\tt [} {\params} {\tt ] :} {\sort} +{\record} & ::= & {\tt Record} {\ident} \zeroone{{\tt [} {\params} {\tt ]}} {\tt :} {\sort} \verb.:=. \zeroone{\ident} \verb!{! \zeroone{\nelist{\field}{;}} \verb!}! \verb:.:\\ @@ -33,24 +33,31 @@ construction allows to define ``signatures''. \label{record-syntax} \end{figure} -\noindent In the simple case, the command -``{\tt Record} {\ident} {\tt [} {\params} {\tt ]} \texttt{:} +\noindent In the expression + +\smallskip +{\tt Record} {\ident} {\tt [} {\params} {\tt ]} \texttt{:} {\sort} := {\ident$_0$} \verb+{+ {\ident$_1$} \texttt{:} {\term$_1$}; \dots - {\ident$_n$} \texttt{:} {\term$_n$} \verb+}+.'', + {\ident$_n$} \texttt{:} {\term$_n$} \verb+}+. +\smallskip + the identifier {\ident} is the name of the defined record and {\sort} is its type. The identifier {\ident$_0$} is the name of its -constructor. If {\ident$_0$} is omitted, the default name {\tt Build\_{\ident}} is used. The identifiers {\ident$_1$}, .., {\ident$_n$} are the -names of its fields and {\term$_1$}, .., {\term$_n$} their respective -types. Records can have parameters. - -In the more general case, a record may have explicitly defined (aka +constructor. If {\ident$_0$} is omitted, the default name {\tt +Build\_{\ident}} is used. The identifiers {\ident$_1$}, .., +{\ident$_n$} are the names of fields and {\term$_1$}, .., {\term$_n$} +their respective types. Remark that the type of {\ident$_i$} may +depend on the previous {\ident$_j$} (for $j<i$). Thus the order of the +fields is important. Finally, {\params} are the parameters of the +record. + +More generally, a record may have explicitly defined (a.k.a. manifest) fields. For instance, {\tt Record} {\ident} {\tt [} {\params} {\tt ]} \texttt{:} {\sort} := \verb+{+ {\ident$_1$} \texttt{:} {\type$_1$} \verb+;+ {\ident$_2$} \texttt{:=} {\term$_2$} \verb+;+. -{\ident$_3$} \texttt{:} {\type$_3$} \verb+}+. But this is not yet -documented. +{\ident$_3$} \texttt{:} {\type$_3$} \verb+}+ in which case the correctness of {\type$_3$} may rely on the instance {\term$_2$} of {\ident$_2$ and {\term$_2$} in turn may depend on {\ident$_1$}. \Example @@ -67,10 +74,8 @@ Record Rat : Set := mkRat { Rat_irred_cond:(x,y,z:nat)(mult x y)=top/\(mult x z)=bottom->x=(S O)}. \end{coq_example} -A field may depend on other fields appearing before it. -For instance in the above example, the field -\verb+Rat_cond+ depends on the field \verb+bottom+. Thus the order of -the fields is important. +Remark here that the field +\verb+Rat_cond+ depends on the field \verb+bottom+. Let us now see the work done by the {\tt Record} macro. First the macro generates a inductive definition @@ -129,7 +134,7 @@ Check half. The macro generates also, when it is possible, the projection functions for destructuring an object of type {\ident}. These projection functions have the same name that the corresponding -field. In our example: +fields. In our example: \begin{coq_example} Eval Compute in (top half). @@ -524,6 +529,105 @@ can be reused. In this case, the old name is no longer accessible. module with an identifier already used in the module (see \ref{compiled}). \end{Remarks} +\section{Libraries and long names} + +\paragraph{Libraries} + +The theories developed in {\Coq} are stored in {\em libraries}. A +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. + +Libraries have a tree structure. Typically, the {\tt Coq} library +contains the sub-libraries {\tt Init}, {\tt Logic}, {\tt Arith}, {\tt +Lists}, ... The ``dot notation'' is used to separate the different +component of a library name. Typically, the {\tt Arith} library of +{\Coq} standard library is written ``{\tt Coq.Arith}''. + +\medskip +\Rem no space is allowed between the dot and the following +identifier, otherwise the dot is interpreted as the final dot of the +command! +\medskip + +Libraries and sub-libraries can be mapped to physical directories of the +operating system using the command (see \ref{AddLoadPath}) + +\begin{quote} +{\tt Add LoadPath {\it physical\_dir} as {\it (sub-)library}}. +\end{quote} + +A library can inherit the tree structure of a physical directory by +using the command (see \ref{AddRecLoadPath}) + +\begin{quote} +{\tt Add Rec LoadPath {\it physical\_dir} as {\it (sub-)library}}. +\end{quote} + +At some point, (sub-)libraries contain {\it modules} which coincide +with files at the physical level. Modules themselves contain +axioms, parameters, definitions, lemmas and theorems. + +As for sublibraries, the dot notation is used to denote a specific +module, axiom, parameter, definition, lemma or theorem of a +library. Typically, {\tt Coq.Init.Logic.eq} denotes Leibniz' equality +defined in the module {\tt Logic} in the sublibrary {\tt Init} of the +standard library of \Coq. + +\paragraph{Absolute and short names} + +The full name of a library, module, section, definition, theorem, +... is called {\it absolute}. +The final identifier (in the example +above, it is {\tt eq}) is called {\it short name} (or sometimes {\it +base name}. {\Coq} maintains a {\it names table} mapping short names +to absolute names. This greatly simplifies the notations. {\Coq} +cannot accept two constructions (definition, theorem, ...) with the +same absolute name. + +As a special case, the logical name of a library, module or section is +called a {\em logical directory path} (written {\dirpath}). + +\paragraph{Visibility and qualified names} +An absolute path is called {\it visible} when its base name suffices +to denote it. This means the base name is mapped to the absolute name +in {\Coq} name table. + +All the base names of sublibraries, modules, sections, definitions and +theorems are automatically put in the {\Coq} name table. But sometimes, +the short name of a construction defined in a module may hide the short name of another construction defined in another module. +Instead of just distinguishing the clashing names by using the +absolute names, it is enough to prefix the base name just by the name +of the module in which the definition, theorem, ... is defined. +% Remark: when modules will be available, longer qualification may be needed +Such a name built from single identifiers separated by dots is called +a {\em partially qualified name} (or shortly a {\em qualified name}, +written {\qualid}). Especially, both absolute names and short names +are qualified names. To ensure that a construction always remains +accessible, absolute names can never be hidden. + +Examples: + +\begin{coq_eval} +Reset Initial. +\end{coq_eval} + +\begin{coq_example} +Check O. +Definition nat := bool. +Check O. +Check Datatypes.nat. +\end{coq_example} + +\paragraph{Requiring a file} + +A module compiled in a ``.vo'' file comes with a logical names (e.g. +physical file \verb!theories/Init/Datatypes.vo! in {\Coq} installation directory contains logical module {\tt Coq.Init.Datatypes}). +When requiring the file, the mapping between physical directories and logical library should be consistent with the mapping used to compile the file (for modules of the standard library, this is automatic -- check it by typing {\tt Print LoadPath}). + +The command {\tt Add Rec LoadPath} is also available from {\tt coqtop} +and {\tt coqc} by using option~\verb=-R= (see section \ref{Tools}). + \section{Implicit arguments}\index{implicit arguments} The {\Coq} system allows to skip during a function application certain @@ -561,13 +665,13 @@ arguments, one can omit the implicit ones. They are then automatically replaced by symbols ``?'', to be inferred by the mechanism of synthesis of implicit arguments. -\subsubsection{\tt Implicit Arguments {\switch}.} -\comindex{Implicit Arguments} +\subsubsection{\tt Set Implicit Arguments.} +\comindex{Set Implicit Arguments} \label{Implicit Arguments} -If {\switch} is {\tt On} then the command switches on the automatic -mode. If {\switch} is {\tt Off} then the command switches off the -automatic mode. The mode {\tt Off} is the default mode. +This command switches the automatic implicit arguments +mode on. To switch it off, use {\tt Unset Implicit Arguments.}. +The mode is off by default. The computation of implicit arguments takes account of the unfolding of constants. For instance, the variable {\tt p} below has @@ -577,7 +681,7 @@ y) -> (z:U)(R y z) -> (R x z)}. As the variables {\tt x}, {\tt y} and correspond respectively to the positions {\tt 1}, {\tt 2} and {\tt 4}. \begin{coq_example*} -Implicit Arguments On. +Set Implicit Arguments. Variable X : Type. Definition Relation := X -> X -> Prop. Definition Transitivity := [R:Relation] @@ -643,7 +747,7 @@ Let us extend our functional language with the definition of the identity function: \begin{coq_eval} -Implicit Arguments Off. +Unset Implicit Arguments. Reset Initial. \end{coq_eval} \begin{coq_example} @@ -774,6 +878,17 @@ Print the list of declared coercions in the current context. \subsubsection{\tt Print Graph.}\comindex{Print Graph} Print the list of valid path coercions in the current context. +\subsection{Activating the printing of coercions} + +\subsubsection{\tt Set Printing Coercions.} +\comindex{Set Printing Coercions} +\comindex{Unset Printing Coercions} + +This command forces the coercions to be printed. +To skip the printing of coercions, use + {\tt Unset Printing Coercions.}. +By default, coercions are not printed. + %%% Local Variables: %%% mode: latex %%% TeX-master: "Reference-Manual" diff --git a/doc/RefMan-gal.tex b/doc/RefMan-gal.tex index c4fba70c4..7fa478491 100644 --- a/doc/RefMan-gal.tex +++ b/doc/RefMan-gal.tex @@ -52,24 +52,28 @@ Comments in {\Coq} are enclosed between {\tt (*} and {\tt *)}\index{Comments}, and can be nested. Comments are treated as blanks. -\paragraph{Identifiers} +\paragraph{Identifiers and access identifiers} Identifiers, written {\ident}, are sequences of letters, digits, -\verb!_!, \verb!$! %$ +\verb!_! %, \verb!$! and \verb!'!, that do not start with a digit or \verb!'!. That is, they are recognized by the following lexical class: \index{ident@\ident} \begin{center} \begin{tabular}{rcl} -{\firstletter} & ::= & \ml{a..z}\op\ml{A..Z}\op\ml{\_}\op\ml{\$} \\ -{\subsequentletter} & ::= & \ml{a..z}\op\ml{A..Z}\op\ml{0..9}\op\ml{\_}\op\ml{\$}\op\ml{'} \\ +{\firstletter} & ::= & \ml{a..z}\op\ml{A..Z}\op\ml{\_}%\op\ml{\$} + \\ +{\subsequentletter} & ::= & \ml{a..z}\op\ml{A..Z}\op\ml{0..9}\op\ml{\_}%\op\ml{\$} +\op\ml{'} \\ {\ident} & ::= & {\firstletter} \sequencewithoutblank{\subsequentletter}{}\\ \end{tabular} \end{center} Identifiers can contain at most 80 characters, and all characters are meaningful. In particular, identifiers are case-sensitive. +Access identifiers, written {\accessident}, are identifiers prefixed by \verb!.! (dot). + \paragraph{Natural numbers and integers} Numerals are sequences of digits. Integers are numerals optionally preceded by a minus sign. @@ -107,7 +111,7 @@ the end of each line, just before the newline. For instance, \begin{flushleft} \begin{small} \begin{verbatim} -AddPath "/usr/local/coq/\ +Add LoadPath "/usr/local/coq/\ contrib/Rocq/LAMBDA". \end{verbatim} \end{small} @@ -115,9 +119,13 @@ contrib/Rocq/LAMBDA". is correctly parsed, and equivalent to -\begin{coq_example*} -AddPath "$COQLIB/contrib/Rocq/LAMBDA". -\end{coq_example*} +\begin{flushleft} +\begin{small} +\begin{verbatim} +Add LoadPath "/usr/local/coq/contrib/Rocq/LAMBDA". +\end{verbatim} +\end{small} +\end{flushleft} \paragraph{Keywords} The following identifiers are reserved keywords, and cannot be @@ -277,8 +285,8 @@ chapter \ref{Addoc-syntax}. \begin{figure}[htb] \begin{tabular}{|lcl|} \hline -{\term} & ::= & \ident\\ - & $|$ & \sort \\ +{\term} & ::= & {\qualid} \\ + & $|$ & {\sort} \\ & $|$ & {\term} {\tt ->} {\term} \\ & $|$ & {\tt (} {\nelist{\typedidents}{;}} {\tt )} {\term}\\ & $|$ & {\tt [} {\nelist{\localdecls}{;}} {\tt ]} {\term}\\ @@ -288,6 +296,9 @@ chapter \ref{Addoc-syntax}. & $|$ & {\tt Fix} {\ident} \verb.{. \nelist{\fixpointbody}{with} \verb.}.\\ & $|$ & {\tt CoFix} {\ident} \verb.{. \nelist{\cofixpointbody}{with} \verb.}.\\ & & \\ +{\qualid} & ::= & {\ident} \\ + & $|$ & {\qualid} {\accessident} \\ + & & \\ {\sort} & ::= & {\tt Prop} \\ & $|$ & {\tt Set} \\ & $|$ & {\tt Type} \\ @@ -317,10 +328,13 @@ chapter \ref{Addoc-syntax}. \end{figure} %%%%%%% -\subsection{Identifiers} +\subsection{Qualified identifiers and simple identifiers} -Identifiers denotes either {\em variables}, {\em constants}, -{\em inductive types} or {\em constructors of inductive types}. +{\em Qualified identifiers} ({\qualid}) denote {\em constants}, {\em inductive +types} or {\em constructors of inductive types}. +{\em Simple identifiers} (or shortly {\em identifiers}) are a +syntactic subset of qualified identifiers. Identifiers may also +denote {\em variables}, what qualified identifiers do not. \subsection{Sorts}\index{Sorts} \index{Type@{\Type}} @@ -418,7 +432,7 @@ binding of \term$_1$ to the variable $\ident$ in \term$_2$. \medskip \Rem The expression {\tt [}{\ident}{\tt :=}{\term$_1$}{\tt -:}{\type}{\tt ]}{\term$_2$} is equivalent to {\tt [}{\ident}{\tt +:}{\type}{\tt ]}{\term$_2$} is an alternative form for the expression {\tt [}{\ident}{\tt :=(}{\term$_1$}{\tt ::}{\type}{\tt )]}{\term$_2$}. \Rem An alternative equivalent syntax for let-in is {\tt let} {\ident} @@ -460,7 +474,7 @@ well-founded recursion. The expression {\tt CoFix} {\ident$_i$} \verb.{. \ident$_1$ {\tt :} {\type$_1$} {\tt with} {\ldots} {\tt with} -\ident$_n$ {\tt [} \binders$_n$ {\tt ] :} {\type$_n$} \verb.}. denotes +\ident$_n$ {\tt [} \binders$_n$ {\tt ] :} {\type$_n$}~\verb.}. denotes the $i$th component of a block of terms defined by a mutual guarded recursion. \section{\em The Vernacular} @@ -1092,7 +1106,7 @@ with forest_size [f:forest] : nat := A generic command {\tt Scheme} is useful to build automatically various mutual induction principles. It is described in section \ref{Scheme}. -\subsubsection{{\tt CoFixpoint} {\ident} : +\subsubsection{\tt CoFixpoint {\ident} : \type$_0$ := \term$_0$.}\comindex{CoFixpoint}\label{CoFixpoint} The {\tt CoFixpoint} command introduces a method for constructing an diff --git a/doc/RefMan-oth.tex b/doc/RefMan-oth.tex index eaf8d80f8..a83a2a74e 100644 --- a/doc/RefMan-oth.tex +++ b/doc/RefMan-oth.tex @@ -4,19 +4,19 @@ \section{Displaying} -\subsection{\tt Print {\ident}.}\comindex{Print} +\subsection{\tt Print {\qualid}.}\comindex{Print} This command displays on the screen informations about the declared or -defined object {\ident}. +defined object referred by {\qualid}. \begin{ErrMsgs} -\item {\ident} \errindex{not a defined object} +\item {\qualid} \errindex{not a defined object} \end{ErrMsgs} \begin{Variants} -\item {\tt Print Proof {\ident}.}\comindex{Print Proof}\\ -In case \ident\ corresponds to an opaque theorem defined in a section, +\item {\tt Print Proof {\qualid}.}\comindex{Print Proof}\\ +In case \qualid\ denotes an opaque theorem defined in a section, it is stored on a special unprintable form and displayed as -{\tt <recipe>}. {\tt Print Proof} forces the printable form of \ident\ +{\tt <recipe>}. {\tt Print Proof} forces the printable form of \qualid\ to be computed and displays it. \end{Variants} @@ -28,9 +28,9 @@ environment, including sections and modules. \item {\tt Inspect \num.}\comindex{Inspect}\\ This command displays the {\num} last objects of the current environment, including sections and modules. -% \item {\tt Print Section {\ident}.}\comindex{Print Section}\\ -% should correspond to a currently open section, this command -% displays the objects defined since the beginning of this section. +\item {\tt Print Section {\ident}.}\comindex{Print Section}\\ +should correspond to a currently open section, this command +displays the objects defined since the beginning of this section. \item {\tt Print.}\comindex{Print}\\ This command displays the axioms and variables declarations in the environment as well as the constants defined since the last variable @@ -79,15 +79,15 @@ displayed as in \Coq\ terms. \begin{Variants} \item \texttt{Recursive Extraction {\qualid$_1$} ... {\qualid$_n$}.}\\ Recursively extracts all the material needed for the extraction of - globals \qualid$_1$ ... \qualid$_n$. + globals {\qualid$_1$} ... {\qualid$_n$}. \end{Variants} \SeeAlso chapter~\ref{Extraction}. -\subsection{\tt Opaque \ident$_1$ \dots \ident$_n$.} +\subsection{\tt Opaque \qualid$_1$ \dots \qualid$_n$.} \comindex{Opaque}\label{Opaque} -This command forbids the unfolding of the constants \ident$_1$ \dots -\ident$_n$ by tactics using $\delta$-conversion. Unfolding a constant +This command forbids the unfolding of the constants {\qualid$_1$} \dots +{\qualid$_n$} by tactics using $\delta$-conversion. Unfolding a constant is replacing it by its definition. By default, {\tt Theorem} and its alternatives are stamped as {\tt @@ -101,14 +101,14 @@ values are of course relevant in general. \ref{Theorem} \begin{ErrMsgs} -\item \errindex{The reference \ident\ was not found in the current +\item \errindex{The reference \qualid\ was not found in the current environment}\\ - There is no constant in the environment named - \ident. Nevertheless, if you asked \texttt{Opaque foo bar} + There is no constant referred by {\qualid} in the environment. + Nevertheless, if you asked \texttt{Opaque foo bar} and if \texttt{bar} does not exist, \texttt{foo} is set opaque. \end{ErrMsgs} -\subsection{\tt Transparent \ident$_1$ \dots \ident$_n$.} +\subsection{\tt Transparent \qualid$_1$ \dots \qualid$_n$.} \comindex{Transparent}\label{Transparent} This command is the converse of {\tt Opaque}. By default, {\tt Definition} and {\tt Local} declare objects as {\tt Transparent}. @@ -125,10 +125,10 @@ can cause changes in tactic scripts behavior. \begin{ErrMsgs} % \item \errindex{Can not set transparent.}\\ % It is a constant from a required module or a parameter. -\item \errindex{The reference \ident\ was not found in the current +\item \errindex{The reference \qualid\ was not found in the current environment}\\ - There is no constant in the environment named - \ident. Nevertheless, if you give the command \verb|Transparent foo bar.| + There is no constant referred by {\qualid} in the environment. + Nevertheless, if you give the command \verb|Transparent foo bar.| and if \texttt{bar} does not exist, \texttt{foo} is set opaque. \end{ErrMsgs} @@ -144,7 +144,7 @@ library lemmas. \item \errindex{The reference \qualid\ was not found in the current environment}\\ There is no constant in the environment named - \ident. + \qualid. \end{ErrMsgs} \subsection{\tt SearchPattern {\term}.}\comindex{SearchPattern} @@ -336,47 +336,53 @@ its contents is invisible to the user. % ({\ident}{\tt.vo}) is searched first, then the specification file % ({\ident}{\tt.vi}) in case of failure. -\subsection{\tt Require {\ident}.} +\subsection{\tt Require {\dirpath}.} \label{Require} \comindex{Require} -This command loads and opens (imports) the module stored in the file -{\ident}{\tt .vo}. + +This command looks in the loadpath for a file containing module +{\dirpath}, then loads and opens (imports) its contents. +More precisely, if {\dirpath} splits into a library dirpath {\dirpath'} and a module name {\textsl{ident}}, then the file {\ident}{\tt .vo} is searched in a physical path mapped to the logical path {\dirpath'}. + % The implementation file ({\ident}{\tt .vo}) is searched first, % then the specification file ({\ident}{\tt .vi}) in case of failure. If the module required has already been loaded, \Coq\ -simply opens it (as {\tt Import {\ident}} would do it). -If the module required is already loaded and open, \Coq\ -displays the following warning: {\tt {\ident} already imported}. +simply opens it (as {\tt Import {\dirpath}} would do it). +%If the module required is already loaded and open, \Coq\ +%displays the following warning: {\tt {\ident} already imported}. If a module {\it A} contains a command {\tt Require} {\it B} then the command {\tt Require} {\it A} loads the module {\it B} but does not open it (See the {\tt Require Export} variant below). \begin{Variants} -\item {\tt Require Export {\ident}.}\\ +\item {\tt Require Export {\qualid}.}\\ \comindex{Require Export} - This command acts as {\tt Require} {\ident}. But if a module {\it + This command acts as {\tt Require} {\qualid}. But if a module {\it A} contains a command {\tt Require Export} {\it B}, then the command {\tt Require} {\it A} opens the module {\it B} as if the user would have typed {\tt Require}{\it B}. -% \item {\tt Require $[$ Implementation $|$ Specification $]$ {\ident}.}\\ +% \item {\tt Require $[$ Implementation $|$ Specification $]$ {\qualid}.}\\ % \comindex{Require Implementation} % \comindex{Require Specification} % Is the same as {\tt Require}, but specifying explicitly the % implementation ({\tt.vo} file) or the specification ({\tt.vi} % file). -\item {\tt Require {\ident} {\str}.}\\ - Specifies the file to load as being {\str}, instead of - {\ident}. The opened module is still {\ident} and therefore - must have been loaded. -\item {\tt Require {\ident} {\str}.}\\ - Specifies the file to load as being {\str}, instead of - {\ident}. The opened module is still {\ident}. + +% Redundant ? +% \item {\tt Require {\qualid} {\str}.}\\ +% Specifies the file to load as being {\str} but containing module +% {\qualid}. +% The opened module is still {\ident} and therefore must have been loaded. +\item {\tt Require {\qualid} {\str}.}\\ + Specifies the file to load as being {\str} but containing module + {\qualid} which is then opened. \end{Variants} These different variants can be combined. \begin{ErrMsgs} +\item \errindex{Cannot load {\ident}: no physical path bound to {\dirpath}}\\ \item \errindex{Can't find module toto on loadpath}\\ The command did not find the file {\tt toto.vo}. Either {\tt toto.v} exists but is not compiled or {\tt toto.vo} is in a directory @@ -438,14 +444,27 @@ which can be any valid path. Is equivalent to {\tt Pwd.} \end{Variants} -\subsection{\tt AddPath {\str}.}\comindex{AddPath} -This command adds the path {\str} to the current \Coq\ loadpath. +\subsection{\tt Add LoadPath {\str} as {\dirpath}.}\comindex{Add LoadPath} +This command adds the path {\str} to the current \Coq\ loadpath and +maps it to the logical directory {\dirpath}, which means that every +file {\tt M.v} physically lying in directory {\str} will be considered +as a module of logical name ``{\dirpath}{\tt{.M}}''. + +\begin{Variants} +\item {\tt Add LoadPath {\str}.}\\ +Performs as {\tt Add LoadPath {\str} as {\dirpath}.} but for an empty directory path. +\end{Variants} -\subsection{\tt AddRecPath {\str}.}\comindex{AddRecPath} +\subsection{\tt Add Rec LoadPath {\str} as {\dirpath}.}\comindex{Add Rec LoadPath} This command adds the directory {\str} and all its subdirectories -to the current \Coq\ loadpath. +to the current \Coq\ loadpath. The top directory {\str} is mapped to the logical directory {\dirpath}, any subdirectory {\textsl{pdir}} will be mapped to logical directory {\dirpath}{\tt{.pdir}} and so on. -\subsection{\tt DelPath {\str}.}\comindex{DelPath} +\begin{Variants} +\item {\tt Add Rec LoadPath {\str}.}\\ +Works as {\tt Add Rec LoadPath {\str} as {\dirpath}.} but for the empty logical directory path. +\end{Variants} + +\subsection{\tt Remove LoadPath {\str}.}\comindex{Remove LoadPath} This command removes the path {\str} from the current \Coq\ loadpath. \subsection{\tt Print LoadPath.}\comindex{Print LoadPath} @@ -455,11 +474,15 @@ This command displays the current \Coq\ loadpath. This command adds the path {\str} to the current Objective Caml loadpath (see the command {\tt Declare ML Module} in the section \ref{compiled}). +\Rem This command is implied by {\tt Add LoadPath {\str} as {\dirpath}}. + \subsection{\tt Add Rec ML Path {\str}.}\comindex{Add Rec ML Path} This command adds the directory {\str} and all its subdirectories to the current Objective Caml loadpath (see the command {\tt Declare ML Module} in the section \ref{compiled}). +\Rem This command is implied by {\tt Add Rec LoadPath {\str} as {\dirpath}}. + \subsection{\tt Print ML Path {\str}.}\comindex{Print ML Path} This command displays the current Objective Caml loadpath. This command makes sense only under the bytecode version of {\tt @@ -472,15 +495,22 @@ command {\tt Declare ML Module} in the section This command displays the location of file {\str} in the current loadpath. Typically, {\str} is a \texttt{.cmo} or \texttt{.vo} or \texttt{.v} file. -\subsection{\tt Locate Library {\ident}.} +\subsection{\tt Locate Library {\dirpath}.} \comindex{Locate Library} -This command displays the location of the \Coq\ module {\ident} in the current -loadpath. Is is equivalent to {\tt Locate File "}{\ident}{\tt .vo".} +This command gives the status of the \Coq\ module {\dirpath}. If the module is loaded, then it is told. Otherwise, a file containing a module of this logical name is searched in the loadpath. -\subsection{\tt Locate {\ident}.}\comindex{Locate} -This command displays the full name of the identifier {\ident} +\subsection{\tt Locate {\qualid}.}\comindex{Locate} +This command displays the full name of the qualified identifier {\qualid} and consequently the \Coq\ module in which it is defined. +\begin{coq_example} +Locate nat. +Locate Datatypes.O. +Locate Init.Datatypes.O. +Locate Coq.Init.Datatypes.O. +Locate I.Dont.Exist. +\end{coq_example} + \section{States and Reset} \subsection{\tt Reset \ident.} @@ -570,17 +600,17 @@ who programs his own tactics. \SeeAlso chapters \ref{Addoc-syntax} -\subsection{\tt{Infix} {\num} {\str} {\ident}.}\comindex{Infix} +\subsection{\tt{Infix} {\num} {\str} {\qualid}.}\comindex{Infix} -This command declares a prefix operator {\ident} as infix, with the +This command declares the prefix operator denoted by {\qualid} as infix, with the syntax {\term} {\str} {\term}. {\num} is the precedence associated to the operator; it must lie between 1 and 10. The infix operator \str\ associates to the left. {\str} must be a legal token. Both grammar and pretty-print rules are automatically generated for {\str}. \begin{Variants} -\item \texttt{Infix {\rm\sl assoc} {\num} {\str} {\ident}.} \\ - Declares {\ident} as an infix operator with an alternate +\item \texttt{Infix {\rm\sl assoc} {\num} {\str} {\qualid}.} \\ + Declares the full names denoted by {\qualid} as an infix operator with an alternate associativity. {\rm\sl assoc} may be one of {\tt LEFTA}, {\tt RIGHTA} and {\tt NONA}. The default is {\tt LEFTA}. When an associativity is given, the precedence level must lie between 6 and @@ -611,7 +641,7 @@ Objective Caml toplevel. The Objective Caml command: all abstract types of \Coq - section\_path, identfifiers, terms, judgements, \dots. You can also use the file \texttt{base\_include} instead, that loads only the pretty-printers for section\_paths and -identfifiers. +identifiers. % See section \ref{test-and-debug} more information on the % usage of the toplevel. You can return back to \Coq{} with the command: diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex index 119792f11..05ba99764 100644 --- a/doc/RefMan-tac.tex +++ b/doc/RefMan-tac.tex @@ -582,14 +582,16 @@ These parameterized reduction tactics apply to any goal and perform the normalization of the goal according to the specified flags. Since the reduction considered in \Coq\ include $\beta$ (reduction of functional application), $\delta$ (unfolding -of transparent constants, see \ref{Transparent}) -and $\iota$ (reduction of {\tt Cases}, {\tt Fix} and {\tt -CoFix} expressions), every flag is one of {\tt Beta}, {\tt Delta}, -{\tt Iota}, {\tt [\ident$_1$\ldots\ident$_k$]} and -{\tt -[\ident$_1$\ldots\ident$_k$]}. +of transparent constants, see \ref{Transparent}), +$\iota$ (reduction of {\tt Cases}, {\tt Fix} and {\tt +CoFix} expressions) and $\zeta$ (removal of local definitions), every flag is one of {\tt Beta}, {\tt Delta}, +{\tt Iota}, {\tt Zeta}, {\tt [\qualid$_1$\ldots\qualid$_k$]} and +{\tt -[\qualid$_1$\ldots\qualid$_k$]}. The last two flags give the list of constants to unfold, or the list of constants not to unfold. These two -flags can occur only after the {\tt Delta} flag. The goal may be +flags can occur only after the {\tt Delta} flag. +In addition, there is a flag {\tt Evar} to perform instantiation of exitential variables (``?'') when an instantiation actually exists. +The goal may be normalized with two strategies: {\em lazy} ({\tt Lazy} tactic), or {\em call-by-value} ({\tt Cbv} tactic). @@ -613,7 +615,7 @@ computational expressions (i.e. with few dead code). \begin{Variants} \item {\tt Compute}\\ \tacindex{Compute} - This tactic is an alias for {\tt Cbv Beta Delta Iota}. + This tactic is an alias for {\tt Cbv Beta Delta Evar Iota Zeta}. \end{Variants} \begin{ErrMsgs} @@ -657,35 +659,35 @@ $\beta\iota$ rules. But when the $\iota$ rule is not applicable then possible $\delta$-reductions are not applied. For instance trying to use {\tt Simpl} on {\tt (plus n O)=n} will change nothing. -\subsection{\tt Unfold \ident} +\subsection{\tt Unfold \qualid} \tacindex{Unfold}\label{Unfold} -This tactic applies to any goal. The argument {\ident} must be the -name of a defined transparent constant or local definition (see section +This tactic applies to any goal. The argument {\qualid} must denote +a defined transparent constant or local definition (see section \ref{Simpl-definitions} and \ref{Transparent}). The tactic {\tt Unfold} applies the -$\delta$ rule to each occurrence of {\ident} in the current goal and +$\delta$ rule to each occurrence of the constant to which {\qualid} refers + in the current goal and then replaces it with its $\beta\iota$-normal form. -\Warning If the constant is opaque, nothing will happen and no warning +\begin{ErrMsgs} +\item {\qualid} \errindex{does not denote an evaluable constant} is printed. -\begin{ErrMsgs} -\item {\ident} \errindex{does not denote an evaluable constant} \end{ErrMsgs} \begin{Variants} -\item {\tt Unfold {\ident}$_1$ \dots\ \ident$_n$}\\ +\item {\tt Unfold {\qualid}$_1$ \dots\ \qualid$_n$}\\ \tacindex{Unfold \dots\ in} - Replaces {\em simultaneously} {\ident}$_1$, \dots, {\ident}$_n$ with + Replaces {\em simultaneously} {\qualid}$_1$, \dots, {\qualid}$_n$ with their definitions and replaces the current goal with its $\beta\iota$ normal form. -\item {\tt Unfold \num$_1^1$ \dots\ \num$_i^1$ {\ident}$_1$ \dots\ \num$_1^n$ - \dots\ \num$_j^n$ \ident$_n$}\\ +\item {\tt Unfold \num$_1^1$ \dots\ \num$_i^1$ {\qualid}$_1$ \dots\ \num$_1^n$ + \dots\ \num$_j^n$ \qualid$_n$}\\ The lists \num$_1^1$, \dots, \num$_i^1$ and \num$_1^n$, \dots, \num$_j^n$ - are to specify the occurrences of {\ident}$_1$, \dots, \ident$_n$ to be + are to specify the occurrences of {\qualid}$_1$, \dots, \qualid$_n$ to be unfolded. Occurrences are located from left to right in the linear notation of terms.\\ - \ErrMsg {\tt bad occurrence numbers of {\ident}$_i$} + \ErrMsg {\tt bad occurrence numbers of {\qualid}$_i$} \end{Variants} \subsection{{\tt Fold} \term} @@ -1923,8 +1925,8 @@ a hint to a database is: \item {\ident} \errindex{not declared} \end{ErrMsgs} -\item \texttt{Unfold} {\ident}\index[command]{Hint!Unfold}\\ - This adds the tactic {\tt Unfold {\ident}} to the hint list +\item \texttt{Unfold} {\qualid}\index[command]{Hint!Unfold}\\ + This adds the tactic {\tt Unfold {\qualid}} to the hint list that will only be used when the head constant of the goal is \ident. Its cost is 4. @@ -2003,7 +2005,7 @@ There are shortcuts that allow to define several goal at once: Notice that the hint name is the same that the theorem given as hint. \item \comindex{Hints Immediate}\texttt{Hints Immediate \ident$_1$ \dots\ \ident$_n$ : \ident.}\\ -\item \comindex{Hints Unfold}\texttt{Hints Unfold \ident$_1$ \dots\ \ident$_n$ : \ident.}\\ +\item \comindex{Hints Unfold}\texttt{Hints Unfold \qualid$_1$ \dots\ \qualid$_n$ : \ident.}\\ \end{itemize} %\begin{Warnings} diff --git a/doc/macros.tex b/doc/macros.tex index 3ff8fb6d9..f60cef26e 100755 --- a/doc/macros.tex +++ b/doc/macros.tex @@ -115,6 +115,7 @@ \newcommand{\localdef}{\textrm{\textsl{local\_def}}} \newcommand{\localdecls}{\textrm{\textsl{local\_decls}}} \newcommand{\ident}{\textrm{\textsl{ident}}} +\newcommand{\accessident}{\textrm{\textsl{access\_ident}}} \newcommand{\inductivebody}{\textrm{\textsl{ind\_body}}} \newcommand{\inductive}{\textrm{\textsl{inductive}}} \newcommand{\integer}{\textrm{\textsl{integer}}} @@ -144,6 +145,7 @@ \newcommand{\term}{\textrm{\textsl{term}}} \newcommand{\module}{\textrm{\textsl{module}}} \newcommand{\qualid}{\textrm{\textsl{qualid}}} +\newcommand{\dirpath}{\textrm{\textsl{qualid}}} \newcommand{\typedidents}{\textrm{\textsl{typed\_idents}}} \newcommand{\type}{\textrm{\textsl{type}}} \newcommand{\vref}{\textrm{\textsl{ref}}} |