From 0fe2b5d4d63bcbc63d48a386949094c23e4c274e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 31 Oct 2018 17:57:47 +0100 Subject: Port to coqpp. --- tuto0/_CoqProject | 2 +- tuto0/src/g_tuto0.ml4 | 14 -- tuto0/src/g_tuto0.mlg | 18 +++ tuto1/_CoqProject | 4 +- tuto1/src/g_tuto1.ml4 | 149 -------------------- tuto1/src/g_tuto1.mlg | 154 +++++++++++++++++++++ tuto2/_CoqProject | 2 +- tuto2/src/demo.ml4 | 347 ---------------------------------------------- tuto2/src/demo.mlg | 375 ++++++++++++++++++++++++++++++++++++++++++++++++++ tuto3/_CoqProject | 4 +- tuto3/src/g_tuto3.ml4 | 42 ------ tuto3/src/g_tuto3.mlg | 46 +++++++ 12 files changed, 599 insertions(+), 558 deletions(-) delete mode 100644 tuto0/src/g_tuto0.ml4 create mode 100644 tuto0/src/g_tuto0.mlg delete mode 100644 tuto1/src/g_tuto1.ml4 create mode 100644 tuto1/src/g_tuto1.mlg delete mode 100644 tuto2/src/demo.ml4 create mode 100644 tuto2/src/demo.mlg delete mode 100644 tuto3/src/g_tuto3.ml4 create mode 100644 tuto3/src/g_tuto3.mlg diff --git a/tuto0/_CoqProject b/tuto0/_CoqProject index dd93e1fa79..76368e3ac7 100644 --- a/tuto0/_CoqProject +++ b/tuto0/_CoqProject @@ -6,5 +6,5 @@ theories/Demo.v src/tuto0_main.ml src/tuto0_main.mli -src/g_tuto0.ml4 +src/g_tuto0.mlg src/tuto0_plugin.mlpack diff --git a/tuto0/src/g_tuto0.ml4 b/tuto0/src/g_tuto0.ml4 deleted file mode 100644 index d6e95ba0f7..0000000000 --- a/tuto0/src/g_tuto0.ml4 +++ /dev/null @@ -1,14 +0,0 @@ -DECLARE PLUGIN "tuto0_plugin" - -open Pp -open Ltac_plugin - -VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY -| [ "HelloWorld" ] -> [ Feedback.msg_notice (strbrk Tuto0_main.message) ] -END - -TACTIC EXTEND hello_world_tactic -| [ "hello_world" ] -> - [ let _ = Feedback.msg_notice (str Tuto0_main.message) in - Tacticals.New.tclIDTAC ] -END diff --git a/tuto0/src/g_tuto0.mlg b/tuto0/src/g_tuto0.mlg new file mode 100644 index 0000000000..5c633fe862 --- /dev/null +++ b/tuto0/src/g_tuto0.mlg @@ -0,0 +1,18 @@ +DECLARE PLUGIN "tuto0_plugin" + +{ + +open Pp +open Ltac_plugin + +} + +VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY +| [ "HelloWorld" ] -> { Feedback.msg_notice (strbrk Tuto0_main.message) } +END + +TACTIC EXTEND hello_world_tactic +| [ "hello_world" ] -> + { let _ = Feedback.msg_notice (str Tuto0_main.message) in + Tacticals.New.tclIDTAC } +END diff --git a/tuto1/_CoqProject b/tuto1/_CoqProject index ce14ee2b87..585d1360be 100644 --- a/tuto1/_CoqProject +++ b/tuto1/_CoqProject @@ -9,5 +9,5 @@ src/simple_declare.mli src/simple_declare.ml src/simple_print.ml src/simple_print.mli -src/g_tuto1.ml4 -src/tuto1_plugin.mlpack \ No newline at end of file +src/g_tuto1.mlg +src/tuto1_plugin.mlpack diff --git a/tuto1/src/g_tuto1.ml4 b/tuto1/src/g_tuto1.ml4 deleted file mode 100644 index 1f4660d1f0..0000000000 --- a/tuto1/src/g_tuto1.ml4 +++ /dev/null @@ -1,149 +0,0 @@ -DECLARE PLUGIN "tuto1_plugin" - -(* If we forget this line and include our own tactic definition using - TACTIC EXTEND, as below, then we get the strange error message - no implementation available for Tacentries, only when compiling - theories/Loader.v -*) -open Ltac_plugin -open Pp -(* This module defines the types of arguments to be used in the - EXTEND directives below, for example the string one. *) -open Stdarg - -VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY -| [ "Hello" string(s) ] -> - [ Feedback.msg_notice (strbrk "Hello " ++ str s) ] -END - -(* reference is allowed as a syntactic entry, but so are all the entries - found the signature of module Prim in file coq/parsing/pcoq.mli *) - -VERNAC COMMAND EXTEND HelloAgain CLASSIFIED AS QUERY -| [ "HelloAgain" reference(r)] -> -(* The function Ppconstr.pr_qualid was found by searching all mli files - for a function of type qualid -> Pp.t *) - [ Feedback.msg_notice - (strbrk "Hello again " ++ Ppconstr.pr_qualid r)] -END - -(* According to parsing/pcoq.mli, e has type constr_expr *) -(* this type is defined in pretyping/constrexpr.ml *) -(* Question for the developers: why is the file constrexpr.ml and not - constrexpr.mli --> Easier for packing the software in components. *) -VERNAC COMMAND EXTEND TakingConstr CLASSIFIED AS QUERY -| [ "Cmd1" constr(e) ] -> - [ let _ = e in Feedback.msg_notice (strbrk "Cmd1 parsed something") ] -END - -(* The next step is to make something of parsed expression. - Interesting information in interp/constrintern.mli *) - -(* There are several phases of transforming a parsed expression into - the final internal data-type (constr). There exists a collection of - functions that combine all the phases *) - -VERNAC COMMAND EXTEND TakingConstr2 CLASSIFIED AS QUERY -| [ "Cmd2" constr(e) ] -> - [ let _ = Constrintern.interp_constr - (Global.env()) - (* Make sure you don't use Evd.empty here, as this does not - check consistency with existing universe constraints. *) - (Evd.from_env (Global.env())) e in - Feedback.msg_notice (strbrk "Cmd2 parsed something legitimate") ] -END - -(* This is to show what happens when typing in an empty environment - with an empty evd. - Question for the developers: why does "Cmd3 (fun x : nat => x)." - raise an anomaly, not the same error as "Cmd3 (fun x : a => x)." *) - -VERNAC COMMAND EXTEND TakingConstr3 CLASSIFIED AS QUERY -| [ "Cmd3" constr(e) ] -> - [ let _ = Constrintern.interp_constr Environ.empty_env - Evd.empty e in - Feedback.msg_notice - (strbrk "Cmd3 accepted something in the empty context")] -END - -(* When adding a definition, we have to be careful that just - the operation of constructing a well-typed term may already change - the environment, at the level of universe constraints (which - are recorded in the evd component). The function - Constrintern.interp_constr ignores this side-effect, so it should - not be used here. *) - -(* Looking at the interface file interp/constrintern.ml4, I lost - some time because I did not see that the "constr" type appearing - there was "EConstr.constr" and not "Constr.constr". *) - -VERNAC COMMAND EXTEND Define1 CLASSIFIED AS SIDEFF -| [ "Cmd4" ident(i) constr(e) ] -> - [ let v = Constrintern.interp_constr (Global.env()) - (Evd.from_env (Global.env())) e in - Simple_declare.packed_declare_definition ~poly:(Attributes.(parse polymorphic atts)) i v ] -END - -VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY -| [ "Cmd5" constr(e) ] -> - [ let v = Constrintern.interp_constr (Global.env()) - (Evd.from_env (Global.env())) e in - let (_, ctx) = v in - let evd = Evd.from_ctx ctx in - Feedback.msg_notice - (Printer.pr_econstr_env (Global.env()) evd - (Simple_check.simple_check1 v)) ] -END - -VERNAC COMMAND EXTEND Check2 CLASSIFIED AS QUERY -| [ "Cmd6" constr(e) ] -> - [ let v = Constrintern.interp_constr (Global.env()) - (Evd.from_env (Global.env())) e in - let evd, ty = Simple_check.simple_check2 v in - Feedback.msg_notice - (Printer.pr_econstr_env (Global.env()) evd ty) ] -END - -VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY -| [ "Cmd7" constr(e) ] -> - [ let v = Constrintern.interp_constr (Global.env()) - (Evd.from_env (Global.env())) e in - let (a, ctx) = v in - let evd = Evd.from_ctx ctx in - Feedback.msg_notice - (Printer.pr_econstr_env (Global.env()) evd - (Simple_check.simple_check3 v)) ] -END - -(* This command takes a name and return its value. It does less - than Print, because it fails on constructors, axioms, and inductive types. - This should be improved, because the error message is an anomaly. - Anomalies should never appear even when using a command outside of its - intended use. *) -VERNAC COMMAND EXTEND ExamplePrint CLASSIFIED AS QUERY -| [ "Cmd8" reference(r) ] -> - [ let env = Global.env() in - let evd = Evd.from_env env in - Feedback.msg_notice - (Printer.pr_econstr_env env evd - (EConstr.of_constr - (Simple_print.simple_body_access (Nametab.global r)))) ] -END - -TACTIC EXTEND my_intro -| [ "my_intro" ident(i) ] -> - [ Tactics.introduction i] -END - -(* if one write this: - VERNAC COMMAND EXTEND exploreproof CLASSIFIED AS QUERY - it gives an error message that is basically impossible to understand. *) - -VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY -| [ "Cmd9" ] -> - [ let p = Proof_global.give_me_the_proof () in - let sigma, env = Pfedit.get_current_context () in - let pprf = Proof.partial_proof p in - Feedback.msg_notice - (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf) ] -END diff --git a/tuto1/src/g_tuto1.mlg b/tuto1/src/g_tuto1.mlg new file mode 100644 index 0000000000..4df284d2d9 --- /dev/null +++ b/tuto1/src/g_tuto1.mlg @@ -0,0 +1,154 @@ +DECLARE PLUGIN "tuto1_plugin" + +{ + +(* If we forget this line and include our own tactic definition using + TACTIC EXTEND, as below, then we get the strange error message + no implementation available for Tacentries, only when compiling + theories/Loader.v +*) +open Ltac_plugin +open Attributes +open Pp +(* This module defines the types of arguments to be used in the + EXTEND directives below, for example the string one. *) +open Stdarg + +} + +VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY +| [ "Hello" string(s) ] -> + { Feedback.msg_notice (strbrk "Hello " ++ str s) } +END + +(* reference is allowed as a syntactic entry, but so are all the entries + found the signature of module Prim in file coq/parsing/pcoq.mli *) + +VERNAC COMMAND EXTEND HelloAgain CLASSIFIED AS QUERY +| [ "HelloAgain" reference(r)] -> +(* The function Ppconstr.pr_qualid was found by searching all mli files + for a function of type qualid -> Pp.t *) + { Feedback.msg_notice + (strbrk "Hello again " ++ Ppconstr.pr_qualid r)} +END + +(* According to parsing/pcoq.mli, e has type constr_expr *) +(* this type is defined in pretyping/constrexpr.ml *) +(* Question for the developers: why is the file constrexpr.ml and not + constrexpr.mli --> Easier for packing the software in components. *) +VERNAC COMMAND EXTEND TakingConstr CLASSIFIED AS QUERY +| [ "Cmd1" constr(e) ] -> + { let _ = e in Feedback.msg_notice (strbrk "Cmd1 parsed something") } +END + +(* The next step is to make something of parsed expression. + Interesting information in interp/constrintern.mli *) + +(* There are several phases of transforming a parsed expression into + the final internal data-type (constr). There exists a collection of + functions that combine all the phases *) + +VERNAC COMMAND EXTEND TakingConstr2 CLASSIFIED AS QUERY +| [ "Cmd2" constr(e) ] -> + { let _ = Constrintern.interp_constr + (Global.env()) + (* Make sure you don't use Evd.empty here, as this does not + check consistency with existing universe constraints. *) + (Evd.from_env (Global.env())) e in + Feedback.msg_notice (strbrk "Cmd2 parsed something legitimate") } +END + +(* This is to show what happens when typing in an empty environment + with an empty evd. + Question for the developers: why does "Cmd3 (fun x : nat => x)." + raise an anomaly, not the same error as "Cmd3 (fun x : a => x)." *) + +VERNAC COMMAND EXTEND TakingConstr3 CLASSIFIED AS QUERY +| [ "Cmd3" constr(e) ] -> + { let _ = Constrintern.interp_constr Environ.empty_env + Evd.empty e in + Feedback.msg_notice + (strbrk "Cmd3 accepted something in the empty context")} +END + +(* When adding a definition, we have to be careful that just + the operation of constructing a well-typed term may already change + the environment, at the level of universe constraints (which + are recorded in the evd component). The function + Constrintern.interp_constr ignores this side-effect, so it should + not be used here. *) + +(* Looking at the interface file interp/constrintern.ml4, I lost + some time because I did not see that the "constr" type appearing + there was "EConstr.constr" and not "Constr.constr". *) + +VERNAC COMMAND EXTEND Define1 CLASSIFIED AS SIDEFF +| #[ poly = polymorphic ] [ "Cmd4" ident(i) constr(e) ] -> + { let v = Constrintern.interp_constr (Global.env()) + (Evd.from_env (Global.env())) e in + Simple_declare.packed_declare_definition ~poly i v } +END + +VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY +| [ "Cmd5" constr(e) ] -> + { let v = Constrintern.interp_constr (Global.env()) + (Evd.from_env (Global.env())) e in + let (_, ctx) = v in + let evd = Evd.from_ctx ctx in + Feedback.msg_notice + (Printer.pr_econstr_env (Global.env()) evd + (Simple_check.simple_check1 v)) } +END + +VERNAC COMMAND EXTEND Check2 CLASSIFIED AS QUERY +| [ "Cmd6" constr(e) ] -> + { let v = Constrintern.interp_constr (Global.env()) + (Evd.from_env (Global.env())) e in + let evd, ty = Simple_check.simple_check2 v in + Feedback.msg_notice + (Printer.pr_econstr_env (Global.env()) evd ty) } +END + +VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY +| [ "Cmd7" constr(e) ] -> + { let v = Constrintern.interp_constr (Global.env()) + (Evd.from_env (Global.env())) e in + let (a, ctx) = v in + let evd = Evd.from_ctx ctx in + Feedback.msg_notice + (Printer.pr_econstr_env (Global.env()) evd + (Simple_check.simple_check3 v)) } +END + +(* This command takes a name and return its value. It does less + than Print, because it fails on constructors, axioms, and inductive types. + This should be improved, because the error message is an anomaly. + Anomalies should never appear even when using a command outside of its + intended use. *) +VERNAC COMMAND EXTEND ExamplePrint CLASSIFIED AS QUERY +| [ "Cmd8" reference(r) ] -> + { let env = Global.env() in + let evd = Evd.from_env env in + Feedback.msg_notice + (Printer.pr_econstr_env env evd + (EConstr.of_constr + (Simple_print.simple_body_access (Nametab.global r)))) } +END + +TACTIC EXTEND my_intro +| [ "my_intro" ident(i) ] -> + { Tactics.introduction i } +END + +(* if one write this: + VERNAC COMMAND EXTEND exploreproof CLASSIFIED AS QUERY + it gives an error message that is basically impossible to understand. *) + +VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY +| [ "Cmd9" ] -> + { let p = Proof_global.give_me_the_proof () in + let sigma, env = Pfedit.get_current_context () in + let pprf = Proof.partial_proof p in + Feedback.msg_notice + (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf) } +END diff --git a/tuto2/_CoqProject b/tuto2/_CoqProject index bdafdb5f04..cf9cb5cc26 100644 --- a/tuto2/_CoqProject +++ b/tuto2/_CoqProject @@ -2,5 +2,5 @@ -I src theories/Test.v -src/demo.ml4 +src/demo.mlg src/demo_plugin.mlpack diff --git a/tuto2/src/demo.ml4 b/tuto2/src/demo.ml4 deleted file mode 100644 index 981d41fa5c..0000000000 --- a/tuto2/src/demo.ml4 +++ /dev/null @@ -1,347 +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 .ml4 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: - - [ () ] - - 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 (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 diff --git a/tuto2/src/demo.mlg b/tuto2/src/demo.mlg new file mode 100644 index 0000000000..966c05acdc --- /dev/null +++ b/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 diff --git a/tuto3/_CoqProject b/tuto3/_CoqProject index 6a3c1978a7..e2a60a430f 100644 --- a/tuto3/_CoqProject +++ b/tuto3/_CoqProject @@ -8,5 +8,5 @@ src/tuto_tactic.ml src/tuto_tactic.mli src/construction_game.ml src/construction_game.mli -src/g_tuto3.ml4 -src/tuto3_plugin.mlpack \ No newline at end of file +src/g_tuto3.mlg +src/tuto3_plugin.mlpack diff --git a/tuto3/src/g_tuto3.ml4 b/tuto3/src/g_tuto3.ml4 deleted file mode 100644 index 71c6be16c8..0000000000 --- a/tuto3/src/g_tuto3.ml4 +++ /dev/null @@ -1,42 +0,0 @@ -DECLARE PLUGIN "tuto3_plugin" - -open Ltac_plugin - -open Construction_game - -(* This one is necessary, to avoid message about missing wit_string *) -open Stdarg - -VERNAC COMMAND EXTEND ShowTypeConstruction CLASSIFIED AS QUERY -| [ "Tuto3_1" ] -> - [ let env = Global.env () in - let evd = Evd.from_env env in - let evd, s = Evd.new_sort_variable Evd.univ_rigid evd in - let new_type_2 = EConstr.mkSort s in - let evd, _ = - Typing.type_of (Global.env()) (Evd.from_env (Global.env())) new_type_2 in - Feedback.msg_notice - (Printer.pr_econstr_env env evd new_type_2) ] -END - -VERNAC COMMAND EXTEND ShowOneConstruction CLASSIFIED AS QUERY -| [ "Tuto3_2" ] -> [ example_sort_app_lambda () ] -END - -TACTIC EXTEND collapse_hyps -| [ "pack" "hypothesis" ident(i) ] -> - [ Tuto_tactic.pack_tactic i ] -END - -(* More advanced examples, where automatic proof happens but - no tactic is being called explicitely. The first one uses - type classes. *) -VERNAC COMMAND EXTEND TriggerClasses CLASSIFIED AS QUERY -| [ "Tuto3_3" int(n) ] -> [ example_classes n ] -END - -(* The second one uses canonical structures. *) -VERNAC COMMAND EXTEND TriggerCanonical CLASSIFIED AS QUERY -| [ "Tuto3_4" int(n) ] -> [ example_canonical n ] -END - diff --git a/tuto3/src/g_tuto3.mlg b/tuto3/src/g_tuto3.mlg new file mode 100644 index 0000000000..82ba45726e --- /dev/null +++ b/tuto3/src/g_tuto3.mlg @@ -0,0 +1,46 @@ +DECLARE PLUGIN "tuto3_plugin" + +{ + +open Ltac_plugin + +open Construction_game + +(* This one is necessary, to avoid message about missing wit_string *) +open Stdarg + +} + +VERNAC COMMAND EXTEND ShowTypeConstruction CLASSIFIED AS QUERY +| [ "Tuto3_1" ] -> + { let env = Global.env () in + let evd = Evd.from_env env in + let evd, s = Evd.new_sort_variable Evd.univ_rigid evd in + let new_type_2 = EConstr.mkSort s in + let evd, _ = + Typing.type_of (Global.env()) (Evd.from_env (Global.env())) new_type_2 in + Feedback.msg_notice + (Printer.pr_econstr_env env evd new_type_2) } +END + +VERNAC COMMAND EXTEND ShowOneConstruction CLASSIFIED AS QUERY +| [ "Tuto3_2" ] -> { example_sort_app_lambda () } +END + +TACTIC EXTEND collapse_hyps +| [ "pack" "hypothesis" ident(i) ] -> + { Tuto_tactic.pack_tactic i } +END + +(* More advanced examples, where automatic proof happens but + no tactic is being called explicitely. The first one uses + type classes. *) +VERNAC COMMAND EXTEND TriggerClasses CLASSIFIED AS QUERY +| [ "Tuto3_3" int(n) ] -> { example_classes n } +END + +(* The second one uses canonical structures. *) +VERNAC COMMAND EXTEND TriggerCanonical CLASSIFIED AS QUERY +| [ "Tuto3_4" int(n) ] -> { example_canonical n } +END + -- cgit v1.2.3