API: ltac1-tactic as an argument

Changelog.md

@@ -1,5 +1,15 @@
 # Changelog
 
+## UNRELEASED
+
+### APIs
+
+- New `ltac1-tactic` opaque data type
+- New `tac` argument constructor
+- Change `coq.ltac.call-ltac1` now accepts either a string (tactic name) or
+  a tactic expression (of type `ltac1-tactic`)
+- New `ltac_tactic:(...)` syntax to pass tactic expressions to Elpi tactics
+
 ## [1.19.1] - 30/08/2023
 
 Requires Elpi 1.16.5 and Coq 8.18.

README.md

@@ -261,13 +261,14 @@ Tactics also accept Ltac variables as follows:
 - `ltac_int:(v)` (for `v` of type `int` or `integer`)
 - `ltac_term:(v)` (for `v` of type `constr` or `open_constr` or `uconstr` or `hyp`)
 - `ltac_(string|int|term)_list:(v)` (for `v` of type `list` of ...)
+- `ltac_tactic:(t)` (for `t` of type `tactic_expr`)
 - `ltac_attributes:(v)` (for `v` of type `attributes`)
 For example:
 ```coq
-Tactic Notation "tac" string(X) ident(Y) int(Z) hyp(T) constr_list(L) :=
-  elpi tac ltac_string:(X) ltac_string:(Y) ltac_int:(Z) ltac_term:(T) ltac_term_list:(L).
+Tactic Notation "tac" string(X) ident(Y) int(Z) hyp(T) constr_list(L) simple_intropattern_list(P) :=
+  elpi tac ltac_string:(X) ltac_string:(Y) ltac_int:(Z) ltac_term:(T) ltac_term_list:(L) ltac_tactic:(intros P).
 ```
-lets one write `tac "a" b 3 H t1 t2 t3` in any Ltac context.
+lets one write `tac "a" b 3 H t1 t2 t3 [|m]` in any Ltac context.
 Arguments are first interpreted by Ltac according to the types declared
 in the tactic notation and then injected in the corresponding Elpi argument.
 For example `H` must be an existing hypothesis, since it is typed with

coq-builtin.elpi

@@ -52,6 +52,9 @@ type int       int    -> argument. % Eg. 1 -2.
 type str       string -> argument. % Eg. x "y" z.w. or any Coq keyword/symbol
 type trm       term   -> argument. % Eg. (t).
 
+% Extra arguments for tactics
+type tac       ltac1-tactic -> argument.
+
 % Extra arguments for commands. [Definition], [Axiom], [Record] and [Context]
 % take precedence over the [str] argument above (when not "quoted").
 %
@@ -1521,6 +1524,10 @@ external pred coq.strategy.get i:constant, o:conversion_strategy.
 
 % -- Coq's tactics --------------------------------------------
 
+% LTac1 tactic expression
+typeabbrev ltac1-tactic (ctype "ltac1-tactic").
+
+
 % [coq.ltac.fail Level ...] Interrupts the Elpi program and calls Ltac's
 % fail Level Msg, where Msg is the printing of the remaining arguments.
 % Level can be left unspecified and defaults to 0
@@ -1538,9 +1545,13 @@ external type coq.ltac.fail int -> variadic any prop.
 external pred coq.ltac.collect-goals i:term, o:list sealed-goal, 
                                      o:list sealed-goal.
 
-% [coq.ltac.call-ltac1 Tac G GL] Calls Ltac1 tactic named Tac on goal G
-% (passing the arguments of G, see coq.ltac.call for a handy wrapper)
-external pred coq.ltac.call-ltac1 i:string, i:goal, o:list sealed-goal.
+% [coq.ltac.call-ltac1 Tac G GL] Calls Ltac1 tactic Tac on goal G (passing
+% the arguments of G, see coq.ltac.call for a handy wrapper).
+% Tac can either be a string (the tactic name), or a value
+% of type ltac1-tactic, see the tac argument constructor
+% and the ltac_tactic:(...) syntax to pass arguments to
+% an elpi tactic.
+external pred coq.ltac.call-ltac1 i:any, i:goal, o:list sealed-goal.
 
 % [coq.ltac.id-free? ID G] 
 %     Fails if ID is already used in G. Note that ids which are taken are

