1 (* Title: Pure/hugsclass.ML |
|
2 ID: $Id$ |
|
3 Author: Florian Haftmann, TU Muenchen |
|
4 |
|
5 Haskell98-like type classes, logically simulated by locales ("hugsclass") |
|
6 *) |
|
7 |
|
8 (*!!! for now, only experimental scratch code !!!*) |
|
9 |
|
10 signature HUGSCLASS = |
|
11 sig |
|
12 val add_hugsclass: bstring -> xstring list -> Locale.element list -> theory -> theory |
|
13 (* val add_hugsclass_i: bstring -> string list -> Locale.element list -> theory -> theory *) |
|
14 |
|
15 val get_locale_for_hugsclass: theory -> string -> string |
|
16 val get_axclass_for_hugsclass: theory -> string -> class |
|
17 val add_members_x: xstring * xstring list -> theory -> theory |
|
18 val add_members: string * string list -> theory -> theory |
|
19 val add_tycons_x: xstring * xstring list -> theory -> theory |
|
20 val add_tycons: string * string list -> theory -> theory |
|
21 val the_members: theory -> class -> string list |
|
22 val the_tycons: theory -> class -> string list |
|
23 |
|
24 val is_hugsclass: theory -> class -> bool |
|
25 val get_arities: theory -> sort -> string -> sort list |
|
26 val get_superclasses: theory -> class -> class list |
|
27 end; |
|
28 |
|
29 structure Hugsclass : HUGSCLASS = |
|
30 struct |
|
31 |
|
32 |
|
33 |
|
34 (** data kind 'Pure/classes' **) |
|
35 |
|
36 type hugsclass_info = { |
|
37 locale_name: string, |
|
38 axclass_name: string, |
|
39 members: string list, |
|
40 tycons: string list |
|
41 }; |
|
42 |
|
43 structure HugsclassesData = TheoryDataFun ( |
|
44 struct |
|
45 val name = "Pure/hugsclasses"; |
|
46 type T = hugsclass_info Symtab.table; |
|
47 val empty = Symtab.empty; |
|
48 val copy = I; |
|
49 val extend = I; |
|
50 fun merge _ = Symtab.merge (K true); |
|
51 fun print _ tab = (Pretty.writeln o Pretty.chunks) (map Pretty.str (Symtab.keys tab)); |
|
52 end |
|
53 ); |
|
54 |
|
55 val _ = Context.add_setup [HugsclassesData.init]; |
|
56 val print_hugsclasses = HugsclassesData.print; |
|
57 |
|
58 fun lookup_hugsclass_info thy class = Symtab.lookup (HugsclassesData.get thy, class); |
|
59 |
|
60 fun get_hugsclass_info thy class = |
|
61 case lookup_hugsclass_info thy class |
|
62 of NONE => error ("undeclared hugs class " ^ quote class) |
|
63 | SOME info => info; |
|
64 |
|
65 fun put_hugsclass_info class info thy = |
|
66 thy |
|
67 |> HugsclassesData.put (Symtab.update ((class, info), HugsclassesData.get thy)); |
|
68 |
|
69 |
|
70 (* name mangling *) |
|
71 |
|
72 fun get_locale_for_hugsclass thy class = |
|
73 #locale_name (get_hugsclass_info thy class) |
|
74 |
|
75 fun get_axclass_for_hugsclass thy class = |
|
76 #axclass_name (get_hugsclass_info thy class) |
|
77 |
|
78 |
|
79 (* assign members to type classes *) |
|
80 |
|
81 local |
|
82 |
|
83 fun gen_add_members prep_class prep_member (raw_class, raw_members_new) thy = |
|
84 let |
|
85 val class = prep_class thy raw_class |
|
86 val members_new = map (prep_member thy) raw_members_new |
|
87 val {locale_name, axclass_name, members, tycons} = |
|
88 get_hugsclass_info thy class |
|
89 in |
|
90 thy |
|
91 |> put_hugsclass_info class { |
|
92 locale_name = locale_name, |
|
93 axclass_name = axclass_name, |
|
94 members = members @ members_new, |
|
95 tycons = tycons |
|
96 } |
|
97 end |
|
98 |
|
99 in |
|
100 |
|
101 val add_members_x = gen_add_members Sign.intern_class Sign.intern_const |
|
102 val add_members = gen_add_members (K I) (K I) |
|
103 |
|
104 end |
|
105 |
|
106 |
|
107 (* assign type constructors to type classes *) |
|
108 |
|
109 local |
|
110 |
|
111 fun gen_add_tycons prep_class prep_type (raw_class, raw_tycons_new) thy = |
|
112 let |
|
113 val class = prep_class thy raw_class |
|
114 val tycons_new = map (prep_type thy) raw_tycons_new |
|
115 val {locale_name, axclass_name, members, tycons} = |
|
116 get_hugsclass_info thy class |
|
117 in |
|
118 thy |
|
119 |> put_hugsclass_info class { |
|
120 locale_name = locale_name, |
|
121 axclass_name = axclass_name, |
|
122 members = members, |
|
123 tycons = tycons @ tycons_new |
|
124 } |
|
125 end; |
|
126 |
|
127 in |
|
128 |
|
129 val add_tycons_x = gen_add_tycons Sign.intern_class Sign.intern_type |
|
130 val add_tycons = gen_add_tycons (K I) (K I) |
|
131 |
|
132 end |
|
133 |
|
134 |
|
135 (* retrieve members *) |
|
136 |
|
137 val the_members = (#members oo get_hugsclass_info) |
|
138 |
|
139 |
|
140 (* retrieve type constructor associations *) |
|
141 |
|
142 val the_tycons = (#tycons oo get_hugsclass_info) |
|
143 |
|
144 |
|
145 |
|
146 (** class declaration **) |
|
147 |
|
148 local |
|
149 |
|
150 fun gen_add_hugsclass prep_class bname raw_superclss raw_locelems thy = |
|
151 let |
|
152 val name_class = Sign.full_name thy bname |
|
153 val name_loc = Sign.full_name thy bname |
|
154 val superclss = map (prep_class thy) raw_superclss |
|
155 val _ = map (get_hugsclass_info thy) superclss |
|
156 val defaultS = Sign.defaultS thy |
|
157 val axsuperclss = case superclss of [] => defaultS |
|
158 | _ => superclss |
|
159 val locexpr = |
|
160 superclss |
|
161 |> map (get_locale_for_hugsclass thy) |
|
162 |> map (Locale.Locale) |
|
163 |> Locale.Merge |
|
164 (* fun inferT_axm pre_tm = |
|
165 let |
|
166 val pp = Sign.pp thy; |
|
167 val (t, _) = Sign.infer_types pp thy (K NONE) (K NONE) [] true ([pre_tm], TFree ("a", [])); |
|
168 in t end |
|
169 fun axiom_for members = (bname, inferT_axm |
|
170 (ObjectLogic.assert_propT thy (list_comb (Const (name, dummyT), map (fn (mname, mtyp, _) => Const (mname, mtyp)) members)))) *) |
|
171 fun constify thy (mname, mtyp, _) = Const (Sign.intern_const thy mname, mtyp) |
|
172 fun axiom_for loc members thy = case Sign.const_type thy loc |
|
173 of SOME pred_type => [((bname, |
|
174 (ObjectLogic.assert_propT thy |
|
175 (list_comb (Const (loc, Type.unvarifyT pred_type), map (constify thy) members)))), []) |
|
176 ] |
|
177 | NONE => (writeln "--- no const_type"; []) |
|
178 fun get_members locname thy = |
|
179 let |
|
180 val ctxt = ProofContext.init thy |
|
181 |> Locale.read_context_statement (SOME locname) [] [] |
|
182 |> #4 |
|
183 |> `(fn ctxt => ((writeln o commas o ProofContext.fixed_names_of) ctxt; ctxt)) |> snd |
|
184 val ctx' = ProofContext.init thy |
|
185 |> Locale.read_context_statement (SOME locname) [] [] |
|
186 |> #3 |
|
187 |> `(fn ctxt => ((writeln o commas o ProofContext.fixed_names_of) ctxt; ctxt)) |> snd |
|
188 val fixed = ProofContext.fixed_names_of ctxt |
|
189 fun mk_member fixed = (fixed, (the o ProofContext.default_type ctxt) fixed, NoSyn) |
|
190 in map mk_member fixed end; |
|
191 fun add_constraint class (mname, mtyp, _) thy = |
|
192 let |
|
193 val classes = snd (#classes (Type.rep_tsig (#tsig (Sign.rep_sg thy)))) |
|
194 val tfree = case (typ_tfrees o Type.unvarifyT) mtyp |
|
195 of [(tfree, sort)] => if Sorts.sort_eq classes (sort, defaultS) |
|
196 then tfree |
|
197 else error ("sort constraint not permitted in member " ^ quote mname) |
|
198 | _ => error ("no or more than one type variable in declaration for member " ^ quote mname) |
|
199 fun constrain_tfree (tfree, _) = TFree (tfree, [class]) |
|
200 in Sign.add_const_constraint_i |
|
201 (Sign.intern_const thy mname, map_type_tfree constrain_tfree mtyp) thy |
|
202 end; |
|
203 in |
|
204 thy |
|
205 |> Locale.add_locale true bname locexpr raw_locelems |
|
206 |> `(fn _ => writeln "(1) added locale") |> snd |
|
207 |> `(get_members name_loc) |
|
208 |-> (fn members => |
|
209 Sign.add_consts_i members |
|
210 #> `(fn _ => writeln "(2) added members") #> snd |
|
211 #> `(axiom_for name_loc members) |
|
212 #-> (fn axiom => |
|
213 AxClass.add_axclass_i (bname, axsuperclss) axiom #> fst |
|
214 #> `(fn _ => writeln "(3) added axclass") #> snd |
|
215 #> fold (add_constraint name_class) members |
|
216 #> `(fn _ => writeln "(4) constrained members") #> snd |
|
217 #> add_members (name_class, map #1 members) |
|
218 #> `(fn _ => writeln "(5) added class members") #> snd |
|
219 #> put_hugsclass_info name_class { |
|
220 locale_name = name_loc, |
|
221 axclass_name = name_class, |
|
222 members = [], |
|
223 tycons = [] |
|
224 } |
|
225 )) |
|
226 end |
|
227 |
|
228 in |
|
229 |
|
230 val add_hugsclass = gen_add_hugsclass (Sign.intern_class); |
|
231 val add_hugsclass_i = gen_add_hugsclass (K I); |
|
232 |
|
233 end; |
|
234 |
|
235 |
|
236 |
|
237 (** technical class relations *) |
|
238 |
|
239 fun is_hugsclass thy = can (the_tycons thy) |
|
240 |
|
241 fun get_arities thy sort tycons = |
|
242 let |
|
243 val tsig = Type.rep_tsig (#tsig (Sign.rep_sg thy)) |
|
244 val clss_arities = (snd (#classes tsig), #arities tsig) |
|
245 in |
|
246 Sorts.mg_domain clss_arities tycons sort |
|
247 |> map (filter (is_hugsclass thy)) |
|
248 (*!!! assert -> error on fail *) |
|
249 end |
|
250 |
|
251 fun get_superclasses thy class = |
|
252 Sorts.direct_supercls (snd (#classes (Type.rep_tsig (#tsig (Sign.rep_sg thy))))) class |
|
253 |> filter (is_hugsclass thy) |
|
254 |
|
255 |
|
256 (** outer syntax **) |
|
257 |
|
258 local |
|
259 |
|
260 structure P = OuterParse |
|
261 and K = OuterSyntax.Keyword |
|
262 |
|
263 in |
|
264 |
|
265 val (classK, extendsK) = ("class", "extends") |
|
266 |
|
267 val classP = |
|
268 OuterSyntax.command classK "define type class" K.thy_decl ( |
|
269 P.name |
|
270 -- Scan.optional (P.$$$ extendsK |-- P.list1 P.xname) [] |
|
271 -- Scan.repeat P.locale_element |
|
272 >> (fn (((name, superclss), locelems)) |
|
273 => Toplevel.theory (add_hugsclass name superclss locelems)) |
|
274 ) |
|
275 |
|
276 val (instanceK, whereK) = ("inst", "where") |
|
277 |
|
278 val instanceP = |
|
279 OuterSyntax.command instanceK "prove type arity" K.thy_goal (( |
|
280 Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 (P.group "sort" P.xname) --| P.$$$ ")")) [] |
|
281 -- P.xname --| P.$$$ "::" |
|
282 -- P.group "class" P.xname |
|
283 -- Scan.optional (P.$$$ whereK |-- Scan.repeat1 P.spec_name) []) |
|
284 >> (fn (((arity, ty), class), defs) |
|
285 => |
|
286 Toplevel.theory (IsarThy.add_defs (true, defs)) |
|
287 #> (AxClass.instance_arity_proof (ty, arity, class) |
|
288 |> (Toplevel.print oo Toplevel.theory_to_proof)) |
|
289 ) |
|
290 ) |
|
291 |
|
292 val _ = OuterSyntax.add_parsers [classP, instanceP] |
|
293 |
|
294 val _ = OuterSyntax.add_keywords [extendsK] |
|
295 |
|
296 end |
|
297 |
|
298 end |
|
299 |
|
300 (* |
|
301 |
|
302 PureThy.add_thms [Thm.no_attributes (intro_name bclass, intro)] |
|
303 get_thm thy PureThy. |
|
304 |
|
305 rename intro rule |
|
306 check defs -> should contain any member |
|
307 wie syntax extrahieren? |
|
308 cases für locales |
|
309 |
|
310 isomorphism |
|
311 |
|
312 locale sg = fixes prod assumes assoc: ... |
|
313 |
|
314 consts prod :: "'a::type => 'a => 'a" |
|
315 |
|
316 axclass sg < type |
|
317 sg: "sg prod" |
|
318 |
|
319 constraints prod :: "'a::sg => 'a => 'a" |
|
320 |
|
321 |
|
322 theory Scratch imports Main begin |
|
323 |
|
324 (* class definition *) |
|
325 |
|
326 locale sg = |
|
327 fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<degree>" 60) |
|
328 assumes assoc: "(x \<degree> y) \<degree> z = x \<degree> (y \<degree> z)" |
|
329 |
|
330 classes sg |
|
331 consts prod :: "'a::sg \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<degree>\<degree>" 60) |
|
332 classrel sg < type |
|
333 axioms sg: "sg prod" |
|
334 |
|
335 interpretation sg: sg [prod] by (rule sg) |
|
336 |
|
337 |
|
338 (* abstract reasoning *) |
|
339 |
|
340 lemma (in sg) |
|
341 bar: "x \<degree> y = x \<degree> y" .. |
|
342 |
|
343 lemma baz: |
|
344 fixes x :: "'a::sg" |
|
345 shows "x \<degree>\<degree> y = x \<degree>\<degree> y" .. |
|
346 |
|
347 (* class instantiation *) |
|
348 |
|
349 interpretation sg_list: sg ["op @"] |
|
350 by (rule sg.intro) (simp only: append_assoc) |
|
351 arities list :: (type) sg |
|
352 defs (overloaded) prod_list_def: "prod == op @" |
|
353 |
|
354 interpretation sg_prod: sg ["%p q. (fst p \<degree>\<degree> fst q, snd p \<degree>\<degree> snd q)"] |
|
355 by (rule sg.intro) (simp add: sg.assoc) |
|
356 |
|
357 arities * :: (sg, sg) sg |
|
358 |
|
359 *) |
|