1 (* Title: Pure/Isar/class_target.ML |
|
2 Author: Florian Haftmann, TU Muenchen |
|
3 |
|
4 Type classes derived from primitive axclasses and locales -- mechanisms. |
|
5 *) |
|
6 |
|
7 signature CLASS_TARGET = |
|
8 sig |
|
9 (*classes*) |
|
10 val register: class -> class list -> ((string * typ) * (string * typ)) list |
|
11 -> sort -> morphism -> morphism -> thm option -> thm option -> thm |
|
12 -> theory -> theory |
|
13 |
|
14 val is_class: theory -> class -> bool |
|
15 val base_sort: theory -> class -> sort |
|
16 val rules: theory -> class -> thm option * thm |
|
17 val these_params: theory -> sort -> (string * (class * (string * typ))) list |
|
18 val these_defs: theory -> sort -> thm list |
|
19 val these_operations: theory -> sort |
|
20 -> (string * (class * (typ * term))) list |
|
21 val print_classes: theory -> unit |
|
22 |
|
23 val begin: class list -> sort -> Proof.context -> Proof.context |
|
24 val init: class -> theory -> Proof.context |
|
25 val declare: class -> (binding * mixfix) * (term list * term) -> theory -> theory |
|
26 val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> theory -> theory |
|
27 val class_prefix: string -> string |
|
28 val refresh_syntax: class -> Proof.context -> Proof.context |
|
29 val redeclare_operations: theory -> sort -> Proof.context -> Proof.context |
|
30 |
|
31 (*instances*) |
|
32 val init_instantiation: string list * (string * sort) list * sort |
|
33 -> theory -> Proof.context |
|
34 val instance_arity_cmd: xstring list * xstring list * xstring -> theory -> Proof.state |
|
35 val instantiation_instance: (local_theory -> local_theory) |
|
36 -> local_theory -> Proof.state |
|
37 val prove_instantiation_instance: (Proof.context -> tactic) |
|
38 -> local_theory -> local_theory |
|
39 val prove_instantiation_exit: (Proof.context -> tactic) |
|
40 -> local_theory -> theory |
|
41 val prove_instantiation_exit_result: (morphism -> 'a -> 'b) |
|
42 -> (Proof.context -> 'b -> tactic) -> 'a -> local_theory -> 'b * theory |
|
43 val conclude_instantiation: local_theory -> local_theory |
|
44 val instantiation_param: local_theory -> binding -> string option |
|
45 val confirm_declaration: binding -> local_theory -> local_theory |
|
46 val pretty_instantiation: local_theory -> Pretty.T |
|
47 val read_multi_arity: theory -> xstring list * xstring list * xstring |
|
48 -> string list * (string * sort) list * sort |
|
49 val type_name: string -> string |
|
50 val instantiation: string list * (string * sort) list * sort -> theory -> local_theory |
|
51 val instantiation_cmd: xstring list * xstring list * xstring -> theory -> local_theory |
|
52 |
|
53 (*subclasses*) |
|
54 val register_subclass: class * class -> morphism option -> Element.witness option |
|
55 -> morphism -> theory -> theory |
|
56 val classrel: class * class -> theory -> Proof.state |
|
57 val classrel_cmd: xstring * xstring -> theory -> Proof.state |
|
58 |
|
59 (*tactics*) |
|
60 val intro_classes_tac: thm list -> tactic |
|
61 val default_intro_tac: Proof.context -> thm list -> tactic |
|
62 end; |
|
63 |
|
64 structure Class_Target : CLASS_TARGET = |
|
65 struct |
|
66 |
|
67 (** class data **) |
|
68 |
|
69 datatype class_data = ClassData of { |
|
70 |
|
71 (* static part *) |
|
72 consts: (string * string) list |
|
73 (*locale parameter ~> constant name*), |
|
74 base_sort: sort, |
|
75 base_morph: morphism |
|
76 (*static part of canonical morphism*), |
|
77 export_morph: morphism, |
|
78 assm_intro: thm option, |
|
79 of_class: thm, |
|
80 axiom: thm option, |
|
81 |
|
82 (* dynamic part *) |
|
83 defs: thm list, |
|
84 operations: (string * (class * (typ * term))) list |
|
85 |
|
86 }; |
|
87 |
|
88 fun make_class_data ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom), |
|
89 (defs, operations)) = |
|
90 ClassData { consts = consts, base_sort = base_sort, |
|
91 base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro, |
|
92 of_class = of_class, axiom = axiom, defs = defs, operations = operations }; |
|
93 fun map_class_data f (ClassData { consts, base_sort, base_morph, export_morph, assm_intro, |
|
94 of_class, axiom, defs, operations }) = |
|
95 make_class_data (f ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom), |
|
96 (defs, operations))); |
|
97 fun merge_class_data _ (ClassData { consts = consts, |
|
98 base_sort = base_sort, base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro, |
|
99 of_class = of_class, axiom = axiom, defs = defs1, operations = operations1 }, |
|
100 ClassData { consts = _, base_sort = _, base_morph = _, export_morph = _, assm_intro = _, |
|
101 of_class = _, axiom = _, defs = defs2, operations = operations2 }) = |
|
102 make_class_data ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom), |
|
103 (Thm.merge_thms (defs1, defs2), |
|
104 AList.merge (op =) (K true) (operations1, operations2))); |
|
105 |
|
106 structure ClassData = Theory_Data |
|
107 ( |
|
108 type T = class_data Graph.T |
|
109 val empty = Graph.empty; |
|
110 val extend = I; |
|
111 val merge = Graph.join merge_class_data; |
|
112 ); |
|
113 |
|
114 |
|
115 (* queries *) |
|
116 |
|
117 fun lookup_class_data thy class = case try (Graph.get_node (ClassData.get thy)) class |
|
118 of SOME (ClassData data) => SOME data |
|
119 | NONE => NONE; |
|
120 |
|
121 fun the_class_data thy class = case lookup_class_data thy class |
|
122 of NONE => error ("Undeclared class " ^ quote class) |
|
123 | SOME data => data; |
|
124 |
|
125 val is_class = is_some oo lookup_class_data; |
|
126 |
|
127 val ancestry = Graph.all_succs o ClassData.get; |
|
128 val heritage = Graph.all_preds o ClassData.get; |
|
129 |
|
130 fun these_params thy = |
|
131 let |
|
132 fun params class = |
|
133 let |
|
134 val const_typs = (#params o AxClass.get_info thy) class; |
|
135 val const_names = (#consts o the_class_data thy) class; |
|
136 in |
|
137 (map o apsnd) |
|
138 (fn c => (class, (c, (the o AList.lookup (op =) const_typs) c))) const_names |
|
139 end; |
|
140 in maps params o ancestry thy end; |
|
141 |
|
142 val base_sort = #base_sort oo the_class_data; |
|
143 |
|
144 fun rules thy class = |
|
145 let val { axiom, of_class, ... } = the_class_data thy class |
|
146 in (axiom, of_class) end; |
|
147 |
|
148 fun all_assm_intros thy = |
|
149 Graph.fold (fn (_, (ClassData { assm_intro, ... }, _)) => fold (insert Thm.eq_thm) |
|
150 (the_list assm_intro)) (ClassData.get thy) []; |
|
151 |
|
152 fun these_defs thy = maps (#defs o the_class_data thy) o ancestry thy; |
|
153 fun these_operations thy = maps (#operations o the_class_data thy) o ancestry thy; |
|
154 |
|
155 val base_morphism = #base_morph oo the_class_data; |
|
156 fun morphism thy class = case Element.eq_morphism thy (these_defs thy [class]) |
|
157 of SOME eq_morph => base_morphism thy class $> eq_morph |
|
158 | NONE => base_morphism thy class; |
|
159 val export_morphism = #export_morph oo the_class_data; |
|
160 |
|
161 fun print_classes thy = |
|
162 let |
|
163 val ctxt = ProofContext.init_global thy; |
|
164 val algebra = Sign.classes_of thy; |
|
165 val arities = |
|
166 Symtab.empty |
|
167 |> Symtab.fold (fn (tyco, arities) => fold (fn (class, _) => |
|
168 Symtab.map_default (class, []) (insert (op =) tyco)) arities) |
|
169 (Sorts.arities_of algebra); |
|
170 val the_arities = these o Symtab.lookup arities; |
|
171 fun mk_arity class tyco = |
|
172 let |
|
173 val Ss = Sorts.mg_domain algebra tyco [class]; |
|
174 in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end; |
|
175 fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: " |
|
176 ^ setmp_CRITICAL show_sorts false (Syntax.string_of_typ ctxt o Type.strip_sorts) ty); |
|
177 fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [ |
|
178 (SOME o Pretty.str) ("class " ^ Sign.extern_class thy class ^ ":"), |
|
179 (SOME o Pretty.block) [Pretty.str "supersort: ", |
|
180 (Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes thy) class], |
|
181 ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks) |
|
182 (Pretty.str "parameters:" :: ps)) o map mk_param |
|
183 o these o Option.map #params o try (AxClass.get_info thy)) class, |
|
184 (SOME o Pretty.block o Pretty.breaks) [ |
|
185 Pretty.str "instances:", |
|
186 Pretty.list "" "" (map (mk_arity class) (the_arities class)) |
|
187 ] |
|
188 ] |
|
189 in |
|
190 (Pretty.writeln o Pretty.chunks o separate (Pretty.str "") |
|
191 o map mk_entry o Sorts.all_classes) algebra |
|
192 end; |
|
193 |
|
194 |
|
195 (* updaters *) |
|
196 |
|
197 fun register class sups params base_sort base_morph export_morph |
|
198 axiom assm_intro of_class thy = |
|
199 let |
|
200 val operations = map (fn (v_ty as (_, ty), (c, _)) => |
|
201 (c, (class, (ty, Free v_ty)))) params; |
|
202 val add_class = Graph.new_node (class, |
|
203 make_class_data (((map o pairself) fst params, base_sort, |
|
204 base_morph, export_morph, assm_intro, of_class, axiom), ([], operations))) |
|
205 #> fold (curry Graph.add_edge class) sups; |
|
206 in ClassData.map add_class thy end; |
|
207 |
|
208 fun activate_defs class thms thy = case Element.eq_morphism thy thms |
|
209 of SOME eq_morph => fold (fn cls => fn thy => |
|
210 Context.theory_map (Locale.amend_registration (cls, base_morphism thy cls) |
|
211 (eq_morph, true) (export_morphism thy cls)) thy) (heritage thy [class]) thy |
|
212 | NONE => thy; |
|
213 |
|
214 fun register_operation class (c, (t, some_def)) thy = |
|
215 let |
|
216 val base_sort = base_sort thy class; |
|
217 val prep_typ = map_type_tfree |
|
218 (fn (v, sort) => if Name.aT = v |
|
219 then TFree (v, base_sort) else TVar ((v, 0), sort)); |
|
220 val t' = map_types prep_typ t; |
|
221 val ty' = Term.fastype_of t'; |
|
222 in |
|
223 thy |
|
224 |> (ClassData.map o Graph.map_node class o map_class_data o apsnd) |
|
225 (fn (defs, operations) => |
|
226 (fold cons (the_list some_def) defs, |
|
227 (c, (class, (ty', t'))) :: operations)) |
|
228 |> activate_defs class (the_list some_def) |
|
229 end; |
|
230 |
|
231 fun register_subclass (sub, sup) some_dep_morph some_wit export thy = |
|
232 let |
|
233 val intros = (snd o rules thy) sup :: map_filter I |
|
234 [Option.map (Drule.export_without_context_open o Element.conclude_witness) some_wit, |
|
235 (fst o rules thy) sub]; |
|
236 val tac = EVERY (map (TRYALL o Tactic.rtac) intros); |
|
237 val classrel = Skip_Proof.prove_global thy [] [] (Logic.mk_classrel (sub, sup)) |
|
238 (K tac); |
|
239 val diff_sort = Sign.complete_sort thy [sup] |
|
240 |> subtract (op =) (Sign.complete_sort thy [sub]) |
|
241 |> filter (is_class thy); |
|
242 val add_dependency = case some_dep_morph |
|
243 of SOME dep_morph => Locale.add_dependency sub |
|
244 (sup, dep_morph $> Element.satisfy_morphism (the_list some_wit)) export |
|
245 | NONE => I |
|
246 in |
|
247 thy |
|
248 |> AxClass.add_classrel classrel |
|
249 |> ClassData.map (Graph.add_edge (sub, sup)) |
|
250 |> activate_defs sub (these_defs thy diff_sort) |
|
251 |> add_dependency |
|
252 end; |
|
253 |
|
254 |
|
255 (** classes and class target **) |
|
256 |
|
257 (* class context syntax *) |
|
258 |
|
259 fun these_unchecks thy = map (fn (c, (_, (ty, t))) => (t, Const (c, ty))) |
|
260 o these_operations thy; |
|
261 |
|
262 fun redeclare_const thy c = |
|
263 let val b = Long_Name.base_name c |
|
264 in Sign.intern_const thy b = c ? Variable.declare_const (b, c) end; |
|
265 |
|
266 fun synchronize_class_syntax sort base_sort ctxt = |
|
267 let |
|
268 val thy = ProofContext.theory_of ctxt; |
|
269 val algebra = Sign.classes_of thy; |
|
270 val operations = these_operations thy sort; |
|
271 fun subst_class_typ sort = map_type_tfree (K (TVar ((Name.aT, 0), sort))); |
|
272 val primary_constraints = |
|
273 (map o apsnd) (subst_class_typ base_sort o fst o snd) operations; |
|
274 val secondary_constraints = |
|
275 (map o apsnd) (fn (class, (ty, _)) => subst_class_typ [class] ty) operations; |
|
276 fun improve (c, ty) = (case AList.lookup (op =) primary_constraints c |
|
277 of SOME ty' => (case try (Type.raw_match (ty', ty)) Vartab.empty |
|
278 of SOME tyenv => (case Vartab.lookup tyenv (Name.aT, 0) |
|
279 of SOME (_, ty' as TVar (vi, sort)) => |
|
280 if Type_Infer.is_param vi |
|
281 andalso Sorts.sort_le algebra (base_sort, sort) |
|
282 then SOME (ty', TFree (Name.aT, base_sort)) |
|
283 else NONE |
|
284 | _ => NONE) |
|
285 | NONE => NONE) |
|
286 | NONE => NONE) |
|
287 fun subst (c, ty) = Option.map snd (AList.lookup (op =) operations c); |
|
288 val unchecks = these_unchecks thy sort; |
|
289 in |
|
290 ctxt |
|
291 |> fold (redeclare_const thy o fst) primary_constraints |
|
292 |> Overloading.map_improvable_syntax (K (((primary_constraints, secondary_constraints), |
|
293 (((improve, subst), true), unchecks)), false)) |
|
294 |> Overloading.set_primary_constraints |
|
295 end; |
|
296 |
|
297 fun refresh_syntax class ctxt = |
|
298 let |
|
299 val thy = ProofContext.theory_of ctxt; |
|
300 val base_sort = base_sort thy class; |
|
301 in synchronize_class_syntax [class] base_sort ctxt end; |
|
302 |
|
303 fun redeclare_operations thy sort = |
|
304 fold (redeclare_const thy o fst) (these_operations thy sort); |
|
305 |
|
306 fun begin sort base_sort ctxt = |
|
307 ctxt |
|
308 |> Variable.declare_term |
|
309 (Logic.mk_type (TFree (Name.aT, base_sort))) |
|
310 |> synchronize_class_syntax sort base_sort |
|
311 |> Overloading.add_improvable_syntax; |
|
312 |
|
313 fun init class thy = |
|
314 thy |
|
315 |> Locale.init class |
|
316 |> begin [class] (base_sort thy class); |
|
317 |
|
318 |
|
319 (* class target *) |
|
320 |
|
321 val class_prefix = Logic.const_of_class o Long_Name.base_name; |
|
322 |
|
323 fun declare class ((c, mx), (type_params, dict)) thy = |
|
324 let |
|
325 val morph = morphism thy class; |
|
326 val b = Morphism.binding morph c; |
|
327 val b_def = Morphism.binding morph (Binding.suffix_name "_dict" b); |
|
328 val c' = Sign.full_name thy b; |
|
329 val dict' = Morphism.term morph dict; |
|
330 val ty' = map Term.fastype_of type_params ---> Term.fastype_of dict'; |
|
331 val def_eq = Logic.mk_equals (list_comb (Const (c', ty'), type_params), dict') |
|
332 |> map_types Type.strip_sorts; |
|
333 in |
|
334 thy |
|
335 |> Sign.declare_const ((b, Type.strip_sorts ty'), mx) |
|
336 |> snd |
|
337 |> Thm.add_def false false (b_def, def_eq) |
|
338 |>> apsnd Thm.varifyT_global |
|
339 |-> (fn (_, def_thm) => PureThy.store_thm (b_def, def_thm) |
|
340 #> snd |
|
341 #> null type_params ? register_operation class (c', (dict', SOME (Thm.symmetric def_thm)))) |
|
342 |> Sign.add_const_constraint (c', SOME ty') |
|
343 end; |
|
344 |
|
345 fun abbrev class prmode ((c, mx), rhs) thy = |
|
346 let |
|
347 val morph = morphism thy class; |
|
348 val unchecks = these_unchecks thy [class]; |
|
349 val b = Morphism.binding morph c; |
|
350 val c' = Sign.full_name thy b; |
|
351 val rhs' = Pattern.rewrite_term thy unchecks [] rhs; |
|
352 val ty' = Term.fastype_of rhs'; |
|
353 val rhs'' = map_types Logic.varifyT_global rhs'; |
|
354 in |
|
355 thy |
|
356 |> Sign.add_abbrev (#1 prmode) (b, rhs'') |
|
357 |> snd |
|
358 |> Sign.add_const_constraint (c', SOME ty') |
|
359 |> Sign.notation true prmode [(Const (c', ty'), mx)] |
|
360 |> not (#1 prmode = Print_Mode.input) ? register_operation class (c', (rhs', NONE)) |
|
361 end; |
|
362 |
|
363 |
|
364 (* simple subclasses *) |
|
365 |
|
366 local |
|
367 |
|
368 fun gen_classrel mk_prop classrel thy = |
|
369 let |
|
370 fun after_qed results = |
|
371 ProofContext.theory ((fold o fold) AxClass.add_classrel results); |
|
372 in |
|
373 thy |
|
374 |> ProofContext.init_global |
|
375 |> Proof.theorem NONE after_qed [[(mk_prop thy classrel, [])]] |
|
376 end; |
|
377 |
|
378 in |
|
379 |
|
380 val classrel = |
|
381 gen_classrel (Logic.mk_classrel oo AxClass.cert_classrel); |
|
382 val classrel_cmd = |
|
383 gen_classrel (Logic.mk_classrel oo AxClass.read_classrel); |
|
384 |
|
385 end; (*local*) |
|
386 |
|
387 |
|
388 (** instantiation target **) |
|
389 |
|
390 (* bookkeeping *) |
|
391 |
|
392 datatype instantiation = Instantiation of { |
|
393 arities: string list * (string * sort) list * sort, |
|
394 params: ((string * string) * (string * typ)) list |
|
395 (*(instantiation parameter, type constructor), (local instantiation parameter, typ)*) |
|
396 } |
|
397 |
|
398 structure Instantiation = Proof_Data |
|
399 ( |
|
400 type T = instantiation |
|
401 fun init _ = Instantiation { arities = ([], [], []), params = [] }; |
|
402 ); |
|
403 |
|
404 fun mk_instantiation (arities, params) = |
|
405 Instantiation { arities = arities, params = params }; |
|
406 fun get_instantiation lthy = case Instantiation.get (Local_Theory.target_of lthy) |
|
407 of Instantiation data => data; |
|
408 fun map_instantiation f = (Local_Theory.target o Instantiation.map) |
|
409 (fn Instantiation { arities, params } => mk_instantiation (f (arities, params))); |
|
410 |
|
411 fun the_instantiation lthy = case get_instantiation lthy |
|
412 of { arities = ([], [], []), ... } => error "No instantiation target" |
|
413 | data => data; |
|
414 |
|
415 val instantiation_params = #params o get_instantiation; |
|
416 |
|
417 fun instantiation_param lthy b = instantiation_params lthy |
|
418 |> find_first (fn (_, (v, _)) => Binding.name_of b = v) |
|
419 |> Option.map (fst o fst); |
|
420 |
|
421 fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) = |
|
422 let |
|
423 val ctxt = ProofContext.init_global thy; |
|
424 val all_arities = map (fn raw_tyco => ProofContext.read_arity ctxt |
|
425 (raw_tyco, raw_sorts, raw_sort)) raw_tycos; |
|
426 val tycos = map #1 all_arities; |
|
427 val (_, sorts, sort) = hd all_arities; |
|
428 val vs = Name.names Name.context Name.aT sorts; |
|
429 in (tycos, vs, sort) end; |
|
430 |
|
431 |
|
432 (* syntax *) |
|
433 |
|
434 fun synchronize_inst_syntax ctxt = |
|
435 let |
|
436 val Instantiation { params, ... } = Instantiation.get ctxt; |
|
437 |
|
438 val lookup_inst_param = AxClass.lookup_inst_param |
|
439 (Sign.consts_of (ProofContext.theory_of ctxt)) params; |
|
440 fun subst (c, ty) = case lookup_inst_param (c, ty) |
|
441 of SOME (v_ty as (_, ty)) => SOME (ty, Free v_ty) |
|
442 | NONE => NONE; |
|
443 val unchecks = |
|
444 map (fn ((c, _), v_ty as (_, ty)) => (Free v_ty, Const (c, ty))) params; |
|
445 in |
|
446 ctxt |
|
447 |> Overloading.map_improvable_syntax |
|
448 (fn (((primary_constraints, _), (((improve, _), _), _)), _) => |
|
449 (((primary_constraints, []), (((improve, subst), false), unchecks)), false)) |
|
450 end; |
|
451 |
|
452 |
|
453 (* target *) |
|
454 |
|
455 val sanitize_name = (*necessary as long as "dirty" type identifiers are permitted*) |
|
456 let |
|
457 fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s |
|
458 orelse s = "'" orelse s = "_"; |
|
459 val is_junk = not o is_valid andf Symbol.is_regular; |
|
460 val junk = Scan.many is_junk; |
|
461 val scan_valids = Symbol.scanner "Malformed input" |
|
462 ((junk |-- |
|
463 (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.many is_valid >> implode) |
|
464 --| junk)) |
|
465 ::: Scan.repeat ((Scan.many1 is_valid >> implode) --| junk)); |
|
466 in |
|
467 explode #> scan_valids #> implode |
|
468 end; |
|
469 |
|
470 val type_name = sanitize_name o Long_Name.base_name; |
|
471 |
|
472 fun resort_terms pp algebra consts constraints ts = |
|
473 let |
|
474 fun matchings (Const (c_ty as (c, _))) = (case constraints c |
|
475 of NONE => I |
|
476 | SOME sorts => fold2 (curry (Sorts.meet_sort algebra)) |
|
477 (Consts.typargs consts c_ty) sorts) |
|
478 | matchings _ = I |
|
479 val tvartab = (fold o fold_aterms) matchings ts Vartab.empty |
|
480 handle Sorts.CLASS_ERROR e => error (Sorts.class_error pp e); |
|
481 val inst = map_type_tvar |
|
482 (fn (vi, sort) => TVar (vi, the_default sort (Vartab.lookup tvartab vi))); |
|
483 in if Vartab.is_empty tvartab then NONE else SOME ((map o map_types) inst ts) end; |
|
484 |
|
485 fun init_instantiation (tycos, vs, sort) thy = |
|
486 let |
|
487 val _ = if null tycos then error "At least one arity must be given" else (); |
|
488 val class_params = these_params thy (filter (can (AxClass.get_info thy)) sort); |
|
489 fun get_param tyco (param, (_, (c, ty))) = |
|
490 if can (AxClass.param_of_inst thy) (c, tyco) |
|
491 then NONE else SOME ((c, tyco), |
|
492 (param ^ "_" ^ type_name tyco, map_atyps (K (Type (tyco, map TFree vs))) ty)); |
|
493 val params = map_product get_param tycos class_params |> map_filter I; |
|
494 val primary_constraints = map (apsnd |
|
495 (map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) class_params; |
|
496 val pp = Syntax.pp_global thy; |
|
497 val algebra = Sign.classes_of thy |
|
498 |> fold (fn tyco => Sorts.add_arities pp |
|
499 (tyco, map (fn class => (class, map snd vs)) sort)) tycos; |
|
500 val consts = Sign.consts_of thy; |
|
501 val improve_constraints = AList.lookup (op =) |
|
502 (map (fn (_, (class, (c, _))) => (c, [[class]])) class_params); |
|
503 fun resort_check ts ctxt = case resort_terms (Syntax.pp ctxt) algebra consts improve_constraints ts |
|
504 of NONE => NONE |
|
505 | SOME ts' => SOME (ts', ctxt); |
|
506 val lookup_inst_param = AxClass.lookup_inst_param consts params; |
|
507 val typ_instance = Type.typ_instance (Sign.tsig_of thy); |
|
508 fun improve (c, ty) = case lookup_inst_param (c, ty) |
|
509 of SOME (_, ty') => if typ_instance (ty', ty) then SOME (ty, ty') else NONE |
|
510 | NONE => NONE; |
|
511 in |
|
512 thy |
|
513 |> Theory.checkpoint |
|
514 |> ProofContext.init_global |
|
515 |> Instantiation.put (mk_instantiation ((tycos, vs, sort), params)) |
|
516 |> fold (Variable.declare_typ o TFree) vs |
|
517 |> fold (Variable.declare_names o Free o snd) params |
|
518 |> (Overloading.map_improvable_syntax o apfst) |
|
519 (K ((primary_constraints, []), (((improve, K NONE), false), []))) |
|
520 |> Overloading.add_improvable_syntax |
|
521 |> Context.proof_map (Syntax.add_term_check 0 "resorting" resort_check) |
|
522 |> synchronize_inst_syntax |
|
523 end; |
|
524 |
|
525 fun confirm_declaration b = (map_instantiation o apsnd) |
|
526 (filter_out (fn (_, (c', _)) => c' = Binding.name_of b)) |
|
527 #> Local_Theory.target synchronize_inst_syntax |
|
528 |
|
529 fun gen_instantiation_instance do_proof after_qed lthy = |
|
530 let |
|
531 val (tycos, vs, sort) = (#arities o the_instantiation) lthy; |
|
532 val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, map snd vs, sort)) tycos; |
|
533 fun after_qed' results = |
|
534 Local_Theory.theory (fold (AxClass.add_arity o Thm.varifyT_global) results) |
|
535 #> after_qed; |
|
536 in |
|
537 lthy |
|
538 |> do_proof after_qed' arities_proof |
|
539 end; |
|
540 |
|
541 val instantiation_instance = gen_instantiation_instance (fn after_qed => fn ts => |
|
542 Proof.theorem NONE (after_qed o map the_single) (map (fn t => [(t, [])]) ts)); |
|
543 |
|
544 fun prove_instantiation_instance tac = gen_instantiation_instance (fn after_qed => |
|
545 fn ts => fn lthy => after_qed (map (fn t => Goal.prove lthy [] [] t |
|
546 (fn {context, ...} => tac context)) ts) lthy) I; |
|
547 |
|
548 fun prove_instantiation_exit tac = prove_instantiation_instance tac |
|
549 #> Local_Theory.exit_global; |
|
550 |
|
551 fun prove_instantiation_exit_result f tac x lthy = |
|
552 let |
|
553 val morph = ProofContext.export_morphism lthy |
|
554 (ProofContext.init_global (ProofContext.theory_of lthy)); |
|
555 val y = f morph x; |
|
556 in |
|
557 lthy |
|
558 |> prove_instantiation_exit (fn ctxt => tac ctxt y) |
|
559 |> pair y |
|
560 end; |
|
561 |
|
562 fun conclude_instantiation lthy = |
|
563 let |
|
564 val (tycos, vs, sort) = (#arities o the_instantiation) lthy; |
|
565 val thy = ProofContext.theory_of lthy; |
|
566 val _ = map (fn tyco => if Sign.of_sort thy |
|
567 (Type (tyco, map TFree vs), sort) |
|
568 then () else error ("Missing instance proof for type " ^ quote (Sign.extern_type thy tyco))) |
|
569 tycos; |
|
570 in lthy end; |
|
571 |
|
572 fun pretty_instantiation lthy = |
|
573 let |
|
574 val { arities = (tycos, vs, sort), params } = the_instantiation lthy; |
|
575 val thy = ProofContext.theory_of lthy; |
|
576 fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort); |
|
577 fun pr_param ((c, _), (v, ty)) = |
|
578 (Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==", |
|
579 (Pretty.str o Sign.extern_const thy) c, Pretty.str "::", Syntax.pretty_typ_global thy ty]; |
|
580 in |
|
581 (Pretty.block o Pretty.fbreaks) |
|
582 (Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params) |
|
583 end; |
|
584 |
|
585 fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c); |
|
586 |
|
587 fun instantiation_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy = |
|
588 case instantiation_param lthy b |
|
589 of SOME c => if mx <> NoSyn then syntax_error c |
|
590 else lthy |> Local_Theory.theory_result (AxClass.declare_overloaded (c, U) |
|
591 ##>> AxClass.define_overloaded b_def (c, rhs)) |
|
592 ||> confirm_declaration b |
|
593 | NONE => lthy |> |
|
594 Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params); |
|
595 |
|
596 fun instantiation arities thy = |
|
597 thy |
|
598 |> init_instantiation arities |
|
599 |> Local_Theory.init NONE "" |
|
600 {define = Generic_Target.define instantiation_foundation, |
|
601 notes = Generic_Target.notes |
|
602 (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts), |
|
603 abbrev = Generic_Target.abbrev |
|
604 (fn prmode => fn (b, mx) => fn (t, _) => fn _ => Generic_Target.theory_abbrev prmode ((b, mx), t)), |
|
605 declaration = K Generic_Target.theory_declaration, |
|
606 syntax_declaration = K Generic_Target.theory_declaration, |
|
607 pretty = single o pretty_instantiation, |
|
608 reinit = instantiation arities o ProofContext.theory_of, |
|
609 exit = Local_Theory.target_of o conclude_instantiation}; |
|
610 |
|
611 fun instantiation_cmd arities thy = |
|
612 instantiation (read_multi_arity thy arities) thy; |
|
613 |
|
614 |
|
615 (* simplified instantiation interface with no class parameter *) |
|
616 |
|
617 fun instance_arity_cmd raw_arities thy = |
|
618 let |
|
619 val (tycos, vs, sort) = read_multi_arity thy raw_arities; |
|
620 val sorts = map snd vs; |
|
621 val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos; |
|
622 fun after_qed results = ProofContext.theory |
|
623 ((fold o fold) AxClass.add_arity results); |
|
624 in |
|
625 thy |
|
626 |> ProofContext.init_global |
|
627 |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) arities) |
|
628 end; |
|
629 |
|
630 |
|
631 (** tactics and methods **) |
|
632 |
|
633 fun intro_classes_tac facts st = |
|
634 let |
|
635 val thy = Thm.theory_of_thm st; |
|
636 val classes = Sign.all_classes thy; |
|
637 val class_trivs = map (Thm.class_triv thy) classes; |
|
638 val class_intros = map_filter (try (#intro o AxClass.get_info thy)) classes; |
|
639 val assm_intros = all_assm_intros thy; |
|
640 in |
|
641 Method.intros_tac (class_trivs @ class_intros @ assm_intros) facts st |
|
642 end; |
|
643 |
|
644 fun default_intro_tac ctxt [] = |
|
645 intro_classes_tac [] ORELSE Locale.intro_locales_tac true ctxt [] |
|
646 | default_intro_tac _ _ = no_tac; |
|
647 |
|
648 fun default_tac rules ctxt facts = |
|
649 HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE |
|
650 default_intro_tac ctxt facts; |
|
651 |
|
652 val _ = Context.>> (Context.map_theory |
|
653 (Method.setup (Binding.name "intro_classes") (Scan.succeed (K (METHOD intro_classes_tac))) |
|
654 "back-chain introduction rules of classes" #> |
|
655 Method.setup (Binding.name "default") (Attrib.thms >> (METHOD oo default_tac)) |
|
656 "apply some intro/elim rule")); |
|
657 |
|
658 end; |
|
659 |
|