Start working on function extraction

2 files changed, 40 insertions, 6 deletions

diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index a1b56964..a839c0a3 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -469,3 +469,13 @@ let extract_fun_def_register_names (ctx : extraction_ctx)
   in
   (* Return *)
   ctx
+
+(** Extract a function definition.
+
+    Note that all the names used for extraction should already have been
+    registered.
+ *)
+let extract_fun_def (ctx : extraction_ctx) (fmt : F.formatter)
+    (qualif : fun_def_qualif) (def : fun_def) : unit =
+  (* TODO *)
+  ()
diff --git a/src/Translate.ml b/src/Translate.ml
index b840b7bc..95cae60b 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -350,10 +350,20 @@ let translate_module (filename : string) (config : C.partial_config)
     let def = Pure.TypeDefId.Map.find id trans_types in
     ExtractToFStar.extract_type_def extract_ctx fmt qualif def
   in
-  let export_function (id : Pure.FunDefId.id) : unit =
-    (* TODO *)
-    (*    let pure_defs = Pure.FunDefId.Map.find id trans_funs in *)
-    ()
+  (* In case of recursive functions, we always extract the forward and
+   * backward functions as mutually recursive functions.
+   * There are many situations where they are actually not mutually recursive:
+   * we could detect such cases. TODO *)
+  let export_functions (is_rec : bool) (fls : Pure.fun_def list) : unit =
+    List.iteri
+      (fun i def ->
+        let qualif =
+          if not is_rec then ExtractToFStar.Let
+          else if i = 0 then ExtractToFStar.LetRec
+          else ExtractToFStar.And
+        in
+        ExtractToFStar.extract_fun_def extract_ctx fmt qualif def)
+      fls
   in
   let export_decl (decl : M.declaration_group) : unit =
     match decl with
@@ -366,9 +376,23 @@ let translate_module (filename : string) (config : C.partial_config)
             in
             export_type qualif id)
           ids
-    | Fun (NonRec id) -> export_function id
-    | Fun (Rec ids) -> List.iter export_function ids
+    | Fun (NonRec id) ->
+        (* Concatenate *)
+        let fwd, back_ls = Pure.FunDefId.Map.find id trans_funs in
+        let fls = fwd :: back_ls in
+        (* Translate *)
+        export_functions false fls
+    | Fun (Rec ids) ->
+        (* Concatenate *)
+        let compute_fun_id_list (id : Pure.FunDefId.id) : Pure.fun_def list =
+          let fwd, back_ls = Pure.FunDefId.Map.find id trans_funs in
+          fwd :: back_ls
+        in
+        let fls = List.concat (List.map compute_fun_id_list ids) in
+        (* Translate *)
+        export_functions true fls
   in
+
   List.iter export_decl m.declarations;
 
   (* Close the box and end the formatting *)