10.4 The tactic writer mini-HOWTO

10.4.1 How to add a vernacular command

The command to register a vernacular command can be found in module Vernacinterp:

val vinterp_add : string * (vernac_arg list -> unit -> unit) -> unit;;
The first argument is the name, the second argument is a function that parses the arguments and returns a function of type unit®unit that do the job.

In this section we will show how to add a vernacular command CheckCheck that print a type of a term and the type of its type.

File dcheck.ml:

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")
;;
Like for a new tactic, a new syntax entry must be created.

File DCheck.v:

Declare ML Module "dcheck.ml".

Grammar vernac vernac := 
  dblcheck [ "CheckCheck" comarg($c) ] -> [(DblCheck $c)].
We are now able to test our new command:

Coq < Require DCheck.
Coq < CheckCheck O.
O:nat:Set
Most Coq vernacular commands are registered in the module src/env/vernacentries.ml. One can see more examples here.

10.4.2 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 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 src/proofs/macros.ml (which implements the Tactic Definition command). Tactic macros are stored in the imperative hashtable 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 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 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 mactab

So, now, we can say that mactab is synchronous with the Reset mechanismTM.

Notice that this wonstrl_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 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.

10.3.5 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 tactics and 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 tactics, since they make use of the propositional equality type. Those tactics which are independent from the context --like for example Cut, Intros, etc-- are defined in the directory src/tactics. This latter directory also contains some useful tools for programming new tactics, referred in Section 10.5.

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.

Basic Tactics

The file Tactics contain the implementation of the basic tactics provided by Coq. The following tactics are some of the most used ones: