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
|
|
10 |
val add_consts: class * xstring list -> theory -> theory
|
|
11 |
val add_consts_i: class * string list -> theory -> theory
|
|
12 |
val add_tycos: class * xstring list -> theory -> theory
|
|
13 |
val add_tycos_i: class * (string * string) list -> theory -> theory
|
|
14 |
val the_consts: theory -> class -> string list
|
|
15 |
val the_tycos: theory -> class -> (string * string) list
|
|
16 |
|
|
17 |
val is_class: theory -> class -> bool
|
|
18 |
val get_arities: theory -> sort -> string -> sort list
|
|
19 |
val get_superclasses: theory -> class -> class list
|
|
20 |
val get_const_sign: theory -> string -> string * typ
|
|
21 |
val get_inst_consts_sign: theory -> string * class -> (string * typ) list
|
|
22 |
val lookup_const_class: theory -> string -> class option
|
|
23 |
val get_classtab: theory -> (string list * (string * string) list) Symtab.table
|
|
24 |
|
|
25 |
type sortcontext = (string * sort) list
|
|
26 |
datatype sortlookup = Instance of (class * string) * sortlookup list list
|
|
27 |
| Lookup of class list * (string * int)
|
|
28 |
val extract_sortctxt: theory -> typ -> sortcontext
|
|
29 |
val extract_sortlookup: theory -> typ * typ -> sortlookup list list
|
|
30 |
end;
|
|
31 |
|
|
32 |
structure ClassPackage: CLASS_PACKAGE =
|
|
33 |
struct
|
|
34 |
|
|
35 |
|
|
36 |
(* data kind 'Pure/classes' *)
|
|
37 |
|
|
38 |
type class_data = {
|
|
39 |
locale_name: string,
|
|
40 |
axclass_name: string,
|
|
41 |
consts: string list,
|
|
42 |
tycos: (string * string) list
|
|
43 |
};
|
|
44 |
|
|
45 |
structure ClassesData = TheoryDataFun (
|
|
46 |
struct
|
|
47 |
val name = "Pure/classes";
|
|
48 |
type T = class_data Symtab.table * class Symtab.table;
|
|
49 |
val empty = (Symtab.empty, Symtab.empty);
|
|
50 |
val copy = I;
|
|
51 |
val extend = I;
|
|
52 |
fun merge _ ((t1, r1), (t2, r2))=
|
|
53 |
(Symtab.merge (op =) (t1, t2),
|
|
54 |
Symtab.merge (op =) (r1, r2));
|
|
55 |
fun print _ (tab, _) = (Pretty.writeln o Pretty.chunks) (map Pretty.str (Symtab.keys tab));
|
|
56 |
end
|
|
57 |
);
|
|
58 |
|
|
59 |
val lookup_class_data = Symtab.lookup o fst o ClassesData.get;
|
|
60 |
val lookup_const_class = Symtab.lookup o snd o ClassesData.get;
|
|
61 |
|
|
62 |
fun get_class_data thy class =
|
|
63 |
case lookup_class_data thy class
|
|
64 |
of NONE => error ("undeclared class " ^ quote class)
|
|
65 |
| SOME data => data;
|
|
66 |
|
|
67 |
fun put_class_data class data =
|
|
68 |
ClassesData.map (apfst (Symtab.update (class, data)));
|
|
69 |
fun add_const class const =
|
|
70 |
ClassesData.map (apsnd (Symtab.update (const, class)));
|
|
71 |
|
|
72 |
|
|
73 |
(* name mangling *)
|
|
74 |
|
|
75 |
fun get_locale_for_class thy class =
|
|
76 |
#locale_name (get_class_data thy class);
|
|
77 |
|
|
78 |
fun get_axclass_for_class thy class =
|
|
79 |
#axclass_name (get_class_data thy class);
|
|
80 |
|
|
81 |
|
|
82 |
(* assign consts to type classes *)
|
|
83 |
|
|
84 |
local
|
|
85 |
|
|
86 |
fun gen_add_consts prep_class prep_const (raw_class, raw_consts_new) thy =
|
|
87 |
let
|
|
88 |
val class = prep_class thy raw_class;
|
|
89 |
val consts_new = map (prep_const thy) raw_consts_new;
|
|
90 |
val {locale_name, axclass_name, consts, tycos} =
|
|
91 |
get_class_data thy class;
|
|
92 |
in
|
|
93 |
thy
|
|
94 |
|> put_class_data class {
|
|
95 |
locale_name = locale_name,
|
|
96 |
axclass_name = axclass_name,
|
|
97 |
consts = consts @ consts_new,
|
|
98 |
tycos = tycos
|
|
99 |
}
|
|
100 |
|> fold (add_const class) consts_new
|
|
101 |
end;
|
|
102 |
|
|
103 |
in
|
|
104 |
|
|
105 |
val add_consts = gen_add_consts Sign.intern_class Sign.intern_const;
|
|
106 |
val add_consts_i = gen_add_consts (K I) (K I);
|
|
107 |
|
|
108 |
end; (* local *)
|
|
109 |
|
|
110 |
val the_consts = #consts oo get_class_data;
|
|
111 |
|
|
112 |
|
|
113 |
(* assign type constructors to type classes *)
|
|
114 |
|
|
115 |
local
|
|
116 |
|
|
117 |
fun gen_add_tycos prep_class prep_type (raw_class, raw_tycos_new) thy =
|
|
118 |
let
|
|
119 |
val class = prep_class thy raw_class
|
|
120 |
val tycos_new = map (prep_type thy) raw_tycos_new
|
|
121 |
val {locale_name, axclass_name, consts, tycos} =
|
|
122 |
get_class_data thy class
|
|
123 |
in
|
|
124 |
thy
|
|
125 |
|> put_class_data class {
|
|
126 |
locale_name = locale_name,
|
|
127 |
axclass_name = axclass_name,
|
|
128 |
consts = consts,
|
|
129 |
tycos = tycos @ tycos_new
|
|
130 |
}
|
|
131 |
end;
|
|
132 |
|
|
133 |
in
|
|
134 |
|
|
135 |
fun add_tycos xs thy =
|
|
136 |
gen_add_tycos Sign.intern_class (rpair (Context.theory_name thy) oo Sign.intern_type) xs thy;
|
|
137 |
val add_tycos_i = gen_add_tycos (K I) (K I);
|
|
138 |
|
|
139 |
end; (* local *)
|
|
140 |
|
|
141 |
val the_tycos = #tycos oo get_class_data;
|
|
142 |
|
|
143 |
|
|
144 |
(* class queries *)
|
|
145 |
|
|
146 |
fun is_class thy = is_some o lookup_class_data thy;
|
|
147 |
|
|
148 |
fun filter_class thy = filter (is_class thy);
|
|
149 |
|
|
150 |
fun assert_class thy class =
|
|
151 |
if is_class thy class then class
|
|
152 |
else error ("not a class: " ^ quote class);
|
|
153 |
|
|
154 |
fun get_arities thy sort tycon =
|
|
155 |
Sorts.mg_domain (Sign.classes_arities_of thy) tycon sort
|
|
156 |
|> (map o map) (assert_class thy);
|
|
157 |
|
|
158 |
fun get_superclasses thy class =
|
|
159 |
Sorts.superclasses (Sign.classes_of thy) class
|
|
160 |
|> filter_class thy;
|
|
161 |
|
|
162 |
|
|
163 |
(* instance queries *)
|
|
164 |
|
|
165 |
fun get_const_sign thy const =
|
|
166 |
let
|
|
167 |
val class = (the o lookup_const_class thy) const;
|
|
168 |
val ty = (Type.unvarifyT o Sign.the_const_constraint thy) const;
|
|
169 |
val tvar = fold_atyps
|
|
170 |
(fn TFree (tvar, sort) =>
|
|
171 |
if Sorts.sort_eq (Sign.classes_of thy) ([class], sort) then K (SOME tvar) else I | _ => I) ty NONE
|
|
172 |
|> the;
|
|
173 |
val ty' = map_type_tfree (fn (tvar', sort) =>
|
|
174 |
if tvar' = tvar
|
|
175 |
then TFree (tvar, [])
|
|
176 |
else TFree (tvar', sort)
|
|
177 |
) ty;
|
|
178 |
in (tvar, ty') end;
|
|
179 |
|
|
180 |
fun get_inst_consts_sign thy (tyco, class) =
|
|
181 |
let
|
|
182 |
val consts = the_consts thy class;
|
|
183 |
val arities = get_arities thy [class] tyco;
|
|
184 |
val const_signs = map (get_const_sign thy) consts;
|
|
185 |
val vars_used = fold (fn (tvar, ty) => curry (gen_union (op =))
|
|
186 |
(map fst (typ_tfrees ty) |> remove (op =) tvar)) const_signs [];
|
|
187 |
val vars_new = Term.invent_names vars_used "'a" (length arities);
|
|
188 |
val typ_arity = Type (tyco, map2 TFree (vars_new, arities));
|
|
189 |
val instmem_signs =
|
|
190 |
map (fn (tvar, ty) => typ_subst_atomic [(TFree (tvar, []), typ_arity)] ty) const_signs;
|
|
191 |
in consts ~~ instmem_signs end;
|
|
192 |
|
|
193 |
fun get_classtab thy =
|
|
194 |
Symtab.fold
|
|
195 |
(fn (class, { consts = consts, tycos = tycos, ... }) =>
|
|
196 |
Symtab.update_new (class, (consts, tycos)))
|
|
197 |
(fst (ClassesData.get thy)) Symtab.empty;
|
|
198 |
|
|
199 |
|
|
200 |
(* extracting dictionary obligations from types *)
|
|
201 |
|
|
202 |
type sortcontext = (string * sort) list;
|
|
203 |
|
|
204 |
fun extract_sortctxt thy typ =
|
|
205 |
(typ_tfrees o Type.unvarifyT) typ
|
|
206 |
|> map (apsnd (filter_class thy))
|
|
207 |
|> filter (not o null o snd);
|
|
208 |
|
|
209 |
datatype sortlookup = Instance of (class * string) * sortlookup list list
|
|
210 |
| Lookup of class list * (string * int)
|
|
211 |
|
|
212 |
fun extract_sortlookup thy (raw_typ_def, raw_typ_use) =
|
|
213 |
let
|
|
214 |
val typ_def = Type.varifyT raw_typ_def;
|
|
215 |
val typ_use = Type.varifyT raw_typ_use;
|
|
216 |
val match_tab = Sign.typ_match thy (typ_def, typ_use) Vartab.empty;
|
|
217 |
fun tab_lookup vname = (the o Vartab.lookup match_tab) (vname, 0);
|
|
218 |
fun get_superclass_derivation (subclasses, superclass) =
|
|
219 |
(the oo get_first) (fn subclass =>
|
|
220 |
Sorts.class_le_path (Sign.classes_of thy) (subclass, superclass)
|
|
221 |
) subclasses;
|
|
222 |
fun mk_class_deriv thy subclasses superclass =
|
|
223 |
case get_superclass_derivation (subclasses, superclass)
|
|
224 |
of (subclass::deriv) => (rev deriv, find_index_eq subclass subclasses);
|
|
225 |
fun mk_lookup (sort_def, (Type (tycon, tys))) =
|
|
226 |
let
|
|
227 |
val arity_lookup = map2 mk_lookup
|
|
228 |
(map (filter_class thy) (Sorts.mg_domain (Sign.classes_arities_of thy) tycon sort_def), tys)
|
|
229 |
in map (fn class => Instance ((class, tycon), arity_lookup)) sort_def end
|
|
230 |
| mk_lookup (sort_def, TVar ((vname, _), sort_use)) =
|
|
231 |
let
|
|
232 |
fun mk_look class =
|
|
233 |
let val (deriv, classindex) = mk_class_deriv thy sort_use class
|
|
234 |
in Lookup (deriv, (vname, classindex)) end;
|
|
235 |
in map mk_look sort_def end;
|
|
236 |
in
|
|
237 |
extract_sortctxt thy raw_typ_def
|
|
238 |
|> map (tab_lookup o fst)
|
|
239 |
|> map (apfst (filter_class thy))
|
|
240 |
|> filter (not o null o fst)
|
|
241 |
|> map mk_lookup
|
|
242 |
end;
|
|
243 |
|
|
244 |
|
|
245 |
(* outer syntax *)
|
|
246 |
|
|
247 |
local
|
|
248 |
|
|
249 |
structure P = OuterParse
|
|
250 |
and K = OuterKeyword;
|
|
251 |
|
|
252 |
in
|
|
253 |
|
|
254 |
val classcgK = "codegen_class";
|
|
255 |
|
|
256 |
fun classcg raw_class raw_consts raw_tycos thy =
|
|
257 |
let
|
|
258 |
val class = Sign.intern_class thy raw_class;
|
|
259 |
in
|
|
260 |
thy
|
|
261 |
|> put_class_data class {
|
|
262 |
locale_name = "",
|
|
263 |
axclass_name = class,
|
|
264 |
consts = [],
|
|
265 |
tycos = []
|
|
266 |
}
|
|
267 |
|> add_consts (class, raw_consts)
|
|
268 |
|> add_tycos (class, raw_tycos)
|
|
269 |
end
|
|
270 |
|
|
271 |
val classcgP =
|
|
272 |
OuterSyntax.command classcgK "codegen data for classes" K.thy_decl (
|
|
273 |
P.xname
|
|
274 |
-- ((P.$$$ "\\<Rightarrow>" || P.$$$ "=>") |-- (P.list1 P.name))
|
|
275 |
-- (Scan.optional ((P.$$$ "\\<Rightarrow>" || P.$$$ "=>") |-- (P.list1 P.name)) [])
|
|
276 |
>> (fn ((name, tycos), consts) => (Toplevel.theory (classcg name consts tycos)))
|
|
277 |
)
|
|
278 |
|
|
279 |
val _ = OuterSyntax.add_parsers [classcgP];
|
|
280 |
|
|
281 |
val _ = OuterSyntax.add_keywords ["\\<Rightarrow>", "=>"];
|
|
282 |
|
|
283 |
end; (* local *)
|
|
284 |
|
|
285 |
|
|
286 |
(* setup *)
|
|
287 |
|
|
288 |
val _ = Context.add_setup [ClassesData.init];
|
|
289 |
|
|
290 |
end; (* struct *)
|