Avoid writing eta expansions for primitives

This takes the example in
coq#10107 (comment)
from 0.15s to 0.12s (-20%)

We need to modify the closure representation to provide backtraces and
profile stacks for primitives.

plugins/ltac2/tac2entries.ml

@@ -477,11 +477,7 @@ let register_primitive ?deprecation ?(local = false) {loc;v=id} t ml =
       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 = GTacPrm ml in
   let def = {
     tacdef_local = local;
     tacdef_mutable = false;

plugins/ltac2/tac2env.ml

@@ -114,7 +114,9 @@ module MLMap = Map.Make(ML)
 
 let primitive_map = ref MLMap.empty
 
-let define_primitive name f = primitive_map := MLMap.add name f !primitive_map
+let define_primitive name f =
+  let f = annotate_prim_closure name f in
+  primitive_map := MLMap.add name f !primitive_map
 let interp_primitive name = MLMap.find name !primitive_map
 
 (** Name management *)

plugins/ltac2/tac2expr.mli

@@ -178,7 +178,7 @@ type glb_tacexpr =
 | GTacWth of glb_tacexpr open_match
 | GTacFullMatch of glb_tacexpr * (glb_pat * glb_tacexpr) list
 | GTacExt : (_, 'a) Tac2dyn.Arg.tag * 'a -> glb_tacexpr
-| GTacPrm of ml_tactic_name * glb_tacexpr list
+| GTacPrm of ml_tactic_name
 
 (** {5 Parsing & Printing} *)
 

plugins/ltac2/tac2ffi.ml

@@ -37,14 +37,14 @@ type valexpr =
 | ValFloat of Float64.t
   (** Primitive floats *)
 
-and closure = MLTactic : (valexpr, 'v) arity0 * 'v -> closure
+and closure = MLTactic : (valexpr, 'v) arity0 * Tac2expr.ml_tactic_name option * 'v -> closure
 
 let arity_one = OneAty
 let arity_suc a = AddAty a
 
 type 'a arity = (valexpr, 'a) arity0
 
-let mk_closure arity f = MLTactic (arity, f)
+let mk_closure arity f = MLTactic (arity, None, f)
 
 module Valexpr =
 struct
@@ -407,23 +407,27 @@ type ('a, 'b) fun1 = closure
 let fun1 (r0 : 'a repr) (r1 : 'b repr) : ('a, 'b) fun1 repr = closure
 let to_fun1 r0 r1 f = to_closure f
 
-let rec apply : type a. a arity -> a -> valexpr list -> valexpr Proofview.tactic =
-  fun arity f args -> match args, arity with
-  | [], arity -> Proofview.tclUNIT (ValCls (MLTactic (arity, f)))
+let wrap prim tac = match prim with
+  | None -> tac
+  | Some prim -> Tac2bt.with_frame (FrPrim prim) tac
+
+let rec apply : type a. a arity -> _ -> a -> valexpr list -> valexpr Proofview.tactic =
+  fun arity prim f args -> match args, arity with
+  | [], arity -> Proofview.tclUNIT (ValCls (MLTactic (arity, prim, f)))
   (* A few hardcoded cases for efficiency *)
-  | [a0], OneAty -> f a0
-  | [a0; a1], AddAty OneAty -> f a0 a1
-  | [a0; a1; a2], AddAty (AddAty OneAty) -> f a0 a1 a2
-  | [a0; a1; a2; a3], AddAty (AddAty (AddAty OneAty)) -> f a0 a1 a2 a3
+  | [a0], OneAty -> wrap prim (f a0)
+  | [a0; a1], AddAty OneAty -> wrap prim (f a0 a1)
+  | [a0; a1; a2], AddAty (AddAty OneAty) -> wrap prim (f a0 a1 a2)
+  | [a0; a1; a2; a3], AddAty (AddAty (AddAty OneAty)) -> wrap prim (f a0 a1 a2 a3)
   (* Generic cases *)
   | a :: args, OneAty ->
-    f a >>= fun f ->
-    let MLTactic (arity, f) = to_closure f in
-    apply arity f args
+    wrap prim (f a) >>= fun f ->
+    let MLTactic (arity, prim, f) = to_closure f in
+    apply arity prim f args
   | a :: args, AddAty arity ->
-    apply arity (f a) args
+    apply arity prim (f a) args
 
-let apply (MLTactic (arity, f)) args = apply arity f args
+let apply (MLTactic (arity, wrap, f)) args = apply arity wrap f args
 
 type n_closure =
 | NClosure : 'a arity * (valexpr list -> 'a) -> n_closure
@@ -437,7 +441,11 @@ let rec abstract n f =
 let abstract n f =
   let () = assert (n > 0) in
   let NClosure (arity, f) = abstract n f in
-  MLTactic (arity, f [])
+  MLTactic (arity, None, f [])
 
 let app_fun1 cls r0 r1 x =
   apply cls [r0.r_of x] >>= fun v -> Proofview.tclUNIT (r1.r_to v)
+
+let annotate_prim_closure prim (MLTactic (arity, prim0, f)) =
+  assert (Option.is_empty prim0);
+  MLTactic (arity, Some prim, f)

plugins/ltac2/tac2ffi.mli

@@ -51,6 +51,8 @@ val arity_suc : 'a arity -> (valexpr -> 'a) arity
 
 val mk_closure : 'v arity -> 'v -> closure
 
+val annotate_prim_closure : Tac2expr.ml_tactic_name -> closure -> closure
+
 module Valexpr :
 sig
   type t = valexpr

plugins/ltac2/tac2interp.ml

@@ -156,9 +156,8 @@ let rec interp (ist : environment) = function
 | GTacOpn (kn, el) ->
   Proofview.Monad.List.map (fun e -> interp ist e) el >>= fun el ->
   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)
+| GTacPrm ml ->
+  return (of_closure (Tac2env.interp_primitive ml))
 | GTacExt (tag, e) ->
   let tpe = Tac2env.interp_ml_object tag in
   with_frame (FrExtn (tag, e)) (tpe.Tac2env.ml_interp ist e)
@@ -242,9 +241,11 @@ and eval_pure bnd kn = function
   let bnd = List.fold_left fold bnd vals in
   eval_pure bnd kn body
 
+| GTacPrm ml -> of_closure (Tac2env.interp_primitive ml)
+
 | GTacAtm (AtmStr _) | GTacSet _
 | GTacApp _ | GTacCse _ | GTacPrj _
-| GTacPrm _ | GTacExt _ | GTacWth _
+| GTacExt _ | GTacWth _
 | GTacFullMatch _ ->
   anomaly (Pp.str "Term is not a syntactical value")
 

plugins/ltac2/tac2print.ml

@@ -404,13 +404,9 @@ let pr_glbexpr_gen lvl c =
     let env = Global.env() in
     let sigma = Evd.from_env env in
     hov 0 (tpe.ml_print env sigma arg) (* FIXME *)
-  | GTacPrm (prm, args) ->
-    let args = match args with
-    | [] -> mt ()
-    | _ -> spc () ++ pr_sequence (pr_glbexpr E0) args
-    in
+  | GTacPrm prm ->
     hov 0 (str "@external" ++ spc () ++ qstring prm.mltac_plugin ++ spc () ++
-      qstring prm.mltac_tactic ++ args)
+      qstring prm.mltac_tactic)
   and pr_applied_constructor lvl tpe n cl =
     let factorized =
       if KerName.equal tpe t_list then