diff options
author | Son Ho | 2022-02-09 16:35:36 +0100 |
---|---|---|
committer | Son Ho | 2022-02-09 16:35:36 +0100 |
commit | dd1a786022b493c10da6f4d6d1c88a41b70e1eb5 (patch) | |
tree | 959895c7e52f45635fff8999f9d8dcb0de0782c1 /src/PureMicroPasses.ml | |
parent | 056e6af4cf469dc9d72dff5222363edd9b563588 (diff) |
Implement the generation of `decreases` clauses in the definition
signatures
Diffstat (limited to '')
-rw-r--r-- | src/PureMicroPasses.ml | 8 |
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 } |