From de0431f31d77a53445a6731560a25c24b52384bf Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sat, 29 Jan 2022 20:35:44 +0100
Subject: Cleanup a bit

---
 src/Collections.ml    | 17 +++++++++++++++++
 src/ExtractToFStar.ml | 23 ++++-------------------
 2 files changed, 21 insertions(+), 19 deletions(-)

diff --git a/src/Collections.ml b/src/Collections.ml
index bb7c37f1..125cab1f 100644
--- a/src/Collections.ml
+++ b/src/Collections.ml
@@ -38,6 +38,23 @@ module List = struct
 
   (** Return the n first elements of the list *)
   let prefix (n : int) (ls : 'a list) : 'a list = fst (split_at ls n)
+
+  (** Iter and link the iterations.
+
+    Iterate over a list, but call a function between every two elements
+    (but not before the first element, and not after the last).
+ *)
+  let iter_link (link : unit -> unit) (f : 'a -> unit) (ls : 'a list) : unit =
+    let rec iter ls =
+      match ls with
+      | [] -> ()
+      | [ x ] -> f x
+      | x :: y :: ls ->
+          f x;
+          link ();
+          iter (y :: ls)
+    in
+    iter ls
 end
 
 module type OrderedType = sig
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index 4491a722..d0726ac7 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -6,23 +6,6 @@ open TranslateCore
 open PureToExtract
 module F = Format
 
-(** Iter "between".
-
-    Iterate over a list, but call a function between every two elements
-    (but not before the first element, and not after the last).
- *)
-let list_iterb (between : unit -> unit) (f : 'a -> unit) (ls : 'a list) : unit =
-  let rec iter ls =
-    match ls with
-    | [] -> ()
-    | [ x ] -> f x
-    | x :: y :: ls ->
-        f x;
-        between ();
-        iter (y :: ls)
-  in
-  iter ls
-
 (** [inside] constrols whether we should add parentheses or not around type
     application (if `true` we add parentheses).
  *)
@@ -33,13 +16,15 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
       match type_id with
       | Tuple ->
           F.pp_print_string fmt "(";
-          list_iterb (F.pp_print_space fmt) (extract_ty ctx fmt true) tys;
+          Collections.List.iter_link (F.pp_print_space fmt)
+            (extract_ty ctx fmt true) tys;
           F.pp_print_string fmt ")"
       | AdtId _ | Assumed _ ->
           if inside then F.pp_print_string fmt "(";
           F.pp_print_string fmt (ctx_get_type type_id ctx);
           if tys <> [] then F.pp_print_space fmt ();
-          list_iterb (F.pp_print_space fmt) (extract_ty ctx fmt true) tys;
+          Collections.List.iter_link (F.pp_print_space fmt)
+            (extract_ty ctx fmt true) tys;
           if inside then F.pp_print_string fmt ")")
   | TypeVar vid -> F.pp_print_string fmt (ctx_get_type_var vid ctx)
   | Bool -> F.pp_print_string fmt ctx.fmt.bool_name
-- 
cgit v1.2.3