Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455565758596061626364656667686970717273747576777879(************************************************************************)(* * 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) *)(************************************************************************)
type t = string
type char63 = Uint63.t
(* Maximum length on a 32-bits system. *)let max_length_int : int = 16777211
let max_length : Uint63.t = Uint63.of_int max_length_int
let to_string : t -> string = fun s -> s
let of_string : string -> t option = fun s -> if String.length s <= max_length_int then Some s else None
(* Return a string of size [max_length] if the parameter is too large. Use [c land 255] if [c] is not a valid character. *)let make : Uint63.t -> char63 -> t = fun i c -> let i = Uint63.to_int_min i max_length_int in let c = Uint63.l_and c (Uint63.of_int 255) in let c = Char.chr (Uint63.to_int_min c 255) in String.make i c
let length : t -> Uint63.t = fun s -> Uint63.of_int (String.length s)
(* Out of bound access gives '\x00'. *)let get : t -> Uint63.t -> char63 = fun s i -> let i = Uint63.to_int_min i max_length_int in if i < String.length s then Uint63.of_int (Char.code (String.get s i)) else Uint63.zero
(* Returns an empty string if the [off] is out of bounds. If the [off] is in bounds, but there are less than [len] characters from this offset, the full suffix from [off] is returned. *)let sub : t -> Uint63.t -> Uint63.t -> t = fun s off len -> let off = Uint63.to_int_min off max_int in let len = Uint63.to_int_min len max_int in let len_s = String.length s in if off < len_s then String.sub s off (min len (len_s - off)) else ""
(* Only the longest possible prefix of [s2] is used, so that the resulting string satisfies the maximum length constraint. *)let cat : t -> t -> t = fun s1 s2 -> let len1 = String.length s1 in let len2 = String.length s2 in if len1 + len2 <= max_length_int then s1 ^ s2 else s1 ^ String.sub s2 0 (max_length_int - len1)
let compare : t -> t -> int = String.compare
let equal : t -> t -> bool = String.equal
let hash : t -> int = Hashtbl.hash
let unsafe_of_string : string -> t = fun s -> s
let compile : t -> string = Printf.sprintf "Pstring.unsafe_of_string %S"