[isabelle-dev] adhoc overloading

[Makarius]

On Fri, 31 May 2013, Christian Sternagel wrote:

> - 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.)

The f is the theory -> theory case, so the good old linearity-of-update 
principle applies.  Your overload_cmd / gen_overload looks non-linear wrt. 
the initial context: you need to refer to the updated one in every step of 
the fold, not the initial one as a "constant" that has been updated 
already.

Generally, you don't have to make everything work on Context.generic. 
Read-only functions like unresolved_overloading_error are fine with a 
plain ctxt : Proof.context, and logical operations like unifiable_with 
using old-style thy : theory.

As a rule of thumb, you have Proof.context most of the time, theory 
rarely, Context.generic and its funny embedding and conversion operations 
only when maintaining generic data in some declaration (or attribute).


> adhoc_overloading
>  foo foo_list
>
> parses "foo" and "foo_list" with "Parse.const" and preprocesses all its 
> arguments by "Proof_Context.read_const ctxt false dummyT", which I thought 
> was the canonical way to check whether a string is a (locally fixed) 
> constant.

As a general principle, you internalize user input only once in the 
outermost command (potentially with user error).  Then you turn it into 
some canonical logical entity (type, term, fact), and apply that in the 
declaration after tranforming it via the morphism you get eventually.

So lets say your "constant name" first looks like a Const or Free. Then in 
the second stage, that internal form is transformed by some term morphism. 
You check if it still looks fine (Const or Free) and do the right thing; 
if not you give up your data without failing (sometimes warnings help, 
sometimes warnings are just noisy).


> For completeness find my current adhoc_overloading.ML attached (but be 
> aware that it is far from finished; it is merely a sandbox in which I 
> play to find out more about the internals of Isabelle).

A few more hints on that file:

   * If you inline that small adhoc_overloding.ML into the theory as ML 
section, it will be just one piece in the end for users to import.

   * Same.function seems to be a let-over from the version by Alex Krauss. 
He had that once in his function package, copied from somewhere else 
(probably old code of mine).  There is no point to do such low-level 
optimizations in the syntax layer.  It is for hardcore kernel operations 
only, to make them hard to understand and look terrific.

   * "variant_tab" as a name is a bit bulky; consider using just "variants".

   * Symtab.delete is strict, it will fail if the element is absent. 
Consider using permissive Symtab.delete_safe by default, or other variants 
like Symtab.remove.


> Sorry for the lengthy email, but it's really hard to find your way 
> through the existing Isabelle/ML API without professional help ;)

Reading the sources alone won't help here -- you need to develop a feeling 
for the kind of music that is played when looking at the score, err 
source.

Maybe you know the end of the film "Amadeus" 
http://en.wikipedia.org/wiki/Amadeus_%28film%29 where you have Mozart 
lying sick in bed and dictating some great music to Salieri.  That guy 
then just produces a few black marks on the paper, but the real thing 
happens in the mind of the composer (for illustration it is also made 
audible for the one who watches the movie). Confutatis maledictis flammis 
acribus addictis, etc.  In the very end of the film Salieri gets insane, 
but that is another story ...


 	Makarius