aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.merlin2
-rw-r--r--configure.ml9
-rw-r--r--ide/coqide.ml4
-rw-r--r--ide/ideutils.ml25
-rw-r--r--interp/dumpglob.ml17
-rw-r--r--kernel/cemitcodes.ml47
-rw-r--r--kernel/names.ml9
-rw-r--r--kernel/names.mli1
-rw-r--r--kernel/nativevalues.ml8
-rw-r--r--kernel/term_typing.ml3
-rw-r--r--lib/cThread.ml18
-rw-r--r--lib/cThread.mli4
-rw-r--r--lib/cUnix.ml8
-rw-r--r--lib/cUnix.mli2
-rw-r--r--lib/pp_control.ml2
-rw-r--r--lib/util.ml8
-rw-r--r--library/nameops.ml20
-rw-r--r--parsing/cLexer.ml418
-rw-r--r--plugins/extraction/common.ml5
-rw-r--r--plugins/extraction/scheme.ml6
-rw-r--r--plugins/extraction/table.ml4
-rw-r--r--plugins/ltac/profile_ltac.ml2
-rw-r--r--tools/coq_makefile.ml21
-rw-r--r--tools/coqdoc/alpha.ml7
-rw-r--r--tools/coqdoc/index.ml12
-rw-r--r--tools/coqworkmgr.ml9
-rw-r--r--toplevel/coqloop.ml36
-rw-r--r--toplevel/coqloop.mli2
-rw-r--r--toplevel/vernac.ml16
29 files changed, 169 insertions, 156 deletions
diff --git a/.merlin b/.merlin
index bda18d549..394db528d 100644
--- a/.merlin
+++ b/.merlin
@@ -1,4 +1,4 @@
-FLG -rectypes -thread
+FLG -rectypes -thread -safe-string
S ltac
B ltac
diff --git a/configure.ml b/configure.ml
index 82ce931d6..dfc6724a2 100644
--- a/configure.ml
+++ b/configure.ml
@@ -264,6 +264,10 @@ module Prefs = struct
let debug = ref true
let profile = ref false
let annotate = ref false
+ (* Note, disabling this should be OK, but be careful with the
+ sharing invariants.
+ *)
+ let safe_string = ref true
let nativecompiler = ref (not (os_type_win32 || os_type_cygwin))
let coqwebsite = ref "http://coq.inria.fr/"
let force_caml_version = ref false
@@ -386,6 +390,9 @@ let coq_annotate_flag =
then if program_in_path "ocamlmerlin" then "-bin-annot" else "-annot"
else ""
+let coq_safe_string =
+ if !Prefs.safe_string then "-safe-string" else ""
+
let cflags = "-Wall -Wno-unused -g -O2"
(** * Architecture *)
@@ -1118,7 +1125,7 @@ let write_makefile f =
pr "CAMLHLIB=%S\n\n" camllib;
pr "# Caml link command and Caml make top command\n";
pr "# Caml flags\n";
- pr "CAMLFLAGS=-rectypes %s\n" coq_annotate_flag;
+ pr "CAMLFLAGS=-rectypes %s %s\n" coq_annotate_flag coq_safe_string;
pr "# User compilation flag\n";
pr "USERFLAGS=\n\n";
pr "# Flags for GCC\n";
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 450bfcdfb..eec829f34 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -887,8 +887,8 @@ let alpha_items menu_name item_name l =
| [] -> ()
| [s] -> mk_item s
| s::_ as ll ->
- let name = item_name^" "^(String.make 1 s.[0]) in
- let label = "_@..." in label.[1] <- s.[0];
+ let name = Printf.sprintf "%s %c" item_name s.[0] in
+ let label = Printf.sprintf "_%c..." s.[0] in
item name ~label menu_name;
List.iter mk_item ll
in
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 06a132732..c3a280796 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -294,18 +294,20 @@ let coqtop_path () =
match cmd_coqtop#get with
| Some s -> s
| None ->
- let prog = String.copy Sys.executable_name in
try
- let pos = String.length prog - 6 in
- let i = Str.search_backward (Str.regexp_string "coqide") prog pos
+ let old_prog = Sys.executable_name in
+ let pos = String.length old_prog - 6 in
+ let i = Str.search_backward (Str.regexp_string "coqide") old_prog pos
in
- String.blit "coqtop" 0 prog i 6;
- if Sys.file_exists prog then prog
+ let new_prog = Bytes.of_string old_prog in
+ Bytes.blit_string "coqtop" 0 new_prog i 6;
+ let new_prog = Bytes.to_string new_prog in
+ if Sys.file_exists new_prog then new_prog
else
let in_macos_bundle =
Filename.concat
- (Filename.dirname prog)
- (Filename.concat "../Resources/bin" (Filename.basename prog))
+ (Filename.dirname new_prog)
+ (Filename.concat "../Resources/bin" (Filename.basename new_prog))
in if Sys.file_exists in_macos_bundle then in_macos_bundle
else "coqtop"
with Not_found -> "coqtop"
@@ -357,7 +359,7 @@ let stat f =
let maxread = 4096
-let read_string = String.create maxread
+let read_string = Bytes.create maxread
let read_buffer = Buffer.create maxread
(** Read the content of file [f] and add it to buffer [b].
@@ -368,7 +370,7 @@ let read_file name buf =
let len = ref 0 in
try
while len := input ic read_string 0 maxread; !len > 0 do
- Buffer.add_substring buf read_string 0 !len
+ Buffer.add_subbytes buf read_string 0 !len
done;
close_in ic
with e -> close_in ic; raise e
@@ -381,8 +383,9 @@ let read_file name buf =
let io_read_all chan =
Buffer.clear read_buffer;
let read_once () =
- let len = Glib.Io.read_chars ~buf:read_string ~pos:0 ~len:maxread chan in
- Buffer.add_substring read_buffer read_string 0 len
+ (* XXX: Glib.Io must be converted to bytes / -safe-string upstream *)
+ let len = Glib.Io.read_chars ~buf:(Bytes.unsafe_to_string read_string) ~pos:0 ~len:maxread chan in
+ Buffer.add_subbytes read_buffer read_string 0 len
in
begin
try while true do read_once () done
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index b020f8945..9f549b0c0 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -173,32 +173,33 @@ let cook_notation df sc =
(* - all single quotes in terminal tokens are doubled *)
(* - characters < 32 are represented by '^A, '^B, '^C, etc *)
(* The output is decoded in function Index.prepare_entry of coqdoc *)
- let ntn = String.make (String.length df * 5) '_' in
+ let ntn = Bytes.make (String.length df * 5) '_' in
let j = ref 0 in
let l = String.length df - 1 in
let i = ref 0 in
+ let open Bytes in (* Bytes.set *)
while !i <= l do
assert (df.[!i] != ' ');
if df.[!i] == '_' && (Int.equal !i l || df.[!i+1] == ' ') then
(* Next token is a non-terminal *)
- (ntn.[!j] <- 'x'; incr j; incr i)
+ (set ntn !j 'x'; incr j; incr i)
else begin
(* Next token is a terminal *)
- ntn.[!j] <- '\''; incr j;
+ set ntn !j '\''; incr j;
while !i <= l && df.[!i] != ' ' do
if df.[!i] < ' ' then
let c = char_of_int (int_of_char 'A' + int_of_char df.[!i] - 1) in
(String.blit ("'^" ^ String.make 1 c) 0 ntn !j 3; j := !j+3; incr i)
else begin
- if df.[!i] == '\'' then (ntn.[!j] <- '\''; incr j);
- ntn.[!j] <- df.[!i]; incr j; incr i
+ if df.[!i] == '\'' then (set ntn !j '\''; incr j);
+ set ntn !j df.[!i]; incr j; incr i
end
done;
- ntn.[!j] <- '\''; incr j
+ set ntn !j '\''; incr j
end;
- if !i <= l then (ntn.[!j] <- '_'; incr j; incr i)
+ if !i <= l then (set ntn !j '_'; incr j; incr i)
done;
- let df = String.sub ntn 0 !j in
+ let df = Bytes.sub_string ntn 0 !j in
match sc with Some sc -> ":" ^ sc ^ ":" ^ df | _ -> "::" ^ df
let dump_notation_location posl df (((path,secpath),_),sc) =
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index ad7a41a34..f2c3b402b 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -24,33 +24,45 @@ type reloc_info =
type patch = reloc_info * int
let patch_char4 buff pos c1 c2 c3 c4 =
- String.unsafe_set buff pos c1;
- String.unsafe_set buff (pos + 1) c2;
- String.unsafe_set buff (pos + 2) c3;
- String.unsafe_set buff (pos + 3) c4
+ Bytes.unsafe_set buff pos c1;
+ Bytes.unsafe_set buff (pos + 1) c2;
+ Bytes.unsafe_set buff (pos + 2) c3;
+ Bytes.unsafe_set buff (pos + 3) c4
let patch buff (pos, n) =
patch_char4 buff pos
(Char.unsafe_chr n) (Char.unsafe_chr (n asr 8)) (Char.unsafe_chr (n asr 16))
(Char.unsafe_chr (n asr 24))
+(* val patch_int : emitcodes -> ((\*pos*\)int * int) list -> emitcodes *)
let patch_int buff patches =
(* copy code *before* patching because of nested evaluations:
the code we are patching might be called (and thus "concurrently" patched)
and results in wrong results. Side-effects... *)
- let buff = String.copy buff in
+ let buff = Bytes.of_string buff in
let () = List.iter (fun p -> patch buff p) patches in
- buff
+ (* Note: we follow the apporach suggested by Gabriel Scherer in
+ PR#136 here, and use unsafe as we own buff.
+
+ The crux of the question that avoids defining emitcodes just as a
+ Byte.t is the call to hcons in to_memory below. Even if disabling
+ this optimization has no visible time impact, test data shows
+ that the optimization is indeed triggered quite often so we
+ choose ugliness over altering the semantics.
+
+ Handle with care.
+ *)
+ Bytes.unsafe_to_string buff
(* Buffering of bytecode *)
-let out_buffer = ref(String.create 1024)
+let out_buffer = ref(Bytes.create 1024)
and out_position = ref 0
let out_word b1 b2 b3 b4 =
let p = !out_position in
- if p >= String.length !out_buffer then begin
- let len = String.length !out_buffer in
+ if p >= Bytes.length !out_buffer then begin
+ let len = Bytes.length !out_buffer in
let new_len =
if len <= Sys.max_string_length / 2
then 2 * len
@@ -58,8 +70,8 @@ let out_word b1 b2 b3 b4 =
if len = Sys.max_string_length
then invalid_arg "String.create" (* Pas la bonne exception .... *)
else Sys.max_string_length in
- let new_buffer = String.create new_len in
- String.blit !out_buffer 0 new_buffer 0 len;
+ let new_buffer = Bytes.create new_len in
+ Bytes.blit !out_buffer 0 new_buffer 0 len;
out_buffer := new_buffer
end;
patch_char4 !out_buffer p (Char.unsafe_chr b1)
@@ -94,10 +106,10 @@ let extend_label_table needed =
let backpatch (pos, orig) =
let displ = (!out_position - orig) asr 2 in
- !out_buffer.[pos] <- Char.unsafe_chr displ;
- !out_buffer.[pos+1] <- Char.unsafe_chr (displ asr 8);
- !out_buffer.[pos+2] <- Char.unsafe_chr (displ asr 16);
- !out_buffer.[pos+3] <- Char.unsafe_chr (displ asr 24)
+ Bytes.set !out_buffer pos @@ Char.unsafe_chr displ;
+ Bytes.set !out_buffer (pos+1) @@ Char.unsafe_chr (displ asr 8);
+ Bytes.set !out_buffer (pos+2) @@ Char.unsafe_chr (displ asr 16);
+ Bytes.set !out_buffer (pos+3) @@ Char.unsafe_chr (displ asr 24)
let define_label lbl =
if lbl >= Array.length !label_table then extend_label_table lbl;
@@ -305,7 +317,7 @@ let init () =
label_table := Array.make 16 (Label_undefined []);
reloc_info := []
-type emitcodes = string
+type emitcodes = String.t
let length = String.length
@@ -369,9 +381,8 @@ let to_memory (init_code, fun_code, fv) =
init();
emit init_code;
emit fun_code;
- let code = String.create !out_position in
- String.unsafe_blit !out_buffer 0 code 0 !out_position;
(** Later uses of this string are all purely functional *)
+ let code = Bytes.sub_string !out_buffer 0 !out_position in
let code = CString.hcons code in
let reloc = List.rev !reloc_info in
Array.iter (fun lbl ->
diff --git a/kernel/names.ml b/kernel/names.ml
index 1f138581c..ee8d838da 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -50,17 +50,20 @@ struct
| None -> true
| Some _ -> false
+ let of_bytes s =
+ let s = Bytes.to_string s in
+ check_soft s;
+ String.hcons s
+
let of_string s =
let () = check_soft s in
- let s = String.copy s in
String.hcons s
let of_string_soft s =
let () = check_soft ~warn:false s in
- let s = String.copy s in
String.hcons s
- let to_string id = String.copy id
+ let to_string id = id
let print id = str id
diff --git a/kernel/names.mli b/kernel/names.mli
index 6b0a80625..be9b9422b 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -43,6 +43,7 @@ sig
(** Check that a string may be converted to an identifier.
@raise Unicode.Unsupported if the provided string contains unsupported UTF-8 characters. *)
+ val of_bytes : bytes -> t
val of_string : string -> t
(** Converts a string into an identifier.
@raise UserError if the string is not valid, or echo a warning if it contains invalid identifier characters.
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 8093df304..965ed67b0 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -491,12 +491,12 @@ let str_encode expr =
let str_decode s =
let mshl_expr_len = String.length s / 2 in
let mshl_expr = Buffer.create mshl_expr_len in
- let buf = String.create 2 in
+ let buf = Bytes.create 2 in
for i = 0 to mshl_expr_len - 1 do
- String.blit s (2*i) buf 0 2;
- Buffer.add_char mshl_expr (bin_of_hex buf)
+ Bytes.blit_string s (2*i) buf 0 2;
+ Buffer.add_char mshl_expr (bin_of_hex (Bytes.to_string buf))
done;
- Marshal.from_string (Buffer.contents mshl_expr) 0
+ Marshal.from_bytes (Buffer.to_bytes mshl_expr) 0
(** Retroknowledge, to be removed when we switch to primitive integers *)
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index a63eb3376..22b7eebcb 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -76,8 +76,7 @@ let inline_side_effects env body ctx side_eff =
let cbl = List.filter not_exists cbl in
let cname c =
let name = string_of_con c in
- for i = 0 to String.length name - 1 do
- if name.[i] == '.' || name.[i] == '#' then name.[i] <- '_' done;
+ let name = String.map (fun c -> if c == '.' || c == '#' then '_' else c) name in
Name (id_of_string name) in
let rec sub c i x = match kind_of_term x with
| Const (c', _) when eq_constant c c' -> mkRel i
diff --git a/lib/cThread.ml b/lib/cThread.ml
index 4f60a6974..9f642b3ce 100644
--- a/lib/cThread.ml
+++ b/lib/cThread.ml
@@ -36,7 +36,7 @@ let really_read_fd fd s off len =
let really_read_fd_2_oc fd oc len =
let i = ref 0 in
let size = 4096 in
- let s = String.create size in
+ let s = Bytes.create size in
while !i < len do
let len = len - !i in
let r = thread_friendly_read_fd fd s ~off:0 ~len:(min len size) in
@@ -55,11 +55,13 @@ let thread_friendly_really_read_line ic =
try
let fd = Unix.descr_of_in_channel ic in
let b = Buffer.create 1024 in
- let s = String.make 1 '\000' in
- while s <> "\n" do
+ let s = Bytes.make 1 '\000' in
+ let endl = Bytes.of_string "\n" in
+ (* Bytes.equal is in 4.03.0 *)
+ while Bytes.compare s endl <> 0 do
let n = thread_friendly_read_fd fd s ~off:0 ~len:1 in
if n = 0 then raise End_of_file;
- if s <> "\n" then Buffer.add_string b s;
+ if Bytes.compare s endl <> 0 then Buffer.add_bytes b s;
done;
Buffer.contents b
with Unix.Unix_error _ -> raise End_of_file
@@ -67,15 +69,15 @@ let thread_friendly_really_read_line ic =
let thread_friendly_input_value ic =
try
let fd = Unix.descr_of_in_channel ic in
- let header = String.create Marshal.header_size in
+ let header = Bytes.create Marshal.header_size in
really_read_fd fd header 0 Marshal.header_size;
let body_size = Marshal.data_size header 0 in
let desired_size = body_size + Marshal.header_size in
if desired_size <= Sys.max_string_length then begin
- let msg = String.create desired_size in
- String.blit header 0 msg 0 Marshal.header_size;
+ let msg = Bytes.create desired_size in
+ Bytes.blit header 0 msg 0 Marshal.header_size;
really_read_fd fd msg Marshal.header_size body_size;
- Marshal.from_string msg 0
+ Marshal.from_bytes msg 0
end else begin
(* Workaround for 32 bit systems and data > 16M *)
let name, oc =
diff --git a/lib/cThread.mli b/lib/cThread.mli
index 7302dfb55..36477a116 100644
--- a/lib/cThread.mli
+++ b/lib/cThread.mli
@@ -19,8 +19,8 @@ val prepare_in_channel_for_thread_friendly_io : in_channel -> thread_ic
val thread_friendly_input_value : thread_ic -> 'a
val thread_friendly_read :
- thread_ic -> string -> off:int -> len:int -> int
+ thread_ic -> Bytes.t -> off:int -> len:int -> int
val thread_friendly_really_read :
- thread_ic -> string -> off:int -> len:int -> unit
+ thread_ic -> Bytes.t -> off:int -> len:int -> unit
val thread_friendly_really_read_line : thread_ic -> string
diff --git a/lib/cUnix.ml b/lib/cUnix.ml
index cb436511f..2542b9751 100644
--- a/lib/cUnix.ml
+++ b/lib/cUnix.ml
@@ -91,15 +91,15 @@ let rec waitpid_non_intr pid =
let run_command ?(hook=(fun _ ->())) c =
let result = Buffer.create 127 in
let cin,cout,cerr = Unix.open_process_full c (Unix.environment ()) in
- let buff = String.make 127 ' ' in
- let buffe = String.make 127 ' ' in
+ let buff = Bytes.make 127 ' ' in
+ let buffe = Bytes.make 127 ' ' in
let n = ref 0 in
let ne = ref 0 in
while n:= input cin buff 0 127 ; ne := input cerr buffe 0 127 ;
!n+ !ne <> 0
do
- let r = String.sub buff 0 !n in (hook r; Buffer.add_string result r);
- let r = String.sub buffe 0 !ne in (hook r; Buffer.add_string result r);
+ let r = Bytes.sub buff 0 !n in (hook r; Buffer.add_bytes result r);
+ let r = Bytes.sub buffe 0 !ne in (hook r; Buffer.add_bytes result r);
done;
(Unix.close_process_full (cin,cout,cerr), Buffer.contents result)
diff --git a/lib/cUnix.mli b/lib/cUnix.mli
index f03719c3d..c6bcf6347 100644
--- a/lib/cUnix.mli
+++ b/lib/cUnix.mli
@@ -46,7 +46,7 @@ val file_readable_p : string -> bool
is called on each elements read on stdout or stderr. *)
val run_command :
- ?hook:(string->unit) -> string -> Unix.process_status * string
+ ?hook:(bytes->unit) -> string -> Unix.process_status * string
(** [sys_command] launches program [prog] with arguments [args].
It behaves like [Sys.command], except that we rely on
diff --git a/lib/pp_control.ml b/lib/pp_control.ml
index 890ffe0a1..ab8dc0798 100644
--- a/lib/pp_control.ml
+++ b/lib/pp_control.ml
@@ -58,7 +58,7 @@ let with_fp chan out_function flush_function =
(* Output on a channel ch *)
let with_output_to ch =
- let ft = with_fp ch (output ch) (fun () -> flush ch) in
+ let ft = with_fp ch (output_substring ch) (fun () -> flush ch) in
set_gp ft deep_gp;
ft
diff --git a/lib/util.ml b/lib/util.ml
index 9fb0d48ee..0d2425f27 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -161,11 +161,11 @@ let iraise = Exninfo.iraise
let open_utf8_file_in fname =
let is_bom s =
- Int.equal (Char.code s.[0]) 0xEF &&
- Int.equal (Char.code s.[1]) 0xBB &&
- Int.equal (Char.code s.[2]) 0xBF
+ Int.equal (Char.code (Bytes.get s 0)) 0xEF &&
+ Int.equal (Char.code (Bytes.get s 1)) 0xBB &&
+ Int.equal (Char.code (Bytes.get s 2)) 0xBF
in
let in_chan = open_in fname in
- let s = " " in
+ let s = Bytes.make 3 ' ' in
if input in_chan s 0 3 < 3 || not (is_bom s) then seek_in in_chan 0;
in_chan
diff --git a/library/nameops.ml b/library/nameops.ml
index 6020db33d..098f5112f 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -61,7 +61,7 @@ let make_ident sa = function
if c < code_of_0 || c > code_of_9 then sa ^ (string_of_int n)
else sa ^ "_" ^ (string_of_int n) in
Id.of_string s
- | None -> Id.of_string (String.copy sa)
+ | None -> Id.of_string sa
let root_of_id id =
let suffixstart = cut_ident true id in
@@ -92,20 +92,20 @@ let increment_subscript id =
add (carrypos-1)
end
else begin
- let newid = String.copy id in
- String.fill newid (carrypos+1) (len-1-carrypos) '0';
- newid.[carrypos] <- Char.chr (Char.code c + 1);
+ let newid = Bytes.of_string id in
+ Bytes.fill newid (carrypos+1) (len-1-carrypos) '0';
+ Bytes.set newid carrypos (Char.chr (Char.code c + 1));
newid
end
else begin
- let newid = id^"0" in
+ let newid = Bytes.of_string (id^"0") in
if carrypos < len-1 then begin
- String.fill newid (carrypos+1) (len-1-carrypos) '0';
- newid.[carrypos+1] <- '1'
+ Bytes.fill newid (carrypos+1) (len-1-carrypos) '0';
+ Bytes.set newid (carrypos+1) '1'
end;
newid
end
- in Id.of_string (add (len-1))
+ in Id.of_bytes (add (len-1))
let has_subscript id =
let id = Id.to_string id in
@@ -113,9 +113,9 @@ let has_subscript id =
let forget_subscript id =
let numstart = cut_ident false id in
- let newid = String.make (numstart+1) '0' in
+ let newid = Bytes.make (numstart+1) '0' in
String.blit (Id.to_string id) 0 newid 0 numstart;
- (Id.of_string newid)
+ (Id.of_bytes newid)
let add_suffix id s = Id.of_string (Id.to_string id ^ s)
let add_prefix s id = Id.of_string (s ^ Id.to_string id)
diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index 02a720d2d..72bd11e03 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -240,18 +240,19 @@ let unfreeze tt = (token_tree := tt)
(* The string buffering machinery *)
-let buff = ref (String.create 80)
+let buff = ref (Bytes.create 80)
let store len x =
- if len >= String.length !buff then
- buff := !buff ^ String.create (String.length !buff);
- !buff.[len] <- x;
+ let open Bytes in
+ if len >= length !buff then
+ buff := cat !buff (create (length !buff));
+ set !buff len x;
succ len
let rec nstore n len cs =
if n>0 then nstore (n-1) (store len (Stream.next cs)) cs else len
-let get_buff len = String.sub !buff 0 len
+let get_buff len = Bytes.sub_string !buff 0 len
(* The classical lexer: idents, numbers, quoted strings, comments *)
@@ -382,6 +383,7 @@ let push_char c =
real_push_char c
let push_string s = Buffer.add_string current_comment s
+let push_bytes s = Buffer.add_bytes current_comment s
let null_comment s =
let rec null i =
@@ -716,13 +718,13 @@ let strip s =
in
if len == String.length s then s
else
- let s' = String.create len in
+ let s' = Bytes.create len in
let rec loop i i' =
if i == String.length s then s'
else if s.[i] == ' ' then loop (i + 1) i'
- else begin s'.[i'] <- s.[i]; loop (i + 1) (i' + 1) end
+ else begin Bytes.set s' i' s.[i]; loop (i + 1) (i' + 1) end
in
- loop 0 0
+ Bytes.to_string (loop 0 0)
let terminal s =
let s = strip s in
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index de97ba97c..0a591e786 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -91,10 +91,7 @@ let begins_with_CoqXX s =
let unquote s =
if lang () != Scheme then s
- else
- let s = String.copy s in
- for i=0 to String.length s - 1 do if s.[i] == '\'' then s.[i] <- '~' done;
- s
+ else String.map (fun c -> if c == '\'' then '~' else c) s
let rec qualify delim = function
| [] -> assert false
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index a6309e61f..8d0cc4a0d 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -40,11 +40,7 @@ let preamble _ comment _ usf =
(if usf.mldummy then str "(define __ (lambda (_) __))\n\n" else mt ())
let pr_id id =
- let s = Id.to_string id in
- for i = 0 to String.length s - 1 do
- if s.[i] == '\'' then s.[i] <- '~'
- done;
- str s
+ str @@ String.map (fun c -> if c == '\'' then '~' else c) (Id.to_string id)
let paren = pp_par true
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 5e7d810c9..d6a334c5f 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -773,9 +773,7 @@ let file_of_modfile mp =
| MPfile f -> Id.to_string (List.hd (DirPath.repr f))
| _ -> assert false
in
- let s = String.copy (string_of_modfile mp) in
- if s.[0] != s0.[0] then s.[0] <- s0.[0];
- s
+ String.mapi (fun i c -> if i = 0 then s0.[0] else c) (string_of_modfile mp)
let add_blacklist_entries l =
blacklist_table :=
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 2514ededb..58123f63e 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -257,7 +257,7 @@ let string_of_call ck =
(Pptactic.pr_glob_tactic (Global.env ())
te)
) in
- for i = 0 to String.length s - 1 do if s.[i] = '\n' then s.[i] <- ' ' done;
+ let s = String.map (fun c -> if c = '\n' then ' ' else c) s in
let s = try String.sub s 0 (CString.string_index_from s 0 "(*") with Not_found -> s in
CString.strip s
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 4842a8915..4dfb7af6a 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -125,12 +125,9 @@ let physical_dir_of_logical_dir ldir =
let le = String.length ldir - 1 in
let pdir =
if le >= 0 && ldir.[le] = '.' then String.sub ldir 0 (le - 1)
- else String.copy ldir
+ else ldir
in
- for i = 0 to le - 1 do
- if pdir.[i] = '.' then pdir.[i] <- '/';
- done;
- pdir
+ String.map (fun c -> if c = '.' then '/' else c) pdir
let standard opt =
print "byte:\n";
@@ -524,10 +521,10 @@ let variables is_install opt (args,defs) =
List.iter (fun c -> print " \\
-I \"$(COQLIB)/"; print c; print "\"") Coq_config.plugins_dirs; print "\n";
print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n\n";
- print "CAMLC?=$(OCAMLFIND) ocamlc -c -rectypes -thread\n";
- print "CAMLOPTC?=$(OCAMLFIND) opt -c -rectypes -thread\n";
- print "CAMLLINK?=$(OCAMLFIND) ocamlc -rectypes -thread\n";
- print "CAMLOPTLINK?=$(OCAMLFIND) opt -rectypes -thread\n";
+ print "CAMLC?=$(OCAMLFIND) ocamlc -c -rectypes -thread -safe-string\n";
+ print "CAMLOPTC?=$(OCAMLFIND) opt -c -rectypes -thread -safe-string\n";
+ print "CAMLLINK?=$(OCAMLFIND) ocamlc -rectypes -thread -safe-string\n";
+ print "CAMLOPTLINK?=$(OCAMLFIND) opt -rectypes -thread -safe-string\n";
print "CAMLDEP?=$(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack\n";
print "CAMLLIB?=$(shell $(OCAMLFIND) printconf stdlib)\n";
print "GRAMMARS?=grammar.cma\n";
@@ -767,9 +764,9 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other
begin
print "mlihtml: $(MLIFILES:.mli=.cmi)\n";
print "\t mkdir $@ || rm -rf $@/*\n";
- print "\t$(OCAMLFIND) ocamldoc -html -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
+ print "\t$(OCAMLFIND) ocamldoc -html -safe-string -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
print "all-mli.tex: $(MLIFILES:.mli=.cmi)\n";
- print "\t$(OCAMLFIND) ocamldoc -latex -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
+ print "\t$(OCAMLFIND) ocamldoc -latex -safe-string -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
end;
if !some_vfile then
begin
@@ -885,7 +882,7 @@ let check_overlapping_include (_,inc_i,inc_r) =
*)
let merlin targets (ml_inc,_,_) =
print ".merlin:\n";
- print "\t@echo 'FLG -rectypes' > .merlin\n" ;
+ print "\t@echo 'FLG -rectypes -safe-string' > .merlin\n" ;
List.iter (fun c ->
printf "\t@echo \"B $(COQLIB)%s\" >> .merlin\n" c)
lib_dirs ;
diff --git a/tools/coqdoc/alpha.ml b/tools/coqdoc/alpha.ml
index f817ed5a2..3d92c9356 100644
--- a/tools/coqdoc/alpha.ml
+++ b/tools/coqdoc/alpha.ml
@@ -26,12 +26,7 @@ let norm_char c =
if !latin1 then norm_char_latin1 c else
Char.uppercase c
-let norm_string s =
- let u = String.copy s in
- for i = 0 to String.length s - 1 do
- u.[i] <- norm_char s.[i]
- done;
- u
+let norm_string = String.map (fun s -> norm_char s)
let compare_char c1 c2 = match norm_char c1, norm_char c2 with
| ('A'..'Z' as c1), ('A'..'Z' as c2) -> compare c1 c2
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index 9be791a8d..34108eff4 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -197,7 +197,7 @@ let prepare_entry s = function
let h = try String.index_from s 0 ':' with _ -> err () in
let i = try String.index_from s (h+1) ':' with _ -> err () in
let sc = String.sub s (h+1) (i-h-1) in
- let ntn = String.make (String.length s - i) ' ' in
+ let ntn = Bytes.make (String.length s - i) ' ' in
let k = ref 0 in
let j = ref (i+1) in
let quoted = ref false in
@@ -205,22 +205,22 @@ let prepare_entry s = function
while !j <= l do
if not !quoted then begin
(match s.[!j] with
- | '_' -> ntn.[!k] <- ' '; incr k
- | 'x' -> ntn.[!k] <- '_'; incr k
+ | '_' -> Bytes.set ntn !k ' '; incr k
+ | 'x' -> Bytes.set ntn !k '_'; incr k
| '\'' -> quoted := true
| _ -> assert false)
end
else
if s.[!j] = '\'' then
if (!j = l || s.[!j+1] = '_') then quoted := false
- else (incr j; ntn.[!k] <- s.[!j]; incr k)
+ else (incr j; Bytes.set ntn !k s.[!j]; incr k)
else begin
- ntn.[!k] <- s.[!j];
+ Bytes.set ntn !k s.[!j];
incr k
end;
incr j
done;
- let ntn = String.sub ntn 0 !k in
+ let ntn = Bytes.sub_string ntn 0 !k in
if sc = "" then ntn else ntn ^ " (" ^ sc ^ ")"
| _ ->
s
diff --git a/tools/coqworkmgr.ml b/tools/coqworkmgr.ml
index d7bdf907a..b8e69d6c6 100644
--- a/tools/coqworkmgr.ml
+++ b/tools/coqworkmgr.ml
@@ -72,10 +72,13 @@ let really_read_fd fd s off len =
let raw_input_line fd =
try
let b = Buffer.create 80 in
- let s = String.make 1 '\000' in
- while s <> "\n" do
+ let s = Bytes.make 1 '\000' in
+ let endl = Bytes.of_string "\n" in
+ let endr = Bytes.of_string "\r" in
+ while Bytes.compare s endl <> 0 do
really_read_fd fd s 0 1;
- if s <> "\n" && s <> "\r" then Buffer.add_string b s;
+ if Bytes.compare s endl <> 0 && Bytes.compare s endr <> 0
+ then Buffer.add_bytes b s;
done;
Buffer.contents b
with Unix.Unix_error _ -> raise End_of_file
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index e9771cfa4..0dfd06726 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -20,7 +20,7 @@ let top_stderr x = msg_with ~pp_tag:Ppstyle.pp_tag !Pp_control.err_ft x
type input_buffer = {
mutable prompt : unit -> string;
- mutable str : string; (* buffer of already read characters *)
+ mutable str : Bytes.t; (* buffer of already read characters *)
mutable len : int; (* number of chars in the buffer *)
mutable bols : int list; (* offsets in str of beginning of lines *)
mutable tokens : Gram.coq_parsable; (* stream of tokens *)
@@ -28,9 +28,9 @@ type input_buffer = {
(* Double the size of the buffer. *)
-let resize_buffer ibuf =
- let nstr = String.create (2 * String.length ibuf.str + 1) in
- String.blit ibuf.str 0 nstr 0 (String.length ibuf.str);
+let resize_buffer ibuf = let open Bytes in
+ let nstr = create (2 * length ibuf.str + 1) in
+ blit ibuf.str 0 nstr 0 (length ibuf.str);
ibuf.str <- nstr
(* Delete all irrelevant lines of the input buffer. Keep the last line
@@ -40,7 +40,7 @@ let resynch_buffer ibuf =
match ibuf.bols with
| ll::_ ->
let new_len = ibuf.len - ll in
- String.blit ibuf.str ll ibuf.str 0 new_len;
+ Bytes.blit ibuf.str ll ibuf.str 0 new_len;
ibuf.len <- new_len;
ibuf.bols <- [];
ibuf.start <- ibuf.start + ll
@@ -65,8 +65,8 @@ let prompt_char ic ibuf count =
try
let c = input_char ic in
if c == '\n' then ibuf.bols <- (ibuf.len+1) :: ibuf.bols;
- if ibuf.len == String.length ibuf.str then resize_buffer ibuf;
- ibuf.str.[ibuf.len] <- c;
+ if ibuf.len == Bytes.length ibuf.str then resize_buffer ibuf;
+ Bytes.set ibuf.str ibuf.len c;
ibuf.len <- ibuf.len + 1;
Some c
with End_of_file ->
@@ -75,7 +75,7 @@ let prompt_char ic ibuf count =
(* Reinitialize the char stream (after a Drop) *)
let reset_input_buffer ic ibuf =
- ibuf.str <- "";
+ ibuf.str <- Bytes.empty;
ibuf.len <- 0;
ibuf.bols <- [];
ibuf.tokens <- Gram.parsable (Stream.from (prompt_char ic ibuf));
@@ -109,19 +109,19 @@ let dotted_location (b,e) =
else
(String.make (e-b-1) '.', " ")
-let blanch_utf8_string s bp ep =
- let s' = String.make (ep-bp) ' ' in
+let blanch_utf8_string s bp ep = let open Bytes in
+ let s' = make (ep-bp) ' ' in
let j = ref 0 in
for i = bp to ep - 1 do
- let n = Char.code s.[i] in
+ let n = Char.code (get s i) in
(* Heuristic: assume utf-8 chars are printed using a single
fixed-size char and therefore contract all utf-8 code into one
space; in any case, preserve tabulation so
that its effective interpretation in terms of spacing is preserved *)
- if s.[i] == '\t' then s'.[!j] <- '\t';
+ if get s i == '\t' then set s' !j '\t';
if n < 0x80 || 0xC0 <= n then incr j
done;
- String.sub s' 0 !j
+ Bytes.sub_string s' 0 !j
let print_highlight_location ib loc =
let (bp,ep) = Loc.unloc loc in
@@ -132,17 +132,17 @@ let print_highlight_location ib loc =
| ([],(bl,el)) ->
let shift = blanch_utf8_string ib.str bl bp in
let span = String.length (blanch_utf8_string ib.str bp ep) in
- (str"> " ++ str(String.sub ib.str bl (el-bl-1)) ++ fnl () ++
+ (str"> " ++ str(Bytes.sub_string ib.str bl (el-bl-1)) ++ fnl () ++
str"> " ++ str(shift) ++ str(String.make span '^'))
| ((b1,e1)::ml,(bn,en)) ->
let (d1,s1) = dotted_location (b1,bp) in
let (dn,sn) = dotted_location (ep,en) in
let l1 = (str"> " ++ str d1 ++ str s1 ++
- str(String.sub ib.str bp (e1-bp))) in
+ str(Bytes.sub_string ib.str bp (e1-bp))) in
let li =
prlist (fun (bi,ei) ->
- (str"> " ++ str(String.sub ib.str bi (ei-bi)))) ml in
- let ln = (str"> " ++ str(String.sub ib.str bn (ep-bn)) ++
+ (str"> " ++ str(Bytes.sub_string ib.str bi (ei-bi)))) ml in
+ let ln = (str"> " ++ str(Bytes.sub_string ib.str bn (ep-bn)) ++
str sn ++ str dn) in
(l1 ++ li ++ ln)
in
@@ -220,7 +220,7 @@ let top_buffer =
^ emacs_prompt_endstring()
in
{ prompt = pr;
- str = "";
+ str = Bytes.empty;
len = 0;
bols = [];
tokens = Gram.parsable (Stream.of_list []);
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index e40353e0f..d248f2f70 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -15,7 +15,7 @@ open Pp
type input_buffer = {
mutable prompt : unit -> string;
- mutable str : string; (** buffer of already read characters *)
+ mutable str : Bytes.t; (** buffer of already read characters *)
mutable len : int; (** number of chars in the buffer *)
mutable bols : int list; (** offsets in str of begining of lines *)
mutable tokens : Pcoq.Gram.coq_parsable; (** stream of tokens *)
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index f914f83b9..b73321c00 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -108,7 +108,7 @@ let verbose_phrase verbch loc =
let s = Bytes.create len in
seek_in ch (fst loc);
really_input ch s 0 len;
- Feedback.msg_notice (str s)
+ Feedback.msg_notice (str (Bytes.to_string s))
| None -> ()
exception End_of_input
@@ -126,7 +126,7 @@ let chan_beautify = ref stdout
let beautify_suffix = ".beautified"
let set_formatter_translator ch =
- let out s b e = output ch s b e in
+ let out s b e = output_substring ch s b e in
Format.set_formatter_output_functions out (fun () -> flush ch);
Format.set_max_boxes max_int
@@ -161,13 +161,11 @@ let pr_new_syntax po loc chan_beautify ocom =
let pp_cmd_header loc com =
let shorten s = try (String.sub s 0 30)^"..." with _ -> s in
- let noblank s =
- for i = 0 to Bytes.length s - 1 do
- match s.[i] with
- | ' ' | '\n' | '\t' | '\r' -> s.[i] <- '~'
- | _ -> ()
- done;
- s
+ let noblank s = String.map (fun c ->
+ match c with
+ | ' ' | '\n' | '\t' | '\r' -> '~'
+ | x -> x
+ ) s
in
let (start,stop) = Loc.unloc loc in
let safe_pr_vernac x =
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 03:01:29 +0000