adding code generation setup for String.implode and String.explode in OCaml (contributed by Andreas Lochbihler)
authorbulwahn
Mon May 02 10:50:07 2011 +0200 (2011-05-02)
changeset 4259885ca44488a29
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
     1.1 --- a/src/HOL/Library/Code_Char.thy	Mon May 02 01:20:28 2011 +0200
     1.2 +++ b/src/HOL/Library/Code_Char.thy	Mon May 02 10:50:07 2011 +0200
     1.3 @@ -48,13 +48,13 @@
     1.4  
     1.5  code_const implode
     1.6    (SML "String.implode")
     1.7 -  (OCaml "failwith/ \"implode\"")
     1.8 +  (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)")
     1.9    (Haskell "_")
    1.10    (Scala "!(\"\" ++/ _)")
    1.11  
    1.12  code_const explode
    1.13    (SML "String.explode")
    1.14 -  (OCaml "failwith/ \"explode\"")
    1.15 +  (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) [])")
    1.16    (Haskell "_")
    1.17    (Scala "!(_.toList)")
    1.18