[isabelle-dev] priority queues

[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.


To avoid further complication, here are some hints as if this would be 
isabelle-users (so I refer to the latest official release):

   http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2012/src/Pure/General/heap.ML
   http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2012/src/Pure/General/table.ML
   http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2012/src/Pure/General/graph.ML

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

http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2012/src/Pure/Concurrent/task_queue.ML#l147
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2012/src/Pure/Concurrent/task_queue.ML#l324


 	Makarius