12 structure Literal: LITERAL = |
12 structure Literal: LITERAL = |
13 struct |
13 struct |
14 |
14 |
15 datatype character = datatype String_Syntax.character; |
15 datatype character = datatype String_Syntax.character; |
16 |
16 |
17 fun mk_literal_syntax [] = Syntax.const @{const_syntax String.empty_literal} |
17 fun mk_literal_syntax [] = Syntax.const \<^const_syntax>\<open>String.empty_literal\<close> |
18 | mk_literal_syntax (c :: cs) = |
18 | mk_literal_syntax (c :: cs) = |
19 list_comb (Syntax.const @{const_syntax String.Literal}, String_Syntax.mk_bits_syntax 7 c) |
19 list_comb (Syntax.const \<^const_syntax>\<open>String.Literal\<close>, String_Syntax.mk_bits_syntax 7 c) |
20 $ mk_literal_syntax cs; |
20 $ mk_literal_syntax cs; |
21 |
21 |
22 val dest_literal_syntax = |
22 val dest_literal_syntax = |
23 let |
23 let |
24 fun dest (Const (@{const_syntax String.empty_literal}, _)) = [] |
24 fun dest (Const (\<^const_syntax>\<open>String.empty_literal\<close>, _)) = [] |
25 | dest (Const (@{const_syntax String.Literal}, _) $ b0 $ b1 $ b2 $ b3 $ b4 $ b5 $ b6 $ t) = |
25 | dest (Const (\<^const_syntax>\<open>String.Literal\<close>, _) $ 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 |
26 String_Syntax.classify_character (String_Syntax.dest_bits_syntax [b0, b1, b2, b3, b4, b5, b6]) :: dest t |
27 | dest t = raise Match; |
27 | dest t = raise Match; |
28 in dest end; |
28 in dest end; |
29 |
29 |
30 fun ascii_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = |
30 fun ascii_tr [(c as Const (\<^syntax_const>\<open>_constrain\<close>, _)) $ t $ u] = |
31 c $ ascii_tr [t] $ u |
31 c $ ascii_tr [t] $ u |
32 | ascii_tr [Const (num, _)] = |
32 | ascii_tr [Const (num, _)] = |
33 (mk_literal_syntax o single o (fn n => n mod 128) o #value o Lexicon.read_num) 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); |
34 | ascii_tr ts = raise TERM ("ascii_tr", ts); |
35 |
35 |
36 fun literal_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = |
36 fun literal_tr [(c as Const (\<^syntax_const>\<open>_constrain\<close>, _)) $ t $ u] = |
37 c $ literal_tr [t] $ u |
37 c $ literal_tr [t] $ u |
38 | literal_tr [Free (str, _)] = |
38 | literal_tr [Free (str, _)] = |
39 (mk_literal_syntax o map String_Syntax.ascii_ord_of o String_Syntax.plain_strings_of) str |
39 (mk_literal_syntax o map String_Syntax.ascii_ord_of o String_Syntax.plain_strings_of) str |
40 | literal_tr ts = raise TERM ("literal_tr", ts); |
40 | literal_tr ts = raise TERM ("literal_tr", ts); |
41 |
41 |
42 fun ascii k = Syntax.const @{syntax_const "_Ascii"} |
42 fun ascii k = Syntax.const \<^syntax_const>\<open>_Ascii\<close> |
43 $ Syntax.free (String_Syntax.hex k); |
43 $ Syntax.free (String_Syntax.hex k); |
44 |
44 |
45 fun literal cs = Syntax.const @{syntax_const "_Literal"} |
45 fun literal cs = Syntax.const \<^syntax_const>\<open>_Literal\<close> |
46 $ Syntax.const (Lexicon.implode_str cs); |
46 $ Syntax.const (Lexicon.implode_str cs); |
47 |
47 |
48 fun empty_literal_tr' _ = literal []; |
48 fun empty_literal_tr' _ = literal []; |
49 |
49 |
50 fun literal_tr' [b0, b1, b2, b3, b4, b5, b6, t] = |
50 fun literal_tr' [b0, b1, b2, b3, b4, b5, b6, t] = |
51 let |
51 let |
52 val cs = |
52 val cs = |
53 dest_literal_syntax (list_comb (Syntax.const @{const_syntax String.Literal}, [b0, b1, b2, b3, b4, b5, b6, t])) |
53 dest_literal_syntax (list_comb (Syntax.const \<^const_syntax>\<open>String.Literal\<close>, [b0, b1, b2, b3, b4, b5, b6, t])) |
54 fun is_printable (Char _) = true |
54 fun is_printable (Char _) = true |
55 | is_printable (Ord _) = false; |
55 | is_printable (Ord _) = false; |
56 fun the_char (Char c) = c; |
56 fun the_char (Char c) = c; |
57 fun the_ascii [Ord i] = i; |
57 fun the_ascii [Ord i] = i; |
58 in |
58 in |
76 (case mapp xs of |
76 (case mapp xs of |
77 NONE => NONE |
77 NONE => NONE |
78 | SOME ys => SOME (y :: ys))) |
78 | SOME ys => SOME (y :: ys))) |
79 in Option.map g o mapp end; |
79 in Option.map g o mapp end; |
80 |
80 |
81 fun implode_bit (IConst { sym = Code_Symbol.Constant @{const_name False}, ... }) = SOME 0 |
81 fun implode_bit (IConst { sym = Code_Symbol.Constant \<^const_name>\<open>False\<close>, ... }) = SOME 0 |
82 | implode_bit (IConst { sym = Code_Symbol.Constant @{const_name True}, ... }) = SOME 1 |
82 | implode_bit (IConst { sym = Code_Symbol.Constant \<^const_name>\<open>True\<close>, ... }) = SOME 1 |
83 | implode_bit _ = NONE |
83 | implode_bit _ = NONE |
84 |
84 |
85 fun implode_ascii (b0, b1, b2, b3, b4, b5, b6) = |
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]; |
86 map_partial (chr o Integer.eval_radix 2) implode_bit [b0, b1, b2, b3, b4, b5, b6]; |
87 |
87 |
88 fun implode_literal b0 b1 b2 b3 b4 b5 b6 t = |
88 fun implode_literal b0 b1 b2 b3 b4 b5 b6 t = |
89 let |
89 let |
90 fun dest_literal (IConst { sym = Code_Symbol.Constant @{const_name String.Literal}, ... } |
90 fun dest_literal (IConst { sym = Code_Symbol.Constant \<^const_name>\<open>String.Literal\<close>, ... } |
91 `$ b0 `$ b1 `$ b2 `$ b3 `$ b4 `$ b5 `$ b6 `$ t) = SOME ((b0, b1, b2, b3, b4, b5, b6), t) |
91 `$ b0 `$ b1 `$ b2 `$ b3 `$ b4 `$ b5 `$ b6 `$ t) = SOME ((b0, b1, b2, b3, b4, b5, b6), t) |
92 | dest_literal _ = NONE; |
92 | dest_literal _ = NONE; |
93 val (bss', t') = Code_Thingol.unfoldr dest_literal t; |
93 val (bss', t') = Code_Thingol.unfoldr dest_literal t; |
94 val bss = (b0, b1, b2, b3, b4, b5, b6) :: bss'; |
94 val bss = (b0, b1, b2, b3, b4, b5, b6) :: bss'; |
95 in |
95 in |
96 case t' of |
96 case t' of |
97 IConst { sym = Code_Symbol.Constant @{const_name String.zero_literal_inst.zero_literal}, ... } |
97 IConst { sym = Code_Symbol.Constant \<^const_name>\<open>String.zero_literal_inst.zero_literal\<close>, ... } |
98 => map_partial implode implode_ascii bss |
98 => map_partial implode implode_ascii bss |
99 | _ => NONE |
99 | _ => NONE |
100 end; |
100 end; |
101 |
101 |
102 fun add_code target thy = |
102 fun add_code target thy = |
105 case implode_literal b0 b1 b2 b3 b4 b5 b6 t of |
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 |
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"; |
107 | NONE => Code_Printer.eqn_error thy thm "Illegal string literal expression"; |
108 in |
108 in |
109 thy |
109 thy |
110 |> Code_Target.set_printings (Code_Symbol.Constant (@{const_name String.Literal}, |
110 |> Code_Target.set_printings (Code_Symbol.Constant (\<^const_name>\<open>String.Literal\<close>, |
111 [(target, SOME (Code_Printer.complex_const_syntax (8, pretty)))])) |
111 [(target, SOME (Code_Printer.complex_const_syntax (8, pretty)))])) |
112 end; |
112 end; |
113 |
113 |
114 val _ = |
114 val _ = |
115 Theory.setup |
115 Theory.setup |
116 (Sign.parse_translation |
116 (Sign.parse_translation |
117 [(@{syntax_const "_Ascii"}, K ascii_tr), |
117 [(\<^syntax_const>\<open>_Ascii\<close>, K ascii_tr), |
118 (@{syntax_const "_Literal"}, K literal_tr)] #> |
118 (\<^syntax_const>\<open>_Literal\<close>, K literal_tr)] #> |
119 Sign.print_translation |
119 Sign.print_translation |
120 [(@{const_syntax String.Literal}, K literal_tr'), |
120 [(\<^const_syntax>\<open>String.Literal\<close>, K literal_tr'), |
121 (@{const_syntax String.empty_literal}, K empty_literal_tr')]); |
121 (\<^const_syntax>\<open>String.empty_literal\<close>, K empty_literal_tr')]); |
122 |
122 |
123 end |
123 end |