Tac2externals: wrap last application of the closure to make it pure

otherwise it can be quite footgunny (even though it's hard to get a
visible bug without the ltac2 compiler), for instance the current
implementation of Array.set is incorrect without this.

See also SkySkimmer/coq-ltac2-compiler#17
and https://coq.zulipchat.com/#narrow/stream/278935-Ltac2/topic/thunking.20and.20.60thaw.60

plugins/ltac2/tac2externals.ml

@@ -82,8 +82,11 @@ let define : type v f. _ -> (v,f) spec -> f -> unit = fun n ar v ->
     match ar with
     | S (V tr) -> tr v
     | S (F _) ->
-        let cl = Tac2ffi.mk_closure (arity_of ar) (interp_spec ar v) in
-        Tac2ffi.of_closure cl
+      let arity = arity_of ar in
+      let v = interp_spec ar v in
+      let v = Tac2ffi.purify_closure arity v in
+      let cl = Tac2ffi.mk_closure arity v in
+      Tac2ffi.of_closure cl
     | _ -> invalid_arg "Tac2def.define: not a pure value"
   in
   Tac2env.define_primitive n v

plugins/ltac2/tac2ffi.ml

@@ -476,3 +476,8 @@ let app_fun1 cls r0 r1 x =
 let annotate_closure fr (MLTactic (arity, fr0, f)) =
   assert (Option.is_empty fr0);
   MLTactic (arity, Some fr, f)
+
+let rec purify_closure : type a. a arity -> a -> a = fun arity f ->
+  match arity with
+  | OneAty -> (fun x -> Proofview.tclUNIT () >>= fun () -> f x)
+  | AddAty a -> (fun x -> purify_closure a (f x))

plugins/ltac2/tac2ffi.mli

@@ -46,12 +46,19 @@ val arity_one : (valexpr -> valexpr Proofview.tactic) arity
 val arity_suc : 'a arity -> (valexpr -> 'a) arity
 
 val mk_closure : 'v arity -> 'v -> closure
+(** The arrows in ['v] should be pure. Use [tclLIFT] or do
+    [tclUNIT () >>= fun () -> f args] when you need effects. *)
+
 val mk_closure_val : 'v arity -> 'v -> valexpr
 (** Composition of [mk_closure] and [ValCls] *)
 
 val annotate_closure : Tac2expr.frame -> closure -> closure
 (** The closure must not be already annotated *)
 
+val purify_closure : 'v arity -> 'v -> 'v
+(** For internal use (Tac2externals). Wraps the last application of the ['v] argument
+    to make it pure. *)
+
 module Valexpr :
 sig
   type t = valexpr