src/HOL/Library/Code_Char.thy
 author Manuel Eberl Mon Mar 26 16:14:16 2018 +0200 (18 months ago) changeset 67951 655aa11359dc parent 65884 d76937b773d9 permissions -rw-r--r--
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
1 (*  Title:      HOL/Library/Code_Char.thy
2     Author:     Florian Haftmann
3 *)
5 section \<open>Code generation of pretty characters (and strings)\<close>
7 theory Code_Char
8 imports Main Char_ord
9 begin
11 code_printing
12   type_constructor char \<rightharpoonup>
13     (SML) "char"
14     and (OCaml) "char"
15     and (Haskell) "Prelude.Char"
16     and (Scala) "Char"
18 setup \<open>
19   fold String_Code.add_literal_char ["SML", "OCaml", "Haskell", "Scala"]
21 \<close>
23 code_printing
24   constant integer_of_char \<rightharpoonup>
25     (SML) "!(IntInf.fromInt o Char.ord)"
26     and (OCaml) "Big'_int.big'_int'_of'_int (Char.code _)"
27     and (Haskell) "Prelude.toInteger (Prelude.fromEnum (_ :: Prelude.Char))"
28     and (Scala) "BigInt(_.toInt)"
29 | constant char_of_integer \<rightharpoonup>
30     (SML) "!(Char.chr o IntInf.toInt)"
31     and (OCaml) "Char.chr (Big'_int.int'_of'_big'_int _)"
32     and (Haskell) "!(let chr k | (0 <= k && k < 256) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)"
33     and (Scala) "!((k: BigInt) => if (BigInt(0) <= k && k < BigInt(256)) k.charValue else sys.error(\"character value out of range\"))"
34 | class_instance char :: equal \<rightharpoonup>
36 | constant "HOL.equal :: char \<Rightarrow> char \<Rightarrow> bool" \<rightharpoonup>
37     (SML) "!((_ : char) = _)"
38     and (OCaml) "!((_ : char) = _)"
39     and (Haskell) infix 4 "=="
40     and (Scala) infixl 5 "=="
41 | constant "Code_Evaluation.term_of :: char \<Rightarrow> term" \<rightharpoonup>
42     (Eval) "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))"
44 code_reserved SML
45   char
47 code_reserved OCaml
48   char
50 code_reserved Scala
51   char
53 code_reserved SML String
55 code_printing
56   constant String.implode \<rightharpoonup>
57     (SML) "String.implode"
58     and (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)"
59     and (Haskell) "_"
60     and (Scala) "!(\"\" ++/ _)"
61 | constant String.explode \<rightharpoonup>
62     (SML) "String.explode"
63     and (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) [])"
64     and (Haskell) "_"
65     and (Scala) "!(_.toList)"
67 code_printing
68   constant "Orderings.less_eq :: char \<Rightarrow> char \<Rightarrow> bool" \<rightharpoonup>
69     (SML) "!((_ : char) <= _)"
70     and (OCaml) "!((_ : char) <= _)"
71     and (Haskell) infix 4 "<="
72     and (Scala) infixl 4 "<="
73     and (Eval) infixl 6 "<="
74 | constant "Orderings.less :: char \<Rightarrow> char \<Rightarrow> bool" \<rightharpoonup>
75     (SML) "!((_ : char) < _)"
76     and (OCaml) "!((_ : char) < _)"
77     and (Haskell) infix 4 "<"
78     and (Scala) infixl 4 "<"
79     and (Eval) infixl 6 "<"
80 |  constant "Orderings.less_eq :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
81     (SML) "!((_ : string) <= _)"
82     and (OCaml) "!((_ : string) <= _)"
83     \<comment> \<open>Order operations for @{typ String.literal} work in Haskell only
84           if no type class instance needs to be generated, because String = [Char] in Haskell
85           and @{typ "char list"} need not have the same order as @{typ String.literal}.\<close>
86     and (Haskell) infix 4 "<="
87     and (Scala) infixl 4 "<="
88     and (Eval) infixl 6 "<="
89 | constant "Orderings.less :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
90     (SML) "!((_ : string) < _)"
91     and (OCaml) "!((_ : string) < _)"
92     and (Haskell) infix 4 "<"
93     and (Scala) infixl 4 "<"
94     and (Eval) infixl 6 "<"
96 end