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 works for hash tables but also for a single integer (the Undo stack size, modified by the Set Undo command, for example).

10.4.3 The right way to access to Coq constants from your ML code

With their long names, Coq constants are stored using:

The identifier is exactly the identifier that is used in Coq to denote the constant; the section path can be known using the Locate command:

Coq <   Locate S.
#Datatypes#nat.cci

Coq <   Locate nat.
#Datatypes#nat.cci

Coq <   Locate eq.
#Logic#eq.cci

Now it is easy to get a constant by its name and section path:

let constant sp id = 
  Machops.global_reference (Names.gLOB (Termenv.initial_sign ())) 
    (Names.path_of_string sp) (Names.id_of_string id);;
The only issue is that if one cannot put:

let coq_S = constant "#Datatypes#nat.cci" "S";;
in his tactic's code. That is because this sentence is evaluated before the module Datatypes is loaded. The solution is to use the lazy evaluation of Objective Caml:

let coq_S = lazy (constant "#Datatypes#nat.cci" "S");;

... (Lazy.force coq_S) ...
Be sure to call always Lazy.force behind a closure -- i.e. inside a function body or behind the lazy keyword.

One can see examples of that technique in the source code of Coq, for example tactics/contrib/polynom/ring.ml or tactics/contrib/polynom/coq_omega.ml.