diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/util.ml | 10 | ||||
| -rw-r--r-- | lib/util.mli | 1 |
2 files changed, 10 insertions, 1 deletions
diff --git a/lib/util.ml b/lib/util.ml index c4229fd322..e6c76f7f3d 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -699,7 +699,7 @@ let list_split_when p = split_when_loop [] (* [list_split_by p l] splits [l] into two lists [(l1,l2)] such that elements of - [l1] satisfy [p] and elements of [l2] do not *) + [l1] satisfy [p] and elements of [l2] do not; order is preserved *) let list_split_by p = let rec split_by_loop = function | [] -> ([],[]) @@ -858,6 +858,14 @@ let rec list_cartesians_filter op init ll = let rec list_drop_last = function [] -> assert false | hd :: [] -> [] | hd :: tl -> hd :: list_drop_last tl +(* Factorize lists of pairs according to the left argument *) +let rec list_factorize_left = function + | (a,b)::l -> + let al,l' = list_split_by (fun (a',b) -> a=a') l in + (a,(b::List.map snd al)) :: list_factorize_left l' + | [] -> + [] + (* Arrays *) let array_compare item_cmp v1 v2 = diff --git a/lib/util.mli b/lib/util.mli index 868a76711c..37d15792f2 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -191,6 +191,7 @@ val list_cartesians_filter : ('a -> 'b -> 'b option) -> 'b -> 'a list list -> 'b list val list_union_map : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b +val list_factorize_left : ('a * 'b) list -> ('a * 'b list) list (** {6 Arrays. } *) |