1(*  Title:      HOL/Tools/literal.ML
2    Author:     Florian Haftmann, TU Muenchen
3
4Logical and syntactic operations on literals (see also HOL/Tools/hologic.ML).
5*)
6
7signature LITERAL =
8sig
9  val add_code: string -> theory -> theory
10end
11
12structure Literal: LITERAL =
13struct
14
15datatype character = datatype String_Syntax.character;
16
17fun mk_literal_syntax [] = Syntax.const \<^const_syntax>\<open>String.empty_literal\<close>
18  | mk_literal_syntax (c :: cs) =
19      list_comb (Syntax.const \<^const_syntax>\<open>String.Literal\<close>, String_Syntax.mk_bits_syntax 7 c)
20        $ mk_literal_syntax cs;
21
22val dest_literal_syntax =
23  let
24    fun dest (Const (\<^const_syntax>\<open>String.empty_literal\<close>, _)) = []
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
27      | dest t = raise Match;
28  in dest end;
29
30fun ascii_tr [(c as Const (\<^syntax_const>\<open>_constrain\<close>, _)) $ 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
36fun literal_tr [(c as Const (\<^syntax_const>\<open>_constrain\<close>, _)) $ t $ u] =
37      c $ literal_tr [t] $ u
38  | literal_tr [Free (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);
41
42fun ascii k = Syntax.const \<^syntax_const>\<open>_Ascii\<close>
43  $ Syntax.free (String_Syntax.hex k);
44
45fun literal cs = Syntax.const \<^syntax_const>\<open>_Literal\<close>
46  $ Syntax.const (Lexicon.implode_str cs);
47
48fun empty_literal_tr' _ = literal [];
49
50fun 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>\<open>String.Literal\<close>, [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
67open Basic_Code_Thingol;
68
69fun 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
81fun implode_bit (IConst { sym = Code_Symbol.Constant \<^const_name>\<open>False\<close>, ... }) = SOME 0
82  | implode_bit (IConst { sym = Code_Symbol.Constant \<^const_name>\<open>True\<close>, ... }) = SOME 1
83  | implode_bit _ = NONE
84
85fun 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
88fun implode_literal b0 b1 b2 b3 b4 b5 b6 t =
89  let
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)
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>\<open>String.zero_literal_inst.zero_literal\<close>, ... }
98        => map_partial implode implode_ascii bss
99    | _ => NONE
100  end;
101
102fun 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>\<open>String.Literal\<close>,
111      [(target, SOME (Code_Printer.complex_const_syntax (8, pretty)))]))
112  end;
113
114val _ =
115  Theory.setup
116   (Sign.parse_translation
117     [(\<^syntax_const>\<open>_Ascii\<close>, K ascii_tr),
118      (\<^syntax_const>\<open>_Literal\<close>, K literal_tr)] #>
119    Sign.print_translation
120     [(\<^const_syntax>\<open>String.Literal\<close>, K literal_tr'),
121      (\<^const_syntax>\<open>String.empty_literal\<close>, K empty_literal_tr')]);
122
123end
124