1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7section "Print Words in Hex" 8 9theory Hex_Words 10imports 11 "HOL-Word.Word" 12begin 13 14text \<open>Print words in hex.\<close> 15 16(* mostly clagged from Num.thy *) 17typed_print_translation \<open> 18let 19 fun dest_num (Const (@{const_syntax Num.Bit0}, _) $ n) = 2 * dest_num n 20 | dest_num (Const (@{const_syntax Num.Bit1}, _) $ n) = 2 * dest_num n + 1 21 | dest_num (Const (@{const_syntax Num.One}, _)) = 1; 22 23 fun dest_bin_hex_str tm = 24 let 25 val num = dest_num tm; 26 val pre = if num < 10 then "" else "0x" 27 in 28 pre ^ (Int.fmt StringCvt.HEX num) 29 end; 30 31 fun num_tr' sign ctxt T [n] = 32 let 33 val k = dest_bin_hex_str n; 34 val t' = Syntax.const @{syntax_const "_Numeral"} $ 35 Syntax.free (sign ^ k); 36 in 37 case T of 38 Type (@{type_name fun}, [_, T' as Type("Word.word",_)]) => 39 if not (Config.get ctxt show_types) andalso can Term.dest_Type T' 40 then t' 41 else Syntax.const @{syntax_const "_constrain"} $ t' $ 42 Syntax_Phases.term_of_typ ctxt T' 43 | T' => if T' = dummyT then t' else raise Match 44 end; 45in [(@{const_syntax numeral}, num_tr' "")] end 46\<close> 47 48end 49