Put parts of ltac2_plugin which depend on ltac1 in a separate plugin

This requires a new `ltac2_ltac1_common_plugin` for things used by both
(profile_ltac, goal selectors and the "use_default" `...` syntax).
We could also put that stuff in vernac/.

For now we still load the split off parts in Ltac2.Init.

It could also make sense to load it in Ltac2.Ltac1 (and require that
in Ltac2.Notations as a few notations use `ltac1:()`).

doc/Makefile.docgram

@@ -30,7 +30,8 @@ DOC_MLGS := \
 	plugins/ring/g_ring.mlg \
 	plugins/rtauto/g_rtauto.mlg \
 	plugins/syntax/g_number_string.mlg \
-	plugins/ltac2/g_ltac2.mlg
+	plugins/ltac2/g_ltac2.mlg plugins/ltac2_ltac1/g_ltac2_ltac1.mlg \
+	plugins/ltac2_ltac1_common/g_ltac2_ltac1_common.mlg
 DOC_EDIT_MLGS := $(wildcard doc/tools/docgram/*.edit_mlg)
 DOC_RSTS := $(wildcard doc/sphinx/*/*.rst) $(wildcard doc/sphinx/*/*/*.rst)
 

lib/core_plugins_findlib_compat.ml

@@ -21,6 +21,8 @@ let legacy_to_findlib = [
   ("extraction_plugin",             ["plugins";"extraction"]) ;
   ("funind_plugin",                 ["plugins";"funind"]) ;
   ("ltac2_plugin",                  ["plugins";"ltac2"]) ;
+  ("ltac2_ltac1_plugin",            ["plugins";"ltac2_ltac1"]) ;
+  ("ltac2_ltac1_common_plugin",     ["plugins";"ltac2_ltac1_common"]) ;
   ("nsatz_plugin",                  ["plugins";"nsatz"]) ;
   ("rtauto_plugin",                 ["plugins";"rtauto"]) ;
   ("ssrmatching_plugin",            ["plugins";"ssrmatching"]) ;

plugins/ltac/dune

@@ -3,7 +3,7 @@
  (public_name coq-core.plugins.ltac)
  (synopsis "Coq's LTAC tactic language")
  (modules :standard \ tauto)
- (libraries coq-core.vernac))
+ (libraries ltac2_ltac1_common_plugin))
 
 (library
  (name tauto_plugin)

plugins/ltac/g_ltac.mlg

@@ -27,6 +27,8 @@ open Pcoq.Constr
 open Pvernac.Vernac_
 open Pltac
 
+open Ltac2_ltac1_common_plugin.G_ltac2_ltac1_common
+
 let fail_default_value = Locus.ArgArg 0
 
 let arg_of_expr = function
@@ -48,19 +50,11 @@ let reference_to_id qid =
 
 let tactic_mode = Entry.make "tactic_command"
 
-let toplevel_selector = Entry.make "toplevel_selector"
 let tacdef_body = Entry.make "tacdef_body"
 
 (* Registers [tactic_mode] as a parser for proof editing *)
 let classic_proof_mode = Pvernac.register_proof_mode "Classic" tactic_mode
 
-(* Hack to parse "[ id" without dropping [ *)
-let test_bracket_ident =
-  let open Pcoq.Lookahead in
-  to_entry "test_bracket_ident" begin
-    lk_kw "[" >> lk_ident
-  end
-
 (* Tactics grammar rules *)
 
 let hint = G_proofs.hint
@@ -71,7 +65,7 @@ let for_extraargs = ()
 
 GRAMMAR EXTEND Gram
   GLOBAL: tactic tacdef_body ltac_expr binder_tactic tactic_value command hint
-          tactic_mode constr_may_eval constr_eval toplevel_selector
+          tactic_mode constr_may_eval constr_eval
           term;
 
   tactic_then_last:
@@ -119,7 +113,7 @@ GRAMMAR EXTEND Gram
       | IDENT "abstract"; tc = NEXT -> { CAst.make ~loc (TacAbstract (tc,None)) }
       | IDENT "abstract"; tc = NEXT; "using";  s = ident ->
         { CAst.make ~loc (TacAbstract (tc,Some s)) }
-      | IDENT "only"; sel = selector; ":"; ta = ltac_expr -> { CAst.make ~loc (TacSelect (sel, ta)) } ]
+      | IDENT "only"; sel = goal_selector; ":"; ta = ltac_expr -> { CAst.make ~loc (TacSelect (sel, ta)) } ]
 (*End of To do*)
     | "2" RIGHTA
       [ ta0 = ltac_expr; "+"; ta1 = ltac_expr -> { CAst.make ~loc (TacOr (ta0,ta1)) }
@@ -293,30 +287,6 @@ GRAMMAR EXTEND Gram
     [ [ tac = ltac_expr -> { tac } ] ]
   ;
 
-  range_selector:
-    [ [ n = natural ; "-" ; m = natural -> { (n, m) }
-      | n = natural -> { (n, n) } ] ]
-  ;
-  (* We unfold a range selectors list once so that we can make a special case
-   * for a unique SelectNth selector. *)
-  range_selector_or_nth:
-    [ [ n = natural ; "-" ; m = natural;
-        l = OPT [","; l = LIST1 range_selector SEP "," -> { l } ] ->
-        { Goal_select.SelectList ((n, m) :: Option.default [] l) }
-      | n = natural;
-        l = OPT [","; l = LIST1 range_selector SEP "," -> { l } ] ->
-        { let open Goal_select in
-          Option.cata (fun l -> SelectList ((n, n) :: l)) (SelectNth n) l } ] ]
-  ;
-  selector:
-  [ [ l = range_selector_or_nth -> { l }
-    | test_bracket_ident; "["; id = ident; "]" -> { Goal_select.SelectId id } ] ]
-  ;
-  toplevel_selector:
-    [ [ sel = selector; ":" -> { sel }
-    |   "!"; ":" -> { Goal_select.SelectAlreadyFocused }
-    |   IDENT "all"; ":" -> { Goal_select.SelectAll } ] ]
-  ;
   tactic_mode:
     [ [ g = OPT toplevel_selector; tac = G_vernac.query_command -> { Vernacexpr.VernacSynPure (tac g) }
       | g = OPT toplevel_selector; "{" -> { Vernacexpr.VernacSynPure (Vernacexpr.VernacSubproof g) } ] ]
@@ -348,16 +318,6 @@ open Tacarg
 open Vernacextend
 open Libnames
 
-let pr_ltac_selector s = Pptactic.pr_goal_selector ~toplevel:true s
-
-}
-
-VERNAC ARGUMENT EXTEND ltac_selector PRINTED BY { pr_ltac_selector }
-| [ toplevel_selector(s) ] -> { s }
-END
-
-{
-
 let pr_ltac_info n = str "Info" ++ spc () ++ int n
 
 }
