Providing an API to access the parsing engine summary in a first-class way.

Instead of hardwiring a few special cases in Egramcoq, we allow the grammar
state to contain arbitrary data structures. This permits to extend the parsing
engine while retaining the synchronization with the global state, e.g. for use
in plugins.

4 files changed, 43 insertions, 261 deletions

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 8c4930806e..f0c12ab8ef 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -217,115 +217,48 @@ let extend_constr_pat_notation ng =
   let ext = ETConstr (level, ()), ng.notgram_assoc in
   extend_constr e ext (make_cases_pattern_action mkact) true ng.notgram_prods
 
-let extend_constr_notation ng =
+let extend_constr_notation (_, ng) =
   (* Add the notation in constr *)
   let nb = extend_constr_constr_notation ng in
   (* Add the notation in cases_pattern *)
   let nb' = extend_constr_pat_notation ng in
   nb + nb'
 
-(**********************************************************************)
-(** Grammar declaration for Tactic Notation (Coq level)               *)
-
-let get_tactic_entry n =
-  if Int.equal n 0 then
-    Tactic.simple_tactic, None
-  else if Int.equal n 5 then
-    Tactic.binder_tactic, None
-  else if 1<=n && n<5 then
-    Tactic.tactic_expr, Some (Extend.Level (string_of_int n))
-  else
-    error ("Invalid Tactic Notation level: "^(string_of_int n)^".")
+module GrammarCommand = Dyn.Make(struct end)
+module GrammarInterp = struct type 'a t = 'a -> int end
+module GrammarInterpMap = GrammarCommand.Map(GrammarInterp)
 
-(**********************************************************************)
-(** State of the grammar extensions                                   *)
+let grammar_interp = ref GrammarInterpMap.empty
 
-type tactic_grammar = {
-  tacgram_level : int;
-  tacgram_prods : Tacexpr.raw_tactic_expr grammar_prod_item list;
-}
+let (grammar_state : (int * GrammarCommand.t) list ref) = ref []
 
-type all_grammar_command =
-  | Notation of Notation.level * notation_grammar
-  | TacticGrammar of KerName.t * tactic_grammar
-  | MLTacticGrammar of ml_tactic_name * Tacexpr.raw_tactic_expr grammar_prod_item list list
+type 'a grammar_command = 'a GrammarCommand.tag
 
-(** ML Tactic grammar extensions *)
+let create_grammar_command name interp : _ grammar_command =
+  let obj = GrammarCommand.create name in
+  let () = grammar_interp := GrammarInterpMap.add obj interp !grammar_interp in
+  obj
 
-let add_ml_tactic_entry name prods =
-  let entry = Tactic.simple_tactic in
-  let mkact i loc l : raw_tactic_expr =
-    let open Tacexpr in
-    let entry = { mltac_name = name; mltac_index = i } in
-    let map arg = TacGeneric arg in
-    TacML (loc, entry, List.map map l)
-  in
-  let rules = List.map_i (fun i p -> make_rule (mkact i) p) 0 prods in
-  synchronize_level_positions ();
-  grammar_extend entry None (None, [(None, None, List.rev rules)]);
-  1
-
-(* Declaration of the tactic grammar rule *)
-
-let head_is_ident tg = match tg.tacgram_prods with
-| GramTerminal _::_ -> true
-| _ -> false
-
-(** Tactic grammar extensions *)
-
-let add_tactic_entry kn tg =
-  let entry, pos = get_tactic_entry tg.tacgram_level in
-  let mkact loc l =
-    let filter = function
-    | GramTerminal _ -> None
-    | GramNonTerminal (_, t, _) -> Some (Genarg.unquote t)
-    in
-    let types = List.map_filter filter tg.tacgram_prods in
-    let map arg t =
-      (** HACK to handle especially the tactic(...) entry *)
-      let wit = Genarg.rawwit Constrarg.wit_tactic in
-      if Genarg.argument_type_eq t (Genarg.unquote wit) then
-        Tacexp (Genarg.out_gen wit arg)
-      else
-        TacGeneric arg
-    in
-    let l = List.map2 map l types in
-    (TacAlias (loc,kn,l):raw_tactic_expr)
-  in
-  let () =
-    if Int.equal tg.tacgram_level 0 && not (head_is_ident tg) then
-      error "Notation for simple tactic must start with an identifier."
-  in
-  let rules = make_rule mkact tg.tacgram_prods in
-  synchronize_level_positions ();
-  grammar_extend entry None (pos, [(None, None, List.rev [rules])]);
-  1
-
-let (grammar_state : (int * all_grammar_command) list ref) = ref []
-
-let extend_grammar gram =
-  let nb = match gram with
-  | Notation (_,a) -> extend_constr_notation a
-  | TacticGrammar (kn, g) -> add_tactic_entry kn g
-  | MLTacticGrammar (name, pr) -> add_ml_tactic_entry name pr
-  in
-  grammar_state := (nb,gram) :: !grammar_state
+let extend_grammar tag g =
+  let nb = GrammarInterpMap.find tag !grammar_interp g in
+  grammar_state := (nb, GrammarCommand.Dyn (tag, g)) :: !grammar_state
 
