This example was sent to me by Matej Kosik, in preparation for a Coq Implementors Workshop.<\/p>\n
\r\n(* -------------------------------------------------------------------------- *)\r\n(* *)\r\n(* Initial ritual dance *)\r\n(* *)\r\n(* -------------------------------------------------------------------------- *)\r\n\r\nDECLARE PLUGIN \"demo\"\r\n\r\n(*\r\n Use this macro before any of the other Ocaml macros.\r\n\r\n Each plugin has a unique name.\r\n We have decided to name this plugin as \"demo\".\r\n That means that:\r\n \r\n (1) If we want to load this particular plugin to Coq toplevel,\r\n we must use the following command.\r\n\r\n Declare ML Module \"demo\".\r\n\r\n (2) The above command will succeed only if there is \"demo.cmxs\"\r\n in some of the directories that Coq is supposed to look\r\n (i.e. the ones we specified via \"-I ...\" command line options).\r\n*)\r\n\r\n(* -------------------------------------------------------------------------- *)\r\n(* *)\r\n(* How to define a new Vernacular command? *)\r\n(* *)\r\n(* -------------------------------------------------------------------------- *)\r\n\r\nVERNAC COMMAND EXTEND Cmd1 CLASSIFIED AS QUERY\r\n [ \"Cmd1\" ] -> [ () ]\r\nEND\r\n\r\n(*\r\n These:\r\n\r\n VERNAC COMMAND EXTEND\r\n\r\n and\r\n\r\n END\r\n\r\n mark the beginning and the end of the definition of a new Vernacular command.\r\n\r\n Cmd1 is a unique identifier (which must start with an upper-case letter)\r\n associated with the new Vernacular command we are defining.\r\n\r\n CLASSIFIED AS QUERY tells Coq that the new Vernacular command:\r\n - changes neither the global environment\r\n - nor does it modify the plugin's state.\r\n\r\n If the new command could:\r\n - change the global environment\r\n - or modify a plugin's state\r\n then one would have to use CLASSIFIED AS SIDEFF instead.\r\n\r\n This:\r\n\r\n [ \"Cmd1\" ] -> [ () ]\r\n\r\n defines:\r\n - the parsing rule\r\n - the interpretation rule\r\n\r\n The parsing rule and the interpretation rule are separated by -> token.\r\n\r\n The parsing rule, in this case, is:\r\n\r\n [ \"Cmd1\" ]\r\n\r\n By convention, all vernacular command start with an upper-case letter.\r\n\r\n The [ and ] characters mark the beginning and the end of the parsing rule.\r\n The parsing rule itself says that the syntax of the newly defined command\r\n is composed from a single terminal Cmd1.\r\n \r\n The interpretation rule, in this case, is:\r\n\r\n [ () ]\r\n\r\n Like in case of the parsing rule,\r\n [ and ] characters mark the beginning and the end of the interpretation rule.\r\n In this case, the following Ocaml expression:\r\n\r\n ()\r\n\r\n defines the effect of the Vernacular command we have just defined.\r\n That is, it behaves is no-op.\r\n*)\r\n\r\n(* -------------------------------------------------------------------------- *)\r\n(* *)\r\n(* How to define a new Vernacular command with some terminal parameters? *)\r\n(* *)\r\n(* -------------------------------------------------------------------------- *)\r\n\r\nVERNAC COMMAND EXTEND Cmd2 CLASSIFIED AS QUERY\r\n [ \"Cmd2\" \"With\" \"Some\" \"Terminal\" \"Parameters\" ] -> [ () ]\r\nEND\r\n\r\n(*\r\n As shown above, the Vernacular command can be composed from\r\n any number of terminals.\r\n\r\n By convention, each of these terminals starts with an upper-case letter.\r\n*)\r\n\r\n(* -------------------------------------------------------------------------- *)\r\n(* *)\r\n(* How to define a new Vernacular command with some non-terminal parameter? *)\r\n(* *)\r\n(* -------------------------------------------------------------------------- *)\r\n\r\nopen Stdarg\r\n\r\nVERNAC COMMAND EXTEND Cmd3 CLASSIFIED AS QUERY\r\n [ \"Cmd3\" int(i) ] -> [ () ]\r\nEND\r\n\r\n(*\r\n This:\r\n\r\n open Stdarg\r\n\r\n is needed as some identifiers in the Ocaml code generated by the\r\n\r\n VERNAC COMMAND EXTEND ... END\r\n\r\n macros are not fully qualified.\r\n\r\n This:\r\n\r\n int(i)\r\n\r\n means that the new command is expected to be followed by an integer.\r\n The integer is bound in the parsing rule to variable i.\r\n This variable i then can be used in the interpretation rule.\r\n\r\n To see value of which Ocaml types can be bound this way,\r\n look at the wit_* function declared in interp\/stdarg.mli\r\n (in the Coq's codebase).\r\n \r\n If we drop the wit_ prefix, we will get the token\r\n that we can use in the parsing rule.\r\n That is, since there exists wit_int, we know that\r\n we can write:\r\n\r\n int(i)\r\n\r\n By looking at the signature of the wit_int function:\r\n\r\n val wit_int : int uniform_genarg_type\r\n\r\n we also know that variable i will have the type int.\r\n\r\n The types of wit_* functions are either:\r\n\r\n 'c uniform_genarg_type\r\n\r\n or\r\n\r\n ('a,'b,'c) genarg_type\r\n\r\n In both cases, the bound variable will have type 'c.\r\n*)\r\n\r\n(* -------------------------------------------------------------------------- *)\r\n(* *)\r\n(* How to define a new Vernacular command with variable number of arguments? *)\r\n(* *)\r\n(* -------------------------------------------------------------------------- *)\r\n\r\nVERNAC COMMAND EXTEND Cmd4 CLASSIFIED AS QUERY\r\n [ \"Cmd4\" int_list(l) ] -> [ () ]\r\nEND\r\n\r\n(*\r\n This:\r\n\r\n int_list(l)\r\n\r\n means that the new Vernacular command is expected to be followed\r\n by a (whitespace separated) list of integers.\r\n This list of integers is bound to the indicated l.\r\n \r\n In this case, as well as in the cases we point out below, instead of int\r\n in int_list we could use any other supported type, e.g. ident, bool, ...\r\n \r\n To see which other Ocaml type constructors (in addition to list)\r\n are supported, have a look at the parse_user_entry function defined\r\n in grammar\/q_util.mlp file.\r\n \r\n E.g.:\r\n - ne_int_list(x) would represent a non-empty list of integers,\r\n - int_list(x) would represent a list of integers,\r\n - int_opt(x) would represent a value of type int option,\r\n - \u00b7\u00b7\u00b7\r\n*)\r\n\r\n(* -------------------------------------------------------------------------- *)\r\n(* *)\r\n(* How to define a new Vernacular command that takes values of a custom type? *)\r\n(* *)\r\n(* -------------------------------------------------------------------------- *)\r\n\r\nopen Ltac_plugin\r\n\r\n(*\r\n If we want to avoid a compilation failure\r\n\r\n \"no implementation available for Tacenv\"\r\n\r\n then we have to open the Ltac_plugin module.\r\n*)\r\n\r\n(*\r\n Pp module must be opened because some of the macros that are part of the API\r\n do not expand to fully qualified names.\r\n*)\r\n\r\ntype type_5 = Foo_5 | Bar_5\r\n\r\n(*\r\n We define a type of values that we want to pass to our Vernacular command.\r\n*)\r\n\r\n(*\r\n By default, we are able to define new Vernacular commands that can take\r\n parameters of some of the supported types. Which types are supported,\r\n that was discussed earlier.\r\n\r\n If we want to be able to define Vernacular command that takes parameters\r\n of a type that is not supported by default, we must use the following macro:\r\n*)\r\n\r\nopen Pp\r\n\r\nVERNAC ARGUMENT EXTEND custom5\r\n| [ \"Foo_5\" ] -> [ Foo_5 ]\r\n| [ \"Bar_5\" ] -> [ Bar_5 ]\r\nEND\r\n\r\n(*\r\n where:\r\n\r\n custom5\r\n\r\n indicates that, from now on, in our parsing rules we can write:\r\n\r\n custom5(some_variable)\r\n\r\n in those places where we expect user to provide an input\r\n that can be parsed by the parsing rules above\r\n (and interpreted by the interpretations rules above).\r\n*)\r\n\r\n(* Here: *)\r\n\r\nVERNAC COMMAND EXTEND Cmd5 CLASSIFIED AS QUERY\r\n [ \"Cmd5\" custom5(x) ] -> [ () ]\r\nEND\r\n\r\n(*\r\n we define a new Vernacular command whose parameters, provided by the user,\r\n can be mapped to values of type_5.\r\n*)\r\n\r\n(* -------------------------------------------------------------------------- *)\r\n(* *)\r\n(* How to give a feedback to the user? *)\r\n(* *)\r\n(* -------------------------------------------------------------------------- *)\r\n\r\nVERNAC COMMAND EXTEND Cmd6 CLASSIFIED AS QUERY\r\n [ \"Cmd6\" ] -> [ Feedback.msg_notice ?loc (Pp.str \"Everything is awesome!\") ]\r\nEND\r\n\r\n(*\r\n The following functions:\r\n\r\n - Feedback.msg_info : Pp.t -> unit\r\n - Feedback.msg_notice : Pp.t -> unit\r\n - Feedback.msg_warning : Pp.t -> unit\r\n - Feedback.msg_error : Pp.t -> unit\r\n - Feedback.msg_debug : Pp.t -> unit\r\n\r\n enable us to give user a textual feedback.\r\n\r\n Pp module enable us to represent and construct pretty-printing instructions.\r\n The concepts defined and the services provided by the Pp module are in\r\n various respects related to the concepts and services provided\r\n by the Format module that is part of the Ocaml standard library.\r\n*)\r\n\r\n(* -------------------------------------------------------------------------- *)\r\n(* *)\r\n(* How to implement a Vernacular command with (undoable) side-effects? *)\r\n(* *)\r\n(* -------------------------------------------------------------------------- *)\r\n\r\nopen Summary.Local\r\n\r\n(*\r\n By opening Summary.Local module we shadow the original functions\r\n that we traditionally use for implementing stateful behavior.\r\n\r\n ref\r\n !\r\n :=\r\n\r\n are now shadowed by their counterparts in Summary.Local. *)\r\n\r\nlet counter = ref ~name:\"counter\" 0\r\n\r\nVERNAC COMMAND EXTEND Cmd7 CLASSIFIED AS SIDEFF\r\n [ \"Cmd7\" ] -> [ counter := succ !counter;\r\n Feedback.msg_notice (Pp.str \"counter = \" ++ Pp.str (string_of_int (!counter))) ]\r\nEND\r\n\r\nTACTIC EXTEND tactic1\r\n [ \"tactic1\" ] -> [ Proofview.tclUNIT () ]\r\nEND\r\n\r\n(* ---- *)\r\n\r\ntype custom = Foo_2 | Bar_2\r\n\r\nlet pr_custom _ _ _ = function\r\n | Foo_2 -> Pp.str \"Foo_2\"\r\n | Bar_2 -> Pp.str \"Bar_2\"\r\n\r\nARGUMENT EXTEND custom2 PRINTED BY pr_custom\r\n| [ \"Foo_2\" ] -> [ Foo_2 ]\r\n| [ \"Bar_2\" ] -> [ Bar_2 ]\r\nEND\r\n\r\nTACTIC EXTEND tactic2\r\n [ \"tactic2\" custom2(x) ] -> [ Proofview.tclUNIT () ]\r\nEND\r\n<\/pre>\nOnce compiled this code can be used in the following Coq example.<\/p>\n
\r\nDeclare ML Module \"demo\".\r\n\r\nCmd1.\r\nCmd2 With Some Terminal Parameters.\r\nCmd3 42.\r\nCmd4 100 200 300 400.\r\nCmd5 Foo_5.\r\nCmd5 Bar_5.\r\nCmd6.\r\nCmd7.\r\nCmd7.\r\nCmd7.\r\n\r\nGoal True.\r\nProof.\r\n tactic1.\r\n tactic2 Foo_2.\r\n tactic2 Bar_2.\r\nAbort.\r\n<\/pre>\n","protected":false},"excerpt":{"rendered":"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\u2026<\/p>\n