10732
|
1 |
(* Title: HOL/Tools/string_syntax.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Markus Wenzel, TU Muenchen
|
|
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE)
|
|
5 |
|
|
6 |
Concrete syntax for hex chars and strings. Assumes consts and syntax
|
|
7 |
of theory HOL/String.
|
|
8 |
*)
|
|
9 |
|
|
10 |
signature STRING_SYNTAX =
|
|
11 |
sig
|
|
12 |
val setup: (theory -> theory) list
|
|
13 |
end;
|
|
14 |
|
|
15 |
structure StringSyntax: STRING_SYNTAX =
|
|
16 |
struct
|
|
17 |
|
|
18 |
|
|
19 |
(* chars *)
|
|
20 |
|
|
21 |
fun syntax_xstr x = Syntax.const "_xstr" $ Syntax.free x;
|
|
22 |
|
|
23 |
|
|
24 |
val zero = ord "0";
|
|
25 |
val ten = ord "A" - 10;
|
|
26 |
|
|
27 |
fun mk_nib n =
|
|
28 |
Syntax.const ("H0" ^ chr (n + (if n <= 9 then zero else ten)));
|
|
29 |
|
|
30 |
fun dest_nib (Const (c, _)) =
|
|
31 |
(case explode c of
|
|
32 |
["H", "0", h] => ord h - (if h <= "9" then zero else ten)
|
|
33 |
| _ => raise Match)
|
|
34 |
| dest_nib _ = raise Match;
|
|
35 |
|
|
36 |
fun dest_nibs t1 t2 = chr (dest_nib t1 * 16 + dest_nib t2);
|
|
37 |
|
|
38 |
|
|
39 |
fun mk_char c =
|
|
40 |
Syntax.const "Char" $ mk_nib (ord c div 16) $ mk_nib (ord c mod 16);
|
|
41 |
|
|
42 |
fun dest_char (Const ("Char", _) $ t1 $ t2) = dest_nibs t1 t2
|
|
43 |
| dest_char _ = raise Match;
|
|
44 |
|
|
45 |
|
|
46 |
fun char_tr (*"_Char"*) [Free (xstr, _)] =
|
|
47 |
(case Syntax.explode_xstr xstr of
|
|
48 |
[c] => mk_char c
|
|
49 |
| _ => error ("Single character expected: " ^ xstr))
|
|
50 |
| char_tr (*"_Char"*) ts = raise TERM ("char_tr", ts);
|
|
51 |
|
|
52 |
fun char_tr' (*"Char"*) [t1, t2] =
|
|
53 |
Syntax.const "_Char" $ syntax_xstr (Syntax.implode_xstr [dest_nibs t1 t2])
|
|
54 |
| char_tr' (*"Char"*) _ = raise Match;
|
|
55 |
|
|
56 |
|
|
57 |
(* strings *)
|
|
58 |
|
|
59 |
fun mk_string [] = Syntax.const Syntax.constrainC $ Syntax.const "Nil" $ Syntax.const "string"
|
|
60 |
| mk_string (t :: ts) = Syntax.const "Cons" $ t $ mk_string ts;
|
|
61 |
|
|
62 |
fun dest_string (Const ("Nil", _)) = []
|
|
63 |
| dest_string (Const ("Cons", _) $ c $ cs) = dest_char c :: dest_string cs
|
|
64 |
| dest_string _ = raise Match;
|
|
65 |
|
|
66 |
|
|
67 |
fun string_tr (*"_String"*) [Free (xstr, _)] =
|
|
68 |
mk_string (map mk_char (Syntax.explode_xstr xstr))
|
|
69 |
| string_tr (*"_String"*) ts = raise TERM ("string_tr", ts);
|
|
70 |
|
|
71 |
fun cons_tr' (*"Cons"*) [c, cs] =
|
|
72 |
Syntax.const "_String" $
|
|
73 |
syntax_xstr (Syntax.implode_xstr (dest_char c :: dest_string cs))
|
|
74 |
| cons_tr' (*"Cons"*) ts = raise Match;
|
|
75 |
|
|
76 |
|
|
77 |
(* theory setup *)
|
|
78 |
|
|
79 |
val setup =
|
|
80 |
[Theory.add_trfuns
|
|
81 |
([], [("_Char", char_tr), ("_String", string_tr)],
|
|
82 |
[("Char", char_tr'), ("Cons", cons_tr')], [])];
|
|
83 |
|
|
84 |
end;
|