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:
-
a section path
- an identifier
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
.