elpi/coq-HOAS.elpi

@@ -37,6 +37,9 @@ type int       int    -> argument. % Eg. 1 -2.
 type str       string -> argument. % Eg. x "y" z.w. or any Coq keyword/symbol
 type trm       term   -> argument. % Eg. (t).
 
+% Extra arguments for tactics
+type tac       ltac1-tactic -> argument.
+
 % Extra arguments for commands. [Definition], [Axiom], [Record] and [Context]
 % take precedence over the [str] argument above (when not "quoted").
 %

src/coq_elpi_arg_HOAS.ml

@@ -407,27 +407,37 @@ type raw_ltac_term = Constrexpr.constr_expr
 type glob_ltac_term = Glob_term.glob_constr
 type top_ltac_term = Geninterp.interp_sign * Names.Id.t
 
+type raw_ltac_tactic = Ltac_plugin.Tacexpr.raw_tactic_expr
+type glob_ltac_tactic = Ltac_plugin.Tacexpr.glob_tactic_expr
+type top_ltac_tactic = Geninterp.Val.t
+
 type ltac_ty = Int | String | Term | List of ltac_ty
 
-type ('a,'f) t =
-  | Int : int            -> ('a,'f) t
-  | String : string      -> ('a,'f) t
-  | Term : 'a            -> ('a,'f) t
-  | LTac : ltac_ty * 'f  -> ('a,'f) t
+type ('a,'f,'t) t =
+  | Int : int            -> ('a,'f,'t) t
+  | String : string      -> ('a,'f,'t) t
+  | Term : 'a            -> ('a,'f,'t) t
+  | LTac : ltac_ty * 'f  -> ('a,'f,'t) t
+  | LTacTactic : 't  -> ('a,'f,'t) t
 
-type raw = (raw_term, raw_ltac_term) t
-type glob = (glob_term, glob_ltac_term) t
-type top = (top_term, top_ltac_term) t
+type raw =  (raw_term,  raw_ltac_term,  raw_ltac_tactic) t
+type glob = (glob_term, glob_ltac_term, glob_ltac_tactic) t
+type top =  (top_term,  top_ltac_term,  top_ltac_tactic) t
 
 let pr_raw_ltac_arg _ _ _ = Pp.str "TODO: pr_raw_ltac_arg"
 let pr_glob_ltac_arg _ _ _ = Pp.str "TODO: pr_glob_ltac_arg"
 let pr_top_ltac_arg _ _ _ = Pp.str "TODO: pr_top_ltac_arg"
 
-let pr_arg f k x = match x with
+let pr_raw_ltac_tactic _ _ _ = Pp.str "TODO: pr_raw_ltac_tactic"
+let pr_glob_ltac_tactic _ _ _ = Pp.str "TODO: pr_glob_ltac_tactic"
+let pr_top_ltac_tactic _ _ _ = Pp.str "TODO: pr_top_ltac_tactic"
+
+let pr_arg f k t x = match x with
   | Int n -> Pp.int n
   | String s -> Pp.qstring s
   | Term s -> f s
   | LTac(_, s) -> k s
+  | LTacTactic s -> t s
 
 let pr_glob_constr_and_expr env sigma = function
   | (_, Some c) ->
@@ -441,22 +451,26 @@ let pp_raw env sigma : raw -> Pp.t =
   pr_arg
     (Ppconstr.pr_constr_expr env sigma)
     (pr_raw_ltac_arg env sigma)
+    (pr_raw_ltac_tactic env sigma)
 
 let pp_glob env sigma =
   pr_arg
     (pr_glob_constr_and_expr env sigma)
     (pr_glob_ltac_arg env sigma)
