Monad-thunk every nontrivial nontac_expr

src/tac2compile.ml

@@ -747,8 +747,15 @@ let rec pp_nontac_expr = function
 (* produce a ocaml term of type valexpr tactic *)
 and pp_expr e =
   let { spilled_exprs = nonvals; head_expr = e; } = e in
-  if List.is_empty nonvals then pp_head_expr e
-  else surround (pp_binds Id.print pp_expr nonvals ++ pp_head_expr e)
+  let mainpp =
+    if List.is_empty nonvals then pp_head_expr e
+    else surround (pp_binds Id.print pp_expr nonvals ++ pp_head_expr e)
+  in
+  match e with
+  | Return _ | LetRec _ -> mainpp
+  | _ ->
+    (* monad-thunk nontrivial computations *)
+    surround (str "PV.tclUNIT () >>= fun () ->" ++ spc() ++ mainpp)
 
 and pp_head_expr = function
   | Return e -> surround (str "PV.tclUNIT" ++ spc() ++ pp_nontac_expr e)
@@ -845,36 +852,25 @@ and pp_head_expr = function
          hv 0 (prlist pp_branch brs ++ str "end"))
 
   | CtorMut (i, es) ->
-    (* Not sure if we actually need to thunk this one but let's be safe. *)
-    hv 1
-      (str "(PV.tclUNIT () >>= fun () ->" ++ spc() ++
-       str "PV.tclUNIT" ++ spc() ++
+    str "PV.tclUNIT" ++ spc() ++
+    surround
+      (str "ValBlk" ++ spc() ++
        surround
-         (str "ValBlk" ++ spc() ++
-          surround
-            (int i ++ str "," ++ spc() ++
-             hov 2
-               (str "[|" ++ pp_val_list es ++ str "|]"))) ++
-       str ")")
+         (int i ++ str "," ++ spc() ++
+          hov 2
+            (str "[|" ++ pp_val_list es ++ str "|]")))
 
   | PrjMut (e, i) ->
-    (* Don't forget to delay the side effect with a thunk! *)
-    hv 1
-      (str "(PV.tclUNIT () >>= fun () ->" ++ spc() ++
-       str "PV.tclUNIT" ++ spc() ++
-       surround
-         (str "Tac2ffi.Valexpr.field" ++ spc() ++ pp_nontac_expr e ++ spc() ++ int i) ++
-       str ")")
+    str "PV.tclUNIT" ++ spc() ++
+    surround
+      (str "Tac2ffi.Valexpr.field" ++ spc() ++ pp_nontac_expr e ++ spc() ++ int i)
 
   | Set (e1,i,e2) ->
-    (* Don't forget to delay the side effect with a thunk! *)
-    hv 1
-      (str "(PV.tclUNIT () >>= fun () ->" ++ spc() ++
-       h (str "let () = Tac2ffi.Valexpr.set_field" ++ spc() ++
-          pp_nontac_expr e1 ++ spc() ++ int i ++ spc() ++
-          pp_nontac_expr e2 ++ spc()) ++
-       str "in" ++ spc() ++
-       str "PV.tclUNIT (ValInt 0))")
+    h (str "let () = Tac2ffi.Valexpr.set_field" ++ spc() ++
+       pp_nontac_expr e1 ++ spc() ++ int i ++ spc() ++
+       pp_nontac_expr e2 ++ spc()) ++
+    str "in" ++ spc() ++
+    str "PV.tclUNIT (ValInt 0)"
 
   | Ext (ids, v) ->
     surround

tests/Makefile.coq.local

@@ -0,0 +1 @@
+CAMLPKGS:=-package coq-core.plugins.ltac2

tests/_CoqProject

@@ -9,3 +9,10 @@ minibench.v
 compiler_bug_4.v
 compiler_bug_6.v
 compiler_bug_14.v
+compiler_bug_17.v
+
+-I src
+
+src/META.compiler-bugs
+src/compiler_bug_17.ml
+src/compiler_bug_17_plugin.mlpack

tests/compiler_bug_17.v

@@ -0,0 +1,21 @@
+From Ltac2 Require Import Ltac2 Printf.
+
+From Ltac2Compiler Require Import Ltac2Compiler.
+
+Declare ML Module "compiler-bugs.compiler_bug_17".
+
+Ltac2 @ external push : unit -> int := "compiler-bugs.compiler_bug_17" "push".
+Ltac2 @ external pop : int -> unit := "compiler-bugs.compiler_bug_17" "pop".
+Ltac2 @ external reset : unit -> unit := "compiler-bugs.compiler_bug_17" "reset".
+
+Ltac2 test2 () :=
+  let outer := push () in
+  let inner := push () in
+  ltac1:(assert False) >
+          [pop inner; pop outer|let outer := push () in pop outer].
+
+Ltac2 Compile test2.
+
+Goal True /\ True.
+  test2 ().
+Abort.

tests/src/META.compiler-bugs

@@ -0,0 +1,10 @@
+package "compiler_bug_17" (
+    directory = "."
+    version = "dev"
+    requires = "coq-core.plugins.ltac2"
+    archive(byte) = "compiler_bug_17_plugin.cma"
+    archive(native) = "compiler_bug_17_plugin.cmxa"
+    plugin(byte) = "compiler_bug_17_plugin.cma"
+    plugin(native) = "compiler_bug_17_plugin.cmxs"
+)
+directory = "."

tests/src/compiler_bug_17.ml

@@ -0,0 +1,20 @@
+open Ltac2_plugin
+open Tac2ffi
+open Tac2expr
+open Tac2externals
+
+let define s = define { mltac_plugin = "compiler-bugs.compiler_bug_17"; mltac_tactic = s }
+
+let state : int ref = Summary.ref ~name:"tac2compile_bug17" 0
+let push  : unit -> int  = fun () ->
+  state := 1 + !state; !state
+let pop   : int -> unit  = fun i ->
+  if i == !state then
+    state := i - 1
+  else
+    raise Not_found
+let reset : unit -> unit = fun _ -> state := 0
+
+let _ = define "push"  (unit @-> ret int) push
+let _ = define "pop"   (int @-> ret unit) pop
+let _ = define "reset" (unit @-> ret unit) reset

tests/src/compiler_bug_17_plugin.mlpack

@@ -0,0 +1 @@
+Compiler_bug_17