(moving the discussion from isabelle-users to isabelle-dev, since it is
getting into implementation details)
Makarius wrote:
The situation of the datatype package is twofold:
(1) It is very complex already.
(2) It still needs to be localized.
Practically this means that I will have to spend quite some time with it
myself, to upgrade it to the current system infrastructure. I hope that
this is still feasible, so that this key component of Isabelle/HOL is
not stuck in the past -- due to a load of features that is too heavy to
lift it again.
I am also a bit worried about the complexity in there. I think, some of
it could be reduced by moving out stuff that is unrelated to the core
construction:
a) sort-constraints: They can be provided on the user level only and
need not be pushed through the whole thing.
b) case combinators (and syntax for them, including the syntax for
nested cases): This could be moved into a "datatype interpretation" like
size functions etc. Probably the same for split rules.
c) alt_names (discussed on a recent thread, but still unresolved,
probably obsolete)
http://thread.gmane.org/gmane.science.mathematics.logic.isabelle.devel/1131
d) varying parameter names, as also discussed recently. This hasn't
worked for a long time (has it ever?) and does not add additional
generality.
http://thread.gmane.org/gmane.science.mathematics.logic.isabelle.devel/197
It may be helpful to separate/eliminate these things before attempting a
localization. Of course, the main complication remains: The intricate
unrolling of nested types.
In principle, I am willing to help with this, but not before the
deadlines in February.
Alex
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
