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. --- tuto1/_CoqProject | 4 +- tuto1/src/g_tuto1.ml4 | 149 ------------------------------------------------ tuto1/src/g_tuto1.mlg | 154 ++++++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 156 insertions(+), 151 deletions(-) delete mode 100644 tuto1/src/g_tuto1.ml4 create mode 100644 tuto1/src/g_tuto1.mlg (limited to 'tuto1') 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 -- cgit v1.2.3