208
|
1 |
(* Title: HOL/String.thy
|
|
2 |
ID: $Id$
|
|
3 |
|
|
4 |
Hex chars. 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 |
open Syntax;
|
|
30 |
|
|
31 |
val ssquote = enclose "''" "''";
|
|
32 |
|
|
33 |
|
|
34 |
(* chars *)
|
|
35 |
|
|
36 |
val zero = ord "0";
|
|
37 |
val ten = ord "A" - 10;
|
|
38 |
|
|
39 |
fun mk_nib n =
|
|
40 |
const ("H0" ^ chr (n + (if n <= 9 then zero else ten)));
|
|
41 |
|
|
42 |
fun dest_nib (Const (c, _)) =
|
|
43 |
(case explode c of
|
|
44 |
["H", "0", h] => ord h - (if h <= "9" then zero else ten)
|
|
45 |
| _ => raise Match)
|
|
46 |
| dest_nib _ = raise Match;
|
|
47 |
|
|
48 |
fun dest_nibs t1 t2 = chr (dest_nib t1 * 16 + dest_nib t2);
|
|
49 |
|
|
50 |
|
|
51 |
fun mk_char c =
|
|
52 |
const "Char" $ mk_nib (ord c div 16) $ mk_nib (ord c mod 16);
|
|
53 |
|
|
54 |
fun dest_char (Const ("Char", _) $ t1 $ t2) = dest_nibs t1 t2
|
|
55 |
| dest_char _ = raise Match;
|
|
56 |
|
|
57 |
|
|
58 |
fun char_tr (*"_Char"*) [Free (c, _)] =
|
|
59 |
if size c = 1 then mk_char c
|
|
60 |
else error ("Bad character: " ^ quote c)
|
|
61 |
| char_tr (*"_Char"*) ts = raise_term "char_tr" ts;
|
|
62 |
|
|
63 |
fun char_tr' (*"Char"*) [t1, t2] =
|
|
64 |
const "_Char" $ free (ssquote (dest_nibs t1 t2))
|
|
65 |
| char_tr' (*"Char"*) _ = raise Match;
|
|
66 |
|
|
67 |
|
|
68 |
(* strings *)
|
|
69 |
|
|
70 |
fun mk_string [] = const constrainC $ const "[]" $ const "string"
|
|
71 |
| mk_string (t :: ts) = const "op #" $ t $ mk_string ts;
|
|
72 |
|
|
73 |
fun dest_string (Const ("[]", _)) = []
|
|
74 |
| dest_string (Const ("op #", _) $ c $ cs) = dest_char c :: dest_string cs
|
|
75 |
| dest_string _ = raise Match;
|
|
76 |
|
|
77 |
|
|
78 |
fun string_tr (*"_String"*) [Free (txt, _)] =
|
|
79 |
mk_string (map mk_char (explode txt))
|
|
80 |
| string_tr (*"_String"*) ts = raise_term "string_tr" ts;
|
|
81 |
|
|
82 |
fun cons_tr' (*"op #"*) [c, cs] =
|
|
83 |
const "_String" $ free (ssquote (implode (dest_char c :: dest_string cs)))
|
|
84 |
| cons_tr' (*"op #"*) ts = raise Match;
|
|
85 |
|
|
86 |
in
|
|
87 |
val parse_translation = [("_Char", char_tr), ("_String", string_tr)];
|
|
88 |
val print_translation = [("Char", char_tr'), ("op #", cons_tr')];
|
|
89 |
end;
|
|
90 |
|