Ltac2: use 0 argument externals when possible

doc/changelog/06-Ltac2-language/17534-ltac2-0arg-empty.rst

@@ -0,0 +1,4 @@
+- **Changed:**
+  `Array.empty`, `Message.Format.stop` and `Pattern.empty_context` are not thunked
+  (`#17534 <https://github.com/coq/coq/pull/17534>`_,
+  by Gaëtan Gilbert).

plugins/ltac2/tac2core.ml

@@ -264,7 +264,7 @@ let () =
 
 let () = define "message_concat" (pp @-> pp @-> ret pp) Pp.app
 
-let () = define "format_stop" (unit @-> ret format) (fun _ -> [])
+let () = define "format_stop" (ret format) []
 
 let () =
   define "format_string" (format @-> ret format) @@ fun s ->
@@ -337,7 +337,7 @@ let () =
 
 (** Array *)
 
-let () = define "array_empty" (unit @-> ret valexpr) (fun _ -> v_blk 0 [||])
+let () = define "array_empty" (ret valexpr) (v_blk 0 [||])
 
 let () =
   define "array_make" (int @-> valexpr @-> tac valexpr) @@ fun n x ->
@@ -812,8 +812,8 @@ let () =
 
 let () =
   define "pattern_empty_context"
-    (unit @-> ret (repr_ext val_matching_context))
-    (fun _ -> Constr_matching.empty_context)
+    (ret (repr_ext val_matching_context))
+    Constr_matching.empty_context
 
 let () =
   define "pattern_matches" (pattern @-> constr @-> tac valexpr) @@ fun pat c ->

plugins/ltac2/tac2quote.ml

@@ -553,5 +553,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

test-suite/ltac2/array_lib.v

@@ -45,14 +45,14 @@ Goal True.
   Fail check_eq_int ((init 3 (fun i => (Int.add i 10)))) [10;11;13].
 
   (* test empty with int *)
-  check_eq_int (empty ()) [].
-  check_eq_int (append (empty ()) (init 3 (fun i => (Int.add i 10)))) [10;11;12].
-  check_eq_int (append (init 3 (fun i => (Int.add i 10))) (empty ())) [10;11;12].
+  check_eq_int empty [].
+  check_eq_int (append empty (init 3 (fun i => (Int.add i 10)))) [10;11;12].
+  check_eq_int (append (init 3 (fun i => (Int.add i 10))) empty) [10;11;12].
 
   (* test empty with bool *)
-  check_eq_bool (empty ()) [].
-  check_eq_bool (append (empty ()) (init 3 (fun i => (Int.ge i 2)))) [false;false;true].
-  check_eq_bool (append (init 3 (fun i => (Int.ge i 2))) (empty ())) [false;false;true].
+  check_eq_bool empty [].
+  check_eq_bool (append empty (init 3 (fun i => (Int.ge i 2)))) [false;false;true].
+  check_eq_bool (append (init 3 (fun i => (Int.ge i 2))) empty) [false;false;true].
 
   (* test init with int *)
   check_eq_int (init 0 (fun i => (Int.add i 10))) [].

test-suite/ltac2/fragile_matching.v

@@ -109,7 +109,7 @@ Module RealCodeTest.
             } =>
             true
           end)
-        (Array.empty ())
+        Array.empty
     }.
 
 End RealCodeTest.

user-contrib/Ltac2/Array.v

@@ -34,7 +34,7 @@ Require Ltac2.Message.
 (* Question: what is returned in case of an out of range value?
    Answer:   Ltac2 throws a panic *)
 
-Ltac2 @external empty : unit -> 'a array := "coq-core.plugins.ltac2" "array_empty".
+Ltac2 @external empty : 'a array := "coq-core.plugins.ltac2" "array_empty".
 Ltac2 @external make : int -> 'a -> 'a array := "coq-core.plugins.ltac2" "array_make".
 Ltac2 @external length : 'a array -> int := "coq-core.plugins.ltac2" "array_length".
 Ltac2 @external get : 'a array -> int -> 'a := "coq-core.plugins.ltac2" "array_get".
@@ -48,7 +48,7 @@ Ltac2 @external concat : ('a array) list -> 'a array := "coq-core.plugins.ltac2"
 Ltac2 lowlevel_sub (arr : 'a array) (start : int) (len : int) :=
   let l := length arr in
   match Int.equal l 0 with
-  | true => empty ()
+  | true => empty
   | false =>
       let newarr:=make len (get arr 0) in
       lowlevel_blit arr start newarr 0 len;
@@ -67,7 +67,7 @@ Ltac2 init (l : int) (f : int->'a) :=
     end
   in
   match Int.le l 0 with
-  | true => empty ()
+  | true => empty
   | false =>
       let arr:=make l (f 0) in
       init_aux arr 1 (Int.sub l 1) f;
@@ -174,7 +174,7 @@ Ltac2 of_list (ls : 'a list) :=
     | _ :: tl => Int.add 1 (list_length tl)
     end in
   match ls with
-  | [] => empty ()
+  | [] => empty
   | hd::tl =>
       let anew := make (list_length ls) hd in
       of_list_aux ls anew 0;

user-contrib/Ltac2/Message.v

@@ -32,7 +32,7 @@ Module Format.
 
 (** Only for internal use. *)
 
-Ltac2 @ external stop : unit -> ('a, 'b, 'c, 'a) format := "coq-core.plugins.ltac2" "format_stop".
+Ltac2 @ external stop : ('a, 'b, 'c, 'a) format := "coq-core.plugins.ltac2" "format_stop".
 
 Ltac2 @ external string : ('a, 'b, 'c, 'd) format ->
   (string -> 'a, 'b, 'c, 'd) format := "coq-core.plugins.ltac2" "format_string".

user-contrib/Ltac2/Pattern.v

@@ -20,7 +20,7 @@ Ltac2 Type match_kind := [
 | MatchContext
 ].
 
-Ltac2 @ external empty_context : unit -> context :=
+Ltac2 @ external empty_context : context :=
   "coq-core.plugins.ltac2" "pattern_empty_context".
 (** A trivial context only made of the hole. *)
 
@@ -88,7 +88,7 @@ Ltac2 lazy_match0 t (pats:'a constr_matching) :=
     let p := match knd with
     | MatchPattern =>
       (fun _ =>
-        let context := empty_context () in
+        let context := empty_context in
         let bind := matches_vect pat t in
         fun _ => f context bind)
     | MatchContext =>
@@ -109,7 +109,7 @@ Ltac2 multi_match0 t (pats:'a constr_matching) :=
     let p := match knd with
     | MatchPattern =>
       (fun _ =>
-        let context := empty_context () in
+        let context := empty_context in
         let bind := matches_vect pat t in
         f context bind)
     | MatchContext =>