Moving the Ltac definition command to an EXTEND based command.

3 files changed, 97 insertions, 0 deletions

diff --git a/tactics/g_ltac.ml4 b/tactics/g_ltac.ml4
index d75073877e..f46a670080 100644
--- a/tactics/g_ltac.ml4
+++ b/tactics/g_ltac.ml4
@@ -48,6 +48,7 @@ let new_entry name =
   e
 
 let selector = new_entry "vernac:selector"
+let tacdef_body = new_entry "tactic:tacdef_body"
 
 (* Registers the Classic Proof Mode (which uses [tactic_mode] as a parser for
     proof editing and changes nothing else). Then sets it as the default proof mode. *)
@@ -311,6 +312,7 @@ open Constrarg
 open Vernacexpr
 open Vernac_classifier
 open Goptions
+open Libnames
 
 let print_info_trace = ref None
 
@@ -409,3 +411,19 @@ VERNAC COMMAND EXTEND VernacPrintLtac CLASSIFIED AS QUERY
 | [ "Print" "Ltac" reference(r) ] ->
   [ msg_notice (Tacintern.print_ltac (snd (Libnames.qualid_of_reference r))) ]
 END
+
+VERNAC ARGUMENT EXTEND ltac_tacdef_body
+| [ tacdef_body(t) ] -> [ t ]
+END
+
+VERNAC COMMAND EXTEND VernacDeclareTacticDefinition
+| [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => [
+    VtSideff (List.map (function
+      | TacticDefinition ((_,r),_) -> r
+      | TacticRedefinition (Ident (_,r),_) -> r
+      | TacticRedefinition (Qualid (_,q),_) -> snd(repr_qualid q)) l), VtLater
+  ] -> [
+    let lc = Locality.LocalityFixme.consume () in
+    Tacentries.register_ltac (Locality.make_module_locality lc) l
+  ]
+END
diff --git a/tactics/tacentries.ml b/tactics/tacentries.ml
index e40f5f46a0..711cd8d9d0 100644
--- a/tactics/tacentries.ml
+++ b/tactics/tacentries.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Pp
 open Errors
 open Util
 open Names
@@ -14,6 +15,8 @@ open Pcoq
 open Egramml
 open Egramcoq
 open Vernacexpr
+open Libnames
+open Nameops
 
 (**********************************************************************)
 (* Tactic Notation                                                    *)
@@ -184,3 +187,77 @@ let add_ml_tactic_notation name prods =
   } in
   Lib.add_anonymous_leaf (inMLTacticGrammar obj);
   extend_atomic_tactic name prods
+
+(** Command *)
+
+
+type tacdef_kind =
+  | NewTac of Id.t
+  | UpdateTac of Nametab.ltac_constant
+
+let is_defined_tac kn =
+  try ignore (Tacenv.interp_ltac kn); true with Not_found -> false
+
+let register_ltac local tacl =
+  let map tactic_body =
+    match tactic_body with
+    | TacticDefinition ((loc,id), body) ->
+        let kn = Lib.make_kn id in
+        let id_pp = pr_id id in
+        let () = if is_defined_tac kn then
+          Errors.user_err_loc (loc, "",
+            str "There is already an Ltac named " ++ id_pp ++ str".")
+        in
+        let is_primitive =
+          try
+            match Pcoq.parse_string Pcoq.Tactic.tactic (Id.to_string id) with
+            | Tacexpr.TacArg _ -> false
+            | _ -> true (* most probably TacAtom, i.e. a primitive tactic ident *)
+          with e when Errors.noncritical e -> true (* prim tactics with args, e.g. "apply" *)
+        in
+        let () = if is_primitive then
+          msg_warning (str "The Ltac name " ++ id_pp ++
+            str " may be unusable because of a conflict with a notation.")
+        in
+        NewTac id, body
+    | TacticRedefinition (ident, body) ->
+        let loc = loc_of_reference ident in
+        let kn =
+          try Nametab.locate_tactic (snd (qualid_of_reference ident))
+          with Not_found ->
+            Errors.user_err_loc (loc, "",
+                        str "There is no Ltac named " ++ pr_reference ident ++ str ".")
+        in
+        UpdateTac kn, body
+  in
+  let rfun = List.map map tacl in
+  let recvars =
+    let fold accu (op, _) = match op with
+    | UpdateTac _ -> accu
+    | NewTac id -> (Lib.make_path id, Lib.make_kn id) :: accu
+    in
+    List.fold_left fold [] rfun
+  in
+  let ist = Tacintern.make_empty_glob_sign () in
+  let map (name, body) =
+    let body = Flags.with_option Tacintern.strict_check (Tacintern.intern_tactic_or_tacarg ist) body in
+    (name, body)
+  in
+  let defs () =
+    (** Register locally the tactic to handle recursivity. This function affects
+        the whole environment, so that we transactify it afterwards. *)
+    let iter_rec (sp, kn) = Nametab.push_tactic (Nametab.Until 1) sp kn in
+    let () = List.iter iter_rec recvars in
+    List.map map rfun
+  in
+  let defs = Future.transactify defs () in
+  let iter (def, tac) = match def with
+  | NewTac id ->
+    Tacenv.register_ltac false local id tac;
+    Flags.if_verbose msg_info (Nameops.pr_id id ++ str " is defined")
+  | UpdateTac kn ->
+    Tacenv.redefine_ltac local kn tac;
+    let name = Nametab.shortest_qualid_of_tactic kn in
+    Flags.if_verbose msg_info (Libnames.pr_qualid name ++ str " is redefined")
+  in
+  List.iter iter defs
diff --git a/tactics/tacentries.mli b/tactics/tacentries.mli
index 635415b9d2..3cf0bc5cc9 100644
--- a/tactics/tacentries.mli
+++ b/tactics/tacentries.mli
@@ -17,3 +17,5 @@ val add_tactic_notation :
 
 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