author | wenzelm |
Fri, 02 Jan 2009 19:30:12 +0100 | |
changeset 29317 | 9faf1dfb4e7c |
parent 24712 | 64ed05609568 |
child 31048 | ac146fc38b51 |
permissions | -rw-r--r-- |
21759 | 1 |
(* Title: HOL/Tools/string_syntax.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
Concrete syntax for hex chars and strings. |
|
5 |
*) |
|
6 |
||
7 |
signature STRING_SYNTAX = |
|
8 |
sig |
|
9 |
val setup: theory -> theory |
|
10 |
end; |
|
11 |
||
12 |
structure StringSyntax: STRING_SYNTAX = |
|
13 |
struct |
|
14 |
||
15 |
||
16 |
(* nibble *) |
|
17 |
||
18 |
val mk_nib = |
|
19 |
Syntax.Constant o unprefix "List.nibble." o |
|
20 |
fst o Term.dest_Const o HOLogic.mk_nibble; |
|
21 |
||
22 |
fun dest_nib (Syntax.Constant c) = |
|
23 |
HOLogic.dest_nibble (Const ("List.nibble." ^ c, dummyT)) |
|
24 |
handle TERM _ => raise Match; |
|
25 |
||
26 |
||
27 |
(* char *) |
|
28 |
||
29 |
fun mk_char s = |
|
30 |
if Symbol.is_ascii s then |
|
31 |
Syntax.Appl [Syntax.Constant "Char", mk_nib (ord s div 16), mk_nib (ord s mod 16)] |
|
32 |
else error ("Non-ASCII symbol: " ^ quote s); |
|
33 |
||
21775 | 34 |
val specials = explode "\\\"`'"; |
21759 | 35 |
|
36 |
fun dest_chr c1 c2 = |
|
37 |
let val c = chr (dest_nib c1 * 16 + dest_nib c2) in |
|
38 |
if not (member (op =) specials c) andalso Symbol.is_ascii c andalso Symbol.is_printable c |
|
39 |
then c else raise Match |
|
40 |
end; |
|
41 |
||
42 |
fun dest_char (Syntax.Appl [Syntax.Constant "Char", c1, c2]) = dest_chr c1 c2 |
|
43 |
| dest_char _ = raise Match; |
|
44 |
||
29317 | 45 |
fun syntax_string cs = |
46 |
Syntax.Appl [Syntax.Constant "_inner_string", Syntax.Variable (Syntax.implode_xstr cs)]; |
|
21759 | 47 |
|
48 |
||
49 |
fun char_ast_tr [Syntax.Variable xstr] = |
|
50 |
(case Syntax.explode_xstr xstr of |
|
51 |
[c] => mk_char c |
|
52 |
| _ => error ("Single character expected: " ^ xstr)) |
|
53 |
| char_ast_tr asts = raise AST ("char_ast_tr", asts); |
|
54 |
||
29317 | 55 |
fun char_ast_tr' [c1, c2] = Syntax.Appl [Syntax.Constant "_Char", syntax_string [dest_chr c1 c2]] |
21759 | 56 |
| char_ast_tr' _ = raise Match; |
57 |
||
58 |
||
59 |
(* string *) |
|
60 |
||
61 |
fun mk_string [] = Syntax.Constant "Nil" |
|
62 |
| mk_string (c :: cs) = Syntax.Appl [Syntax.Constant "Cons", mk_char c, mk_string cs]; |
|
63 |
||
64 |
fun string_ast_tr [Syntax.Variable xstr] = |
|
65 |
(case Syntax.explode_xstr xstr of |
|
66 |
[] => Syntax.Appl |
|
67 |
[Syntax.Constant Syntax.constrainC, Syntax.Constant "Nil", Syntax.Constant "string"] |
|
68 |
| cs => mk_string cs) |
|
69 |
| string_ast_tr asts = raise AST ("string_tr", asts); |
|
70 |
||
71 |
fun list_ast_tr' [args] = Syntax.Appl [Syntax.Constant "_String", |
|
29317 | 72 |
syntax_string (map dest_char (Syntax.unfold_ast "_args" args))] |
21759 | 73 |
| list_ast_tr' ts = raise Match; |
74 |
||
75 |
||
76 |
(* theory setup *) |
|
77 |
||
78 |
val setup = |
|
24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
21775
diff
changeset
|
79 |
Sign.add_trfuns |
21759 | 80 |
([("_Char", char_ast_tr), ("_String", string_ast_tr)], [], [], |
81 |
[("Char", char_ast_tr'), ("@list", list_ast_tr')]); |
|
82 |
||
83 |
end; |