author  haftmann 
Mon, 22 Feb 2010 11:10:20 +0100  
changeset 35299  4f4d5bf4ea08 
parent 35115  446c5063e4fd 
child 35363  09489d8ffece 
permissions  rwrr 
31048
ac146fc38b51
refined HOL string theories and corresponding ML fragments
haftmann
parents:
31031
diff
changeset

1 
(* Author: Florian Haftmann, TU Muenchen *) 
26168  2 

3 
header {* Reflecting Pure types into HOL *} 

4 

28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28562
diff
changeset

5 
theory Typerep 
31048
ac146fc38b51
refined HOL string theories and corresponding ML fragments
haftmann
parents:
31031
diff
changeset

6 
imports Plain String 
26168  7 
begin 
8 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31137
diff
changeset

9 
datatype typerep = Typerep String.literal "typerep list" 
26168  10 

28335  11 
class typerep = 
31031  12 
fixes typerep :: "'a itself \<Rightarrow> typerep" 
26168  13 
begin 
14 

29574  15 
definition typerep_of :: "'a \<Rightarrow> typerep" where 
28335  16 
[simp]: "typerep_of x = typerep TYPE('a)" 
26168  17 

18 
end 

19 

35115  20 
syntax 
21 
"_TYPEREP" :: "type => logic" ("(1TYPEREP/(1'(_')))") 

22 

23 
parse_translation {* 

26168  24 
let 
28335  25 
fun typerep_tr (*"_TYPEREP"*) [ty] = 
35115  26 
Syntax.const @{const_syntax typerep} $ 
27 
(Syntax.const @{syntax_const "_constrain"} $ Syntax.const @{const_syntax "TYPE"} $ 

28 
(Syntax.const "itself" $ ty)) (* FIXME @{type_syntax} *) 

28335  29 
 typerep_tr (*"_TYPEREP"*) ts = raise TERM ("typerep_tr", ts); 
35115  30 
in [(@{syntax_const "_TYPEREP"}, typerep_tr)] end 
31 
*} 

32 

33 
typed_print_translation {* 

34 
let 

35 
fun typerep_tr' show_sorts (*"typerep"*) (* FIXME @{type_syntax} *) 

26168  36 
(Type ("fun", [Type ("itself", [T]), _])) (Const (@{const_syntax TYPE}, _) :: ts) = 
35115  37 
Term.list_comb 
38 
(Syntax.const @{syntax_const "_TYPEREP"} $ Syntax.term_of_typ show_sorts T, ts) 

28335  39 
 typerep_tr' _ T ts = raise Match; 
35115  40 
in [(@{const_syntax typerep}, typerep_tr')] end 
26168  41 
*} 
42 

31137  43 
setup {* 
44 
let 

26168  45 

31137  46 
fun add_typerep tyco thy = 
26168  47 
let 
28335  48 
val sorts = replicate (Sign.arity_number thy tyco) @{sort typerep}; 
26168  49 
val vs = Name.names Name.context "'a" sorts; 
50 
val ty = Type (tyco, map TFree vs); 

28335  51 
val lhs = Const (@{const_name typerep}, Term.itselfT ty > @{typ typerep}) 
26168  52 
$ Free ("T", Term.itselfT ty); 
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31137
diff
changeset

53 
val rhs = @{term Typerep} $ HOLogic.mk_literal tyco 
31137  54 
$ HOLogic.mk_list @{typ typerep} (map (HOLogic.mk_typerep o TFree) vs); 
26168  55 
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); 
56 
in 

57 
thy 

33553  58 
> Theory_Target.instantiation ([tyco], vs, @{sort typerep}) 
26168  59 
> `(fn lthy => Syntax.check_term lthy eq) 
28965  60 
> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq))) 
26168  61 
> snd 
31137  62 
> Class.prove_instantiation_exit (K (Class.intro_classes_tac [])) 
26168  63 
end; 
64 

31137  65 
fun ensure_typerep tyco thy = if not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep}) 
66 
andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort type} 

67 
then add_typerep tyco thy else thy; 

68 

69 
in 

26168  70 

31137  71 
add_typerep @{type_name fun} 
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31205
diff
changeset

72 
#> Typedef.interpretation ensure_typerep 
35299
4f4d5bf4ea08
proper distinction of code datatypes and abstypes
haftmann
parents:
35115
diff
changeset

73 
#> Code.datatype_interpretation (ensure_typerep o fst) 
4f4d5bf4ea08
proper distinction of code datatypes and abstypes
haftmann
parents:
35115
diff
changeset

74 
#> Code.abstype_interpretation (ensure_typerep o fst) 
26168  75 

31137  76 
end 
26168  77 
*} 
78 

28562  79 
lemma [code]: 
28346
b8390cd56b8f
discontinued special treatment of op = vs. eq_class.eq
haftmann
parents:
28335
diff
changeset

80 
"eq_class.eq (Typerep tyco1 tys1) (Typerep tyco2 tys2) \<longleftrightarrow> eq_class.eq tyco1 tyco2 
b8390cd56b8f
discontinued special treatment of op = vs. eq_class.eq
haftmann
parents:
28335
diff
changeset

81 
\<and> list_all2 eq_class.eq tys1 tys2" 
b8390cd56b8f
discontinued special treatment of op = vs. eq_class.eq
haftmann
parents:
28335
diff
changeset

82 
by (auto simp add: equals_eq [symmetric] list_all2_eq [symmetric]) 
26168  83 

28335  84 
code_type typerep 
31031  85 
(Eval "Term.typ") 
26168  86 

28335  87 
code_const Typerep 
31031  88 
(Eval "Term.Type/ (_, _)") 
26168  89 

31031  90 
code_reserved Eval Term 
26168  91 

28335  92 
hide (open) const typerep Typerep 
26168  93 

94 
end 