Quelle pstring.ml Sprache: SML

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

quality99%

¤ Dauer der Verarbeitung: 0.22 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.