diff --git a/src/libraries/stdlib/transitioning.ml.in b/src/libraries/stdlib/transitioning.ml.in index 676dc9b6fa4483a8132c3939540f520efd3df9dc..18f57b5196e274749cb4cec156755ad5906757ce 100644 --- a/src/libraries/stdlib/transitioning.ml.in +++ b/src/libraries/stdlib/transitioning.ml.in @@ -20,3 +20,14 @@ (* *) (**************************************************************************) +module List = struct + + let concat_map f l = + let rec aux f acc = function + | [] -> List.rev acc + | x :: l -> + let xs = f x in + aux f (List.rev_append xs acc) l + in aux f [] l + +end diff --git a/src/libraries/stdlib/transitioning.mli b/src/libraries/stdlib/transitioning.mli index 415b987eba7c80bb120dcf25dc0d9a1687ade500..e838d35296fbf19e045a2dc483b9c57594bc22c1 100644 --- a/src/libraries/stdlib/transitioning.mli +++ b/src/libraries/stdlib/transitioning.mli @@ -32,3 +32,8 @@ *) (** {1 OCaml} *) + +module List: sig + (** since 4.10.0 *) + val concat_map: ('a -> 'b list) -> 'a list -> 'b list +end diff --git a/src/plugins/value/partitioning/partition.ml b/src/plugins/value/partitioning/partition.ml index 47476096e816545ed6f7da392a5bcb34b7050579..4af621c4009d47b7ce15aa6d9947d4cdb4cf5fbb 100644 --- a/src/plugins/value/partitioning/partition.ml +++ b/src/plugins/value/partitioning/partition.ml @@ -388,8 +388,7 @@ struct None end - let split_state ~monitor (term : split_term) - (key : key) (state : state) : (key * state) list = + let split_state ~monitor term (key, state) : (key * state) list = try let update_key (v, x) = { key with splits = SplitMap.add term v key.splits }, x @@ -403,31 +402,28 @@ struct with Operation_failed -> [(key,state)] let split ~monitor (kind : split_kind) (term : split_term) (p : t) = - let add_split acc (key,state) = + let add_split (key, state) = let dynamic_splits = match kind with | Static -> SplitMap.remove term key.dynamic_splits | Dynamic -> SplitMap.add term monitor key.dynamic_splits in let key = { key with dynamic_splits } in - split_state ~monitor term key state @ acc + split_state ~monitor term (key, state) in - List.fold_left add_split [] p + Transitioning.List.concat_map add_split p let update_dynamic_splits p = (* Update one state *) - let update_state acc (key,state) = + let update_state (key, state) = (* Split the states in the list l for the given exp *) - let update_exp exp monitor l = - let resplit acc (k,x) = - split_state ~monitor exp k x @ acc - in - List.fold_left resplit [] l + let update_exp term monitor l = + Transitioning.List.concat_map (split_state ~monitor term) l in (* Foreach exp in original state: split *) - SplitMap.fold update_exp key.dynamic_splits [(key,state)] @ acc + SplitMap.fold update_exp key.dynamic_splits [(key,state)] in - List.fold_left update_state [] p + Transitioning.List.concat_map update_state p let map_keys (f : key -> state -> key) (p : t) : t = List.map (fun (k,x) -> f k x, x) p