diff options
Diffstat (limited to 'doc/plugin_tutorial/tuto2/src/demo.mlg')
| -rw-r--r-- | doc/plugin_tutorial/tuto2/src/demo.mlg | 375 |
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 |