author | wenzelm |
Sat, 07 Mar 2009 22:17:25 +0100 | |
changeset 30345 | 76fd85bbf139 |
parent 29875 | 4a1510b5f886 |
child 31090 | 3be41b271023 |
permissions | -rw-r--r-- |
20426 | 1 |
(* Title: HOL/Tools/typecopy_package.ML |
2 |
Author: Florian Haftmann, TU Muenchen |
|
3 |
||
20855 | 4 |
Introducing copies of types using trivial typedefs; datatype-like abstraction. |
20426 | 5 |
*) |
6 |
||
7 |
signature TYPECOPY_PACKAGE = |
|
8 |
sig |
|
9 |
type info = { |
|
10 |
vs: (string * sort) list, |
|
11 |
constr: string, |
|
12 |
typ: typ, |
|
13 |
inject: thm, |
|
14 |
proj: string * typ, |
|
15 |
proj_def: thm |
|
16 |
} |
|
30345 | 17 |
val add_typecopy: binding * string list -> typ -> (binding * binding) option |
20483
04aa552a83bc
TypedefPackage.add_typedef_* now yields name of introduced type constructor
haftmann
parents:
20426
diff
changeset
|
18 |
-> theory -> (string * info) * theory |
20426 | 19 |
val get_typecopies: theory -> string list |
25506 | 20 |
val get_info: theory -> string -> info option |
25489 | 21 |
val interpretation: (string -> theory -> theory) -> theory -> theory |
28664 | 22 |
val add_typecopy_default_code: string -> theory -> theory |
22846 | 23 |
val print_typecopies: theory -> unit |
20426 | 24 |
val setup: theory -> theory |
25 |
end; |
|
26 |
||
27 |
structure TypecopyPackage: TYPECOPY_PACKAGE = |
|
28 |
struct |
|
29 |
||
30 |
(* theory data *) |
|
31 |
||
32 |
type info = { |
|
33 |
vs: (string * sort) list, |
|
34 |
constr: string, |
|
35 |
typ: typ, |
|
36 |
inject: thm, |
|
37 |
proj: string * typ, |
|
38 |
proj_def: thm |
|
39 |
}; |
|
40 |
||
41 |
structure TypecopyData = TheoryDataFun |
|
22846 | 42 |
( |
24626
85eceef2edc7
introduced generic concepts for theory interpretators
haftmann
parents:
24624
diff
changeset
|
43 |
type T = info Symtab.table; |
85eceef2edc7
introduced generic concepts for theory interpretators
haftmann
parents:
24624
diff
changeset
|
44 |
val empty = Symtab.empty; |
20426 | 45 |
val copy = I; |
46 |
val extend = I; |
|
24626
85eceef2edc7
introduced generic concepts for theory interpretators
haftmann
parents:
24624
diff
changeset
|
47 |
fun merge _ = Symtab.merge (K true); |
22846 | 48 |
); |
49 |
||
50 |
fun print_typecopies thy = |
|
51 |
let |
|
24626
85eceef2edc7
introduced generic concepts for theory interpretators
haftmann
parents:
24624
diff
changeset
|
52 |
val tab = TypecopyData.get thy; |
22846 | 53 |
fun mk (tyco, { vs, constr, typ, proj = (proj, _), ... } : info) = |
54 |
(Pretty.block o Pretty.breaks) [ |
|
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26732
diff
changeset
|
55 |
Syntax.pretty_typ_global thy (Type (tyco, map TFree vs)), |
22846 | 56 |
Pretty.str "=", |
57 |
(Pretty.str o Sign.extern_const thy) constr, |
|
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26732
diff
changeset
|
58 |
Syntax.pretty_typ_global thy typ, |
22846 | 59 |
Pretty.block [Pretty.str "(", (Pretty.str o Sign.extern_const thy) proj, Pretty.str ")"]]; |
20426 | 60 |
in |
22846 | 61 |
(Pretty.writeln o Pretty.block o Pretty.fbreaks) |
62 |
(Pretty.str "type copies:" :: map mk (Symtab.dest tab)) |
|
20426 | 63 |
end; |
64 |
||
24626
85eceef2edc7
introduced generic concepts for theory interpretators
haftmann
parents:
24624
diff
changeset
|
65 |
val get_typecopies = Symtab.keys o TypecopyData.get; |
25506 | 66 |
val get_info = Symtab.lookup o TypecopyData.get; |
20426 | 67 |
|
68 |
||
25489 | 69 |
(* interpretation of type copies *) |
20426 | 70 |
|
24711 | 71 |
structure TypecopyInterpretation = InterpretationFun(type T = string val eq = op =); |
25489 | 72 |
val interpretation = TypecopyInterpretation.interpretation; |
20426 | 73 |
|
28664 | 74 |
fun add_typecopy (raw_tyco, raw_vs) raw_ty constr_proj thy = |
20426 | 75 |
let |
28664 | 76 |
val ty = Sign.certify_typ thy raw_ty; |
29272 | 77 |
val vs = |
78 |
AList.make (the_default HOLogic.typeS o AList.lookup (op =) (Term.add_tfreesT ty [])) raw_vs; |
|
20426 | 79 |
val tac = Tactic.rtac UNIV_witness 1; |
20483
04aa552a83bc
TypedefPackage.add_typedef_* now yields name of introduced type constructor
haftmann
parents:
20426
diff
changeset
|
80 |
fun add_info tyco ( { abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs, |
20426 | 81 |
Rep_name = c_rep, Abs_inject = inject, |
21708 | 82 |
Abs_inverse = inverse, ... } : TypedefPackage.info ) thy = |
20426 | 83 |
let |
84 |
val exists_thm = |
|
85 |
UNIV_I |
|
86 |
|> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT ty_rep))] []; |
|
87 |
val inject' = inject OF [exists_thm, exists_thm]; |
|
88 |
val proj_def = inverse OF [exists_thm]; |
|
89 |
val info = { |
|
90 |
vs = vs, |
|
91 |
constr = c_abs, |
|
92 |
typ = ty_rep, |
|
93 |
inject = inject', |
|
94 |
proj = (c_rep, ty_abs --> ty_rep), |
|
95 |
proj_def = proj_def |
|
96 |
}; |
|
97 |
in |
|
98 |
thy |
|
24626
85eceef2edc7
introduced generic concepts for theory interpretators
haftmann
parents:
24624
diff
changeset
|
99 |
|> (TypecopyData.map o Symtab.update_new) (tyco, info) |
24711 | 100 |
|> TypecopyInterpretation.data tyco |
20483
04aa552a83bc
TypedefPackage.add_typedef_* now yields name of introduced type constructor
haftmann
parents:
20426
diff
changeset
|
101 |
|> pair (tyco, info) |
20426 | 102 |
end |
103 |
in |
|
104 |
thy |
|
28664 | 105 |
|> TypedefPackage.add_typedef false (SOME raw_tyco) (raw_tyco, map fst vs, NoSyn) |
26475
3cc1e48d0ce1
eliminated quiet_mode ref of some packages (avoid CRITICAL setmp!);
wenzelm
parents:
25864
diff
changeset
|
106 |
(HOLogic.mk_UNIV ty) (Option.map swap constr_proj) tac |
20483
04aa552a83bc
TypedefPackage.add_typedef_* now yields name of introduced type constructor
haftmann
parents:
20426
diff
changeset
|
107 |
|-> (fn (tyco, info) => add_info tyco info) |
20426 | 108 |
end; |
109 |
||
110 |
||
25489 | 111 |
(* code generator setup *) |
20835 | 112 |
|
28664 | 113 |
fun add_typecopy_default_code tyco thy = |
25489 | 114 |
let |
28664 | 115 |
val SOME { constr = constr_name, proj = (proj, _), proj_def = proj_eq, vs = raw_vs, |
116 |
typ = raw_ty_rep, ... } = get_info thy tyco; |
|
117 |
val inst_meet = Sorts.meet_sort_typ (Sign.classes_of thy) |
|
29875 | 118 |
(Logic.varifyT raw_ty_rep, [HOLogic.class_eq]) handle Sorts.CLASS_ERROR _ => I; |
119 |
val ty_inst = Logic.unvarifyT o inst_meet o Logic.varifyT; |
|
28664 | 120 |
val vs = (map dest_TFree o snd o dest_Type o ty_inst) |
121 |
(Type (tyco, map TFree raw_vs)); |
|
122 |
val ty_rep = ty_inst raw_ty_rep; |
|
123 |
val SOME { Rep_inject = proj_inject, ... } = TypedefPackage.get_info thy tyco; |
|
124 |
val ty_constr = Logic.unvarifyT (Sign.the_const_type thy constr_name); |
|
125 |
val constr = (constr_name, ty_constr) |
|
28423 | 126 |
val ty = Type (tyco, map TFree vs); |
28664 | 127 |
fun mk_eq ty t_x t_y = Const (@{const_name eq_class.eq}, ty --> ty --> HOLogic.boolT) |
128 |
$ t_x $ t_y; |
|
129 |
fun mk_proj t = Const (proj, ty --> ty_rep) $ t; |
|
130 |
val (t_x, t_y) = (Free ("x", ty), Free ("y", ty)); |
|
131 |
val def_eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq) |
|
29875 | 132 |
(mk_eq ty t_x t_y, HOLogic.mk_eq (mk_proj t_x, mk_proj t_y)); |
28664 | 133 |
fun mk_eq_refl thy = @{thm HOL.eq_refl} |
134 |
|> Thm.instantiate |
|
135 |
([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT ty)], []) |
|
136 |
|> AxClass.unoverload thy; |
|
25489 | 137 |
in |
25506 | 138 |
thy |
28664 | 139 |
|> Code.add_datatype [constr] |
140 |
|> Code.add_eqn proj_eq |
|
28423 | 141 |
|> TheoryTarget.instantiation ([tyco], vs, [HOLogic.class_eq]) |
28664 | 142 |
|> `(fn lthy => Syntax.check_term lthy def_eq) |
143 |
|-> (fn def_eq => Specification.definition |
|
28965 | 144 |
(NONE, (Attrib.empty_binding, def_eq))) |
28664 | 145 |
|-> (fn (_, (_, def_thm)) => |
146 |
Class.prove_instantiation_exit_result Morphism.thm |
|
147 |
(fn _ => fn def_thm => Class.intro_classes_tac [] |
|
148 |
THEN (Simplifier.rewrite_goals_tac |
|
149 |
(map Simpdata.mk_eq [def_thm, @{thm eq}, proj_inject])) |
|
150 |
THEN ALLGOALS (rtac @{thm refl})) def_thm) |
|
151 |
|-> (fn def_thm => Code.add_eqn def_thm) |
|
152 |
|> `(fn thy => mk_eq_refl thy) |
|
153 |
|-> (fn refl_thm => Code.add_nonlinear_eqn refl_thm) |
|
25489 | 154 |
end; |
20426 | 155 |
|
25489 | 156 |
val setup = |
157 |
TypecopyInterpretation.init |
|
29875 | 158 |
#> interpretation add_typecopy_default_code |
20426 | 159 |
|
22846 | 160 |
end; |