Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165(************************************************************************)(* * 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 * 'cval on_snd : ('a -> 'b) -> 'c * 'a -> 'c * 'bval 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 * 'dval on_pi2 : ('a -> 'b) -> 'c * 'a * 'd -> 'c * 'b * 'dval on_pi3 : ('a -> 'b) -> 'c * 'd * 'a -> 'c * 'd * 'b
(** {6 Projections from triplets } *)
val pi1 : 'a * 'b * 'c -> 'aval pi2 : 'a * 'b * 'c -> 'bval pi3 : 'a * 'b * 'c -> 'c
(** {6 Chars. } *)
val is_letter : char -> boolval is_digit : char -> boolval is_ident_tail : char -> boolval is_blank : char -> bool
(** {6 Empty type} *)
module Empty :sig type t val abort : t -> 'aend
(** {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 = CList
val (@) : 'a list -> 'a list -> 'a list
(** {6 Arrays. } *)
module Array = CArray
(** {6 Sets. } *)
module Set = CSet
(** {6 Maps. } *)
module Map = 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 -> 'aval iterate : ('a -> 'a) -> int -> 'a -> 'aval repeat : int -> ('a -> unit) -> 'a -> unitval 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
val protect_ref : scope:(unit -> 'a) -> 'b ref -> 'a
val protect_state : freeze:(unit -> 'st) -> unfreeze:('st ->unit) -> scope:(unit -> 'a) -> 'a
val atomify : ('a -> 'b) -> 'a -> 'b
(** {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 -> 'cend
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 *)