More precise monad thunking (#21)

src/tac2compile.ml

@@ -768,7 +768,7 @@ let rec pp_nontac_expr = function
     pp_mk_closure_val (List.length nas)
       (surround
          (h (str "fun" ++ pp_binders nas ++ str " ->") ++ spc() ++
-          pp_expr e))
+          str "PV.tclUNIT () >>= fun () ->" ++ spc() ++  pp_expr e))
   | Ctor (i, es) -> str "(ValBlk (" ++ int i ++ str ", [|" ++ pp_val_list es ++ str "|]))"
   | PrjV (e, i) ->
     surround
@@ -804,10 +804,10 @@ and pp_expr e =
     else surround (pp_binds Id.print pp_expr nonvals ++ pp_head_expr e)
   in
   match e with
-  | Return _ | LetRec _ -> mainpp
-  | _ ->
+  | Match _ | CtorMut _ | PrjMut _ | Set _ ->
     (* monad-thunk nontrivial computations *)
     surround (str "PV.tclUNIT () >>= fun () ->" ++ spc() ++ mainpp)
+  | App _ | Return _ | LetNoRec _ | LetRec _ | Ext _ -> mainpp
 
 and pp_head_expr = function
   | Return e -> surround (str "PV.tclUNIT" ++ spc() ++ pp_nontac_expr e)
@@ -943,7 +943,7 @@ let pp_one_constant (kn, knid, na, bnd, e) =
     | Fun (nas, e) ->
       hv 2
         (str "let " ++ h (str na ++ pp_binders nas) ++ str " =" ++ spc() ++
-         pp_expr e) ++ fnl() ++ fnl()
+         str "PV.tclUNIT () >>= fun () ->" ++ spc() ++ pp_expr e) ++ fnl() ++ fnl()
     | _ -> hv 2 (str "let " ++ str na ++ str " =" ++ spc() ++ pp_nontac_expr e) ++ fnl() ++ fnl()
   in
   let pp_set_compiled =

tests/compiler_bug_17.v

@@ -14,8 +14,20 @@ Ltac2 test2 () :=
   ltac1:(assert False) >
           [pop inner; pop outer|let outer := push () in pop outer].
 
-Ltac2 Compile test2.
+Ltac2 aux1 outer inner _ := pop inner; pop outer.
+Ltac2 aux2 _ := let outer := push() in pop outer.
+
+Ltac2 test3 :=
+  fun _ =>
+    let outer := push () in
+    let inner := push () in
+    let l :=
+      [aux1 outer inner; aux2],
+        None with t := fun _ => ltac1:(assert False) in
+                         dispatch0 t l.
+
+Ltac2 Compile test2 test3.
 
 Goal True /\ True.
-  test2 ().
+  test3 ().
 Abort.