+    (pr_glob_ltac_tactic env sigma)
 
 let pp_top env sigma : top -> Pp.t =
   pr_arg
     ((fun (_,x) -> pr_glob_constr_and_expr env sigma x))
     (pr_top_ltac_arg env sigma)
+    (pr_top_ltac_tactic env sigma)
 
 let glob glob_sign : raw -> _ * glob = function
   | Int _ as x -> glob_sign, x
   | String _ as x -> glob_sign, x
   | Term t -> glob_sign, Term (intern_tactic_constr glob_sign t)
   | LTac(ty,t) -> glob_sign, LTac (ty,fst @@ intern_tactic_constr glob_sign t)
+  | LTacTactic t -> glob_sign, LTacTactic (Ltac_plugin.Tacintern.glob_tactic t)
 
 let subst mod_subst = function
   | Int _ as x -> x
@@ -465,7 +479,9 @@ let subst mod_subst = function
       Term (Ltac_plugin.Tacsubst.subst_glob_constr_and_expr mod_subst t)
   | LTac(ty,t) ->
       LTac(ty,(Detyping.subst_glob_constr (Global.env()) mod_subst t))        
-
+  | LTacTactic t ->
+      LTacTactic (Ltac_plugin.Tacsubst.subst_tactic mod_subst t)
+
 let interp return ist = function
   | Int _ as x -> return x
   | String _ as x -> return x
@@ -476,6 +492,7 @@ let interp return ist = function
         | Glob_term.GVar id -> id
         | _ -> assert false in
         return @@ LTac(ty,(ist,id))
+  | LTacTactic t -> return @@ LTacTactic (Ltac_plugin.Tacinterp.Value.of_closure ist t)
 
 
 let add_genarg tag pr_raw pr_glob pr_top glob subst interp =
@@ -636,6 +653,7 @@ let rec do_context_constr coq_ctx csts fields ~depth state =
 
 let strc = E.Constants.declare_global_symbol "str"
 let trmc = E.Constants.declare_global_symbol "trm"
+let tacc = E.Constants.declare_global_symbol "tac"
 let intc = E.Constants.declare_global_symbol "int"
 let ctxc = E.Constants.declare_global_symbol "ctx-decl"
 
@@ -735,9 +753,23 @@ let rec in_elpi_ltac_arg ~depth ?calldepth coq_ctx hyps sigma state ty ist v =
       with Taccoerce.CannotCoerceTo _ ->
         raise (Taccoerce.CannotCoerceTo "a term")
 
+let { CD.cin = of_ltac_tactic; isc = is_ltac_tactic; cout = to_ltac_tactic }, tac = CD.declare {
+  CD.name = "ltac1-tactic";
+  doc = "LTac1 tactic expression";
+  pp = (fun fmt _ -> Format.fprintf fmt "«ltac1-tactic»");
+  compare = (fun a b -> 0);
+  hash = (fun x -> Hashtbl.hash x);
+  hconsed = false;
+  constants = [];
+}
+
+let in_elpi_ltac_tactic ~depth ?calldepth coq_ctx hyps sigma state t =
+  state, [E.mkApp tacc (of_ltac_tactic t) []], []
+
 let in_elpi_tac ~depth ?calldepth coq_ctx hyps sigma state x =
   let open Tac in
   match x with
+  | LTacTactic t -> in_elpi_ltac_tactic ~depth ?calldepth coq_ctx hyps sigma state t
   | LTac(ty,(ist,id)) ->
       let v = try Id.Map.find id ist.Geninterp.lfun with Not_found -> assert false in
       begin try
@@ -828,7 +860,7 @@ let in_elpi_cmd ~depth ?calldepth coq_ctx state ~raw (x : Cmd.top) =
       let sigma = get_sigma state in
       in_elpi_elab_term_arg ~depth ?calldepth state coq_ctx hyps sigma ist glob_or_expr
 
