summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2022-01-29 20:35:44 +0100
committerSon Ho2022-01-29 20:35:44 +0100
commitde0431f31d77a53445a6731560a25c24b52384bf (patch)
tree0822cf604d2a865e8ef2e4e0cd7144410e107130 /src
parent79af7f999e3a41e3c5f9a30819a7cc43b5397c56 (diff)
Cleanup a bit
Diffstat (limited to '')
-rw-r--r--src/Collections.ml17
-rw-r--r--src/ExtractToFStar.ml23
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