[isabelle-dev] adhoc overloading

[Makarius]

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