[isabelle-dev] priority queues
Steffen Juilf Smolka
steffen.smolka at in.tum.de
Sat Oct 27 20:54:01 CEST 2012
> 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):
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.
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.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the isabelle-dev