diff options
Diffstat (limited to 'lib/cList.ml')
| -rw-r--r-- | lib/cList.ml | 718 |
1 files changed, 718 insertions, 0 deletions
diff --git a/lib/cList.ml b/lib/cList.ml new file mode 100644 index 000000000..e3f35dcac --- /dev/null +++ b/lib/cList.ml @@ -0,0 +1,718 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +module type S = +sig + val length : 'a list -> int + val hd : 'a list -> 'a + val tl : 'a list -> 'a list + val nth : 'a list -> int -> 'a + val rev : 'a list -> 'a list + val append : 'a list -> 'a list -> 'a list + val rev_append : 'a list -> 'a list -> 'a list + val concat : 'a list list -> 'a list + val flatten : 'a list list -> 'a list + val iter : ('a -> unit) -> 'a list -> unit + val map : ('a -> 'b) -> 'a list -> 'b list + val rev_map : ('a -> 'b) -> 'a list -> 'b list + val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a + val fold_right : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b + val iter2 : ('a -> 'b -> unit) -> 'a list -> 'b list -> unit + val map2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list + val rev_map2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list + val fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b list -> 'c list -> 'a + val fold_right2 : ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c + val for_all : ('a -> bool) -> 'a list -> bool + val exists : ('a -> bool) -> 'a list -> bool + val for_all2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool + val exists2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool + val mem : 'a -> 'a list -> bool + val memq : 'a -> 'a list -> bool + val find : ('a -> bool) -> 'a list -> 'a + val filter : ('a -> bool) -> 'a list -> 'a list + val find_all : ('a -> bool) -> 'a list -> 'a list + val partition : ('a -> bool) -> 'a list -> 'a list * 'a list + val assoc : 'a -> ('a * 'b) list -> 'b + val assq : 'a -> ('a * 'b) list -> 'b + val mem_assoc : 'a -> ('a * 'b) list -> bool + val mem_assq : 'a -> ('a * 'b) list -> bool + val remove_assoc : 'a -> ('a * 'b) list -> ('a * 'b) list + val remove_assq : 'a -> ('a * 'b) list -> ('a * 'b) list + val split : ('a * 'b) list -> 'a list * 'b list + val combine : 'a list -> 'b list -> ('a * 'b) list + val sort : ('a -> 'a -> int) -> 'a list -> 'a list + val stable_sort : ('a -> 'a -> int) -> 'a list -> 'a list + val fast_sort : ('a -> 'a -> int) -> 'a list -> 'a list + val merge : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list +end + +module type ExtS = +sig + include S + val compare : ('a -> 'a -> int) -> 'a list -> 'a list -> int + val equal : ('a -> 'a -> bool) -> 'a list -> 'a list -> bool + val add_set : 'a -> 'a list -> 'a list + val eq_set : 'a list -> 'a list -> bool + val intersect : 'a list -> 'a list -> 'a list + val union : 'a list -> 'a list -> 'a list + val unionq : 'a list -> 'a list -> 'a list + val subtract : 'a list -> 'a list -> 'a list + val subtractq : 'a list -> 'a list -> 'a list + + (** [tabulate f n] builds [[f 0; ...; f (n-1)]] *) + val tabulate : (int -> 'a) -> int -> 'a list + val make : int -> 'a -> 'a list + val assign : 'a list -> int -> 'a -> 'a list + val distinct : 'a list -> bool + val duplicates : 'a list -> 'a list + val filter2 : ('a -> 'b -> bool) -> 'a list * 'b list -> 'a list * 'b list + val map_filter : ('a -> 'b option) -> 'a list -> 'b list + val map_filter_i : (int -> 'a -> 'b option) -> 'a list -> 'b list + val filter_with : bool list -> 'a list -> 'a list + val filter_along : ('a -> bool) -> 'a list -> 'b list -> 'b list + + (** [smartmap f [a1...an] = List.map f [a1...an]] but if for all i + [ f ai == ai], then [smartmap f l==l] *) + val smartmap : ('a -> 'a) -> 'a list -> 'a list + val map_left : ('a -> 'b) -> 'a list -> 'b list + val map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list + val map2_i : + (int -> 'a -> 'b -> 'c) -> int -> 'a list -> 'b list -> 'c list + val map3 : + ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list + val map4 : + ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list + val map_to_array : ('a -> 'b) -> 'a list -> 'b array + val filter_i : + (int -> 'a -> bool) -> 'a list -> 'a list + + (** [smartfilter f [a1...an] = List.filter f [a1...an]] but if for all i + [f ai = true], then [smartfilter f l==l] *) + val smartfilter : ('a -> bool) -> 'a list -> 'a list + + (** [index] returns the 1st index of an element in a list (counting from 1) *) + val index : 'a -> 'a list -> int + val index_f : ('a -> 'a -> bool) -> 'a -> 'a list -> int + + (** [unique_index x l] returns [Not_found] if [x] doesn't occur exactly once *) + val unique_index : 'a -> 'a list -> int + + (** [index0] behaves as [index] except that it starts counting at 0 *) + val index0 : 'a -> 'a list -> int + val index0_f : ('a -> 'a -> bool) -> 'a -> 'a list -> int + val iter3 : ('a -> 'b -> 'c -> unit) -> 'a list -> 'b list -> 'c list -> unit + val iter_i : (int -> 'a -> unit) -> 'a list -> unit + val fold_right_i : (int -> 'a -> 'b -> 'b) -> int -> 'a list -> 'b -> 'b + val fold_left_i : (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a + val fold_right_and_left : + ('a -> 'b -> 'b list -> 'a) -> 'b list -> 'a -> 'a + val fold_left3 : ('a -> 'b -> 'c -> 'd -> 'a) -> 'a -> 'b list -> 'c list -> 'd list -> 'a + val for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool + val except : 'a -> 'a list -> 'a list + val remove : 'a -> 'a list -> 'a list + val remove_first : 'a -> 'a list -> 'a list + val remove_assoc_in_triple : 'a -> ('a * 'b * 'c) list -> ('a * 'b * 'c) list + val assoc_snd_in_triple : 'a -> ('a * 'b * 'c) list -> 'b + val for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool + val sep_last : 'a list -> 'a * 'a list + val try_find_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b + val try_find : ('a -> 'b) -> 'a list -> 'b + val uniquize : 'a list -> 'a list + + (** merges two sorted lists and preserves the uniqueness property: *) + val merge_uniq : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list + val subset : 'a list -> 'a list -> bool + val chop : int -> 'a list -> 'a list * 'a list + (* former [split_at] was a duplicate of [chop] *) + val split_when : ('a -> bool) -> 'a list -> 'a list * 'a list + val split_by : ('a -> bool) -> 'a list -> 'a list * 'a list + val split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list + val partition_by : ('a -> 'a -> bool) -> 'a list -> 'a list list + val firstn : int -> 'a list -> 'a list + val last : 'a list -> 'a + val lastn : int -> 'a list -> 'a list + val skipn : int -> 'a list -> 'a list + val skipn_at_least : int -> 'a list -> 'a list + val addn : int -> 'a -> 'a list -> 'a list + val prefix_of : 'a list -> 'a list -> bool + + (** [drop_prefix p l] returns [t] if [l=p++t] else return [l] *) + val drop_prefix : 'a list -> 'a list -> 'a list + val drop_last : 'a list -> 'a list + + (** [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)] *) + val map_append : ('a -> 'b list) -> 'a list -> 'b list + val join_map : ('a -> 'b list) -> 'a list -> 'b list + + (** raises [Invalid_argument] if the two lists don't have the same length *) + val map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list + val share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list + + (** [fold_map f e_0 [l_1...l_n] = e_n,[k_1...k_n]] + where [(e_i,k_i)=f e_{i-1} l_i] *) + val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list + val fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a + val map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list + val assoc_f : ('a -> 'a -> bool) -> 'a -> ('a * 'b) list -> 'b + + (** A generic cartesian product: for any operator (**), + [cartesian (**) [x1;x2] [y1;y2] = [x1**y1; x1**y2; x2**y1; x2**y1]], + and so on if there are more elements in the lists. *) + val cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list + + (** [cartesians] is an n-ary cartesian product: it iterates + [cartesian] over a list of lists. *) + val cartesians : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b list + + (** combinations [[a;b];[c;d]] returns [[a;c];[a;d];[b;c];[b;d]] *) + val combinations : 'a list list -> 'a list list + val combine3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list + + (** Keep only those products that do not return None *) + val cartesian_filter : + ('a -> 'b -> 'c option) -> 'a list -> 'b list -> 'c list + val cartesians_filter : + ('a -> 'b -> 'b option) -> 'b -> 'a list list -> 'b list + + val union_map : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b + val factorize_left : ('a * 'b) list -> ('a * 'b list) list +end + +include List + +(* Lists *) + +let rec compare cmp l1 l2 = + if l1 == l2 then 0 else + match l1,l2 with + [], [] -> 0 + | _::_, [] -> 1 + | [], _::_ -> -1 + | x1::l1, x2::l2 -> + (match cmp x1 x2 with + | 0 -> compare cmp l1 l2 + | c -> c) + +let rec equal cmp l1 l2 = + l1 == l2 || + match l1, l2 with + | [], [] -> true + | x1 :: l1, x2 :: l2 -> + cmp x1 x2 && equal cmp l1 l2 + | _ -> false + +let intersect l1 l2 = + List.filter (fun x -> List.mem x l2) l1 + +let union l1 l2 = + let rec urec = function + | [] -> l2 + | a::l -> if List.mem a l2 then urec l else a::urec l + in + urec l1 + +let unionq l1 l2 = + let rec urec = function + | [] -> l2 + | a::l -> if List.memq a l2 then urec l else a::urec l + in + urec l1 + +let subtract l1 l2 = + if l2 = [] then l1 else List.filter (fun x -> not (List.mem x l2)) l1 + +let subtractq l1 l2 = + if l2 = [] then l1 else List.filter (fun x -> not (List.memq x l2)) l1 + +let tabulate f len = + let rec tabrec n = + if n = len then [] else (f n)::(tabrec (n+1)) + in + tabrec 0 + +let addn n v = + let rec aux n l = + if n = 0 then l + else aux (pred n) (v::l) + in + if n < 0 then invalid_arg "List.addn" + else aux n + +let make n v = addn n v [] + +let assign l n e = + let rec assrec stk = function + | ((h::t), 0) -> List.rev_append stk (e::t) + | ((h::t), n) -> assrec (h::stk) (t, n-1) + | ([], _) -> failwith "List.assign" + in + assrec [] (l,n) + +let rec smartmap f l = match l with + [] -> l + | h::tl -> + let h' = f h and tl' = smartmap f tl in + if h'==h && tl'==tl then l + else h'::tl' + +let map_left f = (* ensures the order in case of side-effects *) + let rec map_rec = function + | [] -> [] + | x::l -> let v = f x in v :: map_rec l + in + map_rec + +let map_i f = + let rec map_i_rec i = function + | [] -> [] + | x::l -> let v = f i x in v :: map_i_rec (i+1) l + in + map_i_rec + +let map2_i f i l1 l2 = + let rec map_i i = function + | ([], []) -> [] + | ((h1::t1), (h2::t2)) -> let v = f i h1 h2 in v :: map_i (succ i) (t1,t2) + | (_, _) -> invalid_arg "map2_i" + in + map_i i (l1,l2) + +let map3 f l1 l2 l3 = + let rec map = function + | ([], [], []) -> [] + | ((h1::t1), (h2::t2), (h3::t3)) -> let v = f h1 h2 h3 in v::map (t1,t2,t3) + | (_, _, _) -> invalid_arg "map3" + in + map (l1,l2,l3) + +let map4 f l1 l2 l3 l4 = + let rec map = function + | ([], [], [], []) -> [] + | ((h1::t1), (h2::t2), (h3::t3), (h4::t4)) -> let v = f h1 h2 h3 h4 in v::map (t1,t2,t3,t4) + | (_, _, _, _) -> invalid_arg "map4" + in + map (l1,l2,l3,l4) + +let map_to_array f l = + Array.of_list (List.map f l) + +let rec smartfilter f l = match l with + [] -> l + | h::tl -> + let tl' = smartfilter f tl in + if f h then + if tl' == tl then l + else h :: tl' + else tl' + +let index_f f x = + let rec index_x n = function + | y::l -> if f x y then n else index_x (succ n) l + | [] -> raise Not_found + in + index_x 1 + +let index0_f f x l = index_f f x l - 1 + +let index x = + let rec index_x n = function + | y::l -> if x = y then n else index_x (succ n) l + | [] -> raise Not_found + in + index_x 1 + +let index0 x l = index x l - 1 + +let unique_index x = + let rec index_x n = function + | y::l -> + if x = y then + if List.mem x l then raise Not_found + else n + else index_x (succ n) l + | [] -> raise Not_found + in index_x 1 + +let fold_right_i f i l = + let rec it_f i l a = match l with + | [] -> a + | b::l -> f (i-1) b (it_f (i-1) l a) + in + it_f (List.length l + i) l + +let fold_left_i f = + let rec it_list_f i a = function + | [] -> a + | b::l -> it_list_f (i+1) (f i a b) l + in + it_list_f + +let rec fold_left3 f accu l1 l2 l3 = + match (l1, l2, l3) with + ([], [], []) -> accu + | (a1::l1, a2::l2, a3::l3) -> fold_left3 f (f accu a1 a2 a3) l1 l2 l3 + | (_, _, _) -> invalid_arg "List.fold_left3" + +(* [fold_right_and_left f [a1;...;an] hd = + f (f (... (f (f hd + an + [an-1;...;a1]) + an-1 + [an-2;...;a1]) + ...) + a2 + [a1]) + a1 + []] *) + +let fold_right_and_left f l hd = + let rec aux tl = function + | [] -> hd + | a::l -> let hd = aux (a::tl) l in f hd a tl + in aux [] l + +let iter3 f l1 l2 l3 = + let rec iter = function + | ([], [], []) -> () + | ((h1::t1), (h2::t2), (h3::t3)) -> f h1 h2 h3; iter (t1,t2,t3) + | (_, _, _) -> invalid_arg "map3" + in + iter (l1,l2,l3) + +let iter_i f l = fold_left_i (fun i _ x -> f i x) 0 () l + +let for_all_i p = + let rec for_all_p i = function + | [] -> true + | a::l -> p i a && for_all_p (i+1) l + in + for_all_p + +let except x l = List.filter (fun y -> not (x = y)) l + +let remove = except (* Alias *) + +let rec remove_first a = function + | b::l when a = b -> l + | b::l -> b::remove_first a l + | [] -> raise Not_found + +let rec remove_assoc_in_triple x = function + | [] -> [] + | (y,_,_ as z)::l -> if x = y then l else z::remove_assoc_in_triple x l + +let rec assoc_snd_in_triple x = function + [] -> raise Not_found + | (a,b,_)::l -> if Pervasives.compare a x = 0 then b else assoc_snd_in_triple x l + +let add_set x l = if List.mem x l then l else x::l + +let eq_set l1 l2 = + let rec aux l1 = function + | [] -> l1 = [] + | a::l2 -> aux (remove_first a l1) l2 in + try aux l1 l2 with Not_found -> false + +let for_all2eq f l1 l2 = + try List.for_all2 f l1 l2 with Invalid_argument _ -> false + +let filter_i p = + let rec filter_i_rec i = function + | [] -> [] + | x::l -> let l' = filter_i_rec (succ i) l in if p i x then x::l' else l' + in + filter_i_rec 0 + +let rec sep_last = function + | [] -> failwith "sep_last" + | hd::[] -> (hd,[]) + | hd::tl -> let (l,tl) = sep_last tl in (l,hd::tl) + +let try_find_i f = + let rec try_find_f n = function + | [] -> failwith "try_find_i" + | h::t -> try f n h with Failure _ -> try_find_f (n+1) t + in + try_find_f + +let try_find f = + let rec try_find_f = function + | [] -> failwith "try_find" + | h::t -> try f h with Failure _ -> try_find_f t + in + try_find_f + +let uniquize l = + let visited = Hashtbl.create 23 in + let rec aux acc = function + | h::t -> if Hashtbl.mem visited h then aux acc t else + begin + Hashtbl.add visited h h; + aux (h::acc) t + end + | [] -> List.rev acc + in aux [] l + +let distinct l = + let visited = Hashtbl.create 23 in + let rec loop = function + | h::t -> + if Hashtbl.mem visited h then false + else + begin + Hashtbl.add visited h h; + loop t + end + | [] -> true + in loop l + +let rec merge_uniq cmp l1 l2 = + match l1, l2 with + | [], l2 -> l2 + | l1, [] -> l1 + | h1 :: t1, h2 :: t2 -> + let c = cmp h1 h2 in + if c = 0 + then h1 :: merge_uniq cmp t1 t2 + else if c <= 0 + then h1 :: merge_uniq cmp t1 l2 + else h2 :: merge_uniq cmp l1 t2 + +let rec duplicates = function + | [] -> [] + | x::l -> + let l' = duplicates l in + if List.mem x l then add_set x l' else l' + +let rec filter2 f = function + | [], [] as p -> p + | d::dp, l::lp -> + let (dp',lp' as p) = filter2 f (dp,lp) in + if f d l then d::dp', l::lp' else p + | _ -> invalid_arg "List.filter2" + +let rec map_filter f = function + | [] -> [] + | x::l -> + let l' = map_filter f l in + match f x with None -> l' | Some y -> y::l' + +let map_filter_i f = + let rec aux i = function + | [] -> [] + | x::l -> + let l' = aux (succ i) l in + match f i x with None -> l' | Some y -> y::l' + in aux 0 + +let filter_along f filter l = + snd (filter2 (fun b c -> f b) (filter,l)) + +let filter_with filter l = + filter_along (fun x -> x) filter l + +let subset l1 l2 = + let t2 = Hashtbl.create 151 in + List.iter (fun x -> Hashtbl.add t2 x ()) l2; + let rec look = function + | [] -> true + | x::ll -> try Hashtbl.find t2 x; look ll with Not_found -> false + in + look l1 + +(* [chop i l] splits [l] into two lists [(l1,l2)] such that + [l1++l2=l] and [l1] has length [i]. + It raises [Failure] when [i] is negative or greater than the length of [l] *) + +let chop n l = + let rec chop_aux i acc = function + | tl when i=0 -> (List.rev acc, tl) + | h::t -> chop_aux (pred i) (h::acc) t + | [] -> failwith "List.chop" + in + chop_aux n [] l + +(* [split_when p l] splits [l] into two lists [(l1,a::l2)] such that + [l1++(a::l2)=l], [p a=true] and [p b = false] for every element [b] of [l1]. + If there is no such [a], then it returns [(l,[])] instead *) +let split_when p = + let rec split_when_loop x y = + match y with + | [] -> (List.rev x,[]) + | (a::l) -> if (p a) then (List.rev x,y) else split_when_loop (a::x) l + in + split_when_loop [] + +(* [split_by p l] splits [l] into two lists [(l1,l2)] such that elements of + [l1] satisfy [p] and elements of [l2] do not; order is preserved *) +let split_by p = + let rec split_by_loop = function + | [] -> ([],[]) + | a::l -> + let (l1,l2) = split_by_loop l in if p a then (a::l1,l2) else (l1,a::l2) + in + split_by_loop + +let rec split3 = function + | [] -> ([], [], []) + | (x,y,z)::l -> + let (rx, ry, rz) = split3 l in (x::rx, y::ry, z::rz) + +let rec insert_in_class f a = function + | [] -> [[a]] + | (b::_ as l)::classes when f a b -> (a::l)::classes + | l::classes -> l :: insert_in_class f a classes + +let partition_by f l = + List.fold_right (insert_in_class f) l [] + +let firstn n l = + let rec aux acc = function + | (0, l) -> List.rev acc + | (n, (h::t)) -> aux (h::acc) (pred n, t) + | _ -> failwith "firstn" + in + aux [] (n,l) + +let rec last = function + | [] -> failwith "List.last" + | [x] -> x + | _ :: l -> last l + +let lastn n l = + let len = List.length l in + let rec aux m l = + if m = n then l else aux (m - 1) (List.tl l) + in + if len < n then failwith "lastn" else aux len l + +let rec skipn n l = match n,l with + | 0, _ -> l + | _, [] -> failwith "List.skipn" + | n, _::l -> skipn (pred n) l + +let skipn_at_least n l = + try skipn n l with Failure _ -> [] + +let prefix_of prefl l = + let rec prefrec = function + | (h1::t1, h2::t2) -> h1 = h2 && prefrec (t1,t2) + | ([], _) -> true + | (_, _) -> false + in + prefrec (prefl,l) + +let drop_prefix p l = +(* if l=p++t then return t else l *) + let rec drop_prefix_rec = function + | ([], tl) -> Some tl + | (_, []) -> None + | (h1::tp, h2::tl) -> + if h1 = h2 then drop_prefix_rec (tp,tl) else None + in + match drop_prefix_rec (p,l) with + | Some r -> r + | None -> l + +let map_append f l = List.flatten (List.map f l) +let join_map = map_append (* Alias *) + +let map_append2 f l1 l2 = List.flatten (List.map2 f l1 l2) + +let share_tails l1 l2 = + let rec shr_rev acc = function + | ((x1::l1), (x2::l2)) when x1 == x2 -> shr_rev (x1::acc) (l1,l2) + | (l1,l2) -> (List.rev l1, List.rev l2, acc) + in + shr_rev [] (List.rev l1, List.rev l2) + +let rec fold_map f e = function + | [] -> (e,[]) + | h::t -> + let e',h' = f e h in + let e'',t' = fold_map f e' t in + e'',h'::t' + +(* (* tail-recursive version of the above function *) +let fold_map f e l = + let g (e,b') h = + let (e',h') = f e h in + (e',h'::b') + in + let (e',lrev) = List.fold_left g (e,[]) l in + (e',List.rev lrev) +*) + +(* The same, based on fold_right, with the effect accumulated on the right *) +let fold_map' f l e = + List.fold_right (fun x (l,e) -> let (y,e) = f x e in (y::l,e)) l ([],e) + +let map_assoc f = List.map (fun (x,a) -> (x,f a)) + +let rec assoc_f f a = function + | (x, e) :: xs -> if f a x then e else assoc_f f a xs + | [] -> raise Not_found + +(* Specification: + - =p= is set equality (double inclusion) + - f such that \forall l acc, (f l acc) =p= append (f l []) acc + - let g = fun x -> f x [] in + - union_map f l acc =p= append (flatten (map g l)) acc + *) +let union_map f l acc = + List.fold_left + (fun x y -> f y x) + acc + l + +(* A generic cartesian product: for any operator (**), + [cartesian (**) [x1;x2] [y1;y2] = [x1**y1; x1**y2; x2**y1; x2**y1]], + and so on if there are more elements in the lists. *) + +let cartesian op l1 l2 = + map_append (fun x -> List.map (op x) l2) l1 + +(* [cartesians] is an n-ary cartesian product: it iterates + [cartesian] over a list of lists. *) + +let cartesians op init ll = + List.fold_right (cartesian op) ll [init] + +(* combinations [[a;b];[c;d]] gives [[a;c];[a;d];[b;c];[b;d]] *) + +let combinations l = cartesians (fun x l -> x::l) [] l + +let rec combine3 x y z = + match x, y, z with + | [], [], [] -> [] + | (x :: xs), (y :: ys), (z :: zs) -> + (x, y, z) :: combine3 xs ys zs + | _, _, _ -> raise (Invalid_argument "List.combine3") + +(* Keep only those products that do not return None *) + +let cartesian_filter op l1 l2 = + map_append (fun x -> map_filter (op x) l2) l1 + +(* Keep only those products that do not return None *) + +let cartesians_filter op init ll = + List.fold_right (cartesian_filter op) ll [init] + +(* Drop the last element of a list *) + +let rec drop_last = function [] -> assert false | hd :: [] -> [] | hd :: tl -> hd :: drop_last tl + +(* Factorize lists of pairs according to the left argument *) +let rec factorize_left = function + | (a,b)::l -> + let al,l' = split_by (fun (a',b) -> a=a') l in + (a,(b::List.map snd al)) :: factorize_left l' + | [] -> + [] + |