Ltac2: use 0 argument externals when possible

plugins/ltac2/tac2core.ml

@@ -235,7 +235,11 @@ let pf_apply ?(catch_exceptions=false) f =
 (** Primitives *)
 
 let define_primitive name arity f =
-  Tac2env.define_primitive (pname name) (mk_closure arity f)
+  Tac2env.define_primitive (pname name) (of_closure (mk_closure arity f))
+
+(** This should only be used for pure values: no mutable types. For
+    everything else use define0 which defines a thunk. *)
+let defineval name v = Tac2env.define_primitive (pname name) v
 
 let define0 name f = define_primitive name arity_one (fun _ -> f)
 
@@ -305,9 +309,7 @@ let () = define2 "message_concat" pp pp begin fun m1 m2 ->
   return (Value.of_pp (Pp.app m1 m2))
 end
 
-let () = define0 "format_stop" begin
-  return (Value.of_ext val_format [])
-end
+let () = defineval "format_stop" (Value.of_ext val_format [])
 
 let () = define1 "format_string" format begin fun s ->
   return (Value.of_ext val_format (Tac2print.FmtString :: s))
@@ -380,9 +382,7 @@ end
 
 (** Array *)
 
-let () = define0 "array_empty" begin
-  return (v_blk 0 (Array.of_list []))
-end
+let () = defineval "array_empty" (v_blk 0 (Array.of_list []))
 
 let () = define2 "array_make" int valexpr begin fun n x ->
   if n < 0 || n > Sys.max_array_length then throw err_outofbounds
@@ -897,9 +897,7 @@ let () = define_equality "projection_equal" (repr_ext val_projection) Projection
 
 let empty_context = Constr_matching.empty_context
 
-let () = define0 "pattern_empty_context" begin
-  return (Value.of_ext val_matching_context empty_context)
-end
+let () = defineval "pattern_empty_context" (Value.of_ext val_matching_context empty_context)
 
 let () = define2 "pattern_matches" pattern constr begin fun pat c ->
   pf_apply begin fun env sigma ->

test-suite/ltac2/array_lib.v

@@ -44,15 +44,15 @@ Goal True.
   (* Test failure *)
   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].
+  (* test empty with int *) Set Debug "backtrace".
+  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 := "ltac2" "array_empty".
+Ltac2 @external empty : 'a array := "ltac2" "array_empty".
 Ltac2 @external make : int -> 'a -> 'a array := "ltac2" "array_make".
 Ltac2 @external length : 'a array -> int := "ltac2" "array_length".
 Ltac2 @external get : 'a array -> int -> 'a := "ltac2" "array_get".
@@ -48,7 +48,7 @@ Ltac2 @external concat : ('a array) list -> 'a array := "ltac2" "array_concat".
 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 := "ltac2" "format_stop".
+Ltac2 @ external stop : ('a, 'b, 'c, 'a) format := "ltac2" "format_stop".
 
 Ltac2 @ external string : ('a, 'b, 'c, 'd) format ->
   (string -> 'a, 'b, 'c, 'd) format := "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 :=
   "ltac2" "pattern_empty_context".
 (** A trivial context only made of the hole. *)
 
@@ -86,7 +86,7 @@ Ltac2 lazy_match0 t pats :=
     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 =>
@@ -107,7 +107,7 @@ Ltac2 multi_match0 t pats :=
     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 =>