Infering atomic ML entries from their grammar.

3 files changed, 50 insertions, 56 deletions

diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index cca734720f..ef7cdbfa3a 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -86,14 +86,6 @@ let make_prod_item = function
 let mlexpr_of_clause cl =
   mlexpr_of_list (fun (a,_,_) -> mlexpr_of_list make_prod_item a) cl
 
-let rec make_tags loc = function
-  | [] -> <:expr< [] >>
-  | ExtNonTerminal (t, _, p) :: l ->
-      let l = make_tags loc l in
-      let t = mlexpr_of_argtype loc t in
-      <:expr< [ $t$ :: $l$ ] >>
-  | _::l -> make_tags loc l
-
 let make_one_printing_rule (pt,_,e) =
   let level = mlexpr_of_int 0 in (* only level 0 supported here *)
   let loc = MLast.loc_of_expr e in
@@ -103,41 +95,6 @@ let make_one_printing_rule (pt,_,e) =
 
 let make_printing_rule r = mlexpr_of_list make_one_printing_rule r
 
-let make_empty_check = function
-| ExtNonTerminal (t, e, _)->
-  let is_extra = match t with ExtraArgType _ -> true | _ -> false in
-  if is_possibly_empty e || is_extra then
-    (* This possibly parses epsilon *)
-    let wit = make_wit loc t in
-    let rawwit = make_rawwit loc t in
-    <:expr<
-      match Genarg.default_empty_value $wit$ with
-      [ None -> raise Exit
-      | Some v ->
-        Tacintern.intern_genarg Tacintern.fully_empty_glob_sign
-          (Genarg.in_gen $rawwit$ v) ] >>
-  else
-  (* This does not parse epsilon (this Exit is static time) *)
-    raise Exit
-| ExtTerminal _ ->
-  (* Idem *)
-  raise Exit
-
-let rec possibly_atomic loc = function
-| [] -> []
-| ((ExtNonTerminal _ :: _ | []), _, _) :: rem ->
-  (** This is not parsed by the TACTIC EXTEND rules *)
-  assert false
-| (ExtTerminal s :: prods, _, _) :: rem ->
-  let entry =
-    try
-      let l = List.map make_empty_check prods in
-      let l = mlexpr_of_list (fun x -> x) l in
-      (s, <:expr< try Some $l$ with [ Exit -> None ] >>)
-    with Exit -> (s, <:expr< None >>)
-  in
-  entry :: possibly_atomic loc rem
-
 (** Special treatment of constr entries *)
 let is_constr_gram = function
 | ExtTerminal _ -> false
@@ -193,10 +150,7 @@ let declare_tactic loc s c cl = match cl with
   let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in
   let pp = make_printing_rule cl in
   let gl = mlexpr_of_clause cl in
-  let atom =
-    mlexpr_of_list (mlexpr_of_pair mlexpr_of_string (fun x -> x))
-      (possibly_atomic loc cl) in
-  let obj = <:expr< fun () -> Metasyntax.add_ml_tactic_notation $se$ $gl$ $atom$ >> in
+  let obj = <:expr< fun () -> Metasyntax.add_ml_tactic_notation $se$ $gl$ >> in
   declare_str_items loc
     [ <:str_item< do {
       try do {
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 5a47fc0ea1..0d002aa8e9 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -149,8 +149,6 @@ let add_tactic_notation (local,n,prods,e) =
 (**********************************************************************)
 (* ML Tactic entries                                                  *)
 
-type atomic_entry = string * Genarg.glob_generic_argument list option
-
 type ml_tactic_grammar_obj = {
   mltacobj_name : Tacexpr.ml_tactic_name;
   (** ML-side unique name *)
@@ -158,12 +156,56 @@ type ml_tactic_grammar_obj = {
   (** Grammar rules generating the ML tactic. *)
 }
 
+exception NonEmptyArgument
+
+let default_empty_value wit = match Genarg.default_empty_value wit with
+| None -> raise NonEmptyArgument
+| Some v -> v
+
+let rec empty_value : type a b c s. (a, b, c) Genarg.genarg_type -> (s, a) entry_key -> a =
+fun wit key -> match key with
+| Alist1 key ->
+  begin match wit with
+  | Genarg.ListArg wit -> [empty_value wit key]
+  | Genarg.ExtraArg _ -> default_empty_value wit
+  end
+| Alist1sep (key, _) ->
+  begin match wit with
+  | Genarg.ListArg wit -> [empty_value wit key]
+  | Genarg.ExtraArg _ -> default_empty_value wit
+  end
+| Alist0 _ -> []
+| Alist0sep (_, _) -> []
+| Amodifiers _ -> []
+| Aopt _ -> None
+| Aentry _ -> default_empty_value wit
+| Aentryl (_, _) -> default_empty_value wit
+
+| Atoken _ -> raise NonEmptyArgument
+| Aself -> raise NonEmptyArgument
+| Anext -> raise NonEmptyArgument
+
 (** ML tactic notations whose use can be restricted to an identifier are added
     as true Ltac entries. *)
 let extend_atomic_tactic name entries =
-  let add_atomic i (id, args) = match args with
+  let map_prod prods =
+    let (hd, rem) = match prods with
+    | GramTerminal s :: rem -> (s, rem)
+    | _ -> assert false (** Not handled by the ML extension syntax *)
+    in
+    let empty_value = function
+    | GramTerminal s -> raise NonEmptyArgument
+    | GramNonTerminal (_, typ, e) ->
+      let Genarg.Rawwit wit = typ in
+      let def = Genarg.in_gen typ (empty_value wit e) in
+      Tacintern.intern_genarg Tacintern.fully_empty_glob_sign def
+    in
+    try Some (hd, List.map empty_value rem) with NonEmptyArgument -> None
+  in
+  let entries = List.map map_prod entries in
+  let add_atomic i args = match args with
   | None -> ()
-  | Some args ->
+  | Some (id, args) ->
     let open Tacexpr in
     let args = List.map (fun a -> TacGeneric a) args in
     let entry = { mltac_name = name; mltac_index = i } in
@@ -186,13 +228,13 @@ let inMLTacticGrammar : ml_tactic_grammar_obj -> obj =
     subst_function = (fun (_, o) -> o);
   }
 
-let add_ml_tactic_notation name prods atomic =
+let add_ml_tactic_notation name prods =
   let obj = {
     mltacobj_name = name;
     mltacobj_prod = prods;
   } in
   Lib.add_anonymous_leaf (inMLTacticGrammar obj);
-  extend_atomic_tactic name atomic
+  extend_atomic_tactic name prods
 
 (**********************************************************************)
 (* Printing grammar entries                                           *)
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index 826886f678..5d01405b27 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -21,10 +21,8 @@ val add_tactic_notation :
   locality_flag * int * grammar_tactic_prod_item_expr list * raw_tactic_expr ->
     unit
 
-type atomic_entry = string * Genarg.glob_generic_argument list option
-
 val add_ml_tactic_notation : ml_tactic_name ->
-  Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list list -> atomic_entry list -> unit
+  Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list list -> unit
 
 (** Adding a (constr) notation in the environment*)