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 sigma = Evd.from_ctx ctx in
    Feedback.msg_notice
    (Printer.pr_econstr_env (Global.env()) sigma
       (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 sigma, ty = Simple_check.simple_check2 v in
    Feedback.msg_notice
      (Printer.pr_econstr_env (Global.env()) sigma 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 sigma = Evd.from_ctx ctx in
      Feedback.msg_notice
      (Printer.pr_econstr_env (Global.env()) sigma
         (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 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)))) }
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
| ![ proof_query ] [ "Cmd9" ] ->
  { fun ~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