Quelle g_tuto1.mlg Sprache: unbekannt

Untersuchungsergebnis.mlg Download desUnknown {[0] [0] [0]}zum Wurzelverzeichnis wechseln

(** See dev/doc/parsing.md for mlg doc *)

DECLARE PLUGIN "rocq-plugin-tutorial.tuto1"

{

(* 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 Pp
(* This module defines the types of arguments to be used in the
   EXTEND directives below, for example the string one. *)
open Stdarg

}

(*** Printing inputs ***)

(*
* 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

(*
* 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

(*** 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

(*** 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

(*** 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.
*
* It needs the ability to access the body of opaque constants, which is given by STATE opaque_access.
* This makes the expected type of the implementation be
* [opaque_access:Global.indirect_accessor -> unit] instead of [unit].
*)
VERNAC COMMAND EXTEND ExamplePrint CLASSIFIED AS QUERY STATE opaque_access
| [ "MyPrint" reference(r) ] ->
   { fun ~opaque_access ->
     let env = Global.env () in
     let sigma = Evd.from_env env in
     try
       let t = Simple_print.simple_body_access ~opaque_access (Nametab.global r) in
       Feedback.msg_notice (Printer.pr_econstr_env env sigma t)
     with Failure s ->
       CErrors.user_err (str s)
   }
END

(*
* 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.
*
* [![opaque_access]] is equivalent to [STATE opaque_access] but is specific to that parsing rule.
*)
VERNAC COMMAND EXTEND DefineLookup CLASSIFIED AS SIDEFF
| #[ poly = Attributes.polymorphic ] ![opaque_access] [ "DefineLookup" ident(i) ":=" constr(e) ] ->
   { fun ~opaque_access ->
     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 ~opaque_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
| [ "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
| [ "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

(*** Convertibility ***)

(*
* 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

(*** 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 ] [ "ExploreProof" ] ->
  { fun ~pstate ->
    let sigma, env = Declare.Proof.get_current_context pstate in
    let pprf = Proof.partial_proof (Declare.Proof.get pstate) in
    Feedback.msg_notice
      (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf)
  }
END

Quelle g_tuto1.mlg Sprache: unbekannt

[ zur Elbe Produktseite wechseln0.73Quellennavigators ]