-type coq_arg = Cint of int | Cstr of string | Ctrm of EConstr.t
+type coq_arg = Cint of int | Cstr of string | Ctrm of EConstr.t | CLtac1 of Geninterp.Val.t
 
 let in_coq_arg ~depth proof_context constraints state t =
   match E.look ~depth t with
@@ -845,5 +877,13 @@ let in_coq_arg ~depth proof_context constraints state t =
   | E.App(c,t,[]) when c == trmc ->
       let state, t, gls = lp2constr ~depth proof_context constraints state t in
       state, Ctrm t, gls
+  | E.App(c,t,[]) when c == trmc ->
+    let state, t, gls = lp2constr ~depth proof_context constraints state t in
+    state, Ctrm t, gls
+  | E.App(c,t,[]) when c == tacc ->
+    begin match E.look ~depth t with
+    | E.CData c when is_ltac_tactic c -> state, CLtac1 (to_ltac_tactic c), []
+    | _ -> raise API.Conversion.(TypeErr (TyName"argument",depth,t))
+    end
   | _ -> raise API.Conversion.(TypeErr (TyName"argument",depth,t))
 

src/coq_elpi_arg_HOAS.mli

@@ -68,23 +68,32 @@ type raw_ltac_term = Constrexpr.constr_expr
 type glob_ltac_term = Glob_term.glob_constr
 type top_ltac_term = Geninterp.interp_sign * Names.Id.t
 
+type raw_ltac_tactic = Ltac_plugin.Tacexpr.raw_tactic_expr
+type glob_ltac_tactic = Ltac_plugin.Tacexpr.glob_tactic_expr
+type top_ltac_tactic = Geninterp.Val.t
+
 type ltac_ty = Int | String | Term | List of ltac_ty
 
-type ('a,'f) t =
-  | Int : int            -> ('a,'f) t
-  | String : string      -> ('a,'f) t
-  | Term : 'a            -> ('a,'f) t
-  | LTac : ltac_ty * 'f  -> ('a,'f) t
+type ('a,'f,'t) t =
+  | Int : int            -> ('a,'f,'t) t
+  | String : string      -> ('a,'f,'t) t
+  | Term : 'a            -> ('a,'f,'t) t
+  | LTac : ltac_ty * 'f  -> ('a,'f,'t) t
+  | LTacTactic : 't  -> ('a,'f,'t) t
 
-type raw = (raw_term, raw_ltac_term) t
-type glob = (glob_term, glob_ltac_term) t
-type top = (top_term, top_ltac_term) t
+type raw =  (raw_term,  raw_ltac_term,  raw_ltac_tactic) t
+type glob = (glob_term, glob_ltac_term, glob_ltac_tactic) t
+type top =  (top_term,  top_ltac_term,  top_ltac_tactic) t
 
 val subst : Mod_subst.substitution -> glob -> glob
 val wit : (raw, glob, top) Genarg.genarg_type
 
 end
 
+val tac : Tac.top_ltac_tactic Elpi.API.Conversion.t
+val is_ltac_tactic : Elpi.API.RawOpaqueData.t -> bool
+val to_ltac_tactic : Elpi.API.RawOpaqueData.t -> Tac.top_ltac_tactic
+
 (* for tactics *)
 val in_elpi_tac :
   depth:int -> ?calldepth:int -> 
@@ -114,7 +123,7 @@ val in_elpi_cmd :
   Cmd.top ->
   Elpi.API.State.t * term * Elpi.API.Conversion.extra_goals
 
-type coq_arg = Cint of int | Cstr of string | Ctrm of EConstr.t
+type coq_arg = Cint of int | Cstr of string | Ctrm of EConstr.t | CLtac1 of Geninterp.Val.t
 
 val in_coq_arg :
   depth:int ->

src/coq_elpi_arg_syntax.mlg

@@ -12,6 +12,8 @@ open Gramlib
 open Pcoq.Constr
 open Pcoq.Prim
 open Pvernac.Vernac_
