68028
|
1 |
(* Title: HOL/Tools/literal.ML
|
|
2 |
Author: Florian Haftmann, TU Muenchen
|
|
3 |
|
|
4 |
Logical and syntactic operations on literals (see also HOL/Tools/hologic.ML).
|
|
5 |
*)
|
|
6 |
|
|
7 |
signature LITERAL =
|
|
8 |
sig
|
|
9 |
val add_code: string -> theory -> theory
|
|
10 |
end
|
|
11 |
|
|
12 |
structure Literal: LITERAL =
|
|
13 |
struct
|
|
14 |
|
|
15 |
datatype character = datatype String_Syntax.character;
|
|
16 |
|
|
17 |
fun mk_literal_syntax [] = Syntax.const @{const_syntax String.empty_literal}
|
|
18 |
| mk_literal_syntax (c :: cs) =
|
|
19 |
list_comb (Syntax.const @{const_syntax String.Literal}, String_Syntax.mk_bits_syntax 7 c)
|
|
20 |
$ mk_literal_syntax cs;
|
|
21 |
|
|
22 |
val dest_literal_syntax =
|
|
23 |
let
|
|
24 |
fun dest (Const (@{const_syntax String.empty_literal}, _)) = []
|
|
25 |
| dest (Const (@{const_syntax String.Literal}, _) $ b0 $ b1 $ b2 $ b3 $ b4 $ b5 $ b6 $ t) =
|
|
26 |
String_Syntax.classify_character (String_Syntax.dest_bits_syntax [b0, b1, b2, b3, b4, b5, b6]) :: dest t
|
|
27 |
| dest t = raise Match;
|
|
28 |
in dest end;
|
|
29 |
|
|
30 |
fun ascii_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
|
|
31 |
c $ ascii_tr [t] $ u
|
|
32 |
| ascii_tr [Const (num, _)] =
|
|
33 |
(mk_literal_syntax o single o (fn n => n mod 128) o #value o Lexicon.read_num) num
|
|
34 |
| ascii_tr ts = raise TERM ("ascii_tr", ts);
|
|
35 |
|
|
36 |
fun literal_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
|
|
37 |
c $ literal_tr [t] $ u
|
|
38 |
| literal_tr [Free (str, _)] =
|
|
39 |
(mk_literal_syntax o map ord o String_Syntax.plain_strings_of) str
|
|
40 |
| literal_tr ts = raise TERM ("literal_tr", ts);
|
|
41 |
|
|
42 |
fun ascii k = Syntax.const @{syntax_const "_Ascii"}
|
|
43 |
$ Syntax.free (String_Syntax.hex k);
|
|
44 |
|
|
45 |
fun literal cs = Syntax.const @{syntax_const "_Literal"}
|
|
46 |
$ Syntax.const (Lexicon.implode_str cs);
|
|
47 |
|
|
48 |
fun empty_literal_tr' _ = literal [];
|
|
49 |
|
|
50 |
fun literal_tr' [b0, b1, b2, b3, b4, b5, b6, t] =
|
|
51 |
let
|
|
52 |
val cs =
|
|
53 |
dest_literal_syntax (list_comb (Syntax.const @{const_syntax String.Literal}, [b0, b1, b2, b3, b4, b5, b6, t]))
|
|
54 |
fun is_printable (Char _) = true
|
|
55 |
| is_printable (Ord _) = false;
|
|
56 |
fun the_char (Char c) = c;
|
|
57 |
fun the_ascii [Ord i] = i;
|
|
58 |
in
|
|
59 |
if forall is_printable cs
|
|
60 |
then literal (map the_char cs)
|
|
61 |
else if length cs = 1
|
|
62 |
then ascii (the_ascii cs)
|
|
63 |
else raise Match
|
|
64 |
end
|
|
65 |
| literal_tr' _ = raise Match;
|
|
66 |
|
|
67 |
open Basic_Code_Thingol;
|
|
68 |
|
|
69 |
fun map_partial g f =
|
|
70 |
let
|
|
71 |
fun mapp [] = SOME []
|
|
72 |
| mapp (x :: xs) =
|
|
73 |
(case f x of
|
|
74 |
NONE => NONE
|
|
75 |
| SOME y =>
|
|
76 |
(case mapp xs of
|
|
77 |
NONE => NONE
|
|
78 |
| SOME ys => SOME (y :: ys)))
|
|
79 |
in Option.map g o mapp end;
|
|
80 |
|
|
81 |
fun implode_bit (IConst { sym = Code_Symbol.Constant @{const_name False}, ... }) = SOME 0
|
|
82 |
| implode_bit (IConst { sym = Code_Symbol.Constant @{const_name True}, ... }) = SOME 1
|
|
83 |
| implode_bit _ = NONE
|
|
84 |
|
|
85 |
fun implode_ascii (b0, b1, b2, b3, b4, b5, b6) =
|
|
86 |
map_partial (chr o Integer.eval_radix 2) implode_bit [b0, b1, b2, b3, b4, b5, b6];
|
|
87 |
|
|
88 |
fun implode_literal b0 b1 b2 b3 b4 b5 b6 t =
|
|
89 |
let
|
|
90 |
fun dest_literal (IConst { sym = Code_Symbol.Constant @{const_name String.Literal}, ... }
|
|
91 |
`$ b0 `$ b1 `$ b2 `$ b3 `$ b4 `$ b5 `$ b6 `$ t) = SOME ((b0, b1, b2, b3, b4, b5, b6), t)
|
|
92 |
| dest_literal _ = NONE;
|
|
93 |
val (bss', t') = Code_Thingol.unfoldr dest_literal t;
|
|
94 |
val bss = (b0, b1, b2, b3, b4, b5, b6) :: bss';
|
|
95 |
in
|
|
96 |
case t' of
|
|
97 |
IConst { sym = Code_Symbol.Constant @{const_name String.zero_literal_inst.zero_literal}, ... }
|
|
98 |
=> map_partial implode implode_ascii bss
|
|
99 |
| _ => NONE
|
|
100 |
end;
|
|
101 |
|
|
102 |
fun add_code target thy =
|
|
103 |
let
|
|
104 |
fun pretty literals _ thm _ _ [(b0, _), (b1, _), (b2, _), (b3, _), (b4, _), (b5, _), (b6, _), (t, _)] =
|
|
105 |
case implode_literal b0 b1 b2 b3 b4 b5 b6 t of
|
|
106 |
SOME s => (Code_Printer.str o Code_Printer.literal_string literals) s
|
|
107 |
| NONE => Code_Printer.eqn_error thy thm "Illegal string literal expression";
|
|
108 |
in
|
|
109 |
thy
|
|
110 |
|> Code_Target.set_printings (Code_Symbol.Constant (@{const_name String.Literal},
|
|
111 |
[(target, SOME (Code_Printer.complex_const_syntax (8, pretty)))]))
|
|
112 |
end;
|
|
113 |
|
|
114 |
val _ =
|
|
115 |
Theory.setup
|
|
116 |
(Sign.parse_translation
|
|
117 |
[(@{syntax_const "_Ascii"}, K ascii_tr),
|
|
118 |
(@{syntax_const "_Literal"}, K literal_tr)] #>
|
|
119 |
Sign.print_translation
|
|
120 |
[(@{const_syntax String.Literal}, K literal_tr'),
|
|
121 |
(@{const_syntax String.empty_literal}, K empty_literal_tr')]);
|
|
122 |
|
|
123 |
end
|