Document native_compute.

3 files changed, 58 insertions, 6 deletions

diff --git a/CHANGES b/CHANGES
index c9e0ebfd2c..f5991416b1 100644
--- a/CHANGES
+++ b/CHANGES
@@ -146,6 +146,9 @@ Tactics
 - Matching using "lazymatch" was fundamentally modified. It now behaves
   like "match" (immediate execution of the matching branch) but without
   the backtracking mechanism in case of failure.
+- New conversion tactic "native_compute": evaluates the goal (or an hypothesis)
+  with a call-by-value strategy, using the OCaml native compiler. Useful on
+  very intensive computations.
 - New "cbn" tactic, a well-behaved simpl.
 - Repeated identical calls to omega should now produce identical proof terms.
 - Tactics btauto, a reflexive Boolean tautology solver.
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index e05ed721a5..1b7adc2517 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -2960,6 +2960,7 @@ performs the conversion in hypotheses {\ident}$_1$\ldots {\ident}$_n$.
 \tacindex{lazy}
 \tacindex{compute}
 \tacindex{vm\_compute}\label{vmcompute}
+\tacindex{native\_compute}\label{nativecompute}
 
 These parameterized reduction tactics apply to any goal and perform
 the normalization of the goal according to the specified flags. In
@@ -3028,12 +3029,20 @@ computational expressions (i.e. with few dead code).
 
 \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.
+  This tactic evaluates the goal using the optimized call-by-value evaluation
+  bytecode-based virtual machine described in
+  \cite{CompiledStrongReduction}. 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.
+
+\item {\tt native\_compute} \tacindex{native\_compute}
+
+  This tactic evaluates the goal by compilation to \ocaml{} as described in
+  \cite{FullReduction}. If \Coq{} is running in native code, it can be typically
+  two to five times faster than {\tt vm\_compute}. Note however that the
+  compilation cost is higher, so it is worth using only for intensive
+  computations.
 
 \end{Variants}
 
diff --git a/doc/refman/biblio.bib b/doc/refman/biblio.bib
index fdcc8a7b07..d78ce4f2c6 100644
--- a/doc/refman/biblio.bib
+++ b/doc/refman/biblio.bib
@@ -1327,3 +1327,43 @@ Languages},
  address = {New York, NY, USA},
  keywords = {canonical structures, coq, custom proof automation, hoare type theory, interactive theorem proving, tactics, type classes},
 }
+
+@inproceedings{CompiledStrongReduction,
+  author    = {Benjamin Gr{\'{e}}goire and
+               Xavier Leroy},
+  editor    = {Mitchell Wand and
+               Simon L. Peyton Jones},
+  title     = {A compiled implementation of strong reduction},
+  booktitle = {Proceedings of the Seventh {ACM} {SIGPLAN} International Conference
+               on Functional Programming {(ICFP} '02), Pittsburgh, Pennsylvania,
+               USA, October 4-6, 2002.},
+  pages     = {235--246},
+  publisher = {{ACM}},
+  year      = {2002},
+  url       = {http://doi.acm.org/10.1145/581478.581501},
+  doi       = {10.1145/581478.581501},
+  timestamp = {Tue, 11 Jun 2013 13:49:16 +0200},
+  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/icfp/GregoireL02},
+  bibsource = {dblp computer science bibliography, http://dblp.org}
+}
+
+@inproceedings{FullReduction,
+  author    = {Mathieu Boespflug and
+               Maxime D{\'{e}}n{\`{e}}s and
+               Benjamin Gr{\'{e}}goire},
+  editor    = {Jean{-}Pierre Jouannaud and
+               Zhong Shao},
+  title     = {Full Reduction at Full Throttle},
+  booktitle = {Certified Programs and Proofs - First International Conference, {CPP}
+               2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
+  series    = {Lecture Notes in Computer Science},
+  volume    = {7086},
+  pages     = {362--377},
+  publisher = {Springer},
+  year      = {2011},
+  url       = {http://dx.doi.org/10.1007/978-3-642-25379-9_26},
+  doi       = {10.1007/978-3-642-25379-9_26},
+  timestamp = {Thu, 17 Nov 2011 13:33:48 +0100},
+  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/cpp/BoespflugDG11},
+  bibsource = {dblp computer science bibliography, http://dblp.org}
+}
\ No newline at end of file