Re: [isabelle] Named_Target.reinit



This is a good opportunity to describe the rationale behind the local
theory / target / named target matter in more detail »as it is by now«.

The fundamental ideas have been presented in »Local Theory
Specifications in Isabelle/Isar« by Haftmann/Wenzel; as usual, the
implementation is a little bit more involved, and also some extensions
have appeared since then, notably nested target contexts and confined
interpretation.

What is a *local theory*? The extension of a proof context with an
abstract signature to allow definitional extensions (most prominently,
*define* and *note* – the actual interface can be found as *type
operations* in Pure/Isar/local_theory.ML).

A *target* is a particular implementation of the local theory signature.

The picture is a little complicated by the possibility to stack
arbitrary many auxiliary contexts on top a target (»context fixes …
assumes … begin … end« in Isar). However, these merely add variables and
assumptions in a canonical way; the target at the bottom of this stack,
the *bottom target,* is not really affected by this. So, if we speak
about target, we most times refer to a particular bottom target with a
(possibly empty) stack auf axuiliary contexts on top of it.

Conceptually, there are two main targets: the theory target and the
locale target, which can be seen as the most generic targets possible.

A slight variant of the locale target is the class target, which adds a
canonical interpretation on the theory level. An important class of
targets are *theory-like targets*, which behave almost like the theory
target, but feature slight modifications like additional syntax and a
consistency check before leaving the local theory. The overloading and
instantiation targets are prominent examples.

Concerning the concept of *named target. *Each type class and locale in
a theory can be referred to by a string s; if we identify the empty
string with the theory itself, Named_Target.init s opens a local theory
for the theory / locale / class with the appropriate theory / locale /
class target. This »selection by name« manifests in the Isar toplevel
also (»context s begin … end«), and hence the prominent status of these
named targets in the system infrastructure.

An important consequence of the abstract nature of local theories is
that only target implementations are allowed to break their abstraction;
client code is expected to operate on any kind of local theory
regardless of the particular (bottom) target. In the Isabelle
distribution, there are currently (Isabelle2014-RC0) four spots which
are candidates for a violation of this principle:

./Pure/Isar/class_declaration.ML:349:    val proto_sub = case
Named_Target.class_of lthy of
./Pure/Isar/expression.ML:925:  if Named_Target.is_theory lthy
./Pure/Isar/expression.ML:932:      if Named_Target.is_theory lthy
./Tools/quickcheck.ML:365:    val some_locale =
Named_Target.bottom_locale_of lthy;

The first one is sane since the class target is allowed to break its own
abstraction. Number two and three are similar. The last one is indeed a
little bit odd, but since its is some kind of diagnostic device, it is
maybe ok.

Generally, user space tools should refrain from using those
abstraction-breaking query operations in Named_Target. The same holds
for the Named_Target.switch (or its earlier predecessor,
Named_Target.reinit) which is a device to master the following situation
with an ad-hoc local theory switch which is currently allowed in Isar:

context s
begin

…

definition (in t):
  …

…

end

If client code implements its own target, in most cases it will be a
theory-like target. There are two possibilites to approach it:

a) Something like
    |> Local_Theory.init naming
       {define = Generic_Target.define …,
        notes = Generic_Target.notes Generic_Target.theory_notes,
        abbrev = Generic_Target.abbrev Generic_Target.theory_abbrev,
        declaration = K Generic_Target.theory_declaration,
        subscription = Generic_Target.theory_registration,
        pretty = …,
        exit = … #> Local_Theory.target_of #> Sign.change_end_local}
(cf. Pure/Isar/class.ML) See how Generic_Target provides everything
needed to plug together implementations of local theory operations on
the spot.

b) If the target only adds a check or something similar before leaving
the local theory, it can also be setup using Named_Target.theory_like_init.

Hope this helps,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.