Update, expand, and document plugin tutorial 2

1 files changed, 0 insertions, 375 deletions

diff --git a/doc/plugin_tutorial/tuto2/src/demo.mlg b/doc/plugin_tutorial/tuto2/src/demo.mlg
deleted file mode 100644
index 966c05acdc..0000000000
--- a/doc/plugin_tutorial/tuto2/src/demo.mlg
+++ /dev/null
@@ -1,375 +0,0 @@
-(* -------------------------------------------------------------------------- *)
-(*                                                                            *)
-(*                            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