Removing the dependency of every level of tactic ATSs on glob_tactic_expr.

Instead of putting the body directly in the AST, we register it in a table.

This time it should work properly. Tactic notation are given kernel names to
ensure the unicity of their contents.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17079 85f007b7-540e-0410-9357-904b9bb8a0f7

13 files changed, 132 insertions, 67 deletions

diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index 12de0bcbe..e56f7a34e 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -125,9 +125,8 @@ let make_one_printing_rule se (pt,_,e) =
   let level = mlexpr_of_int 0 in (* only level 0 supported here *)
   let loc = MLast.loc_of_expr e in
   let prods = mlexpr_of_list mlexpr_terminals_of_grammar_tactic_prod_item_expr pt in
-  <:expr< { Pptactic.pptac_key = $se$;
-            pptac_args = $make_tags loc pt$;
-            pptac_prods = ($level$, $prods$) } >>
+  <:expr< ($se$, { Pptactic.pptac_args = $make_tags loc pt$;
+            pptac_prods = ($level$, $prods$) }) >>
 
 let make_printing_rule se = mlexpr_of_list (make_one_printing_rule se)
 
@@ -203,7 +202,7 @@ let declare_tactic loc s c cl =
 	     (Pp.str ("Exception in tactic extend " ^ $se$ ^": "))
 	     (Errors.print e)) ];
       Egramml.extend_tactic_grammar $se$ $gl$;
-      List.iter Pptactic.declare_extra_tactic_pprule $pp$; } >>
+      List.iter (fun (s, r) -> Pptactic.declare_ml_tactic_pprule s r) $pp$; } >>
     ]
 
 open Pcaml
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 0ddf58b74..87af636b4 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -178,8 +178,7 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
   | TacExtend of Loc.t * string * 'lev generic_argument list
 
   (* For syntax extensions *)
