diff options
Diffstat (limited to 'doc/plugin_tutorial')
37 files changed, 1411 insertions, 706 deletions
diff --git a/doc/plugin_tutorial/README.md b/doc/plugin_tutorial/README.md index f82edb2352..6d142a9af8 100644 --- a/doc/plugin_tutorial/README.md +++ b/doc/plugin_tutorial/README.md @@ -1,34 +1,20 @@ How to write plugins in Coq =========================== - # Working environment : merlin, tuareg (open question) + # Working environment + + In addition to installing OCaml and Coq, it can help to install several tools for development. - ## OCaml & related tools + ## Merlin These instructions use [OPAM](http://opam.ocaml.org/doc/Install.html) ```shell -opam init --root=$PWD/CIW2018 --compiler=4.06.0 -j2 -eval `opam config env --root=$PWD/CIW2018` -opam install camlp5 ocamlfind num # Coq's dependencies -opam install lablgtk # Coqide's dependencies (optional) opam install merlin # prints instructions for vim and emacs ``` - ## Coq - -```shell -git clone git@github.com:coq/coq.git -cd coq -./configure -profile devel -make -j2 -cd .. -export PATH=$PWD/coq/bin:$PATH -``` - ## This tutorial ```shell -git clone git@github.com:ybertot/plugin_tutorials.git cd plugin_tutorials/tuto0 make .merlin # run before opening .ml files in your editor make # build @@ -40,6 +26,8 @@ make # build package a ml4 file in a plugin, organize a `Makefile`, `_CoqProject` - Example of syntax to add a new toplevel command - Example of function call to print a simple message + - Example of function call to print a simple warning + - Example of function call to raise a simple error to the user - Example of syntax to add a simple tactic (that does nothing and prints a message) - To use it: @@ -54,19 +42,23 @@ make # build Require Import Tuto0.Loader. HelloWorld. ``` - # tuto1 : Ocaml to Coq communication + You can also modify and run `theories/Demo.v`. + + # tuto1 : OCaml to Coq communication Explore the memory of Coq, modify it - - Commands that take arguments: strings, symbols, expressions of the calculus of constructions + - Commands that take arguments: strings, integers, symbols, expressions of the calculus of constructions + - Examples of using environments correctly + - Examples of using state (the evar_map) correctly - Commands that interact with type-checking in Coq + - A command that checks convertibility between two terms - A command that adds a new definition or theorem - - A command that uses a name and exploits the existing definitions - or theorems + - A command that uses a name and exploits the existing definitions or theorems - A command that exploits an existing ongoing proof - A command that defines a new tactic Compilation and loading must be performed as for `tuto0`. - # tuto2 : Ocaml to Coq communication + # tuto2 : OCaml to Coq communication A more step by step introduction to writing commands - Explanation of the syntax of entries - Adding a new type to and parsing to the available choices diff --git a/doc/plugin_tutorial/tuto0/src/dune b/doc/plugin_tutorial/tuto0/src/dune index 79d561061d..ab9b4dd531 100644 --- a/doc/plugin_tutorial/tuto0/src/dune +++ b/doc/plugin_tutorial/tuto0/src/dune @@ -3,7 +3,4 @@ (public_name coq.plugins.tutorial.p0) (libraries coq.plugins.ltac)) -(rule - (targets g_tuto0.ml) - (deps (:pp-file g_tuto0.mlg) ) - (action (run coqpp %{pp-file}))) +(coq.pp (modules g_tuto0)) diff --git a/doc/plugin_tutorial/tuto0/src/g_tuto0.mlg b/doc/plugin_tutorial/tuto0/src/g_tuto0.mlg index 5c633fe862..97689adfed 100644 --- a/doc/plugin_tutorial/tuto0/src/g_tuto0.mlg +++ b/doc/plugin_tutorial/tuto0/src/g_tuto0.mlg @@ -5,14 +5,70 @@ DECLARE PLUGIN "tuto0_plugin" open Pp open Ltac_plugin +let tuto_warn = CWarnings.create ~name:"name" ~category:"category" + (fun _ -> strbrk Tuto0_main.message) + } +(*** Printing messages ***) + +(* + * This defines a command that prints HelloWorld. + * Note that Feedback.msg_notice can be used to print messages. + *) VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY | [ "HelloWorld" ] -> { Feedback.msg_notice (strbrk Tuto0_main.message) } END +(* + * This is a tactic version of the same thing. + *) TACTIC EXTEND hello_world_tactic | [ "hello_world" ] -> { let _ = Feedback.msg_notice (str Tuto0_main.message) in Tacticals.New.tclIDTAC } END + +(*** Printing warnings ***) + +(* + * This defines a command that prints HelloWorld as a warning. + * tuto_warn is defined at the top-level, before the command runs, + * which is standard. + *) +VERNAC COMMAND EXTEND HelloWarning CLASSIFIED AS QUERY +| [ "HelloWarning" ] -> + { + tuto_warn () + } +END + +(* + * This is a tactic version of the same thing. + *) +TACTIC EXTEND hello_warning_tactic +| [ "hello_warning" ] -> + { + let _ = tuto_warn () in + Tacticals.New.tclIDTAC + } +END + +(*** Printing errors ***) + +(* + * This defines a command that prints HelloWorld inside of an error. + * Note that CErrors.user_err can be used to raise errors to the user. + *) +VERNAC COMMAND EXTEND HelloError CLASSIFIED AS QUERY +| [ "HelloError" ] -> { CErrors.user_err (str Tuto0_main.message) } +END + +(* + * This is a tactic version of the same thing. + *) +TACTIC EXTEND hello_error_tactic +| [ "hello_error" ] -> + { let _ = CErrors.user_err (str Tuto0_main.message) in + Tacticals.New.tclIDTAC } +END diff --git a/doc/plugin_tutorial/tuto0/theories/Demo.v b/doc/plugin_tutorial/tuto0/theories/Demo.v index bdc61986af..54d5239421 100644 --- a/doc/plugin_tutorial/tuto0/theories/Demo.v +++ b/doc/plugin_tutorial/tuto0/theories/Demo.v @@ -1,8 +1,28 @@ From Tuto0 Require Import Loader. +(*** Printing messages ***) + HelloWorld. Lemma test : True. Proof. hello_world. Abort. + +(*** Printing warnings ***) + +HelloWarning. + +Lemma test : True. +Proof. +hello_warning. +Abort. + +(*** Signaling errors ***) + +Fail HelloError. + +Lemma test : True. +Proof. +Fail hello_error. +Abort. diff --git a/doc/plugin_tutorial/tuto1/_CoqProject b/doc/plugin_tutorial/tuto1/_CoqProject index 585d1360be..60f9f0a0c7 100644 --- a/doc/plugin_tutorial/tuto1/_CoqProject +++ b/doc/plugin_tutorial/tuto1/_CoqProject @@ -2,7 +2,10 @@ -I src theories/Loader.v +theories/Demo.v +src/inspector.mli +src/inspector.ml src/simple_check.mli src/simple_check.ml src/simple_declare.mli diff --git a/doc/plugin_tutorial/tuto1/src/dune b/doc/plugin_tutorial/tuto1/src/dune index cf9c674b14..054d5ecd26 100644 --- a/doc/plugin_tutorial/tuto1/src/dune +++ b/doc/plugin_tutorial/tuto1/src/dune @@ -3,7 +3,4 @@ (public_name coq.plugins.tutorial.p1) (libraries coq.plugins.ltac)) -(rule - (targets g_tuto1.ml) - (deps (:pp-file g_tuto1.mlg) ) - (action (run coqpp %{pp-file}))) +(coq.pp (modules g_tuto1)) diff --git a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg index 1d0aca1caf..73d94c2a51 100644 --- a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg +++ b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg @@ -8,7 +8,6 @@ DECLARE PLUGIN "tuto1_plugin" 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. *) @@ -16,141 +15,280 @@ open Stdarg } -VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY -| [ "Hello" string(s) ] -> - { Feedback.msg_notice (strbrk "Hello " ++ str s) } -END +(*** Printing inputs ***) -(* 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 *) +(* + * This command prints an input from the user. + * + * A list with allowable inputs can be found in interp/stdarg.mli, + * plugin/ltac/extraargs.mli, and plugin/ssr/ssrparser.mli + * (remove the wit_ prefix), but not all of these are allowable + * (unit and bool, for example, are not usable from within here). + * + * We include only some examples that are standard and useful for commands. + * Some of the omitted examples are useful for tactics. + * + * Inspector is our own file that defines a simple messaging function. + * The printing functions (pr_qualid and so on) are in printing. + * + * Some of these cases would be ambiguous if we used "What's" for each of + * these. For example, all of these are terms. We purposely disambiguate. + *) +VERNAC COMMAND EXTEND WhatIsThis CLASSIFIED AS QUERY +| [ "What's" constr(e) ] -> + { + let env = Global.env () in (* we'll explain later *) + let sigma = Evd.from_env env in (* we'll explain later *) + Inspector.print_input e (Ppconstr.pr_constr_expr env sigma) "term" + } +| [ "What" "kind" "of" "term" "is" string(s) ] -> + { Inspector.print_input s strbrk "string" } +| [ "What" "kind" "of" "term" "is" int(i) ] -> + { Inspector.print_input i Pp.int "int" } +| [ "What" "kind" "of" "term" "is" ident(id) ] -> + { Inspector.print_input id Ppconstr.pr_id "identifier" } +| [ "What" "kind" "of" "identifier" "is" reference(r) ] -> + { Inspector.print_input r Ppconstr.pr_qualid "reference" } +END -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)} +(* + * This command demonstrates basic combinators built into the DSL here. + * You can generalize this for constr_list, constr_opt, int_list, and so on. + *) +VERNAC COMMAND EXTEND WhatAreThese CLASSIFIED AS QUERY +| [ "What" "is" int_list(l) "a" "list" "of" ] -> + { + let print l = str "[" ++ Pp.prlist_with_sep (fun () -> str ";") Pp.int l ++ str "]" in + Inspector.print_input l print "int list" + } +| [ "Is" ne_int_list(l) "nonempty" ] -> + { + let print l = str "[" ++ Pp.prlist_with_sep (fun () -> str ";") Pp.int l ++ str "]" in + Inspector.print_input l print "nonempty int list" + } +| [ "And" "is" int_opt(o) "provided" ] -> + { + let print o = strbrk (if Option.has_some o then "Yes" else "No") in + Feedback.msg_notice (print o) + } 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") } + +(*** Interning terms ***) + +(* + * The next step is to make something of parsed expression. + * Interesting information in interp/constrintern.mli. + * + * When you read in constr(e), e will have type Constrexpr.constr_expr, + * which is defined in pretyping/constrexpr.ml. Your plugin + * will want a different representation. + * + * The important function is Constrintern.interp_constr_evars, + * which converts between a constr_expr and an + * (EConstr.constr, evar_map) pair. This essentially contains + * an internal representation of the term along with some state. + * For more on the state, read /dev/doc/econstr.md. + * + * NOTE ON INTERNING: Always prefer Constrintern.interp_constr_evars + * over Constrintern.interp_constr. The latter is an internal function + * not meant for external use. + * + * To get your initial environment, call Global.env (). + * To get state from that environment, call Evd.from_env on that environment. + * It is important to NEVER use the empty environment or Evd.empty; + * if you do, you will get confusing errors. + * + * NOTE ON STATE: It is important to use the evar_map that is returned to you. + * Otherwise, you may get cryptic errors later in your plugin. + * For example, you may get universe inconsistency errors. + * In general, if a function returns an evar_map to you, that's the one + * you want to thread through the rest of your command. + * + * NOTE ON STYLE: In general, it's better practice to move large + * chunks of OCaml code like this one into an .ml file. We include + * this here because it's really important to understand how to + * thread state in a plugin, and it's easier to see that if it's in the + * top-level file itself. + *) +VERNAC COMMAND EXTEND Intern CLASSIFIED AS QUERY +| [ "Intern" constr(e) ] -> + { + let env = Global.env () in (* use this; never use empty *) + let sigma = Evd.from_env env in (* use this; never use empty *) + let debug sigma = Termops.pr_evar_map ~with_univs:true None env sigma in + Feedback.msg_notice (strbrk "State before intern: " ++ debug sigma); + let (sigma, t) = Constrintern.interp_constr_evars env sigma e in + Feedback.msg_notice (strbrk "State after intern: " ++ debug sigma); + let print t = Printer.pr_econstr_env env sigma t in + Feedback.msg_notice (strbrk "Interned: " ++ print t) + } 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") } +(*** Defining terms ***) + +(* + * To define a term, we start similarly to our intern functionality, + * then we call another function. We define this function in + * the Simple_declare module. + * + * The line #[ poly = Attributes.polymorphic ] says that this command accepts + * polymorphic attributes. + * @SkySkimmer: Here, poly is what the result is bound to in the + * rule's code. Multiple attributes may be used separated by ;, and we have + * punning so foo is equivalent to foo = foo. + * + * The declare_definition function returns the reference + * that was defined. This reference will be present in the new environment. + * If you want to refer to it later in your plugin, you must use an + * updated environment and the constructed reference. + * + * Note since we are now defining a term, we must classify this + * as a side-effect (CLASSIFIED AS SIDEFF). + *) +VERNAC COMMAND EXTEND MyDefine CLASSIFIED AS SIDEFF +| #[ poly = Attributes.polymorphic ] [ "MyDefine" ident(i) ":=" constr(e) ] -> + { + let env = Global.env () in + let sigma = Evd.from_env env in + let (sigma, t) = Constrintern.interp_constr_evars env sigma e in + let r = Simple_declare.declare_definition ~poly i sigma t in + let print r = strbrk "Defined " ++ Printer.pr_global r ++ strbrk "." in + Feedback.msg_notice (print r) + } 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")} +(*** Printing terms ***) + +(* + * This command takes a name and return its value. It does less + * than Print, because it fails on constructors, axioms, and inductive types. + * It signals an error to the user for unsupported terms. + * + * Simple_print contains simple_body_access, which shows how to look up + * a global reference. + *) +VERNAC COMMAND EXTEND ExamplePrint CLASSIFIED AS QUERY +| [ "MyPrint" reference(r) ] -> + { + let env = Global.env () in + let sigma = Evd.from_env env in + try + let t = Simple_print.simple_body_access (Nametab.global r) in + Feedback.msg_notice (Printer.pr_econstr_env env sigma t) + with Failure s -> + CErrors.user_err (str s) + } 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 } +(* + * This command shows that after you define a new term, + * you can also look it up. But there's a catch! You need to actually + * refresh your environment. Otherwise, the defined term + * will not be in the environment. + * + * Using the global reference as opposed to the ID is generally + * a good idea, otherwise you might end up running into unforeseen + * problems inside of modules and sections and so on. + * + * Inside of simple_body_access, note that it uses Global.env (), + * which refreshes the environment before looking up the term. + *) +VERNAC COMMAND EXTEND DefineLookup CLASSIFIED AS SIDEFF +| #[ poly = Attributes.polymorphic ] [ "DefineLookup" ident(i) ":=" constr(e) ] -> + { + let env = Global.env () in + let sigma = Evd.from_env env in + let (sigma, t) = Constrintern.interp_constr_evars env sigma e in + let r = Simple_declare.declare_definition ~poly i sigma t in + let print r = strbrk "Defined " ++ Printer.pr_global r ++ strbrk "." in + Feedback.msg_notice (print r); + let env = Global.env () in + let sigma = Evd.from_env env in + let t = Simple_print.simple_body_access r in + let print t = strbrk "Found " ++ Printer.pr_econstr_env env sigma t in + Feedback.msg_notice (print t) + } END +(*** Checking terms ***) + +(* + * These are two commands for simple type-checking of terms. + * The bodies and explanations of the differences are in simple_check.ml. + *) + 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)) } +| [ "Check1" constr(e) ] -> + { + let env = Global.env () in + let sigma = Evd.from_env env in + let (sigma, t) = Constrintern.interp_constr_evars env sigma e in + let (sigma, typ) = Simple_check.simple_check1 env sigma t in + Feedback.msg_notice (Printer.pr_econstr_env env sigma typ) + } 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) } +| [ "Check2" constr(e) ] -> + { + let env = Global.env () in + let sigma = Evd.from_env env in + let (sigma, t) = Constrintern.interp_constr_evars env sigma e in + let typ = Simple_check.simple_check2 env sigma t in + Feedback.msg_notice (Printer.pr_econstr_env env sigma typ) + } 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 +(*** Convertibility ***) -(* 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)))) } +(* + * This command checks if there is a possible assignment of + * constraints in the state under which the two terms are + * convertible. + *) +VERNAC COMMAND EXTEND Convertible CLASSIFIED AS QUERY +| [ "Convertible" constr(e1) constr(e2) ] -> + { + let env = Global.env () in + let sigma = Evd.from_env env in + let (sigma, t1) = Constrintern.interp_constr_evars env sigma e1 in + let (sigma, t2) = Constrintern.interp_constr_evars env sigma e2 in + match Reductionops.infer_conv env sigma t1 t2 with + | Some _ -> + Feedback.msg_notice (strbrk "Yes :)") + | None -> + Feedback.msg_notice (strbrk "No :(") + } END +(*** Introducing terms ***) + +(* + * We can call the tactics defined in Tactics within our tactics. + * Here we call intros. + *) 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. *) +(*** Exploring proof state ***) +(* + * This command demonstrates exploring the proof state from within + * a command. + * + * Note that Pfedit.get_current_context gets us the environment + * and state within a proof, as opposed to the global environment + * and state. This is important within tactics. + *) VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY -| ![ proof ] [ "Cmd9" ] -> +| ![ proof_query ] [ "ExploreProof" ] -> { fun ~pstate -> - Option.iter (fun (pstate : Proof_global.t) -> - let sigma, env = Pfedit.get_current_context pstate in - let pprf = Proof.partial_proof Proof_global.(give_me_the_proof pstate) in - Feedback.msg_notice - (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf)) pstate; - pstate } + let sigma, env = Pfedit.get_current_context pstate in + let pprf = Proof.partial_proof (Proof_global.get_proof pstate) in + Feedback.msg_notice + (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf) + } END diff --git a/doc/plugin_tutorial/tuto1/src/inspector.ml b/doc/plugin_tutorial/tuto1/src/inspector.ml new file mode 100644 index 0000000000..d37cbdb74c --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/inspector.ml @@ -0,0 +1,8 @@ +open Pp + +(* + * Inspect an input and print a feedback message explaining what it is + *) +let print_input (a : 'a) (printer : 'a -> Pp.t) (type_str : string) : unit = + let msg = printer a ++ strbrk (Printf.sprintf " is a %s." type_str) in + Feedback.msg_notice msg diff --git a/doc/plugin_tutorial/tuto1/src/inspector.mli b/doc/plugin_tutorial/tuto1/src/inspector.mli new file mode 100644 index 0000000000..52b970bbe0 --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/inspector.mli @@ -0,0 +1,4 @@ +(* + * Inspect an input and print a feedback message explaining what it is + *) +val print_input : 'a -> ('a -> Pp.t) -> string -> unit diff --git a/doc/plugin_tutorial/tuto1/src/simple_check.ml b/doc/plugin_tutorial/tuto1/src/simple_check.ml index 2949adde73..684864a056 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_check.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_check.ml @@ -1,32 +1,14 @@ -let simple_check1 value_with_constraints = - begin - let evalue, st = value_with_constraints in - let evd = Evd.from_ctx st in -(* This is reverse engineered from vernacentries.ml *) -(* The point of renaming is to make sure the bound names printed by Check - can be re-used in `apply with` tactics that use bound names to - refer to arguments. *) - let j = Environ.on_judgment EConstr.of_constr - (Arguments_renaming.rename_typing (Global.env()) - (EConstr.to_constr evd evalue)) in - let {Environ.uj_type=x}=j in x - end - -let simple_check2 value_with_constraints = - let evalue, st = value_with_constraints in - let evd = Evd.from_ctx st in -(* This version should be preferred if bound variable names are not so - important, you want to really verify that the input is well-typed, +let simple_check1 env sigma evalue = +(* This version should be preferred if you want to really + verify that the input is well-typed, and if you want to obtain the type. *) (* Note that the output value is a pair containing a new evar_map: typing will fill out blanks in the term by add evar bindings. *) - Typing.type_of (Global.env()) evd evalue + Typing.type_of env sigma evalue -let simple_check3 value_with_constraints = - let evalue, st = value_with_constraints in - let evd = Evd.from_ctx st in -(* This version should be preferred if bound variable names are not so - important and you already expect the input to have been type-checked - before. Set ~lax to false if you want an anomaly to be raised in - case of a type error. Otherwise a ReTypeError exception is raised. *) - Retyping.get_type_of ~lax:true (Global.env()) evd evalue +let simple_check2 env sigma evalue = +(* This version should be preferred if you already expect the input to + have been type-checked before. Set ~lax to false if you want an anomaly + to be raised in case of a type error. Otherwise a ReTypeError exception + is raised. *) + Retyping.get_type_of ~lax:true env sigma evalue diff --git a/doc/plugin_tutorial/tuto1/src/simple_check.mli b/doc/plugin_tutorial/tuto1/src/simple_check.mli index bcf1bf56cf..4b28ac74fe 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_check.mli +++ b/doc/plugin_tutorial/tuto1/src/simple_check.mli @@ -1,8 +1,5 @@ val simple_check1 : - EConstr.constr Evd.in_evar_universe_context -> EConstr.constr + Environ.env -> Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.constr val simple_check2 : - EConstr.constr Evd.in_evar_universe_context -> Evd.evar_map * EConstr.constr - -val simple_check3 : - EConstr.constr Evd.in_evar_universe_context -> EConstr.constr + Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml index 23f8fbe888..9dd4700db5 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -1,25 +1,12 @@ -(* Ideally coq/coq#8811 would get merged and then this function could be much simpler. *) -let edeclare ?hook ~ontop ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps = - let sigma = Evd.minimize_universes sigma in - let body = EConstr.to_constr sigma body in - let tyopt = Option.map (EConstr.to_constr sigma) tyopt in - let uvars_fold uvars c = - Univ.LSet.union uvars (Vars.universes_of_constr c) in - let uvars = List.fold_left uvars_fold Univ.LSet.empty - (Option.List.cons tyopt [body]) in - let sigma = Evd.restrict_universe_context sigma uvars in - let univs = Evd.check_univ_decl ~poly sigma udecl in +let edeclare ?hook ~name ~poly ~scope ~kind ~opaque sigma udecl body tyopt imps = + let sigma, ce = DeclareDef.prepare_definition ~allow_evars:false + ~opaque ~poly sigma udecl ~types:tyopt ~body in let uctx = Evd.evar_universe_context sigma in let ubinders = Evd.universe_binders sigma in - let ce = Declare.definition_entry ?types:tyopt ~univs body in let hook_data = Option.map (fun hook -> hook, uctx, []) hook in - DeclareDef.declare_definition ~ontop ident k ce ubinders imps ?hook_data + DeclareDef.declare_definition ~name ~scope ~kind ubinders ce imps ?hook_data -let packed_declare_definition ~poly ident value_with_constraints = - let body, ctx = value_with_constraints in - let sigma = Evd.from_ctx ctx in - let k = (Decl_kinds.Global, poly, Decl_kinds.Definition) in +let declare_definition ~poly name sigma body = let udecl = UState.default_univ_decl in - ignore (edeclare ~ontop:None ident k ~opaque:false sigma udecl body None []) - -(* But this definition cannot be undone by Reset ident *) + edeclare ~name ~poly ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) + ~kind:Decls.Definition ~opaque:false sigma udecl body None [] diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.mli b/doc/plugin_tutorial/tuto1/src/simple_declare.mli index fd74e81526..c55b36742f 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.mli +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.mli @@ -1,5 +1,4 @@ open Names -open EConstr -val packed_declare_definition : - poly:bool -> Id.t -> constr Evd.in_evar_universe_context -> unit +val declare_definition : + poly:bool -> Id.t -> Evd.evar_map -> EConstr.t -> Names.GlobRef.t diff --git a/doc/plugin_tutorial/tuto1/src/simple_print.ml b/doc/plugin_tutorial/tuto1/src/simple_print.ml index cfc38ff9c9..88afec14d5 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_print.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_print.ml @@ -2,16 +2,17 @@ type constr is given in the coq-dpdgraph plugin. *) let simple_body_access gref = + let open Names.GlobRef in match gref with - | Globnames.VarRef _ -> + | VarRef _ -> failwith "variables are not covered in this example" - | Globnames.IndRef _ -> + | IndRef _ -> failwith "inductive types are not covered in this example" - | Globnames.ConstructRef _ -> + | ConstructRef _ -> failwith "constructors are not covered in this example" - | Globnames.ConstRef cst -> + | ConstRef cst -> let cb = Environ.lookup_constant cst (Global.env()) in - match Global.body_of_constant_body cb with - | Some(e, _) -> e + match Global.body_of_constant_body Library.indirect_accessor cb with + | Some(e, _, _) -> EConstr.of_constr e | None -> failwith "This term has no value" diff --git a/doc/plugin_tutorial/tuto1/src/simple_print.mli b/doc/plugin_tutorial/tuto1/src/simple_print.mli index 254b56ff79..943e26acb6 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_print.mli +++ b/doc/plugin_tutorial/tuto1/src/simple_print.mli @@ -1 +1 @@ -val simple_body_access : Names.GlobRef.t -> Constr.constr +val simple_body_access : Names.GlobRef.t -> EConstr.constr diff --git a/doc/plugin_tutorial/tuto1/src/tuto1_plugin.mlpack b/doc/plugin_tutorial/tuto1/src/tuto1_plugin.mlpack index a797a509e0..9309f78cd0 100644 --- a/doc/plugin_tutorial/tuto1/src/tuto1_plugin.mlpack +++ b/doc/plugin_tutorial/tuto1/src/tuto1_plugin.mlpack @@ -1,3 +1,4 @@ +Inspector Simple_check Simple_declare Simple_print diff --git a/doc/plugin_tutorial/tuto1/theories/Demo.v b/doc/plugin_tutorial/tuto1/theories/Demo.v new file mode 100644 index 0000000000..5723e2f82e --- /dev/null +++ b/doc/plugin_tutorial/tuto1/theories/Demo.v @@ -0,0 +1,95 @@ +From Tuto1 Require Import Loader. + +(*** Printing user inputs ***) + +Definition definition := 5. +What's definition. +What kind of term is definition. +What kind of identifier is definition. + +What is 1 2 3 a list of. +What is a list of. (* no arguments = empty list *) + +Is 1 2 3 nonempty. +(* Is nonempty *) (* does not parse *) + +And is 1 provided. +And is provided. + +(*** Interning terms ***) + +Intern 3. +Intern definition. +Intern (fun (x : Prop) => x). +Intern (fun (x : Type) => x). +Intern (forall (T : Type), T). +Intern (fun (T : Type) (t : T) => t). +Intern _. +Intern (Type : Type). + +(*** Defining terms ***) + +MyDefine n := 1. +Print n. + +MyDefine f := (fun (x : Type) => x). +Print f. + +(*** Printing terms ***) + +MyPrint f. +MyPrint n. +Fail MyPrint nat. + +DefineLookup n' := 1. +DefineLookup f' := (fun (x : Type) => x). + +(*** Checking terms ***) + +Check1 3. +Check1 definition. +Check1 (fun (x : Prop) => x). +Check1 (fun (x : Type) => x). +Check1 (forall (T : Type), T). +Check1 (fun (T : Type) (t : T) => t). +Check1 _. +Check1 (Type : Type). + +Check2 3. +Check2 definition. +Check2 (fun (x : Prop) => x). +Check2 (fun (x : Type) => x). +Check2 (forall (T : Type), T). +Check2 (fun (T : Type) (t : T) => t). +Check2 _. +Check2 (Type : Type). + +(*** Convertibility ***) + +Convertible 1 1. +Convertible (fun (x : Type) => x) (fun (x : Type) => x). +Convertible Type Type. +Convertible 1 ((fun (x : nat) => x) 1). + +Convertible 1 2. +Convertible (fun (x : Type) => x) (fun (x : Prop) => x). +Convertible Type Prop. +Convertible 1 ((fun (x : nat) => x) 2). + +(*** Introducing variables ***) + +Theorem foo: + forall (T : Set) (t : T), T. +Proof. + my_intro T. my_intro t. apply t. +Qed. + +(*** Exploring proof state ***) + +Fail ExploreProof. (* not in a proof *) + +Theorem bar: + forall (T : Set) (t : T), T. +Proof. + ExploreProof. my_intro T. ExploreProof. my_intro t. ExploreProof. apply t. +Qed. diff --git a/doc/plugin_tutorial/tuto2/_CoqProject b/doc/plugin_tutorial/tuto2/_CoqProject index cf9cb5cc26..0d7a644271 100644 --- a/doc/plugin_tutorial/tuto2/_CoqProject +++ b/doc/plugin_tutorial/tuto2/_CoqProject @@ -1,6 +1,15 @@ --R theories/ Tuto +-R theories Tuto2 -I src -theories/Test.v -src/demo.mlg -src/demo_plugin.mlpack +theories/Loader.v +theories/Demo.v +theories/Count.v + +src/custom.ml +src/custom.mli +src/counter.ml +src/counter.mli +src/persistent_counter.ml +src/persistent_counter.mli +src/g_tuto2.mlg +src/tuto2_plugin.mlpack diff --git a/doc/plugin_tutorial/tuto2/src/counter.ml b/doc/plugin_tutorial/tuto2/src/counter.ml new file mode 100644 index 0000000000..8721090d42 --- /dev/null +++ b/doc/plugin_tutorial/tuto2/src/counter.ml @@ -0,0 +1,22 @@ +(* + * This file defines our counter, which we use in the Count command. + *) + +(* + * Our counter is simply a reference called "counter" to an integer. + * + * Summary.ref behaves like ref, but also registers a summary to Coq. + *) +let counter = Summary.ref ~name:"counter" 0 + +(* + * We can increment our counter: + *) +let increment () = + counter := succ !counter + +(* + * We can also read the value of our counter: + *) +let value () = + !counter diff --git a/doc/plugin_tutorial/tuto2/src/counter.mli b/doc/plugin_tutorial/tuto2/src/counter.mli new file mode 100644 index 0000000000..984bc1d2cc --- /dev/null +++ b/doc/plugin_tutorial/tuto2/src/counter.mli @@ -0,0 +1,13 @@ +(* + * This file defines our counter, which we use in the Count command. + *) + +(* + * Increment the counter + *) +val increment : unit -> unit + +(* + * Determine the value of the counter + *) +val value : unit -> int diff --git a/doc/plugin_tutorial/tuto2/src/custom.ml b/doc/plugin_tutorial/tuto2/src/custom.ml new file mode 100644 index 0000000000..648786d3bd --- /dev/null +++ b/doc/plugin_tutorial/tuto2/src/custom.ml @@ -0,0 +1,5 @@ +(* + * This file defines a custom type for the PassCustom command. + *) + +type custom_type = Foo | Bar diff --git a/doc/plugin_tutorial/tuto2/src/custom.mli b/doc/plugin_tutorial/tuto2/src/custom.mli new file mode 100644 index 0000000000..648786d3bd --- /dev/null +++ b/doc/plugin_tutorial/tuto2/src/custom.mli @@ -0,0 +1,5 @@ +(* + * This file defines a custom type for the PassCustom command. + *) + +type custom_type = Foo | Bar 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 diff --git a/doc/plugin_tutorial/tuto2/src/demo_plugin.mlpack b/doc/plugin_tutorial/tuto2/src/demo_plugin.mlpack deleted file mode 100644 index 4f0b8480b5..0000000000 --- a/doc/plugin_tutorial/tuto2/src/demo_plugin.mlpack +++ /dev/null @@ -1 +0,0 @@ -Demo diff --git a/doc/plugin_tutorial/tuto2/src/dune b/doc/plugin_tutorial/tuto2/src/dune index f2bc405455..8c4b04b1ae 100644 --- a/doc/plugin_tutorial/tuto2/src/dune +++ b/doc/plugin_tutorial/tuto2/src/dune @@ -3,7 +3,4 @@ (public_name coq.plugins.tutorial.p2) (libraries coq.plugins.ltac)) -(rule - (targets demo.ml) - (deps (:pp-file demo.mlg) ) - (action (run coqpp %{pp-file}))) +(coq.pp (modules g_tuto2)) diff --git a/doc/plugin_tutorial/tuto2/src/g_tuto2.mlg b/doc/plugin_tutorial/tuto2/src/g_tuto2.mlg new file mode 100644 index 0000000000..a3ce60d432 --- /dev/null +++ b/doc/plugin_tutorial/tuto2/src/g_tuto2.mlg @@ -0,0 +1,618 @@ +(* -------------------------------------------------------------------------- *) +(* *) +(* Initial ritual dance *) +(* *) +(* -------------------------------------------------------------------------- *) + +DECLARE PLUGIN "tuto2_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 "tuto2_plugin". + That means that: + + (1) We write the following command in a file called Loader.v: + + Declare ML Module "tuto2_plugin". + + to load this command into the Coq top-level. + + (2) Users can then load our plugin in other Coq files by writing: + + From Tuto2 Require Import Loader. + + where Loader is the name of the file that declares "tuto2_plugin", + and where Tuto2 is the name passed to the -R argument in our _CoqProject. + + (3) The above commands will succeed only if there is "tuto2_plugin.cmxs" + in some of the directories where Coq is supposed to look + (i.e. the ones we specified via "-I ..." command line options in + _CoqProject). As long as this is listed in our _CoqProject, the + Makefile takes care of placing it in the right directory. + + (4) The file "tuto2_plugin.mlpack" lists the OCaml modules to be linked in + "tuto2_plugin.cmxs". + + (5) The file "tuto2_plugin.mlpack" as well as all .ml, .mli and .mlg files + are listed in the "_CoqProject" file. + *) + +(* -------------------------------------------------------------------------- *) +(* *) +(* Importing OCaml dependencies *) +(* *) +(* -------------------------------------------------------------------------- *) + +(* + * This .mlg file is parsed into a .ml file. You can put OCaml in this file + * inside of curly braces. It's best practice to use this only to import + * other modules, and include most of your functionality in those modules. + * + * Here we list all of the dependencies that these commands have, and explain + * why. We also refer to the first command that uses them, where further + * explanation can be found in context. + *) +{ + (*** Dependencies from Coq ***) + + (* + * This lets us take non-terminal arguments to a command (for example, + * the PassInt command that takes an integer argument needs this + * this dependency). + * + * First used by: PassInt + *) + open Stdarg + + (* + * This is Coq's pretty-printing module. Here, we need it to use some + * useful syntax for pretty-printing. + * + * First use by: Count + *) + open Pp +} + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to define a new Vernacular command? *) +(* *) +(* -------------------------------------------------------------------------- *) + +(* + This command does nothing: +*) +VERNAC COMMAND EXTEND NoOp CLASSIFIED AS QUERY +| [ "Nothing" ] -> { () } +END + +(* + --- Defining a Command --- + + These: + + VERNAC COMMAND EXTEND + + and + + END + + mark the beginning and the end of the definition of a new Vernacular command. + + --- Assigning a Command a Unique Identifier --- + + NoOp is a unique identifier (which must start with an upper-case letter) + associated with the new Vernacular command we are defining. It is good + to make this identifier descriptive. + + --- Classifying a Command --- + + CLASSIFIED AS QUERY tells Coq that the new Vernacular command neither: + - changes the global environment, nor + - modifies 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. + + --- Defining Parsing and Interpretation Rules --- + + This: + + [ "Nothing" ] -> { () } + + defines: + - the parsing rule (left) + - the interpretation rule (right) + + The parsing rule and the interpretation rule are separated by -> token. + + The parsing rule, in this case, is: + + [ "Nothing" ] + + By convention, all vernacular command start with an upper-case letter. + + The '[' and ']' characters mark the beginning and the end of the parsing + rule, respectively. The parsing rule itself says that the syntax of the + newly defined command is composed from a single terminal Nothing. + + The interpretation rule, in this case, is: + + { () } + + Similarly to the case of the parsing rule, the + '{' 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. + + --- Calling a Command --- + + In Demo.v, we call this command by writing: + + Nothing. + + since our parsing rule is "Nothing". This does nothing, since our + interpretation rule is (). +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to define a new Vernacular command with some terminal parameters? *) +(* *) +(* -------------------------------------------------------------------------- *) + +(* + This command takes some terminal parameters and does nothing. +*) +VERNAC COMMAND EXTEND NoOpTerminal CLASSIFIED AS QUERY +| [ "Command" "With" "Some" "Terminal" "Parameters" ] -> { () } +END + +(* + --- Defining a Command with Terminal Parameters --- + + 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. + + --- Calling a Command with Terminal Parameters --- + + In Demo.v, we call this command by writing: + + Command With Some Terminal Parameters. + + to match our parsing rule. As expected, this does nothing. + + --- Recognizing Syntax Errors --- + + Note that if we were to omit any of these terminals, for example by writing: + + Command. + + it would fail to parse (as expected), showing this error to the user: + + Syntax error: illegal begin of vernac. +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to define a new Vernacular command with some non-terminal parameter? *) +(* *) +(* -------------------------------------------------------------------------- *) + +(* + This command takes an integer argument and does nothing. +*) +VERNAC COMMAND EXTEND PassInt CLASSIFIED AS QUERY +| [ "Pass" int(i) ] -> { () } +END + +(* + --- Dependencies --- + + Since this command takes a non-terminal argument, it is the first + to depend on Stdarg (opened at the top of this file). + + --- Defining a Command with Non-Terminal Arguments --- + + 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). There are more examples in tuto1. + + 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. + + --- Recognizing Build Errors --- + + The mapping from int(i) to wit_int is automatic. + This is why, if we forget to open Stdarg, we will get this error: + + Unbound value wit_int + + when we try to build our plugin. It is good to recognize this error, + since this is a common mistake in plugin development, and understand + that the fix is to open the file (Stdarg) where wit_int is defined. + + --- Calling a Command with Terminal Arguments --- + + We call this command in Demo.v by writing: + + Pass 42. + + We could just as well pass any other integer. As expected, this command + does nothing. + + --- Recognizing Syntax Errors --- + + As in our previous command, if we were to omit the arguments to the command, + for example by writing: + + Pass. + + it would fail to parse (as expected), showing this error to the user: + + Syntax error: [prim:integer] expected after 'Pass' (in [vernac:command]). + + The same thing would happen if we passed the wrong argument type: + + Pass True. + + If we pass too many arguments: + + Pass 15 20. + + we will get a different syntax error: + + Syntax error: '.' expected after [vernac:command] (in [vernac_aux]). + + It is good to recognize these errors, since doing so can help you + catch mistakes you make defining your parser rules during plugin + development. +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to define a new Vernacular command with variable number of arguments? *) +(* *) +(* -------------------------------------------------------------------------- *) + +(* + This command takes a list of integers and does nothing: +*) +VERNAC COMMAND EXTEND AcceptIntList CLASSIFIED AS QUERY +| [ "Accept" int_list(l) ] -> { () } +END + +(* + --- Dependencies --- + + Much like PassInt, this command depends on Stdarg. + + --- Defining a Command that Takes a Variable Number of Arguments --- + + 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, ... + + --- Other Ways to Take a Variable Number of Arguments --- + + To see which other Ocaml type constructors (in addition to list) + are supported, have a look at the parse_user_entry function defined + in the coqpp/coqpp_parse.mly 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, + - ยทยทยท + + Much like with int_list, we could use any other supported type here. + There are some more examples of this in tuto1. + + --- Calling a Command with a Variable Number of Arguments --- + + We call this command in Demo.v by writing: + + Accept 100 200 300 400. + + As expected, this does nothing. + + Since our parser rule uses int_list, the arguments to Accept can be a + list of integers of any length. For example, we can pass the empty list: + + Accept. + + or just one argument: + + Accept 2. + + and so on. +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to define a new Vernacular command that takes values of a custom type? *) +(* *) +(* -------------------------------------------------------------------------- *) + +(* + --- Defining Custom Types --- + + Vernacular commands can take custom types in addition to the built-in + ones. The first step to taking these custom types as arguments is + to define them. + + + We define a type of values that we want to pass to our Vernacular command + in custom.ml/custom.mli. The type is very simple: + + type custom_type : Foo | Bar. + + --- Using our New Module --- + + Now that we have a new OCaml module Custom, in order to use it, we must + do the following: + + 1. Add src/custom.ml and src/custom.mli to our _CoqProject + 2. Add Custom to our tuto2_plugin.mlpack + + This workflow will become very familiar to you when you add new modules + to your plugins, so it is worth getting used to. + + --- Depending on our New Module --- + + Now that our new module is listed in both _CoqProject and tuto2_plugin.mlpack, + we can use fully qualified names Custom.Foo and Custom.Bar. + + Alternatively, we could add the dependency on our module: + + open Custom. + + to the top of the file, and then refer to Foo and Bar directly. + + --- Telling Coq About our New Argument Type --- + + 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: +*) +VERNAC ARGUMENT EXTEND custom +| [ "Foo" ] -> { Custom.Foo } +| [ "Bar" ] -> { Custom.Bar } +END + +(* + where: + + custom + + indicates that, from now on, in our parsing rules we can write: + + custom(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). +*) + +(* + --- Defining a Command that Takes an Argument of a Custom Type --- + + Now that Coq is aware of our new argument type, we can define a command + that uses it. This command takes an argument Foo or Bar and does nothing: +*) +VERNAC COMMAND EXTEND PassCustom CLASSIFIED AS QUERY +| [ "Foobar" custom(x) ] -> { () } +END + +(* + --- Calling a Command that Takes an Argument of a Custom Type --- + + We call this command in Demo.v by writing: + + Foobar Foo. + Foobar Bar. + + As expected, both of these do nothing. In the first case, x gets + the value Custom.Foo : Custom.custom_type, since our custom parsing + and interpretation rules (VERNAC ARGUMENT EXTEND custom ...) map + the input Foo to Custom.Foo. Similarly, in the second case, x gets + the value Custom.Bar : Custom.custom_type. +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to give a feedback to the user? *) +(* *) +(* -------------------------------------------------------------------------- *) + +(* + So far we have defined commands that do nothing. + We can also signal feedback to the user. + + This command tells the user that everything is awesome: +*) +VERNAC COMMAND EXTEND Awesome CLASSIFIED AS QUERY +| [ "Is" "Everything" "Awesome" ] -> + { + Feedback.msg_notice (Pp.str "Everything is awesome!") + } +END + +(* + --- Pretty Printing --- + + User feedback functions like Feedback.msg_notice take a Pp.t as an argument. + Check the Pp module to see which functions are available to construct + a Pp.t. + + The 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. + + --- Giving Feedback --- + + Once we have a Pp.t, we can use the following functions: + + - Feedback.msg_info : Pp.t -> unit + - Feedback.msg_notice : Pp.t -> unit + - Feedback.msg_warning : Pp.t -> unit + - Feedback.msg_debug : Pp.t -> unit + + to give user a textual feedback. Examples of some of these can be + found in tuto0. + + --- Signaling Errors --- + + While there is a Feedback.msg_error, when signaling an error, + it is currently better practice to use user_err. There is an example of + this in tuto0. +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to implement a Vernacular command with (undoable) side-effects? *) +(* *) +(* -------------------------------------------------------------------------- *) + +(* + This command counts how many times it has been called since importing + our plugin, and signals that information to the user: + *) +VERNAC COMMAND EXTEND Count CLASSIFIED AS SIDEFF +| [ "Count" ] -> + { + Counter.increment (); + let v = Counter.value () in + Feedback.msg_notice (Pp.str "Times Count has been called: " ++ Pp.int v) + } +END + +(* + --- Dependencies --- + + If we want to use the ++ syntax, then we need to depend on Pp explicitly. + This is why, at the top, we write: + + open Pp. + + --- Defining the Counter --- + + We define our counter in the Counter module. Please see counter.ml and + counter.mli for details. + + As with Custom, we must modify our _CoqProject and tuto2_plugin.mlpack + so that we can use Counter in our code. + + --- Classifying the Command --- + + This command has undoable side-effects: When the plugin is first loaded, + the counter is instantiated to 0. After each time we call Count, the value of + the counter increases by 1. + + Thus, we must write CLASSIFIED AS SIDEEFF for this command, rather than + CLASSIFIED AS QUERY. See the explanation from the NoOp command earlier if + you do not remember the distinction. + + --- Calling the Command --- + + We call our command three times in Demo.v by writing: + + Count. + Count. + Count. + + This gives us the following output: + + Times Count has been called: 1 + Times Count has been called: 2 + Times Count has been called: 3 + + Note that when the plugin is first loaded, the counter is 0. It increases + each time Count is called. + + --- Behavior with Imports --- + + Count.v shows the behavior with imports. Note that if we import Demo.v, + the counter is set to 0 from the beginning, even though Demo.v calls + Count three times. + + In other words, this is not persistent! +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to implement a Vernacular command that uses persistent storage? *) +(* *) +(* -------------------------------------------------------------------------- *) + +(* + * This command is like Count, but it is persistent across modules: + *) +VERNAC COMMAND EXTEND CountPersistent CLASSIFIED AS SIDEFF +| [ "Count" "Persistent" ] -> + { + Persistent_counter.increment (); + let v = Persistent_counter.value () in + Feedback.msg_notice (Pp.str "Times Count Persistent has been called: " ++ Pp.int v) + } +END + +(* + --- Persistent Storage --- + + Everything is similar to the Count command, except that we use a counter + that is persistent. See persistent_counter.ml for details. + + The key trick is that we must create a persistent object for our counter + to persist across modules. Coq has some useful APIs for this in Libobject. + We demonstrate these in persistent_counter.ml. + + This is really, really useful if you want, for example, to cache some + results that your plugin computes across modules. A persistent object + can be a hashtable, for example, that maps inputs to outputs your command + has already computed, if you know the result will not change. + + --- Calling the Command --- + + We call the command in Demo.v and in Count.v, just like we did with Count. + Note that this time, the value of the counter from Demo.v persists in Count.v. +*) diff --git a/doc/plugin_tutorial/tuto2/src/persistent_counter.ml b/doc/plugin_tutorial/tuto2/src/persistent_counter.ml new file mode 100644 index 0000000000..868f6ab99b --- /dev/null +++ b/doc/plugin_tutorial/tuto2/src/persistent_counter.ml @@ -0,0 +1,56 @@ +(* + * This file defines our persistent counter, which we use in the + * CountPersistent command. + *) + +(* + * At its core, our persistent counter looks exactly the same as + * our non-persistent counter (with a different name to prevent collisions): + *) +let counter = Summary.ref ~name:"persistent_counter" 0 + +(* + * The difference is that we need to declare it as a persistent object + * using Libobject.declare_object. To do that, we define a function that + * saves the value that is passed to it into the reference we have just defined: + *) +let cache_count (_, v) = + counter := v + +(* + * We then use declare_object to create a function that takes an integer value + * (the type our counter refers to) and creates a persistent object from that + * value: + *) +let declare_counter : int -> Libobject.obj = + let open Libobject in + declare_object + { + (default_object "COUNTER") with + cache_function = cache_count; + load_function = (fun _ -> cache_count); + } +(* + * See Libobject for more information on what other information you + * can pass here, and what all of these functions mean. + * + * For example, if we passed the same thing that we pass to load_function + * to open_function, then our last call to Count Persistent in Count.v + * would return 4 and not 6. + *) + +(* + * Incrementing our counter looks almost identical: + *) +let increment () = + Lib.add_anonymous_leaf (declare_counter (succ !counter)) +(* + * except that we must call our declare_counter function to get a persistent + * object. We then pass this object to Lib.add_anonymous_leaf. + *) + +(* + * Reading a value does not change at all: + *) +let value () = + !counter diff --git a/doc/plugin_tutorial/tuto2/src/persistent_counter.mli b/doc/plugin_tutorial/tuto2/src/persistent_counter.mli new file mode 100644 index 0000000000..d3c88e19a6 --- /dev/null +++ b/doc/plugin_tutorial/tuto2/src/persistent_counter.mli @@ -0,0 +1,14 @@ +(* + * This file defines our persistent counter, which we use in the + * CountPersistent command. + *) + +(* + * Increment the persistent counter + *) +val increment : unit -> unit + +(* + * Determine the value of the persistent counter + *) +val value : unit -> int diff --git a/doc/plugin_tutorial/tuto2/src/tuto2_plugin.mlpack b/doc/plugin_tutorial/tuto2/src/tuto2_plugin.mlpack new file mode 100644 index 0000000000..0bc7402978 --- /dev/null +++ b/doc/plugin_tutorial/tuto2/src/tuto2_plugin.mlpack @@ -0,0 +1,4 @@ +Custom +Counter +Persistent_counter +G_tuto2 diff --git a/doc/plugin_tutorial/tuto2/theories/Count.v b/doc/plugin_tutorial/tuto2/theories/Count.v new file mode 100644 index 0000000000..3287342b75 --- /dev/null +++ b/doc/plugin_tutorial/tuto2/theories/Count.v @@ -0,0 +1,19 @@ +Require Import Demo. + +(*** Local ***) + +Count. +Count. + +Import Demo. + +Count. + +(*** Persistent ***) + +Count Persistent. +Count Persistent. + +Import Demo. + +Count Persistent. diff --git a/doc/plugin_tutorial/tuto2/theories/Demo.v b/doc/plugin_tutorial/tuto2/theories/Demo.v new file mode 100644 index 0000000000..73b5fcca62 --- /dev/null +++ b/doc/plugin_tutorial/tuto2/theories/Demo.v @@ -0,0 +1,63 @@ +From Tuto2 Require Import Loader. + +(*** A no-op command ***) + +Nothing. + +(*** No-op commands with arguments ***) + +(* + * Terminal parameters: + *) +Command With Some Terminal Parameters. +(* Command. *) (* does not parse *) + +(* + * A single non-terminal argument: + *) +Pass 42. +(* Pass. *) (* does not parse *) +(* Pass True. *) (* does not parse *) +(* Pass 15 20. *) (* does not parse *) + +(* + * A list of non-terminal arguments: + *) +Accept 100 200 300 400. +Accept. +Accept 2. + +(* + * A custom argument: + *) +Foobar Foo. +Foobar Bar. + +(*** Commands that give feedback ***) + +(* + * Simple feedback: + *) +Is Everything Awesome. + +(*** Storage and side effects ***) + +(* + * Local side effects: + *) +Count. +Count. +Count. +(* + * See Count.v for behavior in modules that import this one. + *) + +(* + * Persistent side effects: + *) +Count Persistent. +Count Persistent. +Count Persistent. +(* + * See Count.v for behavior in modules that import this one. + *) diff --git a/doc/plugin_tutorial/tuto2/theories/Loader.v b/doc/plugin_tutorial/tuto2/theories/Loader.v new file mode 100644 index 0000000000..9ce9991c86 --- /dev/null +++ b/doc/plugin_tutorial/tuto2/theories/Loader.v @@ -0,0 +1 @@ +Declare ML Module "tuto2_plugin". diff --git a/doc/plugin_tutorial/tuto2/theories/Test.v b/doc/plugin_tutorial/tuto2/theories/Test.v deleted file mode 100644 index 38e83bfff1..0000000000 --- a/doc/plugin_tutorial/tuto2/theories/Test.v +++ /dev/null @@ -1,19 +0,0 @@ -Declare ML Module "demo_plugin". - -Cmd1. -Cmd2 With Some Terminal Parameters. -Cmd3 42. -Cmd4 100 200 300 400. -Cmd5 Foo_5. -Cmd5 Bar_5. -Cmd6. -Cmd7. -Cmd7. -Cmd7. - -Goal True. -Proof. - tactic1. - tactic2 Foo_2. - tactic2 Bar_2. -Abort. diff --git a/doc/plugin_tutorial/tuto3/src/construction_game.ml b/doc/plugin_tutorial/tuto3/src/construction_game.ml index 663113d012..2a2acb6001 100644 --- a/doc/plugin_tutorial/tuto3/src/construction_game.ml +++ b/doc/plugin_tutorial/tuto3/src/construction_game.ml @@ -3,15 +3,15 @@ open Context let find_reference = Coqlib.find_reference [@ocaml.warning "-3"] -let example_sort evd = +let example_sort sigma = (* creating a new sort requires that universes should be recorded in the evd datastructure, so this datastructure also needs to be passed around. *) - let evd, s = Evd.new_sort_variable Evd.univ_rigid evd in + let sigma, s = Evd.new_sort_variable Evd.univ_rigid sigma in let new_type = EConstr.mkSort s in - evd, new_type + sigma, new_type -let c_one evd = +let c_one sigma = (* In the general case, global references may refer to universe polymorphic objects, and their universe has to be made afresh when creating an instance. *) let gr_S = @@ -19,129 +19,129 @@ let c_one evd = (* the long name of "S" was found with the command "About S." *) let gr_O = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "O" in - let evd, c_O = Evarutil.new_global evd gr_O in - let evd, c_S = Evarutil.new_global evd gr_S in + let sigma, c_O = Evarutil.new_global sigma gr_O in + let sigma, c_S = Evarutil.new_global sigma gr_S in (* Here is the construction of a new term by applying functions to argument. *) - evd, EConstr.mkApp (c_S, [| c_O |]) + sigma, EConstr.mkApp (c_S, [| c_O |]) -let dangling_identity env evd = +let dangling_identity env sigma = (* I call this a dangling identity, because it is not polymorph, but the type on which it applies is left unspecified, as it is represented by an existential variable. The declaration for this existential variable needs to be added in the evd datastructure. *) - let evd, type_type = example_sort evd in - let evd, arg_type = Evarutil.new_evar env evd type_type in + let sigma, type_type = example_sort sigma in + let sigma, arg_type = Evarutil.new_evar env sigma type_type in (* Notice the use of a De Bruijn index for the inner occurrence of the bound variable. *) - evd, EConstr.mkLambda(nameR (Names.Id.of_string "x"), arg_type, + sigma, EConstr.mkLambda(nameR (Names.Id.of_string "x"), arg_type, EConstr.mkRel 1) -let dangling_identity2 env evd = +let dangling_identity2 env sigma = (* This example uses directly a function that produces an evar that is meant to be a type. *) - let evd, (arg_type, type_type) = - Evarutil.new_type_evar env evd Evd.univ_rigid in - evd, EConstr.mkLambda(nameR (Names.Id.of_string "x"), arg_type, + let sigma, (arg_type, type_type) = + Evarutil.new_type_evar env sigma Evd.univ_rigid in + sigma, EConstr.mkLambda(nameR (Names.Id.of_string "x"), arg_type, EConstr.mkRel 1) let example_sort_app_lambda () = let env = Global.env () in - let evd = Evd.from_env env in - let evd, c_v = c_one evd in + let sigma = Evd.from_env env in + let sigma, c_v = c_one sigma in (* dangling_identity and dangling_identity2 can be used interchangeably here *) - let evd, c_f = dangling_identity2 env evd in + let sigma, c_f = dangling_identity2 env sigma in let c_1 = EConstr.mkApp (c_f, [| c_v |]) in let _ = Feedback.msg_notice - (Printer.pr_econstr_env env evd c_1) in + (Printer.pr_econstr_env env sigma c_1) in (* type verification happens here. Type verification will update existential variable information in the evd part. *) - let evd, the_type = Typing.type_of env evd c_1 in + let sigma, the_type = Typing.type_of env sigma c_1 in (* At display time, you will notice that the system knows about the existential variable being instantiated to the "nat" type, even though c_1 still contains the meta-variable. *) Feedback.msg_notice - ((Printer.pr_econstr_env env evd c_1) ++ + ((Printer.pr_econstr_env env sigma c_1) ++ str " has type " ++ - (Printer.pr_econstr_env env evd the_type)) + (Printer.pr_econstr_env env sigma the_type)) -let c_S evd = +let c_S sigma = let gr = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "S" in - Evarutil.new_global evd gr + Evarutil.new_global sigma gr -let c_O evd = +let c_O sigma = let gr = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "O" in - Evarutil.new_global evd gr + Evarutil.new_global sigma gr -let c_E evd = +let c_E sigma = let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "EvenNat" in - Evarutil.new_global evd gr + Evarutil.new_global sigma gr -let c_D evd = +let c_D sigma = let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "tuto_div2" in - Evarutil.new_global evd gr + Evarutil.new_global sigma gr -let c_Q evd = +let c_Q sigma = let gr = find_reference "Tuto3" ["Coq"; "Init"; "Logic"] "eq" in - Evarutil.new_global evd gr + Evarutil.new_global sigma gr -let c_R evd = +let c_R sigma = let gr = find_reference "Tuto3" ["Coq"; "Init"; "Logic"] "eq_refl" in - Evarutil.new_global evd gr + Evarutil.new_global sigma gr -let c_N evd = +let c_N sigma = let gr = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "nat" in - Evarutil.new_global evd gr + Evarutil.new_global sigma gr -let c_C evd = +let c_C sigma = let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "C" in - Evarutil.new_global evd gr + Evarutil.new_global sigma gr -let c_F evd = +let c_F sigma = let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "S_ev" in - Evarutil.new_global evd gr + Evarutil.new_global sigma gr -let c_P evd = +let c_P sigma = let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "s_half_proof" in - Evarutil.new_global evd gr + Evarutil.new_global sigma gr (* If c_S was universe polymorphic, we should have created a new constant at each iteration of buildup. *) -let mk_nat evd n = - let evd, c_S = c_S evd in - let evd, c_O = c_O evd in +let mk_nat sigma n = + let sigma, c_S = c_S sigma in + let sigma, c_O = c_O sigma in let rec buildup = function | 0 -> c_O | n -> EConstr.mkApp (c_S, [| buildup (n - 1) |]) in - if n <= 0 then evd, c_O else evd, buildup n + if n <= 0 then sigma, c_O else sigma, buildup n let example_classes n = let env = Global.env () in - let evd = Evd.from_env env in - let evd, c_n = mk_nat evd n in - let evd, n_half = mk_nat evd (n / 2) in - let evd, c_N = c_N evd in - let evd, c_div = c_D evd in - let evd, c_even = c_E evd in - let evd, c_Q = c_Q evd in - let evd, c_R = c_R evd in + let sigma = Evd.from_env env in + let sigma, c_n = mk_nat sigma n in + let sigma, n_half = mk_nat sigma (n / 2) in + let sigma, c_N = c_N sigma in + let sigma, c_div = c_D sigma in + let sigma, c_even = c_E sigma in + let sigma, c_Q = c_Q sigma in + let sigma, c_R = c_R sigma in let arg_type = EConstr.mkApp (c_even, [| c_n |]) in - let evd0 = evd in - let evd, instance = Evarutil.new_evar env evd arg_type in + let sigma0 = sigma in + let sigma, instance = Evarutil.new_evar env sigma arg_type in let c_half = EConstr.mkApp (c_div, [|c_n; instance|]) in - let _ = Feedback.msg_notice (Printer.pr_econstr_env env evd c_half) in - let evd, the_type = Typing.type_of env evd c_half in - let _ = Feedback.msg_notice (Printer.pr_econstr_env env evd c_half) in + let _ = Feedback.msg_notice (Printer.pr_econstr_env env sigma c_half) in + let sigma, the_type = Typing.type_of env sigma c_half in + let _ = Feedback.msg_notice (Printer.pr_econstr_env env sigma c_half) in let proved_equality = EConstr.mkCast(EConstr.mkApp (c_R, [| c_N; c_half |]), Constr.DEFAULTcast, EConstr.mkApp (c_Q, [| c_N; c_half; n_half|])) in (* This is where we force the system to compute with type classes. *) (* Question to coq developers: why do we pass two evd arguments to - solve_remaining_evars? Is the choice of evd0 relevant here? *) - let evd = Pretyping.solve_remaining_evars - (Pretyping.default_inference_flags true) env evd ~initial:evd0 in - let evd, final_type = Typing.type_of env evd proved_equality in - Feedback.msg_notice (Printer.pr_econstr_env env evd proved_equality) + solve_remaining_evars? Is the choice of sigma0 relevant here? *) + let sigma = Pretyping.solve_remaining_evars + (Pretyping.default_inference_flags true) env sigma ~initial:sigma0 in + let sigma, final_type = Typing.type_of env sigma proved_equality in + Feedback.msg_notice (Printer.pr_econstr_env env sigma proved_equality) (* This function, together with definitions in Data.v, shows how to trigger automatic proofs at the time of typechecking, based on @@ -152,36 +152,36 @@ let example_classes n = *) let example_canonical n = let env = Global.env () in - let evd = Evd.from_env env in + let sigma = Evd.from_env env in (* Construct a natural representation of this integer. *) - let evd, c_n = mk_nat evd n in + let sigma, c_n = mk_nat sigma n in (* terms for "nat", "eq", "S_ev", "eq_refl", "C" *) - let evd, c_N = c_N evd in - let evd, c_F = c_F evd in - let evd, c_R = c_R evd in - let evd, c_C = c_C evd in - let evd, c_P = c_P evd in + let sigma, c_N = c_N sigma in + let sigma, c_F = c_F sigma in + let sigma, c_R = c_R sigma in + let sigma, c_C = c_C sigma in + let sigma, c_P = c_P sigma in (* the last argument of C *) let refl_term = EConstr.mkApp (c_R, [|c_N; c_n |]) in (* Now we build two existential variables, for the value of the half and for the "S_ev" structure that triggers the proof search. *) - let evd, ev1 = Evarutil.new_evar env evd c_N in + let sigma, ev1 = Evarutil.new_evar env sigma c_N in (* This is the type for the second existential variable *) let csev = EConstr.mkApp (c_F, [| ev1 |]) in - let evd, ev2 = Evarutil.new_evar env evd csev in + let sigma, ev2 = Evarutil.new_evar env sigma csev in (* Now we build the C structure. *) let test_term = EConstr.mkApp (c_C, [| c_n; ev1; ev2; refl_term |]) in (* Type-checking this term will compute values for the existential variables *) - let evd, final_type = Typing.type_of env evd test_term in + let sigma, final_type = Typing.type_of env sigma test_term in (* The computed type has two parameters, the second one is the proof. *) - let value = match EConstr.kind evd final_type with + let value = match EConstr.kind sigma final_type with | Constr.App(_, [| _; the_half |]) -> the_half | _ -> failwith "expecting the whole type to be \"cmp _ the_half\"" in - let _ = Feedback.msg_notice (Printer.pr_econstr_env env evd value) in + let _ = Feedback.msg_notice (Printer.pr_econstr_env env sigma value) in (* I wish for a nicer way to get the value of ev2 in the evar_map *) - let prf_struct = EConstr.of_constr (EConstr.to_constr evd ev2) in + let prf_struct = EConstr.of_constr (EConstr.to_constr sigma ev2) in let the_prf = EConstr.mkApp (c_P, [| ev1; prf_struct |]) in - let evd, the_statement = Typing.type_of env evd the_prf in + let sigma, the_statement = Typing.type_of env sigma the_prf in Feedback.msg_notice - (Printer.pr_econstr_env env evd the_prf ++ str " has type " ++ - Printer.pr_econstr_env env evd the_statement) + (Printer.pr_econstr_env env sigma the_prf ++ str " has type " ++ + Printer.pr_econstr_env env sigma the_statement) diff --git a/doc/plugin_tutorial/tuto3/src/dune b/doc/plugin_tutorial/tuto3/src/dune index ba6d8b288f..678dd71328 100644 --- a/doc/plugin_tutorial/tuto3/src/dune +++ b/doc/plugin_tutorial/tuto3/src/dune @@ -4,7 +4,4 @@ (flags :standard -warn-error -3) (libraries coq.plugins.ltac)) -(rule - (targets g_tuto3.ml) - (deps (:pp-file g_tuto3.mlg)) - (action (run coqpp %{pp-file}))) +(coq.pp (modules g_tuto3)) diff --git a/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg b/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg index 82ba45726e..14b8eb5f07 100644 --- a/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg +++ b/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg @@ -14,13 +14,13 @@ 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 sigma = Evd.from_env env in + let sigma, s = Evd.new_sort_variable Evd.univ_rigid sigma in let new_type_2 = EConstr.mkSort s in - let evd, _ = + let sigma, _ = 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) } + (Printer.pr_econstr_env env sigma new_type_2) } END VERNAC COMMAND EXTEND ShowOneConstruction CLASSIFIED AS QUERY @@ -33,7 +33,7 @@ TACTIC EXTEND collapse_hyps END (* More advanced examples, where automatic proof happens but - no tactic is being called explicitely. The first one uses + no tactic is being called explicitly. The first one uses type classes. *) VERNAC COMMAND EXTEND TriggerClasses CLASSIFIED AS QUERY | [ "Tuto3_3" int(n) ] -> { example_classes n } diff --git a/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml b/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml index 2d541087ce..796a65f40d 100644 --- a/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml +++ b/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml @@ -65,10 +65,10 @@ let package i = Goal.enter begin fun gl -> and return the value a. *) (* Remark by Maxime: look for destApp combinator. *) -let unpack_type evd term = +let unpack_type sigma term = let report () = CErrors.user_err (Pp.str "expecting a packed type") in - match EConstr.kind evd term with + match EConstr.kind sigma term with | Constr.App (_, [| ty |]) -> ty | _ -> report () @@ -76,19 +76,19 @@ let unpack_type evd term = A -> pack B -> C and return A, B, C but it is not used in the current version of our tactic. It is kept as an example. *) -let two_lambda_pattern evd term = +let two_lambda_pattern sigma term = let report () = CErrors.user_err (Pp.str "expecting two nested implications") in (* Note that pattern-matching is always done through the EConstr.kind function, which only provides one-level deep patterns. *) - match EConstr.kind evd term with + match EConstr.kind sigma term with (* Here we recognize the outer implication *) | Constr.Prod (_, ty1, l1) -> (* Here we recognize the inner implication *) - (match EConstr.kind evd l1 with + (match EConstr.kind sigma l1 with | Constr.Prod (n2, packed_ty2, deep_conclusion) -> (* Here we recognized that the second type is an application *) - ty1, unpack_type evd packed_ty2, deep_conclusion + ty1, unpack_type sigma packed_ty2, deep_conclusion | _ -> report ()) | _ -> report () @@ -104,22 +104,22 @@ let get_type_of_hyp env id = let repackage i h_hyps_id = Goal.enter begin fun gl -> let env = Goal.env gl in - let evd = Tacmach.New.project gl in + let sigma = Tacmach.New.project gl in let concl = Tacmach.New.pf_concl gl in let (ty1 : EConstr.t) = get_type_of_hyp env i in let (packed_ty2 : EConstr.t) = get_type_of_hyp env h_hyps_id in - let ty2 = unpack_type evd packed_ty2 in + let ty2 = unpack_type sigma packed_ty2 in let new_packed_type = EConstr.mkApp (c_P (), [| ty1; ty2 |]) in let open EConstr in let new_packed_value = mkApp (c_R (), [| ty1; ty2; mkVar i; mkApp (c_U (), [| ty2; mkVar h_hyps_id|]) |]) in - Refine.refine ~typecheck:true begin fun evd -> - let evd, new_goal = Evarutil.new_evar env evd + Refine.refine ~typecheck:true begin fun sigma -> + let sigma, new_goal = Evarutil.new_evar env sigma (mkArrowR (mkApp(c_H (), [| new_packed_type |])) (Vars.lift 1 concl)) in - evd, mkApp (new_goal, + sigma, mkApp (new_goal, [|mkApp(c_M (), [|new_packed_type; new_packed_value |]) |]) end end |