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.
