On Fri, 31 May 2013, Christian Sternagel wrote:
- To set up a command ("adhoc_overloading" in my case) that should also work
inside local contexts I use "Outer_Syntax.local_theory".
This is fine. Basically you make some concrete syntax for this:
syntax_declaration {*
fn phi => fn context => update (transform phi data) context
*}
See also http://www4.in.tum.de/~wenzelm/papers/context-methods.pdf section
3, especially 3.4.
- For data related to the command I use "Generic_Data" (since it should be
available in top-level theories as well as local contexts).
Yes, and for any update operation you need to work uniformly with
Context.generic, not attempt any special things (like updating the
background theory of a Proof.context!).
- Investigating "notation" a bit (but not understanding the implementation
details ;)), I suspect that "Local_Theory.declaration" is used to make
changes in my "Generic_Data" persistent. What is the purpose of the "{syntax:
bool, pervasive: bool}" argument of "Local_Theory.declaration".
'declaration' is the general abstract non-sense of the "local everything"
approach; section 3.4 also explains that 'declare' happens to be
equivalent due to the flexibility of attributes -- at least at the level
of abstraction of the paper.
The additional flags "syntax" and "pervasive" are only available to the
full Local_Theory.declaration and actual Isar commands built on top of
that, not in the "declare attribute" form.
"syntax" gives it a special status in the bootstrap process of locale
expressions. So you better enable that flag here, like 'notation' does.
"pervasive" means it would write through all layers of the Haftmann-Wenzel
Sandwich (which is now a Neapolitan wafer -- as an Austrian you should
know what it is). This is better disabled for syntax things.
- "Local_Theory.declaration" expects a "declaration" as argument, which
abbreviates the type "morphism -> Context.generic -> Context.generic". For
the time being I just ignore "morphism" (of course I will have to understand
and incorporate it at some point).
Ignoring the morphism means it only works in the global theory context,
where it is the identify. The "local everything" approach is about
getting the handling the morphism right wrt. your update function on the
tool-specific data, when it is applied to a particular target context.
- So far so good. Everything compiles fine. When I actually use my newly
defined command, I get the error "Stale theory encountered". So obviously I'm
doing something wrong in the above "f" (if I replace "f" by "I" the error
disappears, but of course then I can also not make changes in my
"Generic_Data" persistent.)
I can't say on the spot what is wrong, apart from some oddities. Why have
Context.mapping with Context.theory_map/proof_map in the first place? You
should be able to work on Context.generic directly to update your generic
data.
Moreover, you need to get naming conventions right: lthy : local_theory
refers to the full Haftmann-Wenzel Sandwich, but as you apply updates to
particular target contexts it is no longer that. So it should be just
ctxt = Context.proof_of context for read_const.
More hints when I've studied the rest of the examples setup ...
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
