Improve PureMicroPasses.filter_useless and regenerate the betree code

2 files changed, 10 insertions, 0 deletions

diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 25d760fe..b9441397 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -828,6 +828,14 @@ let filter_useless (filter_monadic_calls : bool) (ctx : trans_ctx)
             let dont_filter () =
               let re, used_re = self#visit_texpression env re in
               let used = VarId.Set.union used (used_re ()) in
+              (* Simplify the left pattern if it only contains dummy variables *)
+              let lv =
+                if all_dummies then
+                  let ty = lv.ty in
+                  let value = PatDummy in
+                  { value; ty }
+                else lv
+              in
               (Let (monadic, lv, re, e), fun _ -> used)
             in
             (* Potentially filter the let-binding *)
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 81d81789..49b696b2 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -2314,6 +2314,8 @@ and translate_forward_end (ectx : C.eval_ctx)
         let call = mk_apps func args in
         call
       in
+
+      (* Create the let expression with the loop call *)
       mk_let effect_info.can_fail out_pat loop_call next_e
 
 and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =