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