From 3c6255c3c43fef1a5c20925b661af7ce2d5c177f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Thu, 18 Jul 2024 16:33:30 +0200
Subject: [PATCH] Tac2externals: wrap closures to make them 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

Close #18631
---
 plugins/ltac2/tac2externals.ml | 7 +++++--
 plugins/ltac2/tac2val.ml       | 7 +++++++
 plugins/ltac2/tac2val.mli      | 7 +++++++
 3 files changed, 19 insertions(+), 2 deletions(-)

diff --git a/plugins/ltac2/tac2externals.ml b/plugins/ltac2/tac2externals.ml
index bf470da51327..4a6ba81e347b 100644
--- a/plugins/ltac2/tac2externals.ml
+++ b/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 = Tac2val.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 = Tac2val.purify_closure arity v in
+      let cl = Tac2val.mk_closure arity v in
+      Tac2ffi.of_closure cl
     | _ -> invalid_arg "Tac2def.define: not a pure value"
   in
   Tac2env.define_primitive n v
diff --git a/plugins/ltac2/tac2val.ml b/plugins/ltac2/tac2val.ml
index b15698fd8f9e..1b96ee0b23e2 100644
--- a/plugins/ltac2/tac2val.ml
+++ b/plugins/ltac2/tac2val.ml
@@ -123,3 +123,10 @@ let abstract n f =
 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 -> (unit -> a) -> a = fun arity f ->
+  match arity with
+  | OneAty -> (fun x -> Proofview.tclUNIT () >>= fun () -> f () x)
+  | AddAty a -> (fun x -> purify_closure a (fun () -> f () x))
+
+let purify_closure ar f = purify_closure ar (fun () -> f)
diff --git a/plugins/ltac2/tac2val.mli b/plugins/ltac2/tac2val.mli
index d50411abc61d..529c4ce407d7 100644
--- a/plugins/ltac2/tac2val.mli
+++ b/plugins/ltac2/tac2val.mli
@@ -57,12 +57,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 applications of the ['v] argument
+    to make it pure. *)
+
 val to_closure : valexpr -> closure
 
 val apply : closure -> valexpr list -> valexpr Proofview.tactic