Merge PR #9003: [vernacextend] Consolidate extension points API

8 files changed, 147 insertions, 94 deletions

diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index 88638b295b..bc0b0310b3 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -9,7 +9,14 @@
 (************************************************************************)
 
 open CErrors
-open Vernacexpr
+
+(** The type of parsing attribute data *)
+type vernac_flags = vernac_flag list
+and vernac_flag = string * vernac_flag_value
+and vernac_flag_value =
+  | VernacFlagEmpty
+  | VernacFlagLeaf of string
+  | VernacFlagList of vernac_flags
 
 let unsupported_attributes = function
   | [] -> ()
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index c81082d5ad..c2dde4cbcc 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -8,7 +8,13 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Vernacexpr
+(** The type of parsing attribute data *)
+type vernac_flags = vernac_flag list
+and vernac_flag = string * vernac_flag_value
+and vernac_flag_value =
+  | VernacFlagEmpty
+  | VernacFlagLeaf of string
+  | VernacFlagList of vernac_flags
 
 type +'a attribute
 (** The type of attributes. When parsing attributes if an ['a
@@ -80,7 +86,7 @@ val parse_with_extra : 'a attribute -> vernac_flags -> vernac_flags * 'a
 
 (** * Defining attributes. *)
 
-type 'a key_parser = 'a option -> Vernacexpr.vernac_flag_value -> 'a
+type 'a key_parser = 'a option -> vernac_flag_value -> 'a
 (** A parser for some key in an attribute. It is given a nonempty ['a
     option] when the attribute is multiply set for some command.
 
diff --git a/vernac/egramml.mli b/vernac/egramml.mli
index a90ef97e7d..3689f60383 100644
--- a/vernac/egramml.mli
+++ b/vernac/egramml.mli
@@ -21,10 +21,10 @@ type 's grammar_prod_item =
       ('s, 'a) Extend.symbol) Loc.located -> 's grammar_prod_item
 
 val extend_vernac_command_grammar :
-  Vernacexpr.extend_name -> vernac_expr Pcoq.Entry.t option ->
+  extend_name -> vernac_expr Pcoq.Entry.t option ->
     vernac_expr grammar_prod_item list -> unit
 
-val get_extend_vernac_rule : Vernacexpr.extend_name -> vernac_expr grammar_prod_item list
+val get_extend_vernac_rule : extend_name -> vernac_expr grammar_prod_item list
 
 val proj_symbol : ('a, 'b, 'c) Extend.ty_user_symbol -> ('a, 'b, 'c) Genarg.genarg_type
 
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 960e74827a..3cdf81ced0 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -30,6 +30,7 @@ open Pcoq.Prim
 open Pcoq.Constr
 open Pcoq.Module
 open Pvernac.Vernac_
+open Attributes
 
 let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:"; "where"; "at" ]
 let _ = List.iter CLexer.add_keyword vernac_kw
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index f65fae60ee..2ddd210365 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1214,6 +1214,7 @@ open Pputils
 
 let rec pr_vernac_flag (k, v) =
   let k = keyword k in
+  let open Attributes in
   match v with
   | VernacFlagEmpty -> k
   | VernacFlagLeaf v -> k ++ str " = " ++ qs v
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 180d763946..122005e011 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -219,13 +219,6 @@ type section_subset_expr =
 
     {b ("ExtractionBlacklist", 0)} indicates {b Extraction Blacklist {i ident{_1}} ... {i ident{_n}}} command.
  *)
-type extend_name =
-  (** Name of the vernac entry where the tactic is defined, typically found
-      after the VERNAC EXTEND statement in the source. *)
-  string *
-  (** Index of the extension in the VERNAC EXTEND statement. Each parsing branch
-      is given an offset, starting from zero. *)
-  int
 
 (* This type allows registering the inlining of constants in native compiler.
    It will be extended with primitive inductive types and operators *)
@@ -253,6 +246,14 @@ type vernac_argument_status = {
   implicit_status : vernac_implicit_status;
 }
 
+type extend_name =
+  (** Name of the vernac entry where the tactic is defined, typically found
+      after the VERNAC EXTEND statement in the source. *)
+  string *
+  (** Index of the extension in the VERNAC EXTEND statement. Each parsing branch
+      is given an offset, starting from zero. *)
+  int
+
 type nonrec vernac_expr =
 
   | VernacLoad of verbose_flag * string
@@ -395,71 +396,11 @@ type nonrec vernac_expr =
   (* For extension *)
   | VernacExtend of extend_name * Genarg.raw_generic_argument list
 
-type vernac_flags = vernac_flag list
-and vernac_flag = string * vernac_flag_value
-and vernac_flag_value =
-  | VernacFlagEmpty
-  | VernacFlagLeaf of string
-  | VernacFlagList of vernac_flags
-
 type vernac_control =
-  | VernacExpr of vernac_flags * vernac_expr
+  | VernacExpr of Attributes.vernac_flags * vernac_expr
   (* boolean is true when the `-time` batch-mode command line flag was set.
      the flag is used to print differently in `-time` vs `Time foo` *)
   | VernacTime of bool * vernac_control CAst.t
   | VernacRedirect of string * vernac_control CAst.t
   | VernacTimeout of int * vernac_control
   | VernacFail of vernac_control
-
-(* A vernac classifier provides information about the exectuion of a
-   command:
-
-   - vernac_when: encodes if the vernac may alter the parser [thus
-     forcing immediate execution], or if indeed it is pure and parsing
-     can continue without its execution.
-
-   - vernac_type: if it is starts, ends, continues a proof or
-     alters the global state or is a control command like BackTo or is
-     a query like Check.
-
-   The classification works on the assumption that we have 3 states:
-   parsing, execution (global enviroment, etc...), and proof
-   state. For example, commands that only alter the proof state are
-   considered safe to delegate to a worker.
-
-*)
-type vernac_type =
-  (* Start of a proof *)
-  | VtStartProof of vernac_start
-  (* Command altering the global state, bad for parallel
-     processing. *)
-  | VtSideff of vernac_sideff_type
-  (* End of a proof *)
-  | VtQed of vernac_qed_type
-  (* A proof step *)
-  | VtProofStep of proof_step
-  (* To be removed *)
-  | VtProofMode of string
-  (* Queries are commands assumed to be "pure", that is to say, they
-     don't modify the interpretation state. *)
-  | VtQuery
-  (* To be removed *)
-  | VtMeta
-  | VtUnknown
-and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *)
-and vernac_start = string * opacity_guarantee * Id.t list
-and vernac_sideff_type = Id.t list
-and opacity_guarantee =
-  | GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
-  | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*)
-and proof_step = { (* TODO: inline with OCaml 4.03 *)
-  parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ];
-  proof_block_detection : proof_block_name option
-}
-and solving_tac = bool (* a terminator *)
-and anon_abstracting_tac = bool (* abstracting anonymously its result *)
-and proof_block_name = string (* open type of delimiters *)
-type vernac_when =
-  | VtNow
-  | VtLater
-type vernac_classification = vernac_type * vernac_when
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index 5fba586298..3a321ecdb4 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -12,7 +12,43 @@ open Util
 open Pp
 open CErrors
 
