author | haftmann |
Sat, 12 Mar 2016 22:04:52 +0100 | |
changeset 62597 | b3f2b8c906a6 |
parent 58822 | 90a5e981af3e |
child 68028 | 1f9f973eed2a |
permissions | -rw-r--r-- |
21759 | 1 |
(* Title: HOL/Tools/string_syntax.ML |
2 |
Author: Makarius |
|
3 |
||
62597 | 4 |
Concrete syntax for chars and strings. |
21759 | 5 |
*) |
6 |
||
58822 | 7 |
structure String_Syntax: sig end = |
21759 | 8 |
struct |
9 |
||
62597 | 10 |
(* numeral *) |
21759 | 11 |
|
62597 | 12 |
fun hex_digit n = if n = 10 then "A" |
13 |
else if n = 11 then "B" |
|
14 |
else if n = 12 then "C" |
|
15 |
else if n = 13 then "D" |
|
16 |
else if n = 14 then "E" |
|
17 |
else if n = 15 then "F" |
|
18 |
else string_of_int n; |
|
21759 | 19 |
|
62597 | 20 |
fun hex_prefix ms = "0x" ^ implode (replicate (2 - length ms) "0" @ ms); |
21 |
||
22 |
fun hex n = hex_prefix (map hex_digit (radixpand (16, n))); |
|
21759 | 23 |
|
24 |
||
25 |
(* char *) |
|
26 |
||
62597 | 27 |
fun mk_char_syntax n = |
28 |
if n = 0 then Syntax.const @{const_name Groups.zero} |
|
29 |
else Syntax.const @{const_syntax Char} $ Numeral.mk_num_syntax n; |
|
30 |
||
31 |
fun mk_char_syntax' c = |
|
32 |
if Symbol.is_ascii c then mk_char_syntax (ord c) |
|
33 |
else if c = "\<newline>" then mk_char_syntax 10 |
|
34 |
else error ("Bad character: " ^ quote c); |
|
35 |
||
36 |
fun plain_string_of str = |
|
37 |
map fst (Lexicon.explode_str (str, Position.none)); |
|
38 |
||
39 |
datatype character = Char of string | Ord of int | Unprintable; |
|
21759 | 40 |
|
40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
35363
diff
changeset
|
41 |
val specials = raw_explode "\\\"`'"; |
21759 | 42 |
|
62597 | 43 |
fun dest_char_syntax c = |
44 |
case try Numeral.dest_num_syntax c of |
|
45 |
SOME n => |
|
46 |
if n < 256 then |
|
47 |
let |
|
48 |
val s = chr n |
|
49 |
in |
|
50 |
if not (member (op =) specials s) andalso Symbol.is_ascii s andalso Symbol.is_printable s |
|
51 |
then Char s |
|
52 |
else if s = "\n" then Char "\<newline>" |
|
53 |
else Ord n |
|
54 |
end |
|
55 |
else Unprintable |
|
56 |
| NONE => Unprintable; |
|
21759 | 57 |
|
62597 | 58 |
fun dest_char_ast (Ast.Appl [Ast.Constant @{syntax_const "_Char"}, Ast.Constant s]) = |
59 |
plain_string_of s |
|
60 |
| dest_char_ast _ = raise Match; |
|
21759 | 61 |
|
62597 | 62 |
fun char_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = |
63 |
c $ char_tr [t] $ u |
|
64 |
| char_tr [Free (str, _)] = |
|
65 |
(case plain_string_of str of |
|
66 |
[c] => mk_char_syntax' c |
|
67 |
| _ => error ("Single character expected: " ^ str)) |
|
68 |
| char_tr ts = raise TERM ("char_tr", ts); |
|
21759 | 69 |
|
62597 | 70 |
fun char_ord_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = |
71 |
c $ char_ord_tr [t] $ u |
|
72 |
| char_ord_tr [Const (num, _)] = |
|
73 |
(mk_char_syntax o #value o Lexicon.read_num) num |
|
74 |
| char_ord_tr ts = raise TERM ("char_ord_tr", ts); |
|
21759 | 75 |
|
62597 | 76 |
fun char_tr' [t] = (case dest_char_syntax t of |
77 |
Char s => Syntax.const @{syntax_const "_Char"} $ |
|
78 |
Syntax.const (Lexicon.implode_str [s]) |
|
79 |
| Ord n => |
|
80 |
if n = 0 |
|
81 |
then Syntax.const @{const_syntax Groups.zero} |
|
82 |
else Syntax.const @{syntax_const "_Char_ord"} $ |
|
83 |
Syntax.free (hex n) |
|
84 |
| _ => raise Match) |
|
85 |
| char_tr' _ = raise Match; |
|
21759 | 86 |
|
87 |
||
88 |
(* string *) |
|
89 |
||
62597 | 90 |
fun mk_string_syntax [] = Syntax.const @{const_syntax Nil} |
91 |
| mk_string_syntax (c :: cs) = |
|
92 |
Syntax.const @{const_syntax Cons} $ mk_char_syntax' c $ mk_string_syntax cs; |
|
21759 | 93 |
|
62597 | 94 |
fun mk_string_ast ss = |
95 |
Ast.Appl [Ast.Constant @{syntax_const "_inner_string"}, |
|
96 |
Ast.Variable (Lexicon.implode_str ss)]; |
|
97 |
||
98 |
fun string_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = |
|
99 |
c $ string_tr [t] $ u |
|
100 |
| string_tr [Free (str, _)] = |
|
101 |
mk_string_syntax (plain_string_of str) |
|
102 |
| string_tr ts = raise TERM ("char_tr", ts); |
|
21759 | 103 |
|
35115 | 104 |
fun list_ast_tr' [args] = |
42224
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
40627
diff
changeset
|
105 |
Ast.Appl [Ast.Constant @{syntax_const "_String"}, |
62597 | 106 |
(mk_string_ast o maps dest_char_ast o Ast.unfold_ast @{syntax_const "_args"}) args] |
51160
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
46483
diff
changeset
|
107 |
| list_ast_tr' _ = raise Match; |
21759 | 108 |
|
109 |
||
110 |
(* theory setup *) |
|
111 |
||
58822 | 112 |
val _ = |
113 |
Theory.setup |
|
62597 | 114 |
(Sign.parse_translation |
115 |
[(@{syntax_const "_Char"}, K char_tr), |
|
116 |
(@{syntax_const "_Char_ord"}, K char_ord_tr), |
|
117 |
(@{syntax_const "_String"}, K string_tr)] #> |
|
118 |
Sign.print_translation |
|
119 |
[(@{const_syntax Char}, K char_tr')] #> |
|
58822 | 120 |
Sign.print_ast_translation |
62597 | 121 |
[(@{syntax_const "_list"}, K list_ast_tr')]); |
21759 | 122 |
|
123 |
end; |