Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869(************************************************************************)(* * 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) *)(************************************************************************)
(** Primitive [string] type. *)
type t = private string
type char63 = Uint63.t
val max_length_int : intval max_length : Uint63.t
(** [to_string s] converts the primitive string [s] into a standard string. *)val to_string : t -> string
(** [of_string s] converts string [s] into a primitive string if its size does not exceed [max_length_int], and returns [None] otherwise. *)val of_string : string -> t option
(** [make i c] returns a string of size [min i max_length] containing only the character with code [c l_and 255]. *)val make : Uint63.t -> char63 -> t
(** [length s] gives the length of string [s]. *)val length : t -> Uint63.t
(** [get s i] gives the code of the character stored at index [i] in [s]. When index [i] is invalid, the function returns zero. *)val get : t -> Uint63.t -> char63
(** [sub s off len] returns the substring of [s] starting at offset [off], and of length [len], when possible. If [off] is not a valid offset in [s], the empty string is returned. If [off] is a valid offset, the function returns the longest possible suffix of [s] that: (1) starts at [off], and (2) does not have more than [len] characters. *)val sub : t -> Uint63.t -> Uint63.t -> t
(** [cat s1 s2] returns the concatenation of [s1] and of the longest prefix of [s2] such that the sum of their lengths does not exceed [max_length]. *)val cat : t -> t -> t
(** [compare s1 s2] returns [0] if [s1] and [s2] are equal, a number less than [0] if [s1] is smaller than [s2], and a number greater than [0] if [s1] is greater than [s2]. *)val compare : t -> t -> int
(** [equal s1 s2] indicates whether [s1] and [s2] are equal. *)val equal : t -> t -> bool
(** [hash s] gives a hash of [s], with the same value as [Hashtbl.hash s]. *)val hash : t -> int
(** [unsafe_of_string s] converts [s] into a primitive string without checking whether its size satisfies the length constraint. Callers of this function must ensure that [length s <= max_length_int], which is always the case if [s] was obtained via [to_string]. NOTE: this function is used in generated code, via [compile]. *)val unsafe_of_string : string -> t
(** [compile s] outputs an OCaml expression producing primitive string [s]. *)val compile : t -> string