[isabelle] A generic machinery for syntactic abbreviations?

Dear all,

recently, I stumbled over three related but separately implemented
abbreviation-like mechanisms:

* abbreviations;
* the Âuser space type system for class operations which parses global
f as local ones and prints them the other way round;
* ad-hoc overloading from ~~/src/Tools/Adhoc_Overloading.thy.

All three accomplish a similar thing, the systematic (un)folding of
syntactic abbreviations according to syntactic equations "(c :: T) ==
rhs". All three are delicate, since there is no logic foundation to
guide them and details are abysmal. One of the details is that, during
reading of abbreviation rhses, abbreviations on the rhses themselves
must not be unfolded. Hence, they somehow participate in the same game;
however, all three have different implementations.

My impression is that only a unified mechanism can work out the subtle
failures occasionally but stubbornly observed. It would operate somehow
like that:
* Generalize the existing abbreviations to a machinery which allows
registration of syntactic abbreviation equations "(c :: T) == rhs" â
whether as bare term or ML function, has to be worked out.
* The class target and ad-hoc overloading would simply reuse that
abbreviation machinery and stop tinkering with self-baken solutions.

Surely still some time to be invested there, but maybe essential to
survive in the middle run.

Does this sound reasonable?


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.