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