Ajout section sur TACTIC EXTEND

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

1 files changed, 225 insertions, 0 deletions

diff --git a/doc/RefMan-tus.tex b/doc/RefMan-tus.tex
index e4867bf243..d296c0b47b 100755
--- a/doc/RefMan-tus.tex
+++ b/doc/RefMan-tus.tex
@@ -1786,5 +1786,230 @@ Finally, the traditional \ocaml{} debugging tools like the directives
 execution of your functions. Frequently, a better solution is to use
 the \ocaml{} debugger, see Chapter \ref{Utilities}.
 
+\section{Concrete syntax for ML tactic and vernacular command}
+\label{Notations-for-ML-command}
+
+\subsection{The general case}
+
+The standard way to bind an ML-written tactic or vernacular command to
+a concrete {\Coq} syntax is to use the
+\verb=TACTIC EXTEND= and \verb=VERNAC COMMAND EXTEND= macros.
+
+These macros can be used in any {\ocaml} file defining a (new) ML tactic
+or vernacular command. They are expanded into pure {\ocaml} code by
+the {\camlpppp} preprocessor of {\ocaml}. Concretely, files that use
+these macros need to be compiled by giving to {\tt ocamlc} the option 
+
+\verb=-pp "camlp4o -I $(COQTOP)/parsing grammar.cma pa_extend.cmo"=
+
+\noindent which is the default for every file compiled by means of a Makefile
+generated by {\tt coq\_makefile} (cf chapter \ref {Addoc-coqc}). So,
+just do \verb=make= in this latter case.
+
+The syntax of the macros is given on figure
+\ref{EXTEND-syntax}. They can be used at any place of an {\ocaml}
+files where an ML sentence (called \verb=str_item= in the {\tt ocamlc}
+parser) is expected. For each rule, the left-hand-side describes the
+grammar production and the right-hand-side its interpretation which
+must be an {\ocaml} expression. Each grammar production starts with
+the concrete name of the tactic or command in {\Coq} and is followed
+by arguments, possibly separated by terminal symbols or words.
+Here is an example:
+
+\begin{verbatim}
+TACTIC EXTEND Replace
+  [ "replace" constr(c1) "with" constr(c2) ] -> [ replace c1 c2 ]
+END
+\end{verbatim}
+
+\newcommand{\grule}{\textrm{\textsl{rule}}}
+\newcommand{\stritem}{\textrm{\textsl{ocaml\_str\_item}}}
+\newcommand{\camlexpr}{\textrm{\textsl{ocaml\_expr}}}
+\newcommand{\arginfo}{\textrm{\textsl{argument\_infos}}}
+\newcommand{\lident}{\textrm{\textsl{lower\_ident}}}
+\newcommand{\argument}{\textrm{\textsl{argument}}}
+\newcommand{\entry}{\textrm{\textsl{entry}}}
+\newcommand{\argtype}{\textrm{\textsl{argtype}}}
+
+\begin{figure}
+\begin{tabular}{|lcll|}
+\hline
+{\stritem}
+ & ::= & 
+\multicolumn{2}{l|}{{\tt TACTIC EXTEND} {\ident} \nelist{\grule}{$|$} {\tt END}}\\
+ & $|$ & \multicolumn{2}{l|}{{\tt VERNAC COMMAND EXTEND} {\ident} \nelist{\grule}{$|$} {\tt END}}\\
+&&\multicolumn{2}{l|}{}\\
+{\grule} & ::= & 
+\multicolumn{2}{l|}{{\tt [} {\str} \sequence{\argument}{} {\tt ] -> [} {\camlexpr} {\tt ]}}\\
+&&\multicolumn{2}{l|}{}\\
+{\argument} & ::= & {\str} &\mbox{(terminal)}\\
+ & $|$ & {\entry} {\tt (} {\lident} {\tt )} &\mbox{(non-terminal)}\\
+&&\multicolumn{2}{l|}{}\\
+{\entry} 
+ & ::= & {\tt string} & (a string)\\
+ & $|$ & {\tt preident} & (an identifier typed as a {\tt string})\\
+ & $|$ & {\tt ident} & (an identifier of type {\tt identifier})\\
+ & $|$ & {\tt global} & (a qualified identifier)\\
+ & $|$ & {\tt constr} & (a {\Coq} term)\\
+ & $|$ & {\tt openconstr} & (a {\Coq} term with holes)\\
+ & $|$ & {\tt sort} & (a {\Coq} sort)\\
+ & $|$ & {\tt tactic} & (an ${\cal L}_{tac}$ expression)\\
+ & $|$ & {\tt constr\_with\_bindings} & (a {\Coq} term with a list of bindings\footnote{as for the tactics {\tt apply} and {\tt elim}})\\
+ & $|$ & {\tt int\_or\_var} & (an integer or an identifier denoting an integer)\\
+ & $|$ & {\tt quantified\_hypothesis} & (a quantified hypothesis\footnote{as for the tactics {\tt intros until}})\\
+ & $|$ & {\tt {\entry}\_opt} & (an optional {\entry} )\\
+ & $|$ & {\tt ne\_{\entry}\_list} & (a non empty list of {\entry})\\
+ & $|$ & {\tt {\entry}\_list} & (a list of {\entry})\\
+ & $|$ & {\tt bool} & (a boolean: no grammar rule, just for typing)\\
+ & $|$ & {\lident} & (a user-defined entry)\\
+\hline
+\end{tabular}
+\caption{Syntax of the macros binding {\ocaml} tactics or commands to a {\Coq} syntax}
+\label{EXTEND-syntax}
+\end{figure}
+
+There is a set of predefined non-terminal entries which are
+automatically translated into an {\ocaml} object of a given type. The
+type is not the same for tactics and for vernacular commands. It is
+given in the following table:
+
+\begin{small}
+\noindent \begin{tabular}{|l|l|l|}
+\hline
+{\entry} & {\it type for tactics} & {\it type for commands} \\
+{\tt string} & {\tt string} & {\tt string}\\
+{\tt preident} & {\tt string} & {\tt string}\\
+{\tt ident} & {\tt identifier} & {\tt identifier}\\
+{\tt global} & {\tt global\_reference} & {\tt qualid}\\
+{\tt constr} & {\tt constr} & {\tt constr\_expr}\\
+{\tt openconstr} & {\tt open\_constr} & {\tt constr\_expr}\\
+{\tt sort} & {\tt sorts} & {\tt rawsort}\\
+{\tt tactic} & {\tt glob\_tactic\_expr * tactic} & {\tt raw\_tactic\_expr}\\
+{\tt constr\_with\_bindings} & {\tt constr with\_bindings} & {\tt constr\_expr with\_bindings}\\\\
+{\tt int\_or\_var} & {\tt int or\_var} & {\tt int or\_var}\\
+{\tt quantified\_hypothesis} & {\tt quantified\_hypothesis} & {\tt quantified\_hypothesis}\\
+{\tt {\entry}\_opt} & {\it the type of entry} {\tt option} & {\it the type of entry} {\tt option}\\
+{\tt ne\_{\entry}\_list} & {\it the type of entry} {\tt list} & {\it the type of entry} {\tt list}\\
+{\tt {\entry}\_list} & {\it the type of entry} {\tt list} & {\it the type of entry} {\tt list}\\
+{\tt bool} & {\tt bool} & {\tt bool}\\
+{\lident} & {user-provided, cf next section} & {user-provided, cf next section}\\
+\hline
+\end{tabular}
+\end{small}
+
+\bigskip
+
+Notice that {\entry} consists in a single identifier and that the {\tt
+\_opt}, {\tt \_list}, ... modifiers are part of the identifier.
+Here is now another example of a tactic which takes either a non empty
+list of identifiers and executes the {\ocaml} function {\tt subst} or
+takes no arguments and executes the{\ocaml} function {\tt subst\_all}.
+
+\begin{verbatim}
+TACTIC EXTEND Subst
+| [ "subst" ne_ident_list(l) ] -> [ subst l ]
+| [ "subst" ] -> [ subst_all ]
+END
+\end{verbatim}
+
+\subsection{Adding grammar entries for tactic or command arguments}
+
+In case parsing the arguments of the tactic or the vernacular command
+involves grammar entries other than the predefined entries listed
+above, you have to declare a new entry using the macros
+\verb=ARGUMENT EXTEND= or \verb=VERNAC ARGUMENT EXTEND=. The syntax is
+given on figure \ref{ARGUMENT-EXTEND-syntax}. Notice that arguments
+declared by \verb=ARGUMENT EXTEND= can be used for arguments of both
+tactics and vernacular commands while arguments declared by
+\verb=VERNAC ARGUMENT EXTEND= can only be used by vernacular commands.
+
+For \verb=VERNAC ARGUMENT EXTEND=, the identifier is the name of the
+entry and it must be a valid {\ocaml} identifier (especially it must
+be lowercase).  The grammar rules works as before except that they do
+not have to start by a terminal symbol or word.  As an example, here
+is how the {\Coq} {\tt Extraction Language {\it language}} parses its
+argument:
+
+\begin{verbatim}
+VERNAC ARGUMENT EXTEND language
+| [ "Ocaml" ] -> [ Ocaml ]
+| [ "Haskell" ] -> [ Haskell ]
+| [ "Scheme" ] -> [ Scheme ]
+| [ "Toplevel" ] -> [ Toplevel ]
+END
+\end{verbatim}
+
+For tactic arguments, and especially for \verb=ARGUMENT EXTEND=, the
+procedure is more subtle because tactics are objects of the {\Coq}
+environment which can be printed and interpreted. Then the syntax
+requires extra information providing a printer and a type telling how
+the argument behaves. Here is an example of entry parsing a pair of
+optional {\Coq} terms.
+
+\begin{verbatim}
+let pp_minus_div_arg pr_constr pr_tactic (omin,odiv) = 
+  if omin=None && odiv=None then mt() else
+    spc() ++ str "with" ++
+    pr_opt (fun c -> str "minus := " ++ pr_constr c) omin ++
+    pr_opt (fun c -> str "div := " ++ pr_constr c) odiv
+
+ARGUMENT EXTEND minus_div_arg 
+  TYPED AS constr_opt * constr_opt
+  PRINTED BY pp_minus_div_arg
+| [ "with" minusarg(m) divarg_opt(d) ] -> [ Some m, d ]
+| [ "with" divarg(d) minusarg_opt(m) ] -> [ m, Some d ]
+| [ ] -> [ None, None ]
+END
+\end{verbatim}
+
+Notice that the type {\tt constr\_opt * constr\_opt} tells that the
+object behaves as a pair of optional {\Coq} terms, i.e. as an object
+of {\ocaml} type {\tt constr option * constr option} if in a
+\verb=TACTIC EXTEND= macro and of type {\tt constr\_expr option *
+constr\_expr option} if in a \verb=VERNAC COMMAND EXTEND= macro.
+
+As for the printer, it must be a function expecting a printer for
+terms, a printer for tactics and returning a printer for the created
+argument. Especially, each sub-{\term} and each sub-{\tac} in the
+argument must be typed by the corresponding printers. Otherwise, the
+{\ocaml} code will not be well-typed.
+
+\Rem The entry {\tt bool} is bound to no syntax but it can be used to
+give the type of an argument as in the following example:
+
+\begin{verbatim}
+let pr_orient _prc _prt = function
+  | true -> mt ()
+  | false -> str " <-"
+
+ARGUMENT EXTEND orient TYPED AS bool PRINTED BY pr_orient
+| [ "->" ] -> [ true ]
+| [ "<-" ] -> [ false ]
+| [ ] -> [ true ]
+END
+\end{verbatim}
+
+\begin{figure}
+\begin{tabular}{|lcl|}
+\hline
+{\stritem} & ::= & 
+ {\tt ARGUMENT EXTEND} {\ident} {\arginfo} {\nelist{\grule}{$|$}} {\tt END}\\
+& $|$ & {\tt VERNAC ARGUMENT EXTEND} {\ident} {\nelist{\grule}{$|$}} {\tt END}\\
+\\
+{\arginfo} & ::= & {\tt TYPED AS} {\argtype} \\
+&& {\tt PRINTED BY} {\lident} \\
+%&& \zeroone{{\tt INTERPRETED BY} {\lident}}\\
+%&& \zeroone{{\tt GLOBALIZED BY} {\lident}}\\
+%&& \zeroone{{\tt SUBSTITUTED BY} {\lident}}\\
+%&& \zeroone{{\tt RAW\_TYPED AS} {\lident} {\tt RAW\_PRINTED BY} {\lident}}\\
+%&& \zeroone{{\tt GLOB\_TYPED AS} {\lident} {\tt GLOB\_PRINTED BY} {\lident}}\\
+\\
+{\argtype} & ::= & {\argtype} {\tt *} {\argtype} \\ 
+& $|$ & {\entry} \\
+\hline
+\end{tabular}
+\caption{Syntax of the macros binding {\ocaml} tactics or commands to a {\Coq} syntax}
+\label{ARGUMENT-EXTEND-syntax}
+\end{figure}
 
 %\end{document}