Theory Typerep
section ‹Reflecting Pure types into HOL›
theory Typerep
imports String
begin
datatype typerep = Typerep String.literal "typerep list"
class typerep =
fixes typerep :: "'a itself ⇒ typerep"
begin
definition typerep_of :: "'a ⇒ typerep" where
[simp]: "typerep_of x = typerep TYPE('a)"
end
syntax
"_TYPEREP" :: "type => logic" ("(1TYPEREP/(1'(_')))")
parse_translation ‹
let
fun typerep_tr [ty] =
Syntax.const \<^const_syntax>‹typerep› $
(Syntax.const \<^syntax_const>‹_constrain› $ Syntax.const \<^const_syntax>‹Pure.type› $
(Syntax.const \<^type_syntax>‹itself› $ ty))
| typerep_tr ts = raise TERM ("typerep_tr", ts);
in [(\<^syntax_const>‹_TYPEREP›, K typerep_tr)] end
›
typed_print_translation ‹
let
fun typerep_tr' ctxt \<^Type>‹fun \<^Type>‹itself T› _›
(Const (\<^const_syntax>‹Pure.type›, _) :: ts) =
Term.list_comb
(Syntax.const \<^syntax_const>‹_TYPEREP› $ Syntax_Phases.term_of_typ ctxt T, ts)
| typerep_tr' _ T ts = raise Match;
in [(\<^const_syntax>‹typerep›, typerep_tr')] end
›