167 |
167 |
168 fun specification_of thy = #spec o the_locale thy; |
168 fun specification_of thy = #spec o the_locale thy; |
169 |
169 |
170 fun dependencies_of thy name = the_locale thy name |> |
170 fun dependencies_of thy name = the_locale thy name |> |
171 #dependencies |> map fst; |
171 #dependencies |> map fst; |
|
172 |
|
173 (* Print instance and qualifiers *) |
|
174 |
|
175 fun pretty_reg thy (name, morph) = |
|
176 let |
|
177 val name' = extern thy name; |
|
178 val ctxt = ProofContext.init_global thy; |
|
179 fun prt_qual (qual, mand) = Pretty.str (qual ^ (if mand then "!" else "?")); |
|
180 fun prt_quals qs = Pretty.separate "." (map prt_qual qs) |> Pretty.block; |
|
181 val prt_term = Pretty.quote o Syntax.pretty_term ctxt; |
|
182 fun prt_term' t = if !show_types |
|
183 then Pretty.block [prt_term t, Pretty.brk 1, Pretty.str "::", |
|
184 Pretty.brk 1, (Pretty.quote o Syntax.pretty_typ ctxt) (type_of t)] |
|
185 else prt_term t; |
|
186 fun prt_inst ts = |
|
187 Pretty.block (Pretty.breaks (Pretty.str name' :: map prt_term' ts)); |
|
188 |
|
189 val qs = Binding.name "x" |> Morphism.binding morph |> Binding.prefix_of; |
|
190 val ts = instance_of thy name morph; |
|
191 in |
|
192 case qs of |
|
193 [] => prt_inst ts |
|
194 | qs => Pretty.block [prt_quals qs, Pretty.brk 1, Pretty.str ":", |
|
195 Pretty.brk 1, prt_inst ts] |
|
196 end; |
172 |
197 |
173 |
198 |
174 (*** Activate context elements of locale ***) |
199 (*** Activate context elements of locale ***) |
175 |
200 |
176 (** Identifiers: activated locales in theory or proof context **) |
201 (** Identifiers: activated locales in theory or proof context **) |
346 (* table of mixin lists, per list mixins in reverse order of declaration; |
371 (* table of mixin lists, per list mixins in reverse order of declaration; |
347 lists indexed by registration serial, |
372 lists indexed by registration serial, |
348 entries for empty lists may be omitted *) |
373 entries for empty lists may be omitted *) |
349 val empty = (Idtab.empty, Inttab.empty); |
374 val empty = (Idtab.empty, Inttab.empty); |
350 val extend = I; |
375 val extend = I; |
351 fun merge ((r1, m1), (r2, m2)) : T = |
376 fun merge ((reg1, mix1), (reg2, mix2)) : T = |
352 (Idtab.join (K (fst)) (r1, r2), (* pick left registration, FIXME? *) |
377 (Idtab.join (fn id => fn (r1 as (_, s1), r2 as (_, s2)) => |
353 Inttab.join (K (Library.merge (eq_snd op =))) (m1, m2)); |
378 if s1 = s2 then raise Idtab.SAME else raise Idtab.DUP id) (reg1, reg2), |
|
379 Inttab.join (K (Library.merge (eq_snd op =))) (mix1, mix2)) |
|
380 handle Idtab.DUP id => |
|
381 (* distinct interpretations with same base: merge their mixins *) |
|
382 let |
|
383 val (_, s1) = Idtab.lookup reg1 id |> the; |
|
384 val (morph2, s2) = Idtab.lookup reg2 id |> the; |
|
385 val reg2' = Idtab.update (id, (morph2, s1)) reg2; |
|
386 val mix2' = case Inttab.lookup mix2 s2 of |
|
387 NONE => mix2 | |
|
388 SOME mxs => Inttab.delete s2 mix2 |> Inttab.update_new (s1, mxs); |
|
389 val _ = warning "Removed duplicate interpretation after retrieving its mixins."; |
|
390 (* FIXME print interpretations, |
|
391 which is not straightforward without theory context *) |
|
392 in merge ((reg1, mix1), (reg2', mix2')) end; |
354 (* FIXME consolidate with dependencies, consider one data slot only *) |
393 (* FIXME consolidate with dependencies, consider one data slot only *) |
355 ); |
394 ); |
356 |
395 |
357 |
396 |
358 (* Primitive operations *) |
397 (* Primitive operations *) |
418 val activate = activate_notes' Element.init (Element.transfer_morphism o Context.theory_of) thy export; |
457 val activate = activate_notes' Element.init (Element.transfer_morphism o Context.theory_of) thy export; |
419 in roundup thy activate export dep (get_idents context, context) |-> put_idents end; |
458 in roundup thy activate export dep (get_idents context, context) |-> put_idents end; |
420 |
459 |
421 |
460 |
422 (* Diagnostic *) |
461 (* Diagnostic *) |
423 |
|
424 fun pretty_reg thy (name, morph) = |
|
425 let |
|
426 val name' = extern thy name; |
|
427 val ctxt = ProofContext.init_global thy; |
|
428 fun prt_qual (qual, mand) = Pretty.str (qual ^ (if mand then "!" else "?")); |
|
429 fun prt_quals qs = Pretty.separate "." (map prt_qual qs) |> Pretty.block; |
|
430 val prt_term = Pretty.quote o Syntax.pretty_term ctxt; |
|
431 fun prt_term' t = if !show_types |
|
432 then Pretty.block [prt_term t, Pretty.brk 1, Pretty.str "::", |
|
433 Pretty.brk 1, (Pretty.quote o Syntax.pretty_typ ctxt) (type_of t)] |
|
434 else prt_term t; |
|
435 fun prt_inst ts = |
|
436 Pretty.block (Pretty.breaks (Pretty.str name' :: map prt_term' ts)); |
|
437 |
|
438 val qs = Binding.name "x" |> Morphism.binding morph |> Binding.prefix_of; |
|
439 val ts = instance_of thy name morph; |
|
440 in |
|
441 case qs of |
|
442 [] => prt_inst ts |
|
443 | qs => Pretty.block [prt_quals qs, Pretty.brk 1, Pretty.str ":", |
|
444 Pretty.brk 1, prt_inst ts] |
|
445 end; |
|
446 |
462 |
447 fun print_registrations thy raw_name = |
463 fun print_registrations thy raw_name = |
448 (case these_registrations thy (intern thy raw_name) of |
464 (case these_registrations thy (intern thy raw_name) of |
449 [] => Pretty.str ("no interpretations") |
465 [] => Pretty.str ("no interpretations") |
450 | regs => Pretty.big_list "interpretations:" (map (pretty_reg thy) (rev regs))) |
466 | regs => Pretty.big_list "interpretations:" (map (pretty_reg thy) (rev regs))) |