krauss at in.tum.de
Tue Jan 20 22:49:19 CET 2009
Brian Huffman wrote:
> I, for one, am rather alarmed at the hurdles that Amine was forced to
> overcome to do a simple merge of two theories.
> I think that the automatic class-instantiations should be disabled
> immediately, and replaced with a new top-level command so that these
> instantiations can be done explicitly, and individually.
In fact, "typerep" is not the only class that is instantiated
automatically. Another one is "size", which is also of a technical
nature. But it never posed problems, I think, because it is installed
early enough that everybody inherits from it.
I think that automatic class instantiations are acceptable provided that
a) the class is for "internal" use of some tools and manual
instantiation is discouraged, and b) The mechanism is installed early
enough to avoid the merge issue.
IMO the options are
1) Make the whole Typerep theory optional, to be loaded together with
the Imperative HOL theories.
2) Typerep provides a top-level command for generating the instantiations.
3) Move Typerep up the hierarchy, such that it is always present and
there are no merge problems.
Note that 1 and 2 do not actually solve the problem but only limit it to
theories that use Imperative HOL (in 1) or the top-level command (in 2).
I think I nevertheless prefer option 1, since Typerep is really a
The cleanest, but also the hardest solution would be to make class
instances "applicative" instead of "generative" (I may be streching the
terms a bit far here), such that equal class instances do *not* collide
at a later merge.
More information about the isabelle-dev