Implement the generation of `decreases` clauses in the definition

signatures

1 files changed, 6 insertions, 2 deletions

diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index dba6b5e8..b4f16e6e 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -617,10 +617,14 @@ let filter_useless (filter_monadic_calls : bool) (ctx : trans_ctx)
   in
   (* Visit the body *)
   let body, used_vars = expr_visitor#visit_texpression () def.body in
-  (* Visit the parameters *)
+  (* Visit the parameters - TODO: update: we need filter only if the definition
+   * is not recursive (otherwise it might mess up with the decrease clauses).
+   * For now we deactivate the filtering *)
   let used_vars = used_vars () in
   let inputs_lvs =
-    List.map (fun lv -> fst (filter_typed_lvalue used_vars lv)) def.inputs_lvs
+    if false then
+      List.map (fun lv -> fst (filter_typed_lvalue used_vars lv)) def.inputs_lvs
+    else def.inputs_lvs
   in
   (* Return *)
   { def with body; inputs_lvs }