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

include module type of List

(** {6 Equality, testing} *)

val compare : 'a cmp -> 'a list cmp
(** Lexicographic order on lists. *)

val equal : 'a eq -> 'a list eq
(** Lift equality to list type. *)

val is_empty : 'a list -> bool
(** Check whether a list is empty *)

val mem_f : 'a eq -> 'a -> 'a list -> bool
(** Same as [List.mem], for some specific equality *)

val for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool
(** Same as [List.for_all] but with an index *)

val for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
(** Same as [List.for_all2] but returning [false] when of different length *)

val exists_i : (int -> 'a -> bool) -> int -> 'a list -> bool
(** Same as [List.exists] but with an index *)

val prefix_of : 'a eq -> 'a list eq
(** [prefix_of eq l1 l2] returns [true] if [l1] is a prefix of [l2], [false]
    otherwise. It uses [eq] to compare elements *)

val same_length : 'a list -> 'b list -> bool
(** A more efficient variant of [for_all2eq (fun _ _ -> true)] *)

(** {6 Creating lists} *)

val interval : int -> int -> int list
(** [interval i j] creates the list [[i; i + 1; ...; j]], or [[]] when
    [j < i]. *)

val make : int -> 'a -> 'a list
(** [make n x] returns a list made of [n] times [x]. Raise
    [Invalid_argument _] if [n] is negative. *)

val addn : int -> 'a -> 'a list -> 'a list
(** [addn n x l] adds [n] times [x] on the left of [l]. *)

val init : int -> (int -> 'a) -> 'a list
(** [init n f] constructs the list [f 0; ... ; f (n - 1)]. Raise
    [Invalid_argument _] if [n] is negative *)

val append : 'a list -> 'a list -> 'a list
(** Like OCaml's [List.append] but tail-recursive. *)

val concat : 'a list list -> 'a list
(** Like OCaml's [List.concat] but tail-recursive. *)

val flatten : 'a list list -> 'a list
(** Synonymous of [concat] *)

(** {6 Lists as arrays} *)

val assign : 'a list -> int -> 'a -> 'a list
(** [assign l i x] sets the [i]-th element of [l] to [x], starting
    from [0]. Raise [Failure _] if [i] is out of range. *)

(** {6 Filtering} *)

val filter : ('a -> bool) -> 'a list -> 'a list
(** Like OCaml [List.filter] but tail-recursive and physically returns
    the original list if the predicate holds for all elements. *)

val filter2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
(** Like [List.filter] but with 2 arguments, raise [Invalid_argument _]
    if the lists are not of same length. *)

val filteri : (int -> 'a -> bool) -> 'a list -> 'a list
(** Like [List.filter] but with an index starting from [0] *)

val filter_with : bool list -> 'a list -> 'a list
(** [filter_with bl l] selects elements of [l] whose corresponding element in
    [bl] is [true]. Raise [Invalid_argument _] if sizes differ. *)

val map_filter : ('a -> 'b option) -> 'a list -> 'b list
(** Like [map] but keeping only non-[None] elements *)

val map_filter_i : (int -> 'a -> 'b option) -> 'a list -> 'b list
(** Like [map_filter] but with an index starting from [0] *)

val partitioni : (int -> 'a -> bool) -> 'a list -> 'a list * 'a list
(** Like [List.partition] but with an index starting from [0] *)

(** {6 Applying functorially} *)

val map : ('a -> 'b) -> 'a list -> 'b list
(** Like OCaml [List.map] but tail-recursive *)

val map2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
(** Like OCaml [List.map2] but tail-recursive *)

val map_left : ('a -> 'b) -> 'a list -> 'b list
(** As [map] but ensures the left-to-right order of evaluation. *)

val concat_map : ('a -> 'b list) -> 'a list -> 'b list
(** Like OCaml [List.concat_map] but tail-recursive. Alternatively,
    the composition of [concat] and [map] *)

val map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list
(** Like OCaml [List.mapi] but tail-recursive. Alternatively, like
    [map] but with an index *)

val map2_i :
  (int -> 'a -> 'b -> 'c) -> int -> 'a list -> 'b list -> 'c list
(** Like [map2] but with an index *)

val map3 :
  ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
(** Like [map] but for 3 lists. *)

val map4 : ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list ->
  'd list -> 'e list
(** Like [map] but for 4 lists. *)

val map_until : ('a -> 'b option) -> 'a list -> 'b list * 'a list
(** [map_until f l] applies f to the elements of l until one returns None,
    then returns the list of elements where f was applied
    and the tail where f was not applied *)

val map_of_array : ('a -> 'b) -> 'a array -> 'b list
(** [map_of_array f a] behaves as [List.map f (Array.to_list a)] *)

val map_append : ('a -> 'b list) -> 'a list -> 'b list
(** [map_append f [x1; ...; xn]] returns [f x1 @ ... @ f xn]. *)

val map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list
(** Like [map_append] but for two lists; raises [Invalid_argument _]
    if the two lists do not have the same length. *)

val extend : bool list -> 'a -> 'a list -> 'a list
(** [extend l a [a1..an]] assumes that the number of [true] in [l] is [n];
    it extends [a1..an] by inserting [a] at the position of [false] in [l] *)

val count : ('a -> bool) -> 'a list -> int
(** Count the number of elements satisfying a predicate *)

(** {6 Finding position} *)

val index : 'a eq -> 'a -> 'a list -> int
(** [index] returns the 1st index of an element in a list (counting from 1). *)

val index_opt : 'a eq -> 'a -> 'a list -> int option
(** [index_opt] returns the 1st index of an element in a list (counting from 1)
    and None otherwise. *)

val index0 : 'a eq -> 'a -> 'a list -> int
(** [index0] behaves as [index] except that it starts counting at 0. *)

(** {6 Folding} *)

val fold_left_until : ('c -> 'a -> 'c CSig.until) -> 'c -> 'a list -> 'c
(** acts like [fold_left f acc s] while [f] returns
    [Cont acc']; it stops returning [c] as soon as [f] returns [Stop c]. *)

val fold_right_i :  (int -> 'a -> 'b -> 'b) -> int -> 'a list -> 'b -> 'b
(** Like [List.fold_right] but with an index *)

val fold_left_i :  (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a
(** Like [List.fold_left] but with an index *)

val fold_right_and_left : ('b -> 'a -> 'a list -> 'b) -> 'a list -> 'b -> 'b
(** [fold_right_and_left f [a1;...;an] hd] is
    [f (f (... (f (f hd an [an-1;...;a1]) an-1 [an-2;...;a1]) ...) a2 [a1]) a1 []] *)

val fold_left3 : ('a -> 'b -> 'c -> 'd -> 'a) -> 'a -> 'b list -> 'c list -> 'd list -> 'a
(** Like [List.fold_left] but for 3 lists; raise [Invalid_argument _] if
    not all lists of the same size *)

val fold_left4 : ('a -> 'b -> 'c -> 'd -> 'e -> 'a) -> 'a -> 'b list -> 'c list -> 'd list -> 'e list -> 'a
(** Like [List.fold_left] but for 4 lists; raise [Invalid_argument _] if
    not all lists of the same size *)

val fold_left2_set : exn -> ('a -> 'b -> 'c -> 'b list -> 'c list -> 'a) -> 'a -> 'b list -> 'c list -> 'a
(** Fold sets, i.e. lists up to order; the folding function tells
    when elements match by returning a value and raising the given
    exception otherwise; sets should have the same size; raise the
    given exception if no pairing of the two sets is found;;
    complexity in O(n^2) *)

val fold_left_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
(** [fold_left_map f e_0 [a1;...;an]] is [e_n,[k_1...k_n]]
    where [(e_i,k_i)] is [f e_{i-1} ai] for each i<=n *)

val fold_right_map : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
(** Same, folding on the right *)

val fold_left2_map : ('a -> 'b -> 'c -> 'a * 'd) -> 'a -> 'b list -> 'c list -> 'a * 'd list
(** Same with two lists, folding on the left *)

val fold_right2_map : ('b -> 'c -> 'a -> 'd * 'a) -> 'b list -> 'c list -> 'a -> 'd list * 'a
(** Same with two lists, folding on the right *)

val fold_left3_map : ('a -> 'b -> 'c -> 'd -> 'a * 'e) -> 'a -> 'b list -> 'c list -> 'd list -> 'a * 'e list
(** Same with three lists, folding on the left *)

val fold_left4_map : ('a -> 'b -> 'c -> 'd -> 'e -> 'a * 'r) -> 'a -> 'b list -> 'c list -> 'd list -> 'e list -> 'a * 'r list
(** Same with four lists, folding on the left *)

val fold_left5_map : ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'a * 'r) -> 'a -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'a * 'r list
(** Same with five lists, folding on the left *)

(** {6 Splitting} *)

val remove : 'a eq -> 'a -> 'a list -> 'a list
(** [remove eq a l] Remove all occurrences of [a] in [l] *)

val remove_first : ('a -> bool) -> 'a list -> 'a list
(** Remove the first element satisfying a predicate, or raise [Not_found] *)

val extract_first : ('a -> bool) -> 'a list -> 'a list * 'a
(** Remove and return the first element satisfying a predicate,
    or raise [Not_found] *)

val find_map : ('a -> 'b option) -> 'a list -> 'b option
(** [find_map f l] applies [f] to the elements of [l] in order,
    and returns the first result of the form [Some v], or [None]
    if none exist.

    In stdlib since OCaml 4.10.0
*)

val find_map_exn : ('a -> 'b option) -> 'a list -> 'b
(** Like [find_map] but raises [Not_found] instead of returning [None]. *)

exception IndexOutOfRange
val goto: int -> 'a list -> 'a list * 'a list
(** [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]. *)

val split_when : ('a -> bool) -> 'a list -> 'a list * 'a list
(** [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. *)

val sep_first : 'a list -> 'a * 'a list
(** [sep_first l] returns [(a,l')] such that [l] is [a::l'].
    It raises [Failure _] if the list is empty. *)

val sep_last : 'a list -> 'a * 'a list
(** [sep_last l] returns [(a,l')] such that [l] is [l'@[a]].
    It raises [Failure _] if the list is empty. *)

val drop_last : 'a list -> 'a list
(** Remove the last element of the list. It raises [Failure _] if the
    list is empty. This is the second part of [sep_last]. *)

val last : 'a list -> 'a
(** Return the last element of the list. It raises [Failure _] if the
    list is empty. This is the first part of [sep_last]. *)

val lastn : int -> 'a list -> 'a list
(** [lastn n l] returns the [n] last elements of [l]. It raises
    [Failure _] if [n] is less than 0 or larger than the length of [l] *)

val chop : int -> 'a list -> 'a list * 'a list
(** [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]. *)

val firstn : int -> 'a list -> 'a list
(** [firstn n l] Returns the [n] first elements of [l]. It raises
    [Failure _] if [n] negative or too large. This is the first part
    of [chop]. *)

val skipn : int -> 'a list -> 'a list
(** [skipn n l] drops the [n] first elements of [l]. It raises
    [Failure _] if [n] is less than 0 or larger than the length of [l].
    This is the second part of [chop]. *)

val skipn_at_best : int -> 'a list -> 'a list
(** Same as [skipn] but returns [] if [n] is larger than the length of
    the list. *)

val drop_prefix : 'a eq -> 'a list -> 'a list -> 'a list
(** [drop_prefix eq l1 l] returns [l2] if [l=l1++l2] else return [l]. *)

val insert : 'a eq -> 'a -> 'a list -> 'a list
(** Insert at the (first) position so that if the list is ordered wrt to the
    total order given as argument, the order is preserved *)

val share_tails : 'a eq -> 'a list -> 'a list -> 'a list * 'a list * 'a list
(** [share_tails l1 l2] returns [(l1',l2',l)] such that [l1] is
    [l1'\@l] and [l2] is [l2'\@l] and [l] is maximal amongst all such
    decompositions *)

(** {6 Association lists} *)

val map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list
(** Applies a function on the codomain of an association list *)

val assoc_f : 'a eq -> 'a -> ('a * 'b) list -> 'b
(** Like [List.assoc] but using the equality given as argument *)

val assoc_f_opt : 'a eq -> 'a -> ('a * 'b) list -> 'b option
(** Like [List.assoc_opt] but using the equality given as argument *)

val remove_assoc_f : 'a eq -> 'a -> ('a * 'b) list -> ('a * 'b) list
(** Remove first matching element; unchanged if no such element *)

val mem_assoc_f : 'a eq -> 'a -> ('a * 'b) list -> bool
(** Like [List.mem_assoc] but using the equality given as argument *)

val factorize_left : 'a eq -> ('a * 'b) list -> ('a * 'b list) list
(** Create a list of associations from a list of pairs *)

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

val split : ('a * 'b) list -> 'a list * 'b list
(** Like OCaml's [List.split] but tail-recursive. *)

val combine : 'a list -> 'b list -> ('a * 'b) list
(** Like OCaml's [List.combine] but tail-recursive. *)

val split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list
(** Like [split] but for triples *)

val split4 : ('a * 'b * 'c * 'd) list -> 'a list * 'b list * 'c list * 'd list
(** Like [split] but for quads *)

val combine3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list
(** Like [combine] but for triples *)

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

val add_set : 'a eq -> 'a -> 'a list -> 'a list
(** [add_set x l] adds [x] in [l] if it is not already there, or returns [l]
    otherwise. *)

val eq_set : 'a eq -> 'a list eq
(** Test equality up to permutation. It respects multiple occurrences
    and thus works also on multisets. *)

val subset : 'a list eq
(** Tell if a list is a subset of another up to permutation. It expects
    each element to occur only once. *)

val merge_set : 'a cmp -> 'a list -> 'a list -> 'a list
(** Merge two sorted lists and preserves the uniqueness property. *)

val intersect : 'a eq -> 'a list -> 'a list -> 'a list
(** Return the intersection of two lists, assuming and preserving
    uniqueness of elements *)

val union : 'a eq -> 'a list -> 'a list -> 'a list
(** Return the union of two lists, assuming and preserving
    uniqueness of elements *)

val unionq : 'a list -> 'a list -> 'a list
(** [union] specialized to physical equality *)

val subtract : 'a eq -> 'a list -> 'a list -> 'a list
(** Remove from the first list all elements from the second list. *)

val subtractq : 'a list -> 'a list -> 'a list
(** [subtract] specialized to physical equality *)

(** {6 Uniqueness and duplication} *)

val distinct : 'a list -> bool
(** Return [true] if all elements of the list are distinct. *)

val distinct_f : 'a cmp -> 'a list -> bool
(** Like [distinct] but using the equality given as argument *)

val duplicates : 'a eq -> 'a list -> 'a list
(** Return the list of unique elements which appear at least twice. Elements
    are kept in the order of their first appearance. *)

val uniquize_key : ('a -> 'b) -> 'a list -> 'a list
(** Return the list of elements without duplicates using the
    function to associate a comparison key to each element.
    This is the list unchanged if there was none. *)

val uniquize : 'a list -> 'a list
(** Return the list of elements without duplicates.
    This is the list unchanged if there was none. *)

val sort_uniquize : 'a cmp -> 'a list -> 'a list
(** Return a sorted version of a list without duplicates
    according to some comparison function. *)

val min : 'a cmp -> 'a list -> 'a
(** Return minimum element according to some comparison function.

    @raise Not_found on an empty list. *)

(** {6 Cartesian product} *)

val cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
(** A generic binary 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 cartesians : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b list
(** [cartesians op init l] is an n-ary cartesian product: it builds
    the list of all [op a1 .. (op an init) ..] for [a1], ..., [an] in
    the product of the elements of the lists *)

val combinations : 'a list list -> 'a list list
(** [combinations l] returns the list of [n_1] * ... * [n_p] tuples
    [[a11;...;ap1];...;[a1n_1;...;apn_pd]] whenever [l] is a list
    [[a11;..;a1n_1];...;[ap1;apn_p]]; otherwise said, it is
    [cartesians (::) [] l] *)

val cartesians_filter :
  ('a -> 'b -> 'b option) -> 'b -> 'a list list -> 'b list
(** Like [cartesians op init l] but keep only the tuples for which
    [op] returns [Some _] on all the elements of the tuple. *)

(** When returning a list of same type as the input, maximally
    shares the suffix of the output which is physically equal to the
    corresponding suffix of the input *)
module Smart :
sig
  val map : ('a -> 'a) -> 'a list -> 'a list
  (** Like [List.map] but sharing with the input the longest suffix
      of the output which is physically the same as the input; in
      particular, [Smart.map f l == l] (physically) if [f a == a]
      (physically) for all members of the list *)

  val fold_left_map : ('a -> 'b -> 'a * 'b) -> 'a -> 'b list -> 'a * 'b list
  (** Idem for the second argument of [List.fold_left_map f e l]
      relatively to the second argument of [f] *)

  val fold_right_map : ('b -> 'a -> 'b * 'a) -> 'b list -> 'a -> 'b list * 'a
  (** Idem for the first argument of [List.fold_right_map f l e]
      relatively to the second argument of [f] *)
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