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.

3 files changed, 235 insertions, 5 deletions

diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4
index d33ec91f9d..4d3507cbc4 100644
--- a/ltac/extraargs.ml4
+++ b/ltac/extraargs.ml4
@@ -25,7 +25,7 @@ open Locus
 
 let create_generic_quotation name e wit =
   let inject (loc, v) = Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit wit) v) in
-  Egramcoq.create_ltac_quotation name inject (e, None)
+  Tacentries.create_ltac_quotation name inject (e, None)
 
 let () = create_generic_quotation "integer" Pcoq.Prim.integer Stdarg.wit_int
 let () = create_generic_quotation "string" Pcoq.Prim.string Stdarg.wit_string
@@ -38,7 +38,7 @@ let () = create_generic_quotation "ipattern" Pcoq.Tactic.simple_intropattern Con
 let () = create_generic_quotation "open_constr" Pcoq.Constr.lconstr Constrarg.wit_open_constr
 let () =
   let inject (loc, v) = Tacexpr.Tacexp v in
-  Egramcoq.create_ltac_quotation "ltac" inject (Pcoq.Tactic.tactic_expr, Some 5)
+  Tacentries.create_ltac_quotation "ltac" inject (Pcoq.Tactic.tactic_expr, Some 5)
 
 (* Rewriting orientation *)
 
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml
index 711cd8d9d0..99c2213e19 100644
--- a/ltac/tacentries.ml
+++ b/ltac/tacentries.ml
@@ -11,6 +11,7 @@ open Errors
 open Util
 open Names
 open Libobject
+open Genarg
 open Pcoq
 open Egramml
 open Egramcoq
@@ -19,6 +20,196 @@ open Libnames
 open Nameops
 
 (**********************************************************************)
+(* 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 atactic n =
+  let open Extend in
+  if n = 5 then Aentry (name_of_entry Tactic.binder_tactic)
+  else Aentryl (name_of_entry Tactic.tactic_expr, n)
+
+type entry_name = EntryName :
+  'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, 'a) Extend.symbol -> entry_name
+
+let try_get_entry u s =
+  let open Extend in
+  (** 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 open Extend in
+  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 Constrarg.wit_tactic, Aself)
+  else if check_lvl (n + 1) then EntryName (rawwit Constrarg.wit_tactic, Anext)
+  else EntryName (rawwit Constrarg.wit_tactic, atactic n)
+
+let rec parse_user_entry s sep =
+  let open Extend in
+  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 interp_entry_name up_level s sep =
+  let open Extend in
+  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)
+
+(**********************************************************************)
+(** 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)^".")
+
+(**********************************************************************)
+(** State of the grammar extensions                                   *)
+
+type tactic_grammar = {
+  tacgram_level : int;
+  tacgram_prods : Tacexpr.raw_tactic_expr grammar_prod_item list;
+}
+
+(** ML Tactic grammar extensions *)
+
+let add_ml_tactic_entry (name, prods) =
+  let entry = Tactic.simple_tactic in
+  let mkact i loc l : Tacexpr.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 open Tacexpr in
+  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 tactic_grammar =
+  create_grammar_command "TacticGrammar" add_tactic_entry
+
+let ml_tactic_grammar =
+  create_grammar_command "MLTacticGrammar" add_ml_tactic_entry
+
+let extend_tactic_grammar kn ntn = extend_grammar tactic_grammar (kn, ntn)
+let extend_ml_tactic_grammar n ntn = extend_grammar ml_tactic_grammar (n, ntn)
+
+(**********************************************************************)
 (* Tactic Notation                                                    *)
 
 let interp_prod_item lev = function
@@ -63,13 +254,13 @@ let cache_tactic_notation (_, tobj) =
   let key = tobj.tacobj_key in
   let () = check_key key in
   Tacenv.register_alias key tobj.tacobj_body;
-  Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram;
+  extend_tactic_grammar key tobj.tacobj_tacgram;
   Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp
 
 let open_tactic_notation i (_, tobj) =
   let key = tobj.tacobj_key in
   if Int.equal i 1 && not tobj.tacobj_local then
-    Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram
+    extend_tactic_grammar key tobj.tacobj_tacgram
 
 let load_tactic_notation i (_, tobj) =
   let key = tobj.tacobj_key in
@@ -78,7 +269,7 @@ let load_tactic_notation i (_, tobj) =
   Tacenv.register_alias key tobj.tacobj_body;
   Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp;
   if Int.equal i 1 && not tobj.tacobj_local then
-    Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram
+    extend_tactic_grammar key tobj.tacobj_tacgram
 
 let subst_tactic_notation (subst, tobj) =
   let (ids, body) = tobj.tacobj_body in
@@ -188,6 +379,37 @@ let add_ml_tactic_notation name prods =
   Lib.add_anonymous_leaf (inMLTacticGrammar obj);
   extend_atomic_tactic name prods
 
+(**********************************************************************)
+(** Ltac quotations                                                   *)
+
+let ltac_quotations = ref String.Set.empty
+
+let create_ltac_quotation name cast (e, l) =
+  let open Extend in
+  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])
+
 (** Command *)
 
 
diff --git a/ltac/tacentries.mli b/ltac/tacentries.mli
index 3cf0bc5cc9..b60d8f478e 100644
--- a/ltac/tacentries.mli
+++ b/ltac/tacentries.mli
@@ -19,3 +19,11 @@ val add_ml_tactic_notation : ml_tactic_name ->
   Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list list -> unit
 
 val register_ltac : bool -> Vernacexpr.tacdef_body list -> unit
+
+(** {5 Adding tactic quotations} *)
+
+val create_ltac_quotation : string ->
+  ('grm Loc.located -> raw_tactic_arg) -> ('grm Pcoq.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]. *)