diff options
Diffstat (limited to 'doc/refman/RefMan-tus.tex')
| -rw-r--r-- | doc/refman/RefMan-tus.tex | 2015 |
1 files changed, 2015 insertions, 0 deletions
diff --git a/doc/refman/RefMan-tus.tex b/doc/refman/RefMan-tus.tex new file mode 100644 index 00000000..8be5c963 --- /dev/null +++ b/doc/refman/RefMan-tus.tex @@ -0,0 +1,2015 @@ +%\documentclass[11pt]{article} +%\usepackage{fullpage,euler} +%\usepackage[latin1]{inputenc} +%\begin{document} +%\title{Writing ad-hoc Tactics in Coq} +%\author{} +%\date{} +%\maketitle +%\tableofcontents +%\clearpage + +\chapter{Writing ad-hoc Tactics in Coq} +\label{WritingTactics} + +\section{Introduction} + +\Coq\ is an open proof environment, in the sense that the collection of +proof strategies offered by the system can be extended by the user. +This feature has two important advantages. First, the user can develop +his/her own ad-hoc proof procedures, customizing the system for a +particular domain of application. Second, the repetitive and tedious +aspects of the proofs can be abstracted away implementing new tactics +for dealing with them. For example, this may be useful when a theorem +needs several lemmas which are all proven in a similar but not exactly +the same way. Let us illustrate this with an example. + +Consider the problem of deciding the equality of two booleans. The +theorem establishing that this is always possible is state by +the following theorem: + +\begin{coq_example*} +Theorem decideBool : (x,y:bool){x=y}+{~x=y}. +\end{coq_example*} + +The proof proceeds by case analysis on both $x$ and $y$. This yields +four cases to solve. The cases $x=y=\textsl{true}$ and +$x=y=\textsl{false}$ are immediate by the reflexivity of equality. + +The other two cases follow by discrimination. The following script +describes the proof: + +\begin{coq_example*} +Destruct x. + Destruct y. + Left ; Reflexivity. + Right; Discriminate. + Destruct y. + Right; Discriminate. + Left ; Reflexivity. +\end{coq_example*} +\begin{coq_eval} +Abort. +\end{coq_eval} + +Now, consider the theorem stating the same property but for the +following enumerated type: + +\begin{coq_example*} +Inductive Set Color := Blue:Color | White:Color | Red:Color. +Theorem decideColor : (c1,c2:Color){c1=c2}+{~c1=c2}. +\end{coq_example*} + +This theorem can be proven in a very similar way, reasoning by case +analysis on $c_1$ and $c_2$. Once more, each of the (now six) cases is +solved either by reflexivity or by discrimination: + +\begin{coq_example*} +Destruct c1. + Destruct c2. + Left ; Reflexivity. + Right ; Discriminate. + Right ; Discriminate. + Destruct c2. + Right ; Discriminate. + Left ; Reflexivity. + Right ; Discriminate. + Destruct c2. + Right ; Discriminate. + Right ; Discriminate. + Left ; Reflexivity. +\end{coq_example*} +\begin{coq_eval} +Abort. +\end{coq_eval} + +If we face the same theorem for an enumerated datatype corresponding +to the days of the week, it would still follow a similar pattern. In +general, the general pattern for proving the property +$(x,y:R)\{x=y\}+\{\neg x =y\}$ for an enumerated type $R$ proceeds as +follow: +\begin{enumerate} +\item Analyze the cases for $x$. +\item For each of the sub-goals generated by the first step, analyze +the cases for $y$. +\item The remaining subgoals follow either by reflexivity or +by discrimination. +\end{enumerate} + +Let us describe how this general proof procedure can be introduced in +\Coq. + +\section{Tactic Macros} + +The simplest way to introduce it is to define it as new a +\textsl{tactic macro}, as follows: + +\begin{coq_example*} +Tactic Definition DecideEq [$a $b] := + [<:tactic:<Destruct $a; + Destruct $b; + (Left;Reflexivity) Orelse (Right;Discriminate)>>]. +\end{coq_example*} + +The general pattern of the proof is abstracted away using the +tacticals ``\texttt{;}'' and \texttt{Orelse}, and introducing two +parameters for the names of the arguments to be analyzed. + +Once defined, this tactic can be called like any other tactic, just +supplying the list of terms corresponding to its real arguments. Let us +revisit the proof of the former theorems using the new tactic +\texttt{DecideEq}: + +\begin{coq_example*} +Theorem decideBool : (x,y:bool){x=y}+{~x=y}. +DecideEq x y. +Defined. +\end{coq_example*} +\begin{coq_example*} +Theorem decideColor : (c1,c2:Color){c1=c2}+{~c1=c2}. +DecideEq c1 c2. +Defined. +\end{coq_example*} + +In general, the command \texttt{Tactic Definition} associates a name +to a parameterized tactic expression, built up from the tactics and +tacticals that are already available. The general syntax rule for this +command is the following: + +\begin{tabbing} +\texttt{Tactic Definition} \textit{tactic-name} \= +\texttt{[}\$$id_1\ldots \$id_n$\texttt{]}\\ +\> := \texttt{[<:tactic:<} \textit{tactic-expression} \verb+>>]+ +\end{tabbing} + +This command provides a quick but also very primitive mechanism for +introducing new tactics. It does not support recursive definitions, +and the arguments of a tactic macro are restricted to term +expressions. Moreover, there is no static checking of the definition +other than the syntactical one. Any error in the definition of the +tactic ---for instance, a call to an undefined tactic--- will not be +noticed until the tactic is called. + +%This command provides a very primitive mechanism for introducing new +%tactics. The arguments of a tactic macro are restricted to term +%expressions. Hence, it is not possible to define higher order tactics +%with this command. Also, there is no static checking of the definition +%other than syntactical. If the tactic contain errors in its definition +%--for instance, a call to an undefined tactic-- this will be noticed +%during the tactic call. + +Let us illustrate the weakness of this way of introducing new tactics +trying to extend our proof procedure to work on a larger class of +inductive types. Consider for example the decidability of equality +for pairs of booleans and colors: + +\begin{coq_example*} +Theorem decideBoolXColor : (p1,p2:bool*Color){p1=p2}+{~p1=p2}. +\end{coq_example*} + +The proof still proceeds by a double case analysis, but now the +constructors of the type take two arguments. Therefore, the sub-goals +that can not be solved by discrimination need further considerations +about the equality of such arguments: + +\begin{coq_example} + Destruct p1; + Destruct p2; Try (Right;Discriminate);Intros. +\end{coq_example} + +The half of the disjunction to be chosen depends on whether or not +$b=b_0$ and $c=c_0$. These equalities can be decided automatically +using the previous lemmas about booleans and colors. If both +equalities are satisfied, then it is sufficient to rewrite $b$ into +$b_0$ and $c$ into $c_0$, so that the left half of the goal follows by +reflexivity. Otherwise, the right half follows by first contraposing +the disequality, and then applying the invectiveness of the pairing +constructor. + +As the cases associated to each argument of the pair are very similar, +a tactic macro can be introduced to abstract this part of the proof: + +\begin{coq_example*} +Hints Resolve decideBool decideColor. +Tactic Definition SolveArg [$t1 $t2] := + [<:tactic:< + ElimType {$t1=$t2}+{~$t1=$t2}; + [(Intro equality;Rewrite equality;Clear equality) | + (Intro diseq; Right; Red; Intro absurd; + Apply diseq;Injection absurd;Trivial) | + Auto]>>]. +\end{coq_example*} + +This tactic is applied to each corresponding pair of arguments of the +arguments, until the goal can be solved by reflexivity: + +\begin{coq_example*} +SolveArg b b0; + SolveArg c c0; + Left; Reflexivity. +Defined. +\end{coq_example*} + +Therefore, a more general strategy for deciding the property +$(x,y:R)\{x=y\}+\{\neg x =y\}$ on $R$ can be sketched as follows: +\begin{enumerate} +\item Eliminate $x$ and then $y$. +\item Try discrimination to solve those goals where $x$ and $y$ has +been introduced by different constructors. +\item If $x$ and $y$ have been introduced by the same constructor, +then iterate the tactic \textsl{SolveArg} for each pair of +arguments. +\item Finally, solve the left half of the goal by reflexivity. +\end{enumerate} + +The implementation of this stronger proof strategy needs to perform a +term decomposition, in order to extract the list of arguments of each +constructor. It also requires the introduction of recursively defined +tactics, so that the \textsl{SolveArg} can be iterated on the lists of +arguments. These features are not supported by the \texttt{Tactic +Definition} command. One possibility could be extended this command in +order to introduce recursion, general parameter passing, +pattern-matching, etc, but this would quickly lead us to introduce the +whole \ocaml{} into \Coq\footnote{This is historically true. In fact, +\ocaml{} is a direct descendent of ML, a functional programming language +conceived language for programming the tactics of the theorem prover +LCF.}. Instead of doing this, we prefer to give to the user the +possibility of writing his/her own tactics directly in \ocaml{}, and then +to link them dynamically with \Coq's code. This requires a minimal +knowledge about \Coq's implementation. The next section provides an +overview of \Coq's architecture. + +%It is important to point out that the introduction of a new tactic +%never endangers the correction of the theorems proven in the extended +%system. In order to understand why, let us introduce briefly the system +%architecture. + +\section{An Overview of \Coq's Architecture} + +The implementation of \Coq\ is based on eight \textsl{logical +modules}. By ``module'' we mean here a logical piece of code having a +conceptual unity, that may concern several \ocaml{} files. By the sake of +organization, all the \ocaml{} files concerning a logical module are +grouped altogether into the same sub-directory. The eight modules +are: + +\begin{tabular}{lll} +1. & The logical framework & (directory \texttt{src/generic})\\ +2. & The language of constructions & (directory \texttt{src/constr})\\ +3. & The type-checker & (directory \texttt{src/typing})\\ +4. & The proof engine & (directory \texttt{src/proofs})\\ +5. & The language of basic tactics & (directory \texttt{src/tactics})\\ +6. & The vernacular interpreter & (directory \texttt{src/env})\\ +7. & The parser and the pretty-printer & (directory \texttt{src/parsing})\\ +8. & The standard library & (directory \texttt{src/lib}) +\end{tabular} + +\vspace{1em} + +The following sections briefly present each of the modules above. +This presentation is not intended to be a complete description of \Coq's +implementation, but rather a guideline to be read before taking a look +at the sources. For each of the modules, we also present some of its +most important functions, which are sufficient to implement a large +class of tactics. + + +\subsection{The Logical Framework} +\label{LogicalFramework} + +At the very heart of \Coq there is a generic untyped language for +expressing abstractions, applications and global constants. This +language is used as a meta-language for expressing the terms of the +Calculus of Inductive Constructions. General operations on terms like +collecting the free variables of an expression, substituting a term for +a free variable, etc, are expressed in this language. + +The meta-language \texttt{'op term} of terms has seven main +constructors: +\begin{itemize} +\item $(\texttt{VAR}\;id)$, a reference to a global identifier called $id$; +\item $(\texttt{Rel}\;n)$, a bound variable, whose binder is the $nth$ + binder up in the term; +\item $\texttt{DLAM}\;(x,t)$, a deBruijn's binder on the term $t$; +\item $\texttt{DLAMV}\;(x,vt)$, a deBruijn's binder on all the terms of + the vector $vt$; +\item $(\texttt{DOP0}\;op)$, a unary operator $op$; +\item $\texttt{DOP2}\;(op,t_1,t_2)$, the application of a binary +operator $op$ to the terms $t_1$ and $t_2$; +\item $\texttt{DOPN} (op,vt)$, the application of an n-ary operator $op$ to the +vector of terms $vt$. +\end{itemize} + +In this meta-language, bound variables are represented using the +so-called deBrujin's indexes. In this representation, an occurrence of +a bound variable is denoted by an integer, meaning the number of +binders that must be traversed to reach its own +binder\footnote{Actually, $(\texttt{Rel}\;n)$ means that $(n-1)$ binders +have to be traversed, since indexes are represented by strictly +positive integers.}. On the other hand, constants are referred by its +name, as usual. For example, if $A$ is a variable of the current +section, then the lambda abstraction $[x:A]x$ of the Calculus of +Constructions is represented in the meta-language by the term: + +\begin{displaymath} +(DOP2 (Lambda,(Var\;A),DLAM (x,(Rel\;1))) +\end{displaymath} + +In this term, $Lambda$ is a binary operator. Its first argument +correspond to the type $A$ of the bound variable, while the second is +a body of the abstraction, where $x$ is bound. The name $x$ is just kept +to pretty-print the occurrences of the bound variable. + +%Similarly, the product +%$(A:Prop)A$ of the Calculus of Constructions is represented by the +%term: +%\begin{displaumath} +%DOP2 (Prod, DOP0 (Sort (Prop Null)), DLAM (Name \#A, Rel 1)) +%\end{displaymath} + +The following functions perform some of the most frequent operations +on the terms of the meta-language: +\begin{description} +\fun{val Generic.subst1 : 'op term -> 'op term -> 'op term} + {$(\texttt{subst1}\;t_1\;t_2)$ substitutes $t_1$ for + $\texttt{(Rel}\;1)$ in $t_2$.} +\fun{val Generic.occur\_var : identifier -> 'op term -> bool} + {Returns true when the given identifier appears in the term, + and false otherwise.} +\fun{val Generic.eq\_term : 'op term -> 'op term -> bool} + {Implements $\alpha$-equality for terms.} +\fun{val Generic.dependent : 'op term -> 'op term -> bool} + {Returns true if the first term is a sub-term of the second.} +%\fun{val Generic.subst\_var : identifier -> 'op term -> 'op term} +% { $(\texttt{subst\_var}\;id\;t)$ substitutes the deBruijn's index +% associated to $id$ to every occurrence of the term +% $(\texttt{VAR}\;id)$ in $t$.} +\end{description} + +\subsubsection{Identifiers, names and sections paths.} + +Three different kinds of names are used in the meta-language. They are +all defined in the \ocaml{} file \texttt{Names}. + +\paragraph{Identifiers.} The simplest kind of names are +\textsl{identifiers}. An identifier is a string possibly indexed by an +integer. They are used to represent names that are not unique, like +for example the name of a variable in the scope of a section. The +following operations can be used for handling identifiers: + +\begin{description} +\fun{val Names.make\_ident : string -> int -> identifier} + {The value $(\texttt{make\_ident}\;x\;i)$ creates the + identifier $x_i$. If $i=-1$, then the identifier has + is created with no index at all.} +\fun{val Names.repr\_ident : identifier -> string * int} + {The inverse operation of \texttt{make\_ident}: + it yields the string and the index of the identifier.} +\fun{val Names.lift\_ident : identifier -> identifier} + {Increases the index of the identifier by one.} +\fun{val Names.next\_ident\_away : \\ +\qquad identifier -> identifier list -> identifier} + {\\ Generates a new identifier with the same root string than the + given one, but with a new index, different from all the indexes of + a given list of identifiers.} +\fun{val Names.id\_of\_string : string -> + identifier} + {Creates an identifier from a string.} +\fun{val Names.string\_of\_id : identifier -> string} + {The inverse operation: transforms an identifier into a string} +\end{description} + +\paragraph{Names.} A \textsl{name} is either an identifier or the +special name \texttt{Anonymous}. Names are used as arguments of +binders, in order to pretty print bound variables. +The following operations can be used for handling names: + +\begin{description} +\fun{val Names.Name: identifier -> Name} + {Constructs a name from an identifier.} +\fun{val Names.Anonymous : Name} + {Constructs a special, anonymous identifier, like the variable abstracted + in the term $[\_:A]0$.} +\fun{val + Names.next\_name\_away\_with\_default : \\ \qquad + string->name->identifier list->identifier} +{\\ If the name is not anonymous, then this function generates a new + identifier different from all the ones in a given list. Otherwise, it + generates an identifier from the given string.} +\end{description} + +\paragraph{Section paths.} +\label{SectionPaths} +A \textsl{section-path} is a global name to refer to an object without +ambiguity. It can be seen as a sort of filename, where open sections +play the role of directories. Each section path is formed by three +components: a \textsl{directory} (the list of open sections); a +\textsl{basename} (the identifier for the object); and a \textsl{kind} +(either CCI for the terms of the Calculus of Constructions, FW for the +the terms of $F_\omega$, or OBJ for other objects). For example, the +name of the following constant: +\begin{verbatim} + Section A. + Section B. + Section C. + Definition zero := O. +\end{verbatim} + +is internally represented by the section path: + +$$\underbrace{\mathtt{\#A\#B\#C}}_{\mbox{dirpath}} +\underbrace{\mathtt{\tt \#zero}}_{\mbox{basename}} +\underbrace{\mathtt{\tt .cci}_{\;}}_{\mbox{kind}}$$ + +When one of the sections is closed, a new constant is created with an +updated section-path,a nd the old one is no longer reachable. In our +example, after closing the section \texttt{C}, the new section-path +for the constant {\tt zero} becomes: +\begin{center} +\texttt{ \#A\#B\#zero.cci} +\end{center} + +The following operations can be used to handle section paths: + +\begin{description} +\fun{val Names.string\_of\_path : section\_path -> string} + {Transforms the section path into a string.} +\fun{val Names.path\_of\_string : string -> section\_path} + {Parses a string an returns the corresponding section path.} +\fun{val Names.basename : section\_path -> identifier} + {Provides the basename of a section path} +\fun{val Names.dirpath : section\_path -> string list} + {Provides the directory of a section path} +\fun{val Names.kind\_of\_path : section\_path -> path\_kind} + {Provides the kind of a section path} +\end{description} + +\subsubsection{Signatures} + +A \textsl{signature} is a mapping associating different informations +to identifiers (for example, its type, its definition, etc). The +following operations could be useful for working with signatures: + +\begin{description} +\fun{val Names.ids\_of\_sign : 'a signature -> identifier list} + {Gets the list of identifiers of the signature.} +\fun{val Names.vals\_of\_sign : 'a signature -> 'a list} + {Gets the list of values associated to the identifiers of the signature.} +\fun{val Names.lookup\_glob1 : \\ \qquad +identifier -> 'a signature -> (identifier * + 'a)} + {\\ Gets the value associated to a given identifier of the signature.} +\end{description} + + +\subsection{The Terms of the Calculus of Constructions} + +The language of the Calculus of Inductive Constructions described in +Chapter \ref{Cic} is implemented on the top of the logical framework, +instantiating the parameter $op$ of the meta-language with a +particular set of operators. In the implementation this language is +called \texttt{constr}, the language of constructions. + +% The only difference +%with respect to the one described in Section \ref{} is that the terms +%of \texttt{constr} may contain \textsl{existential variables}. An +%existential variable is a place holder representing a part of the term +%that is still to be constructed. Such ``open terms'' are necessary +%when building proofs interactively. + +\subsubsection{Building Constructions} + +The user does not need to know the choices made to represent +\texttt{constr} in the meta-language. They are abstracted away by the +following constructor functions: + +\begin{description} +\fun{val Term.mkRel : int -> constr} + {$(\texttt{mkRel}\;n)$ represents deBrujin's index $n$.} + +\fun{val Term.mkVar : identifier -> constr} + {$(\texttt{mkVar}\;id)$ + represents a global identifier named $id$, like a variable + inside the scope of a section, or a hypothesis in a proof}. + +\fun{val Term.mkExistential : constr} + {\texttt{mkExistential} represents an implicit sub-term, like the question + marks in the term \texttt{(pair ? ? O true)}.} + +%\fun{val Term.mkMeta : int -> constr} +% {$(\texttt{mkMeta}\;n)$ represents an existential variable, whose +% name is the integer $n$.} + +\fun{val Term.mkProp : constr} + {$\texttt{mkProp}$ represents the sort \textsl{Prop}.} + +\fun{val Term.mkSet : constr} + {$\texttt{mkSet}$ represents the sort \textsl{Set}.} + +\fun{val Term.mkType : Impuniv.universe -> constr} + {$(\texttt{mkType}\;u)$ represents the term + $\textsl{Type}(u)$. The universe $u$ is represented as a + section path indexed by an integer. } + +\fun{val Term.mkConst : section\_path -> constr array -> constr} + {$(\texttt{mkConst}\;c\;v)$ represents a constant whose name is + $c$. The body of the constant is stored in a global table, + accessible through the name of the constant. The array of terms + $v$ corresponds to the variables of the environment appearing in + the body of the constant when it was defined. For instance, a + constant defined in the section \textsl{Foo} containing the + variable $A$, and whose body is $[x:Prop\ra Prop](x\;A)$ is + represented inside the scope of the section by + $(\texttt{mkConst}\;\texttt{\#foo\#f.cci}\;[| \texttt{mkVAR}\;A + |])$. Once the section is closed, the constant is represented by + the term $(\texttt{mkConst}\;\#f.cci\;[| |])$, and its body + becomes $[A:Prop][x:Prop\ra Prop](x\;A)$}. + +\fun{val Term.mkMutInd : section\_path -> int -> constr array ->constr} + {$(\texttt{mkMutInd}\;c\;i)$ represents the $ith$ type + (starting from zero) of the block of mutually dependent + (co)inductive types, whose first type is $c$. Similarly to the + case of constants, the array of terms represents the current + environment of the (co)inductive type. The definition of the type + (its arity, its constructors, whether it is inductive or co-inductive, etc.) + is stored in a global hash table, accessible through the name of + the type.} + +\fun{val Term.mkMutConstruct : \\ \qquad section\_path -> int -> int -> constr array + ->constr} {\\ $(\texttt{mkMutConstruct}\;c\;i\;j)$ represents the + $jth$ constructor of the $ith$ type of the block of mutually + dependent (co)inductive types whose first type is $c$. The array + of terms represents the current environment of the (co)inductive + type.} + +\fun{val Term.mkCast : constr -> constr -> constr} + {$(\texttt{mkCast}\;t\;T)$ represents the annotated term $t::T$ in + \Coq's syntax.} + +\fun{val Term.mkProd : name ->constr ->constr -> constr} + {$(\texttt{mkProd}\;x\;A\;B)$ represents the product $(x:A)B$. + The free ocurrences of $x$ in $B$ are represented by deBrujin's + indexes.} + +\fun{val Term.mkNamedProd : identifier -> constr -> constr -> constr} + {$(\texttt{produit}\;x\;A\;B)$ represents the product $(x:A)B$, + but the bound occurrences of $x$ in $B$ are denoted by + the identifier $(\texttt{mkVar}\;x)$. The function automatically + changes each occurrences of this identifier into the corresponding + deBrujin's index.} + +\fun{val Term.mkArrow : constr -> constr -> constr} + {$(\texttt{arrow}\;A\;B)$ represents the type $(A\rightarrow B)$.} + +\fun{val Term.mkLambda : name -> constr -> constr -> constr} + {$(\texttt{mkLambda}\;x\;A\;b)$ represents the lambda abstraction + $[x:A]b$. The free ocurrences of $x$ in $B$ are represented by deBrujin's + indexes.} + +\fun{val Term.mkNamedLambda : identifier -> constr -> constr -> constr} + {$(\texttt{lambda}\;x\;A\;b)$ represents the lambda abstraction + $[x:A]b$, but the bound occurrences of $x$ in $B$ are denoted by + the identifier $(\texttt{mkVar}\;x)$. } + +\fun{val Term.mkAppLA : constr array -> constr} + {$(\texttt{mkAppLA}\;t\;[|t_1\ldots t_n|])$ represents the application + $(t\;t_1\;\ldots t_n)$.} + +\fun{val Term.mkMutCaseA : \\ \qquad + case\_info -> constr ->constr + ->constr array -> constr} + {\\ $(\texttt{mkMutCaseA}\;r\;P\;m\;[|f_1\ldots f_n|])$ + represents the term \Case{P}{m}{f_1\ldots f_n}. The first argument + $r$ is either \texttt{None} or $\texttt{Some}\;(c,i)$, where the + pair $(c,i)$ refers to the inductive type that $m$ belongs to.} + +\fun{val Term.mkFix : \\ \qquad +int array->int->constr array->name + list->constr array->constr} + {\\ $(\texttt{mkFix}\;[|k_1\ldots k_n |]\;i\;[|A_1\ldots + A_n|]\;[|f_1\ldots f_n|]\;[|t_1\ldots t_n|])$ represents the term + $\Fix{f_i}{f_1/k_1:A_1:=t_1 \ldots f_n/k_n:A_n:=t_n}$} + +\fun{val Term.mkCoFix : \\ \qquad + int -> constr array -> name list -> + constr array -> constr} + {\\ $(\texttt{mkCoFix}\;i\;[|A_1\ldots + A_n|]\;[|f_1\ldots f_n|]\;[|t_1\ldots t_n|])$ represents the term + $\CoFix{f_i}{f_1:A_1:=t_1 \ldots f_n:A_n:=t_n}$. There are no + decreasing indexes in this case.} +\end{description} + +\subsubsection{Decomposing Constructions} + +Each of the construction functions above has its corresponding +(partial) destruction function, whose name is obtained changing the +prefix \texttt{mk} by \texttt{dest}. In addition to these functions, a +concrete datatype \texttt{kindOfTerm} can be used to do pattern +matching on terms without dealing with their internal representation +in the meta-language. This concrete datatype is described in the \ocaml{} +file \texttt{term.mli}. The following function transforms a construction +into an element of type \texttt{kindOfTerm}: + +\begin{description} +\fun{val Term.kind\_of\_term : constr -> kindOfTerm} + {Destructs a term of the language \texttt{constr}, +yielding the direct components of the term. Hence, in order to do +pattern matching on an object $c$ of \texttt{constr}, it is sufficient +to do pattern matching on the value $(\texttt{kind\_of\_term}\;c)$.} +\end{description} + +Part of the information associated to the constants is stored in +global tables. The following functions give access to such +information: + +\begin{description} +\fun{val Termenv.constant\_value : constr -> constr} + {If the term denotes a constant, projects the body of a constant} +\fun{Termenv.constant\_type : constr -> constr} + {If the term denotes a constant, projects the type of the constant} +\fun{val mind\_arity : constr -> constr} + {If the term denotes an inductive type, projects its arity (i.e., + the type of the inductive type).} +\fun{val Termenv.mis\_is\_finite : mind\_specif -> bool} + {Determines whether a recursive type is inductive or co-inductive.} +\fun{val Termenv.mind\_nparams : constr -> int} + {If the term denotes an inductive type, projects the number of + its general parameters.} +\fun{val Termenv.mind\_is\_recursive : constr -> bool} + {If the term denotes an inductive type, + determines if the type has at least one recursive constructor. } +\fun{val Termenv.mind\_recargs : constr -> recarg list array array} + {If the term denotes an inductive type, returns an array $v$ such + that the nth element of $v.(i).(j)$ is + \texttt{Mrec} if the $nth$ argument of the $jth$ constructor of + the $ith$ type is recursive, and \texttt{Norec} if it is not.}. +\end{description} + +\subsection{The Type Checker} +\label{TypeChecker} + +The third logical module is the type checker. It concentrates two main +tasks concerning the language of constructions. + +On one hand, it contains the type inference and type-checking +functions. The type inference function takes a term +$a$ and a signature $\Gamma$, and yields a term $A$ such that +$\Gamma \vdash a:A$. The type-checking function takes two terms $a$ +and $A$ and a signature $\Gamma$, and determines whether or not +$\Gamma \vdash a:A$. + +On the other hand, this module is in charge of the compilation of +\Coq's abstract syntax trees into the language \texttt{constr} of +constructions. This compilation seeks to eliminate all the ambiguities +contained in \Coq's abstract syntax, restoring the information +necessary to type-check it. It concerns at least the following steps: +\begin{enumerate} +\item Compiling the pattern-matching expressions containing +constructor patterns, wild-cards, etc, into terms that only +use the primitive \textsl{Case} described in Chapter \ref{Cic} +\item Restoring type coercions and synthesizing the implicit arguments +(the one denoted by question marks in +{\Coq} syntax: cf section \ref{Coercions}). +\item Transforming the named bound variables into deBrujin's indexes. +\item Classifying the global names into the different classes of +constants (defined constants, constructors, inductive types, etc). +\end{enumerate} + +\subsection{The Proof Engine} + +The fourth stage of \Coq's implementation is the \textsl{proof engine}: +the interactive machine for constructing proofs. The aim of the proof +engine is to construct a top-down derivation or \textsl{proof tree}, +by the application of \textsl{tactics}. A proof tree has the following +general structure:\\ + +\begin{displaymath} +\frac{\Gamma \vdash ? = t(?_1,\ldots?_n) : G} + {\hspace{3ex}\frac{\displaystyle \Gamma_1 \vdash ?_1 = t_1(\ldots) : G_1} + {\stackrel{\vdots}{\displaystyle {\Gamma_{i_1} \vdash ?_{i_1} + : G_{i_1}}}}(tac_1) + \;\;\;\;\;\;\;\;\; + \frac{\displaystyle \Gamma_n \vdash ?_n = t_n(\ldots) : G_n} + {\displaystyle \stackrel{\vdots}{\displaystyle {\Gamma_{i_m} \vdash ?_{i_m} : + G_{i_m}}}}(tac_n)} (tac) +\end{displaymath} + + +\noindent Each node of the tree is called a \textsl{goal}. A goal +is a record type containing the following three fields: +\begin{enumerate} +\item the conclusion $G$ to be proven; +\item a typing signature $\Gamma$ for the free variables in $G$; +\item if the goal is an internal node of the proof tree, the +definition $t(?_1,\ldots?_n)$ of an \textsl{existential variable} +(i.e. a possible undefined constant) $?$ of type $G$ in terms of the +existential variables of the children sub-goals. If the node is a +leaf, the existential variable maybe still undefined. +\end{enumerate} + +Once all the existential variables have been defined the derivation is +completed, and a construction can be generated from the proof tree, +replacing each of the existential variables by its definition. This +is exactly what happens when one of the commands +\texttt{Qed}, \texttt{Save} or \texttt{Defined} is invoked +(cf. Section \ref{Qed}). The saved theorem becomes a defined constant, +whose body is the proof object generated. + +\paragraph{Important:} Before being added to the +context, the proof object is type-checked, in order to verify that it is +actually an object of the expected type $G$. Hence, the correctness +of the proof actually does not depend on the tactics applied to +generate it or the machinery of the proof engine, but only on the +type-checker. In other words, extending the system with a potentially +bugged new tactic never endangers the consistency of the system. + +\subsubsection{What is a Tactic?} +\label{WhatIsATactic} +%Let us now explain what is a tactic, and how the user can introduce +%new ones. + +From an operational point of view, the current state of the proof +engine is given by the mapping $emap$ from existential variables into +goals, plus a pointer to one of the leaf goals $g$. Such a pointer +indicates where the proof tree will be refined by the application of a +\textsl{tactic}. A tactic is a function from the current state +$(g,emap)$ of the proof engine into a pair $(l,val)$. The first +component of this pair is the list of children sub-goals $g_1,\ldots +g_n$ of $g$ to be yielded by the tactic. The second one is a +\textsl{validation function}. Once the proof trees $\pi_1,\ldots +\pi_n$ for $g_1,\ldots g_n$ have been completed, this validation +function must yield a proof tree $(val\;\pi_1,\ldots \pi_n)$ deriving +$g$. + +Tactics can be classified into \textsl{primitive} ones and +\textsl{defined} ones. Primitive tactics correspond to the five basic +operations of the proof engine: + +\begin{enumerate} +\item Introducing a universally quantified variable into the local +context of the goal. +\item Defining an undefined existential variable +\item Changing the conclusion of the goal for another +--definitionally equal-- term. +\item Changing the type of a variable in the local context for another +definitionally equal term. +\item Erasing a variable from the local context. +\end{enumerate} + +\textsl{Defined} tactics are tactics constructed by combining these +primitive operations. Defined tactics are registered in a hash table, +so that they can be introduced dynamically. In order to define such a +tactic table, it is necessary to fix what a \textsl{possible argument} +of a tactic may be. The type \texttt{tactic\_arg} of the possible +arguments for tactics is a union type including: +\begin{itemize} +\item quoted strings; +\item integers; +\item identifiers; +\item lists of identifiers; +\item plain terms, represented by its abstract syntax tree; +\item well-typed terms, represented by a construction; +\item a substitution for bound variables, like the +substitution in the tactic \\$\texttt{Apply}\;t\;\texttt{with}\;x:=t_1\ldots +x_n:=t_n$, (cf. Section~\ref{apply}); +\item a reduction expression, denoting the reduction strategy to be +followed. +\end{itemize} +Therefore, for each function $tac:a \rightarrow tactic$ implementing a +defined tactic, an associated dynamic tactic $tacargs\_tac: +\texttt{tactic\_arg}\;list \rightarrow tactic$ calling $tac$ must be +written. The aim of the auxiliary function $tacargs\_tac$ is to inject +the arguments of the tactic $tac$ into the type of possible arguments +for a tactic. + +The following function can be used for registering and calling a +defined tactic: + +\begin{description} +\fun{val Tacmach.add\_tactic : \\ \qquad +string -> (tactic\_arg list ->tactic) -> unit} + {\\ Registers a dynamic tactic with the given string as access index.} +\fun{val Tacinterp.vernac\_tactic : string*tactic\_arg list -> tactic} + {Interprets a defined tactic given by its entry in the + tactics table with a particular list of possible arguments.} +\fun{val Tacinterp.vernac\_interp : CoqAst.t -> tactic} + {Interprets a tactic expression formed combining \Coq's tactics and + tacticals, and described by its abstract syntax tree.} +\end{description} + +When programming a new tactic that calls an already defined tactic +$tac$, we have the choice between using the \ocaml{} function +implementing $tac$, or calling the tactic interpreter with the name +and arguments for interpreting $tac$. In the first case, a tactic call +will left the trace of the whole implementation of $tac$ in the proof +tree. In the second, the implementation of $tac$ will be hidden, and +only an invocation of $tac$ will be recalled (cf. the example of +Section \ref{ACompleteExample}. The following combinators can be used +to hide the implementation of a tactic: + +\begin{verbatim} +type 'a hiding_combinator = string -> ('a -> tactic) -> ('a -> tactic) +val Tacmach.hide_atomic_tactic : string -> tactic -> tactic +val Tacmach.hide_constr_tactic : constr hiding_combinator +val Tacmach.hide_constrl_tactic : (constr list) hiding_combinator +val Tacmach.hide_numarg_tactic : int hiding_combinator +val Tacmach.hide_ident_tactic : identifier hiding_combinator +val Tacmach.hide_identl_tactic : identifier hiding_combinator +val Tacmach.hide_string_tactic : string hiding_combinator +val Tacmach.hide_bindl_tactic : substitution hiding_combinator +val Tacmach.hide_cbindl_tactic : + (constr * substitution) hiding_combinator +\end{verbatim} + +These functions first register the tactic by a side effect, and then +yield a function calling the interpreter with the registered name and +the right injection into the type of possible arguments. + +\subsection{Tactics and Tacticals Provided by \Coq} + +The fifth logical module is the library of tacticals and basic tactics +provided by \Coq. This library is distributed into the directories +\texttt{tactics} and \texttt{src/tactics}. The former contains those +basic tactics that make use of the types contained in the basic state +of \Coq. For example, inversion or rewriting tactics are in the +directory \texttt{tactics}, since they make use of the propositional +equality type. Those tactics which are independent from the context +--like for example \texttt{Cut}, \texttt{Intros}, etc-- are defined in +the directory \texttt{src/tactics}. This latter directory also +contains some useful tools for programming new tactics, referred in +Section \ref{SomeUsefulToolsforWrittingTactics}. + +In practice, it is very unusual that the list of sub-goals and the +validation function of the tactic must be explicitly constructed by +the user. In most of the cases, the implementation of a new tactic +consists in supplying the appropriate arguments to the basic tactics +and tacticals. + +\subsubsection{Basic Tactics} + +The file \texttt{Tactics} contain the implementation of the basic +tactics provided by \Coq. The following tactics are some of the most +used ones: + +\begin{verbatim} +val Tactics.intro : tactic +val Tactics.assumption : tactic +val Tactics.clear : identifier list -> tactic +val Tactics.apply : constr -> constr substitution -> tactic +val Tactics.one_constructor : int -> constr substitution -> tactic +val Tactics.simplest_elim : constr -> tactic +val Tactics.elimType : constr -> tactic +val Tactics.simplest_case : constr -> tactic +val Tactics.caseType : constr -> tactic +val Tactics.cut : constr -> tactic +val Tactics.reduce : redexpr -> tactic +val Tactics.exact : constr -> tactic +val Auto.auto : int option -> tactic +val Auto.trivial : tactic +\end{verbatim} + +The functions hiding the implementation of these tactics are defined +in the module \texttt{Hiddentac}. Their names are prefixed by ``h\_''. + +\subsubsection{Tacticals} +\label{OcamlTacticals} + +The following tacticals can be used to combine already existing +tactics: + +\begin{description} +\fun{val Tacticals.tclIDTAC : tactic} + {The identity tactic: it leaves the goal as it is.} + +\fun{val Tacticals.tclORELSE : tactic -> tactic -> tactic} + {Tries the first tactic and in case of failure applies the second one.} + +\fun{val Tacticals.tclTHEN : tactic -> tactic -> tactic} + {Applies the first tactic and then the second one to each generated subgoal.} + +\fun{val Tacticals.tclTHENS : tactic -> tactic list -> tactic} + {Applies a tactic, and then applies each tactic of the tactic list to the + corresponding generated subgoal.} + +\fun{val Tacticals.tclTHENL : tactic -> tactic -> tactic} + {Applies the first tactic, and then applies the second one to the last + generated subgoal.} + +\fun{val Tacticals.tclREPEAT : tactic -> tactic} + {If the given tactic succeeds in producing a subgoal, then it + is recursively applied to each generated subgoal, + and so on until it fails. } + +\fun{val Tacticals.tclFIRST : tactic list -> tactic} + {Tries the tactics of the given list one by one, until one of them + succeeds.} + +\fun{val Tacticals.tclTRY : tactic -> tactic} + {Tries the given tactic and in case of failure applies the {\tt + tclIDTAC} tactical to the original goal.} + +\fun{val Tacticals.tclDO : int -> tactic -> tactic} + {Applies the tactic a given number of times.} + +\fun{val Tacticals.tclFAIL : tactic} + {The always failing tactic: it raises a {\tt UserError} exception.} + +\fun{val Tacticals.tclPROGRESS : tactic -> tactic} + {Applies the given tactic to the current goal and fails if the + tactic leaves the goal unchanged} + +\fun{val Tacticals.tclNTH\_HYP : int -> (constr -> tactic) -> tactic} + {Applies a tactic to the nth hypothesis of the local context. + The last hypothesis introduced correspond to the integer 1.} + +\fun{val Tacticals.tclLAST\_HYP : (constr -> tactic) -> tactic} + {Applies a tactic to the last hypothesis introduced.} + +\fun{val Tacticals.tclCOMPLETE : tactic -> tactic} + {Applies a tactic and fails if the tactic did not solve completely the + goal} + +\fun{val Tacticals.tclMAP : ('a -> tactic) -> 'a list -> tactic} + {Applied to the function \texttt{f} and the list \texttt{[x\_1; + ... ; x\_n]}, this tactical applies the tactic + \texttt{tclTHEN (f x1) (tclTHEN (f x2) ... ))))}} + +\fun{val Tacicals.tclIF : (goal sigma -> bool) -> tactic -> tactic -> tactic} + {If the condition holds, apply the first tactic; otherwise, + apply the second one} + +\end{description} + + +\subsection{The Vernacular Interpreter} + +The sixth logical module of the implementation corresponds to the +interpreter of the vernacular phrases of \Coq. These phrases may be +expressions from the \gallina{} language (definitions), general +directives (setting commands) or tactics to be applied by the proof +engine. + +\subsection{The Parser and the Pretty-Printer} +\label{PrettyPrinter} + +The last logical module is the parser and pretty printer of \Coq, +which is the interface between the vernacular interpreter and the +user. They translate the chains of characters entered at the input +into abstract syntax trees, and vice versa. Abstract syntax trees are +represented by labeled n-ary trees, and its type is called +\texttt{CoqAst.t}. For instance, the abstract syntax tree associated +to the term $[x:A]x$ is: + +\begin{displaymath} +\texttt{Node} + ((0,6), "LAMBDA", + [\texttt{Nvar}~((3, 4),"A");~\texttt{Slam}~((0,6),~Some~"x",~\texttt{Nvar}~((5,6),"x"))]) +\end{displaymath} + +The numbers correspond to \textsl{locations}, used to point to some +input line and character positions in the error messages. As it was +already explained in Section \ref{TypeChecker}, this term is then +translated into a construction term in order to be typed. + +The parser of \Coq\ is implemented using \camlpppp. The lexer and the data +used by \camlpppp\ to generate the parser lay in the directory +\texttt{src/parsing}. This directory also contains \Coq's +pretty-printer. The printing rules lay in the directory +\texttt{src/syntax}. The different entries of the grammar are +described in the module \texttt{Pcoq.Entry}. Let us present here two +important functions of this logical module: + +\begin{description} +\fun{val Pcoq.parse\_string : 'a Grammar.Entry.e -> string -> 'a} + {Parses a given string, trying to recognize a phrase + corresponding to some entry in the grammar. If it succeeds, + it yields a value associated to the grammar entry. For example, + applied to the entry \texttt{Pcoq.Command.command}, this function + parses a term of \Coq's language, and yields a value of type + \texttt{CoqAst.t}. When applied to the entry + \texttt{Pcoq.Vernac.vernac}, it parses a vernacular command and + returns the corresponding Ast.} +\fun{val gentermpr : \\ \qquad +path\_kind -> constr assumptions -> constr -> std\_ppcmds} + {\\ Pretty-prints a well-typed term of certain kind (cf. Section + \ref{SectionPaths}) under its context of typing assumption.} +\fun{val gentacpr : CoqAst.t -> std\_ppcmds} + {Pretty-prints a given abstract syntax tree representing a tactic + expression.} +\end{description} + +\subsection{The General Library} + +In addition to the ones laying in the standard library of \ocaml{}, +several useful modules about lists, arrays, sets, mappings, balanced +trees, and other frequently used data structures can be found in the +directory \texttt{lib}. Before writing a new one, check if it is not +already there! + +\subsubsection{The module \texttt{Std}} +This module in the directory \texttt{src/lib/util} is opened by almost +all modules of \Coq{}. Among other things, it contains a definition of +the different kinds of errors used in \Coq{} : + +\begin{description} +\fun{exception UserError of string * std\_ppcmds} + {This is the class of ``users exceptions''. Such errors arise when + the user attempts to do something illegal, for example \texttt{Intro} + when the current goal conclusion is not a product.} + +\fun{val Std.error : string -> 'a} + {For simple error messages} +\fun{val Std.errorlabstrm : string -> std\_ppcmds -> 'a} + {See section \ref{PrettyPrinter} : this can be used if the user + want to display a term or build a complex error message} + +\fun{exception Anomaly of string * std\_ppcmds} + {This for reporting bugs or things that should not + happen. The tacticals \texttt{tclTRY} and + \texttt{tclTRY} described in section \ref{OcamlTacticals} catch the + exceptions of type \texttt{UserError}, but they don't catch the + anomalies. So, in your code, don't raise any anomaly, unless you + know what you are doing. We also recommend to avoid constructs + such as \texttt{try ... with \_ -> ...} : such constructs can trap + an anomaly and make the debugging process harder.} + +\fun{val Std.anomaly : string -> 'a}{} +\fun{val Std.anomalylabstrm : string -> std\_ppcmds -> 'a}{} +\end{description} + +\section{The tactic writer mini-HOWTO} + +\subsection{How to add a vernacular command} + +The command to register a vernacular command can be found +in module \texttt{Vernacinterp}: + +\begin{verbatim} +val vinterp_add : string * (vernac_arg list -> unit -> unit) -> unit;; +\end{verbatim} + +The first argument is the name, the second argument is a function that +parses the arguments and returns a function of type +\texttt{unit}$\rightarrow$\texttt{unit} that do the job. + +In this section we will show how to add a vernacular command +\texttt{CheckCheck} that print a type of a term and the type of its +type. + +File \texttt{dcheck.ml}: + +\begin{verbatim} +open Vernacinterp;; +open Trad;; +let _ = + vinterp_add + ("DblCheck", + function [VARG_COMMAND com] -> + (fun () -> + let evmap = Evd.mt_evd () + and sign = Termenv.initial_sign () in + let {vAL=c;tYP=t;kIND=k} = + fconstruct_with_univ evmap sign com in + Pp.mSGNL [< Printer.prterm c; 'sTR ":"; + Printer.prterm t; 'sTR ":"; + Printer.prterm k >] ) + | _ -> bad_vernac_args "DblCheck") +;; +\end{verbatim} + +Like for a new tactic, a new syntax entry must be created. + +File \texttt{DCheck.v}: + +\begin{verbatim} +Declare ML Module "dcheck.ml". + +Grammar vernac vernac := + dblcheck [ "CheckCheck" comarg($c) ] -> [(DblCheck $c)]. +\end{verbatim} + +We are now able to test our new command: + +\begin{verbatim} +Coq < Require DCheck. +Coq < CheckCheck O. +O:nat:Set +\end{verbatim} + +Most Coq vernacular commands are registered in the module + \verb+src/env/vernacentries.ml+. One can see more examples here. + +\subsection{How to keep a hashtable synchronous with the reset mechanism} + +This is far more tricky. Some vernacular commands modify some +sort of state (for example by adding something in a hashtable). One +wants that \texttt{Reset} has the expected behavior with this +commands. + +\Coq{} provides a general mechanism to do that. \Coq{} environments +contains objects of three kinds: CCI, FW and OBJ. CCI and FW are for +constants of the calculus. OBJ is a dynamically extensible datatype +that contains sections, tactic definitions, hints for auto, and so +on. + +The simplest example of use of such a mechanism is in file +\verb+src/proofs/macros.ml+ (which implements the \texttt{Tactic + Definition} command). Tactic macros are stored in the imperative +hashtable \texttt{mactab}. There are two functions freeze and unfreeze +to make a copy of the table and to restore the state of table from the +copy. Then this table is declared using \texttt{Library.declare\_summary}. + +What does \Coq{} with that ? \Coq{} defines synchronization points. +At each synchronisation point, the declared tables are frozen (that +is, a copy of this tables is stored). + +When \texttt{Reset }$i$ is called, \Coq{} goes back to the first +synchronisation point that is above $i$ and ``replays'' all objects +between that point +and $i$. It will re-declare constants, re-open section, etc. + +So we need to declare a new type of objects, TACTIC-MACRO-DATA. To +``replay'' on object of that type is to add the corresponding tactic +macro to \texttt{mactab} + +So, now, we can say that \texttt{mactab} is synchronous with the Reset +mechanism$^{\mathrm{TM}}$. + +Notice that this works for hash tables but also for a single integer +(the Undo stack size, modified by the \texttt{Set Undo} command, for +example). + +\subsection{The right way to access to Coq constants from your ML code} + +With their long names, Coq constants are stored using: + +\begin{itemize} +\item a section path +\item an identifier +\end{itemize} + +The identifier is exactly the identifier that is used in \Coq{} to +denote the constant; the section path can be known using the +\texttt{Locate} command: + +\begin{coq_example} + Locate S. + Locate nat. + Locate eq. +\end{coq_example} + +Now it is easy to get a constant by its name and section path: + + +\begin{verbatim} +let constant sp id = + Machops.global_reference (Names.gLOB (Termenv.initial_sign ())) + (Names.path_of_string sp) (Names.id_of_string id);; +\end{verbatim} + + +The only issue is that if one cannot put: + + +\begin{verbatim} +let coq_S = constant "#Datatypes#nat.cci" "S";; +\end{verbatim} + + +in his tactic's code. That is because this sentence is evaluated +\emph{before} the module \texttt{Datatypes} is loaded. The solution is +to use the lazy evaluation of \ocaml{}: + + +\begin{verbatim} +let coq_S = lazy (constant "#Datatypes#nat.cci" "S");; + +... (Lazy.force coq_S) ... +\end{verbatim} + + +Be sure to call always Lazy.force behind a closure -- i.e. inside a +function body or behind the \texttt{lazy} keyword. + +One can see examples of that technique in the source code of \Coq{}, +for example +\verb+tactics/contrib/polynom/ring.ml+ or +\verb+tactics/contrib/polynom/coq_omega.ml+. + +\section{Some Useful Tools for Writing Tactics} +\label{SomeUsefulToolsforWrittingTactics} +When the implementation of a tactic is not a straightforward +combination of tactics and tacticals, the module \texttt{Tacmach} +provides several useful functions for handling goals, calling the +type-checker, parsing terms, etc. This module is intended to be +the interface of the proof engine for the user. + +\begin{description} +\fun{val Tacmach.pf\_hyps : goal sigma -> constr signature} + {Projects the local typing context $\Gamma$ from a given goal $\Gamma\vdash ?:G$.} +\fun{val pf\_concl : goal sigma -> constr} + {Projects the conclusion $G$ from a given goal $\Gamma\vdash ?:G$.} +\fun{val Tacmach.pf\_nth\_hyp : goal sigma -> int -> identifier * + constr} + {Projects the $ith$ typing constraint $x_i:A_i$ from the local + context of the given goal.} +\fun{val Tacmach.pf\_fexecute : goal sigma -> constr -> judgement} + {Given a goal whose local context is $\Gamma$ and a term $a$, this + function infers a type $A$ and a kind $K$ such that the judgement + $a:A:K$ is valid under $\Gamma$, or raises an exception if there + is no such judgement. A judgement is just a record type containing + the three terms $a$, $A$ and $K$.} +\fun{val Tacmach.pf\_infexecute : \\ + \qquad +goal sigma -> constr -> judgement * information} + {\\ In addition to the typing judgement, this function also extracts + the $F_{\omega}$ program underlying the term.} +\fun{val Tacmach.pf\_type\_of : goal sigma -> constr -> constr} + {Infers a term $A$ such that $\Gamma\vdash a:A$ for a given term + $a$, where $\Gamma$ is the local typing context of the goal.} +\fun{val Tacmach.pf\_check\_type : goal sigma -> constr -> constr -> bool} + {This function yields a type $A$ if the two given terms $a$ and $A$ verify $\Gamma\vdash + a:A$ in the local typing context $\Gamma$ of the goal. Otherwise, + it raises an exception.} +\fun{val Tacmach.pf\_constr\_of\_com : goal sigma -> CoqAst.t -> constr} + {Transforms an abstract syntax tree into a well-typed term of the + language of constructions. Raises an exception if the term cannot + be typed.} +\fun{val Tacmach.pf\_constr\_of\_com\_sort : goal sigma -> CoqAst.t -> constr} + {Transforms an abstract syntax tree representing a type into + a well-typed term of the language of constructions. Raises an + exception if the term cannot be typed.} +\fun{val Tacmach.pf\_parse\_const : goal sigma -> string -> constr} + {Constructs the constant whose name is the given string.} +\fun{val +Tacmach.pf\_reduction\_of\_redexp : \\ + \qquad goal sigma -> red\_expr -> constr -> constr} + {\\ Applies a certain kind of reduction function, specified by an + element of the type red\_expr.} +\fun{val Tacmach.pf\_conv\_x : goal sigma -> constr -> constr -> bool} + {Test whether two given terms are definitionally equal.} +\end{description} + +\subsection{Patterns} +\label{Patterns} + +The \ocaml{} file \texttt{Pattern} provides a quick way for describing a +term pattern and performing second-order, binding-preserving, matching +on it. Patterns are described using an extension of \Coq's concrete +syntax, where the second-order meta-variables of the pattern are +denoted by indexed question marks. + +Patterns may depend on constants, and therefore only to make have +sense when certain theories have been loaded. For this reason, they +are stored with a \textsl{module-marker}, telling us which modules +have to be open in order to use the pattern. The following functions +can be used to store and retrieve patterns form the pattern table: + +\begin{description} +\fun{val Pattern.make\_module\_marker : string list -> module\_mark} + {Constructs a module marker from a list of module names.} +\fun{val Pattern.put\_pat : module\_mark -> string -> marked\_term} + {Constructs a pattern from a parseable string containing holes + and a module marker.} +\fun{val Pattern.somatches : constr -> marked\_term-> bool} + {Tests if a term matches a pattern.} +\fun{val dest\_somatch : constr -> marked\_term -> constr list} + {If the term matches the pattern, yields the list of sub-terms + matching the occurrences of the pattern variables (ordered from + left to right). Raises a \texttt{UserError} exception if the term + does not match the pattern.} +\fun{val Pattern.soinstance : marked\_term -> constr list -> constr} + {Substitutes each hole in the pattern + by the corresponding term of the given the list.} +\end{description} + +\paragraph{Warning:} Sometimes, a \Coq\ term may have invisible +sub-terms that the matching functions are nevertheless sensible to. +For example, the \Coq\ term $(?_1,?_2)$ is actually a shorthand for +the expression $(\texttt{pair}\;?\;?\;?_1\;?_2)$. +Hence, matching this term pattern +with the term $(\texttt{true},\texttt{O})$ actually yields the list +$[?;?;\texttt{true};\texttt{O}]$ as result (and \textbf{not} +$[\texttt{true};\texttt{O}]$, as could be expected). + +\subsection{Patterns on Inductive Definitions} + +The module \texttt{Pattern} also includes some functions for testing +if the definition of an inductive type satisfies certain +properties. Such functions may be used to perform pattern matching +independently from the name given to the inductive type and the +universe it inhabits. They yield the value $(\texttt{Some}\;r::l)$ if +the input term reduces into an application of an inductive type $r$ to +a list of terms $l$, and the definition of $r$ satisfies certain +conditions. Otherwise, they yield the value \texttt{None}. + +\begin{description} +\fun{val Pattern.match\_with\_non\_recursive\_type : constr list option} + {Tests if the inductive type $r$ has no recursive constructors} +\fun{val Pattern.match\_with\_disjunction : constr list option} + {Tests if the inductive type $r$ is a non-recursive type + such that all its constructors have a single argument.} +\fun{val Pattern.match\_with\_conjunction : constr list option} + {Tests if the inductive type $r$ is a non-recursive type + with a unique constructor.} +\fun{val Pattern.match\_with\_empty\_type : constr list option} + {Tests if the inductive type $r$ has no constructors at all} +\fun{val Pattern.match\_with\_equation : constr list option} + {Tests if the inductive type $r$ has a single constructor + expressing the property of reflexivity for some type. For + example, the types $a=b$, $A\mbox{==}B$ and $A\mbox{===}B$ satisfy + this predicate.} +\end{description} + +\subsection{Elimination Tacticals} + +It is frequently the case that the subgoals generated by an +elimination can all be solved in a similar way, possibly parametrized +on some information about each case, like for example: +\begin{itemize} +\item the inductive type of the object being eliminated; +\item its arguments (if it is an inductive predicate); +\item the branch number; +\item the predicate to be proven; +\item the number of assumptions to be introduced by the case +\item the signature of the branch, i.e., for each argument of +the branch whether it is recursive or not. +\end{itemize} + +The following tacticals can be useful to deal with such situations. +They + +\begin{description} +\fun{val Elim.simple\_elimination\_then : \\ \qquad +(branch\_args -> tactic) -> constr -> tactic} + {\\ Performs the default elimination on the last argument, and then + tries to solve the generated subgoals using a given parametrized + tactic. The type branch\_args is a record type containing all + information mentioned above.} +\fun{val Elim.simple\_case\_then : \\ \qquad +(branch\_args -> tactic) -> constr -> tactic} + {\\ Similarly, but it performs case analysis instead of induction.} +\end{description} + +\section{A Complete Example} +\label{ACompleteExample} + +In order to illustrate the implementation of a new tactic, let us come +back to the problem of deciding the equality of two elements of an +inductive type. + +\subsection{Preliminaries} + +Let us call \texttt{newtactic} the directory that will contain the +implementation of the new tactic. In this directory will lay two +files: a file \texttt{eqdecide.ml}, containing the \ocaml{} sources that +implements the tactic, and a \Coq\ file \texttt{Eqdecide.v}, containing +its associated grammar rules and the commands to generate a module +that can be loaded dynamically from \Coq's toplevel. + +To compile our project, we will create a \texttt{Makefile} with the +command \texttt{do\_Makefile} (see section \ref{Makefile}) : + +\begin{quotation} + \texttt{do\_Makefile eqdecide.ml EqDecide.v > Makefile}\\ + \texttt{touch .depend}\\ + \texttt{make depend} +\end{quotation} + +We must have kept the sources of \Coq{} somewhere and to set an +environment variable \texttt{COQTOP} that points to that directory. + +\subsection{Implementing the Tactic} + +The file \texttt{eqdecide.ml} contains the implementation of the +tactic in \ocaml{}. Let us recall the main steps of the proof strategy +for deciding the proposition $(x,y:R)\{x=y\}+\{\neg x=y\}$ on the +inductive type $R$: +\begin{enumerate} +\item Eliminate $x$ and then $y$. +\item Try discrimination to solve those goals where $x$ and $y$ has +been introduced by different constructors. +\item If $x$ and $y$ have been introduced by the same constructor, + then analyze one by one the corresponding pairs of arguments. + If they are equal, rewrite one into the other. If they are + not, derive a contradiction from the invectiveness of the + constructor. +\item Once all the arguments have been rewritten, solve the left half +of the goal by reflexivity. +\end{enumerate} + +In the sequel we implement these steps one by one. We start opening +the modules necessary for the implementation of the tactic: + +\begin{verbatim} +open Names +open Term +open Tactics +open Tacticals +open Hiddentac +open Equality +open Auto +open Pattern +open Names +open Termenv +open Std +open Proof_trees +open Tacmach +\end{verbatim} + +The first step of the procedure can be straightforwardly implemented as +follows: + +\begin{verbatim} +let clear_last = (tclLAST_HYP (fun c -> (clear_one (destVar c))));; +\end{verbatim} + +\begin{verbatim} +let mkBranches = + (tclTHEN intro + (tclTHEN (tclLAST_HYP h_simplest_elim) + (tclTHEN clear_last + (tclTHEN intros + (tclTHEN (tclLAST_HYP h_simplest_case) + (tclTHEN clear_last + intros))))));; +\end{verbatim} + +Notice the use of the tactical \texttt{tclLAST\_HYP}, which avoids to +give a (potentially clashing) name to the quantified variables of the +goal when they are introduced. + +The second step of the procedure is implemented by the following +tactic: + +\begin{verbatim} +let solveRightBranch = (tclTHEN simplest_right discrConcl);; +\end{verbatim} + +In order to illustrate how the implementation of a tactic can be +hidden, let us do it with the tactic above: + +\begin{verbatim} +let h_solveRightBranch = + hide_atomic_tactic "solveRightBranch" solveRightBranch +;; +\end{verbatim} + +As it was already mentioned in Section \ref{WhatIsATactic}, the +combinator \texttt{hide\_atomic\_tactic} first registers the tactic +\texttt{solveRightBranch} in the table, and returns a tactic which +calls the interpreter with the used to register it. Hence, when the +tactical \texttt{Info} is used, our tactic will just inform that +\texttt{solveRightBranch} was applied, omitting all the details +corresponding to \texttt{simplest\_right} and \texttt{discrConcl}. + + + +The third step requires some auxiliary functions for constructing the +type $\{c_1=c_2\}+\{\neg c_1=c_2\}$ for a given inductive type $R$ and +two constructions $c_1$ and $c_2$, and for generalizing this type over +$c_1$ and $c_2$: + +\begin{verbatim} +let mmk = make_module_marker ["#Logic.obj";"#Specif.obj"];; +let eqpat = put_pat mmk "eq";; +let sumboolpat = put_pat mmk "sumbool";; +let notpat = put_pat mmk "not";; +let eq = get_pat eqpat;; +let sumbool = get_pat sumboolpat;; +let not = get_pat notpat;; + +let mkDecideEqGoal rectype c1 c2 g = + let equality = mkAppL [eq;rectype;c1;c2] in + let disequality = mkAppL [not;equality] + in mkAppL [sumbool;equality;disequality] +;; +let mkGenDecideEqGoal rectype g = + let hypnames = ids_of_sign (pf_hyps g) in + let xname = next_ident_away (id_of_string "x") hypnames + and yname = next_ident_away (id_of_string "y") hypnames + in (mkNamedProd xname rectype + (mkNamedProd yname rectype + (mkDecideEqGoal rectype (mkVar xname) (mkVar yname) g))) +;; +\end{verbatim} + +The tactic will depend on the \Coq modules \texttt{Logic} and +\texttt{Specif}, since we use the constants corresponding to +propositional equality (\texttt{eq}), computational disjunction +(\texttt{sumbool}), and logical negation (\texttt{not}), defined in +that modules. This is specified creating the module maker +\texttt{mmk} (cf. Section \ref{Patterns}). + +The third step of the procedure can be divided into three sub-steps. +Assume that both $x$ and $y$ have been introduced by the same +constructor. For each corresponding pair of arguments of that +constructor, we have to consider whether they are equal or not. If +they are equal, the following tactic is applied to rewrite one into +the other: + +\begin{verbatim} +let eqCase tac = + (tclTHEN intro + (tclTHEN (tclLAST_HYP h_rewriteLR) + (tclTHEN clear_last + tac))) +;; +\end{verbatim} + + +If they are not equal, then the goal is contraposed and a +contradiction is reached form the invectiveness of the constructor: + +\begin{verbatim} +let diseqCase = + let diseq = (id_of_string "diseq") in + let absurd = (id_of_string "absurd") + in (tclTHEN (intro_using diseq) + (tclTHEN h_simplest_right + (tclTHEN red_in_concl + (tclTHEN (intro_using absurd) + (tclTHEN (h_simplest_apply (mkVar diseq)) + (tclTHEN (h_injHyp absurd) + trivial )))))) +;; +\end{verbatim} + +In the tactic above we have chosen to name the hypotheses because +they have to be applied later on. This introduces a potential risk +of name clashing if the context already contains other hypotheses +also named ``diseq'' or ``absurd''. + +We are now ready to implement the tactic \textsl{SolveArg}. Given the +two arguments $a_1$ and $a_2$ of the constructor, this tactic cuts the +goal with the proposition $\{a_1=a_2\}+\{\neg a_1=a_2\}$, and then +applies the tactics above to each of the generated cases. If the +disjunction cannot be solved automatically, it remains as a sub-goal +to be proven. + +\begin{verbatim} +let solveArg a1 a2 tac g = + let rectype = pf_type_of g a1 in + let decide = mkDecideEqGoal rectype a1 a2 g + in (tclTHENS (h_elimType decide) + [(eqCase tac);diseqCase;default_auto]) g +;; +\end{verbatim} + +The following tactic implements the third and fourth steps of the +proof procedure: + +\begin{verbatim} +let conclpatt = put_pat mmk "{<?1>?2=?3}+{?4}" +;; +let solveLeftBranch rectype g = + let (_::(lhs::(rhs::_))) = + try (dest_somatch (pf_concl g) conclpatt) + with UserError ("somatch",_)-> error "Unexpected conclusion!" in + let nparams = mind_nparams rectype in + let getargs l = snd (chop_list nparams (snd (decomp_app l))) in + let rargs = getargs rhs + and largs = getargs lhs + in List.fold_right2 + solveArg largs rargs (tclTHEN h_simplest_left h_reflexivity) g +;; +\end{verbatim} + +Notice the use of a pattern to decompose the goal and obtain the +inductive type and the left and right hand sides of the equality. A +certain number of arguments correspond to the general parameters of +the type, and must be skipped over. Once the corresponding list of +arguments \texttt{rargs} and \texttt{largs} have been obtained, the +tactic \texttt{solveArg} is iterated on them, leaving a disjunction +whose left half can be solved by reflexivity. + +The following tactic joints together the three steps of the +proof procedure: + +\begin{verbatim} +let initialpatt = put_pat mmk "(x,y:?1){<?1>x=y}+{~(<?1>x=y)}" +;; +let decideGralEquality g = + let (typ::_) = try (dest_somatch (pf_concl g) initialpatt) + with UserError ("somatch",_) -> + error "The goal does not have the expected form" in + let headtyp = hd_app (pf_compute g typ) in + let rectype = match (kind_of_term headtyp) with + IsMutInd _ -> headtyp + | _ -> error ("This decision procedure only" + " works for inductive objects") + in (tclTHEN mkBranches + (tclORELSE h_solveRightBranch (solveLeftBranch rectype))) g +;; +;; +\end{verbatim} + +The tactic above can be specialized in two different ways: either to +decide a particular instance $\{c_1=c_2\}+\{\neg c_1=c_2\}$ of the +universal quantification; or to eliminate this property and obtain two +subgoals containing the hypotheses $c_1=c_2$ and $\neg c_1=c_2$ +respectively. + +\begin{verbatim} +let decideGralEquality = + (tclTHEN mkBranches (tclORELSE h_solveRightBranch solveLeftBranch)) +;; +let decideEquality c1 c2 g = + let rectype = pf_type_of g c1 in + let decide = mkGenDecideEqGoal rectype g + in (tclTHENS (cut decide) [default_auto;decideGralEquality]) g +;; +let compare c1 c2 g = + let rectype = pf_type_of g c1 in + let decide = mkDecideEqGoal rectype c1 c2 g + in (tclTHENS (cut decide) + [(tclTHEN intro + (tclTHEN (tclLAST_HYP simplest_case) + clear_last)); + decideEquality c1 c2]) g +;; +\end{verbatim} + +Next, for each of the tactics that will have an entry in the grammar +we construct the associated dynamic one to be registered in the table +of tactics. This function can be used to overload a tactic name with +several similar tactics. For example, the tactic proving the general +decidability property and the one proving a particular instance for +two terms can be grouped together with the following convention: if +the user provides two terms as arguments, then the specialized tactic +is used; if no argument is provided then the general tactic is invoked. + +\begin{verbatim} +let dyn_decideEquality args g = + match args with + [(COMMAND com1);(COMMAND com2)] -> + let c1 = pf_constr_of_com g com1 + and c2 = pf_constr_of_com g com2 + in decideEquality c1 c2 g + | [] -> decideGralEquality g + | _ -> error "Invalid arguments for dynamic tactic" +;; +add_tactic "DecideEquality" dyn_decideEquality +;; + +let dyn_compare args g = + match args with + [(COMMAND com1);(COMMAND com2)] -> + let c1 = pf_constr_of_com g com1 + and c2 = pf_constr_of_com g com2 + in compare c1 c2 g + | _ -> error "Invalid arguments for dynamic tactic" +;; +add_tactic "Compare" tacargs_compare +;; +\end{verbatim} + +This completes the implementation of the tactic. We turn now to the +\Coq file \texttt{Eqdecide.v}. + + +\subsection{The Grammar Rules} + +Associated to the implementation of the tactic there is a \Coq\ file +containing the grammar and pretty-printing rules for the new tactic, +and the commands to generate an object module that can be then loaded +dynamically during a \Coq\ session. In order to generate an ML module, +the \Coq\ file must contain a +\texttt{Declare ML module} command for all the \ocaml{} files concerning +the implementation of the tactic --in our case there is only one file, +the file \texttt{eqdecide.ml}: + +\begin{verbatim} +Declare ML Module "eqdecide". +\end{verbatim} + +The following grammar and pretty-printing rules are +self-explanatory. We refer the reader to the Section \ref{Grammar} for +the details: + +\begin{verbatim} +Grammar tactic simple_tactic := + EqDecideRuleG1 + [ "Decide" "Equality" comarg($com1) comarg($com2)] -> + [(DecideEquality $com1 $com2)] +| EqDecideRuleG2 + [ "Decide" "Equality" ] -> + [(DecideEquality)] +| CompareRule + [ "Compare" comarg($com1) comarg($com2)] -> + [(Compare $com1 $com2)]. + +Syntax tactic level 0: + EqDecideRulePP1 + [(DecideEquality)] -> + ["Decide" "Equality"] +| EqDecideRulePP2 + [(DecideEquality $com1 $com2)] -> + ["Decide" "Equality" $com1 $com2] +| ComparePP + [(Compare $com1 $com2)] -> + ["Compare" $com1 $com2]. +\end{verbatim} + + +\paragraph{Important:} The names used to label the abstract syntax tree +in the grammar rules ---in this case ``DecideEquality'' and +``Compare''--- must be the same as the name used to register the +tactic in the tactics table. This is what makes the links between the +input entered by the user and the tactic executed by the interpreter. + +\subsection{Loading the Tactic} + +Once the module \texttt{EqDecide.v} has been compiled, the tactic can +be dynamically loaded using the \texttt{Require} command. + +\begin{coq_example} +Require EqDecide. +Goal (x,y:nat){x=y}+{~x=y}. +Decide Equality. +\end{coq_example} + +The implementation of the tactic can be accessed through the +tactical \texttt{Info}: +\begin{coq_example} +Undo. +Info Decide Equality. +\end{coq_example} +\begin{coq_eval} +Abort. +\end{coq_eval} + +Remark that the task performed by the tactic \texttt{solveRightBranch} +is not displayed, since we have chosen to hide its implementation. + +\section{Testing and Debugging your Tactic} +\label{test-and-debug} + +When your tactic does not behave as expected, it is possible to trace +it dynamically from \Coq. In order to do this, you have first to leave +the toplevel of \Coq, and come back to the \ocaml{} interpreter. This can +be done using the command \texttt{Drop} (cf. Section \ref{Drop}). Once +in the \ocaml{} toplevel, load the file \texttt{tactics/include.ml}. +This file installs several pretty printers for proof trees, goals, +terms, abstract syntax trees, names, etc. It also contains the +function \texttt{go:unit -> unit} that enables to go back to \Coq's +toplevel. + +The modules \texttt{Tacmach} and \texttt{Pfedit} contain some basic +functions for extracting information from the state of the proof +engine. Such functions can be used to debug your tactic if +necessary. Let us mention here some of them: + +\begin{description} +\fun{val get\_pftreestate : unit -> pftreestate} + {Projects the current state of the proof engine.} +\fun{val proof\_of\_pftreestate : pftreestate -> proof} + {Projects the current state of the proof tree. A pretty-printer + displays it in a readable form. } +\fun{val top\_goal\_of\_pftreestate : pftreestate -> goal sigma} + {Projects the goal and the existential variables mapping from + the current state of the proof engine.} +\fun{val nth\_goal\_of\_pftreestate : int -> pftreestate -> goal sigma} + {Projects the goal and mapping corresponding to the $nth$ subgoal + that remains to be proven} +\fun{val traverse : int -> pftreestate -> pftreestate} + {Yields the children of the node that the current state of the + proof engine points to.} +\fun{val solve\_nth\_pftreestate : \\ \qquad +int -> tactic -> pftreestate -> pftreestate} + {\\ Provides the new state of the proof engine obtained applying + a given tactic to some unproven sub-goal.} +\end{description} + +Finally, the traditional \ocaml{} debugging tools like the directives +\texttt{trace} and \texttt{untrace} can be used to follow the +execution of your functions. Frequently, a better solution is to use +the \ocaml{} debugger, see Chapter \ref{Utilities}. + +\section{Concrete syntax for ML tactic and vernacular command} +\label{Notations-for-ML-command} + +\subsection{The general case} + +The standard way to bind an ML-written tactic or vernacular command to +a concrete {\Coq} syntax is to use the +\verb=TACTIC EXTEND= and \verb=VERNAC COMMAND EXTEND= macros. + +These macros can be used in any {\ocaml} file defining a (new) ML tactic +or vernacular command. They are expanded into pure {\ocaml} code by +the {\camlpppp} preprocessor of {\ocaml}. Concretely, files that use +these macros need to be compiled by giving to {\tt ocamlc} the option + +\verb=-pp "camlp4o -I $(COQTOP)/parsing grammar.cma pa_extend.cmo"= + +\noindent which is the default for every file compiled by means of a Makefile +generated by {\tt coq\_makefile} (cf chapter \ref {Addoc-coqc}). So, +just do \verb=make= in this latter case. + +The syntax of the macros is given on figure +\ref{EXTEND-syntax}. They can be used at any place of an {\ocaml} +files where an ML sentence (called \verb=str_item= in the {\tt ocamlc} +parser) is expected. For each rule, the left-hand-side describes the +grammar production and the right-hand-side its interpretation which +must be an {\ocaml} expression. Each grammar production starts with +the concrete name of the tactic or command in {\Coq} and is followed +by arguments, possibly separated by terminal symbols or words. +Here is an example: + +\begin{verbatim} +TACTIC EXTEND Replace + [ "replace" constr(c1) "with" constr(c2) ] -> [ replace c1 c2 ] +END +\end{verbatim} + +\newcommand{\grule}{\textrm{\textsl{rule}}} +\newcommand{\stritem}{\textrm{\textsl{ocaml\_str\_item}}} +\newcommand{\camlexpr}{\textrm{\textsl{ocaml\_expr}}} +\newcommand{\arginfo}{\textrm{\textsl{argument\_infos}}} +\newcommand{\lident}{\textrm{\textsl{lower\_ident}}} +\newcommand{\argument}{\textrm{\textsl{argument}}} +\newcommand{\entry}{\textrm{\textsl{entry}}} +\newcommand{\argtype}{\textrm{\textsl{argtype}}} + +\begin{figure} +\begin{tabular}{|lcll|} +\hline +{\stritem} + & ::= & +\multicolumn{2}{l|}{{\tt TACTIC EXTEND} {\ident} \nelist{\grule}{$|$} {\tt END}}\\ + & $|$ & \multicolumn{2}{l|}{{\tt VERNAC COMMAND EXTEND} {\ident} \nelist{\grule}{$|$} {\tt END}}\\ +&&\multicolumn{2}{l|}{}\\ +{\grule} & ::= & +\multicolumn{2}{l|}{{\tt [} {\str} \sequence{\argument}{} {\tt ] -> [} {\camlexpr} {\tt ]}}\\ +&&\multicolumn{2}{l|}{}\\ +{\argument} & ::= & {\str} &\mbox{(terminal)}\\ + & $|$ & {\entry} {\tt (} {\lident} {\tt )} &\mbox{(non-terminal)}\\ +&&\multicolumn{2}{l|}{}\\ +{\entry} + & ::= & {\tt string} & (a string)\\ + & $|$ & {\tt preident} & (an identifier typed as a {\tt string})\\ + & $|$ & {\tt ident} & (an identifier of type {\tt identifier})\\ + & $|$ & {\tt global} & (a qualified identifier)\\ + & $|$ & {\tt constr} & (a {\Coq} term)\\ + & $|$ & {\tt openconstr} & (a {\Coq} term with holes)\\ + & $|$ & {\tt sort} & (a {\Coq} sort)\\ + & $|$ & {\tt tactic} & (an ${\cal L}_{tac}$ expression)\\ + & $|$ & {\tt constr\_with\_bindings} & (a {\Coq} term with a list of bindings\footnote{as for the tactics {\tt apply} and {\tt elim}})\\ + & $|$ & {\tt int\_or\_var} & (an integer or an identifier denoting an integer)\\ + & $|$ & {\tt quantified\_hypothesis} & (a quantified hypothesis\footnote{as for the tactics {\tt intros until}})\\ + & $|$ & {\tt {\entry}\_opt} & (an optional {\entry} )\\ + & $|$ & {\tt ne\_{\entry}\_list} & (a non empty list of {\entry})\\ + & $|$ & {\tt {\entry}\_list} & (a list of {\entry})\\ + & $|$ & {\tt bool} & (a boolean: no grammar rule, just for typing)\\ + & $|$ & {\lident} & (a user-defined entry)\\ +\hline +\end{tabular} +\caption{Syntax of the macros binding {\ocaml} tactics or commands to a {\Coq} syntax} +\label{EXTEND-syntax} +\end{figure} + +There is a set of predefined non-terminal entries which are +automatically translated into an {\ocaml} object of a given type. The +type is not the same for tactics and for vernacular commands. It is +given in the following table: + +\begin{small} +\noindent \begin{tabular}{|l|l|l|} +\hline +{\entry} & {\it type for tactics} & {\it type for commands} \\ +{\tt string} & {\tt string} & {\tt string}\\ +{\tt preident} & {\tt string} & {\tt string}\\ +{\tt ident} & {\tt identifier} & {\tt identifier}\\ +{\tt global} & {\tt global\_reference} & {\tt qualid}\\ +{\tt constr} & {\tt constr} & {\tt constr\_expr}\\ +{\tt openconstr} & {\tt open\_constr} & {\tt constr\_expr}\\ +{\tt sort} & {\tt sorts} & {\tt rawsort}\\ +{\tt tactic} & {\tt glob\_tactic\_expr * tactic} & {\tt raw\_tactic\_expr}\\ +{\tt constr\_with\_bindings} & {\tt constr with\_bindings} & {\tt constr\_expr with\_bindings}\\\\ +{\tt int\_or\_var} & {\tt int or\_var} & {\tt int or\_var}\\ +{\tt quantified\_hypothesis} & {\tt quantified\_hypothesis} & {\tt quantified\_hypothesis}\\ +{\tt {\entry}\_opt} & {\it the type of entry} {\tt option} & {\it the type of entry} {\tt option}\\ +{\tt ne\_{\entry}\_list} & {\it the type of entry} {\tt list} & {\it the type of entry} {\tt list}\\ +{\tt {\entry}\_list} & {\it the type of entry} {\tt list} & {\it the type of entry} {\tt list}\\ +{\tt bool} & {\tt bool} & {\tt bool}\\ +{\lident} & {user-provided, cf next section} & {user-provided, cf next section}\\ +\hline +\end{tabular} +\end{small} + +\bigskip + +Notice that {\entry} consists in a single identifier and that the {\tt +\_opt}, {\tt \_list}, ... modifiers are part of the identifier. +Here is now another example of a tactic which takes either a non empty +list of identifiers and executes the {\ocaml} function {\tt subst} or +takes no arguments and executes the{\ocaml} function {\tt subst\_all}. + +\begin{verbatim} +TACTIC EXTEND Subst +| [ "subst" ne_ident_list(l) ] -> [ subst l ] +| [ "subst" ] -> [ subst_all ] +END +\end{verbatim} + +\subsection{Adding grammar entries for tactic or command arguments} + +In case parsing the arguments of the tactic or the vernacular command +involves grammar entries other than the predefined entries listed +above, you have to declare a new entry using the macros +\verb=ARGUMENT EXTEND= or \verb=VERNAC ARGUMENT EXTEND=. The syntax is +given on figure \ref{ARGUMENT-EXTEND-syntax}. Notice that arguments +declared by \verb=ARGUMENT EXTEND= can be used for arguments of both +tactics and vernacular commands while arguments declared by +\verb=VERNAC ARGUMENT EXTEND= can only be used by vernacular commands. + +For \verb=VERNAC ARGUMENT EXTEND=, the identifier is the name of the +entry and it must be a valid {\ocaml} identifier (especially it must +be lowercase). The grammar rules works as before except that they do +not have to start by a terminal symbol or word. As an example, here +is how the {\Coq} {\tt Extraction Language {\it language}} parses its +argument: + +\begin{verbatim} +VERNAC ARGUMENT EXTEND language +| [ "Ocaml" ] -> [ Ocaml ] +| [ "Haskell" ] -> [ Haskell ] +| [ "Scheme" ] -> [ Scheme ] +| [ "Toplevel" ] -> [ Toplevel ] +END +\end{verbatim} + +For tactic arguments, and especially for \verb=ARGUMENT EXTEND=, the +procedure is more subtle because tactics are objects of the {\Coq} +environment which can be printed and interpreted. Then the syntax +requires extra information providing a printer and a type telling how +the argument behaves. Here is an example of entry parsing a pair of +optional {\Coq} terms. + +\begin{verbatim} +let pp_minus_div_arg pr_constr pr_tactic (omin,odiv) = + if omin=None && odiv=None then mt() else + spc() ++ str "with" ++ + pr_opt (fun c -> str "minus := " ++ pr_constr c) omin ++ + pr_opt (fun c -> str "div := " ++ pr_constr c) odiv + +ARGUMENT EXTEND minus_div_arg + TYPED AS constr_opt * constr_opt + PRINTED BY pp_minus_div_arg +| [ "with" minusarg(m) divarg_opt(d) ] -> [ Some m, d ] +| [ "with" divarg(d) minusarg_opt(m) ] -> [ m, Some d ] +| [ ] -> [ None, None ] +END +\end{verbatim} + +Notice that the type {\tt constr\_opt * constr\_opt} tells that the +object behaves as a pair of optional {\Coq} terms, i.e. as an object +of {\ocaml} type {\tt constr option * constr option} if in a +\verb=TACTIC EXTEND= macro and of type {\tt constr\_expr option * +constr\_expr option} if in a \verb=VERNAC COMMAND EXTEND= macro. + +As for the printer, it must be a function expecting a printer for +terms, a printer for tactics and returning a printer for the created +argument. Especially, each sub-{\term} and each sub-{\tac} in the +argument must be typed by the corresponding printers. Otherwise, the +{\ocaml} code will not be well-typed. + +\Rem The entry {\tt bool} is bound to no syntax but it can be used to +give the type of an argument as in the following example: + +\begin{verbatim} +let pr_orient _prc _prt = function + | true -> mt () + | false -> str " <-" + +ARGUMENT EXTEND orient TYPED AS bool PRINTED BY pr_orient +| [ "->" ] -> [ true ] +| [ "<-" ] -> [ false ] +| [ ] -> [ true ] +END +\end{verbatim} + +\begin{figure} +\begin{tabular}{|lcl|} +\hline +{\stritem} & ::= & + {\tt ARGUMENT EXTEND} {\ident} {\arginfo} {\nelist{\grule}{$|$}} {\tt END}\\ +& $|$ & {\tt VERNAC ARGUMENT EXTEND} {\ident} {\nelist{\grule}{$|$}} {\tt END}\\ +\\ +{\arginfo} & ::= & {\tt TYPED AS} {\argtype} \\ +&& {\tt PRINTED BY} {\lident} \\ +%&& \zeroone{{\tt INTERPRETED BY} {\lident}}\\ +%&& \zeroone{{\tt GLOBALIZED BY} {\lident}}\\ +%&& \zeroone{{\tt SUBSTITUTED BY} {\lident}}\\ +%&& \zeroone{{\tt RAW\_TYPED AS} {\lident} {\tt RAW\_PRINTED BY} {\lident}}\\ +%&& \zeroone{{\tt GLOB\_TYPED AS} {\lident} {\tt GLOB\_PRINTED BY} {\lident}}\\ +\\ +{\argtype} & ::= & {\argtype} {\tt *} {\argtype} \\ +& $|$ & {\entry} \\ +\hline +\end{tabular} +\caption{Syntax of the macros binding {\ocaml} tactics or commands to a {\Coq} syntax} +\label{ARGUMENT-EXTEND-syntax} +\end{figure} + +%\end{document} |