-type 'a vernac_command = 'a -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t
+type vernac_type =
+  (* Start of a proof *)
+  | VtStartProof of vernac_start
+  (* Command altering the global state, bad for parallel
+     processing. *)
+  | VtSideff of vernac_sideff_type
+  (* End of a proof *)
+  | VtQed of vernac_qed_type
+  (* A proof step *)
+  | VtProofStep of {
+      parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ];
+      proof_block_detection : proof_block_name option
+    }
+  (* To be removed *)
+  | VtProofMode of string
+  (* Queries are commands assumed to be "pure", that is to say, they
+     don't modify the interpretation state. *)
+  | VtQuery
+  (* To be removed *)
+  | VtMeta
+  | VtUnknown
+and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *)
+and vernac_start = string * opacity_guarantee * Names.Id.t list
+and vernac_sideff_type = Names.Id.t list
+and opacity_guarantee =
+  | GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
+  | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*)
+and solving_tac = bool (** a terminator *)
+and anon_abstracting_tac = bool (** abstracting anonymously its result *)
+and proof_block_name = string (** open type of delimiters *)
+
+type vernac_when =
+  | VtNow
+  | VtLater
+type vernac_classification = vernac_type * vernac_when
+
+type 'a vernac_command = 'a -> atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t
 
 type plugin_args = Genarg.raw_generic_argument list
 
@@ -68,10 +104,23 @@ let call opn converted_args ~atts ~st =
 
 (** VERNAC EXTEND registering *)
 
-type classifier = Genarg.raw_generic_argument list -> Vernacexpr.vernac_classification
+type classifier = Genarg.raw_generic_argument list -> vernac_classification
+
+(** Classifiers  *)
+let classifiers : classifier array String.Map.t ref = ref String.Map.empty
+
+let get_vernac_classifier (name, i) args =
+  (String.Map.find name !classifiers).(i) args
+
+let declare_vernac_classifier name f =
+  classifiers := String.Map.add name f !classifiers
+
+let classify_as_query = VtQuery, VtLater
+let classify_as_sideeff = VtSideff [], VtLater
+let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None}, VtLater
 
 type (_, _) ty_sig =
