diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/PureMicroPasses.ml | 8 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 2 |
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 = |