-  | TacAlias of Loc.t * string *
-      (Id.t * 'lev generic_argument) list * (DirPath.t * glob_tactic_expr)
+  | TacAlias of Loc.t * KerName.t * (Id.t * 'lev generic_argument) list
 
 (** Possible arguments of a tactic definition *)
 
@@ -250,14 +249,14 @@ and ('t,'p,'c,'i,'r,'n,'l) gen_tactic_fun_ast =
 
 (** Globalized tactics *)
 
-and g_trm = glob_constr_and_expr
-and g_pat = glob_constr_and_expr * constr_pattern
-and g_cst = evaluable_global_reference and_short_name or_var
-and g_ind = inductive or_var
-and g_ref = ltac_constant located or_var
-and g_nam  = Id.t located
+type g_trm = glob_constr_and_expr
+type g_pat = glob_constr_and_expr * constr_pattern
+type g_cst = evaluable_global_reference and_short_name or_var
+type g_ind = inductive or_var
+type g_ref = ltac_constant located or_var
+type g_nam  = Id.t located
 
-and glob_tactic_expr =
+type glob_tactic_expr =
     (g_trm, g_pat, g_cst, g_ind, g_ref, g_nam, glevel) gen_tactic_expr
 
 type glob_atomic_tactic_expr =
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 34e0dcdef..a6ac42cf1 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -246,15 +246,13 @@ let get_tactic_entry n =
 (** State of the grammar extensions                                   *)
 
 type tactic_grammar = {
-  tacgram_key : string;
   tacgram_level : int;
   tacgram_prods : grammar_prod_item list;
-  tacgram_tactic : DirPath.t * Tacexpr.glob_tactic_expr;
 }
 
 type all_grammar_command =
   | Notation of Notation.level * notation_grammar
-  | TacticGrammar of tactic_grammar
+  | TacticGrammar of KerName.t * tactic_grammar
 
 (* Declaration of the tactic grammar rule *)
 
@@ -262,19 +260,19 @@ let head_is_ident tg = match tg.tacgram_prods with
 | GramTerminal _::_ -> true
 | _ -> false
 
-let add_tactic_entry tg =
+let add_tactic_entry kn tg =
   let entry, pos = get_tactic_entry tg.tacgram_level in
   let rules =
     if Int.equal tg.tacgram_level 0 then begin
       if not (head_is_ident tg) then
         error "Notation for simple tactic must start with an identifier.";
       let mkact loc l =
-        (TacAlias (loc,tg.tacgram_key,l,tg.tacgram_tactic):raw_atomic_tactic_expr) in
+        (TacAlias (loc,kn,l):raw_atomic_tactic_expr) in
       make_rule mkact tg.tacgram_prods
     end
     else
       let mkact loc l =
-        (TacAtom(loc,TacAlias(loc,tg.tacgram_key,l,tg.tacgram_tactic)):raw_tactic_expr) in
+        (TacAtom(loc,TacAlias(loc,kn,l)):raw_tactic_expr) in
       make_rule mkact tg.tacgram_prods in
   synchronize_level_positions ();
   grammar_extend entry None (Option.map of_coq_position pos,[(None, None, List.rev [rules])]);
@@ -285,14 +283,14 @@ 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 g -> add_tactic_entry g in
+  | TacticGrammar (kn, g) -> add_tactic_entry kn g in
   grammar_state := (nb,gram) :: !grammar_state
 
 let extend_constr_grammar pr ntn =
   extend_grammar (Notation (pr, ntn))
 
-let extend_tactic_grammar ntn =
-  extend_grammar (TacticGrammar ntn)
+let extend_tactic_grammar kn ntn =
+  extend_grammar (TacticGrammar (kn, ntn))
 
 let recover_constr_grammar ntn prec =
   let filter = function
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli
index 9ae49f718..19e8ee8f6 100644
--- a/parsing/egramcoq.mli
+++ b/parsing/egramcoq.mli
@@ -41,10 +41,8 @@ type notation_grammar = {
 }
 
 type tactic_grammar = {
-  tacgram_key : string;
   tacgram_level : int;
   tacgram_prods : grammar_prod_item list;
-  tacgram_tactic : DirPath.t * Tacexpr.glob_tactic_expr;
 }
 
 (** {5 Adding notations} *)
@@ -52,7 +50,7 @@ type tactic_grammar = {
 val extend_constr_grammar : Notation.level -> notation_grammar -> unit
 (** Add a term notation rule to the parsing system. *)
 
-val extend_tactic_grammar : tactic_grammar -> unit
+val extend_tactic_grammar : KerName.t -> tactic_grammar -> unit
 (** Add a tactic notation rule to the parsing system. *)
 
 val recover_constr_grammar : notation -> Notation.level -> notation_grammar
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 2ce3eba06..f52e10979 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -30,18 +30,21 @@ let pr_global x = Nametab.pr_global_env Id.Set.empty x
 type grammar_terminals = string option list
 
 type pp_tactic = {
-  pptac_key : string;
   pptac_args : argument_type list;
   pptac_prods : int * grammar_terminals;
 }
 
-  (* Extensions *)
+(* ML Extensions *)
 let prtac_tab = Hashtbl.create 17
 
-let declare_extra_tactic_pprule pt =
-  Hashtbl.add prtac_tab (pt.pptac_key, pt.pptac_args) (pt.pptac_prods)
+(* Tactic notations *)
+let prnotation_tab = Hashtbl.create 17
 
-let exists_extra_tactic_pprule s tags = Hashtbl.mem prtac_tab (s,tags)
+let declare_ml_tactic_pprule key pt =
+  Hashtbl.add prtac_tab (key, pt.pptac_args) pt.pptac_prods
+
+let declare_notation_tactic_pprule kn pt =
+  Hashtbl.add prnotation_tab (kn, pt.pptac_args) pt.pptac_prods
 
 type 'a raw_extra_genarg_printer =
     (constr_expr -> std_ppcmds) ->
@@ -268,6 +271,15 @@ let pr_extend_gen pr_gen lev s l =
   with Not_found ->
     str s ++ spc() ++ pr_sequence pr_gen l ++ str" (* Generic printer *)"
 
+let pr_alias_gen pr_gen lev s l =
+  try
+    let tags = List.map genarg_tag l in
+    let (lev',pl) = Hashtbl.find prnotation_tab (s,tags) in
+    let p = pr_tacarg_using_rule pr_gen (pl,l) in
+    if lev' > lev then surround p else p
+  with Not_found ->
+    KerName.print s ++ spc() ++ pr_sequence pr_gen l ++ str" (* Generic printer *)"
+
 let pr_raw_extend prc prlc prtac prpat =
   pr_extend_gen (pr_raw_generic prc prlc prtac prpat pr_reference)
 let pr_glob_extend prc prlc prtac prpat =
@@ -275,6 +287,13 @@ let pr_glob_extend prc prlc prtac prpat =
 let pr_extend prc prlc prtac prpat =
   pr_extend_gen (pr_top_generic prc prlc prtac prpat)
 
+let pr_raw_alias prc prlc prtac prpat =
+  pr_alias_gen (pr_raw_generic prc prlc prtac prpat pr_reference)
+let pr_glob_alias prc prlc prtac prpat =
+  pr_alias_gen (pr_glb_generic prc prlc prtac prpat)
+let pr_alias prc prlc prtac prpat =
+  pr_extend_gen (pr_top_generic prc prlc prtac prpat)
+
 (**********************************************************************)
 (* The tactic printer                                                 *)
 
@@ -543,13 +562,14 @@ let level_of (n,p) = match p with E -> n | L -> n-1 | Prec n -> n | Any -> lseq
 
 let make_pr_tac pr_tac_level
   (pr_constr,pr_lconstr,pr_pat,pr_lpat,
-   pr_cst,pr_ind,pr_ref,pr_ident,pr_extend,strip_prod_binders, pr_gen) =
+   pr_cst,pr_ind,pr_ref,pr_ident,pr_extend,pr_alias,strip_prod_binders, pr_gen) =
 
 (* some shortcuts *)
 let pr_bindings = pr_bindings pr_lconstr pr_constr in
 let pr_ex_bindings = pr_bindings_gen true pr_lconstr pr_constr in
 let pr_with_bindings = pr_with_bindings pr_lconstr pr_constr in
 let pr_extend = pr_extend pr_constr pr_lconstr pr_tac_level pr_pat in
+let pr_alias = pr_alias pr_constr pr_lconstr pr_tac_level pr_pat in
 let pr_red_expr = pr_red_expr (pr_constr,pr_lconstr,pr_cst,pr_pat) in
 
 let pr_constrarg c = spc () ++ pr_constr c in
@@ -623,8 +643,8 @@ let rec pr_atom0 = function
 and pr_atom1 = function
   | TacExtend (loc,s,l) ->
       pr_with_comments loc (pr_extend 1 s l)
-  | TacAlias (loc,s,l,_) ->
-      pr_with_comments loc (pr_extend 1 s (List.map snd l))
+  | TacAlias (loc,kn,l) ->
+      pr_with_comments loc (pr_alias 1 kn (List.map snd l))
 
   (* Basic tactics *)
   | TacIntroPattern [] as t -> pr_atom0 t
@@ -912,9 +932,9 @@ let rec pr_tac inherited tac =
       pr_tac (lcomplete,E) t, lcomplete
   | TacId l ->
       str "idtac" ++ prlist (pr_arg (pr_message_token pr_ident)) l, latom
-  | TacAtom (loc,TacAlias (_,s,l,_)) ->
+  | TacAtom (loc,TacAlias (_,kn,l)) ->
       pr_with_comments loc
-        (pr_extend (level_of inherited) s (List.map snd l)),
+        (pr_alias (level_of inherited) kn (List.map snd l)),
       latom
   | TacAtom (loc,t) ->
       pr_with_comments loc (hov 1 (pr_atom1 t)), ltatom
@@ -971,6 +991,7 @@ let raw_printers =
      pr_reference,
      pr_or_metaid pr_lident,
      pr_raw_extend,
+     pr_raw_alias,
      strip_prod_binders_expr,
      Genprint.generic_raw_print)
 
@@ -994,6 +1015,7 @@ let pr_glob_tactic_level env =
      pr_ltac_or_var (pr_located pr_ltac_constant),
      pr_lident,
      pr_glob_extend,
+     pr_glob_alias,
      strip_prod_binders_glob_constr,
      Genprint.generic_glb_print)
   in
diff --git a/printing/pptactic.mli b/printing/pptactic.mli
index 59a3fc830..47640afa6 100644
--- a/printing/pptactic.mli
+++ b/printing/pptactic.mli
@@ -8,6 +8,7 @@
 
 open Pp
 open Genarg
+open Names
 open Constrexpr
 open Tacexpr
 open Proof_type
@@ -48,15 +49,12 @@ val declare_extra_genarg_pprule :
 type grammar_terminals = string option list
 
 type pp_tactic = {
-  pptac_key : string;
   pptac_args : argument_type list;
   pptac_prods : int * grammar_terminals;
 }
 
-  (** if the boolean is false then the extension applies only to old syntax *)
-val declare_extra_tactic_pprule : pp_tactic -> unit
-
-val exists_extra_tactic_pprule : string -> argument_type list -> bool
+val declare_ml_tactic_pprule : string -> pp_tactic -> unit
+val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit
 
 val pr_raw_generic :
   (constr_expr -> std_ppcmds) ->
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
new file mode 100644
index 000000000..1a277c740
--- /dev/null
+++ b/tactics/tacenv.ml
@@ -0,0 +1,24 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Util
+open Pp
+open Names
+open Tacexpr
+
+type alias = KerName.t
+
+let alias_map = Summary.ref ~name:"tactic-alias"
+  (KNmap.empty : (DirPath.t * glob_tactic_expr) KNmap.t)
+
+let register_alias key dp tac =
+  alias_map := KNmap.add key (dp, tac) !alias_map
+
+let interp_alias key =
+  try KNmap.find key !alias_map
+  with Not_found -> Errors.anomaly (str "Unknown tactic alias: " ++ KerName.print key)
diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli
new file mode 100644
index 000000000..8fada3920
--- /dev/null
+++ b/tactics/tacenv.mli
@@ -0,0 +1,21 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+open Tacexpr
+
+(** This module centralizes the various ways of registering tactics. *)
+
+type alias = KerName.t
+(** Type of tactic alias, used in the [TacAlias] node. *)
+
+val register_alias : alias -> DirPath.t -> glob_tactic_expr -> unit
+(** Register a tactic alias. *)
+
+val interp_alias : alias -> (DirPath.t * glob_tactic_expr)
+(** Recover the the body of an alias. *)
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 42ea649ec..edbec7a04 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -634,9 +634,9 @@ let rec intern_atomic lf ist x =
   | TacExtend (loc,opn,l) ->
       !assert_tactic_installed opn;
       TacExtend (adjust_loc loc,opn,List.map (intern_genarg ist) l)
-  | TacAlias (loc,s,l,(dir,body)) ->
+  | TacAlias (loc,s,l) ->
       let l = List.map (fun (id,a) -> (id,intern_genarg ist a)) l in
-      TacAlias (loc,s,l,(dir,body))
+      TacAlias (loc,s,l)
 
 and intern_tactic onlytac ist tac = snd (intern_tactic_seq onlytac ist tac)
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 248a5d36b..e6afbbaf7 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2231,7 +2231,8 @@ and interp_atomic ist tac =
       Proofview.V82.tclEVARS sigma <*>
       tac args ist
       end
-  | TacAlias (loc,s,l,(_,body)) ->
+  | TacAlias (loc,s,l) ->
+      let (_, body) = Tacenv.interp_alias s in
       Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
       let rec f x =
@@ -2332,7 +2333,7 @@ and interp_atomic ist tac =
         Proofview.Goal.return (Id.Map.add x v accu)
       in
       List.fold_right addvar l (Proofview.Goal.return ist.lfun) >>= fun lfun ->
-      let trace = push_trace (loc,LtacNotationCall s) ist in
+      let trace = push_trace (loc,LtacNotationCall (KerName.to_string s)) ist in
       let ist = {
         lfun = lfun;
         extra = TacStore.set ist.extra f_trace trace; } in
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 7c968865a..7491c9a8f 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -219,9 +219,9 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   (* For extensions *)
   | TacExtend (_loc,opn,l) ->
       TacExtend (dloc,opn,List.map (subst_genarg subst) l)
-  | TacAlias (_,s,l,(dir,body)) ->
-      TacAlias (dloc,s,List.map (fun (id,a) -> (id,subst_genarg subst a)) l,
-        (dir,subst_tactic subst body))
+  | TacAlias (_,s,l) ->
+      let s = subst_kn subst s in
+      TacAlias (dloc,s,List.map (fun (id,a) -> (id,subst_genarg subst a)) l)
 
 and subst_tactic subst (t:glob_tactic_expr) = match t with
   | TacAtom (_loc,t) -> TacAtom (dloc, subst_atomic subst t)
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index 7b91665ad..f1227c234 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -15,6 +15,7 @@ Equality
 Contradiction
 Inv
 Leminv
+Tacenv
 Tacsubst
 Taccoerce
 Tacintern
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 4bce9b73e..b2493a2a1 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -65,26 +65,37 @@ type tactic_grammar_obj = {
   tacobj_local : locality_flag;
   tacobj_tacgram : tactic_grammar;
   tacobj_tacpp : Pptactic.pp_tactic;
+  tacobj_body : DirPath.t * Tacexpr.glob_tactic_expr
 }
 
-let cache_tactic_notation (_, tobj) =
-  Egramcoq.extend_tactic_grammar tobj.tacobj_tacgram;
-  Pptactic.declare_extra_tactic_pprule tobj.tacobj_tacpp
+let cache_tactic_notation ((_, key), tobj) =
+  let (dp, body) = tobj.tacobj_body in
+  Tacenv.register_alias key dp body;
+  Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram;
+  Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp
 
-let subst_tactic_parule subst tg =
-  let dir, tac = tg.tacgram_tactic in
-  { tg with tacgram_tactic = (dir, Tacsubst.subst_tactic subst tac); }
+let open_tactic_notation i ((_, key), tobj) =
+  if Int.equal i 1 && not tobj.tacobj_local then
+    Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram
+
+let load_tactic_notation i ((_, key), tobj) =
+  let (dp, body) = tobj.tacobj_body in
+  (** Only add the printing and interpretation rules. *)
+  Tacenv.register_alias key dp 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
 
 let subst_tactic_notation (subst, tobj) =
-  { tobj with
-    tacobj_tacgram = subst_tactic_parule subst tobj.tacobj_tacgram; }
+  let dir, tac = tobj.tacobj_body in
+  { tobj with tacobj_body = (dir, Tacsubst.subst_tactic subst tac); }
 
-let classify_tactic_notation tacobj =
-  if tacobj.tacobj_local then Dispose else Substitute tacobj
+let classify_tactic_notation tacobj = Substitute tacobj
 
 let inTacticGrammar : tactic_grammar_obj -> obj =
   declare_object {(default_object "TacticGrammar") with
-       open_function = (fun i o -> if Int.equal i 1 then cache_tactic_notation o);
+       open_function = open_tactic_notation;
+       load_function = load_tactic_notation;
        cache_function = cache_tactic_notation;
        subst_function = subst_tactic_notation;
        classify_function = classify_tactic_notation}
@@ -98,31 +109,24 @@ let rec tactic_notation_key = function
   | _ :: l -> tactic_notation_key l
   | [] -> "terminal_free_notation"
 
-let rec next_key_away key t =
-  if Pptactic.exists_extra_tactic_pprule key t then next_key_away (key^"'") t
-  else key
-
 let add_tactic_notation (local,n,prods,e) =
   let prods = List.map (interp_prod_item n) prods in
   let tags = make_tags prods in
-  let key = next_key_away (tactic_notation_key prods) tags in
   let pprule = {
-    Pptactic.pptac_key = key;
-    pptac_args = tags;
+    Pptactic.pptac_args = tags;
     pptac_prods = (n, List.map make_terminal_status prods);
   } in
   let ids = List.fold_left cons_production_parameter [] prods in
   let tac = Tacintern.glob_tactic_env ids (Global.env()) e in
   let parule = {
-    tacgram_key = key;
     tacgram_level = n;
     tacgram_prods = prods;
-    tacgram_tactic = (Lib.cwd (), tac);
   } in
   let tacobj = {
     tacobj_local = local;
     tacobj_tacgram = parule;
     tacobj_tacpp = pprule;
+    tacobj_body = (Lib.cwd (), tac);
   } in
   Lib.add_anonymous_leaf (inTacticGrammar tacobj)