author | haftmann |
Tue, 03 Jan 2006 11:32:16 +0100 | |
changeset 18550 | 59b89f625d68 |
parent 18515 | 1cad5c2b2a0b |
child 18575 | 9ccfd1d1e874 |
permissions | -rw-r--r-- |
18168 | 1 |
(* Title: Pure/Tools/class_package.ML |
2 |
ID: $Id$ |
|
3 |
Author: Florian Haftmann, TU Muenchen |
|
4 |
||
5 |
Haskell98-like operational view on type classes. |
|
6 |
*) |
|
7 |
||
8 |
signature CLASS_PACKAGE = |
|
9 |
sig |
|
18515 | 10 |
val add_class: bstring -> Locale.expr -> Element.context list -> theory |
11 |
-> ProofContext.context * theory |
|
12 |
val add_class_i: bstring -> Locale.expr -> Element.context_i list -> theory |
|
13 |
-> ProofContext.context * theory |
|
14 |
val add_classentry: class -> xstring list -> xstring list -> theory -> theory |
|
18168 | 15 |
val the_consts: theory -> class -> string list |
16 |
val the_tycos: theory -> class -> (string * string) list |
|
17 |
||
18360 | 18 |
val syntactic_sort_of: theory -> sort -> sort |
18168 | 19 |
val get_arities: theory -> sort -> string -> sort list |
20 |
val get_superclasses: theory -> class -> class list |
|
18304 | 21 |
val get_const_sign: theory -> string -> string -> typ |
18168 | 22 |
val get_inst_consts_sign: theory -> string * class -> (string * typ) list |
23 |
val lookup_const_class: theory -> string -> class option |
|
24 |
val get_classtab: theory -> (string list * (string * string) list) Symtab.table |
|
25 |
||
26 |
type sortcontext = (string * sort) list |
|
27 |
datatype sortlookup = Instance of (class * string) * sortlookup list list |
|
28 |
| Lookup of class list * (string * int) |
|
29 |
val extract_sortctxt: theory -> typ -> sortcontext |
|
30 |
val extract_sortlookup: theory -> typ * typ -> sortlookup list list |
|
31 |
end; |
|
32 |
||
33 |
structure ClassPackage: CLASS_PACKAGE = |
|
34 |
struct |
|
35 |
||
36 |
||
37 |
(* data kind 'Pure/classes' *) |
|
38 |
||
39 |
type class_data = { |
|
40 |
locale_name: string, |
|
41 |
axclass_name: string, |
|
42 |
consts: string list, |
|
43 |
tycos: (string * string) list |
|
44 |
}; |
|
45 |
||
46 |
structure ClassesData = TheoryDataFun ( |
|
47 |
struct |
|
48 |
val name = "Pure/classes"; |
|
49 |
type T = class_data Symtab.table * class Symtab.table; |
|
50 |
val empty = (Symtab.empty, Symtab.empty); |
|
51 |
val copy = I; |
|
52 |
val extend = I; |
|
53 |
fun merge _ ((t1, r1), (t2, r2))= |
|
54 |
(Symtab.merge (op =) (t1, t2), |
|
55 |
Symtab.merge (op =) (r1, r2)); |
|
56 |
fun print _ (tab, _) = (Pretty.writeln o Pretty.chunks) (map Pretty.str (Symtab.keys tab)); |
|
57 |
end |
|
58 |
); |
|
59 |
||
60 |
val lookup_class_data = Symtab.lookup o fst o ClassesData.get; |
|
61 |
val lookup_const_class = Symtab.lookup o snd o ClassesData.get; |
|
62 |
||
63 |
fun get_class_data thy class = |
|
64 |
case lookup_class_data thy class |
|
65 |
of NONE => error ("undeclared class " ^ quote class) |
|
66 |
| SOME data => data; |
|
67 |
||
68 |
fun put_class_data class data = |
|
69 |
ClassesData.map (apfst (Symtab.update (class, data))); |
|
70 |
fun add_const class const = |
|
71 |
ClassesData.map (apsnd (Symtab.update (const, class))); |
|
18515 | 72 |
val the_consts = #consts oo get_class_data; |
73 |
val the_tycos = #tycos oo get_class_data; |
|
18168 | 74 |
|
75 |
||
76 |
(* name mangling *) |
|
77 |
||
78 |
fun get_locale_for_class thy class = |
|
79 |
#locale_name (get_class_data thy class); |
|
80 |
||
81 |
fun get_axclass_for_class thy class = |
|
82 |
#axclass_name (get_class_data thy class); |
|
83 |
||
84 |
||
18515 | 85 |
(* classes *) |
18168 | 86 |
|
87 |
local |
|
88 |
||
18515 | 89 |
open Element |
90 |
||
91 |
fun gen_add_class add_locale bname raw_import raw_body thy = |
|
18168 | 92 |
let |
18515 | 93 |
fun extract_notes_consts thy elems = |
94 |
elems |
|
18550
59b89f625d68
add_local_context now yields imported and body elements seperatly; additional slight clenup in code
haftmann
parents:
18515
diff
changeset
|
95 |
|> Library.flat |
18515 | 96 |
|> List.mapPartial |
97 |
(fn (Notes notes) => SOME notes |
|
98 |
| _ => NONE) |
|
99 |
|> Library.flat |
|
100 |
|> map (fn (_, facts) => map fst facts) |
|
101 |
|> Library.flat o Library.flat |
|
102 |
|> map prop_of |
|
103 |
|> (fn ts => fold (curry add_term_consts) ts []) |
|
104 |
|> tap (writeln o commas); |
|
105 |
fun extract_tyvar_name thy tys = |
|
106 |
fold (curry add_typ_tfrees) tys [] |
|
107 |
|> (fn [(v, [])] => v |
|
108 |
| [(v, sort)] => |
|
109 |
if Sorts.sort_eq (Sign.classes_of thy) (Sign.defaultS thy, sort) |
|
110 |
then v |
|
111 |
else error ("sort constraint on class type variable: " ^ Sign.string_of_sort thy sort) |
|
112 |
| [] => error ("no class type variable") |
|
113 |
| vs => error ("more than one type variable: " ^ (commas o map (Sign.string_of_typ thy o TFree)) vs)) |
|
114 |
fun extract_tyvar_consts thy elems = |
|
115 |
elems |
|
18550
59b89f625d68
add_local_context now yields imported and body elements seperatly; additional slight clenup in code
haftmann
parents:
18515
diff
changeset
|
116 |
|> Library.flat |
18515 | 117 |
|> List.mapPartial |
118 |
(fn (Fixes consts) => SOME consts |
|
119 |
| _ => NONE) |
|
120 |
|> Library.flat |
|
121 |
|> map (fn (c, ty, syn) => ((c, the ty), the syn)) |
|
122 |
|> `(fn consts => extract_tyvar_name thy (map (snd o fst) consts)); |
|
123 |
(* fun remove_local_syntax ((c, ty), _) thy = |
|
124 |
thy |
|
125 |
|> Sign.add_syntax_i [(c, ty, Syntax.NoSyn)]; *) |
|
126 |
fun add_global_const ((c, ty), syn) thy = |
|
127 |
thy |
|
128 |
|> Sign.add_consts_i [(c, ty, syn)] |
|
129 |
|> `(fn thy => Sign.intern_const thy c) |
|
130 |
fun add_axclass bname_axiom locale_pred cs thy = |
|
131 |
thy |
|
132 |
|> AxClass.add_axclass_i (bname, Sign.defaultS thy) |
|
133 |
[Thm.no_attributes (bname_axiom, |
|
134 |
Const (ObjectLogic.judgment_name thy, dummyT) $ |
|
135 |
list_comb (Const (locale_pred, dummyT), map (fn c => Const (c, dummyT)) cs) |
|
136 |
|> curry (inferT_axm thy) "locale_pred" |> snd)] |
|
137 |
|-> (fn _ => `(fn thy => Sign.intern_class thy bname)) |
|
138 |
fun print_ctxt ctxt elem = |
|
139 |
map Pretty.writeln (Element.pretty_ctxt ctxt elem) |
|
18168 | 140 |
in |
141 |
thy |
|
18515 | 142 |
|> add_locale bname raw_import raw_body |
18550
59b89f625d68
add_local_context now yields imported and body elements seperatly; additional slight clenup in code
haftmann
parents:
18515
diff
changeset
|
143 |
|-> (fn ((_, elems : context_i list list), ctxt) => |
59b89f625d68
add_local_context now yields imported and body elements seperatly; additional slight clenup in code
haftmann
parents:
18515
diff
changeset
|
144 |
tap (fn _ => (map o map) (print_ctxt ctxt) elems) |
18515 | 145 |
#> tap (fn thy => extract_notes_consts thy elems) |
146 |
#> `(fn thy => Locale.intern thy bname) |
|
147 |
#-> (fn name_locale => |
|
148 |
`(fn thy => extract_tyvar_consts thy elems) |
|
149 |
#-> (fn (v, consts) => |
|
150 |
fold_map add_global_const consts |
|
151 |
#-> (fn cs => |
|
152 |
add_axclass (bname ^ "_intro") name_locale cs |
|
153 |
#-> (fn name_axclass => |
|
154 |
put_class_data name_locale { |
|
155 |
locale_name = name_locale, |
|
156 |
axclass_name = name_axclass, |
|
157 |
consts = cs, |
|
158 |
tycos = [] |
|
159 |
}) |
|
160 |
#> fold (add_const name_locale) cs |
|
161 |
#> pair ctxt |
|
162 |
)))) |
|
18168 | 163 |
end; |
164 |
||
165 |
in |
|
166 |
||
18515 | 167 |
val add_class = gen_add_class (Locale.add_locale_context true); |
168 |
val add_class_i = gen_add_class (Locale.add_locale_context_i true); |
|
18168 | 169 |
|
170 |
end; (* local *) |
|
171 |
||
172 |
||
173 |
(* class queries *) |
|
174 |
||
18360 | 175 |
fun is_class thy cls = lookup_class_data thy cls |> Option.map (not o null o #consts) |> the_default false; |
18168 | 176 |
|
18360 | 177 |
fun syntactic_sort_of thy sort = |
178 |
let |
|
179 |
val classes = Sign.classes_of thy; |
|
180 |
fun get_sort cls = |
|
181 |
if is_class thy cls |
|
182 |
then [cls] |
|
183 |
else syntactic_sort_of thy (Sorts.superclasses classes cls); |
|
184 |
in |
|
185 |
map get_sort sort |
|
186 |
|> Library.flat |
|
187 |
|> Sorts.norm_sort classes |
|
188 |
end; |
|
18168 | 189 |
|
190 |
fun get_arities thy sort tycon = |
|
18515 | 191 |
Sorts.mg_domain (Sign.classes_arities_of thy) tycon (syntactic_sort_of thy sort) |
18360 | 192 |
|> map (syntactic_sort_of thy); |
18168 | 193 |
|
194 |
fun get_superclasses thy class = |
|
18515 | 195 |
if is_class thy class |
196 |
then |
|
197 |
Sorts.superclasses (Sign.classes_of thy) class |
|
198 |
|> syntactic_sort_of thy |
|
199 |
else |
|
200 |
error ("no syntactic class: " ^ class); |
|
18168 | 201 |
|
202 |
||
203 |
(* instance queries *) |
|
204 |
||
18304 | 205 |
fun get_const_sign thy tvar const = |
18168 | 206 |
let |
207 |
val class = (the o lookup_const_class thy) const; |
|
18335 | 208 |
val (ty, thaw) = (Type.freeze_thaw_type o Sign.the_const_constraint thy) const; |
18304 | 209 |
val tvars_used = Term.add_tfreesT ty []; |
210 |
val tvar_rename = hd (Term.invent_names (map fst tvars_used) tvar 1); |
|
211 |
in |
|
212 |
ty |
|
213 |
|> map_type_tfree (fn (tvar', sort) => |
|
214 |
if Sorts.sort_eq (Sign.classes_of thy) ([class], sort) |
|
215 |
then TFree (tvar, []) |
|
216 |
else if tvar' = tvar |
|
18335 | 217 |
then TVar ((tvar_rename, 0), sort) |
18304 | 218 |
else TFree (tvar', sort)) |
18335 | 219 |
|> thaw |
18304 | 220 |
end; |
18168 | 221 |
|
222 |
fun get_inst_consts_sign thy (tyco, class) = |
|
223 |
let |
|
224 |
val consts = the_consts thy class; |
|
225 |
val arities = get_arities thy [class] tyco; |
|
18304 | 226 |
val const_signs = map (get_const_sign thy "'a") consts; |
227 |
val vars_used = fold (fn ty => curry (gen_union (op =)) |
|
228 |
(map fst (typ_tfrees ty) |> remove (op =) "'a")) const_signs []; |
|
18168 | 229 |
val vars_new = Term.invent_names vars_used "'a" (length arities); |
18330 | 230 |
val typ_arity = Type (tyco, map2 (curry TFree) vars_new arities); |
18168 | 231 |
val instmem_signs = |
18335 | 232 |
map (typ_subst_TVars [(("'a", 0), typ_arity)]) const_signs; |
18168 | 233 |
in consts ~~ instmem_signs end; |
234 |
||
235 |
fun get_classtab thy = |
|
236 |
Symtab.fold |
|
237 |
(fn (class, { consts = consts, tycos = tycos, ... }) => |
|
238 |
Symtab.update_new (class, (consts, tycos))) |
|
239 |
(fst (ClassesData.get thy)) Symtab.empty; |
|
240 |
||
241 |
||
242 |
(* extracting dictionary obligations from types *) |
|
243 |
||
244 |
type sortcontext = (string * sort) list; |
|
245 |
||
18335 | 246 |
fun extract_sortctxt thy ty = |
247 |
(typ_tfrees o Type.no_tvars) ty |
|
18360 | 248 |
|> map (apsnd (syntactic_sort_of thy)) |
18168 | 249 |
|> filter (not o null o snd); |
250 |
||
251 |
datatype sortlookup = Instance of (class * string) * sortlookup list list |
|
252 |
| Lookup of class list * (string * int) |
|
253 |
||
254 |
fun extract_sortlookup thy (raw_typ_def, raw_typ_use) = |
|
255 |
let |
|
256 |
val typ_def = Type.varifyT raw_typ_def; |
|
257 |
val typ_use = Type.varifyT raw_typ_use; |
|
258 |
val match_tab = Sign.typ_match thy (typ_def, typ_use) Vartab.empty; |
|
259 |
fun tab_lookup vname = (the o Vartab.lookup match_tab) (vname, 0); |
|
260 |
fun get_superclass_derivation (subclasses, superclass) = |
|
261 |
(the oo get_first) (fn subclass => |
|
262 |
Sorts.class_le_path (Sign.classes_of thy) (subclass, superclass) |
|
263 |
) subclasses; |
|
264 |
fun mk_class_deriv thy subclasses superclass = |
|
265 |
case get_superclass_derivation (subclasses, superclass) |
|
18515 | 266 |
of (subclass::deriv) => |
267 |
((rev o filter (is_class thy)) deriv, find_index_eq subclass subclasses); |
|
18168 | 268 |
fun mk_lookup (sort_def, (Type (tycon, tys))) = |
269 |
let |
|
18330 | 270 |
val arity_lookup = map2 (curry mk_lookup) |
18360 | 271 |
(map (syntactic_sort_of thy) (Sorts.mg_domain (Sign.classes_arities_of thy) tycon sort_def)) tys |
18168 | 272 |
in map (fn class => Instance ((class, tycon), arity_lookup)) sort_def end |
273 |
| mk_lookup (sort_def, TVar ((vname, _), sort_use)) = |
|
274 |
let |
|
275 |
fun mk_look class = |
|
18515 | 276 |
let val (deriv, classindex) = mk_class_deriv thy (syntactic_sort_of thy sort_use) class |
18168 | 277 |
in Lookup (deriv, (vname, classindex)) end; |
278 |
in map mk_look sort_def end; |
|
279 |
in |
|
18335 | 280 |
extract_sortctxt thy ((fst o Type.freeze_thaw_type) raw_typ_def) |
18168 | 281 |
|> map (tab_lookup o fst) |
18360 | 282 |
|> map (apfst (syntactic_sort_of thy)) |
18168 | 283 |
|> filter (not o null o fst) |
284 |
|> map mk_lookup |
|
285 |
end; |
|
286 |
||
287 |
||
18335 | 288 |
(* intermediate auxiliary *) |
18168 | 289 |
|
18515 | 290 |
fun add_classentry raw_class raw_cs raw_tycos thy = |
18168 | 291 |
let |
292 |
val class = Sign.intern_class thy raw_class; |
|
18515 | 293 |
val cs = map (Sign.intern_const thy) raw_cs; |
294 |
val tycos = map (rpair (Context.theory_name thy) o Sign.intern_type thy) raw_tycos; |
|
18168 | 295 |
in |
296 |
thy |
|
297 |
|> put_class_data class { |
|
298 |
locale_name = "", |
|
299 |
axclass_name = class, |
|
18515 | 300 |
consts = cs, |
301 |
tycos = tycos |
|
18168 | 302 |
} |
18515 | 303 |
|> fold (add_const class) cs |
18335 | 304 |
end; |
18515 | 305 |
|
306 |
||
307 |
(* toplevel interface *) |
|
308 |
||
309 |
local |
|
310 |
||
311 |
structure P = OuterParse |
|
312 |
and K = OuterKeyword |
|
313 |
||
314 |
in |
|
315 |
||
18550
59b89f625d68
add_local_context now yields imported and body elements seperatly; additional slight clenup in code
haftmann
parents:
18515
diff
changeset
|
316 |
val classK = "class" |
18515 | 317 |
|
318 |
val locale_val = |
|
319 |
(P.locale_expr -- |
|
320 |
Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 P.context_element)) [] || |
|
321 |
Scan.repeat1 P.context_element >> pair Locale.empty); |
|
322 |
||
323 |
val classP = |
|
324 |
OuterSyntax.command classK "operational type classes" K.thy_decl |
|
325 |
(P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, []) |
|
326 |
>> (Toplevel.theory_context |
|
327 |
o (fn f => swap o f) o (fn (name, (expr, elems)) => add_class name expr elems))); |
|
328 |
||
329 |
val _ = OuterSyntax.add_parsers [classP]; |
|
330 |
||
331 |
end; (* local *) |
|
332 |
||
18168 | 333 |
|
334 |
(* setup *) |
|
335 |
||
336 |
val _ = Context.add_setup [ClassesData.init]; |
|
337 |
||
338 |
end; (* struct *) |