TACTIC EXTEND now takes an optional level as argument.

The syntax is: TACTIC EXTEND foo AT LEVEL i

This commit makes it possible to define tacticals like the ssreflect
arrow without having to resort to GEXTEND statements and intepretation
hacks.

Note that it simply makes accessible through the ML interface what Tactic
Notation already supports:

Tactic Notation (at level 1) tactic1(t) "=>" ipats(l) := ...

3 files changed, 19 insertions, 19 deletions

diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp
index fe864ed40..6c1757dd2 100644
--- a/grammar/tacextend.mlp
+++ b/grammar/tacextend.mlp
@@ -82,14 +82,14 @@ let make_var = function
   | ExtNonTerminal (_, p) -> Some p
   | _ -> assert false
 
-let declare_tactic loc s c cl = match cl with
+let declare_tactic loc tacname ~level classification clause = match clause with
 | [(ExtTerminal name) :: rem, _, tac] when List.for_all is_constr_gram rem ->
   (** The extension is only made of a name followed by constr entries: we do not
       add any grammar nor printing rule and add it as a true Ltac definition. *)
   let patt = make_patt rem in
   let vars = List.map make_var rem in
   let vars = mlexpr_of_list (mlexpr_of_option mlexpr_of_ident) vars in
-  let entry = mlexpr_of_string s in
+  let entry = mlexpr_of_string tacname in
   let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in
   let ml = <:expr< { Tacexpr.mltac_name = $se$; Tacexpr.mltac_index = 0 } >> in
   let name = mlexpr_of_string name in
@@ -117,13 +117,14 @@ let declare_tactic loc s c cl = match cl with
 | _ ->
   (** Otherwise we add parsing and printing rules to generate a call to a
       TacML tactic. *)
-  let entry = mlexpr_of_string s in
+  let entry = mlexpr_of_string tacname in
   let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in
-  let gl = mlexpr_of_clause cl in
-  let obj = <:expr< fun () -> Tacentries.add_ml_tactic_notation $se$ $gl$ >> in
+  let gl = mlexpr_of_clause clause in
+  let level = mlexpr_of_int level in
+  let obj = <:expr< fun () -> Tacentries.add_ml_tactic_notation $se$ $level$ $gl$ >> in
   declare_str_items loc
     [ <:str_item< do {
-        Tacenv.register_ml_tactic $se$ (Array.of_list $make_fun_clauses loc s cl$);
+        Tacenv.register_ml_tactic $se$ (Array.of_list $make_fun_clauses loc tacname clause$);
         Mltop.declare_cache_obj $obj$ $plugin_name$; } >>
     ]
 
@@ -134,20 +135,17 @@ EXTEND
   GLOBAL: str_item;
   str_item:
     [ [ "TACTIC"; "EXTEND"; s = tac_name;
+        level = OPT [ "AT"; "LEVEL"; level = INT -> level ];
         c = OPT [ "CLASSIFIED"; "BY"; c = LIDENT -> <:expr< $lid:c$ >> ];
         OPT "|"; l = LIST1 tacrule SEP "|";
         "END" ->
-         declare_tactic loc s c l ] ]
+        let level = match level with Some i -> int_of_string i | None -> 0 in
+         declare_tactic loc s ~level c l ] ]
   ;
   tacrule:
     [ [ "["; l = LIST1 tacargs; "]";
         c = OPT [ "=>"; "["; c = Pcaml.expr; "]" -> c ];
-        "->"; "["; e = Pcaml.expr; "]" ->
-	(match l with
-	  | ExtNonTerminal _ :: _ ->
-	    (* En attendant la syntaxe de tacticielles *)
-	    failwith "Tactic syntax must start with an identifier"
-	  | _ -> (l,c,e))
+        "->"; "["; e = Pcaml.expr; "]" -> (l,c,e)
     ] ]
   ;
   tacargs:
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 2e2b55be7..8570b5a44 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -302,9 +302,9 @@ let cons_production_parameter = function
 | TacTerm _ -> None
 | TacNonTerm (_, _, id) -> Some id
 
-let add_glob_tactic_notation local n prods forml ids tac =
+let add_glob_tactic_notation local ~level prods forml ids tac =
   let parule = {
-    tacgram_level = n;
+    tacgram_level = level;
     tacgram_prods = prods;
   } in
   let tacobj = {
@@ -360,7 +360,7 @@ let extend_atomic_tactic name entries =
   in
   List.iteri add_atomic entries
 
-let add_ml_tactic_notation name prods =
+let add_ml_tactic_notation name ~level prods =
   let len = List.length prods in
   let iter i prods =
     let open Tacexpr in
@@ -372,10 +372,12 @@ let add_ml_tactic_notation name prods =
     let entry = { mltac_name = name; mltac_index = len - i - 1 } in
     let map id = Reference (Misctypes.ArgVar (Loc.ghost, id)) in
     let tac = TacML (Loc.ghost, entry, List.map map ids) in
-    add_glob_tactic_notation false 0 prods true ids tac
+    add_glob_tactic_notation false ~level prods true ids tac
   in
   List.iteri iter (List.rev prods);
-  extend_atomic_tactic name prods
+  (** We call [extend_atomic_tactic] only for "basic tactics" (the ones at
+  tactic_expr level 0) *)
+  if Int.equal level 0 then extend_atomic_tactic name prods
 
 (**********************************************************************)
 (** Ltac quotations                                                   *)
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 969c118fb..069504473 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -45,7 +45,7 @@ val register_tactic_notation_entry : string -> ('a, 'b, 'c) Genarg.genarg_type -
     to finding an argument by name (as in {!Genarg}) if there is none
     matching. *)
 
-val add_ml_tactic_notation : ml_tactic_name ->
+val add_ml_tactic_notation : ml_tactic_name -> level:int ->
   argument grammar_tactic_prod_item_expr list list -> unit
 (** A low-level variant of {!add_tactic_notation} used by the TACTIC EXTEND
     ML-side macro. *)