Ltac2: allow 0 argument externals

This will let us have non-thunk Array.empty and a couple others.

doc/changelog/06-Ltac2-language/17475-ltac2-defineval.rst

@@ -0,0 +1,4 @@
+- **Added:**
+  It is possible to define 0-argument externals
+  (`#17475 <https://github.com/coq/coq/pull/17475>`_,
+  by Gaëtan Gilbert).

plugins/ltac2/tac2entries.ml

@@ -470,18 +470,20 @@ let register_primitive ?deprecation ?(local = false) {loc;v=id} t ml =
   | _ -> 0
   in
   let arrows = count_arrow (snd t) in
-  let () = if Int.equal arrows 0 then
-    user_err ?loc (str "External tactic must have at least one argument") in
   let () =
     try let _ = Tac2env.interp_primitive ml in () with Not_found ->
       user_err ?loc (str "Unregistered primitive " ++
         quote (str ml.mltac_plugin) ++ spc () ++ quote (str ml.mltac_tactic))
   in
-  let init i = Id.of_string (Printf.sprintf "x%i" i) in
-  let names = List.init arrows init in
-  let bnd = List.map (fun id -> Name id) names in
-  let arg = List.map (fun id -> GTacVar id) names in
-  let e = GTacFun (bnd, GTacPrm (ml, arg)) in
+  let e =
+    if arrows > 0 then
+      let init i = Id.of_string (Printf.sprintf "x%i" i) in
+      let names = List.init arrows init in
+      let bnd = List.map (fun id -> Name id) names in
+      let arg = List.map (fun id -> GTacVar id) names in
+      GTacFun (bnd, GTacPrm (ml, arg))
+    else GTacPrm (ml, [])
+  in
   let def = {
     tacdef_local = local;
     tacdef_mutable = false;

plugins/ltac2/tac2env.mli

@@ -117,8 +117,8 @@ val shortest_qualid_of_projection : ltac_projection -> qualid
 (** This state is not part of the summary, contrarily to the ones above. It is
     intended to be used from ML plugins to register ML-side functions. *)
 
-val define_primitive : ml_tactic_name -> closure -> unit
-val interp_primitive : ml_tactic_name -> closure
+val define_primitive : ml_tactic_name -> valexpr -> unit
+val interp_primitive : ml_tactic_name -> valexpr
 
 (** {5 ML primitive types} *)
 

plugins/ltac2/tac2interp.ml

@@ -193,11 +193,15 @@ let rec interp (ist : environment) = function
   return (Tac2ffi.of_open (kn, Array.of_list el))
 | GTacPrm (ml, el) ->
   Proofview.Monad.List.map (fun e -> interp ist e) el >>= fun el ->
-  with_frame (FrPrim ml) (Tac2ffi.apply (Tac2env.interp_primitive ml) el)
+  with_frame (FrPrim ml) (interp_prim_app (Tac2env.interp_primitive ml) el)
 | GTacExt (tag, e) ->
   let tpe = Tac2env.interp_ml_object tag in
   with_frame (FrExtn (tag, e)) (tpe.Tac2env.ml_interp ist e)
 
+and interp_prim_app v = function
+  | [] -> return v
+  | _ :: _ as args -> (Tac2ffi.apply (to_closure v) args)
+
 and interp_closure f =
   let ans = fun args ->
     let { clos_env = ist; clos_var = ids; clos_exp = e; clos_ref = kn } = f in
@@ -277,6 +281,8 @@ and eval_pure bnd kn = function
   let bnd = List.fold_left fold bnd vals in
   eval_pure bnd kn body
 
+| GTacPrm (ml, []) -> Tac2env.interp_primitive ml
+
 | GTacAtm (AtmStr _) | GTacSet _
 | GTacApp _ | GTacCse _ | GTacPrj _
 | GTacPrm _ | GTacExt _ | GTacWth _

plugins/ltac2/tac2quote.ml

@@ -546,5 +546,5 @@ let of_format { v = fmt; loc } =
     with Tac2print.InvalidFormat ->
       CErrors.user_err ?loc (str "Invalid format")
   in
-  let stop = CAst.make @@ CTacApp (global_ref (kername format_prefix "stop"), [of_tuple []]) in
+  let stop = global_ref (kername format_prefix "stop") in
   List.fold_left of_format stop fmt

plugins/ltac2/tac2stdlib.ml

@@ -217,29 +217,31 @@ let pname s = { mltac_plugin = "coq-core.plugins.ltac2"; mltac_tactic = s }
 
 let lift tac = tac <*> return v_unit
 
+let prim_closure arity f = of_closure (mk_closure arity f)
+
 let define_prim0 name tac =
   let tac _ = lift tac in
-  Tac2env.define_primitive (pname name) (mk_closure arity_one tac)
+  Tac2env.define_primitive (pname name) (prim_closure arity_one tac)
 
 let define_prim1 name r0 f =
   let tac x = lift (f (Value.repr_to r0 x)) in
-  Tac2env.define_primitive (pname name) (mk_closure arity_one tac)
+  Tac2env.define_primitive (pname name) (prim_closure arity_one tac)
 
 let define_prim2 name r0 r1 f =
   let tac x y = lift (f (Value.repr_to r0 x) (Value.repr_to r1 y)) in
-  Tac2env.define_primitive (pname name) (mk_closure (arity_suc arity_one) tac)
+  Tac2env.define_primitive (pname name) (prim_closure (arity_suc arity_one) tac)
 
 let define_prim3 name r0 r1 r2 f =
   let tac x y z = lift (f (Value.repr_to r0 x) (Value.repr_to r1 y) (Value.repr_to r2 z)) in
-  Tac2env.define_primitive (pname name) (mk_closure (arity_suc (arity_suc arity_one)) tac)
+  Tac2env.define_primitive (pname name) (prim_closure (arity_suc (arity_suc arity_one)) tac)
 
 let define_prim4 name r0 r1 r2 r3 f =
   let tac x y z u = lift (f (Value.repr_to r0 x) (Value.repr_to r1 y) (Value.repr_to r2 z) (Value.repr_to r3 u)) in
-  Tac2env.define_primitive (pname name) (mk_closure (arity_suc (arity_suc (arity_suc arity_one))) tac)
+  Tac2env.define_primitive (pname name) (prim_closure (arity_suc (arity_suc (arity_suc arity_one))) tac)
 
 let define_prim5 name r0 r1 r2 r3 r4 f =
   let tac x y z u v = lift (f (Value.repr_to r0 x) (Value.repr_to r1 y) (Value.repr_to r2 z) (Value.repr_to r3 u) (Value.repr_to r4 v)) in
-  Tac2env.define_primitive (pname name) (mk_closure (arity_suc (arity_suc (arity_suc (arity_suc arity_one)))) tac)
+  Tac2env.define_primitive (pname name) (prim_closure (arity_suc (arity_suc (arity_suc (arity_suc arity_one)))) tac)
 
 (** Tactics from Tacexpr *)
 
@@ -351,15 +353,15 @@ let lift tac = tac >>= fun c -> Proofview.tclUNIT (Value.of_constr c)
 
 let define_red1 name r0 f =
   let tac x = lift (f (Value.repr_to r0 x)) in
-  Tac2env.define_primitive (pname name) (mk_closure arity_one tac)
+  Tac2env.define_primitive (pname name) (prim_closure arity_one tac)
 
 let define_red2 name r0 r1 f =
   let tac x y = lift (f (Value.repr_to r0 x) (Value.repr_to r1 y)) in
-  Tac2env.define_primitive (pname name) (mk_closure (arity_suc arity_one) tac)
+  Tac2env.define_primitive (pname name) (prim_closure (arity_suc arity_one) tac)
 
 let define_red3 name r0 r1 r2 f =
   let tac x y z = lift (f (Value.repr_to r0 x) (Value.repr_to r1 y) (Value.repr_to r2 z)) in
-  Tac2env.define_primitive (pname name) (mk_closure (arity_suc (arity_suc arity_one)) tac)
+  Tac2env.define_primitive (pname name) (prim_closure (arity_suc (arity_suc arity_one)) tac)
 
 let () = define_red1 "eval_red" constr begin fun c ->
   Tac2tactics.eval_red c