author | wenzelm |
Fri, 26 Oct 2001 23:58:21 +0200 | |
changeset 11952 | b10f1e8862f4 |
parent 10909 | 2bbb1797bbe2 |
permissions | -rw-r--r-- |
5121 | 1 |
(* Title: HOL/String.thy |
2 |
ID: $Id$ |
|
10732 | 3 |
Author: Markus Wenzel, TU Muenchen |
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
5121 | 5 |
|
6 |
Hex chars and strings. |
|
7 |
*) |
|
8 |
||
10909
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
9 |
theory String = List: |
5121 | 10 |
|
10732 | 11 |
datatype nibble = |
10909
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
12 |
Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7 |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
13 |
| Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF |
5121 | 14 |
|
10732 | 15 |
datatype char = Char nibble nibble |
10909
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
16 |
-- "Note: canonical order of character encoding coincides with standard term ordering" |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
17 |
|
10732 | 18 |
types string = "char list" |
5121 | 19 |
|
20 |
syntax |
|
10732 | 21 |
"_Char" :: "xstr => char" ("CHR _") |
22 |
"_String" :: "xstr => string" ("_") |
|
23 |
||
10909
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
24 |
parse_ast_translation {* |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
25 |
let |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
26 |
val constants = Syntax.Appl o map Syntax.Constant; |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
27 |
|
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
28 |
fun mk_nib n = "Nibble" ^ chr (n + (if n <= 9 then ord "0" else ord "A" - 10)); |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
29 |
fun mk_char c = |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
30 |
if Symbol.is_ascii c andalso Symbol.is_printable c then |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
31 |
constants ["Char", mk_nib (ord c div 16), mk_nib (ord c mod 16)] |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
32 |
else error ("Printable ASCII character expected: " ^ quote c); |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
33 |
|
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
34 |
fun mk_string [] = Syntax.Constant "Nil" |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
35 |
| mk_string (c :: cs) = Syntax.Appl [Syntax.Constant "Cons", mk_char c, mk_string cs]; |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
36 |
|
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
37 |
fun char_ast_tr [Syntax.Variable xstr] = |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
38 |
(case Syntax.explode_xstr xstr of |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
39 |
[c] => mk_char c |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
40 |
| _ => error ("Single character expected: " ^ xstr)) |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
41 |
| char_ast_tr asts = raise AST ("char_ast_tr", asts); |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
42 |
|
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
43 |
fun string_ast_tr [Syntax.Variable xstr] = |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
44 |
(case Syntax.explode_xstr xstr of |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
45 |
[] => constants [Syntax.constrainC, "Nil", "string"] |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
46 |
| cs => mk_string cs) |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
47 |
| string_ast_tr asts = raise AST ("string_tr", asts); |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
48 |
in [("_Char", char_ast_tr), ("_String", string_ast_tr)] end; |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
49 |
*} |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
50 |
|
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
51 |
print_ast_translation {* |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
52 |
let |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
53 |
fun dest_nib (Syntax.Constant c) = |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
54 |
(case explode c of |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
55 |
["N", "i", "b", "b", "l", "e", h] => |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
56 |
if "0" <= h andalso h <= "9" then ord h - ord "0" |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
57 |
else if "A" <= h andalso h <= "F" then ord h - ord "A" + 10 |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
58 |
else raise Match |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
59 |
| _ => raise Match) |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
60 |
| dest_nib _ = raise Match; |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
61 |
|
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
62 |
fun dest_chr c1 c2 = |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
63 |
let val c = chr (dest_nib c1 * 16 + dest_nib c2) |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
64 |
in if Symbol.is_printable c then c else raise Match end; |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
65 |
|
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
66 |
fun dest_char (Syntax.Appl [Syntax.Constant "Char", c1, c2]) = dest_chr c1 c2 |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
67 |
| dest_char _ = raise Match; |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
68 |
|
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
69 |
fun xstr cs = Syntax.Appl [Syntax.Constant "_xstr", Syntax.Variable (Syntax.implode_xstr cs)]; |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
70 |
|
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
71 |
fun char_ast_tr' [c1, c2] = Syntax.Appl [Syntax.Constant "_Char", xstr [dest_chr c1 c2]] |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
72 |
| char_ast_tr' _ = raise Match; |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
73 |
|
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
74 |
fun list_ast_tr' [args] = Syntax.Appl [Syntax.Constant "_String", |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
75 |
xstr (map dest_char (Syntax.unfold_ast "_args" args))] |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
76 |
| list_ast_tr' ts = raise Match; |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
77 |
in [("Char", char_ast_tr'), ("@list", list_ast_tr')] end; |
2bbb1797bbe2
improved string syntax (allow translation rules);
wenzelm
parents:
10732
diff
changeset
|
78 |
*} |
5121 | 79 |
|
80 |
end |