diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/Extraction.tex | 40 | ||||
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 39 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 10 |
3 files changed, 63 insertions, 26 deletions
diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex index a963662f64..9da23b54ed 100644 --- a/doc/refman/Extraction.tex +++ b/doc/refman/Extraction.tex @@ -3,7 +3,7 @@ \aauthor{Jean-Christophe Filliâtre and Pierre Letouzey} \index{Extraction} -We present here the \Coq\ extraction commands, used to build certified +\noindent We present here the \Coq\ extraction commands, used to build certified and relatively efficient functional programs, extracting them from either \Coq\ functions or \Coq\ proofs of specifications. The functional languages available as output are currently \ocaml{}, @@ -30,7 +30,7 @@ The next two commands are meant to be used for rapid preview of extraction. They both display extracted term(s) inside \Coq. \begin{description} -\item {\tt Extraction \qualid.} ~\par +\item {\tt Extraction \qualid{}.} ~\par Extraction of a constant or module in the \Coq\ toplevel. \item {\tt Recursive Extraction} \qualid$_1$ \dots\ \qualid$_n$. ~\par @@ -40,7 +40,7 @@ extraction. They both display extracted term(s) inside \Coq. %% TODO error messages -All the following commands produce real ML files. User can choose to produce +\noindent All the following commands produce real ML files. User can choose to produce one monolithic file or one file per \Coq\ library. \begin{description} @@ -76,7 +76,7 @@ one monolithic file or one file per \Coq\ library. using prefixes \verb!coq_! or \verb!Coq_!. \end{description} -The list of globals \qualid$_i$ does not need to be +\noindent The list of globals \qualid$_i$ does not need to be exhaustive: it is automatically completed into a complete and minimal environment. @@ -215,7 +215,7 @@ arguments. In fact, an argument can also be referred by a number indicating its position, starting from 1. \end{description} -When an actual extraction takes place, an error is normally raised if the +\noindent When an actual extraction takes place, an error is normally raised if the {\tt Extraction Implicit} declarations cannot be honored, that is if any of the implicited variables still occurs in the final code. This behavior can be relaxed @@ -260,7 +260,7 @@ what ML term corresponds to a given axiom. be inlined everywhere instead of being declared via a let. \end{description} -Note that the {\tt Extract Inlined Constant} command is sugar +\noindent Note that the {\tt Extract Inlined Constant} command is sugar for an {\tt Extract Constant} followed by a {\tt Extraction Inline}. Hence a {\tt Reset Extraction Inline} will have an effect on the realized and inlined axiom. @@ -279,7 +279,7 @@ Extract Constant X => "int". Extract Constant x => "0". \end{coq_example*} -Notice that in the case of type scheme axiom (i.e. whose type is an +\noindent Notice that in the case of type scheme axiom (i.e. whose type is an arity, that is a sequence of product finished by a sort), then some type variables have to be given. The syntax is then: @@ -287,7 +287,7 @@ variables have to be given. The syntax is then: \item{\tt Extract Constant \qualid\ \str$_1$ \dots\ \str$_n$ => \str.} \end{description} -The number of type variables is checked by the system. +\noindent The number of type variables is checked by the system. \Example \begin{coq_example*} @@ -295,7 +295,7 @@ Axiom Y : Set -> Set -> Set. Extract Constant Y "'a" "'b" => " 'a*'b ". \end{coq_example*} -Realizing an axiom via {\tt Extract Constant} is only useful in the +\noindent Realizing an axiom via {\tt Extract Constant} is only useful in the case of an informative axiom (of sort Type or Set). A logical axiom have no computational content and hence will not appears in extracted terms. But a warning is nonetheless issued if extraction encounters a @@ -325,7 +325,7 @@ native boolean type instead of \Coq\ one. The syntax is the following: pattern-matching of the language will be used. \end{description} -For an inductive type with $k$ constructor, the function used to +\noindent For an inductive type with $k$ constructor, the function used to emulate the match should expect $(k+1)$ arguments, first the $k$ branches in functional form, and then the inductive element to destruct. For instance, the match branch \verb$| S n => foo$ gives the @@ -365,7 +365,7 @@ Extract Inductive bool => "bool" [ "true" "false" ]. Extract Inductive sumbool => "bool" [ "true" "false" ]. \end{coq_example} -If an inductive constructor or type has arity 2 and the corresponding +\noindent If an inductive constructor or type has arity 2 and the corresponding string is enclosed by parenthesis, then the rest of the string is used as infix constructor or type. \begin{coq_example} @@ -373,7 +373,7 @@ Extract Inductive list => "list" [ "[]" "(::)" ]. Extract Inductive prod => "(*)" [ "(,)" ]. \end{coq_example} -As an example of translation to a non-inductive datatype, let's turn +\noindent As an example of translation to a non-inductive datatype, let's turn {\tt nat} into Ocaml's {\tt int} (see caveat above): \begin{coq_example} Extract Inductive nat => int [ "0" "succ" ] @@ -402,7 +402,7 @@ It is possible to instruct the extraction not to use particular filenames. Allow the extraction to use any filename. \end{description} -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} @@ -456,7 +456,7 @@ In Ocaml, we must cast any argument of the constructor dummy. \end{itemize} -Even with those unsafe castings, you should never get error like +\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 from a Coq well-typed terms, so for example inductives will always @@ -489,7 +489,7 @@ Inductive nat : Set := | S : nat -> nat. \end{coq_example*} -This module contains a theorem {\tt eucl\_dev}, whose type is +\noindent This module contains a theorem {\tt eucl\_dev}, whose type is \begin{verbatim} forall b:nat, b > 0 -> forall a:nat, diveucl a b \end{verbatim} @@ -506,7 +506,7 @@ Extraction Inline gt_wf_rec lt_wf_rec induction_ltof2. Recursive Extraction eucl_dev. \end{coq_example} -The inlining of {\tt gt\_wf\_rec} and others is not +\noindent The inlining of {\tt gt\_wf\_rec} and others is not mandatory. It only enhances readability of extracted code. You can then copy-paste the output to a file {\tt euclid.ml} or let \Coq\ do it for you with the following command: @@ -515,7 +515,7 @@ You can then copy-paste the output to a file {\tt euclid.ml} or let Extraction "euclid" eucl_dev. \end{verbatim} -Let us play the resulting program: +\noindent Let us play the resulting program: \begin{verbatim} # #use "euclid.ml";; @@ -543,7 +543,7 @@ val div : int -> int -> int * int = <fun> - : int * int = (11, 8) \end{verbatim} -Note that these {\tt nat\_of\_int} and {\tt int\_of\_nat} are now +\noindent Note that these {\tt nat\_of\_int} and {\tt int\_of\_nat} are now available via a mere {\tt Require Import ExtrOcamlIntConv} and then adding these functions to the list of functions to extract. This file {\tt ExtrOcamlIntConv.v} and some others in {\tt plugins/extraction/} @@ -551,7 +551,7 @@ are meant to help building concrete program via extraction. \asubsection{Extraction's horror museum} -Some pathological examples of extraction are grouped in the file +Some pathological examples of extraction are grouped in the file\\ {\tt test-suite/success/extraction.v} of the sources of \Coq. \asubsection{Users' Contributions} @@ -579,7 +579,7 @@ extraction test: \item {\tt stalmarck} \end{itemize} -{\tt continuations} and {\tt multiplier} are a bit particular. They are +\noindent {\tt continuations} and {\tt multiplier} are a bit particular. They are examples of developments where {\tt Obj.magic} are needed. This is probably due to an heavy use of impredicativity. After compilation, those two examples run nonetheless, thanks to the correction of the diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index ffcb371346..722249191b 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -25,6 +25,7 @@ problems. \def\contexthyp{\textrm{\textsl{context\_hyp}}} \def\tacarg{\nterm{tacarg}} \def\cpattern{\nterm{cpattern}} +\def\selector{\textrm{\textsl{selector}}} The syntax of the tactic language is given Figures~\ref{ltac} and~\ref{ltac-aux}. See Chapter~\ref{BNF-syntax} for a description of @@ -104,6 +105,7 @@ is understood as & | & {\tt exactly\_once} {\tacexprpref}\\ & | & {\tt timeout} {\it (}{\naturalnumber} {\it |} {\ident}{\it )} {\tacexprpref}\\ & | & {\tt time} \zeroone{\qstring} {\tacexprpref}\\ +& | & {\selector} {\tt :} {\tacexprpref}\\ & | & {\tacexprinf} \\ \\ {\tacexprinf} & ::= & @@ -203,7 +205,13 @@ is understood as & $|$ & {\integer} {\tt \,<\,} {\integer}\\ & $|$ & {\integer} {\tt <=} {\integer}\\ & $|$ & {\integer} {\tt \,>\,} {\integer}\\ -& $|$ & {\integer} {\tt >=} {\integer} +& $|$ & {\integer} {\tt >=} {\integer}\\ +\\ +\selector & ::= & + [{\ident}]\\ +& $|$ & {\integer}\\ +& $|$ & \nelist{{\it (}{\integer} {\it |} {\integer} {\tt -} {\integer}{\it )}} + {\tt ,} \end{tabular} \end{centerframe} \caption{Syntax of the tactic language (continued)} @@ -358,7 +366,36 @@ for $=1,...,n$. It fails if the number of focused goals is not exactly $n$. \end{Variants} +\subsubsection[Goal selectors]{Goal selectors\label{ltac:selector} +\tacindex{\tt :}\index{Tacticals!:@{\tt :}}} + +We can restrict the application of a tactic to a subset of +the currently focused goals with: +\begin{quote} +{\selector} {\tt :} {\tacexpr} +\end{quote} +When selecting several goals, the tactic {\tacexpr} is applied globally to +all selected goals. + +\begin{Variants} + \item{} [{\ident}] {\tt :} {\tacexpr} + + In this variant, {\tacexpr} is applied locally to a goal + previously named by the user. + + \item {\num} {\tt :} {\tacexpr} + + In this variant, {\tacexpr} is applied locally to the + {\num}-th goal. + + \item $n_1$-$m_1$, \dots, $n_k$-$m_k$ {\tt :} {\tacexpr} + + In this variant, {\tacexpr} is applied globally to the subset + of goals described by the given ranges. You can write a single + $n$ as a shortcut for $n$-$n$ when specifying multiple ranges. +\end{Variants} +\ErrMsg \errindex{No such goal} \subsubsection[For loop]{For loop\tacindex{do} \index{Tacticals!do@{\tt do}}} diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 54450fe7dc..527226f687 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -42,14 +42,12 @@ language will be described in Chapter~\ref{TacticLanguage}. \index{tactic@{\tac}}} A tactic is applied as an ordinary command. It may be preceded by a -goal selector: {\tt all} if the tactic is to be applied to every -focused goal simultaneously, or a natural number $n$ if it is to be -applied to the $n$-th goal. If no selector is specified, the default +goal selector (see Section \ref{ltac:selector}). +If no selector is specified, the default selector (see Section \ref{default-selector}) is used. \newcommand{\selector}{\nterm{selector}} \begin{tabular}{lcl} -{\selector} & := & {\tt all} | {\num}\\ {\commandtac} & ::= & {\selector} {\tt :} {\tac} {\tt .}\\ & $|$ & {\tac} {\tt .} \end{tabular} @@ -63,7 +61,9 @@ initial value is $1$, hence the tactics are, by default, applied to the first goal. Using {\tt Set Default Goal Selector ``all''} will make is so that tactics are, by default, applied to every goal simultaneously. Then, to apply a tactic {\tt tac} to the first goal -only, you can write {\tt 1:tac}. +only, you can write {\tt 1:tac}. Although more selectors are available, +only {\tt ``all''} or a single natural number are valid default +goal selectors. \subsection[\tt Test Default Goal Selector.] {\tt Test Default Goal Selector.} |