# HG changeset patch
# User bulwahn
# Date 1304326207 -7200
# Node ID 85ca44488a29bc43db043171d053ab90fcc74298
# Parent  20a99a0e65edc06098cd94cd06da53aff61f30b0
adding code generation setup for String.implode and String.explode in OCaml (contributed by Andreas Lochbihler)

diff -r 20a99a0e65ed -r 85ca44488a29 src/HOL/Library/Code_Char.thy
--- a/src/HOL/Library/Code_Char.thy	Mon May 02 01:20:28 2011 +0200
+++ b/src/HOL/Library/Code_Char.thy	Mon May 02 10:50:07 2011 +0200
@@ -48,13 +48,13 @@
 
 code_const implode
   (SML "String.implode")
-  (OCaml "failwith/ \"implode\"")
+  (OCaml "!(let l = _ in let res = String.create (List.length l) in let rec imp i = function | [] -> res | c :: l -> String.set res i c; imp (i + 1) l in imp 0 l)")
   (Haskell "_")
   (Scala "!(\"\" ++/ _)")
 
 code_const explode
   (SML "String.explode")
-  (OCaml "failwith/ \"explode\"")
+  (OCaml "!(let s = _ in let rec exp i l = if i < 0 then l else exp (i - 1) (String.get s i :: l) in exp (String.length s - 1) [])")
   (Haskell "_")
   (Scala "!(_.toList)")