-| TyNil : (atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
+| TyNil : (atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, vernac_classification) ty_sig
 | TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig
 | TyNonTerminal : ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> ('a -> 'r, 'a -> 's) ty_sig
 
@@ -124,7 +173,7 @@ let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s
 | TUentry a -> Aentry (Pcoq.genarg_grammar (Genarg.ExtraArg a))
 | TUentryl (a, i) -> Aentryl (Pcoq.genarg_grammar (Genarg.ExtraArg a), string_of_int i)
 
-let rec untype_grammar : type r s. (r, s) ty_sig -> Vernacexpr.vernac_expr Egramml.grammar_prod_item list = function
+let rec untype_grammar : type r s. (r, s) ty_sig -> 'a Egramml.grammar_prod_item list = function
 | TyNil -> []
 | TyTerminal (tok, ty) -> Egramml.GramTerminal tok :: untype_grammar ty
 | TyNonTerminal (tu, ty) ->
@@ -132,16 +181,6 @@ let rec untype_grammar : type r s. (r, s) ty_sig -> Vernacexpr.vernac_expr Egram
   let symb = untype_user_symbol tu in
   Egramml.GramNonTerminal (Loc.tag (t, symb)) :: untype_grammar ty
 
-let _ = untype_classifier, untype_command, untype_grammar, untype_user_symbol
-
-let classifiers : classifier array String.Map.t ref = ref String.Map.empty
-
-let get_vernac_classifier (name, i) args =
-  (String.Map.find name !classifiers).(i) args
-
-let declare_vernac_classifier name f =
-  classifiers := String.Map.add name f !classifiers
-
 let vernac_extend ~command ?classifier ?entry ext =
   let get_classifier (TyML (_, ty, _, cl)) = match cl with
   | Some cl -> untype_classifier ty cl
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index bb94f3a6a9..7feaccd9a3 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -8,20 +8,75 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+(** Vernacular Extension data *)
+
+(* A vernac classifier provides information about the exectuion of a
+   command:
+
+   - vernac_when: encodes if the vernac may alter the parser [thus
+     forcing immediate execution], or if indeed it is pure and parsing
+     can continue without its execution.
+
+   - vernac_type: if it is starts, ends, continues a proof or
+     alters the global state or is a control command like BackTo or is
+     a query like Check.
+
+   The classification works on the assumption that we have 3 states:
+   parsing, execution (global enviroment, etc...), and proof
+   state. For example, commands that only alter the proof state are
+   considered safe to delegate to a worker.
+
+*)
+type vernac_type =
+  (* Start of a proof *)
+  | VtStartProof of vernac_start
+  (* Command altering the global state, bad for parallel
+     processing. *)
+  | VtSideff of vernac_sideff_type
+  (* End of a proof *)
+  | VtQed of vernac_qed_type
+  (* A proof step *)
+  | VtProofStep of {
+      parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ];
+      proof_block_detection : proof_block_name option
+    }
+  (* To be removed *)
+  | VtProofMode of string
+  (* Queries are commands assumed to be "pure", that is to say, they
+     don't modify the interpretation state. *)
+  | VtQuery
+  (* To be removed *)
+  | VtMeta
+  | VtUnknown
+and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *)
+and vernac_start = string * opacity_guarantee * Names.Id.t list
+and vernac_sideff_type = Names.Id.t list
+and opacity_guarantee =
+  | GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
+  | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*)
+and solving_tac = bool (** a terminator *)
+and anon_abstracting_tac = bool (** abstracting anonymously its result *)
+and proof_block_name = string (** open type of delimiters *)
+
+type vernac_when =
+  | VtNow
+  | VtLater
+type vernac_classification = vernac_type * vernac_when
+
 (** Interpretation of extended vernac phrases. *)
 
-type 'a vernac_command = 'a -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t
+type 'a vernac_command = 'a -> atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t
 
 type plugin_args = Genarg.raw_generic_argument list
 
-val call : Vernacexpr.extend_name -> plugin_args -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t
+val call : Vernacexpr.extend_name -> plugin_args -> atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t
 
 (** {5 VERNAC EXTEND} *)
 
-type classifier = Genarg.raw_generic_argument list -> Vernacexpr.vernac_classification
+type classifier = Genarg.raw_generic_argument list -> vernac_classification
 
 type (_, _) ty_sig =
-| TyNil : (atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
+| TyNil : (atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, vernac_classification) ty_sig
 | TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig
 | TyNonTerminal :
   ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig ->
@@ -32,7 +87,7 @@ type ty_ml = TyML : bool (** deprecated *) * ('r, 's) ty_sig * 'r * 's option ->
 (** Wrapper to dynamically extend vernacular commands. *)
 val vernac_extend :
   command:string ->
-  ?classifier:(string -> Vernacexpr.vernac_classification) ->
+  ?classifier:(string -> vernac_classification) ->
   ?entry:Vernacexpr.vernac_expr Pcoq.Entry.t ->
   ty_ml list -> unit
 
@@ -55,6 +110,9 @@ val vernac_argument_extend : name:string -> 'a vernac_argument ->
   ('a, unit, unit) Genarg.genarg_type * 'a Pcoq.Entry.t
 
 (** {5 STM classifiers} *)
+val get_vernac_classifier : Vernacexpr.extend_name -> classifier
 
-val get_vernac_classifier :
-  Vernacexpr.extend_name -> classifier
+(** Standard constant classifiers *)
+val classify_as_query : vernac_classification
+val classify_as_sideeff : vernac_classification
+val classify_as_proofstep : vernac_classification