Merge pull request #8778 from SkySkimmer/merge-plugin-tuto

Move plugin tutorial to Coq repo

1 files changed, 375 insertions, 0 deletions

diff --git a/doc/plugin_tutorial/tuto2/src/demo.mlg b/doc/plugin_tutorial/tuto2/src/demo.mlg
new file mode 100644
index 0000000000..966c05acdc
--- /dev/null
+++ b/doc/plugin_tutorial/tuto2/src/demo.mlg
@@ -0,0 +1,375 @@
+(* -------------------------------------------------------------------------- *)
+(*                                                                            *)
+(*                            Initial ritual dance                            *)
+(*                                                                            *)
+(* -------------------------------------------------------------------------- *)
+
+DECLARE PLUGIN "demo_plugin"
+
+(*
+   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_plugin".
+   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_plugin".
+
+   (2) The above command will succeed only if there is "demo_plugin.cmxs"
+       in some of the directories that Coq is supposed to look
+       (i.e. the ones we specified via "-I ..." command line options).
+
+   (3) The file "demo_plugin.mlpack" lists the OCaml modules to be linked in
+       "demo_plugin.cmxs".
+
+   (4) The file "demo_plugin.mlpack" as well as all .ml, .mli and .mlg files
+       are listed in the "_CoqProject" file.
+*)
+
+(* -------------------------------------------------------------------------- *)
+(*                                                                            *)
+(*                 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:
+
+     { () }
+
+   Similarly to the 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 (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