[isabelle] Datatype definition can be slow



Hello fellow researchers,

I'm working on a translator from an ML-like language to HOL, and I'm having a
difficulty with translation of inductive datatype definitions.

Datatype definition in Isabelle can be quite slow (at least compared to HOL4)
when the number of constructors goes up (say a few dozen), and time consumption
seems to be super-linear in the number of constructors.  This has a significant
impact on usability since some programs in the source language have very large
datatypes, and it's not always feasible to modify the source programs to make
them friendlier to Isabelle.  Is the poor performance caused by inherent
limitation of the theoretical foundation of the datatype definition package, or
suboptimality of implementation of the package?  Also, does the package provide
a "quick mode" that skips the slow part of the definition process, while
retaining the essential theorems about the datatype being defined?

I once tried to poke into the implementation of the 'datatype' command to find
out what's slowing the thing down, but finally got lost in its sheer
complexity.  The only potential culprit I found is the simplification theorems,
the number of which is quadratic in the number of constructors.

It would be nice to have a datatype definition package without the
aforementioned drawback, but given the size and complexity of current
implementation, improving it seems extremely difficult.

Your thoughts are greatly appreciated.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.