diff options
Diffstat (limited to 'doc/refman/RefMan-ltac.tex')
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 262 |
1 files changed, 228 insertions, 34 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index de9897c4..e7400232 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -103,16 +103,23 @@ is understood as {\tt match reverse goal with} \nelist{\contextrule}{\tt |} {\tt end}\\ & | & {\tt match} {\tacexpr} {\tt with} \nelist{\matchrule}{\tt |} {\tt end}\\ +& | & +{\tt lazymatch goal with} \nelist{\contextrule}{\tt |} {\tt end}\\ +& | & +{\tt lazymatch reverse goal with} \nelist{\contextrule}{\tt |} {\tt end}\\ +& | & +{\tt lazymatch} {\tacexpr} {\tt with} \nelist{\matchrule}{\tt |} {\tt end}\\ & | & {\tt abstract} {\atom}\\ & | & {\tt abstract} {\atom} {\tt using} {\ident} \\ & | & {\tt first [} \nelist{\tacexpr}{\tt |} {\tt ]}\\ & | & {\tt solve [} \nelist{\tacexpr}{\tt |} {\tt ]}\\ -& | & {\tt idtac} ~|~ {\tt idtac} {\qstring}\\ -& | & {\tt fail} ~|~ {\tt fail} {\naturalnumber} {\qstring}\\ +& | & {\tt idtac} \sequence{\messagetoken}{}\\ +& | & {\tt fail} \zeroone{\naturalnumber} \sequence{\messagetoken}{}\\ & | & {\tt fresh} ~|~ {\tt fresh} {\qstring}\\ & | & {\tt context} {\ident} {\tt [} {\term} {\tt ]}\\ & | & {\tt eval} {\nterm{redexpr}} {\tt in} {\term}\\ & | & {\tt type of} {\term}\\ +& | & {\tt external} {\qstring} {\qstring} \nelist{\tacarg}{}\\ & | & {\tt constr :} {\term}\\ & | & \atomictac\\ & | & {\qualid} \nelist{\tacarg}{}\\ @@ -122,6 +129,8 @@ is understood as {\qualid} \\ & | & ()\\ & | & {\tt (} {\tacexpr} {\tt )}\\ +\\ +{\messagetoken}\!\!\!\!\!\! & ::= & {\qstring} ~|~ {\term} ~|~ {\integer} \\ \end{tabular} \end{centerframe} \caption{Syntax of the tactic language} @@ -266,6 +275,12 @@ applied and $v_i$ is applied to the $i$-th generated subgoal by the application of $v_0$, for $=1,...,n$. It fails if the application of $v_0$ does not generate exactly $n$ subgoals. +\variant If no tactic is given for the $i$-th generated subgoal, it +behaves as if the tactic {\tt idtac} were given. For instance, {\tt +split ; [ | auto ]} is a shortcut for +{\tt split ; [ idtac | auto ]}. + + \subsubsection{For loop} \tacindex{do} \index{Tacticals!do@{\tt do}} @@ -369,10 +384,13 @@ tries to apply $v_2$ and so on. It fails if there is no solving tactic. The constant {\tt idtac} is the identity tactic: it leaves any goal unchanged but it appears in the proof script. -\begin{quote} -{\tt idtac} and {\tt idtac "message"} -\end{quote} -The latter variant prints the string on the standard output. + +\variant {\tt idtac \nelist{\messagetoken}{}} + +This prints the given tokens. Strings and integers are printed +literally. If a term is given, it is printed, its variables being +interpreted in the current environment. In particular, if a variable +is given, its value is printed. \subsubsection{Failing} @@ -381,17 +399,24 @@ The latter variant prints the string on the standard output. The tactic {\tt fail} is the always-failing tactic: it does not solve any goal. It is useful for defining other tacticals since it can be -catched by {\tt try} or {\tt match goal}. There are three variants: -\begin{quote} -{\tt fail $n$}, {\tt fail "message"} and {\tt fail $n$ "message"} -\end{quote} +catched by {\tt try} or {\tt match goal}. + +\begin{Variants} +\item {\tt fail $n$}\\ The number $n$ is the failure level. If no level is specified, it defaults to $0$. The level is used by {\tt try} and {\tt match goal}. If $0$, it makes {\tt match goal} considering the next clause (backtracking). If non zero, the current {\tt match goal} block or {\tt try} command is aborted and the level is decremented. -\ErrMsg \errindex{Tactic Failure "message" (level $n$)}. +\item {\tt fail \nelist{\messagetoken}{}}\\ +The given tokens are used for printing the failure message. + +\item {\tt fail $n$ \nelist{\messagetoken}{}}\\ +This is a combination of the previous variants. +\end{Variants} + +\ErrMsg \errindex{Tactic Failure {\it message} (level $n$)}. \subsubsection{Local definitions} \index{Ltac!let} @@ -464,10 +489,13 @@ The {\tacexpr} is evaluated and should yield a term which is matched pattern matching instantiations to the metavariables. If the matching with {\cpattern}$_1$ fails, {\cpattern}$_2$ is used and so on. The pattern {\_} matches any term and shunts all remaining patterns if -any. If {\tacexpr}$_1$ evaluates to a tactic, this tactic is not -immediately applied to the current goal (in contrast with {\tt match -goal}). If all clauses fail (in particular, there is no pattern {\_}) -then a no-matching error is raised. +any. If {\tacexpr}$_1$ evaluates to a tactic and the {\tt match} +expression is in position to be applied to a goal (e.g. it is not +bound to a variable by a {\tt let in}, then this tactic is applied. If +the tactic succeeds, the list of resulting subgoals is the result of +the {\tt match} expression. On the opposite, if it fails, the next +pattern is tried. If all clauses fail (in particular, there is no +pattern {\_}) then a no-matching error is raised. \begin{ErrMsgs} @@ -481,7 +509,8 @@ then a no-matching error is raised. \end{ErrMsgs} -\index{context!in pattern} +\begin{Variants} +\item \index{context!in pattern} There is a special form of patterns to match a subterm against the pattern: \begin{quote} @@ -493,11 +522,36 @@ is the initial term where the matched subterm is replaced by a hole. The definition of {\tt context} in expressions below will show how to use such term contexts. -This operator never makes backtracking. If there are several subterms -matching the pattern, only the first match is considered. Note that -the order of matching is left unspecified. -%% TODO: clarify this point! It *should* be specified +If the evaluation of the right-hand-side of a valid match fails, the +next matching subterm is tried. If no further subterm matches, the +next clause is tried. Matching subterms are considered top-bottom and +from left to right (with respect to the raw printing obtained by +setting option {\tt Printing All}, see section~\ref{SetPrintingAll}). + +\begin{coq_example} +Ltac f x := + match x with + context f [S ?X] => + idtac X; (* To display the evaluation order *) + assert (p := refl_equal 1 : X=1); (* To filter the case X=1 *) + let x:= context f[O] in assert (x=O) (* To observe the context *) + end. +Goal True. +f (3+4). +\end{coq_example} + +\item \index{lazymatch!in Ltac} +\index{Ltac!lazymatch} +Using {\tt lazymatch} instead of {\tt match} has an effect if the +right-hand-side of a clause returns a tactic. With {\tt match}, the +tactic is applied to the current goal (and the next clause is tried if +it fails). With {\tt lazymatch}, the tactic is directly returned as +the result of the whole {\tt lazymatch} block without being first +tried to be applied to the goal. Typically, if the {\tt lazymatch} +block is bound to some variable $x$ in a {\tt let in}, then tactic +expression gets bound to the variable $x$. +\end{Variants} \subsubsection{Pattern matching on goals} \index{Ltac!match goal} @@ -521,8 +575,6 @@ We can make pattern matching on goals using the following expression: \end{tabbing} \end{quote} -% TODO: specify order of hypothesis and explain reverse... - If each hypothesis pattern $hyp_{1,i}$, with $i=1,...,m_1$ is matched (non-linear first order unification) by an hypothesis of the goal and if {\cpattern}$_1$ is matched by the conclusion of the @@ -535,7 +587,9 @@ hypotheses is tried with the same proof context pattern. If there is no other combination of hypotheses then the second proof context pattern is tried and so on. If the next to last proof context pattern fails then {\tacexpr}$_{n+1}$ is evaluated to $v_{n+1}$ and $v_{n+1}$ -is applied. +is applied. Note also that matching against subterms (using the {\tt +context} {\ident} {\tt [} {\cpattern} {\tt ]}) is available and may +itself induce extra backtrackings. \ErrMsg \errindex{No matching clauses for match goal} @@ -552,6 +606,36 @@ pattern, the goal hypothesis are matched in order (fresher hypothesis first), but it possible to reverse this order (older first) with the {\tt match reverse goal with} variant. +\variant +\index{lazymatch goal!in Ltac} +\index{Ltac!lazymatch goal} +\index{lazymatch reverse goal!in Ltac} +\index{Ltac!lazymatch reverse goal} +Using {\tt lazymatch} instead of {\tt match} has an effect if the +right-hand-side of a clause returns a tactic. With {\tt match}, the +tactic is applied to the current goal (and the next clause is tried if +it fails). With {\tt lazymatch}, the tactic is directly returned as +the result of the whole {\tt lazymatch} block without being first +tried to be applied to the goal. Typically, if the {\tt lazymatch} +block is bound to some variable $x$ in a {\tt let in}, then tactic +expression gets bound to the variable $x$. + +\begin{coq_example} +Ltac test_lazy := + lazymatch goal with + | _ => idtac "here"; fail + | _ => idtac "wasn't lazy"; trivial + end. +Ltac test_eager := + match goal with + | _ => idtac "here"; fail + | _ => idtac "wasn't lazy"; trivial + end. +Goal True. +test_lazy || idtac "was lazy". +test_eager || idtac "was lazy". +\end{coq_example} + \subsubsection{Filling a term context} \index{context!in expression} @@ -585,13 +669,6 @@ It evaluates to an identifier unbound in the goal, which is obtained by padding {\qstring} with a number if necessary. If no name is given, the prefix is {\tt H}. -\subsubsection{{\tt type of} {\term}} -%\tacindex{type of} -\index{Ltac!type of} -\index{type of!in Ltac} - -This tactic computes the type of {\term}. - \subsubsection{Computing in a constr} \index{Ltac!eval} \index{eval!in Ltac} @@ -604,6 +681,16 @@ where \nterm{redexpr} is a reduction tactic among {\tt red}, {\tt hnf}, {\tt compute}, {\tt simpl}, {\tt cbv}, {\tt lazy}, {\tt unfold}, {\tt fold}, {\tt pattern}. +\subsubsection{Type-checking a term} +%\tacindex{type of} +\index{Ltac!type of} +\index{type of!in Ltac} + +The following returns the type of {\term}: + +\begin{quote} +{\tt type of} {\term} +\end{quote} \subsubsection{Accessing tactic decomposition} \tacindex{info} @@ -635,10 +722,76 @@ without having to cut manually the proof in smaller lemmas. \ErrMsg \errindex{Proof is not complete} +\subsubsection{Calling an external tactic} +\index{Ltac!external} + +The tactic {\tt external} allows to run an executable outside the +{\Coq} executable. The communication is done via an XML encoding of +constructions. The syntax of the command is + +\begin{quote} +{\tt external} "\textsl{command}" "\textsl{request}" \nelist{\tacarg}{} +\end{quote} + +The string \textsl{command}, to be interpreted in the default +execution path of the operating system, is the name of the external +command. The string \textsl{request} is the name of a request to be +sent to the external command. Finally the list of tactic arguments +have to evaluate to terms. An XML tree of the following form is sent +to the standard input of the external command. +\medskip + +\begin{tabular}{l} +\texttt{<REQUEST req="}\textsl{request}\texttt{">}\\ +the XML tree of the first argument\\ +{\ldots}\\ +the XML tree of the last argument\\ +\texttt{</REQUEST>}\\ +\end{tabular} +\medskip + +Conversely, the external command must send on its standard output an +XML tree of the following forms: + +\medskip +\begin{tabular}{l} +\texttt{<TERM>}\\ +the XML tree of a term\\ +\texttt{</TERM>}\\ +\end{tabular} +\medskip + +\noindent or + +\medskip +\begin{tabular}{l} +\texttt{<CALL uri="}\textsl{ltac\_qualified\_ident}\texttt{">}\\ +the XML tree of a first argument\\ +{\ldots}\\ +the XML tree of a last argument\\ +\texttt{</CALL>}\\ +\end{tabular} + +\medskip +\noindent where \textsl{ltac\_qualified\_ident} is the name of a +defined {\ltac} function and each subsequent XML tree is recursively a +\texttt{CALL} or a \texttt{TERM} node. + +The Document Type Definition (DTD) for terms of the Calculus of +Inductive Constructions is the one developed as part of the MoWGLI +European project. It can be found in the file {\tt dev/doc/cic.dtd} of +the {\Coq} source archive. + +An example of parser for this DTD, written in the Objective Caml - +Camlp4 language, can be found in the file {\tt parsing/g\_xml.ml4} of +the {\Coq} source archive. + \section{Tactic toplevel definitions} \comindex{Ltac} -Basically, tactics toplevel definitions are made as follows: +\subsection{Defining {\ltac} functions} + +Basically, {\ltac} toplevel definitions are made as follows: %{\tt Tactic Definition} {\ident} {\tt :=} {\tacexpr}\\ % %{\tacexpr} is evaluated to $v$ and $v$ is associated to {\ident}. Next, every @@ -649,8 +802,8 @@ Basically, tactics toplevel definitions are made as follows: {\tt Ltac} {\ident} {\ident}$_1$ ... {\ident}$_n$ {\tt :=} {\tacexpr} \end{quote} -This defines a new tactic that can be used in any tactic script or new -tactic toplevel definition. +This defines a new {\ltac} function that can be used in any tactic +script or new {\ltac} toplevel definition. \Rem The preceding definition can equivalently be written: \begin{quote} @@ -674,8 +827,49 @@ possible with the syntax: %usual except that the substitutions are lazily carried out (when an identifier %to be evaluated is the name of a recursive definition). -\endinput +\subsection{Printing {\ltac} tactics} +\comindex{Print Ltac} + +Defined {\ltac} functions can be displayed using the command + +\begin{quote} +{\tt Print Ltac {\qualid}.} +\end{quote} + +\section{Debugging {\ltac} tactics} +\comindex{Set Ltac Debug} +\comindex{Unset Ltac Debug} +\comindex{Test Ltac Debug} + +The {\ltac} interpreter comes with a step-by-step debugger. The +debugger can be activated using the command + +\begin{quote} +{\tt Set Ltac Debug.} +\end{quote} + +\noindent and deactivated using the command + +\begin{quote} +{\tt Unset Ltac Debug.} +\end{quote} + +To know if the debugger is on, use the command \texttt{Test Ltac Debug}. +When the debugger is activated, it stops at every step of the +evaluation of the current {\ltac} expression and it prints information +on what it is doing. The debugger stops, prompting for a command which +can be one of the following: + +\medskip +\begin{tabular}{ll} +simple newline: & go to the next step\\ +h: & get help\\ +x: & exit current evaluation\\ +s: & continue current evaluation without stopping\\ +r$n$: & advance $n$ steps further\\ +\end{tabular} +\endinput \subsection{Permutation on closed lists} |