aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/cList.ml
diff options
context:
space:
mode:
Diffstat (limited to 'lib/cList.ml')
-rw-r--r--lib/cList.ml889
1 files changed, 0 insertions, 889 deletions
diff --git a/lib/cList.ml b/lib/cList.ml
deleted file mode 100644
index 0ef7c3d8b..000000000
--- a/lib/cList.ml
+++ /dev/null
@@ -1,889 +0,0 @@
-(***********************************************************************)
-(* 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 *)
-(***********************************************************************)
-
-type 'a cmp = 'a -> 'a -> int
-type 'a eq = 'a -> 'a -> bool
-
-module type S = module type of List
-
-module type ExtS =
-sig
- include S
- val compare : 'a cmp -> 'a list cmp
- val equal : 'a eq -> 'a list eq
- val is_empty : 'a list -> bool
- val init : int -> (int -> 'a) -> 'a list
- val mem_f : 'a eq -> 'a -> 'a list -> bool
- val add_set : 'a eq -> 'a -> 'a list -> 'a list
- val eq_set : 'a eq -> 'a list -> 'a list -> bool
- val intersect : 'a eq -> 'a list -> 'a list -> 'a list
- val union : 'a eq -> 'a list -> 'a list -> 'a list
- val unionq : 'a list -> 'a list -> 'a list
- val subtract : 'a eq -> 'a list -> 'a list -> 'a list
- val subtractq : 'a list -> 'a list -> 'a list
- val interval : int -> int -> int list
- val make : int -> 'a -> 'a list
- val assign : 'a list -> int -> 'a -> 'a list
- val distinct : 'a list -> bool
- val distinct_f : 'a cmp -> 'a list -> bool
- val duplicates : 'a eq -> '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 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 filteri :
- (int -> 'a -> bool) -> 'a list -> 'a list
- val partitioni :
- (int -> 'a -> bool) -> 'a list -> 'a list * 'a list
- val map_of_array : ('a -> 'b) -> 'a array -> 'b list
- val smartfilter : ('a -> bool) -> 'a list -> 'a list
- val extend : bool list -> 'a -> 'a list -> 'a list
- val count : ('a -> bool) -> 'a list -> int
- val index : 'a eq -> 'a -> 'a list -> int
- val index0 : 'a eq -> 'a -> 'a list -> int
- val iteri : (int -> 'a -> unit) -> 'a list -> unit
- val fold_left_until : ('c -> 'a -> 'c CSig.until) -> 'c -> 'a list -> 'c
- 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 eq -> 'a -> 'a list -> 'a list
- val remove : 'a eq -> 'a -> 'a list -> 'a list
- val remove_first : ('a -> bool) -> 'a list -> 'a list
- val extract_first : ('a -> bool) -> 'a list -> 'a list * 'a
- val insert : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list
- val for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
- val sep_last : 'a list -> 'a * 'a list
- val find_map : ('a -> 'b option) -> 'a list -> 'b
- val uniquize : 'a list -> 'a list
- val sort_uniquize : 'a cmp -> 'a list -> 'a list
- 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
- exception IndexOutOfRange
- val goto : int -> 'a list -> 'a list * 'a list
- val split_when : ('a -> bool) -> 'a list -> 'a list * 'a list
- val split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c 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 eq -> 'a list -> 'a list -> bool
- val drop_prefix : 'a eq -> 'a list -> 'a list -> 'a list
- val drop_last : 'a list -> 'a list
- val map_append : ('a -> 'b list) -> 'a list -> 'b list
- 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
- val fold_left_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
- val fold_right_map : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
- val fold_left2_map : ('a -> 'b -> 'c -> 'a * 'd) -> 'a -> 'b list -> 'c list -> 'a * 'd list
- val fold_right2_map : ('b -> 'c -> 'a -> 'd * 'a) -> 'b list -> 'c list -> 'a -> 'd list * 'a
- val fold_left3_map : ('a -> 'b -> 'c -> 'd -> 'a * 'e) -> 'a -> 'b list -> 'c list -> 'd list -> 'a * 'e list
- val fold_left4_map : ('a -> 'b -> 'c -> 'd -> 'e -> 'a * 'r) -> 'a -> 'b list -> 'c list -> 'd list -> 'e list -> 'a * 'r list
- 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 eq -> 'a -> ('a * 'b) list -> 'b
- val remove_assoc_f : 'a eq -> 'a -> ('a * 'b) list -> ('a * 'b) list
- val mem_assoc_f : 'a eq -> 'a -> ('a * 'b) list -> bool
- val cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
- val cartesians : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b list
- val combinations : 'a list list -> 'a list list
- val combine3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list
- val cartesians_filter :
- ('a -> 'b -> 'b option) -> 'b -> 'a list list -> 'b list
- val factorize_left : 'a eq -> ('a * 'b) list -> ('a * 'b list) list
-
- module type MonoS = sig
- type elt
- val equal : elt list -> elt list -> bool
- val mem : elt -> elt list -> bool
- val assoc : elt -> (elt * 'a) list -> 'a
- val mem_assoc : elt -> (elt * 'a) list -> bool
- val remove_assoc : elt -> (elt * 'a) list -> (elt * 'a) list
- val mem_assoc_sym : elt -> ('a * elt) list -> bool
- end
-
-end
-
-include List
-
-(** Tail-rec implementation of usual functions. This is a well-known trick used
- in, for instance, ExtLib and Batteries. *)
-
-type 'a cell = {
- head : 'a;
- mutable tail : 'a list;
-}
-
-external cast : 'a cell -> 'a list = "%identity"
-
-let rec map_loop f p = function
-| [] -> ()
-| x :: l ->
- let c = { head = f x; tail = [] } in
- p.tail <- cast c;
- map_loop f c l
-
-let map f = function
-| [] -> []
-| x :: l ->
- let c = { head = f x; tail = [] } in
- map_loop f c l;
- cast c
-
-let rec map2_loop f p l1 l2 = match l1, l2 with
-| [], [] -> ()
-| x :: l1, y :: l2 ->
- let c = { head = f x y; tail = [] } in
- p.tail <- cast c;
- map2_loop f c l1 l2
-| _ -> invalid_arg "List.map2"
-
-let map2 f l1 l2 = match l1, l2 with
-| [], [] -> []
-| x :: l1, y :: l2 ->
- let c = { head = f x y; tail = [] } in
- map2_loop f c l1 l2;
- cast c
-| _ -> invalid_arg "List.map2"
-
-let rec map_of_array_loop f p a i l =
- if Int.equal i l then ()
- else
- let c = { head = f (Array.unsafe_get a i); tail = [] } in
- p.tail <- cast c;
- map_of_array_loop f c a (i + 1) l
-
-let map_of_array f a =
- let l = Array.length a in
- if Int.equal l 0 then []
- else
- let c = { head = f (Array.unsafe_get a 0); tail = [] } in
- map_of_array_loop f c a 1 l;
- cast c
-
-let rec append_loop p tl = function
-| [] -> p.tail <- tl
-| x :: l ->
- let c = { head = x; tail = [] } in
- p.tail <- cast c;
- append_loop c tl l
-
-let append l1 l2 = match l1 with
-| [] -> l2
-| x :: l ->
- let c = { head = x; tail = [] } in
- append_loop c l2 l;
- cast c
-
-let rec copy p = function
-| [] -> p
-| x :: l ->
- let c = { head = x; tail = [] } in
- p.tail <- cast c;
- copy c l
-
-let rec init_loop len f p i =
- if Int.equal i len then ()
- else
- let c = { head = f i; tail = [] } in
- p.tail <- cast c;
- init_loop len f c (succ i)
-
-let init len f =
- if len < 0 then invalid_arg "List.init"
- else if Int.equal len 0 then []
- else
- let c = { head = f 0; tail = [] } in
- init_loop len f c 1;
- cast c
-
-let rec concat_loop p = function
-| [] -> ()
-| x :: l -> concat_loop (copy p x) l
-
-let concat l =
- let dummy = { head = Obj.magic 0; tail = [] } in
- concat_loop dummy l;
- dummy.tail
-
-let flatten = concat
-
-let rec split_loop p q = function
-| [] -> ()
-| (x, y) :: l ->
- let cl = { head = x; tail = [] } in
- let cr = { head = y; tail = [] } in
- p.tail <- cast cl;
- q.tail <- cast cr;
- split_loop cl cr l
-
-let split = function
-| [] -> [], []
-| (x, y) :: l ->
- let cl = { head = x; tail = [] } in
- let cr = { head = y; tail = [] } in
- split_loop cl cr l;
- (cast cl, cast cr)
-
-let rec combine_loop p l1 l2 = match l1, l2 with
-| [], [] -> ()
-| x :: l1, y :: l2 ->
- let c = { head = (x, y); tail = [] } in
- p.tail <- cast c;
- combine_loop c l1 l2
-| _ -> invalid_arg "List.combine"
-
-let combine l1 l2 = match l1, l2 with
-| [], [] -> []
-| x :: l1, y :: l2 ->
- let c = { head = (x, y); tail = [] } in
- combine_loop c l1 l2;
- cast c
-| _ -> invalid_arg "List.combine"
-
-let rec filter_loop f p = function
-| [] -> ()
-| x :: l ->
- if f x then
- let c = { head = x; tail = [] } in
- let () = p.tail <- cast c in
- filter_loop f c l
- else
- filter_loop f p l
-
-let filter f l =
- let c = { head = Obj.magic 0; tail = [] } in
- filter_loop f c l;
- c.tail
-
-(** FIXME: Already present in OCaml 4.00 *)
-
-let rec map_i_loop f i p = function
-| [] -> ()
-| x :: l ->
- let c = { head = f i x; tail = [] } in
- p.tail <- cast c;
- map_i_loop f (succ i) c l
-
-let map_i f i = function
-| [] -> []
-| x :: l ->
- let c = { head = f i x; tail = [] } in
- map_i_loop f (succ i) c l;
- cast c
-
-(** Extensions of OCaml Stdlib *)
-
-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 is_empty = function
-| [] -> true
-| _ -> false
-
-let mem_f cmp x l = List.exists (cmp x) l
-
-let intersect cmp l1 l2 =
- filter (fun x -> mem_f cmp x l2) l1
-
-let union cmp l1 l2 =
- let rec urec = function
- | [] -> l2
- | a::l -> if mem_f cmp a l2 then urec l else a::urec l
- in
- urec l1
-
-let subtract cmp l1 l2 =
- if is_empty l2 then l1
- else List.filter (fun x -> not (mem_f cmp x l2)) l1
-
-let unionq l1 l2 = union (==) l1 l2
-let subtractq l1 l2 = subtract (==) l1 l2
-
-let interval n m =
- let rec interval_n (l,m) =
- if n > m then l else interval_n (m::l, pred m)
- in
- interval_n ([], m)
-
-let addn n v =
- let rec aux n l =
- if Int.equal 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 l i = match l, i with
- | ((h::t), 0) -> List.rev_append stk (e :: t)
- | ((h::t), n) -> assrec (h :: stk) t (pred n)
- | ([], _) -> 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 = map
-
-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 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 rec extend l a l' = match l,l' with
- | true::l, b::l' -> b :: extend l a l'
- | false::l, l' -> a :: extend l a l'
- | [], [] -> []
- | _ -> invalid_arg "extend"
-
-let count f l =
- let rec aux acc = function
- | [] -> acc
- | h :: t -> if f h then aux (acc + 1) t else aux acc t in
- aux 0 l
-
-let rec index_f f x l n = match l with
-| [] -> raise Not_found
-| y :: l -> if f x y then n else index_f f x l (succ n)
-
-let index f x l = index_f f x l 1
-
-let index0 f x l = index_f f x l 0
-
-let fold_left_until f accu s =
- let rec aux accu = function
- | [] -> accu
- | x :: xs -> match f accu x with CSig.Stop x -> x | CSig.Cont i -> aux i xs in
- aux accu s
-
-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"
-
-let rec fold_left4 f accu l1 l2 l3 l4 =
- match (l1, l2, l3, l4) with
- ([], [], [], []) -> accu
- | (a1::l1, a2::l2, a3::l3, a4::l4) -> fold_left4 f (f accu a1 a2 a3 a4) l1 l2 l3 l4
- | (_,_, _, _) -> invalid_arg "List.fold_left4"
-
-(* [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 iteri 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 cmp x l = List.filter (fun y -> not (cmp x y)) l
-
-let remove = except (* Alias *)
-
-let rec remove_first p = function
- | b::l when p b -> l
- | b::l -> b::remove_first p l
- | [] -> raise Not_found
-
-let extract_first p li =
- let rec loop rev_left = function
- | [] -> raise Not_found
- | x::right ->
- if p x then List.rev_append rev_left right, x
- else loop (x :: rev_left) right
- in loop [] li
-
-let insert p v l =
- let rec insrec = function
- | [] -> [v]
- | h::tl -> if p v h then v::h::tl else h::insrec tl
- in
- insrec l
-
-let add_set cmp x l = if mem_f cmp x l then l else x :: l
-
-(** List equality up to permutation (but considering multiple occurrences) *)
-
-let eq_set cmp l1 l2 =
- let rec aux l1 = function
- | [] -> is_empty l1
- | a::l2 -> aux (remove_first (cmp 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 filteri 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 partitioni p =
- let rec aux i = function
- | [] -> [], []
- | x :: l ->
- let (l1, l2) = aux (succ i) l in
- if p i x then (x :: l1, l2)
- else (l1, x :: l2)
- in aux 0
-
-let rec sep_last = function
- | [] -> failwith "sep_last"
- | hd::[] -> (hd,[])
- | hd::tl -> let (l,tl) = sep_last tl in (l,hd::tl)
-
-let rec find_map f = function
-| [] -> raise Not_found
-| x :: l ->
- match f x with
- | None -> find_map f l
- | Some y -> y
-
-(* FIXME: we should avoid relying on the generic hash function,
- just as we'd better avoid Pervasives.compare *)
-
-let uniquize l =
- let visited = Hashtbl.create 23 in
- let rec aux acc changed = function
- | h::t -> if Hashtbl.mem visited h then aux acc true t else
- begin
- Hashtbl.add visited h h;
- aux (h::acc) changed t
- end
- | [] -> if changed then List.rev acc else l
- in aux [] false l
-
-(** [sort_uniquize] might be an alternative to the hashtbl-based
- [uniquize], when the order of the elements is irrelevant *)
-
-let rec uniquize_sorted cmp = function
- | a::b::l when Int.equal (cmp a b) 0 -> uniquize_sorted cmp (a::l)
- | a::l -> a::uniquize_sorted cmp l
- | [] -> []
-
-let sort_uniquize cmp l = uniquize_sorted cmp (List.sort cmp l)
-
-(* FIXME: again, generic hash function *)
-
-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 distinct_f cmp l =
- let rec loop = function
- | a::b::_ when Int.equal (cmp a b) 0 -> false
- | a::l -> loop l
- | [] -> true
- in loop (List.sort cmp 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 Int.equal 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 cmp = function
- | [] -> []
- | x::l ->
- let l' = duplicates cmp l in
- if mem_f cmp x l then add_set cmp x l' else l'
-
-let rec filter2_loop f p q l1 l2 = match l1, l2 with
-| [], [] -> ()
-| x :: l1, y :: l2 ->
- if f x y then
- let c1 = { head = x; tail = [] } in
- let c2 = { head = y; tail = [] } in
- let () = p.tail <- cast c1 in
- let () = q.tail <- cast c2 in
- filter2_loop f c1 c2 l1 l2
- else
- filter2_loop f p q l1 l2
-| _ -> invalid_arg "List.filter2"
-
-let filter2 f l1 l2 =
- let c1 = { head = Obj.magic 0; tail = [] } in
- let c2 = { head = Obj.magic 0; tail = [] } in
- filter2_loop f c1 c2 l1 l2;
- (c1.tail, c2.tail)
-
-let rec map_filter_loop f p = function
- | [] -> ()
- | x :: l ->
- match f x with
- | None -> map_filter_loop f p l
- | Some y ->
- let c = { head = y; tail = [] } in
- p.tail <- cast c;
- map_filter_loop f c l
-
-let map_filter f l =
- let c = { head = Obj.magic 0; tail = [] } in
- map_filter_loop f c l;
- c.tail
-
-let rec map_filter_i_loop f i p = function
- | [] -> ()
- | x :: l ->
- match f i x with
- | None -> map_filter_i_loop f (succ i) p l
- | Some y ->
- let c = { head = y; tail = [] } in
- p.tail <- cast c;
- map_filter_i_loop f (succ i) c l
-
-let map_filter_i f l =
- let c = { head = Obj.magic 0; tail = [] } in
- map_filter_i_loop f 0 c l;
- c.tail
-
-let rec filter_with filter l = match filter, l with
-| [], [] -> []
-| true :: filter, x :: l -> x :: filter_with filter l
-| false :: filter, _ :: l -> filter_with filter l
-| _ -> invalid_arg "List.filter_with"
-
-(* FIXME: again, generic hash function *)
-
-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
-
-(** [goto i l] splits [l] into two lists [(l1,l2)] such that
- [(List.rev l1)++l2=l] and [l1] has length [i]. It raises
- [IndexOutOfRange] when [i] is negative or greater than the
- length of [l]. *)
-exception IndexOutOfRange
-let goto n l =
- let rec goto i acc = function
- | tl when Int.equal i 0 -> (acc, tl)
- | h::t -> goto (pred i) (h::acc) t
- | [] -> raise IndexOutOfRange
- in
- goto n [] l
-
-(* [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 =
- try let (h,t) = goto n l in (List.rev h,t)
- with IndexOutOfRange -> failwith "List.chop"
- (* spiwack: should raise [IndexOutOfRange] but I'm afraid of missing
- a try/with when replacing the exception. *)
-
-(* [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 []
-
-let rec split3 = function
- | [] -> ([], [], [])
- | (x,y,z)::l ->
- let (rx, ry, rz) = split3 l in (x::rx, y::ry, z::rz)
-
-let firstn n l =
- let rec aux acc n l =
- match n, l with
- | 0, _ -> 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 Int.equal 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 cmp prefl l =
- let rec prefrec = function
- | (h1::t1, h2::t2) -> cmp h1 h2 && prefrec (t1,t2)
- | ([], _) -> true
- | _ -> false
- in
- prefrec (prefl,l)
-
-(** if [l=p++t] then [drop_prefix p l] is [t] else [l] *)
-
-let drop_prefix cmp p l =
- let rec drop_prefix_rec = function
- | (h1::tp, h2::tl) when cmp h1 h2 -> drop_prefix_rec (tp,tl)
- | ([], tl) -> tl
- | _ -> l
- in
- drop_prefix_rec (p,l)
-
-let map_append f l = List.flatten (List.map f l)
-
-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)
-
-(* Poor man's monadic map *)
-let rec fold_left_map f e = function
- | [] -> (e,[])
- | h::t ->
- let e',h' = f e h in
- let e'',t' = fold_left_map f e' t in
- e'',h'::t'
-
-let fold_map = fold_left_map
-
-(* (* 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_right_map f l e =
- List.fold_right (fun x (l,e) -> let (y,e) = f x e in (y::l,e)) l ([],e)
-
-let fold_map' = fold_right_map
-
-let on_snd f (x,y) = (x,f y)
-
-let fold_left2_map f e l l' =
- on_snd List.rev @@
- List.fold_left2 (fun (e,l) x x' ->
- let (e,y) = f e x x' in
- (e, y::l)
- ) (e, []) l l'
-
-let fold_right2_map f l l' e =
- List.fold_right2 (fun x x' (l,e) -> let (y,e) = f x x' e in (y::l,e)) l l' ([],e)
-
-let fold_left3_map f e l l' l'' =
- on_snd List.rev @@
- fold_left3 (fun (e,l) x x' x'' -> let (e,y) = f e x x' x'' in (e,y::l)) (e,[]) l l' l''
-
-let fold_left4_map f e l1 l2 l3 l4 =
- on_snd List.rev @@
- fold_left4 (fun (e,l) x1 x2 x3 x4 -> let (e,y) = f e x1 x2 x3 x4 in (e,y::l)) (e,[]) l1 l2 l3 l4
-
-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
-
-let remove_assoc_f f a l =
- try remove_first (fun (x,_) -> f a x) l with Not_found -> l
-
-let mem_assoc_f f a l = List.exists (fun (x,_) -> f a x) 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
- | _, _, _ -> invalid_arg "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 cmp = function
- | (a,b)::l ->
- let al,l' = partition (fun (a',_) -> cmp a a') l in
- (a,(b::List.map snd al)) :: factorize_left cmp l'
- | [] -> []
-
-module type MonoS = sig
- type elt
- val equal : elt list -> elt list -> bool
- val mem : elt -> elt list -> bool
- val assoc : elt -> (elt * 'a) list -> 'a
- val mem_assoc : elt -> (elt * 'a) list -> bool
- val remove_assoc : elt -> (elt * 'a) list -> (elt * 'a) list
- val mem_assoc_sym : elt -> ('a * elt) list -> bool
-end
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 15:21:06 +0000