Implement generation of template decrease clauses

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