author | wenzelm |
Tue, 05 Apr 2011 14:25:18 +0200 | |
changeset 42224 | 578a51fae383 |
parent 40627 | becf5d5187cc |
child 42248 | 04bffad68aa4 |
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 |
||
35123 | 12 |
structure String_Syntax: STRING_SYNTAX = |
21759 | 13 |
struct |
14 |
||
15 |
||
16 |
(* nibble *) |
|
17 |
||
18 |
val mk_nib = |
|
42224
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
40627
diff
changeset
|
19 |
Ast.Constant o Syntax.mark_const o |
35123 | 20 |
fst o Term.dest_Const o HOLogic.mk_nibble; |
21759 | 21 |
|
42224
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
40627
diff
changeset
|
22 |
fun dest_nib (Ast.Constant s) = |
35262
9ea4445d2ccf
slightly more abstract syntax mark/unmark operations;
wenzelm
parents:
35256
diff
changeset
|
23 |
(case try Syntax.unmark_const s of |
35256 | 24 |
NONE => raise Match |
25 |
| SOME c => (HOLogic.dest_nibble (Const (c, HOLogic.nibbleT)) handle TERM _ => raise Match)); |
|
21759 | 26 |
|
27 |
||
28 |
(* char *) |
|
29 |
||
30 |
fun mk_char s = |
|
31 |
if Symbol.is_ascii s then |
|
42224
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
40627
diff
changeset
|
32 |
Ast.Appl [Ast.Constant @{const_syntax Char}, mk_nib (ord s div 16), mk_nib (ord s mod 16)] |
21759 | 33 |
else error ("Non-ASCII symbol: " ^ quote s); |
34 |
||
40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
35363
diff
changeset
|
35 |
val specials = raw_explode "\\\"`'"; |
21759 | 36 |
|
37 |
fun dest_chr c1 c2 = |
|
38 |
let val c = chr (dest_nib c1 * 16 + dest_nib c2) in |
|
39 |
if not (member (op =) specials c) andalso Symbol.is_ascii c andalso Symbol.is_printable c |
|
40 |
then c else raise Match |
|
41 |
end; |
|
42 |
||
42224
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
40627
diff
changeset
|
43 |
fun dest_char (Ast.Appl [Ast.Constant @{const_syntax Char}, c1, c2]) = dest_chr c1 c2 |
21759 | 44 |
| dest_char _ = raise Match; |
45 |
||
29317 | 46 |
fun syntax_string cs = |
42224
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
40627
diff
changeset
|
47 |
Ast.Appl [Ast.Constant @{syntax_const "_inner_string"}, Ast.Variable (Syntax.implode_xstr cs)]; |
21759 | 48 |
|
49 |
||
42224
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
40627
diff
changeset
|
50 |
fun char_ast_tr [Ast.Variable xstr] = |
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
40627
diff
changeset
|
51 |
(case Syntax.explode_xstr xstr of |
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
40627
diff
changeset
|
52 |
[c] => mk_char c |
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
40627
diff
changeset
|
53 |
| _ => error ("Single character expected: " ^ xstr)) |
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
40627
diff
changeset
|
54 |
| char_ast_tr asts = raise Ast.AST ("char_ast_tr", asts); |
21759 | 55 |
|
35115 | 56 |
fun char_ast_tr' [c1, c2] = |
42224
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
40627
diff
changeset
|
57 |
Ast.Appl [Ast.Constant @{syntax_const "_Char"}, syntax_string [dest_chr c1 c2]] |
21759 | 58 |
| char_ast_tr' _ = raise Match; |
59 |
||
60 |
||
61 |
(* string *) |
|
62 |
||
42224
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
40627
diff
changeset
|
63 |
fun mk_string [] = Ast.Constant @{const_syntax Nil} |
35115 | 64 |
| mk_string (c :: cs) = |
42224
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
40627
diff
changeset
|
65 |
Ast.Appl [Ast.Constant @{const_syntax Cons}, mk_char c, mk_string cs]; |
21759 | 66 |
|
42224
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
40627
diff
changeset
|
67 |
fun string_ast_tr [Ast.Variable xstr] = |
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
40627
diff
changeset
|
68 |
(case Syntax.explode_xstr xstr of |
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
40627
diff
changeset
|
69 |
[] => |
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
40627
diff
changeset
|
70 |
Ast.Appl |
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
40627
diff
changeset
|
71 |
[Ast.Constant Syntax.constrainC, |
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
40627
diff
changeset
|
72 |
Ast.Constant @{const_syntax Nil}, Ast.Constant @{type_syntax string}] |
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
40627
diff
changeset
|
73 |
| cs => mk_string cs) |
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
40627
diff
changeset
|
74 |
| string_ast_tr asts = raise Ast.AST ("string_tr", asts); |
21759 | 75 |
|
35115 | 76 |
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
|
77 |
Ast.Appl [Ast.Constant @{syntax_const "_String"}, |
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
40627
diff
changeset
|
78 |
syntax_string (map dest_char (Ast.unfold_ast @{syntax_const "_args"} args))] |
21759 | 79 |
| list_ast_tr' ts = raise Match; |
80 |
||
81 |
||
82 |
(* theory setup *) |
|
83 |
||
84 |
val setup = |
|
24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
21775
diff
changeset
|
85 |
Sign.add_trfuns |
35115 | 86 |
([(@{syntax_const "_Char"}, char_ast_tr), (@{syntax_const "_String"}, string_ast_tr)], [], [], |
87 |
[(@{const_syntax Char}, char_ast_tr'), (@{syntax_const "_list"}, list_ast_tr')]); |
|
21759 | 88 |
|
89 |
end; |