author | haftmann |
Wed, 06 May 2009 16:01:23 +0200 | |
changeset 31051 | 4d9b52e0a48c |
child 31055 | 2cf6efca6c71 |
permissions | -rw-r--r-- |
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
1 |
(* Author: Tobias Nipkow, Florian Haftmann, TU Muenchen *) |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
2 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
3 |
header {* Character and string types *} |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
4 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
5 |
theory String |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
6 |
imports List |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
7 |
uses "Tools/string_syntax.ML" |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
8 |
begin |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
9 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
10 |
subsection {* Characters *} |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
11 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
12 |
datatype nibble = |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
13 |
Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7 |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
14 |
| Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
15 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
16 |
lemma UNIV_nibble: |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
17 |
"UNIV = {Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7, |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
18 |
Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF}" (is "_ = ?A") |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
19 |
proof (rule UNIV_eq_I) |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
20 |
fix x show "x \<in> ?A" by (cases x) simp_all |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
21 |
qed |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
22 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
23 |
instance nibble :: finite |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
24 |
by default (simp add: UNIV_nibble) |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
25 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
26 |
datatype char = Char nibble nibble |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
27 |
-- "Note: canonical order of character encoding coincides with standard term ordering" |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
28 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
29 |
lemma UNIV_char: |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
30 |
"UNIV = image (split Char) (UNIV \<times> UNIV)" |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
31 |
proof (rule UNIV_eq_I) |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
32 |
fix x show "x \<in> image (split Char) (UNIV \<times> UNIV)" by (cases x) auto |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
33 |
qed |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
34 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
35 |
instance char :: finite |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
36 |
by default (simp add: UNIV_char) |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
37 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
38 |
lemma size_char [code, simp]: |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
39 |
"size (c::char) = 0" by (cases c) simp |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
40 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
41 |
lemma char_size [code, simp]: |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
42 |
"char_size (c::char) = 0" by (cases c) simp |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
43 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
44 |
primrec nibble_pair_of_char :: "char \<Rightarrow> nibble \<times> nibble" where |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
45 |
"nibble_pair_of_char (Char n m) = (n, m)" |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
46 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
47 |
declare nibble_pair_of_char.simps [code del] |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
48 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
49 |
setup {* |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
50 |
let |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
51 |
val nibbles = map (Thm.cterm_of @{theory} o HOLogic.mk_nibble) (0 upto 15); |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
52 |
val thms = map_product |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
53 |
(fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps}) |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
54 |
nibbles nibbles; |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
55 |
in |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
56 |
PureThy.note_thmss Thm.lemmaK [((Binding.name "nibble_pair_of_char_simps", []), [(thms, [])])] |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
57 |
#-> (fn [(_, thms)] => fold_rev Code.add_eqn thms) |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
58 |
end |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
59 |
*} |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
60 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
61 |
lemma char_case_nibble_pair [code, code inline]: |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
62 |
"char_case f = split f o nibble_pair_of_char" |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
63 |
by (simp add: expand_fun_eq split: char.split) |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
64 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
65 |
lemma char_rec_nibble_pair [code, code inline]: |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
66 |
"char_rec f = split f o nibble_pair_of_char" |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
67 |
unfolding char_case_nibble_pair [symmetric] |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
68 |
by (simp add: expand_fun_eq split: char.split) |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
69 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
70 |
syntax |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
71 |
"_Char" :: "xstr => char" ("CHR _") |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
72 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
73 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
74 |
subsection {* Strings *} |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
75 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
76 |
types string = "char list" |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
77 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
78 |
syntax |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
79 |
"_String" :: "xstr => string" ("_") |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
80 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
81 |
setup StringSyntax.setup |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
82 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
83 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
84 |
subsection {* Strings as dedicated datatype *} |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
85 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
86 |
datatype message_string = STR string |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
87 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
88 |
lemmas [code del] = |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
89 |
message_string.recs message_string.cases |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
90 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
91 |
lemma [code]: "size (s\<Colon>message_string) = 0" |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
92 |
by (cases s) simp_all |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
93 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
94 |
lemma [code]: "message_string_size (s\<Colon>message_string) = 0" |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
95 |
by (cases s) simp_all |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
96 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
97 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
98 |
subsection {* Code generator *} |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
99 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
100 |
text {* This also covers pretty syntax for list literals. *} |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
101 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
102 |
ML {* |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
103 |
local |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
104 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
105 |
open Basic_Code_Thingol; |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
106 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
107 |
fun implode_list naming t = case pairself |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
108 |
(Code_Thingol.lookup_const naming) (@{const_name Nil}, @{const_name Cons}) |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
109 |
of (SOME nil', SOME cons') => let |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
110 |
fun dest_cons (IConst (c, _) `$ t1 `$ t2) = |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
111 |
if c = cons' |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
112 |
then SOME (t1, t2) |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
113 |
else NONE |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
114 |
| dest_cons _ = NONE; |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
115 |
val (ts, t') = Code_Thingol.unfoldr dest_cons t; |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
116 |
in case t' |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
117 |
of IConst (c, _) => if c = nil' then SOME ts else NONE |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
118 |
| _ => NONE |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
119 |
end |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
120 |
| _ => NONE |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
121 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
122 |
fun decode_char naming (IConst (c1, _), IConst (c2, _)) = (case map_filter |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
123 |
(Code_Thingol.lookup_const naming)[@{const_name Nibble0}, @{const_name Nibble1}, |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
124 |
@{const_name Nibble2}, @{const_name Nibble3}, |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
125 |
@{const_name Nibble4}, @{const_name Nibble5}, |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
126 |
@{const_name Nibble6}, @{const_name Nibble7}, |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
127 |
@{const_name Nibble8}, @{const_name Nibble9}, |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
128 |
@{const_name NibbleA}, @{const_name NibbleB}, |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
129 |
@{const_name NibbleC}, @{const_name NibbleD}, |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
130 |
@{const_name NibbleE}, @{const_name NibbleF}] |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
131 |
of nibbles' as [_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _] => let |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
132 |
fun idx c = find_index (curry (op =) c) nibbles'; |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
133 |
fun decode ~1 _ = NONE |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
134 |
| decode _ ~1 = NONE |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
135 |
| decode n m = SOME (chr (n * 16 + m)); |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
136 |
in decode (idx c1) (idx c2) end |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
137 |
| _ => NONE) |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
138 |
| decode_char _ _ = NONE |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
139 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
140 |
fun implode_string naming mk_char mk_string ts = case |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
141 |
Code_Thingol.lookup_const naming @{const_name Char} |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
142 |
of SOME char' => let |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
143 |
fun implode_char (IConst (c, _) `$ t1 `$ t2) = |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
144 |
if c = char' then decode_char naming (t1, t2) else NONE |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
145 |
| implode_char _ = NONE; |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
146 |
val ts' = map implode_char ts; |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
147 |
in if forall is_some ts' |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
148 |
then (SOME o Code_Printer.str o mk_string o implode o map_filter I) ts' |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
149 |
else NONE |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
150 |
end |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
151 |
| _ => NONE; |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
152 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
153 |
fun default_list (target_fxy, target_cons) pr fxy t1 t2 = |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
154 |
Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy [ |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
155 |
pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1, |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
156 |
Code_Printer.str target_cons, |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
157 |
pr (Code_Printer.INFX (target_fxy, Code_Printer.R)) t2 |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
158 |
]; |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
159 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
160 |
fun pretty_list literals = |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
161 |
let |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
162 |
val mk_list = Code_Printer.literal_list literals; |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
163 |
fun pretty pr naming thm vars fxy [(t1, _), (t2, _)] = |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
164 |
case Option.map (cons t1) (implode_list naming t2) |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
165 |
of SOME ts => mk_list (map (pr vars Code_Printer.NOBR) ts) |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
166 |
| NONE => default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2; |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
167 |
in (2, pretty) end; |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
168 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
169 |
fun pretty_list_string literals = |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
170 |
let |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
171 |
val mk_list = Code_Printer.literal_list literals; |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
172 |
val mk_char = Code_Printer.literal_char literals; |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
173 |
val mk_string = Code_Printer.literal_string literals; |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
174 |
fun pretty pr naming thm vars fxy [(t1, _), (t2, _)] = |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
175 |
case Option.map (cons t1) (implode_list naming t2) |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
176 |
of SOME ts => (case implode_string naming mk_char mk_string ts |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
177 |
of SOME p => p |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
178 |
| NONE => mk_list (map (pr vars Code_Printer.NOBR) ts)) |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
179 |
| NONE => default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2; |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
180 |
in (2, pretty) end; |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
181 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
182 |
fun pretty_char literals = |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
183 |
let |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
184 |
val mk_char = Code_Printer.literal_char literals; |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
185 |
fun pretty _ naming thm _ _ [(t1, _), (t2, _)] = |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
186 |
case decode_char naming (t1, t2) |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
187 |
of SOME c => (Code_Printer.str o mk_char) c |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
188 |
| NONE => Code_Printer.nerror thm "Illegal character expression"; |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
189 |
in (2, pretty) end; |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
190 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
191 |
fun pretty_message literals = |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
192 |
let |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
193 |
val mk_char = Code_Printer.literal_char literals; |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
194 |
val mk_string = Code_Printer.literal_string literals; |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
195 |
fun pretty _ naming thm _ _ [(t, _)] = |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
196 |
case implode_list naming t |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
197 |
of SOME ts => (case implode_string naming mk_char mk_string ts |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
198 |
of SOME p => p |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
199 |
| NONE => Code_Printer.nerror thm "Illegal message expression") |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
200 |
| NONE => Code_Printer.nerror thm "Illegal message expression"; |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
201 |
in (1, pretty) end; |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
202 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
203 |
in |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
204 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
205 |
fun add_literal_list target thy = |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
206 |
let |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
207 |
val pr = pretty_list (Code_Target.the_literals thy target); |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
208 |
in |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
209 |
thy |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
210 |
|> Code_Target.add_syntax_const target @{const_name Cons} (SOME pr) |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
211 |
end; |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
212 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
213 |
fun add_literal_list_string target thy = |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
214 |
let |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
215 |
val pr = pretty_list_string (Code_Target.the_literals thy target); |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
216 |
in |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
217 |
thy |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
218 |
|> Code_Target.add_syntax_const target @{const_name Cons} (SOME pr) |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
219 |
end; |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
220 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
221 |
fun add_literal_char target thy = |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
222 |
let |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
223 |
val pr = pretty_char (Code_Target.the_literals thy target); |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
224 |
in |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
225 |
thy |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
226 |
|> Code_Target.add_syntax_const target @{const_name Char} (SOME pr) |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
227 |
end; |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
228 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
229 |
fun add_literal_message str target thy = |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
230 |
let |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
231 |
val pr = pretty_message (Code_Target.the_literals thy target); |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
232 |
in |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
233 |
thy |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
234 |
|> Code_Target.add_syntax_const target str (SOME pr) |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
235 |
end; |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
236 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
237 |
end; |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
238 |
*} |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
239 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
240 |
setup {* |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
241 |
fold (fn target => add_literal_list target) ["SML", "OCaml", "Haskell"] |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
242 |
*} |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
243 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
244 |
code_type message_string |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
245 |
(SML "string") |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
246 |
(OCaml "string") |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
247 |
(Haskell "String") |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
248 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
249 |
setup {* |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
250 |
fold (fn target => add_literal_message @{const_name STR} target) |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
251 |
["SML", "OCaml", "Haskell"] |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
252 |
*} |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
253 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
254 |
code_instance message_string :: eq |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
255 |
(Haskell -) |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
256 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
257 |
code_const "eq_class.eq \<Colon> message_string \<Rightarrow> message_string \<Rightarrow> bool" |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
258 |
(SML "!((_ : string) = _)") |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
259 |
(OCaml "!((_ : string) = _)") |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
260 |
(Haskell infixl 4 "==") |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
261 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
262 |
code_reserved SML string |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
263 |
code_reserved OCaml string |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
264 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
265 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
266 |
types_code |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
267 |
"char" ("string") |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
268 |
attach (term_of) {* |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
269 |
val term_of_char = HOLogic.mk_char o ord; |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
270 |
*} |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
271 |
attach (test) {* |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
272 |
fun gen_char i = |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
273 |
let val j = random_range (ord "a") (Int.min (ord "a" + i, ord "z")) |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
274 |
in (chr j, fn () => HOLogic.mk_char j) end; |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
275 |
*} |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
276 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
277 |
setup {* |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
278 |
let |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
279 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
280 |
fun char_codegen thy defs dep thyname b t gr = |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
281 |
let |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
282 |
val i = HOLogic.dest_char t; |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
283 |
val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
284 |
(fastype_of t) gr; |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
285 |
in SOME (Codegen.str (ML_Syntax.print_string (chr i)), gr') |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
286 |
end handle TERM _ => NONE; |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
287 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
288 |
in Codegen.add_codegen "char_codegen" char_codegen end |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
289 |
*} |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
290 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
291 |
end |