From 056e6af4cf469dc9d72dff5222363edd9b563588 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 9 Feb 2022 13:06:30 +0100
Subject: Start implementing selection of the extracted definitions

---
 src/Translate.ml | 86 ++++++++++++++++++++++++++++++++------------------------
 1 file changed, 49 insertions(+), 37 deletions(-)

(limited to 'src')

diff --git a/src/Translate.ml b/src/Translate.ml
index da0b32a4..9d5d2b75 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -301,20 +301,24 @@ type gen_ctx = {
   extract_ctx : PureToExtract.extraction_ctx;
   trans_types : Pure.type_def Pure.TypeDefId.Map.t;
   trans_funs : (bool * pure_fun_translation) Pure.FunDefId.Map.t;
-  extract_types : bool;
   functions_with_decrease_clause : Pure.FunDefId.Set.t;
+}
+(** Extraction context *)
+
+type gen_config = {
+  extract_types : bool;
   extract_decrease_clauses : bool;
   extract_template_decrease_clauses : bool;
-  extract_functions : bool;
+  extract_fun_defs : bool;
   test_unit_functions : bool;
 }
-(** Extraction context *)
 
 (** A generic utility to generate the extracted definitions: as we may want to
     split the definitions between different files (or not), we can control
     what is precisely extracted.
  *)
-let extract_definitions (fmt : Format.formatter) (ctx : gen_ctx) : unit =
+let extract_definitions (fmt : Format.formatter) (config : gen_config)
+    (ctx : gen_ctx) : unit =
   (* Export the definition groups to the file, in the proper order *)
   let export_type (qualif : ExtractToFStar.type_def_qualif)
       (id : Pure.TypeDefId.id) : unit =
@@ -327,7 +331,7 @@ let extract_definitions (fmt : Format.formatter) (ctx : gen_ctx) : unit =
    *)
   let export_functions (is_rec : bool)
       (pure_ls : (bool * pure_fun_translation) list) : unit =
-    (* Generate the function definitions, filtering the uselss forward
+    (* Concatenate the function definitions, filtering the useless forward
      * functions. *)
     let fls =
       List.concat
@@ -336,28 +340,30 @@ let extract_definitions (fmt : Format.formatter) (ctx : gen_ctx) : unit =
              if keep_fwd then fwd :: back_ls else back_ls)
            pure_ls)
     in
-    (* Check if the functions are mutually recursive - this really works
-     * to check if the forward and backward translations of a single
-     * recursive function are mutually recursive *)
-    let is_mut_rec =
-      if is_rec then
-        if List.length pure_ls <= 1 then
-          not (PureUtils.functions_not_mutually_recursive fls)
-        else true
-      else false
-    in
-    List.iteri
-      (fun i def ->
-        let qualif =
-          if not is_rec then ExtractToFStar.Let
-          else if is_mut_rec then
-            if i = 0 then ExtractToFStar.LetRec else ExtractToFStar.And
-          else ExtractToFStar.LetRec
-        in
-        ExtractToFStar.extract_fun_def ctx.extract_ctx fmt qualif def)
-      fls;
+    (* Extract the function definitions *)
+    (if config.extract_fun_defs then
+     (* Check if the functions are mutually recursive - this really works
+      * to check if the forward and backward translations of a single
+      * recursive function are mutually recursive *)
+     let is_mut_rec =
+       if is_rec then
+         if List.length pure_ls <= 1 then
+           not (PureUtils.functions_not_mutually_recursive fls)
+         else true
+       else false
+     in
+     List.iteri
+       (fun i def ->
+         let qualif =
+           if not is_rec then ExtractToFStar.Let
+           else if is_mut_rec then
+             if i = 0 then ExtractToFStar.LetRec else ExtractToFStar.And
+           else ExtractToFStar.LetRec
+         in
+         ExtractToFStar.extract_fun_def ctx.extract_ctx fmt qualif def)
+       fls);
     (* Insert unit tests if necessary *)
-    if ctx.test_unit_functions then
+    if config.test_unit_functions then
       List.iter
         (fun (keep_fwd, (fwd, _)) ->
           if keep_fwd then
@@ -367,15 +373,17 @@ let extract_definitions (fmt : Format.formatter) (ctx : gen_ctx) : unit =
 
   let export_decl (decl : M.declaration_group) : unit =
     match decl with
-    | Type (NonRec id) -> export_type ExtractToFStar.Type id
+    | Type (NonRec id) ->
+        if config.extract_types then export_type ExtractToFStar.Type id
     | Type (Rec ids) ->
-        List.iteri
-          (fun i id ->
-            let qualif =
-              if i = 0 then ExtractToFStar.Type else ExtractToFStar.And
-            in
-            export_type qualif id)
-          ids
+        if config.extract_types then
+          List.iteri
+            (fun i id ->
+              let qualif =
+                if i = 0 then ExtractToFStar.Type else ExtractToFStar.And
+              in
+              export_type qualif id)
+            ids
     | Fun (NonRec id) ->
         (* Lookup *)
         let pure_fun = Pure.FunDefId.Map.find id ctx.trans_funs in
@@ -506,15 +514,19 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
       extract_ctx = ctx;
       trans_types;
       trans_funs;
-      extract_types = true;
       functions_with_decrease_clause = rec_functions;
+    }
+  in
+  let gen_config =
+    {
+      extract_types = true;
       extract_decrease_clauses = true;
       extract_template_decrease_clauses = false;
-      extract_functions = true;
+      extract_fun_defs = true;
       test_unit_functions = config.test_unit_functions;
     }
   in
-  extract_definitions fmt gen_ctx;
+  extract_definitions fmt gen_config gen_ctx;
 
   (* Close the box and end the formatting *)
   Format.pp_close_box fmt ();
-- 
cgit v1.2.3