From 4f21e67814f3c58cedebb7408ba1f41eb0c619ee Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 18 Jul 2022 11:16:42 +0200
Subject: [PATCH] [Extlib] removed swap (Fun.flip)
---
bin/migration_scripts/manganese2iron.sh | 3 ++-
src/kernel_internals/typing/cabs2cil.ml | 4 ++--
src/kernel_services/ast_data/annotations.ml | 12 ++++++------
src/kernel_services/ast_queries/cil.ml | 4 ++--
src/kernel_services/ast_queries/file.ml | 2 +-
src/libraries/stdlib/extlib.ml | 2 --
src/libraries/stdlib/extlib.mli | 3 ---
7 files changed, 13 insertions(+), 17 deletions(-)
diff --git a/bin/migration_scripts/manganese2iron.sh b/bin/migration_scripts/manganese2iron.sh
index e33d1f41134..2f6fda59997 100755
--- a/bin/migration_scripts/manganese2iron.sh
+++ b/bin/migration_scripts/manganese2iron.sh
@@ -85,7 +85,8 @@ process_file ()
echo "Processing file $file"
fi
sedi "$file" \
- -e 's/Extlib\.id/Fun.id/g'
+ -e 's/Extlib\.id/Fun.id/g' \
+ -e 's/Extlib\.swap/Fun.flip/g'
# this line left empty on purpose
}
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index aeda98b6756..71228ea8e08 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -4324,7 +4324,7 @@ let append_chunk_to_annot ~ghost annot_chunk current_chunk =
let res =
match current_chunk.stmts with
| [(s1, m1, w1, r1, c1); (s2, m2, w2, r2, c2)] ->
- Extlib.swap
+ Fun.flip
Option.bind
(function
| [ s1' ] -> Some (s1', m1 @ m2, w1 @ w2, r1 @ r2, c1 @ c2)
@@ -9690,7 +9690,7 @@ and doDecl local_env (isglobal: bool) : Cabs.definition -> chunk = function
let attr = fc_stdlib_attribute [] in
let tdecl =
List.fold_left
- (Extlib.swap Logic_utils.add_attribute_glob_annot) tdecl attr
+ (Fun.flip Logic_utils.add_attribute_glob_annot) tdecl attr
in
cabsPushGlobal (GAnnot(tdecl,CurrentLoc.get ()))
with LogicTypeError ((source,_),msg) ->
diff --git a/src/kernel_services/ast_data/annotations.ml b/src/kernel_services/ast_data/annotations.ml
index 57dce2e0e7c..e1d697bb238 100644
--- a/src/kernel_services/ast_data/annotations.ml
+++ b/src/kernel_services/ast_data/annotations.ml
@@ -685,13 +685,13 @@ let fold_behaviors f =
let fold_complete f =
fold_spec_gen
(fun s -> s.spec_complete_behaviors)
- (fun f l acc -> List.fold_left (Extlib.swap f) acc l)
+ (fun f l acc -> List.fold_left (Fun.flip f) acc l)
f
let fold_disjoint f =
fold_spec_gen
(fun s -> s.spec_disjoint_behaviors)
- (fun f l acc -> List.fold_left (Extlib.swap f) acc l)
+ (fun f l acc -> List.fold_left (Fun.flip f) acc l)
f
let fold_terminates f =
@@ -710,15 +710,15 @@ let fold_bhv_gen get fold f kf b acc =
let fold_requires f =
fold_bhv_gen (fun b -> b.b_requires)
- (fun f l acc -> List.fold_left (Extlib.swap f) acc l) f
+ (fun f l acc -> List.fold_left (Fun.flip f) acc l) f
let fold_assumes f =
fold_bhv_gen (fun b -> b.b_assumes)
- (fun f l acc -> List.fold_left (Extlib.swap f) acc l) f
+ (fun f l acc -> List.fold_left (Fun.flip f) acc l) f
let fold_ensures f =
fold_bhv_gen (fun b -> b.b_post_cond)
- (fun f l acc -> List.fold_left (Extlib.swap f) acc l) f
+ (fun f l acc -> List.fold_left (Fun.flip f) acc l) f
let fold_assigns f =
fold_filter_generic WritesAny
@@ -730,7 +730,7 @@ let fold_allocates f =
let fold_extended f =
fold_bhv_gen (fun b -> b.b_extended)
- (fun f l acc -> List.fold_left (Extlib.swap f) acc l) f
+ (fun f l acc -> List.fold_left (Fun.flip f) acc l) f
(* remove_code_annot is called when adding a code annotation that must
stay unique for a given combination of statement, active behaviors and
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index da5b7ec3866..df68d08f122 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -6627,7 +6627,7 @@ let rec free_vars_term bound_vars t = match t.term_node with
Logic_var.Set.empty t
| Tlambda(prms,expr) ->
let bound_vars =
- List.fold_left (Extlib.swap Logic_var.Set.add) bound_vars prms
+ List.fold_left (Fun.flip Logic_var.Set.add) bound_vars prms
in
free_vars_term bound_vars expr
| Trange(i1,i2) ->
@@ -6753,7 +6753,7 @@ and free_vars_predicate bound_vars p = match p.pred_content with
| Pforall (lvs,p) | Pexists (lvs,p) ->
let new_bv =
List.fold_left
- (Extlib.swap Logic_var.Set.add) bound_vars lvs
+ (Fun.flip Logic_var.Set.add) bound_vars lvs
in
free_vars_predicate new_bv p
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 7f19c90190b..a5e6dcd4a17 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -1582,7 +1582,7 @@ module Remove_spurious = struct
then acc
else begin
let known_li =
- List.fold_left (Extlib.swap Logic_info.Set.add) acc.logic_infos lis
+ List.fold_left (Fun.flip Logic_info.Set.add) acc.logic_infos lis
in
{ acc with
kept = g::acc.kept;
diff --git a/src/libraries/stdlib/extlib.ml b/src/libraries/stdlib/extlib.ml
index 3ce87a10aa6..301f71af912 100644
--- a/src/libraries/stdlib/extlib.ml
+++ b/src/libraries/stdlib/extlib.ml
@@ -68,8 +68,6 @@ let mk_fun s = ref (fun _ -> mk_labeled_fun s)
let ($) f g x = f (g x)
-let swap f x y = f y x
-
let uncurry f x = f (fst x) (snd x)
let iter_uncurry2 iter f v =
diff --git a/src/libraries/stdlib/extlib.mli b/src/libraries/stdlib/extlib.mli
index e407168776d..2173d5cf200 100644
--- a/src/libraries/stdlib/extlib.mli
+++ b/src/libraries/stdlib/extlib.mli
@@ -62,9 +62,6 @@ val mk_fun: string -> ('a -> 'b) ref
val ($) : ('b -> 'c) -> ('a -> 'b) -> 'a -> 'c
(** Composition. *)
-val swap: ('a -> 'b -> 'c) -> 'b -> 'a -> 'c
-(** Swap arguments. *)
-
val uncurry: ('a -> 'b -> 'c) -> ('a * 'b) -> 'c
val iter_uncurry2:
--
GitLab