Source file cList.ml

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

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 mem_f : 'a eq -> 'a -> 'a list -> bool
  val for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool
  val for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
  val exists_i : (int -> 'a -> bool) -> int -> 'a list -> bool
  val prefix_of : 'a eq -> 'a list -> 'a list -> bool
  val same_length : 'a list -> 'b list -> bool
  val interval : int -> int -> int list
  val make : int -> 'a -> 'a list
  val addn : int -> 'a -> 'a list -> 'a list
  val init : int -> (int -> 'a) -> 'a list
  val append : 'a list -> 'a list -> 'a list
  val concat : 'a list list -> 'a list
  val flatten : 'a list list -> 'a list
  val assign : 'a list -> int -> 'a -> 'a list
  val filter : ('a -> bool) -> 'a list -> 'a list
  val filter2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
  val filteri :
    (int -> 'a -> bool) -> 'a list -> 'a list
  val filter_with : bool list -> 'a list -> 'a list
  val map_filter : ('a -> 'b option) -> 'a list -> 'b list
  val map_filter_i : (int -> 'a -> 'b option) -> 'a list -> 'b list
  val partitioni :
    (int -> 'a -> bool) -> 'a list -> 'a list * 'a list
  val map : ('a -> 'b) -> 'a list -> 'b list
  val map2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c 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_of_array : ('a -> 'b) -> 'a array -> 'b 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 extend : bool list -> 'a -> 'a list -> 'a list
  val count : ('a -> bool) -> 'a list -> int
  val index : 'a eq -> 'a -> 'a list -> int
  val safe_index : 'a eq -> 'a -> 'a list -> int option
  val index0 : 'a eq -> 'a -> 'a list -> int
  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 fold_left2_set : exn -> ('a -> 'b -> 'c -> 'b list -> 'c list -> 'a) -> 'a -> 'b list -> 'c list -> 'a
  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 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 find_map : ('a -> 'b option) -> 'a list -> 'b
  exception IndexOutOfRange
  val goto : int -> 'a list -> 'a list * 'a list
  val split_when : ('a -> bool) -> 'a list -> 'a list * 'a list
  val sep_last : 'a list -> 'a * 'a list
  val drop_last : 'a list -> 'a list
  val last : 'a list -> 'a
  val lastn : int -> 'a list -> 'a list
  val chop : int -> 'a list -> 'a list * 'a list
  val firstn : int -> 'a list -> 'a list
  val skipn : int -> 'a list -> 'a list
  val skipn_at_least : int -> 'a list -> 'a list
  val drop_prefix : 'a eq -> 'a list -> 'a list -> 'a list
  val insert : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list
  val share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list
  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 factorize_left : 'a eq -> ('a * 'b) list -> ('a * 'b list) list
  val split : ('a * 'b) list -> 'a list * 'b list
  val combine : 'a list -> 'b list -> ('a * 'b) list
  val split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list
  val split4 : ('a * 'b * 'c * 'd) list -> 'a list * 'b list * 'c list * 'd list
  val combine3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list
  val add_set : 'a eq -> 'a -> 'a list -> 'a list
  val eq_set : 'a eq -> 'a list -> 'a list -> bool
  val subset : 'a list -> 'a list -> bool
  val merge_set : 'a cmp -> 'a list -> 'a list -> 'a list
  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 distinct : 'a list -> bool
  val distinct_f : 'a cmp -> 'a list -> bool
  val duplicates : 'a eq -> 'a list -> 'a list
  val uniquize_key : ('a -> 'b) -> 'a list -> 'a list
  val uniquize : 'a list -> 'a list
  val sort_uniquize : 'a cmp -> 'a list -> 'a list
  val min : 'a cmp -> 'a list -> 'a
  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 cartesians_filter :
    ('a -> 'b -> 'b option) -> 'b -> 'a list list -> 'b list

  module Smart :
  sig
    val map : ('a -> 'a) -> 'a list -> 'a list
  end

  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"

(** Extensions and redefinitions of OCaml Stdlib *)

(** {6 Equality, testing} *)

let rec same_length l1 l2 = match l1, l2 with
| [], [] -> true
| _ :: l1, _ :: l2 -> same_length l1 l2
| ([], _ :: _) | (_ :: _, []) -> false

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 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 for_all2eq f l1 l2 =
  try List.for_all2 f l1 l2 with Invalid_argument _ -> false

let exists_i p =
  let rec exists_p i = function
    | [] -> false
    | a::l -> p i a || exists_p (i+1) l
  in
  exists_p

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)

(** {6 Creating lists} *)

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 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 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 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

(** {6 Lists as arrays} *)

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

(** {6 Filtering} *)

let rec filter_loop f p = function
  | [] -> ()
  | x :: l' as l ->
    let b = f x in
    filter_loop f p l';
    if b then if p.tail == l' then p.tail <- l else p.tail <- x :: p.tail

let rec filter f = function
  | [] -> []
  | x :: l' as l ->
    if f x then
      let c = { head = x; tail = [] } in
      filter_loop f c l';
      if c.tail == l' then l else cast c
    else
      filter f l'

let rec filter2_loop f p q l1 l2 = match l1, l2 with
  | [], [] -> ()
  | x :: l1', y :: l2' ->
    let b = f x y in
    filter2_loop f p q l1' l2';
    if b then
      if p.tail == l1' then begin
          p.tail <- l1;
          q.tail <- l2
        end
      else begin
          p.tail <- x :: p.tail;
          q.tail <- y :: q.tail
        end
  | _ -> invalid_arg "List.filter2"

let rec filter2 f l1 l2 = match l1, l2 with
  | [], [] -> ([],[])
  | x1 :: l1', x2 :: l2' ->
    let b = f x1 x2 in
    if b then
      let c1 = { head = x1; tail = [] } in
      let c2 = { head = x2; tail = [] } in
      filter2_loop f c1 c2 l1' l2';
      if c1.tail == l1' then (l1, l2) else (cast c1, cast c2)
    else
      filter2 f l1' l2'
  | _ -> invalid_arg "List.filter2"

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 rec filter_with_loop filter p l = match filter, l with
  | [], [] -> ()
  | b :: filter, x :: l' ->
    filter_with_loop filter p l';
    if b then if p.tail == l' then p.tail <- l else p.tail <- x :: p.tail
  | _ -> invalid_arg "List.filter_with"

let rec filter_with filter l = match filter, l with
  | [], [] -> []
  | b :: filter, x :: l' ->
    if b then
      let c = { head = x; tail = [] } in
      filter_with_loop filter c l';
      if c.tail == l' then l else cast c
    else filter_with filter l'
  | _ -> invalid_arg "List.filter_with"

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 rec map_filter f = function
  | [] -> []
  | x :: l' ->
    match f x with
    | None -> map_filter f l'
    | Some y ->
      let c = { head = y; tail = [] } in
      map_filter_loop f c l';
      cast c

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 rec map_filter_i_loop' f i = function
  | [] -> []
  | x :: l' ->
    match f i x with
    | None -> map_filter_i_loop' f (succ i) l'
    | Some y ->
      let c = { head = y; tail = [] } in
      map_filter_i_loop f (succ i) c l';
      cast c

let map_filter_i f l =
  map_filter_i_loop' f 0 l

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

(** {6 Applying functorially} *)

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"

(** Like OCaml [List.mapi] but tail-recursive *)

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

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 rec map3_loop f p l1 l2 l3 = match l1, l2, l3 with
  | [], [], [] -> ()
  | x :: l1, y :: l2, z :: l3 ->
    let c = { head = f x y z; tail = [] } in
    p.tail <- cast c;
    map3_loop f c l1 l2 l3
  | _ -> invalid_arg "List.map3"

let map3 f l1 l2 l3 = match l1, l2, l3 with
  | [], [], [] -> []
  | x :: l1, y :: l2, z :: l3 ->
    let c = { head = f x y z; tail = [] } in
    map3_loop f c l1 l2 l3;
    cast c
  | _ -> invalid_arg "List.map3"

let rec map4_loop f p l1 l2 l3 l4 = match l1, l2, l3, l4 with
  | [], [], [], [] -> ()
  | x :: l1, y :: l2, z :: l3, t :: l4 ->
    let c = { head = f x y z t; tail = [] } in
    p.tail <- cast c;
    map4_loop f c l1 l2 l3 l4
  | _ -> invalid_arg "List.map4"

let map4 f l1 l2 l3 l4 = match l1, l2, l3, l4 with
  | [], [], [], [] -> []
  | x :: l1, y :: l2, z :: l3, t :: l4 ->
    let c = { head = f x y z t; tail = [] } in
    map4_loop f c l1 l2 l3 l4;
    cast c
  | _ -> invalid_arg "List.map4"

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 map_append f l = flatten (map f l)

let map_append2 f l1 l2 = flatten (map2 f l1 l2)

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

(** {6 Finding position} *)

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 safe_index f x l = try Some (index f x l) with Not_found -> None

let index0 f x l = index_f f x l 0

(** {6 Folding} *)

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

(* Match sets as lists according to a matching function, also folding a side effect *)
let rec fold_left2_set e f x l1 l2 =
  match l1 with
  | a1 :: l1 ->
      let rec find seen = function
        | [] -> raise e
        | a2 :: l2 ->
            try fold_left2_set e f (f x a1 a2 l1 l2) l1 (List.rev_append seen l2)
            with e' when e' = e -> find (a2 :: seen) l2 in
      find [] l2
  | [] ->
      if l2 = [] then x else raise e

(* 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'

(* (* tail-recursive version of the above function *)
let fold_left_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 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

(** {6 Splitting} *)

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 rec find_map f = function
  | [] -> raise Not_found
  | x :: l ->
    match f x with
    | None -> find_map f l
    | Some y -> y

(* 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 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 sep_last = function
  | [] -> failwith "sep_last"
  | hd :: [] -> (hd,[])
  | hd :: tl -> let (l,tl) = sep_last tl in (l,hd :: tl)

(* Drop the last element of a list *)

let rec drop_last = function
  | [] -> failwith "drop_last"
  | hd :: [] -> []
  | hd :: tl -> hd :: drop_last tl

let rec last = function
  | [] -> failwith "List.last"
  | hd :: [] -> hd
  | _ :: tl -> last tl

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 _ when n >= 0 -> []

(** 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 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)

(** {6 Association lists} *)

let map_assoc f = 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

(** {6 Operations on lists of tuples} *)

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 split3_loop p q r = function
  | [] -> ()
  | (x, y, z) :: l ->
    let cp = { head = x; tail = [] } in
    let cq = { head = y; tail = [] } in
    let cr = { head = z; tail = [] } in
    p.tail <- cast cp;
    q.tail <- cast cq;
    r.tail <- cast cr;
    split3_loop cp cq cr l

let split3 = function
  | [] -> [], [], []
  | (x, y, z) :: l ->
    let cp = { head = x; tail = [] } in
    let cq = { head = y; tail = [] } in
    let cr = { head = z; tail = [] } in
    split3_loop cp cq cr l;
    (cast cp, cast cq, cast cr)

(** XXX TODO tailrec *)
let rec split4 = function
  | [] -> ([], [], [], [])
  | (a,b,c,d)::l ->
      let (ra, rb, rc, rd) = split4 l in (a::ra, b::rb, c::rc, d::rd)

let rec combine3_loop p l1 l2 l3 = match l1, l2, l3 with
  | [], [], [] -> ()
  | x :: l1, y :: l2, z :: l3 ->
    let c = { head = (x, y, z); tail = [] } in
    p.tail <- cast c;
    combine3_loop c l1 l2 l3
  | _ -> invalid_arg "List.combine3"

let combine3 l1 l2 l3 = match l1, l2, l3 with
  | [], [], [] -> []
  | x :: l1, y :: l2, z :: l3 ->
    let c = { head = (x, y, z); tail = [] } in
    combine3_loop c l1 l2 l3;
    cast c
  | _ -> invalid_arg "List.combine3"

(** {6 Operations on lists seen as sets, preserving uniqueness of elements} *)

(** Add an element, preserving uniqueness of elements *)

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 rec merge_set 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_set cmp t1 t2
    else if c <= 0
    then h1 :: merge_set cmp t1 l2
    else h2 :: merge_set cmp l1 t2

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

(** {6 Uniqueness and duplication} *)

(* FIXME: we should avoid relying on the generic hash function,
   just as we'd better avoid Pervasives.compare *)

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)

(* FIXME: again, generic hash function *)

let uniquize_key f l =
  let visited = Hashtbl.create 23 in
  let rec aux acc changed = function
    | h :: t ->
        let x = f h in
        if Hashtbl.mem visited x then aux acc true t else
          begin
            Hashtbl.add visited x x;
            aux (h :: acc) changed t
          end
    | [] -> if changed then List.rev acc else l
  in
  aux [] false l

let uniquize l = uniquize_key (fun x -> x) 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)

let min cmp l =
  let rec aux cur = function
    | [] -> cur
    | x :: l -> if cmp x cur < 0 then aux x l else aux cur l
  in
  match l with
  | x :: l -> aux x l
  | [] -> raise Not_found

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'

(** {6 Cartesian product} *)

(* 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 -> 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

(* 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]

(* 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 :: map snd al)) :: factorize_left cmp l'
  | [] -> []

module Smart =
struct

  let rec map f l = match l with
  | [] -> l
  | h :: tl ->
    let h' = f h in
    let tl' = map f tl in
    if h' == h && tl' == tl then l else h' :: tl'

end

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