From 3550120641c3b8d84290dc950e717aaf099775f9 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey <pierre.letouzey@inria.fr>
Date: Tue, 7 Feb 2017 23:28:36 +0100
Subject: Revert "Extraction: avoid deprecated functions of module String"

This reverts commit 69c4e7cfa0271f024b2178082e4be2e3ca3be263.

String.capitalize_ascii are only available for ocaml >= 4.03, sorry...
---
 plugins/extraction/common.ml  | 13 +++++--------
 plugins/extraction/common.mli |  3 ---
 plugins/extraction/haskell.ml |  4 ++--
 plugins/extraction/scheme.ml  |  7 ++++++-
 plugins/extraction/table.ml   | 11 +++++------
 5 files changed, 18 insertions(+), 20 deletions(-)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index b93a76b96..de97ba97c 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -92,11 +92,9 @@ let begins_with_CoqXX s =
 let unquote s =
   if lang () != Scheme then s
   else
-    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 s = String.copy s in
+    for i=0 to String.length s - 1 do if s.[i] == '\'' then s.[i] <- '~' done;
+    s
 
 let rec qualify delim = function
   | [] -> assert false
@@ -112,13 +110,12 @@ 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 (ascii_of_id id))
+let lowercase_id id = Id.of_string (String.uncapitalize (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_ascii s)
+  else Id.of_string (String.capitalize s)
 
 type kind = Term | Type | Cons | Mod
 
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index a6351fc4c..b8e95afb3 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -36,9 +36,6 @@ 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 83bb2e135..0692c88cd 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_ascii (Id.to_string id))
-let pr_upper_id id = str (String.capitalize_ascii (Id.to_string id))
+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 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 3bd16138f..a6309e61f 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -39,7 +39,12 @@ 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 = str (unquote (Id.to_string id))
+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 paren = pp_par true
 
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index a8d49ffda..5e7d810c9 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_ascii (Id.to_string (List.hd (DirPath.repr f)))
+  | MPfile f -> String.capitalize (Id.to_string (List.hd (DirPath.repr f)))
   | _ -> assert false
 
 let is_toplevel mp =
@@ -773,14 +773,13 @@ let file_of_modfile mp =
     | MPfile f -> Id.to_string (List.hd (DirPath.repr f))
     | _ -> assert false
   in
-  let s = Bytes.of_string (string_of_modfile mp) in
-  let () = Bytes.set s 0 (s0.[0]) in
-  Bytes.to_string s
+  let s = String.copy (string_of_modfile mp) in
+  if s.[0] != s0.[0] then s.[0] <- s0.[0];
+  s
 
 let add_blacklist_entries l =
   blacklist_table :=
-    List.fold_right
-      (fun s -> Id.Set.add (Id.of_string (String.capitalize_ascii s)))
+    List.fold_right (fun s -> Id.Set.add (Id.of_string (String.capitalize s)))
       l !blacklist_table
 
 (* Registration of operations for rollback. *)
-- 
cgit v1.2.3