A small tutorial for Ocaml plugins to extend the Coq system

This example was sent to me by Matej Kosik, in preparation for a Coq Implementors Workshop.

(* -------------------------------------------------------------------------- *)
(*                                                                            *)
(*                            Initial ritual dance                            *)
(*                                                                            *)
(* -------------------------------------------------------------------------- *)

DECLARE PLUGIN "demo"

(*
   Use this macro before any of the other Ocaml macros.

   Each plugin has a unique name.
   We have decided to name this plugin as "demo".
   That means that:
   
   (1) If we want to load this particular plugin to Coq toplevel,
       we must use the following command.

         Declare ML Module "demo".

   (2) The above command will succeed only if there is "demo.cmxs"
       in some of the directories that Coq is supposed to look
       (i.e. the ones we specified via "-I ..." command line options).
*)

(* -------------------------------------------------------------------------- *)
(*                                                                            *)
(*                 How to define a new Vernacular command?                    *)
(*                                                                            *)
(* -------------------------------------------------------------------------- *)

VERNAC COMMAND EXTEND Cmd1 CLASSIFIED AS QUERY
  [ "Cmd1" ] -> [ () ]
END

(*
   These:

     VERNAC COMMAND EXTEND

   and

     END

   mark the beginning and the end of the definition of a new Vernacular command.

   Cmd1 is a unique identifier (which must start with an upper-case letter)
   associated with the new Vernacular command we are defining.

   CLASSIFIED AS QUERY tells Coq that the new Vernacular command:
   - changes neither the global environment
   - nor does it modify the plugin's state.

   If the new command could:
   - change the global environment
   - or modify a plugin's state
   then one would have to use CLASSIFIED AS SIDEFF instead.

   This:

     [ "Cmd1" ] -> [ () ]

   defines:
   - the parsing rule
   - the interpretation rule

   The parsing rule and the interpretation rule are separated by -> token.

   The parsing rule, in this case, is:

     [ "Cmd1" ]

   By convention, all vernacular command start with an upper-case letter.

   The [ and ] characters mark the beginning and the end of the parsing rule.
   The parsing rule itself says that the syntax of the newly defined command
   is composed from a single terminal Cmd1.
   
   The interpretation rule, in this case, is:

     [ () ]

   Like in case of the parsing rule,
   [ and ] characters mark the beginning and the end of the interpretation rule.
   In this case, the following Ocaml expression:

     ()

   defines the effect of the Vernacular command we have just defined.
   That is, it behaves is no-op.
*)

(* -------------------------------------------------------------------------- *)
(*                                                                            *)
(*   How to define a new Vernacular command with some terminal parameters?    *)
(*                                                                            *)
(* -------------------------------------------------------------------------- *)

VERNAC COMMAND EXTEND Cmd2 CLASSIFIED AS QUERY
  [ "Cmd2" "With" "Some" "Terminal" "Parameters" ] -> [ () ]
END

(*
   As shown above, the Vernacular command can be composed from
   any number of terminals.

   By convention, each of these terminals starts with an upper-case letter.
*)

(* -------------------------------------------------------------------------- *)
(*                                                                            *)
(*  How to define a new Vernacular command with some non-terminal parameter?  *)
(*                                                                            *)
(* -------------------------------------------------------------------------- *)

open Stdarg

VERNAC COMMAND EXTEND Cmd3 CLASSIFIED AS QUERY
  [ "Cmd3" int(i) ] -> [ () ]
END

