Email Gateway (Aug 22 2022 at 10:25): Email Gateway (Aug 22 2022 at 10:25):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear all,
recently, I stumbled over three related but separately implemented
abbreviation-like mechanisms:
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?
Florian
signature.asc
Last updated: Apr 25 2024 at 01:08 UTC