[isabelle-dev] priority queues

[Tobias Nipkow]

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.

Tobias

> 
> 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
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev