# HG changeset patch
# User haftmann
# Date 1548454428 0
# Node ID 6a9a8ef5e4c604f5215323ce29ae9fbfa6a01a87
# Parent  170daa8170bee03662359b3fed565041ce03d1a5
prefer proper strings in OCaml

diff -r 170daa8170be -r 6a9a8ef5e4c6 NEWS
--- a/NEWS	Fri Jan 25 22:13:47 2019 +0000
+++ b/NEWS	Fri Jan 25 22:13:48 2019 +0000
@@ -84,6 +84,9 @@
 file-system. To get generated code dumped into output, use "file \<open>\<close>".
 Minor INCOMPATIBILITY.
 
+* Code generation for OCaml: proper strings are used for literals.
+Minor INCOMPATIBILITY.
+
 * Code generation for Haskell: code includes for Haskell must contain
 proper module frame, nothing is added magically any longer.
 INCOMPATIBILITY.
diff -r 170daa8170be -r 6a9a8ef5e4c6 src/HOL/String.thy
--- a/src/HOL/String.thy	Fri Jan 25 22:13:47 2019 +0000
+++ b/src/HOL/String.thy	Fri Jan 25 22:13:48 2019 +0000
@@ -648,14 +648,19 @@
     and (Scala) infixl 7 "+"
 | constant String.literal_of_asciis \<rightharpoonup>
     (SML) "!(String.implode/ o map (fn k => if 0 <= k andalso k < 128 then (Char.chr o IntInf.toInt) k else raise Fail \"Non-ASCII character in literal\"))"
-    and (OCaml) "!(let ks = _ in let res = Bytes.create (List.length ks) in let rec imp i = function | [] -> res | k :: ks ->
-      let l = Big'_int.int'_of'_big'_int k in if 0 <= l && l < 128 then Bytes.set res i (Char.chr l) else failwith \"Non-ASCII character in literal\"; imp (i + 1) ks in imp 0 ks)"
+    and (OCaml) "!(let xs = _
+      and chr k =
+        let l = Big'_int.int'_of'_big'_int k
+          in if 0 <= l && l < 128
+          then Char.chr l
+          else failwith \"Non-ASCII character in literal\"
+      in String.init (List.length xs) (List.nth (List.map chr xs)))"
     and (Haskell) "map/ (let chr k | (0 <= k && k < 128) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)"
     and (Scala) "\"\"/ ++/ _.map((k: BigInt) => if (BigInt(0) <= k && k < BigInt(128)) k.charValue else sys.error(\"Non-ASCII character in literal\"))"
 | constant String.asciis_of_literal \<rightharpoonup>
     (SML) "!(map (fn c => let val k = Char.ord c in if k < 128 then IntInf.fromInt k else raise Fail \"Non-ASCII character in literal\" end) /o String.explode)"
-    and (OCaml) "!(let s = _ in let rec exp i l = if i < 0 then l else exp (i - 1) (let k = Char.code (Bytes.get s i) in
-      if k < 128 then Big'_int.big'_int'_of'_int k :: l else failwith \"Non-ASCII character in literal\") in exp (Bytes.length s - 1) [])"
+    and (OCaml) "!(let s = _ in let rec exp i l = if i < 0 then l else exp (i - 1) (let k = Char.code (String.get s i) in
+      if k < 128 then Big'_int.big'_int'_of'_int k :: l else failwith \"Non-ASCII character in literal\") in exp (String.length s - 1) [])"
     and (Haskell) "map/ (let ord k | (k < 128) = Prelude.toInteger k in ord . (Prelude.fromEnum :: Prelude.Char -> Prelude.Int))"
     and (Scala) "!(_.toList.map(c => { val k: Int = c.toInt; if (k < 128) BigInt(k) else sys.error(\"Non-ASCII character in literal\") }))"
 | class_instance String.literal :: equal \<rightharpoonup>
@@ -668,10 +673,10 @@
 | constant "(\<le>) :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
     (SML) "!((_ : string) <= _)"
     and (OCaml) "!((_ : string) <= _)"
+    and (Haskell) infix 4 "<="
     \<comment> \<open>Order operations for \<^typ>\<open>String.literal\<close> work in Haskell only
           if no type class instance needs to be generated, because String = [Char] in Haskell
           and \<^typ>\<open>char list\<close> need not have the same order as \<^typ>\<open>String.literal\<close>.\<close>
-    and (Haskell) infix 4 "<="
     and (Scala) infixl 4 "<="
     and (Eval) infixl 6 "<="
 | constant "(<) :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
diff -r 170daa8170be -r 6a9a8ef5e4c6 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Fri Jan 25 22:13:47 2019 +0000
+++ b/src/Tools/Code/code_ml.ML	Fri Jan 25 22:13:48 2019 +0000
@@ -887,7 +887,7 @@
     (target_OCaml, {serializer = serializer_ocaml, literals = literals_ocaml,
       check = {env_var = "ISABELLE_OCAML",
         make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
-        make_command = fn _ => "\"$ISABELLE_OCAML\" -w pu nums.cma ROOT.ocaml"},
+        make_command = fn _ => "\"$ISABELLE_OCAML\" -w pu -safe-string nums.cma ROOT.ocaml"},
       evaluation_args = []})
   #> Code_Target.set_printings (Type_Constructor ("fun",
     [(target_SML, SOME (2, fun_syntax)), (target_OCaml, SOME (2, fun_syntax))]))