Theory Word_Lib.Type_Syntax

(*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

section "Displaying Phantom Types for Word Operations"

theory Type_Syntax
  imports "HOL-Library.Word"
begin

ML ‹
structure Word_Syntax =
struct

  val show_word_types = Attrib.setup_config_bool @{binding show_word_types} (K true)

  fun tr' cnst ctxt typ ts = if Config.get ctxt show_word_types then
      case (Term.binder_types typ, Term.body_type typ) of
        ([\<^Type>‹word S›], \<^Type>‹word T›) =>
          list_comb
            (Syntax.const cnst $ Syntax_Phases.term_of_typ ctxt S $ Syntax_Phases.term_of_typ ctxt T
            , ts)
        | _ => raise Match
  else raise Match

end
›


syntax
  "_Ucast" :: "type ⇒ type ⇒ logic"
    (‹(‹indent=1 notation=‹mixfix UCAST››UCAST/(‹indent=1 notation=‹infix cast››'(_ → _')))›)
syntax_consts
  "_Ucast" == ucast
translations
  "UCAST('s → 't)" => "CONST ucast :: ('s word ⇒ 't word)"
typed_print_translation
  ‹ [(@{const_syntax ucast}, Word_Syntax.tr' @{syntax_const "_Ucast"})] ›


syntax
  "_Scast" :: "type ⇒ type ⇒ logic"
    (‹(‹indent=1 notation=‹mixfix SCAST››SCAST/(‹indent=1 notation=‹infix cast››'(_ → _')))›)
syntax_consts
  "_Scast" == scast
translations
  "SCAST('s → 't)" => "CONST scast :: ('s word ⇒ 't word)"
typed_print_translation
  ‹ [(@{const_syntax scast}, Word_Syntax.tr' @{syntax_const "_Scast"})] ›


syntax
  "_Revcast" :: "type ⇒ type ⇒ logic"
    (‹(‹indent=1 notation=‹mixfix REVCAST››REVCAST/(‹indent=1 notation=‹infix cast››'(_ → _')))›)
syntax_consts
  "_Revcast" == revcast
translations
  "REVCAST('s → 't)" => "CONST revcast :: ('s word ⇒ 't word)"
typed_print_translation
  ‹ [(@{const_syntax revcast}, Word_Syntax.tr' @{syntax_const "_Revcast"})] ›

(* Further candidates for showing word sizes, but with different arities:
   slice, word_cat, word_split, word_rcat, word_rsplit *)

end