prefer proper strings in OCaml
authorhaftmann
Fri Jan 25 22:13:48 2019 +0000 (9 months ago)
changeset 697436a9a8ef5e4c6
parent 69742 170daa8170be
child 69744 bb0a354f6b46
prefer proper strings in OCaml
NEWS
src/HOL/String.thy
src/Tools/Code/code_ml.ML
     1.1 --- a/NEWS	Fri Jan 25 22:13:47 2019 +0000
     1.2 +++ b/NEWS	Fri Jan 25 22:13:48 2019 +0000
     1.3 @@ -84,6 +84,9 @@
     1.4  file-system. To get generated code dumped into output, use "file \<open>\<close>".
     1.5  Minor INCOMPATIBILITY.
     1.6  
     1.7 +* Code generation for OCaml: proper strings are used for literals.
     1.8 +Minor INCOMPATIBILITY.
     1.9 +
    1.10  * Code generation for Haskell: code includes for Haskell must contain
    1.11  proper module frame, nothing is added magically any longer.
    1.12  INCOMPATIBILITY.
     2.1 --- a/src/HOL/String.thy	Fri Jan 25 22:13:47 2019 +0000
     2.2 +++ b/src/HOL/String.thy	Fri Jan 25 22:13:48 2019 +0000
     2.3 @@ -648,14 +648,19 @@
     2.4      and (Scala) infixl 7 "+"
     2.5  | constant String.literal_of_asciis \<rightharpoonup>
     2.6      (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\"))"
     2.7 -    and (OCaml) "!(let ks = _ in let res = Bytes.create (List.length ks) in let rec imp i = function | [] -> res | k :: ks ->
     2.8 -      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)"
     2.9 +    and (OCaml) "!(let xs = _
    2.10 +      and chr k =
    2.11 +        let l = Big'_int.int'_of'_big'_int k
    2.12 +          in if 0 <= l && l < 128
    2.13 +          then Char.chr l
    2.14 +          else failwith \"Non-ASCII character in literal\"
    2.15 +      in String.init (List.length xs) (List.nth (List.map chr xs)))"
    2.16      and (Haskell) "map/ (let chr k | (0 <= k && k < 128) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)"
    2.17      and (Scala) "\"\"/ ++/ _.map((k: BigInt) => if (BigInt(0) <= k && k < BigInt(128)) k.charValue else sys.error(\"Non-ASCII character in literal\"))"
    2.18  | constant String.asciis_of_literal \<rightharpoonup>
    2.19      (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)"
    2.20 -    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
    2.21 -      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) [])"
    2.22 +    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
    2.23 +      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) [])"
    2.24      and (Haskell) "map/ (let ord k | (k < 128) = Prelude.toInteger k in ord . (Prelude.fromEnum :: Prelude.Char -> Prelude.Int))"
    2.25      and (Scala) "!(_.toList.map(c => { val k: Int = c.toInt; if (k < 128) BigInt(k) else sys.error(\"Non-ASCII character in literal\") }))"
    2.26  | class_instance String.literal :: equal \<rightharpoonup>
    2.27 @@ -668,10 +673,10 @@
    2.28  | constant "(\<le>) :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
    2.29      (SML) "!((_ : string) <= _)"
    2.30      and (OCaml) "!((_ : string) <= _)"
    2.31 +    and (Haskell) infix 4 "<="
    2.32      \<comment> \<open>Order operations for \<^typ>\<open>String.literal\<close> work in Haskell only
    2.33            if no type class instance needs to be generated, because String = [Char] in Haskell
    2.34            and \<^typ>\<open>char list\<close> need not have the same order as \<^typ>\<open>String.literal\<close>.\<close>
    2.35 -    and (Haskell) infix 4 "<="
    2.36      and (Scala) infixl 4 "<="
    2.37      and (Eval) infixl 6 "<="
    2.38  | constant "(<) :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
     3.1 --- a/src/Tools/Code/code_ml.ML	Fri Jan 25 22:13:47 2019 +0000
     3.2 +++ b/src/Tools/Code/code_ml.ML	Fri Jan 25 22:13:48 2019 +0000
     3.3 @@ -887,7 +887,7 @@
     3.4      (target_OCaml, {serializer = serializer_ocaml, literals = literals_ocaml,
     3.5        check = {env_var = "ISABELLE_OCAML",
     3.6          make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
     3.7 -        make_command = fn _ => "\"$ISABELLE_OCAML\" -w pu nums.cma ROOT.ocaml"},
     3.8 +        make_command = fn _ => "\"$ISABELLE_OCAML\" -w pu -safe-string nums.cma ROOT.ocaml"},
     3.9        evaluation_args = []})
    3.10    #> Code_Target.set_printings (Type_Constructor ("fun",
    3.11      [(target_SML, SOME (2, fun_syntax)), (target_OCaml, SOME (2, fun_syntax))]))