+open Tacarg
+open Pltac
 
 module EA = Coq_elpi_arg_HOAS
 module U = Coq_elpi_utils
@@ -169,6 +171,9 @@ let of_coq_definition ~loc ~atts name udecl def =
   | Vernacexpr.ProveBody _ ->
       CErrors.user_err ~loc Pp.(str"syntax error: missing Definition body")
 
+let pr_tac env sigma _prc _prlc prtac c =
+  prtac env sigma (Constrexpr.LevelLe 0) c
+
 }
 
 GRAMMAR EXTEND Gram
@@ -258,6 +263,11 @@ GLOB_PRINTED BY { fun _ _ _ -> EA.Cmd.pp_glob env sigma }
 | [ coq_kwd_or_symbol(x) ] -> { EA.Cmd.String x }
 END
 
+ARGUMENT EXTEND elpi_ltac_tactic
+  TYPED AS tactic
+  PRINTED BY { pr_tac env sigma }
+| [ ltac_expr(c) ] -> { c }
+END
 
 ARGUMENT EXTEND elpi_tactic_arg
 TYPED AS elpi_ftactic_arg
@@ -271,6 +281,7 @@ TYPED AS elpi_ftactic_arg
 | [ "ltac_int_list" ":" "(" ident(t) ")" ] -> { EA.Tac.LTac(EA.Tac.List EA.Tac.Int, (CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None))) }
 | [ "ltac_term" ":" "(" ident(t) ")" ] -> { EA.Tac.LTac(EA.Tac.Term, CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None)) }
 | [ "ltac_term_list" ":" "(" ident(t) ")" ] -> { EA.Tac.LTac(EA.Tac.List EA.Tac.Term,(CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None))) }
+| [ "ltac_tactic" ":" "(" elpi_ltac_tactic(t) ")" ] -> { EA.Tac.LTacTactic t }
 END
 
 ARGUMENT EXTEND ltac_attributes

src/coq_elpi_builtins.ml

@@ -3163,7 +3163,8 @@ is equivalent to Elpi Export TacName.|})))),
       let tac_fixed_args = more_args |> List.map (function
         | Coq_elpi_arg_HOAS.Cint n -> Coq_elpi_arg_HOAS.Tac.Int n
         | Coq_elpi_arg_HOAS.Cstr s -> Coq_elpi_arg_HOAS.Tac.String s
-        | Coq_elpi_arg_HOAS.Ctrm t -> Coq_elpi_arg_HOAS.Tac.Term (Coq_elpi_utils.detype env sigma t,None)) in
+        | Coq_elpi_arg_HOAS.Ctrm t -> Coq_elpi_arg_HOAS.Tac.Term (Coq_elpi_utils.detype env sigma t,None)
+        | Coq_elpi_arg_HOAS.CLtac1 _ -> nYI "tactic notation with LTac1 argument") in
       let abbrev_name = Coq_elpi_utils.string_split_on_char '.' name in
       let tac_name = Coq_elpi_utils.string_split_on_char '.' tacname in
       Lib.add_leaf @@ inAbbreviationForTactic { abbrev_name; tac_name; tac_fixed_args};
@@ -3555,6 +3556,8 @@ coq.reduction.lazy.whd_all X Y :-
 
   LPDoc "-- Coq's tactics --------------------------------------------";
 
