1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7section "Displaying Phantom Types for Word Operations"
8
9theory Word_Type_Syntax
10imports "HOL-Word.Word"
11begin
12
13ML \<open>
14structure Word_Syntax =
15struct
16
17  val show_word_types = Attrib.setup_config_bool @{binding show_word_types} (K true)
18
19  fun tr' cnst ctxt typ ts = if Config.get ctxt show_word_types then
20      case (Term.binder_types typ, Term.body_type typ) of
21        ([Type (@{type_name "word"}, [S])], Type (@{type_name "word"}, [T])) =>
22          list_comb
23            (Syntax.const cnst $ Syntax_Phases.term_of_typ ctxt S $ Syntax_Phases.term_of_typ ctxt T
24            , ts)
25        | _ => raise Match
26  else raise Match
27
28end
29\<close>
30
31
32syntax
33  "_Ucast" :: "type \<Rightarrow> type \<Rightarrow> logic" ("(1UCAST/(1'(_ \<rightarrow> _')))")
34translations
35  "UCAST('s \<rightarrow> 't)" => "CONST ucast :: ('s word \<Rightarrow> 't word)"
36typed_print_translation
37  \<open> [(@{const_syntax ucast}, Word_Syntax.tr' @{syntax_const "_Ucast"})] \<close>
38
39
40syntax
41  "_Scast" :: "type \<Rightarrow> type \<Rightarrow> logic" ("(1SCAST/(1'(_ \<rightarrow> _')))")
42translations
43  "SCAST('s \<rightarrow> 't)" => "CONST scast :: ('s word \<Rightarrow> 't word)"
44typed_print_translation
45  \<open> [(@{const_syntax scast}, Word_Syntax.tr' @{syntax_const "_Scast"})] \<close>
46
47
48syntax
49  "_Revcast" :: "type \<Rightarrow> type \<Rightarrow> logic" ("(1REVCAST/(1'(_ \<rightarrow> _')))")
50translations
51  "REVCAST('s \<rightarrow> 't)" => "CONST revcast :: ('s word \<Rightarrow> 't word)"
52typed_print_translation
53  \<open> [(@{const_syntax revcast}, Word_Syntax.tr' @{syntax_const "_Revcast"})] \<close>
54
55(* Further candidates for showing word sizes, but with different arities:
56   slice, word_cat, word_split, word_rcat, word_rsplit *)
57
58end
59