[isabelle-dev] priority queues

[Steffen Juilf Smolka]

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

I'm working on Sledgehammer with Jasmin Blanchette, so in a way this is related to the repository version of Isabelle. I'm not sure if that makes a difference, though…

> 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

Thanks. Jasmin already pointed me to tables. For my application, being able to use min_key as well as max_key is nice, a feature the heap structure does not seem to offer.

Steffen


On 27.10.2012, at 16:58, Makarius <makarius at sketis.net> wrote:

> On Wed, 24 Oct 2012, Lukas Bulwahn wrote:
> 
>> I think priority queues are roughly ordered lists (the priority is the ordering). So, you could have a look at Pure/General/ord_list.ML
> 
> The main virtue of Ord_List is that insert and merge are of the same complexity: linear.  This is important in special applications like maintaining the hyps field of a thm efficiently, but in most other applications the linearity of insert is a performance trap.  The balanced tree structure underlying module Table works better in general.
> 
> 
> 	Makarius

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20121027/583b3610/attachment-0002.html>