diff options
Diffstat (limited to 'doc/plugin_tutorial')
18 files changed, 563 insertions, 270 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/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/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg index 1d0aca1caf..0b005a2341 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.(give_me_the_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 e9b91d5a7e..1e582e6456 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -6,11 +6,9 @@ let edeclare ?hook ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps = let hook_data = Option.map (fun hook -> hook, uctx, []) hook in DeclareDef.declare_definition ident k ce ubinders 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 declare_definition ~poly ident sigma body = let k = (Decl_kinds.Global, poly, Decl_kinds.Definition) in let udecl = UState.default_univ_decl in - ignore (edeclare ident k ~opaque:false sigma udecl body None []) + edeclare ident k ~opaque:false sigma udecl body None [] (* But this definition cannot be undone by Reset ident *) 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..48b5f2214c 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_print.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_print.ml @@ -11,7 +11,7 @@ let simple_body_access gref = failwith "constructors are not covered in this example" | Globnames.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/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/g_tuto3.mlg b/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg index f4d9e7fd5b..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 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 |