[isabelle-dev] [isabelle] rep_datatype and Datatype exception
krauss at in.tum.de
Fri Dec 17 14:30:47 CET 2010
(moving the discussion from isabelle-users to isabelle-dev, since it is
getting into implementation details)
> 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
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,
d) varying parameter names, as also discussed recently. This hasn't
worked for a long time (has it ever?) and does not add additional
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.
More information about the isabelle-dev