Documentation machine virtuelle

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

3 files changed, 49 insertions, 0 deletions

diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 730100eed..64f99835b 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -86,6 +86,7 @@ you move the \Coq\ binaries and library after installation.
 
 \section{Options}
 \index{Options of the command line}
+\label{vmoption}
 
 The following command-line options are recognized by the commands {\tt
   coqc} and {\tt coqtop}, unless stated otherwise:
@@ -239,6 +240,11 @@ The following command-line options are recognized by the commands {\tt
   resulting in a smaller memory requirement and faster compilation;
   warning: this invalidates some features such as the extraction tool.
 
+\item[{\tt -vm}]\ 
+
+  This activates the use of the bytecode-based conversion algorithm
+  for the current session (see section~\ref{SetVirtualMachine}).
+
 \item[{\tt -image} {\em file}]\ 
 
   This option sets the binary image to be used to be {\em file}
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 5ec2d77ca..ac5d3ddd3 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -831,6 +831,38 @@ This command displays the current nesting depth used for display.
 %\subsection{\tt Abstraction ...}
 %Not yet documented.
 
+\section{Controlling the conversion algorithm}
+
+{\Coq} comes with two algorithms to check the convertibility of types
+(see section~\ref{convertibility}). The first algorithm lazily
+compares applicative terms while the other is a brute-force but efficient
+algorithm that first normalizes the terms before comparing them.  The
+second algorithm is based on a bytecode representation of terms
+similar to the bytecode representation used in the ZINC virtual
+machine~\cite{Leroy90}. It is specially useful for intensive
+computation of algebraic values, such as numbers, and for reflexion-based
+tactics.
+
+\subsection{\tt Set Virtual Machine
+\label{SetVirtualMachine}
+\comindex{Set Virtual Machine}}
+
+This activates the bytecode-based conversion algorithm.
+
+\subsection{\tt Unset Virtual Machine
+\comindex{Unset Virtual Machine}}
+
+This deactivates the bytecode-based conversion algorithm.
+
+\subsection{\tt Test Virtual Machine
+\comindex{Test Virtual Machine}}
+
+This tells if the bytecode-based conversion algorithm is
+activated. The default behavior is to have the bytecode-based
+conversion algorithm deactivated.
+
+\SeeAlso sections~\ref{vmcompute} and~\ref{vmoption}.
+
 % $Id$ 
 
 %%% Local Variables: 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index bcf8a8ae7..242193162 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -755,6 +755,7 @@ performs the conversion in hypotheses $H_1\ldots H_n$.
 \tacindex{cbv}
 \tacindex{lazy}
 \tacindex{compute}}
+\label{vmcompute}
 
 These parameterized reduction tactics apply to any goal and perform
 the normalization of the goal according to the specified flags. Since
@@ -798,6 +799,16 @@ computational expressions (i.e. with few dead code).
 \item {\tt compute} \tacindex{compute} 
   
   This tactic is an alias for {\tt cbv beta delta evar iota zeta}.
+
+\item {\tt vm\_compute} \tacindex{vm\_compute}
+
+  This tactic evaluates the goal using the optimized call-by-value
+  evaluation bytecode-based virtual machine. This algorithm is
+  dramatically more efficient than the algorithm used for the {\tt
+  cbv} tactic, but it cannot be fine-tuned. It is specially
+  interesting for full evaluation of algebraic objects. This includes
+  the case of reflexion-based tactics.
+
 \end{Variants}
 
 \begin{ErrMsgs}