1 (* Title: HOL/String.thy |
|
2 ID: $Id$ |
|
3 |
|
4 Hex chars and strings. |
|
5 *) |
|
6 |
|
7 String = List + |
|
8 |
|
9 datatype |
|
10 nibble = H00 | H01 | H02 | H03 | H04 | H05 | H06 | H07 |
|
11 | H08 | H09 | H0A | H0B | H0C | H0D | H0E | H0F |
|
12 |
|
13 datatype |
|
14 char = Char nibble nibble |
|
15 |
|
16 types |
|
17 string = char list |
|
18 |
|
19 syntax |
|
20 "_Char" :: xstr => char ("CHR _") |
|
21 "_String" :: xstr => string ("_") |
|
22 |
|
23 end |
|
24 |
|
25 |
|
26 ML |
|
27 |
|
28 local |
|
29 |
|
30 (* chars *) |
|
31 |
|
32 val zero = ord "0"; |
|
33 val ten = ord "A" - 10; |
|
34 |
|
35 fun mk_nib n = |
|
36 Syntax.const ("H0" ^ chr (n + (if n <= 9 then zero else ten))); |
|
37 |
|
38 fun dest_nib (Const (c, _)) = |
|
39 (case explode c of |
|
40 ["H", "0", h] => ord h - (if h <= "9" then zero else ten) |
|
41 | _ => raise Match) |
|
42 | dest_nib _ = raise Match; |
|
43 |
|
44 fun dest_nibs t1 t2 = chr (dest_nib t1 * 16 + dest_nib t2); |
|
45 |
|
46 |
|
47 fun mk_char c = |
|
48 Syntax.const "Char" $ mk_nib (ord c div 16) $ mk_nib (ord c mod 16); |
|
49 |
|
50 fun dest_char (Const ("Char", _) $ t1 $ t2) = dest_nibs t1 t2 |
|
51 | dest_char _ = raise Match; |
|
52 |
|
53 |
|
54 fun char_tr (*"_Char"*) [Free (xstr, _)] = |
|
55 (case Syntax.explode_xstr xstr of |
|
56 [c] => mk_char c |
|
57 | _ => error ("Single character expected: " ^ xstr)) |
|
58 | char_tr (*"_Char"*) ts = raise TERM ("char_tr", ts); |
|
59 |
|
60 fun char_tr' (*"Char"*) [t1, t2] = |
|
61 Syntax.const "_Char" $ Syntax.free (Syntax.implode_xstr [dest_nibs t1 t2]) |
|
62 | char_tr' (*"Char"*) _ = raise Match; |
|
63 |
|
64 |
|
65 (* strings *) |
|
66 |
|
67 fun mk_string [] = Syntax.const Syntax.constrainC $ Syntax.const "[]" $ Syntax.const "string" |
|
68 | mk_string (t :: ts) = Syntax.const "op #" $ t $ mk_string ts; |
|
69 |
|
70 fun dest_string (Const ("[]", _)) = [] |
|
71 | dest_string (Const ("op #", _) $ c $ cs) = dest_char c :: dest_string cs |
|
72 | dest_string _ = raise Match; |
|
73 |
|
74 |
|
75 fun string_tr (*"_String"*) [Free (xstr, _)] = |
|
76 mk_string (map mk_char (Syntax.explode_xstr xstr)) |
|
77 | string_tr (*"_String"*) ts = raise TERM ("string_tr", ts); |
|
78 |
|
79 fun cons_tr' (*"op #"*) [c, cs] = |
|
80 Syntax.const "_String" $ |
|
81 Syntax.free (Syntax.implode_xstr (dest_char c :: dest_string cs)) |
|
82 | cons_tr' (*"op #"*) ts = raise Match; |
|
83 |
|
84 in |
|
85 val parse_translation = [("_Char", char_tr), ("_String", string_tr)]; |
|
86 val print_translation = [("Char", char_tr'), ("op #", cons_tr')]; |
|
87 end; |
|