diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ExtractToFStar.ml | 3 | ||||
| -rw-r--r-- | src/PureMicroPasses.ml | 9 |
2 files changed, 9 insertions, 3 deletions
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 |