haftmann@31048
|
1 |
(* Author: Florian Haftmann, TU Muenchen *)
|
haftmann@26168
|
2 |
|
haftmann@26168
|
3 |
header {* Reflecting Pure types into HOL *}
|
haftmann@26168
|
4 |
|
haftmann@28952
|
5 |
theory Typerep
|
haftmann@31048
|
6 |
imports Plain String
|
haftmann@26168
|
7 |
begin
|
haftmann@26168
|
8 |
|
haftmann@31205
|
9 |
datatype typerep = Typerep String.literal "typerep list"
|
haftmann@26168
|
10 |
|
haftmann@28335
|
11 |
class typerep =
|
haftmann@31031
|
12 |
fixes typerep :: "'a itself \<Rightarrow> typerep"
|
haftmann@26168
|
13 |
begin
|
haftmann@26168
|
14 |
|
haftmann@29574
|
15 |
definition typerep_of :: "'a \<Rightarrow> typerep" where
|
haftmann@28335
|
16 |
[simp]: "typerep_of x = typerep TYPE('a)"
|
haftmann@26168
|
17 |
|
haftmann@26168
|
18 |
end
|
haftmann@26168
|
19 |
|
wenzelm@35118
|
20 |
syntax
|
wenzelm@35118
|
21 |
"_TYPEREP" :: "type => logic" ("(1TYPEREP/(1'(_')))")
|
wenzelm@35118
|
22 |
|
wenzelm@35118
|
23 |
parse_translation {*
|
haftmann@26168
|
24 |
let
|
haftmann@28335
|
25 |
fun typerep_tr (*"_TYPEREP"*) [ty] =
|
wenzelm@35118
|
26 |
Syntax.const @{const_syntax typerep} $
|
wenzelm@35118
|
27 |
(Syntax.const @{syntax_const "_constrain"} $ Syntax.const @{const_syntax "TYPE"} $
|
wenzelm@35118
|
28 |
(Syntax.const "itself" $ ty)) (* FIXME @{type_syntax} *)
|
haftmann@28335
|
29 |
| typerep_tr (*"_TYPEREP"*) ts = raise TERM ("typerep_tr", ts);
|
wenzelm@35118
|
30 |
in [(@{syntax_const "_TYPEREP"}, typerep_tr)] end
|
wenzelm@35118
|
31 |
*}
|
wenzelm@35118
|
32 |
|
wenzelm@35118
|
33 |
typed_print_translation {*
|
wenzelm@35118
|
34 |
let
|
wenzelm@35118
|
35 |
fun typerep_tr' show_sorts (*"typerep"*) (* FIXME @{type_syntax} *)
|
haftmann@26168
|
36 |
(Type ("fun", [Type ("itself", [T]), _])) (Const (@{const_syntax TYPE}, _) :: ts) =
|
wenzelm@35118
|
37 |
Term.list_comb
|
wenzelm@35118
|
38 |
(Syntax.const @{syntax_const "_TYPEREP"} $ Syntax.term_of_typ show_sorts T, ts)
|
haftmann@28335
|
39 |
| typerep_tr' _ T ts = raise Match;
|
wenzelm@35118
|
40 |
in [(@{const_syntax typerep}, typerep_tr')] end
|
haftmann@26168
|
41 |
*}
|
haftmann@26168
|
42 |
|
haftmann@31137
|
43 |
setup {*
|
haftmann@31137
|
44 |
let
|
haftmann@26168
|
45 |
|
haftmann@31137
|
46 |
fun add_typerep tyco thy =
|
haftmann@26168
|
47 |
let
|
haftmann@28335
|
48 |
val sorts = replicate (Sign.arity_number thy tyco) @{sort typerep};
|
haftmann@26168
|
49 |
val vs = Name.names Name.context "'a" sorts;
|
haftmann@26168
|
50 |
val ty = Type (tyco, map TFree vs);
|
haftmann@28335
|
51 |
val lhs = Const (@{const_name typerep}, Term.itselfT ty --> @{typ typerep})
|
haftmann@26168
|
52 |
$ Free ("T", Term.itselfT ty);
|
haftmann@31205
|
53 |
val rhs = @{term Typerep} $ HOLogic.mk_literal tyco
|
haftmann@31137
|
54 |
$ HOLogic.mk_list @{typ typerep} (map (HOLogic.mk_typerep o TFree) vs);
|
haftmann@26168
|
55 |
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
|
haftmann@26168
|
56 |
in
|
haftmann@26168
|
57 |
thy
|
wenzelm@33595
|
58 |
|> Theory_Target.instantiation ([tyco], vs, @{sort typerep})
|
haftmann@26168
|
59 |
|> `(fn lthy => Syntax.check_term lthy eq)
|
haftmann@28965
|
60 |
|-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
|
haftmann@26168
|
61 |
|> snd
|
haftmann@31137
|
62 |
|> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
|
haftmann@26168
|
63 |
end;
|
haftmann@26168
|
64 |
|
haftmann@31137
|
65 |
fun ensure_typerep tyco thy = if not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep})
|
haftmann@31137
|
66 |
andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort type}
|
haftmann@31137
|
67 |
then add_typerep tyco thy else thy;
|
haftmann@26168
|
68 |
|
haftmann@31137
|
69 |
in
|
haftmann@26168
|
70 |
|
haftmann@31137
|
71 |
add_typerep @{type_name fun}
|
haftmann@31723
|
72 |
#> Typedef.interpretation ensure_typerep
|
haftmann@35299
|
73 |
#> Code.datatype_interpretation (ensure_typerep o fst)
|
haftmann@35299
|
74 |
#> Code.abstype_interpretation (ensure_typerep o fst)
|
haftmann@31137
|
75 |
|
haftmann@31137
|
76 |
end
|
haftmann@26168
|
77 |
*}
|
haftmann@26168
|
78 |
|
haftmann@28562
|
79 |
lemma [code]:
|
haftmann@28346
|
80 |
"eq_class.eq (Typerep tyco1 tys1) (Typerep tyco2 tys2) \<longleftrightarrow> eq_class.eq tyco1 tyco2
|
haftmann@28346
|
81 |
\<and> list_all2 eq_class.eq tys1 tys2"
|
haftmann@28346
|
82 |
by (auto simp add: equals_eq [symmetric] list_all2_eq [symmetric])
|
haftmann@26168
|
83 |
|
haftmann@28335
|
84 |
code_type typerep
|
haftmann@31031
|
85 |
(Eval "Term.typ")
|
haftmann@26168
|
86 |
|
haftmann@28335
|
87 |
code_const Typerep
|
haftmann@31031
|
88 |
(Eval "Term.Type/ (_, _)")
|
haftmann@26168
|
89 |
|
haftmann@31031
|
90 |
code_reserved Eval Term
|
haftmann@26168
|
91 |
|
haftmann@28335
|
92 |
hide (open) const typerep Typerep
|
haftmann@26168
|
93 |
|
haftmann@26168
|
94 |
end
|