Separate interpretation and syntax declaration in tactic notations

This is a step towards #15409.

Author: maximedenes

doc/tools/docgram/common.edit_mlg

@@ -2115,8 +2115,6 @@ ltac2_occs_nums: [
 ltac2_entry: [
 | REPLACE tac2def_typ      (* Ltac2 plugin *)
 | WITH "Ltac2" tac2def_typ
-| REPLACE tac2def_syn      (* Ltac2 plugin *)
-| WITH "Ltac2" tac2def_syn
 | REPLACE tac2def_mut      (* Ltac2 plugin *)
 | WITH "Ltac2" tac2def_mut
 | REPLACE tac2def_val     (* Ltac2 plugin *)
@@ -2145,6 +2143,7 @@ SPLICE: [
 | tac2def_typ
 | tac2def_ext
 | tac2def_syn
+| ltac2def_syn
 | tac2def_mut
 | rec_flag
 | locident

doc/tools/docgram/fullGrammar

@@ -697,6 +697,7 @@ command: [
 | "Number" "Notation" reference reference reference OPT number_options ":" preident
 | "String" "Notation" reference reference reference OPT string_option ":" preident
 | "Ltac2" ltac2_entry      (* ltac2 plugin *)
+| "Ltac2" "Notation" ltac2def_syn      (* ltac2 plugin *)
 | "Ltac2" "Eval" ltac2_expr6      (* ltac2 plugin *)
 | "Print" "Ltac2" reference      (* ltac2 plugin *)
 | "Locate" "Ltac2" reference      (* ltac2 plugin *)
@@ -3561,7 +3562,7 @@ syn_level: [
 ]
 
 tac2def_syn: [
-| "Notation" LIST1 ltac2_scope syn_level ":=" ltac2_expr6      (* ltac2 plugin *)
+| LIST1 ltac2_scope syn_level ":=" ltac2_expr6      (* ltac2 plugin *)
 ]
 
 lident: [
@@ -3938,10 +3939,13 @@ ltac2_entry: [
 | tac2def_val      (* ltac2 plugin *)
 | tac2def_typ      (* ltac2 plugin *)
 | tac2def_ext      (* ltac2 plugin *)
-| tac2def_syn      (* ltac2 plugin *)
 | tac2def_mut      (* ltac2 plugin *)
 ]
 
+ltac2def_syn: [
+| tac2def_syn      (* ltac2 plugin *)
+]
+
 ltac2_expr: [
 | _ltac2_expr      (* ltac2 plugin *)
 ]

doc/tools/docgram/orderedGrammar

@@ -1118,7 +1118,7 @@ command: [
 | "Ltac2" OPT "mutable" OPT "rec" tac2def_body LIST0 ( "with" tac2def_body )
 | "Ltac2" "Type" OPT "rec" tac2typ_def LIST0 ( "with" tac2typ_def )
 | "Ltac2" "@" "external" ident ":" ltac2_type ":=" string string
-| "Ltac2" "Notation" LIST1 ltac2_scope OPT ( ":" natural ) ":=" ltac2_expr
+| "Ltac2" "Notation" LIST1 ltac2_scope OPT ( ":" natural ) ":=" ltac2_expr      (* ltac2 plugin *)
 | "Ltac2" "Set" qualid OPT [ "as" ident ] ":=" ltac2_expr
 | "Ltac2" "Notation" [ string | lident ] ":=" ltac2_expr      (* Ltac2 plugin *)
 | "Ltac2" "Eval" ltac2_expr      (* ltac2 plugin *)

plugins/ltac/g_ltac.mlg

@@ -467,7 +467,9 @@ VERNAC COMMAND EXTEND VernacTacticNotation
   { VtSideff ([], VtNow) } ->
   {
     let n = Option.default 0 n in
-    Tacentries.add_tactic_notation (Locality.make_module_locality locality) n ?deprecation r e;
+    let local = Locality.make_module_locality locality in
+    let tacobj = Tacentries.add_tactic_notation_syntax local n ?deprecation r in
+    Tacentries.add_tactic_notation ?deprecation tacobj e
   }
 END
 

plugins/ltac/tacentries.ml

@@ -251,7 +251,6 @@ type tactic_grammar_obj = {
   tacobj_key : KerName.t;
   tacobj_local : locality_flag;
   tacobj_tacgram : tactic_grammar;
-  tacobj_body : Tacenv.alias_tactic;
   tacobj_forml : bool;
 }
 
@@ -265,71 +264,103 @@ let check_key key =
     user_err Pp.(str "Conflicting tactic notations keys. This can happen when including \
     twice the same module.")
 
-let cache_tactic_notation tobj =
+let cache_tactic_notation (tobj, body) =
   let key = tobj.tacobj_key in
   let () = check_key key in
-  Tacenv.register_alias key tobj.tacobj_body;
-  extend_tactic_grammar key tobj.tacobj_forml tobj.tacobj_tacgram;
-  Pptactic.declare_notation_tactic_pprule key (pprule tobj.tacobj_tacgram)
+  Tacenv.register_alias key body
 
-let open_tactic_notation i tobj =
-  let key = tobj.tacobj_key in
-  if Int.equal i 1 && not tobj.tacobj_local then
-    extend_tactic_grammar key tobj.tacobj_forml tobj.tacobj_tacgram
+let open_tactic_notation i _ = ()
 
-let load_tactic_notation i tobj =
+let load_tactic_notation i (tobj, body) =
   let key = tobj.tacobj_key in
   let () = check_key key in
   (* Only add the printing and interpretation rules. *)
-  Tacenv.register_alias key tobj.tacobj_body;
-  Pptactic.declare_notation_tactic_pprule key (pprule tobj.tacobj_tacgram);
-  if Int.equal i 1 && not tobj.tacobj_local then
-    extend_tactic_grammar key tobj.tacobj_forml tobj.tacobj_tacgram
+  Tacenv.register_alias key body
 
-let subst_tactic_notation (subst, tobj) =
+let subst_tactic_notation (subst, (tobj, body)) =
   let open Tacenv in
-  let alias = tobj.tacobj_body in
   { tobj with
-    tacobj_key = Mod_subst.subst_kn subst tobj.tacobj_key;
-    tacobj_body = { alias with alias_body = Tacsubst.subst_tactic subst alias.alias_body };
-  }
+    tacobj_key = Mod_subst.subst_kn subst tobj.tacobj_key
+  },
+  { body with alias_body = Tacsubst.subst_tactic subst body.alias_body }
 
 let classify_tactic_notation tacobj = Substitute
 
 let ltac_notation_cat = Libobject.create_category "ltac.notations"
 
-let inTacticGrammar : tactic_grammar_obj -> obj =
+let inTacticGrammar : tactic_grammar_obj * Tacenv.alias_tactic -> obj =
   declare_object {(default_object "TacticGrammar") with
        open_function = simple_open ~cat:ltac_notation_cat open_tactic_notation;
        load_function = load_tactic_notation;
        cache_function = cache_tactic_notation;
        subst_function = subst_tactic_notation;
        classify_function = classify_tactic_notation}
 
+let cache_tactic_syntax tobj =
+  let key = tobj.tacobj_key in
+  extend_tactic_grammar key tobj.tacobj_forml tobj.tacobj_tacgram;
+  Pptactic.declare_notation_tactic_pprule key (pprule tobj.tacobj_tacgram)
+
+let open_tactic_syntax i tobj =
+  let key = tobj.tacobj_key in
+  if Int.equal i 1 && not tobj.tacobj_local then
+    extend_tactic_grammar key tobj.tacobj_forml tobj.tacobj_tacgram
+
+let load_tactic_syntax i tobj =
+  let key = tobj.tacobj_key in
+  (* Only add the printing and interpretation rules. *)
+  Pptactic.declare_notation_tactic_pprule key (pprule tobj.tacobj_tacgram);
+  if Int.equal i 1 && not tobj.tacobj_local then
+    extend_tactic_grammar key tobj.tacobj_forml tobj.tacobj_tacgram
+
+let subst_tactic_syntax (subst, tobj) =
+  { tobj with
+    tacobj_key = Mod_subst.subst_kn subst tobj.tacobj_key
+  }
+
+let classify_tactic_syntax tacobj = Substitute
+
+let inTacticSyntax : tactic_grammar_obj -> obj =
+  declare_object {(default_object "TacticSyntax") with
+       object_stage = Summary.Stage.Synterp;
+       open_function = simple_open ~cat:ltac_notation_cat open_tactic_syntax;
+       load_function = load_tactic_syntax;
+       cache_function = cache_tactic_syntax;
+       subst_function = subst_tactic_syntax;
+       classify_function = classify_tactic_syntax}
+
 let cons_production_parameter = function
 | TacTerm _ -> None
 | TacNonTerm (_, (_, ido)) -> ido
 
-let add_glob_tactic_notation local ~level ?deprecation prods forml ids tac =
+let add_glob_tactic_notation ?deprecation tacobj ids tac =
+  let open Tacenv in
+  let body =
+    { alias_args = ids; alias_body = tac; alias_deprecation = deprecation } in
+  Lib.add_leaf (inTacticGrammar (tacobj, body))
+
+let add_glob_tactic_notation_syntax local ~level ?deprecation prods forml =
   let parule = {
     tacgram_level = level;
     tacgram_prods = prods;
   } in
-  let open Tacenv in
   let tacobj = {
     tacobj_key = make_fresh_key prods;
     tacobj_local = local;
     tacobj_tacgram = parule;
-    tacobj_body = { alias_args = ids; alias_body = tac; alias_deprecation = deprecation };
     tacobj_forml = forml;
   } in
-  Lib.add_leaf (inTacticGrammar tacobj)
+  Lib.add_leaf (inTacticSyntax tacobj);
+  tacobj
 
-let add_tactic_notation local n ?deprecation prods e =
-  let ids = List.map_filter cons_production_parameter prods in
-  let prods = List.map interp_prod_item prods in
+let add_tactic_notation ?deprecation tacobj e =
+  let ids = List.map_filter cons_production_parameter tacobj.tacobj_tacgram.tacgram_prods in
   let tac = Tacintern.glob_tactic_env ids (Global.env()) e in
-  add_glob_tactic_notation local ~level:n ?deprecation prods false ids tac
+  add_glob_tactic_notation ?deprecation tacobj ids tac
+
+let add_tactic_notation_syntax local n ?deprecation prods =
+  let prods = List.map interp_prod_item prods in
+  add_glob_tactic_notation_syntax local ~level:n ?deprecation prods false
 
 (**********************************************************************)
 (* ML Tactic entries                                                  *)
@@ -381,7 +412,8 @@ let add_ml_tactic_notation name ~level ?deprecation prods =
     let entry = { mltac_name = name; mltac_index = len - i - 1 } in
     let map id = Reference (Locus.ArgVar (CAst.make id)) in
     let tac = CAst.make (TacML (entry, List.map map ids)) in
-    add_glob_tactic_notation false ~level ?deprecation prods true ids tac
+    let tacobj = add_glob_tactic_notation_syntax false ~level ?deprecation prods true in
+    add_glob_tactic_notation ?deprecation tacobj ids tac
   in
   List.iteri iter (List.rev prods);
   (* We call [extend_atomic_tactic] only for "basic tactics" (the ones

plugins/ltac/tacentries.mli

@@ -25,6 +25,8 @@ type 'a grammar_tactic_prod_item_expr = 'a Pptactic.grammar_tactic_prod_item_exp
 | TacTerm of string
 | TacNonTerm of ('a * Names.Id.t option) Loc.located
 
+type tactic_grammar_obj
+
 type raw_argument = string * string option
 (** An argument type as provided in Tactic notations, i.e. a string like
     "ne_foo_list_opt" together with a separator that only makes sense in the
@@ -35,12 +37,17 @@ type argument = Genarg.ArgT.any Extend.user_symbol
     leaves. *)
 
 val add_tactic_notation :
-  locality_flag -> int -> ?deprecation:Deprecation.t -> raw_argument
-  grammar_tactic_prod_item_expr list -> raw_tactic_expr -> unit
+  ?deprecation:Deprecation.t -> tactic_grammar_obj ->
+  raw_tactic_expr -> unit
 (** [add_tactic_notation local level prods expr] adds a tactic notation in the
     environment at level [level] with locality [local] made of the grammar
     productions [prods] and returning the body [expr] *)
 
+val add_tactic_notation_syntax :
+  locality_flag -> int -> ?deprecation:Deprecation.t -> raw_argument
+  grammar_tactic_prod_item_expr list ->
+  tactic_grammar_obj
+
 val register_tactic_notation_entry : string -> ('a, 'b, 'c) Genarg.genarg_type -> unit
 (** Register an argument under a given entry name for tactic notations. When
     translating [raw_argument] into [argument], atomic names will be first

plugins/ltac2/g_ltac2.mlg

@@ -437,9 +437,9 @@ GRAMMAR EXTEND Gram
     ] ]
   ;
   tac2def_syn:
-    [ [ "Notation"; toks = LIST1 ltac2_scope; n = syn_level; ":=";
+    [ [ toks = LIST1 ltac2_scope; n = syn_level; ":=";
         e = ltac2_expr ->
-        { StrSyn (toks, n, e) }
+        { (toks, n, e) }
     ] ]
   ;
   lident:
@@ -960,27 +960,29 @@ PRINTED BY { pr_ltac2entry }
 | [ tac2def_val(v) ] -> { v }
 | [ tac2def_typ(t) ] -> { t }
 | [ tac2def_ext(e) ] -> { e }
-| [ tac2def_syn(e) ] -> { e }
 | [ tac2def_mut(e) ] -> { e }
 END
 
+VERNAC ARGUMENT EXTEND ltac2def_syn
+PRINTED BY { pr_ltac2entry }
+| [ tac2def_syn(e) ] -> { e }
+END
+
 VERNAC ARGUMENT EXTEND ltac2_expr
 PRINTED BY { pr_ltac2expr }
 | [ _ltac2_expr(e) ] -> { e }
 END
 
-{
-
-let classify_ltac2 = function
-| StrSyn _ -> Vernacextend.(VtSideff ([], VtNow))
-| StrMut _ | StrVal _ | StrPrm _  | StrTyp _ -> Vernacextend.classify_as_sideeff
-
-}
-
 VERNAC COMMAND EXTEND VernacDeclareTactic2Definition
-| #[ raw_attributes ] [ "Ltac2" ltac2_entry(e) ] => { classify_ltac2 e } -> {
+| #[ raw_attributes ] [ "Ltac2" ltac2_entry(e) ] => { Vernacextend.classify_as_sideeff } -> {
   Tac2entries.register_struct raw_attributes e
   }
+| #[ raw_attributes ] [ "Ltac2" "Notation" ltac2def_syn(e) ] => { Vernacextend.(VtSideff ([], VtNow)) } ->
+  {
+    let (toks, n, body) = e in
+    let synterpv = Tac2entries.register_notation raw_attributes toks n body in
+    Tac2entries.register_notation_interpretation synterpv
+  }
 | ![proof_opt_query] [ "Ltac2" "Eval" ltac2_expr(e) ] => { Vernacextend.classify_as_query } -> {
   fun ~pstate -> Tac2entries.perform_eval ~pstate e
   }