author  wenzelm 
Thu, 25 Feb 2010 22:17:33 +0100  
changeset 35363  09489d8ffece 
parent 35299  4f4d5bf4ea08 
child 35430  df2862dc23a8 
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"} $ 

35363  28 
(Syntax.const @{type_syntax itself} $ ty)) 
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 

35363  35 
fun typerep_tr' show_sorts (*"typerep"*) 
36 
(Type (@{type_syntax fun}, [Type (@{type_syntax itself}, [T]), _])) 

37 
(Const (@{const_syntax TYPE}, _) :: ts) = 

35115  38 
Term.list_comb 
39 
(Syntax.const @{syntax_const "_TYPEREP"} $ Syntax.term_of_typ show_sorts T, ts) 

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

31137  44 
setup {* 
45 
let 

26168  46 

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

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

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

58 
thy 

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

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

68 
then add_typerep tyco thy else thy; 

69 

70 
in 

26168  71 

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

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

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

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

31137  77 
end 
26168  78 
*} 
79 

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

81 
"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

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

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

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

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

31031  91 
code_reserved Eval Term 
26168  92 

28335  93 
hide (open) const typerep Typerep 
26168  94 

95 
end 