diff options
author | Son Ho | 2022-02-09 16:57:15 +0100 |
---|---|---|
committer | Son Ho | 2022-02-09 16:57:15 +0100 |
commit | 3cd24d0b0ecd4a7a71587a5f1479852f40f959ff (patch) | |
tree | 9605cea75b0153e04526e79c2604ebb0026b9298 /src/Translate.ml | |
parent | dd1a786022b493c10da6f4d6d1c88a41b70e1eb5 (diff) |
Implement generation of template decrease clauses
Diffstat (limited to 'src/Translate.ml')
-rw-r--r-- | src/Translate.ml | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/Translate.ml b/src/Translate.ml index 3c12bc90..ec817b50 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -347,6 +347,15 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) if keep_fwd then (fwd, fwd) :: back_ls else back_ls) pure_ls) in + (* Extract the decrease clauses template bodies *) + if config.extract_template_decrease_clauses then + List.iter + (fun (_, (fwd, _)) -> + let has_decr_clause = has_decrease_clause fwd in + if has_decr_clause then + ExtractToFStar.extract_template_decrease_clause ctx.extract_ctx fmt + fwd) + pure_ls; (* Extract the function definitions *) (if config.extract_fun_defs then (* Check if the functions are mutually recursive - this really works |