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