diff options
Diffstat (limited to 'doc/refman')
| -rw-r--r-- | doc/refman/Extraction.tex | 40 | ||||
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 64 | ||||
| -rw-r--r-- | doc/refman/RefMan-ssr.tex | 8 |
3 files changed, 88 insertions, 24 deletions
diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex index 79060e6062..cff7be3e96 100644 --- a/doc/refman/Extraction.tex +++ b/doc/refman/Extraction.tex @@ -1,4 +1,4 @@ -\achapter{Extraction of programs in Objective Caml and Haskell} +\achapter{Extraction of programs in OCaml and Haskell} %HEVEA\cutname{extraction.html} \label{Extraction} \aauthor{Jean-Christophe Filliâtre and Pierre Letouzey} @@ -95,12 +95,12 @@ one monolithic file or one file per \Coq\ library. \begin{description} \item {\tt Extraction TestCompile} \qualid$_1$ \dots\ \qualid$_n$. ~\par All the globals (or modules) \qualid$_1$ \dots\ \qualid$_n$ and all - their dependencies are extracted to a temporary Ocaml file, just as in + their dependencies are extracted to a temporary {\ocaml} file, just as in {\tt Extraction "{\em file}"}. Then this temporary file and its - signature are compiled with the same Ocaml compiler used to built - \Coq. This command succeeds only if the extraction and the Ocaml + signature are compiled with the same {\ocaml} compiler used to built + \Coq. This command succeeds only if the extraction and the {\ocaml} compilation succeed (and it fails if the current target language - of the extraction is not Ocaml). + of the extraction is not {\ocaml}). \end{description} \asection{Extraction options} @@ -109,26 +109,26 @@ one monolithic file or one file per \Coq\ library. \comindex{Extraction Language} The ability to fix target language is the first and more important -of the extraction options. Default is Ocaml. +of the extraction options. Default is {\ocaml}. \begin{description} -\item {\tt Extraction Language Ocaml}. +\item {\tt Extraction Language OCaml}. \item {\tt Extraction Language Haskell}. \item {\tt Extraction Language Scheme}. \end{description} \asubsection{Inlining and optimizations} -Since Objective Caml is a strict language, the extracted code has to +Since {\ocaml} is a strict language, the extracted code has to be optimized in order to be efficient (for instance, when using induction principles we do not want to compute all the recursive calls but only the needed ones). So the extraction mechanism provides an automatic optimization routine that will be called each time the user -want to generate Ocaml programs. The optimizations can be split in two +want to generate {\ocaml} programs. The optimizations can be split in two groups: the type-preserving ones -- essentially constant inlining and reductions -- and the non type-preserving ones -- some function abstractions of dummy types are removed when it is deemed safe in order to have more elegant types. Therefore some constants may not appear in the -resulting monolithic Ocaml program. In the case of modular extraction, +resulting monolithic {\ocaml} program. In the case of modular extraction, even if some inlining is done, the inlined constant are nevertheless printed, to ensure session-independent programs. @@ -367,15 +367,15 @@ As for {\tt Extract Inductive}, this command should be used with care: \item Extracting an inductive type to a pre-existing ML inductive type is quite sound. But extracting to a general type (by providing an ad-hoc pattern-matching) will often \emph{not} be fully rigorously -correct. For instance, when extracting {\tt nat} to Ocaml's {\tt +correct. For instance, when extracting {\tt nat} to {\ocaml}'s {\tt int}, it is theoretically possible to build {\tt nat} values that are -larger than Ocaml's {\tt max\_int}. It is the user's responsibility to +larger than {\ocaml}'s {\tt max\_int}. It is the user's responsibility to be sure that no overflow or other bad events occur in practice. \item Translating an inductive type to an ML type does \emph{not} magically improve the asymptotic complexity of functions, even if the ML type is an efficient representation. For instance, when extracting -{\tt nat} to Ocaml's {\tt int}, the function {\tt mult} stays +{\tt nat} to {\ocaml}'s {\tt int}, the function {\tt mult} stays quadratic. It might be interesting to associate this translation with some specific {\tt Extract Constant} when primitive counterparts exist. \end{itemize} @@ -402,7 +402,7 @@ Extract Inductive prod => "(*)" [ "(,)" ]. \end{coq_example} \noindent As an example of translation to a non-inductive datatype, let's turn -{\tt nat} into Ocaml's {\tt int} (see caveat above): +{\tt nat} into {\ocaml}'s {\tt int} (see caveat above): \begin{coq_example} Extract Inductive nat => int [ "0" "succ" ] "(fun fO fS n -> if n=0 then fO () else fS (n-1))". @@ -417,7 +417,7 @@ directly depends from the names of the \Coq\ files. It may happen that these filenames are in conflict with already existing files, either in the standard library of the target language or in other code that is meant to be linked with the extracted code. -For instance the module {\tt List} exists both in \Coq\ and in Ocaml. +For instance the module {\tt List} exists both in \Coq\ and in {\ocaml}. It is possible to instruct the extraction not to use particular filenames. \begin{description} @@ -430,7 +430,7 @@ It is possible to instruct the extraction not to use particular filenames. Allow the extraction to use any filename. \end{description} -\noindent For Ocaml, a typical use of these commands is +\noindent For {\ocaml}, a typical use of these commands is {\tt Extraction Blacklist String List}. \asection{Differences between \Coq\ and ML type systems} @@ -438,7 +438,7 @@ It is possible to instruct the extraction not to use particular filenames. Due to differences between \Coq\ and ML type systems, some extracted programs are not directly typable in ML. -We now solve this problem (at least in Ocaml) by adding +We now solve this problem (at least in {\ocaml}) by adding when needed some unsafe casting {\tt Obj.magic}, which give a generic type {\tt 'a} to any term. @@ -455,7 +455,7 @@ Definition dp := fun (A B:Set)(x:A)(y:B)(f:forall C:Set, C->C) => (f A x, f B y). \end{verbatim} -In Ocaml, for instance, the direct extracted term would be +In {\ocaml}, for instance, the direct extracted term would be \begin{verbatim} let dp x y f = Pair((f () x),(f () y)) \end{verbatim} @@ -480,13 +480,13 @@ Inductive anything : Type := dummy : forall A:Set, A -> anything. \end{verbatim} which corresponds to the definition of an ML dynamic type. -In Ocaml, we must cast any argument of the constructor dummy. +In {\ocaml}, we must cast any argument of the constructor dummy. \end{itemize} \noindent Even with those unsafe castings, you should never get error like ``segmentation fault''. In fact even if your program may seem -ill-typed to the Ocaml type-checker, it can't go wrong: it comes +ill-typed to the {\ocaml} type-checker, it can't go wrong: it comes from a Coq well-typed terms, so for example inductives will always have the correct number of arguments, etc. diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 8d82460a72..ef0f4af8f6 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -709,6 +709,55 @@ runs is displayed. Time is in seconds and is machine-dependent. The {\qstring} argument is optional. When provided, it is used to identify this particular occurrence of {\tt time}. +\subsubsection{Timing a tactic that evaluates to a term\tacindex{time\_constr}\tacindex{restart\_timer}\tacindex{finish\_timing} +\index{Tacticals!time\_constr@{\tt time\_constr}}} +\index{Tacticals!restart\_timer@{\tt restart\_timer}} +\index{Tacticals!finish\_timing@{\tt finish\_timing}} + +Tactic expressions that produce terms can be timed with the experimental tactic +\begin{quote} + {\tt time\_constr} {\tacexpr} +\end{quote} +which evaluates {\tacexpr\tt{ ()}} +and displays the time the tactic expression evaluated, assuming successful evaluation. +Time is in seconds and is machine-dependent. + +This tactic currently does not support nesting, and will report times based on the innermost execution. +This is due to the fact that it is implemented using the tactics +\begin{quote} + {\tt restart\_timer} {\qstring} +\end{quote} +and +\begin{quote} + {\tt finish\_timing} ({\qstring}) {\qstring} +\end{quote} +which (re)set and display an optionally named timer, respectively. +The parenthesized {\qstring} argument to {\tt finish\_timing} is also +optional, and determines the label associated with the timer for +printing. + +By copying the definition of {\tt time\_constr} from the standard +library, users can achive support for a fixed pattern of nesting by +passing different {\qstring} parameters to {\tt restart\_timer} and +{\tt finish\_timing} at each level of nesting. For example: + +\begin{coq_example} +Ltac time_constr1 tac := + let eval_early := match goal with _ => restart_timer "(depth 1)" end in + let ret := tac () in + let eval_early := match goal with _ => finish_timing ( "Tactic evaluation" ) "(depth 1)" end in + ret. + +Goal True. + let v := time_constr + ltac:(fun _ => + let x := time_constr1 ltac:(fun _ => constr:(10 * 10)) in + let y := time_constr1 ltac:(fun _ => eval compute in x) in + y) in + pose v. +Abort. +\end{coq_example} + \subsubsection[Local definitions]{Local definitions\index{Ltac!let@\texttt{let}} \index{Ltac!let rec@\texttt{let rec}} \index{let@\texttt{let}!in Ltac} @@ -1358,6 +1407,21 @@ The following two tactics behave like {\tt idtac} but enable and disable the pro {\tt stop ltac profiling}. \end{quote} +\tacindex{reset ltac profile}\tacindex{show ltac profile} +The following tactics behave like the corresponding vernacular commands and allow displaying and resetting the profile from tactic scripts for benchmarking purposes. + +\begin{quote} +{\tt reset ltac profile}. +\end{quote} + +\begin{quote} +{\tt show ltac profile}. +\end{quote} + +\begin{quote} +{\tt show ltac profile} {\qstring}. +\end{quote} + You can also pass the {\tt -profile-ltac} command line option to {\tt coqc}, which performs a {\tt Set Ltac Profiling} at the beginning of each document, and a {\tt Show Ltac Profile} at the end. Note that the profiler currently does not handle backtracking into multi-success tactics, and issues a warning to this effect in many cases when such backtracking occurs. diff --git a/doc/refman/RefMan-ssr.tex b/doc/refman/RefMan-ssr.tex index be199e0b24..31dabcdd4e 100644 --- a/doc/refman/RefMan-ssr.tex +++ b/doc/refman/RefMan-ssr.tex @@ -3096,10 +3096,10 @@ the tactic \ssrC{rewrite (=~ multi1)} is equivalent to \end{lstlisting} except that the constants \ssrC{eqba, eqab, mult1_rev} have not been created. -Rewriting with multirules -is useful to implement simplification or transformation -procedures, to be applied on terms of small to medium size. For -instance the library \ssrL{ssrnat} provides two implementations for +Rewriting with multirules is useful to implement simplification or +transformation procedures, to be applied on terms of small to medium +size. For instance, the library \ssrL{ssrnat} --- available in the +external math-comp library --- provides two implementations for arithmetic operations on natural numbers: an elementary one and a tail recursive version, less inefficient but also less convenient for reasoning purposes. The library also provides one lemma per such |