From e78717780b729f9a69d908afd9da156fffddfe52 Mon Sep 17 00:00:00 2001
From: Xavier Leroy
Date: Sun, 8 Dec 2019 19:20:21 +0100
Subject: Reimplement string <-> char list conversions

Using only OCaml stdlib functions available in OCaml 4.05.
---
 plugins/extraction/ExtrOcamlNativeString.v | 16 +++++++++++-----
 1 file changed, 11 insertions(+), 5 deletions(-)

(limited to 'plugins')

diff --git a/plugins/extraction/ExtrOcamlNativeString.v b/plugins/extraction/ExtrOcamlNativeString.v
index 45d3ef3d3c..77a16c9524 100644
--- a/plugins/extraction/ExtrOcamlNativeString.v
+++ b/plugins/extraction/ExtrOcamlNativeString.v
@@ -76,15 +76,21 @@ Extract Inlined Constant String.prefix =>
      let l1 = String.length s1 and l2 = String.length s2 in
      l1 <= l2 && String.sub s2 0 l1 = s1)".
 Extract Inlined Constant String.string_of_list_ascii =>
-  "(fun l => String.of_seq (List.to_seq l))".
+  "(fun l ->
+      let a = Array.of_list l in
+      String.init (Array.length a) (fun i -> a.(i)))".
 Extract Inlined Constant String.list_ascii_of_string =>
-  "(fun s => List.of_seq (String.to_seq s))".
+  "(fun s ->
+      Array.to_list (Array.init (String.length s) (fun i -> s.[i])))".
 Extract Inlined Constant String.string_of_list_byte =>
-  "(fun l => String.of_seq (List.to_seq l))".
+  "(fun l ->
+      let a = Array.of_list l in
+      String.init (Array.length a) (fun i -> a.(i)))".
 Extract Inlined Constant String.list_byte_of_string =>
-  "(fun s => List.of_seq (String.to_seq s))".
+  "(fun s ->
+      Array.to_list (Array.init (String.length s) (fun i -> s.[i])))".
 
-(* Other operations in module String:
+(* Other operations in module String (at the time of this writing):
       String.length
       String.get
       String.substring
-- 
cgit v1.2.3