author | paulson |
Thu, 25 Jun 1998 13:57:34 +0200 | |
changeset 5078 | 7b5ea59c0275 |
parent 4253 | 901f690e3a58 |
permissions | -rw-r--r-- |
969 | 1 |
(* Title: HOL/String.thy |
2 |
ID: $Id$ |
|
3 |
||
4253 | 4 |
Hex chars and strings. |
969 | 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 |
|
977
5d57287e5e1e
changed syntax of datatype declarations (curried types for constructor
clasohm
parents:
969
diff
changeset
|
14 |
char = Char nibble nibble |
969 | 15 |
|
16 |
types |
|
1384 | 17 |
string = char list |
969 | 18 |
|
19 |
syntax |
|
1376 | 20 |
"_Char" :: xstr => char ("CHR _") |
21 |
"_String" :: xstr => string ("_") |
|
969 | 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 = |
|
4253 | 36 |
Syntax.const ("H0" ^ chr (n + (if n <= 9 then zero else ten))); |
969 | 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 = |
|
4253 | 48 |
Syntax.const "Char" $ mk_nib (ord c div 16) $ mk_nib (ord c mod 16); |
969 | 49 |
|
50 |
fun dest_char (Const ("Char", _) $ t1 $ t2) = dest_nibs t1 t2 |
|
51 |
| dest_char _ = raise Match; |
|
52 |
||
53 |
||
4253 | 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)) |
|
3795 | 58 |
| char_tr (*"_Char"*) ts = raise TERM ("char_tr", ts); |
969 | 59 |
|
60 |
fun char_tr' (*"Char"*) [t1, t2] = |
|
4253 | 61 |
Syntax.const "_Char" $ Syntax.free (Syntax.implode_xstr [dest_nibs t1 t2]) |
969 | 62 |
| char_tr' (*"Char"*) _ = raise Match; |
63 |
||
64 |
||
65 |
(* strings *) |
|
66 |
||
4253 | 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; |
|
969 | 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 |
||
4253 | 75 |
fun string_tr (*"_String"*) [Free (xstr, _)] = |
76 |
mk_string (map mk_char (Syntax.explode_xstr xstr)) |
|
3795 | 77 |
| string_tr (*"_String"*) ts = raise TERM ("string_tr", ts); |
969 | 78 |
|
79 |
fun cons_tr' (*"op #"*) [c, cs] = |
|
4253 | 80 |
Syntax.const "_String" $ |
81 |
Syntax.free (Syntax.implode_xstr (dest_char c :: dest_string cs)) |
|
969 | 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; |