From 3cd24d0b0ecd4a7a71587a5f1479852f40f959ff Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 9 Feb 2022 16:57:15 +0100
Subject: Implement generation of template decrease clauses

---
 src/Translate.ml | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'src/Translate.ml')

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
-- 
cgit v1.2.3