+  MLData Coq_elpi_arg_HOAS.tac;
+
   MLCode(Pred("coq.ltac.fail",
     In(B.unspec B.int,"Level",
     VariadicIn(unit_ctx, !> B.any, "Interrupts the Elpi program and calls Ltac's fail Level Msg, where Msg is the printing of the remaining arguments. Level can be left unspecified and defaults to 0")),
@@ -3617,29 +3620,42 @@ fold_left over the terms, letin body comes before the type).
     DocAbove);
 
   MLCode(Pred("coq.ltac.call-ltac1",
-    In(B.string, "Tac",
+    In(B.any, "Tac",
     CIn(goal, "G",
     Out(list sealed_goal,"GL",
-    Full(raw_ctx, "Calls Ltac1 tactic named Tac on goal G (passing the arguments of G, see coq.ltac.call for a handy wrapper)")))),
-    (fun tac_name (proof_context,goal,tac_args) _ ~depth _ _ -> abstract__grab_global_env_keep_sigma "coq.ltac.call-ltac1" (fun state ->
+    Full(raw_ctx, {|Calls Ltac1 tactic Tac on goal G (passing the arguments of G, see coq.ltac.call for a handy wrapper).
+Tac can either be a string (the tactic name), or a value
+of type ltac1-tactic, see the tac argument constructor
+and the ltac_tactic:(...) syntax to pass arguments to
+an elpi tactic.|})))),
+    (fun tac (proof_context,goal,tac_args) _ ~depth _ _ -> abstract__grab_global_env_keep_sigma "coq.ltac.call-ltac1" (fun state ->
       let open Ltac_plugin in
       let sigma = get_sigma state in
        let tac_args = tac_args |> List.map (function
          | Coq_elpi_arg_HOAS.Ctrm t -> Tacinterp.Value.of_constr t
          | Coq_elpi_arg_HOAS.Cstr s -> Geninterp.(Val.inject (val_tag (Genarg.topwit Stdarg.wit_string))) s
-         | Coq_elpi_arg_HOAS.Cint i -> Tacinterp.Value.of_int i) in
+         | Coq_elpi_arg_HOAS.Cint i -> Tacinterp.Value.of_int i
+         | Coq_elpi_arg_HOAS.CLtac1 x -> x) in
        let tactic =
-         let tac_name =
-           let q = Libnames.qualid_of_string tac_name in
-           try Tacenv.locate_tactic q
-           with Not_found ->
-             match Tacenv.locate_extended_all_tactic q with
-             | [x] -> x
-             | _::_::_ -> err Pp.(str"Ltac1 tactic " ++ str tac_name ++ str" is ambiguous, qualify the name")
-             | [] -> err Pp.(str"Ltac1 tactic " ++ str tac_name ++ str" not found") in
-         let tacref = Locus.ArgArg (Loc.tag @@ tac_name) in
-         let tacexpr = Tacexpr.(CAst.make @@ TacArg (TacCall (CAst.make @@ (tacref, [])))) in
-         let tac = Tacinterp.Value.of_closure (Tacinterp.default_ist ()) tacexpr in
+         let tac =
+          match E.look ~depth tac with
+          | E.CData s when API.RawOpaqueData.is_string s ->
+              let tac_name = API.RawOpaqueData.to_string s in
+              let tac_name =
+                let q = Libnames.qualid_of_string tac_name in
+                try Tacenv.locate_tactic q
+                with Not_found ->
+                  match Tacenv.locate_extended_all_tactic q with
+                  | [x] -> x
+                  | _::_::_ -> err Pp.(str"Ltac1 tactic " ++ str tac_name ++ str" is ambiguous, qualify the name")
+                  | [] -> err Pp.(str"Ltac1 tactic " ++ str tac_name ++ str" not found") in
+              let tacref = Locus.ArgArg (Loc.tag @@ tac_name) in
+              let tacexpr = Tacexpr.(CAst.make @@ TacArg (TacCall (CAst.make @@ (tacref, [])))) in
+              Tacinterp.Value.of_closure (Tacinterp.default_ist ()) tacexpr
+          | E.CData t when Coq_elpi_arg_HOAS.is_ltac_tactic t ->
+              Coq_elpi_arg_HOAS.to_ltac_tactic t
+          | _ -> U.type_error ("coq.ltac.call-ltac1: string or ltac1-tactic are expected as the tactic to call")
+         in
          Tacinterp.Value.apply tac tac_args in
        let subgoals, sigma =
          let open Proofview in let open Notations in