[isabelle-dev] adhoc overloading
makarius at sketis.net
Fri May 31 21:48:47 CEST 2013
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
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).
> 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)
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
> 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
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 ...
More information about the isabelle-dev