(************************************************************************)
(*         *      The Rocq Prover / The Rocq 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)         *)
(************************************************************************)

(** This module contains numerous utility functions on strings, lists,
   arrays, etc. *)

(** Mapping under pairs *)

val on_fst : ('a -> 'b) -> 'a * 'c -> 'b * 'c
val on_snd : ('a -> 'b) -> 'c * 'a -> 'c * 'b
val map_pair : ('a -> 'b) -> 'a * 'a -> 'b * 'b

(** Folding under pairs *)

val fold_fst : ('c -> 'a -> 'c * 'a) -> 'c -> 'a * 'b -> 'c * ('a * 'b)
val fold_snd : ('c -> 'b -> 'c * 'b) -> 'c -> 'a * 'b -> 'c * ('a * 'b)

(** Equality on pairs *)

val eq_pair : ('a -> 'a -> bool) -> ('b -> 'b -> bool) -> ('a * 'b -> 'a * 'b -> bool)

(** Mapping under triplets *)

val on_pi1 : ('a -> 'b) -> 'a * 'c * 'd -> 'b * 'c * 'd
val on_pi2 : ('a -> 'b) -> 'c * 'a * 'd -> 'c * 'b * 'd
val on_pi3 : ('a -> 'b) -> 'c * 'd * 'a -> 'c * 'd * 'b

(** {6 Projections from triplets } *)

val pi1 : 'a * 'b * 'c -> 'a
val pi2 : 'a * 'b * 'c -> 'b
val pi3 : 'a * 'b * 'c -> 'c

(** {6 Chars. } *)

val is_letter : char -> bool
val is_digit : char -> bool
val is_ident_tail : char -> bool
val is_blank : char -> bool

(** {6 Empty type} *)

module Empty :
sig
  type t
  val abort : t -> 'a
end

(** {6 Strings. } *)

module String = CString

(** Substitute %s in the first chain by the second chain *)
val subst_command_placeholder : string -> string -> string

(** {6 Lists. } *)

module List : module type of CList

val (@) : 'a list -> 'a list -> 'a list

(** {6 Arrays. } *)

module Array : CArray.ExtS

(** {6 Sets. } *)

module Set : module type of CSet

(** {6 Maps. } *)

module Map : module type of CMap

(** {6 Matrices. } *)

val matrix_transpose : 'a list list -> 'a list list

(** {6 Functions. } *)

val identity : 'a -> 'a

(** Left-to-right function composition:

    [f1 %> f2] is [fun x -> f2 (f1 x)].

    [f1 %> f2 %> f3] is [fun x -> f3 (f2 (f1 x))].

    [f1 %> f2 %> f3 %> f4] is [fun x -> f4 (f3 (f2 (f1 x)))]

    etc.
*)
val ( %> ) : ('a -> 'b) -> ('b -> 'c) -> 'a -> 'c

val const : 'a -> 'b -> 'a
val iterate : ('a -> 'a) -> int -> 'a -> 'a
val repeat : int -> ('a -> unit) -> 'a -> unit
val app_opt : ('a -> 'a) option -> 'a -> 'a

(** {6 Delayed computations. } *)

type 'a delayed = unit -> 'a

val delayed_force : 'a delayed -> 'a

(** [try_finally f x g y] applies the main code [f] to [x] and
   returns the result after having applied the finalization
   code [g] to [y]. If the main code raises the exception
   [exn], the finalization code is executed and [exn] is raised.
   If the finalization code itself fails, the exception
   returned is always the one from the finalization code.
   Credit X.Leroy, D.Remy. *)
val try_finally: ('a -> 'b) -> 'a -> ('c -> unit) -> 'c -> 'b

(** {6 Enriched exceptions} *)

type iexn = Exninfo.iexn
[@@ocaml.deprecated "(8.12) please use [Exninfo.iexn]"]

val iraise : Exninfo.iexn -> 'a
[@@ocaml.deprecated "(8.12) please use [Exninfo.iraise]"]

(** {6 Misc. } *)

type ('a, 'b) union = ('a, 'b) CSig.union = Inl of 'a | Inr of 'b
(** Union type *)

module Union :
sig
  val map : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) union -> ('c, 'd) union
  val equal : ('a -> 'a -> bool) -> ('b -> 'b -> bool) -> ('a, 'b) union -> ('a, 'b) union -> bool
  val fold_left : ('c -> 'a -> 'c) -> ('c -> 'b -> 'c) -> 'c -> ('a, 'b) union -> 'c
end

val map_union : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) union -> ('c, 'd) union
(** Alias for [Union.map] *)

type 'a until = 'a CSig.until = Stop of 'a | Cont of 'a
(** Used for browsable-until structures. *)

type ('a, 'b) eq = ('a, 'b) CSig.eq = Refl : ('a, 'a) eq

val sym : ('a, 'b) eq -> ('b, 'a) eq

(** Helpers to write comparison functions *)
module Compare : sig
  type list = [] | (::) : (('a -> 'a -> int) * 'a * 'a) * list -> list

  val compare : list -> int
  (** Compare the elements in the order they are given using the
      provided comparison function until the first non-zero result. *)
end

val open_utf8_file_in : string -> in_channel
(** Open an utf-8 encoded file and skip the byte-order mark if any. *)

val set_temporary_memory : unit -> ('a -> 'a) * (unit -> 'a)
(** A trick which can typically be used to store on the fly the
   computation of values in the "when" clause of a "match" then
   retrieve the evaluated result in the r.h.s of the clause *)