@@ -368,18 +328,6 @@ END
 
 {
 
-let pr_ltac_use_default b =
-  if b then (* Bug: a space is inserted before "..." *) str ".." else mt ()
-
-}
-
-VERNAC ARGUMENT EXTEND ltac_use_default PRINTED BY { pr_ltac_use_default }
-| [ "." ] -> { false }
-| [ "..." ] -> { true }
-END
-
-{
-
 let rm_abstract tac =
   let (loc, tac2) = CAst.(tac.loc, tac.v) in
   match tac2 with

plugins/ltac/g_ltac.mli

@@ -25,28 +25,16 @@ val in_tac :
 
 val tactic_mode : Vernacexpr.vernac_expr Pcoq.Entry.t
 
-val toplevel_selector : Goal_select.t Pcoq.Entry.t
-
 val tacdef_body : Tacexpr.tacdef_body Pcoq.Entry.t
 
 val classic_proof_mode : Pvernac.proof_mode
 
-val test_bracket_ident : unit Pcoq.Entry.t
-
 val hint : Vernacexpr.hints_expr Pcoq.Entry.t
 
-val wit_ltac_selector : (Goal_select.t, unit, unit) Genarg.genarg_type
-
-val ltac_selector : Goal_select.t Pcoq.Entry.t
-
 val wit_ltac_info : (int, unit, unit) Genarg.genarg_type
 
 val ltac_info : int Pcoq.Entry.t
 
-val wit_ltac_use_default : (bool, unit, unit) Genarg.genarg_type
-
-val ltac_use_default : bool Pcoq.Entry.t
-
 val wit_ltac_tactic_level : (int, unit, unit) Genarg.genarg_type
 
 val ltac_tactic_level : int Pcoq.Entry.t

plugins/ltac/pptactic.ml

@@ -1179,6 +1179,20 @@ let pr_goal_selector ~toplevel s =
 
   let pr_atomic_tactic env sigma c = pr_atomic_tactic_level env sigma c
 
+let pp_ltac_call_kind = function
+  | LtacNotationCall s -> pr_alias_key s
+  | LtacNameCall cst -> pr_ltac_constant cst
+  (* todo: don't want the KerName instead? *)
+  | LtacVarCall (_, id, t) -> Names.Id.print id
+  | LtacAtomCall te ->
+    pr_glob_tactic (Global.env ())
+      (CAst.make (TacAtom te))
+  | LtacConstrInterp (env, sigma, c, _) ->
+    pr_glob_constr_env env sigma c
+  | LtacMLCall te ->
+    (pr_glob_tactic (Global.env ())
+       te)
+
 let declare_extra_genarg_pprule wit
   (f : 'a raw_extra_genarg_printer)
   (g : 'b glob_extra_genarg_printer)

plugins/ltac/pptactic.mli

@@ -156,6 +156,7 @@ val pr_match_rule : bool -> ('a -> Pp.t) -> ('b -> Pp.t) ->
 
 val pr_value : entry_relative_level -> Val.t -> Pp.t
 
+val pp_ltac_call_kind : ltac_call_kind -> Pp.t
 
 val ltop : entry_relative_level
 

plugins/ltac/profile_ltac_tactics.mlg

@@ -12,7 +12,7 @@
 
 (** Ltac profiling entrypoints *)
 
-open Profile_ltac
+open Ltac2_ltac1_common_plugin.Profile_ltac
 open Stdarg
 
 }

plugins/ltac/tacinterp.ml

@@ -42,6 +42,12 @@ open Proofview.Notations
 open Context.Named.Declaration
 open Ltac_pretype
 
+let do_profile trace ?count_call tac =
+  Ltac2_ltac1_common_plugin.Profile_ltac.do_profile_gen (function
+      | (_, c) :: _ -> Some (Pptactic.pp_ltac_call_kind c)
+      | [] -> None)
+    trace ?count_call tac
+
 let ltac_trace_info = Tactic_debug.ltac_trace_info
 
 let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v wit ->
@@ -1109,7 +1115,7 @@ and eval_tactic_ist ist tac : unit Proofview.tactic =
   | TacAtom t ->
       let call = LtacAtomCall t in
       let (stack, _) = push_trace(loc,call) ist in
-      Profile_ltac.do_profile stack
+      do_profile stack
         (catch_error_tac_loc loc stack (interp_atomic ist t))
   | TacFun _ | TacLetIn _ | TacMatchGoal _ | TacMatch _ -> interp_tactic ist tac
   | TacId [] -> Proofview.tclLIFT (db_breakpoint (curr_debug ist) [])
@@ -1142,7 +1148,7 @@ and eval_tactic_ist ist tac : unit Proofview.tactic =
   | TacAbstract (t,ido) ->
       let call = LtacMLCall tac in
       let (stack,_) = push_trace(None,call) ist in
-      Profile_ltac.do_profile stack
+      do_profile stack
         (catch_error_tac stack begin
       Proofview.Goal.enter begin fun gl -> Abstract.tclABSTRACT
         (Option.map (interp_ident ist (pf_env gl) (project gl)) ido) (interp_tactic ist t)
@@ -1264,7 +1270,7 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t =
          already in another global reference *)
       let ist = ensure_loc loc ist in
       let (stack, _) = trace in
-      Profile_ltac.do_profile stack ~count_call:false
+      do_profile stack ~count_call:false
         (catch_error_tac_loc (* loc for interpretation *) loc stack
            (val_interp ~appl ist (Tacenv.interp_ltac r)))
 
@@ -1339,7 +1345,7 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
                 ; extra = TacStore.set ist.extra f_trace trace
                 } in
               let (stack, _) = trace in
-              Profile_ltac.do_profile stack ~count_call:false
+              do_profile stack ~count_call:false
                 (catch_error_tac_loc loc stack (val_interp (ensure_loc loc ist) body)) >>= fun v ->
               Ftactic.return (name_vfun (push_appl appl largs) v)
             end
@@ -1392,7 +1398,7 @@ and tactic_of_value ist vle =
         extra = TacStore.set ist.extra f_trace (if !Flags.profile_ltac then ([],[]) else trace); } in
       let tac = name_if_glob appl (eval_tactic_ist ist t) in
       let (stack, _) = trace in
-      Profile_ltac.do_profile stack (catch_error_tac_loc loc stack tac)
+      do_profile stack (catch_error_tac_loc loc stack tac)
   | VFun (appl,(stack,_),loc,vmap,vars,_) ->
      let tactic_nm =
        match appl with

plugins/ltac2/dune

@@ -3,6 +3,6 @@
  (public_name coq-core.plugins.ltac2)
  (synopsis "Ltac2 plugin")
  (modules_without_implementation tac2expr tac2qexpr tac2types)
- (libraries coq-core.plugins.ltac))
+ (libraries ltac2_ltac1_common_plugin))
 
 (coq.pp (modules g_ltac2))