package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file pstring.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq 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"
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct