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