Extraction: avoid deprecated functions of module String

 - A few tweaks of string are now done via the Bytes module
 - lots of String.capitalize_ascii and co

5 files changed, 20 insertions, 18 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index de97ba97c..b93a76b96 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -92,9 +92,11 @@ 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
+    let b = Bytes.of_string s in
+    for i=0 to Bytes.length b - 1 do
+      if Bytes.get b i == '\'' then Bytes.set b i '~'
+    done;
+    Bytes.to_string b
 
 let rec qualify delim = function
   | [] -> assert false
@@ -110,12 +112,13 @@ let pseudo_qualify = qualify "__"
 let is_upper s = match s.[0] with 'A' .. 'Z' -> true | _ -> false
 let is_lower s = match s.[0] with 'a' .. 'z' | '_' -> true | _ -> false
 
-let lowercase_id id = Id.of_string (String.uncapitalize (ascii_of_id id))
+let lowercase_id id =
+  Id.of_string (String.uncapitalize_ascii (ascii_of_id id))
 let uppercase_id id =
   let s = ascii_of_id id in
   assert (not (String.is_empty s));
   if s.[0] == '_' then Id.of_string ("Coq_"^s)
-  else Id.of_string (String.capitalize s)
+  else Id.of_string (String.capitalize_ascii s)
 
 type kind = Term | Type | Cons | Mod
 
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index b8e95afb3..a6351fc4c 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -36,6 +36,9 @@ val pr_binding : Id.t list -> std_ppcmds
 
 val rename_id : Id.t -> Id.Set.t -> Id.t
 
+(** For Scheme extraction, replace the ['] by [~] *)
+val unquote : string -> string
+
 type env = Id.t list * Id.Set.t
 val empty_env : unit -> env
 
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 0692c88cd..83bb2e135 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -21,8 +21,8 @@ open Common
 
 (*s Haskell renaming issues. *)
 
-let pr_lower_id id = str (String.uncapitalize (Id.to_string id))
-let pr_upper_id id = str (String.capitalize (Id.to_string id))
+let pr_lower_id id = str (String.uncapitalize_ascii (Id.to_string id))
+let pr_upper_id id = str (String.capitalize_ascii (Id.to_string id))
 
 let keywords =
   List.fold_right (fun s -> Id.Set.add (Id.of_string s))
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index a6309e61f..3bd16138f 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -39,12 +39,7 @@ let preamble _ comment _ usf =
   str "(load \"macros_extr.scm\")\n\n" ++
   (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
+let pr_id id = str (unquote (Id.to_string id))
 
 let paren = pp_par true
 
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 5e7d810c9..a8d49ffda 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -55,7 +55,7 @@ let is_modfile = function
   | _ -> false
 
 let raw_string_of_modfile = function
-  | MPfile f -> String.capitalize (Id.to_string (List.hd (DirPath.repr f)))
+  | MPfile f -> String.capitalize_ascii (Id.to_string (List.hd (DirPath.repr f)))
   | _ -> assert false
 
 let is_toplevel mp =
@@ -773,13 +773,14 @@ 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
+  let s = Bytes.of_string (string_of_modfile mp) in
+  let () = Bytes.set s 0 (s0.[0]) in
+  Bytes.to_string s
 
 let add_blacklist_entries l =
   blacklist_table :=
-    List.fold_right (fun s -> Id.Set.add (Id.of_string (String.capitalize s)))
+    List.fold_right
+      (fun s -> Id.Set.add (Id.of_string (String.capitalize_ascii s)))
       l !blacklist_table
 
 (* Registration of operations for rollback. *)