[isabelle-dev] priority queues
nipkow at in.tum.de
Sat Oct 27 18:06:56 CEST 2012
Am 27/10/2012 16:55, schrieb Makarius:
> On Wed, 24 Oct 2012, Steffen Juilf Smolka wrote:
>> is there an implementation of priority queues in the isabelle library?
> This is off-topic for this mailing list, which is for things happening around
> the Isabelle development process. Unless you refer to a particularly emerging
> module in some inter-release repository version --
> lets say you are build some add-ons as very early adopter -- everything
> concerning Isabelle/ML programming can be discussed on the main isabelle-users
> mailing list.
Steffen is a sledgehammer code developer with Jasmin and this question is not
appropriate for isabelle-users.
> To avoid further complication, here are some hints as if this would be
> isabelle-users (so I refer to the latest official release):
> The (rarely used) Heap module gives you direct access to the minimum element of
> an ordered collection, which is maintained efficiently.
> The Table module is *the* workhorse for efficient organisation of ordered values
> (sets, maps etc.). Its derivative Graph is equally popular: it introduces
> additional dependencies over a table, often acyclic ones, but cyclic graphs are
> also supported.
> For example, in the Task_Queue implementation that underlies the Future library
> in Isabelle/ML, a graph with a suitable order on tasks is used as a priority
> queue with dependencies. You then take out the smallest element that does not
> have any dependencies. See also
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev