Skip to content

GitLab

Commit 3bc6e61d authored by Michele Alberti's avatar Michele Alberti
Browse files

[kernel][stdlib] Remove FCBuffer and use Buffer instead.

parent edfa608c
Hide whitespace changes
Inline Side-by-side
.Makefile.lint
View file @ 3bc6e61d
......@@ -146,8 +146,6 @@ ML_LINT_KO+=src/libraries/project/state_dependency_graph.mli
ML_LINT_KO+=src/libraries/project/state_selection.ml
ML_LINT_KO+=src/libraries/project/state_selection.mli
ML_LINT_KO+=src/libraries/project/state_topological.mli
ML_LINT_KO+=src/libraries/stdlib/FCBuffer.ml
ML_LINT_KO+=src/libraries/stdlib/FCBuffer.mli
ML_LINT_KO+=src/libraries/stdlib/FCHashtbl.mli
ML_LINT_KO+=src/libraries/stdlib/FCSet.ml
ML_LINT_KO+=src/libraries/stdlib/FCSet.mli
......
Makefile
View file @ 3bc6e61d
......@@ -441,7 +441,6 @@ CMO += $(VERY_FIRST_CMO)
LIB_CMO =\
src/libraries/stdlib/transitioning \
src/libraries/stdlib/FCSet \
src/libraries/stdlib/FCBuffer \
src/libraries/stdlib/FCHashtbl \
src/libraries/stdlib/extlib \
src/libraries/datatype/unmarshal \
......
headers/header_spec.txt
View file @ 3bc6e61d
......@@ -628,8 +628,6 @@ src/libraries/project/state_selection.ml: CEA_LGPL
src/libraries/project/state_selection.mli: CEA_LGPL
src/libraries/project/state_topological.ml: MODIFIED_OCAMLGRAPH
src/libraries/project/state_topological.mli: MODIFIED_OCAMLGRAPH
src/libraries/stdlib/FCBuffer.ml: OCAML_STDLIB
src/libraries/stdlib/FCBuffer.mli: OCAML_STDLIB
src/libraries/stdlib/FCHashtbl.ml: CEA_LGPL
src/libraries/stdlib/FCHashtbl.mli: CEA_LGPL
src/libraries/stdlib/FCMap.ml: OCAML_STDLIB
......
src/libraries/stdlib/FCBuffer.ml deleted 100644 → 0
View file @ edfa608c
(*****************************************************************************)
(* *)
(* This file was originally part of Objective Caml *)
(* *)
(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *)
(* *)
(* Copyright (C) 1996 INRIA *)
(* INRIA (Institut National de Recherche en Informatique et en *)
(* Automatique) *)
(* *)
(* All rights reserved. *)
(* *)
(* This file is distributed under the terms of the GNU Library General *)
(* Public License version 2, with the special exception on linking *)
(* described below. See the GNU Library General Public License version *)
(* 2 for more details (enclosed in the file licenses/LGPLv2). *)
(* *)
(* As a special exception to the GNU Library General Public License, *)
(* you may link, statically or dynamically, a "work that uses the Library" *)
(* with a publicly distributed version of the Library to *)
(* produce an executable file containing portions of the Library, and *)
(* distribute that executable file under terms of your choice, without *)
(* any of the additional requirements listed in clause 6 of the GNU *)
(* Library General Public License. *)
(* By "a publicly distributed version of the Library", *)
(* we mean either the unmodified Library as *)
(* distributed by INRIA, or a modified version of the Library that is *)
(* distributed under the conditions defined in clause 2 of the GNU *)
(* Library General Public License. This exception does not however *)
(* invalidate any other reasons why the executable file might be *)
(* covered by the GNU Library General Public License. *)
(* *)
(* File modified by CEA (Commissariat à l'énergie atomique et aux *)
(* énergies alternatives). *)
(* *)
(*****************************************************************************)
(* Extensible buffers *)
type t =
{mutable buffer : bytes;
mutable position : int;
mutable length : int;
initial_buffer : bytes}
let create n =
let n = if n < 1 then 1 else n in
let n = if n > Sys.max_string_length then Sys.max_string_length else n in
let s = Bytes.create n in
{buffer = s; position = 0; length = n; initial_buffer = s}
let contents b = Bytes.sub_string b.buffer 0 b.position
let to_bytes b = Bytes.sub b.buffer 0 b.position
let sub b ofs len =
if ofs < 0 || len < 0 || ofs > b.position - len
then invalid_arg "Buffer.sub"
else Bytes.sub_string b.buffer ofs len
;;
let sub_bytes b ofs len =
if ofs < 0 || len < 0 || ofs > b.position - len
then invalid_arg "Buffer.sub_bytes"
else Bytes.sub b.buffer ofs len
;;
let blit src srcoff dst dstoff len =
if len < 0 || srcoff < 0 || srcoff > src.position - len
|| dstoff < 0 || dstoff > (Bytes.length dst) - len
then invalid_arg "Buffer.blit"
else
Bytes.unsafe_blit src.buffer srcoff dst dstoff len
;;
(* [calc_size cur_len req_len] computes the new size for a buffer having
[cur_len] bytes, to ensure that it can contain at least [req_len] bytes.
Used by [add_*] and [blit_*] functions.
Raise [Failure] if the new size is too large. *)
let calc_size cur_len req_len =
let new_len = ref cur_len in
while req_len > !new_len do new_len := 2 * !new_len done;
if !new_len > Sys.max_string_length then begin
if req_len <= Sys.max_string_length
then new_len := Sys.max_string_length
else failwith "Buffer.add: cannot grow buffer"
end;
!new_len
(* [resize_aux b len] resizes buffer [b] to ensure it may contain at least
[len] bytes. *)
let resize_aux b len =
let new_len = calc_size b.length len in
let new_buffer = Bytes.create new_len in
b.buffer <- new_buffer;
b.length <- new_len
let resize b len =
let old_buffer = b.buffer in
resize_aux b len;
(* PR#6148: let's keep using [blit] rather than [unsafe_blit] in
this tricky function that is slow anyway. *)
Bytes.blit old_buffer 0 b.buffer 0 b.position
let blit_substring_aux src srclen srcoff dst dstoff len =
if len < 0 || srcoff < 0 || srcoff > srclen - len
|| dstoff < 0 || dstoff > dst.position
then invalid_arg "Buffer.blit_*/add_*"
else
let new_pos = dstoff + len in
let new_len = calc_size dst.length new_pos in
if new_len > dst.length then begin
let old_buffer = dst.buffer in
resize_aux dst new_len; (* dst points to a new buffer now *)
Bytes.blit old_buffer 0 dst.buffer 0 dstoff;
Bytes.blit_string src srcoff dst.buffer dstoff len;
end
else Bytes.blit_string src srcoff dst.buffer dstoff len;
if new_pos > dst.position then dst.position <- new_pos
;;
let blit_buffer src srcoff dst dstoff len =
blit_substring_aux (Bytes.unsafe_to_string src.buffer) src.position srcoff dst dstoff len
let blit_substring src srcoff dst dstoff len =
blit_substring_aux src (String.length src) srcoff dst dstoff len
let blit_subbytes src srcoff dst dstoff len =
blit_substring_aux (Bytes.unsafe_to_string src) (Bytes.length src) srcoff dst dstoff len
let nth b ofs =
if ofs < 0 || ofs >= b.position then
invalid_arg "Buffer.nth"
else Bytes.unsafe_get b.buffer ofs
;;
let length b = b.position
let clear b = b.position <- 0
let reset b =
b.position <- 0; b.buffer <- b.initial_buffer;
b.length <- Bytes.length b.buffer
let truncate b c =
if c < 0 then invalid_arg "Buffer.truncate"
else if b.position > c then b.position <- c
let add_char b c =
let pos = b.position in
if pos >= b.length then resize b (pos + 1);
Bytes.unsafe_set b.buffer pos c;
b.position <- pos + 1
let add_substring b s offset len =
if offset < 0 || len < 0 || offset + len > String.length s
then invalid_arg "Buffer.add_substring/add_subbytes";
blit_substring_aux s (String.length s) offset b b.position len
let add_subbytes b s offset len =
add_substring b (Bytes.unsafe_to_string s) offset len
let add_string b s =
let len = String.length s in
blit_substring_aux s len 0 b b.position len
let add_bytes b s = add_string b (Bytes.unsafe_to_string s)
let add_buffer b bs =
add_subbytes b bs.buffer 0 bs.position
(* read up to [len] bytes from [ic] into [b]. *)
let rec add_channel_rec b ic len =
if len > 0 then (
let n = input ic b.buffer b.position len in
b.position <- b.position + n;
if n = 0 then raise End_of_file
else add_channel_rec b ic (len-n) (* n <= len *)
)
let add_channel b ic len =
if len < 0 || len > Sys.max_string_length then (* PR#5004 *)
invalid_arg "Buffer.add_channel";
if b.position + len > b.length then resize b (b.position + len);
add_channel_rec b ic len
let output_buffer oc b =
output oc b.buffer 0 b.position
let closing = function
| '(' -> ')'
| '{' -> '}'
| _ -> assert false;;
(* opening and closing: open and close characters, typically ( and )
k: balance of opening and closing chars
s: the string where we are searching
start: the index where we start the search. *)
let advance_to_closing opening closing k s start =
let rec advance k i lim =
if i >= lim then raise Not_found else
if s.[i] = opening then advance (k + 1) (i + 1) lim else
if s.[i] = closing then
if k = 0 then i else advance (k - 1) (i + 1) lim
else advance k (i + 1) lim in
advance k start (String.length s);;
let advance_to_non_alpha s start =
let rec advance i lim =
if i >= lim then lim else
match s.[i] with
| 'a' .. 'z' | 'A' .. 'Z' | '0' .. '9' | '_' -> advance (i + 1) lim
| _ -> i in
advance start (String.length s);;
(* We are just at the beginning of an ident in s, starting at start. *)
let find_ident s start lim =
if start >= lim then raise Not_found else
match s.[start] with
(* Parenthesized ident ? *)
| '(' | '{' as c ->
let new_start = start + 1 in
let stop = advance_to_closing c (closing c) 0 s new_start in
String.sub s new_start (stop - start - 1), stop + 1
(* Regular ident *)
| _ ->
let stop = advance_to_non_alpha s (start + 1) in
String.sub s start (stop - start), stop;;
(* Substitute $ident, $(ident), or ${ident} in s,
according to the function mapping f. *)
let add_substitute b f s =
let lim = String.length s in
let rec subst previous i =
if i < lim then begin
match s.[i] with
| '$' as current when previous = '\\' ->
add_char b current;
subst ' ' (i + 1)
| '$' ->
let j = i + 1 in
let ident, next_i = find_ident s j lim in
add_string b (f ident);
subst ' ' next_i
| current when previous == '\\' ->
add_char b '\\';
add_char b current;
subst ' ' (i + 1)
| '\\' as current ->
subst current (i + 1)
| current ->
add_char b current;
subst current (i + 1)
end else
if previous = '\\' then add_char b previous in
subst ' ' 0;;
src/libraries/stdlib/FCBuffer.mli deleted 100644 → 0
View file @ edfa608c
(*****************************************************************************)
(* *)
(* This file was originally part of Objective Caml *)
(* *)
(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *)
(* *)
(* Copyright (C) 1996 INRIA *)
(* INRIA (Institut National de Recherche en Informatique et en *)
(* Automatique) *)
(* *)
(* All rights reserved. *)
(* *)
(* This file is distributed under the terms of the GNU Library General *)
(* Public License version 2, with the special exception on linking *)
(* described below. See the GNU Library General Public License version *)
(* 2 for more details (enclosed in the file licenses/LGPLv2). *)
(* *)
(* As a special exception to the GNU Library General Public License, *)
(* you may link, statically or dynamically, a "work that uses the Library" *)
(* with a publicly distributed version of the Library to *)
(* produce an executable file containing portions of the Library, and *)
(* distribute that executable file under terms of your choice, without *)
(* any of the additional requirements listed in clause 6 of the GNU *)
(* Library General Public License. *)
(* By "a publicly distributed version of the Library", *)
(* we mean either the unmodified Library as *)
(* distributed by INRIA, or a modified version of the Library that is *)
(* distributed under the conditions defined in clause 2 of the GNU *)
(* Library General Public License. This exception does not however *)
(* invalidate any other reasons why the executable file might be *)
(* covered by the GNU Library General Public License. *)
(* *)
(* File modified by CEA (Commissariat à l'énergie atomique et aux *)
(* énergies alternatives). *)
(* *)
(*****************************************************************************)
(** Extensible buffers.
This module implements buffers that automatically expand
as necessary. It provides accumulative concatenation of strings
in quasi-linear time (instead of quadratic time when strings are
concatenated pairwise).
*)
type t
(** The abstract type of buffers. *)
val create : int -> t
(** [create n] returns a fresh buffer, initially empty.
The [n] parameter is the initial size of the internal byte sequence
that holds the buffer contents. That byte sequence is automatically
reallocated when more than [n] characters are stored in the buffer,
but shrinks back to [n] characters when [reset] is called.
For best performance, [n] should be of the same order of magnitude
as the number of characters that are expected to be stored in
the buffer (for instance, 80 for a buffer that holds one output
line). Nothing bad will happen if the buffer grows beyond that
limit, however. In doubt, take [n = 16] for instance.
If [n] is not between 1 and {!Sys.max_string_length}, it will
be clipped to that interval. *)
val contents : t -> string
(** Return a copy of the current contents of the buffer.
The buffer itself is unchanged. *)
val to_bytes : t -> bytes
(** Return a copy of the current contents of the buffer.
The buffer itself is unchanged.
@since 4.02 *)
val sub : t -> int -> int -> string
(** [Buffer.sub b off len] returns (a copy of) the bytes from the
current contents of the buffer [b] starting at offset [off] of
length [len] bytes. May raise [Invalid_argument] if out of bounds
request. The buffer itself is unaffected. *)
val sub_bytes : t -> int -> int -> bytes
(** Same as [sub] but return a byte sequence instead of a string.
@since 4.05 *)
val blit : t -> int -> bytes -> int -> int -> unit
(** [Buffer.blit src srcoff dst dstoff len] copies [len] characters from
the current contents of the buffer [src], starting at offset [srcoff]
to [dst], starting at character [dstoff].
Raise [Invalid_argument] if [srcoff] and [len] do not designate a valid
range of [src], or if [dstoff] and [len] do not designate a valid
range of [dst].
@since 3.11.2
*)
val blit_buffer : t -> int -> t -> int -> int -> unit
(** Similar to [blit], but copies to a buffer, and allows the destination
buffer to grow, that is, [dstoff + len] can be larger than the length of
[dst]. However, there cannot be any holes, i.e. [dstoff] must be smaller
than the original length of [dst].
@since 4.05 *)
val blit_substring : string -> int -> t -> int -> int -> unit
(** Same as [blit_buffer], but copies from a string to a buffer.
@since 4.05 *)
val blit_subbytes : bytes -> int -> t -> int -> int -> unit
(** Same as [blit_buffer], but copies from bytes to a buffer.
@since 4.05 *)
val nth : t -> int -> char
(** get the n-th character of the buffer. Raise [Invalid_argument] if
index out of bounds *)
val length : t -> int
(** Return the number of characters currently contained in the buffer. *)
val clear : t -> unit
(** Empty the buffer. *)
val reset : t -> unit
(** Empty the buffer and deallocate the internal byte sequence holding the
buffer contents, replacing it with the initial internal byte sequence
of length [n] that was allocated by {!Buffer.create} [n].
For long-lived buffers that may have grown a lot, [reset] allows
faster reclamation of the space used by the buffer. *)
val truncate : t -> int -> unit
(** [truncate b c] truncates the length of [b] to be no larger than [c].
Does nothing if the length of [b] is already smaller than or equal [c].
In particular, it does not change the size of the underlying buffer.
Raise [Invalid_argument] if [c < 0].
@since 4.05 *)
val add_char : t -> char -> unit
(** [add_char b c] appends the character [c] at the end of the buffer [b]. *)
val add_string : t -> string -> unit
(** [add_string b s] appends the string [s] at the end of the buffer [b]. *)
val add_bytes : t -> bytes -> unit
(** [add_string b s] appends the string [s] at the end of the buffer [b].
@since 4.02 *)
val add_substring : t -> string -> int -> int -> unit
(** [add_substring b s ofs len] takes [len] characters from offset
[ofs] in string [s] and appends them at the end of the buffer [b]. *)
val add_subbytes : t -> bytes -> int -> int -> unit
(** [add_substring b s ofs len] takes [len] characters from offset
[ofs] in byte sequence [s] and appends them at the end of the buffer [b].
@since 4.02 *)
val add_substitute : t -> (string -> string) -> string -> unit
(** [add_substitute b f s] appends the string pattern [s] at the end
of the buffer [b] with substitution.
The substitution process looks for variables into
the pattern and substitutes each variable name by its value, as
obtained by applying the mapping [f] to the variable name. Inside the
string pattern, a variable name immediately follows a non-escaped
[$] character and is one of the following:
- a non empty sequence of alphanumeric or [_] characters,
- an arbitrary sequence of characters enclosed by a pair of
matching parentheses or curly brackets.
An escaped [$] character is a [$] that immediately follows a backslash
character; it then stands for a plain [$].
Raise [Not_found] if the closing character of a parenthesized variable
cannot be found. *)
val add_buffer : t -> t -> unit
(** [add_buffer b1 b2] appends the current contents of buffer [b2]
at the end of buffer [b1]. [b2] is not modified. *)
val add_channel : t -> in_channel -> int -> unit
(** [add_channel b ic n] reads at most [n] characters from the
input channel [ic] and stores them at the end of buffer [b].
Raise [End_of_file] if the channel contains fewer than [n]
characters. In this case the characters are still added to
the buffer, so as to avoid loss of data. *)
val output_buffer : out_channel -> t -> unit
(** [output_buffer oc b] writes the current contents of buffer [b]
on the output channel [oc]. *)
src/libraries/utils/rich_text.ml
View file @ 3bc6e61d
......@@ -111,7 +111,7 @@ let tgr_buffer = 3145728 (* elasticity (internal overhead) *)
type buffer = {
mutable formatter : Format.formatter ; (* formatter on self (recursive) *)
mutable content : FCBuffer.t ;
mutable content : Buffer.t ;
mutable revtags : tag list ; (* in reverse order *)
mutable stack : (int * tag list) list ; (* opened tag positions *)
}
......@@ -122,52 +122,53 @@ let is_blank = function
let trim_begin buffer =
let rec lookup_fwd text k n =
if k < n && is_blank (FCBuffer.nth text k) then
if k < n && is_blank (Buffer.nth text k) then
lookup_fwd text (succ k) n else k
in lookup_fwd buffer.content 0 (FCBuffer.length buffer.content)
in lookup_fwd buffer.content 0 (Buffer.length buffer.content)
let trim_end buffer =
let rec lookup_bwd text k =
if k >= 0 && is_blank (FCBuffer.nth text k) then
if k >= 0 && is_blank (Buffer.nth text k) then
lookup_bwd text (pred k) else k
in lookup_bwd buffer.content (pred (FCBuffer.length buffer.content))
in lookup_bwd buffer.content (pred (Buffer.length buffer.content))
let shrink buffer =
if FCBuffer.length buffer.content > min_buffer then
FCBuffer.reset buffer.content
if Buffer.length buffer.content > min_buffer then
Buffer.reset buffer.content
let truncate_text buffer size =
if FCBuffer.length buffer.content > size then
if Buffer.length buffer.content > size then
begin
let p = trim_begin buffer in
let q = trim_end buffer in
let n = q+1-p in
if n <= 0 then shrink buffer else
if n <= size then
FCBuffer.blit_buffer buffer.content p buffer.content 0 n
if n <= 0 then
shrink buffer
else if n <= size then
Buffer.blit buffer.content p (Buffer.to_bytes buffer.content) 0 n
else
begin
let n_left = size / 2 - 3 in
let n_right = size - n_left - 5 in
if p > 0 then
FCBuffer.blit_buffer buffer.content p buffer.content 0 n_left ;
FCBuffer.blit_substring "[...]" 0 buffer.content n_left 5 ;
FCBuffer.blit_buffer
Buffer.blit buffer.content p (Buffer.to_bytes buffer.content) 0 n_left;
Buffer.add_substring buffer.content "[...]" n_left 5 ;
Buffer.blit
buffer.content (q-n_right+1)
buffer.content (n_left + 5)
(Buffer.to_bytes buffer.content) (n_left + 5)
n_right ;
FCBuffer.truncate buffer.content size ;
Buffer.truncate buffer.content size ;
end
end
(* All text added shall go through this function *)
let append buffer s k n =
FCBuffer.add_substring buffer.content s k n ;
if FCBuffer.length buffer.content > tgr_buffer then
Buffer.add_substring buffer.content s k n ;
if Buffer.length buffer.content > tgr_buffer then
truncate_text buffer max_buffer
let push_tag buffer _tag =
let p = FCBuffer.length buffer.content in
let p = Buffer.length buffer.content in
buffer.stack <- ( p , buffer.revtags ) :: buffer.stack ;
buffer.revtags <- []
......@@ -175,7 +176,7 @@ let pop_tag buffer tag =
match buffer.stack with
| [] -> ()
| (p,tags)::stack ->
let q = FCBuffer.length buffer.content in
let q = Buffer.length buffer.content in
buffer.stack <- stack ;
let children = List.rev buffer.revtags in
buffer.revtags <- { p ; q ; tag ; children } :: tags
......@@ -189,7 +190,7 @@ let no_mark _tag = ""
let create ?indent ?margin () =
let buffer = {
formatter = Format.err_formatter ;
content = FCBuffer.create min_buffer ;
content = Buffer.create min_buffer ;
revtags = [] ;
stack = [] ;
} in
......@@ -226,13 +227,13 @@ let trim buffer =
p , q
let contents buffer =
truncate_text buffer max_buffer ; FCBuffer.contents buffer.content
truncate_text buffer max_buffer ; Buffer.contents buffer.content
let message buffer =
( FCBuffer.contents buffer.content , List.rev buffer.revtags )
( Buffer.contents buffer.content , List.rev buffer.revtags )
let sub buffer p n = FCBuffer.sub buffer.content p n
let range buffer p q = FCBuffer.sub buffer.content p (q+1-p)
let sub buffer p n = Buffer.sub buffer.content p n
let range buffer p q = Buffer.sub buffer.content p (q+1-p)
let add_char buffer c = Format.pp_print_char buffer.formatter c
let add_string buffer s = Format.pp_print_string buffer.formatter s
......
src/plugins/server/jbuffer.ml
View file @ 3bc6e61d
......@@ -23,22 +23,22 @@
type json = Yojson.Basic.t
type buffer = {
text : FCBuffer.t ;
text : Buffer.t ;
mutable rjson : json list ; (* Current op-codes in reverse order *)
mutable stack : ( string * json list ) list ;
mutable fmt : Format.formatter ;
}
let append buffer s k n =
FCBuffer.add_substring buffer.text s k n
Buffer.add_substring buffer.text s k n
let flush buffer () =
let t = buffer.text in
let n = FCBuffer.length t in
let n = Buffer.length t in
if n > 0 then
let js = `String (FCBuffer.contents t) in
let js = `String (Buffer.contents t) in
buffer.rjson <- js :: buffer.rjson ;
FCBuffer.clear t