-let extend_constr_grammar pr ntn =
-  extend_grammar (Notation (pr, ntn))
+let extend_dyn_grammar (GrammarCommand.Dyn (tag, g)) = extend_grammar tag g
 
-let extend_tactic_grammar kn ntn =
-  extend_grammar (TacticGrammar (kn, ntn))
+let constr_grammar : (Notation.level * notation_grammar) GrammarCommand.tag =
+  create_grammar_command "Notation" extend_constr_notation
 
-let extend_ml_tactic_grammar name ntn =
-  extend_grammar (MLTacticGrammar (name, ntn))
+let extend_constr_grammar pr ntn = extend_grammar constr_grammar (pr, ntn)
 
 let recover_constr_grammar ntn prec =
-  let filter = function
-  | _, Notation (prec', ng) when
-      Notation.level_eq prec prec' &&
-      String.equal ntn ng.notgram_notation -> Some ng
-  | _ -> None
+  let filter (_, gram) : notation_grammar option = match gram with
+  | GrammarCommand.Dyn (tag, obj) ->
+    match GrammarCommand.eq tag constr_grammar with
+    | None -> None
+    | Some Refl ->
+      let (prec', ng) = obj in
+      if Notation.level_eq prec prec' && String.equal ntn ng.notgram_notation then Some ng
+      else None
   in
   match List.map_filter filter !grammar_state with
   | [x] -> x
@@ -334,7 +267,7 @@ let recover_constr_grammar ntn prec =
 (* Summary functions: the state of the lexer is included in that of the parser.
    Because the grammar affects the set of keywords when adding or removing
    grammar rules. *)
-type frozen_t = (int * all_grammar_command) list * Lexer.frozen_t
+type frozen_t = (int * GrammarCommand.t) list * Lexer.frozen_t
 
 let freeze _ : frozen_t = (!grammar_state, Lexer.freeze ())
 
@@ -353,7 +286,7 @@ let unfreeze (grams, lex) =
   remove_levels n;
   grammar_state := common;
   Lexer.unfreeze lex;
-  List.iter extend_grammar (List.rev_map snd redo)
+  List.iter extend_dyn_grammar (List.rev_map snd redo)
 
 (** No need to provide an init function : the grammar state is
     statically available, and already empty initially, while
@@ -373,33 +306,3 @@ let with_grammar_rule_protection f x =
     let reraise = Errors.push reraise in
     let () = unfreeze fs in
     iraise reraise
-
-(**********************************************************************)
-(** Ltac quotations                                                   *)
-
-let ltac_quotations = ref String.Set.empty
-
-let create_ltac_quotation name cast (e, l) =
-  let () =
-    if String.Set.mem name !ltac_quotations then
-      failwith ("Ltac quotation " ^ name ^ " already registered")
-  in
-  let () = ltac_quotations := String.Set.add name !ltac_quotations in
-  let entry = match l with
-  | None -> Aentry (name_of_entry e)
-  | Some l -> Aentryl (name_of_entry e, l)
-  in
-(*   let level = Some "1" in *)
-  let level = None in
-  let assoc = None in
-  let rule =
-    Next (Next (Next (Next (Next (Stop,
-      Atoken (Lexer.terminal name)),
-      Atoken (Lexer.terminal ":")),
-      Atoken (Lexer.terminal "(")),
-      entry),
-      Atoken (Lexer.terminal ")"))
-  in
-  let action _ v _ _ _ loc = cast (loc, v) in
-  let gram = (level, assoc, [Rule (rule, action)]) in
-  Pcoq.grammar_extend Tactic.tactic_arg None (None, [gram])
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli
index 23eaa64eec..6ec1066260 100644
--- a/parsing/egramcoq.mli
+++ b/parsing/egramcoq.mli
@@ -36,34 +36,27 @@ type notation_grammar = {
   notgram_typs : notation_var_internalization_type list;
 }
 
-type tactic_grammar = {
-  tacgram_level : int;
-  tacgram_prods : Tacexpr.raw_tactic_expr grammar_prod_item list;
-}
+(** {5 Extending the parser with Summary-synchronized commands} *)
+
+type 'a grammar_command
+(** Type of synchronized parsing extensions. The ['a] type should be
+    marshallable. *)
+
+val create_grammar_command : string -> ('a -> int) -> 'a grammar_command
+(** Create a new grammar-modifying command with the given name. The function
+    should modify the parser state and return the number of grammar extensions
+    performed. *)
+
+val extend_grammar : 'a grammar_command -> 'a -> unit
+(** Extend the grammar of Coq with the given data. *)
 
 (** {5 Adding notations} *)
 
 val extend_constr_grammar : Notation.level -> notation_grammar -> unit
 (** Add a term notation rule to the parsing system. *)
 
-val extend_tactic_grammar : KerName.t -> tactic_grammar -> unit
-(** Add a tactic notation rule to the parsing system. This produces a TacAlias
-    tactic with the provided kernel name. *)
-
-val extend_ml_tactic_grammar : Tacexpr.ml_tactic_name -> Tacexpr.raw_tactic_expr grammar_prod_item list list -> unit
-(** Add a ML tactic notation rule to the parsing system. This produces a
-    TacML tactic with the provided string as name. *)
-
 val recover_constr_grammar : notation -> Notation.level -> notation_grammar
 (** For a declared grammar, returns the rule + the ordered entry types
     of variables in the rule (for use in the interpretation) *)
 
 val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b
-
-(** {5 Adding tactic quotations} *)
-
-val create_ltac_quotation : string ->
-  ('grm Loc.located -> Tacexpr.raw_tactic_arg) -> ('grm Gram.entry * int option) -> unit
-(** [create_ltac_quotation name f e] adds a quotation rule to Ltac, that is,
-    Ltac grammar now accepts arguments of the form ["name" ":" "(" <e> ")"], and
-    generates an argument using [f] on the entry parsed by [e]. *)
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 207b43064c..75144addb2 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -57,16 +57,6 @@ type typed_entry = TypedEntry : 'a raw_abstract_argument_type * 'a G.entry -> ty
 let object_of_typed_entry (TypedEntry (_, e)) = Gramobj.weaken_entry e
 let weaken_entry x = Gramobj.weaken_entry x
 
-(** General entry keys *)
-
-(** This intermediate abstract representation of entries can
-   both be reified into mlexpr for the ML extensions and
-   dynamically interpreted as entries for the Coq level extensions
-*)
-
-type entry_name = EntryName :
-  'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, 'a) symbol -> entry_name
-
 (** Grammar extensions *)
 
 (** NB: [extend_statment =
@@ -740,108 +730,8 @@ let grammar_extend e reinit ext =
   let ext = of_coq_extend_statement ext in
   unsafe_grammar_extend e reinit ext
 
-(**********************************************************************)
-(* Interpret entry names of the form "ne_constr_list" as entry keys   *)
-
-let coincide s pat off =
-  let len = String.length pat in
-  let break = ref true in
-  let i = ref 0 in
-  while !break && !i < len do
-    let c = Char.code s.[off + !i] in
-    let d = Char.code pat.[!i] in
-    break := Int.equal c d;
-    incr i
-  done;
-  !break
-
 let name_of_entry e = Entry.unsafe_of_name (Gram.Entry.name e)
 
-let atactic n =
-  if n = 5 then Aentry (name_of_entry Tactic.binder_tactic)
-  else Aentryl (name_of_entry Tactic.tactic_expr, n)
-
-let try_get_entry u s =
-  (** Order the effects: get_entry can raise Not_found *)
-  let TypedEntry (typ, e) = get_entry u s in
-  EntryName (typ, Aentry (name_of_entry e))
-
-(** Quite ad-hoc *)
-let get_tacentry n m =
-  let check_lvl n =
-    Int.equal m n
-    && not (Int.equal m 5) (* Because tactic5 is at binder_tactic *)
-    && not (Int.equal m 0) (* Because tactic0 is at simple_tactic *)
-  in
-  if check_lvl n then EntryName (rawwit wit_tactic, Aself)
-  else if check_lvl (n + 1) then EntryName (rawwit wit_tactic, Anext)
-  else EntryName (rawwit wit_tactic, atactic n)
-
-let rec parse_user_entry s sep =
-  let l = String.length s in
-  if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then
-    let entry = parse_user_entry (String.sub s 3 (l-8)) "" in
-    Ulist1 entry
-  else if l > 12 && coincide s "ne_" 0 &&
-                   coincide s "_list_sep" (l-9) then
-    let entry = parse_user_entry (String.sub s 3 (l-12)) "" in
-    Ulist1sep (entry, sep)
-  else if l > 5 && coincide s "_list" (l-5) then
-    let entry = parse_user_entry (String.sub s 0 (l-5)) "" in
-    Ulist0 entry
-  else if l > 9 && coincide s "_list_sep" (l-9) then
-    let entry = parse_user_entry (String.sub s 0 (l-9)) "" in
-    Ulist0sep (entry, sep)
-  else if l > 4 && coincide s "_opt" (l-4) then
-    let entry = parse_user_entry (String.sub s 0 (l-4)) "" in
-    Uopt entry
-  else if l > 5 && coincide s "_mods" (l-5) then
-    let entry = parse_user_entry (String.sub s 0 (l-1)) "" in
-    Umodifiers entry
-  else if Int.equal l 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then
-    let n = Char.code s.[6] - 48 in
-    Uentryl ("tactic", n)
-  else
-    let s = match s with "hyp" -> "var" | _ -> s in
-    Uentry s
-
-let arg_list = function Rawwit t -> Rawwit (ListArg t)
-let arg_opt = function Rawwit t -> Rawwit (OptArg t)
-
-let rec interp_entry_name up_level s sep =
-  let rec eval = function
-  | Ulist1 e ->
-    let EntryName (t, g) = eval e in
-    EntryName (arg_list t, Alist1 g)
-  | Ulist1sep (e, sep) ->
-    let EntryName (t, g) = eval e in
-    EntryName (arg_list t, Alist1sep (g, sep))
-  | Ulist0 e ->
-    let EntryName (t, g) = eval e in
-    EntryName (arg_list t, Alist0 g)
-  | Ulist0sep (e, sep) ->
-    let EntryName (t, g) = eval e in
-    EntryName (arg_list t, Alist0sep (g, sep))
-  | Uopt e ->
-    let EntryName (t, g) = eval e in
-    EntryName (arg_opt t, Aopt g)
-  | Umodifiers e ->
-    let EntryName (t, g) = eval e in
-    EntryName (arg_list t, Amodifiers g)
-  | Uentry s ->
-    begin
-      try try_get_entry uprim s with Not_found ->
-      try try_get_entry uconstr s with Not_found ->
-      try try_get_entry utactic s with Not_found ->
-      error ("Unknown entry "^s^".")
-    end
-  | Uentryl (s, n) ->
-    (** FIXME: do better someday *)
-    assert (String.equal s "tactic");
-    get_tacentry n up_level
-  in
-  eval (parse_user_entry s sep)
-
 let list_entry_names () =
   let add_entry key (TypedEntry (entry, _)) accu = (key, unquote entry) :: accu in
   let ans = Hashtbl.fold add_entry (get_utable uprim) [] in
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 35973a4d72..afe8889096 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -268,13 +268,9 @@ val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option
 
 (** Binding general entry keys to symbols *)
 
-type entry_name = EntryName :
-  'a raw_abstract_argument_type * (raw_tactic_expr, 'a) Extend.symbol -> entry_name
+type typed_entry = TypedEntry : 'a raw_abstract_argument_type * 'a Gram.entry -> typed_entry
 
-(** [interp_entry_name lev n sep] returns the entry corresponding to the name
-    [n] of the form "ne_constr_list" in a tactic entry of level [lev] with
-    separator [sep]. *)
-val interp_entry_name : int -> string -> string -> entry_name
+val get_entry : gram_universe -> string -> typed_entry
 
 (** Recover the list of all known tactic notation entries. *)
 val list_entry_names : unit -> (string * argument_type) list