(*
   This:

     open Stdarg

   is needed as some identifiers in the Ocaml code generated by the

     VERNAC COMMAND EXTEND ... END

   macros are not fully qualified.

   This:

     int(i)

   means that the new command is expected to be followed by an integer.
   The integer is bound in the parsing rule to variable i.
   This variable i then can be used in the interpretation rule.

   To see value of which Ocaml types can be bound this way,
   look at the wit_* function declared in interp/stdarg.mli
   (in the Coq's codebase).
   
   If we drop the wit_ prefix, we will get the token
   that we can use in the parsing rule.
   That is, since there exists wit_int, we know that
   we can write:

     int(i)

   By looking at the signature of the wit_int function:

     val wit_int : int uniform_genarg_type

   we also know that variable i will have the type int.

   The types of wit_* functions are either:

     'c uniform_genarg_type

   or

     ('a,'b,'c) genarg_type

   In both cases, the bound variable will have type 'c.
*)

(* -------------------------------------------------------------------------- *)
(*                                                                            *)
(* How to define a new Vernacular command with variable number of arguments?  *)
(*                                                                            *)
(* -------------------------------------------------------------------------- *)

VERNAC COMMAND EXTEND Cmd4 CLASSIFIED AS QUERY
  [ "Cmd4" int_list(l) ] -> [ () ]
END

(*
   This:

     int_list(l)

   means that the new Vernacular command is expected to be followed
   by a (whitespace separated) list of integers.
   This list of integers is bound to the indicated l.
   
   In this case, as well as in the cases we point out below, instead of int
   in int_list we could use any other supported type, e.g. ident, bool, ...
   
   To see which other Ocaml type constructors (in addition to list)
   are supported, have a look at the parse_user_entry function defined
   in grammar/q_util.mlp file.
   
   E.g.:
   - ne_int_list(x) would represent a non-empty list of integers,
   - int_list(x) would represent a list of integers,
   - int_opt(x) would represent a value of type int option,
   - ···
*)

(* -------------------------------------------------------------------------- *)
(*                                                                            *)
(* How to define a new Vernacular command that takes values of a custom type? *)
(*                                                                            *)
(* -------------------------------------------------------------------------- *)

open Ltac_plugin

(*
   If we want to avoid a compilation failure

     "no implementation available for Tacenv"

   then we have to open the Ltac_plugin module.
*)

(*
   Pp module must be opened because some of the macros that are part of the API
   do not expand to fully qualified names.
*)

type type_5 = Foo_5 | Bar_5

(*
   We define a type of values that we want to pass to our Vernacular command.
*)

(*
   By default, we are able to define new Vernacular commands that can take
   parameters of some of the supported types. Which types are supported,
   that was discussed earlier.

   If we want to be able to define Vernacular command that takes parameters
   of a type that is not supported by default, we must use the following macro:
*)

open Pp

VERNAC ARGUMENT EXTEND custom5
| [ "Foo_5" ] -> [ Foo_5 ]
| [ "Bar_5" ] -> [ Bar_5 ]
END

(*
   where:

     custom5

   indicates that, from now on, in our parsing rules we can write:

     custom5(some_variable)

   in those places where we expect user to provide an input
   that can be parsed by the parsing rules above
   (and interpreted by the interpretations rules above).
*)

(* Here: *)

VERNAC COMMAND EXTEND Cmd5 CLASSIFIED AS QUERY
  [ "Cmd5" custom5(x) ] -> [ () ]
END

(*
   we define a new Vernacular command whose parameters, provided by the user,
   can be mapped to values of type_5.
*)

(* -------------------------------------------------------------------------- *)
(*                                                                            *)
(*                     How to give a feedback to the user?                    *)
(*                                                                            *)
(* -------------------------------------------------------------------------- *)

VERNAC COMMAND EXTEND Cmd6 CLASSIFIED AS QUERY
  [ "Cmd6" ] -> [ Feedback.msg_notice ?loc (Pp.str "Everything is awesome!") ]
END

(*
   The following functions:

     - Feedback.msg_info    : Pp.t -> unit
     - Feedback.msg_notice  : Pp.t -> unit
     - Feedback.msg_warning : Pp.t -> unit
     - Feedback.msg_error   : Pp.t -> unit
     - Feedback.msg_debug   : Pp.t -> unit

   enable us to give user a textual feedback.

   Pp module enable us to represent and construct pretty-printing instructions.
   The concepts defined and the services provided by the Pp module are in
   various respects related to the concepts and services provided
   by the Format module that is part of the Ocaml standard library.
*)

(* -------------------------------------------------------------------------- *)
(*                                                                            *)
(*    How to implement a Vernacular command with (undoable) side-effects?     *)
(*                                                                            *)
(* -------------------------------------------------------------------------- *)

open Summary.Local

(*
   By opening Summary.Local module we shadow the original functions
   that we traditionally use for implementing stateful behavior.

     ref
     !
     :=

   are now shadowed by their counterparts in Summary.Local. *)

let counter = ref ~name:"counter" 0

VERNAC COMMAND EXTEND Cmd7 CLASSIFIED AS SIDEFF
  [ "Cmd7" ] -> [ counter := succ !counter;
                  Feedback.msg_notice (Pp.str "counter = " ++ Pp.str (string_of_int (!counter))) ]
END

TACTIC EXTEND tactic1
  [ "tactic1" ] -> [ Proofview.tclUNIT () ]
END

(* ---- *)

type custom = Foo_2 | Bar_2

let pr_custom _ _ _ = function
  | Foo_2 -> Pp.str "Foo_2"
  | Bar_2 -> Pp.str "Bar_2"

ARGUMENT EXTEND custom2 PRINTED BY pr_custom
| [ "Foo_2" ] -> [ Foo_2 ]
| [ "Bar_2" ] -> [ Bar_2 ]
END

TACTIC EXTEND tactic2
  [ "tactic2" custom2(x) ] -> [ Proofview.tclUNIT () ]
END

Once compiled this code can be used in the following Coq example.

Declare ML Module "demo".

Cmd1.
Cmd2 With Some Terminal Parameters.
Cmd3 42.
Cmd4 100 200 300 400.
Cmd5 Foo_5.
Cmd5 Bar_5.
Cmd6.
Cmd7.
Cmd7.
Cmd7.

Goal True.
Proof.
  tactic1.
  tactic2 Foo_2.
  tactic2 Bar_2.
Abort.

Leave a Reply

Your email address will not be published.