diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/ExtrOcamlNativeString.v | 16 |
1 files changed, 11 insertions, 5 deletions
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 |