On Thu, 10 Nov 2011, Andreas Schropp wrote:
it has come to my attention that attributes are called with a theory, a
proof context and a local theory in this succession. Is this
transforming the input lthy onion from inside out?
I prefer to call it sandwich -- I don't like onions so much :-)
Details of when declarations are actually materialized and applied to some
context are up to local theory target implementations, and other
mechanisms like interpretation. But yes, things are usually done from
bottom to top, inside out. (Roughly in "foundational order".)
The implementation manual states that I have to treat all of them
uniformly. This means that the attribute transformation on a lthy would
not result in an update of the target context but of the auxilliary
context instead. Is this correct and is the target guaranteed to be
transformed in the same way beforehand?
Yes. The update function provided by the user of local theory
declarations should operate directly on the surface context as given,
either Context.Theory or Context.Proof. You cannot even count that it
will be again a local theory in the application, e.g. consider
'interpretation' or 'interpret'.
The target is usually updated before the auxiliary context, but this
should normally not matter, since the lookup should use the very same
surface context.
Note that in official Isabelle2011-1 there is still some confusion here in
Local_Theory.declaration, because it would omit the aux. context. I have
clarified that after the release, with some years delay as usual.
Also, does this mean we store the information resulting
from attributes 3 times, namely in theories, contexts and
local theories, potentially without any sharing?
Normally there is little to share, because the 3 values are different.
The morphism that is applied to the data first will change it according to
the context.
Moreover, in practice it is not really 3 times, since regular declarations
are not "pervasive", i.e. not applied to the background theory, and the
auxiliary context does not persist in the long term -- it merely serves
for "drafting" specifications locally.
If in the process of a local theory transformation I want to store
information to be looked up later, but not escaping the scope of the
target, where should I store it? In the auxilliary context or the target
context?
Local_Theory.target in Isabelle/11d9c2768729 has explicit option
"pervasive" to say if it should go into the background theory. Moreover,
you have can often get clues from the result after applying the morphism
if you still want to make the update. E.g. Proof_Context.target_notation
will give up after the term to be annotated has changed substantially.
Anyway, these are just some generalities. What is your concrete
application?
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
