Langage de tactiques, AutoRewrite, Tauto-Intuition + autres modifs

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

2 files changed, 60 insertions, 21 deletions

diff --git a/doc/Changes.tex b/doc/Changes.tex
index 7534fed2f4..1eec3216d8 100755
--- a/doc/Changes.tex
+++ b/doc/Changes.tex
@@ -17,7 +17,7 @@
 %improvement of implicit arguments synthesis and speed in tactic
 %applications.
 
-TODO: expliquer les changements de AutoRewrite
+\def\ltac{{\cal L}_{tac}}
 
 \section*{Overview}
 
@@ -26,8 +26,8 @@ the implementation code of \Coq. For the end-user, {\Coq}
 V7 provides the following novelties:
 
 \begin{itemize}
-\item A mini-language to write tactics with high-level
-pattern-matching on goals  (see section \ref{Tactics})
+\item A more high-level tactic language called $\ltac$ (see
+section~\ref{Tactics})
 
 \item A primitive let-in construction (see section \ref{Letin})
 \item Structuration of the developments in libraries and use of the
@@ -200,10 +200,16 @@ Remark: A constant, say \verb:``4``:, is equivalent to
 
 \paragraph{{\tt Infix}} was inactive on pretty-printer. Now it works.
 
-\paragraph{Consecutive tokens} should now be separated (e.g. by a
-space). Typically, the string \verb:A->~<nat>O=O: is no longer
-recognized. It should be written \verb:A-> ~ <nat>O=O:... or simply
-\verb:A->~ <nat>O=O: because of a special treatment for \verb:->:!
+\paragraph{Consecutive symbols} are now considered as an unique token.
+Exceptions has been coded in the lexer to separate tokens we do not want to
+separate (for example \verb:A->~B:), but this is not exhaustive and some spaces
+may have to be inserted in some cases which have not been treated
+(incompatibility).
+
+%should now be separated (e.g. by a
+%space). Typically, the string \verb:A->~<nat>O=O: is no longer
+%recognized. It should be written \verb:A-> ~ <nat>O=O:... or simply
+%\verb:A->~ <nat>O=O: because of a special treatment for \verb:->:!
 
 \paragraph{The {\tt command} syntactic class for {\tt Grammar}} has
 been renamed {\tt constr} consistently with the usage for {\tt Syntax}
