From 6b05d49e030e1fba51698b34ed06c3436c23b8a6 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 9 Feb 2022 18:38:15 +0100
Subject: Make minor modifications and cleanup

---
 src/ExtractToFStar.ml  | 3 +++
 src/PureMicroPasses.ml | 9 ++++++---
 2 files changed, 9 insertions(+), 3 deletions(-)

(limited to 'src')

diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index 83eaae9d..506a6d04 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -1011,6 +1011,9 @@ let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter)
   (* Open a box for the definition, so that whenever possible it gets printed on
    * one line - TODO: remove? *)
   F.pp_open_hvbox fmt 0;
+  (* Add the `unfold` keyword *)
+  F.pp_print_string fmt "unfold";
+  F.pp_print_space fmt ();
   (* Open a box for "let FUN_NAME (PARAMS) =" *)
   F.pp_open_hovbox fmt ctx.indent_incr;
   (* > "let FUN_NAME" *)
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index b4f16e6e..e53bc912 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -617,9 +617,12 @@ 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 - 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 *)
+  (* Visit the parameters - TODO: update: we can filter only if the definition
+   * is not recursive (otherwise it might mess up with the decrease clauses:
+   * the decrease clauses uses all the inputs given to the function, if some
+   * inputs are replaced by '_' we can't give it to the function used in the
+   * decreases clause).
+   * For now we deactivate the filtering. *)
   let used_vars = used_vars () in
   let inputs_lvs =
     if false then
-- 
cgit v1.2.3