[isabelle-dev] [isabelle] rep_datatype and Datatype exception

[Alexander Krauss]

(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