[isabelle-dev] performance regression of typedef command

[Makarius]

On Fri, 26 Mar 2010, Brian Huffman wrote:

> In Isabelle 2009, the typedef takes about 5 hundredths of a second on
> my machine, with another few hundredths for the "by simp" part.
>
> In the current development version, with the new "local theory"
> typedef package, the typedef takes nearly *half a second*.

Depends what you mean by current development version.  In cef3c78ace0a 
it's not so slow anymore due to some basic tuning of type signature merge 
operations, which have been historically only used at the beginning of a 
theory but now show up whenever types are declared within a local context.


> In exchange for the extreme slowness, we get the ability to use typedef 
> commands inside locales.

There is much more to the local theory infrastructure than making things 
work in a locale, which is just one example of a "local theory target".

Several years ago we've had a big mess of certain attempts to implement 
structured specifications, i.e. specifications that depend local context 
information, or build up local contexts.  The local theory concept has 
successfully integrated all this and provides a general high level 
infrastructure both for local packages (definition, theorem, inductive, 
function, primrec, etc.), and for local theory targets (locale, class, 
instantiation, overloading, global theory etc.).


Here are just two current examples what you gain from that.

(1) Sane specification primitives for implementing packages.  You say 
Local_Theory.define x t and get a literal x == t (for a locally fixed 
hypothetical x).  The infrastructure takes care of the rest, since version 
09e238561460 the dreaded "hidden polymorphism" is treated here as well, 
i.e. the pathological situation where a definition c == t has more type
variables in t than in the type of t.

In your TPHOLs 2005 paper you've stumbled over that and had to use typedef 
(open) as a workaround.  I've later added some strange workarounds to 
typedef to amend that, but it is a bit much to ask this of every package 
implementation.  See here eafaa9990712 how this cruft disappears at last.

Many other packages were suffering from the same problem, and you can 
hardly call it a bug of these packages, but a misunderstanding about the 
proper specification primitives.  E.g. here is an example workaround 
http://isabelle.in.tum.de/repos/isabelle/annotate/2623b23e41fc/src/HOL/Quickcheck.thy#l148 
to make the function package work with hidden polymorphism of an internal 
inductive definition -- the final result does not even have these extra 
type variables.  (This one is still not updated, the parasitic 'a itself 
argument is no longer necessary.)

In fact, it was Alex who pointed out that Local_Theory.define is the 
proper place to hide such oddities from the user and package implementor, 
and concenrate on the application logic instead.


(2) Control over consequences within the application context, especially 
name spaces and concrete syntax.  Since the idea of interpreting local 
theory content in other situations has been part of the game from the very 
beginning, it opens the possibility for mechanisms to control name space 
scopes and availability of concrete syntax in certain ranges of the formal 
theory text.  You can even do it right now in this simplistic way:

locale loc
begin

typedef 'a foo  ("** _ **") = "{undefined :: 'a}" by simp

typ "nat foo"
typ "** nat **"

end

typ "nat loc.foo"

interpretation loc .

typ "nat foo"
typ "** nat **"


Here the mechanisms to delimit local ranges need some further 
refinements, but you should get the idea even now.

Moreover, one can think of turning the present global theory target into 
something that is closer to locale infrastructure, i.e. keep the name 
space accesses and syntax separate from the other content.  Then we are 
back to the recent discussion about controling scopes and syntax ... and 
it's still not easy to do with lots of historical specification packages 
still around.

Now that typedecl/typedef are localized at last, the other packages that 
depend on them can follow.


 	Makarius