Merge pull request #8778 from SkySkimmer/merge-plugin-tuto

Move plugin tutorial to Coq repo

12 files changed, 282 insertions, 0 deletions

diff --git a/doc/plugin_tutorial/tuto1/Makefile b/doc/plugin_tutorial/tuto1/Makefile
new file mode 100644
index 0000000000..e0e197650d
--- /dev/null
+++ b/doc/plugin_tutorial/tuto1/Makefile
@@ -0,0 +1,14 @@
+ifeq "$(COQBIN)" ""
+  COQBIN=$(dir $(shell which coqtop))/
+endif
+
+%: Makefile.coq
+
+Makefile.coq: _CoqProject
+	$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
+
+tests: all
+	@$(MAKE) -C tests -s clean
+	@$(MAKE) -C tests -s all
+
+-include Makefile.coq
diff --git a/doc/plugin_tutorial/tuto1/_CoqProject b/doc/plugin_tutorial/tuto1/_CoqProject
new file mode 100644
index 0000000000..585d1360be
--- /dev/null
+++ b/doc/plugin_tutorial/tuto1/_CoqProject
@@ -0,0 +1,13 @@
+-R theories Tuto1
+-I src
+
+theories/Loader.v
+
+src/simple_check.mli
+src/simple_check.ml
+src/simple_declare.mli
+src/simple_declare.ml
+src/simple_print.ml
+src/simple_print.mli
+src/g_tuto1.mlg
+src/tuto1_plugin.mlpack
diff --git a/doc/plugin_tutorial/tuto1/src/dune b/doc/plugin_tutorial/tuto1/src/dune
new file mode 100644
index 0000000000..cf9c674b14
--- /dev/null
+++ b/doc/plugin_tutorial/tuto1/src/dune
@@ -0,0 +1,9 @@
+(library
+ (name tuto1_plugin)
+ (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})))
diff --git a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
new file mode 100644
index 0000000000..4df284d2d9
--- /dev/null
+++ b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
@@ -0,0 +1,154 @@
+DECLARE PLUGIN "tuto1_plugin"
+
+{
+
+(* If we forget this line and include our own tactic definition using
+  TACTIC EXTEND, as below, then we get the strange error message
+  no implementation available for Tacentries, only when compiling
+  theories/Loader.v
+*)
+open Ltac_plugin
+open Attributes
+open Pp
+(* This module defines the types of arguments to be used in the
+   EXTEND directives below, for example the string one. *)
+open Stdarg
+
+}
+
+VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY
+| [ "Hello" string(s) ] ->
+  { Feedback.msg_notice (strbrk "Hello " ++ str s) }
+END
+
+(* reference is allowed as a syntactic entry, but so are all the entries
+   found the signature of module Prim in file coq/parsing/pcoq.mli *)
+
+VERNAC COMMAND EXTEND HelloAgain CLASSIFIED AS QUERY
+| [ "HelloAgain" reference(r)] ->
+(* The function Ppconstr.pr_qualid was found by searching all mli files
+   for a function of type qualid -> Pp.t *)
+  { Feedback.msg_notice
+      (strbrk "Hello again " ++ Ppconstr.pr_qualid r)}
+END
+
+(* According to parsing/pcoq.mli, e has type constr_expr *)
+(* this type is defined in pretyping/constrexpr.ml *)
+(* Question for the developers: why is the file constrexpr.ml and not
+   constrexpr.mli --> Easier for packing the software in components. *)
+VERNAC COMMAND EXTEND TakingConstr CLASSIFIED AS QUERY
+| [ "Cmd1" constr(e) ] ->
+  { let _ = e in Feedback.msg_notice (strbrk "Cmd1 parsed something") }
+END
+
+(* The next step is to make something of parsed expression.
+   Interesting information in interp/constrintern.mli *)
+
+(* There are several phases of transforming a parsed expression into
+  the final internal data-type (constr).  There exists a collection of
+  functions that combine all the phases *)
+
+VERNAC COMMAND EXTEND TakingConstr2 CLASSIFIED AS QUERY
+| [ "Cmd2" constr(e) ] ->
+  { let _ = Constrintern.interp_constr
+    (Global.env())
+    (* Make sure you don't use Evd.empty here, as this does not
+      check consistency with existing universe constraints. *)
+    (Evd.from_env (Global.env())) e in
+    Feedback.msg_notice (strbrk "Cmd2 parsed something legitimate") }
+END
+
+(* This is to show what happens when typing in an empty environment
+  with an empty evd.
+ Question for the developers: why does "Cmd3 (fun x : nat => x)."
+ raise an anomaly, not the same error as "Cmd3 (fun x : a => x)." *)
+ 
+VERNAC COMMAND EXTEND TakingConstr3 CLASSIFIED AS QUERY
+| [ "Cmd3" constr(e) ] ->
+  { let _ = Constrintern.interp_constr Environ.empty_env
+      Evd.empty e in
+      Feedback.msg_notice
+        (strbrk "Cmd3 accepted something in the empty context")}
+END
+
+(* When adding a definition, we have to be careful that just
+  the operation of constructing a well-typed term may already change
+  the environment, at the level of universe constraints (which
+  are recorded in the evd component).  The function
+  Constrintern.interp_constr ignores this side-effect, so it should
+  not be used here. *)
+
+(* Looking at the interface file interp/constrintern.ml4, I lost
+  some time because I did not see that the "constr" type appearing
+  there was "EConstr.constr" and not "Constr.constr". *)
+
+VERNAC COMMAND EXTEND Define1 CLASSIFIED AS SIDEFF
+| #[ poly = polymorphic ] [ "Cmd4" ident(i) constr(e) ] ->
+  { let v = Constrintern.interp_constr (Global.env())
+      (Evd.from_env (Global.env())) e in
+    Simple_declare.packed_declare_definition ~poly i v }
+END
+
+VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY
+| [ "Cmd5" constr(e) ] ->
+  { let v = Constrintern.interp_constr (Global.env())
+      (Evd.from_env (Global.env())) e in
+    let (_, ctx) = v in
+    let evd = Evd.from_ctx ctx in
+    Feedback.msg_notice
+    (Printer.pr_econstr_env (Global.env()) evd
+       (Simple_check.simple_check1 v)) }
+END
+
+VERNAC COMMAND EXTEND Check2 CLASSIFIED AS QUERY
+| [ "Cmd6" constr(e) ] ->
+  { let v = Constrintern.interp_constr (Global.env())
+      (Evd.from_env (Global.env())) e in
+    let evd, ty = Simple_check.simple_check2 v in
+    Feedback.msg_notice
+      (Printer.pr_econstr_env (Global.env()) evd ty) }
+END
+
+VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY
+| [ "Cmd7" constr(e) ] ->
+  { let v = Constrintern.interp_constr (Global.env())
+      (Evd.from_env (Global.env())) e in
+    let (a, ctx) = v in
+    let evd = Evd.from_ctx ctx in
+      Feedback.msg_notice
+      (Printer.pr_econstr_env (Global.env()) evd
+         (Simple_check.simple_check3 v)) }
+END
+
+(* This command takes a name and return its value.  It does less
+  than Print, because it fails on constructors, axioms, and inductive types.
+  This should be improved, because the error message is an anomaly.
+  Anomalies should never appear even when using a command outside of its
+  intended use. *)
+VERNAC COMMAND EXTEND ExamplePrint CLASSIFIED AS QUERY
+| [ "Cmd8" reference(r) ] ->
+  { let env = Global.env() in
+    let evd = Evd.from_env env in
+    Feedback.msg_notice
+    (Printer.pr_econstr_env env evd
+      (EConstr.of_constr
+        (Simple_print.simple_body_access (Nametab.global r)))) }
+END
+
+TACTIC EXTEND my_intro
+| [ "my_intro" ident(i) ] ->
+  { Tactics.introduction i }
+END
+
+(* if one write this:
+  VERNAC COMMAND EXTEND exploreproof CLASSIFIED AS QUERY
+  it gives an error message that is basically impossible to understand. *)
+
+VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY
+| [ "Cmd9" ] ->
+  { let p = Proof_global.give_me_the_proof () in
+    let sigma, env = Pfedit.get_current_context () in
+    let pprf = Proof.partial_proof p in
+    Feedback.msg_notice
+      (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf) }
+END
diff --git a/doc/plugin_tutorial/tuto1/src/simple_check.ml b/doc/plugin_tutorial/tuto1/src/simple_check.ml
new file mode 100644
index 0000000000..1f636c531a
--- /dev/null
+++ b/doc/plugin_tutorial/tuto1/src/simple_check.ml
@@ -0,0 +1,32 @@
+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 = Termops.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,
+  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
+
+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
diff --git a/doc/plugin_tutorial/tuto1/src/simple_check.mli b/doc/plugin_tutorial/tuto1/src/simple_check.mli
new file mode 100644
index 0000000000..bcf1bf56cf
--- /dev/null
+++ b/doc/plugin_tutorial/tuto1/src/simple_check.mli
@@ -0,0 +1,8 @@
+val simple_check1 :
+  EConstr.constr Evd.in_evar_universe_context -> 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
diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
new file mode 100644
index 0000000000..9d10a8ba72
--- /dev/null
+++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
@@ -0,0 +1,24 @@
+(* Ideally coq/coq#8811 would get merged and then this function could be much simpler. *)
+let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook =
+  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 ubinders = Evd.universe_binders sigma in
+  let ce = Declare.definition_entry ?types:tyopt ~univs body in
+  DeclareDef.declare_definition ident k ce ubinders imps ~hook
+
+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 udecl = UState.default_univ_decl in
+  let nohook = Lemmas.mk_hook (fun _ x -> ()) in
+  ignore (edeclare ident k ~opaque:false sigma udecl body None [] nohook)
+
+(* 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
new file mode 100644
index 0000000000..fd74e81526
--- /dev/null
+++ b/doc/plugin_tutorial/tuto1/src/simple_declare.mli
@@ -0,0 +1,5 @@
+open Names
+open EConstr
+
+val packed_declare_definition :
+    poly:bool -> Id.t -> constr Evd.in_evar_universe_context -> unit
diff --git a/doc/plugin_tutorial/tuto1/src/simple_print.ml b/doc/plugin_tutorial/tuto1/src/simple_print.ml
new file mode 100644
index 0000000000..cfc38ff9c9
--- /dev/null
+++ b/doc/plugin_tutorial/tuto1/src/simple_print.ml
@@ -0,0 +1,17 @@
+(* A more advanced example of how to explore the structure of terms of
+  type constr is given in the coq-dpdgraph plugin. *)
+
+let simple_body_access gref =
+  match gref with
+  | Globnames.VarRef _ ->
+    failwith "variables are not covered in this example"
+  | Globnames.IndRef _ ->
+    failwith "inductive types are not covered in this example"
+  | Globnames.ConstructRef _ ->
+    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
+    | 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
new file mode 100644
index 0000000000..254b56ff79
--- /dev/null
+++ b/doc/plugin_tutorial/tuto1/src/simple_print.mli
@@ -0,0 +1 @@
+val simple_body_access : Names.GlobRef.t -> Constr.constr
diff --git a/doc/plugin_tutorial/tuto1/src/tuto1_plugin.mlpack b/doc/plugin_tutorial/tuto1/src/tuto1_plugin.mlpack
new file mode 100644
index 0000000000..a797a509e0
--- /dev/null
+++ b/doc/plugin_tutorial/tuto1/src/tuto1_plugin.mlpack
@@ -0,0 +1,4 @@
+Simple_check
+Simple_declare
+Simple_print
+G_tuto1
diff --git a/doc/plugin_tutorial/tuto1/theories/Loader.v b/doc/plugin_tutorial/tuto1/theories/Loader.v
new file mode 100644
index 0000000000..6e8e308b3f
--- /dev/null
+++ b/doc/plugin_tutorial/tuto1/theories/Loader.v
@@ -0,0 +1 @@
+Declare ML Module "tuto1_plugin".