migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
1 (* Title: HOL/Tools/string_code.ML
2 Author: Florian Haftmann, TU Muenchen
4 Code generation for character and string literals.
7 signature STRING_CODE =
9 val add_literal_list_string: string -> theory -> theory
10 val add_literal_char: string -> theory -> theory
11 val add_literal_string: string -> theory -> theory
14 structure String_Code : STRING_CODE =
17 open Basic_Code_Thingol;
19 fun decode_char nibbles' tt =
21 fun idx c = find_index (curry (op =) c) nibbles';
22 fun decode ~1 _ = NONE
24 | decode n m = SOME (chr (n * 16 + m));
26 of (IConst { name = c1, ... }, IConst { name = c2, ... }) => decode (idx c1) (idx c2)
30 fun implode_string literals char' nibbles' ts =
32 fun implode_char (IConst { name = c, ... } `$ t1 `$ t2) =
33 if c = char' then decode_char nibbles' (t1, t2) else NONE
34 | implode_char _ = NONE;
35 val ts' = map_filter implode_char ts;
36 in if length ts = length ts'
37 then (SOME o Code_Printer.str o Code_Printer.literal_string literals o implode) ts'
41 val cs_nibbles = [@{const_name Nibble0}, @{const_name Nibble1},
42 @{const_name Nibble2}, @{const_name Nibble3},
43 @{const_name Nibble4}, @{const_name Nibble5},
44 @{const_name Nibble6}, @{const_name Nibble7},
45 @{const_name Nibble8}, @{const_name Nibble9},
46 @{const_name NibbleA}, @{const_name NibbleB},
47 @{const_name NibbleC}, @{const_name NibbleD},
48 @{const_name NibbleE}, @{const_name NibbleF}];
49 val cs_summa = [@{const_name Nil}, @{const_name Cons}, @{const_name Char}] @ cs_nibbles;
51 fun add_literal_list_string target =
53 fun pretty literals (nil' :: cons' :: char' :: nibbles') pr _ vars fxy [(t1, _), (t2, _)] =
54 case Option.map (cons t1) (List_Code.implode_list nil' cons' t2)
55 of SOME ts => (case implode_string literals char' nibbles' ts
58 Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts))
60 List_Code.default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
62 Code_Target.set_printings (Code_Symbol.Constant (@{const_name Cons},
63 [(target, SOME (Code_Printer.complex_const_syntax (2, (cs_summa, pretty))))]))
66 fun add_literal_char target =
68 fun pretty literals nibbles' _ thm _ _ [(t1, _), (t2, _)] =
69 case decode_char nibbles' (t1, t2)
70 of SOME c => (Code_Printer.str o Code_Printer.literal_char literals) c
71 | NONE => Code_Printer.eqn_error thm "Illegal character expression";
73 Code_Target.set_printings (Code_Symbol.Constant (@{const_name Char},
74 [(target, SOME (Code_Printer.complex_const_syntax (2, (cs_nibbles, pretty))))]))
77 fun add_literal_string target =
79 fun pretty literals (nil' :: cons' :: char' :: nibbles') _ thm _ _ [(t, _)] =
80 case List_Code.implode_list nil' cons' t
81 of SOME ts => (case implode_string literals char' nibbles' ts
83 | NONE => Code_Printer.eqn_error thm "Illegal message expression")
84 | NONE => Code_Printer.eqn_error thm "Illegal message expression";
86 Code_Target.set_printings (Code_Symbol.Constant (@{const_name STR},
87 [(target, SOME (Code_Printer.complex_const_syntax (1, (cs_summa, pretty))))]))