Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
adding code generation setup for String.implode and String.explode in OCaml (contributed by Andreas Lochbihler)
authorbulwahn
Mon, 02 May 2011 10:50:07 +0200
changeset 42598 85ca44488a29
parent 42597 20a99a0e65ed
child 42599 1a82b0400b2a
adding code generation setup for String.implode and String.explode in OCaml (contributed by Andreas Lochbihler)
src/HOL/Library/Code_Char.thy file | annotate | diff | comparison | revisions 
--- 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)")
isabelle