@@ -245,29 +251,56 @@ available to group several commands into a single one (useful for
 
 \section{Tactics}
 \label{Tactics}
-\def\ltac{{\cal L}_{tac}}
+\def\oc{{\sf Objective~Caml}}
 
 \subsection{A tactic language: $\ltac$}
 
-$\ltac$ is a mini-language to write tactics with high-level
-pattern-matching on goals. It has been contributed by David
-Delahaye. A separate documentation entitled $\ltac$ is available in
-the archive or at the author page http://logical.inria.fr/\~delahaye.
+$\ltac$ is a new layer of metalanguage to write tactics and especially to deal
+with small automations for which the use of the full programmable metalanguage
+(\oc{}) would be excessive. $\ltac$ is mainly a	small functional core with
+recursors and elaborated matching operators for terms but also for proof
+contexts. This language can be directly used in proof scripts or in toplevel
+definitions ({\tt Tactic~Definition}). It has been noticed that non-trivial
+tactics can be written with $\ltac$ and to provide a Turing-complete
+programmation framework, a quotation has been built to use $\ltac$ in \oc{}.
+$\ltac$ has been contributed by David Delahaye and to know the foundations of
+this language as well as to get a temporary documentation of $\ltac$, the
+author page can be visited at the following URL:\\
+
+http://logical.inria.fr/\~{}delahaye/
 
 \subsection{Changes in pre-existing tactics}
 \label{TacticChanges}
 
-   \paragraph{{\tt Tauto} and {\bf\tt Intuition}} have been rewritten
-   in $\ltac$. The behaviour of {\bf\tt Intuition} is slightly
-   different w.r.t. to subformulas of the form $(x:A)(P~x)$. This may
-   lead to some incompatibilities.
+   \paragraph{{\tt Tauto} and {\tt Intuition}} have been rewritten using the
+   new tactic language $\ltac$. The code is now quite shorter and a significant
+   increase in performances has been noticed. {\tt Tauto} has exactly the same
+   behavior. {\tt Intuition} is slightly less powerful (w.r.t. to dependent
+   types which are now considered as atomic formulas) but it has clearer
+   semantics. This may lead to some incompatibilities.
 
   \paragraph{{\tt Simpl}} now simplifies mutually defined fixpoints
   as expected (i.e. it does not introduce {\tt Fix id
   \{...\}} expressions).
 
-  \paragraph{{\tt AutoRewrite}} now applies only on main goal (remaining
-  subgoals are handled by {\tt Hint Rewrite}.
+  \paragraph{{\tt AutoRewrite}} now applies only on main goal and the remaining
+  subgoals are handled by\break{}{\tt Hint~Rewrite}. The syntax is now:\\
+
+  {\tt Hint Rewrite $($ -> $|$ <- $)*$ [ $term_1$ $...$ $term_n$ ] in
+    $ident$ using $tac$}\\
+
+  Adds the terms $term_1$ $...$ $term_n$ (their types must be equalities) in
+  the rewriting database $ident$ with the corresponding orientation (given by
+  the arrows; default is left to right) and the tactic $tac$ which is applied
+  to the subgoals generated by a rewriting, the main subgoal excluded.\\
+
+  {\tt AutoRewrite  [ $ident_1$ $...$ $ident_n$ ] using $tac$}\\
+
+  Performs all the rewritings given by the databases $ident_1$ $...$ $ident_n$
+  applying $tac$ to the main subgoal after each rewriting step.\\
+
+  See the contribution \texttt{contrib/Rocq/DEMOS/Demo\_AutoRewrite.v} for
+  examples.
 
   \paragraph{{\tt Intro $hyp$} and {\bf \tt Intros $hyp_1$ ... $hyp_n$}}
   now fail if the hypothesis/variable name provided already exists.
@@ -356,6 +389,8 @@ SearchRewrite (plus ? (plus ? ?)).
 identifiers and the {\tt inside} and {\tt outside} restrictions as
 {\tt SearchPattern} and {\tt SearchRewrite}.
 
+\paragraph{{\tt SearchIsos {\term}.}} has not been ported yet.
+
 \subsection{XML output}
 \label{XML}
 
@@ -376,6 +411,10 @@ http://www.cs.unibo.it/helm).
 	allows to explicitly give what arguments
 	have to be considered as implicit in {\ident}.
 
+\subsection{Tactic debuger}
+
+  \paragraph{{\tt Debug $($ On $|$ Off $)$}} turns on/off the tactic debuger.
+  This is still very experimental and no documentation are provided yet.
 
 \subsection{Syntax standardisation}
 
@@ -458,8 +497,8 @@ documentation tool (see the ``doc'' directory in {\Coq} source).
   \item The ``.vo'' files are not compatible and all ``.v'' files should
   be recompiled.
 
-  \item Consecutive tokens should now be separated (see section
-  \ref{SyntaxExtensions}).
+  \item Consecutive symbols may have to be separated in some cases (see
+  section~\ref{SyntaxExtensions}).
 
   \item Default parsers in {\tt Grammar} and {\tt Syntax} are
   different (see section \ref{GrammarSyntax}).
diff --git a/doc/Makefile.in b/doc/Makefile.in
index f1b0bdee2c..e578bbe5ff 100644
--- a/doc/Makefile.in
+++ b/doc/Makefile.in
@@ -4,7 +4,7 @@
 # Pdf: pdflatex
 # Html:
 #   - hevea: http://para.inria.fr/~maranget/hevea/
-#   - htmlSplit: http://coq.inria.fr/~delahaye
+#   - htmlSplit: http://coq.inria.fr/~delahaye/
 # Rapports INRIA: dviselect, rrkit (par Michel Mauny)
 
 DOCCOQTOP=@COQTOPBYTE@