diff options
Diffstat (limited to 'doc/plugin_tutorial')
| -rw-r--r-- | doc/plugin_tutorial/README.md | 38 | ||||
| -rw-r--r-- | doc/plugin_tutorial/tuto0/src/g_tuto0.mlg | 56 | ||||
| -rw-r--r-- | doc/plugin_tutorial/tuto0/theories/Demo.v | 20 | ||||
| -rw-r--r-- | doc/plugin_tutorial/tuto1/_CoqProject | 3 | ||||
| -rw-r--r-- | doc/plugin_tutorial/tuto1/src/g_tuto1.mlg | 345 | ||||
| -rw-r--r-- | doc/plugin_tutorial/tuto1/src/inspector.ml | 8 | ||||
| -rw-r--r-- | doc/plugin_tutorial/tuto1/src/inspector.mli | 4 | ||||
| -rw-r--r-- | doc/plugin_tutorial/tuto1/src/simple_check.ml | 38 | ||||
| -rw-r--r-- | doc/plugin_tutorial/tuto1/src/simple_check.mli | 7 | ||||
| -rw-r--r-- | doc/plugin_tutorial/tuto1/src/simple_declare.ml | 6 | ||||
| -rw-r--r-- | doc/plugin_tutorial/tuto1/src/simple_declare.mli | 5 | ||||
| -rw-r--r-- | doc/plugin_tutorial/tuto1/src/simple_print.ml | 2 | ||||
| -rw-r--r-- | doc/plugin_tutorial/tuto1/src/simple_print.mli | 2 | ||||
| -rw-r--r-- | doc/plugin_tutorial/tuto1/src/tuto1_plugin.mlpack | 1 | ||||
| -rw-r--r-- | doc/plugin_tutorial/tuto1/theories/Demo.v | 95 |
15 files changed, 462 insertions, 168 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 300d62285a..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,136 +15,276 @@ 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 sigma = Evd.from_ctx ctx in - Feedback.msg_notice - (Printer.pr_econstr_env (Global.env()) sigma - (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 sigma, ty = Simple_check.simple_check2 v in - Feedback.msg_notice - (Printer.pr_econstr_env (Global.env()) sigma 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 sigma = Evd.from_ctx ctx in - Feedback.msg_notice - (Printer.pr_econstr_env (Global.env()) sigma - (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 sigma = Evd.from_env env in - Feedback.msg_notice - (Printer.pr_econstr_env env sigma - (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_query ] [ "Cmd9" ] -> +| ![ proof_query ] [ "ExploreProof" ] -> { fun ~pstate -> let sigma, env = Pfedit.get_current_context pstate in let pprf = Proof.partial_proof Proof_global.(give_me_the_proof pstate) in 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 c2f09c64e0..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 sigma = 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 sigma 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 sigma = 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()) sigma evalue + Typing.type_of env sigma evalue -let simple_check3 value_with_constraints = - let evalue, st = value_with_constraints in - let sigma = 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()) sigma 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 22a0163fbb..48b5f2214c 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_print.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_print.ml @@ -12,6 +12,6 @@ let simple_body_access gref = | Globnames.ConstRef cst -> let cb = Environ.lookup_constant cst (Global.env()) in match Global.body_of_constant_body Library.indirect_accessor cb with - | Some(e, _) -> e + | 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. |