search

HOL-Theorem-Prover / HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
https://hol-theorem-prover.org
Other
630 stars 142 forks source link

Use an efficient datastructure for substitution #336

Open GallagherCommaJack opened 8 years ago

GallagherCommaJack commented 8 years ago

Currently, functions like match_term return substitutions represented as a list of pairs. Why don't all these functions use maps instead of lists?

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

konrad-slind commented 8 years ago

Historical reasons, mainly. Do you have an application needing a huge number of substitutions?

Konrad.

On Fri, Apr 8, 2016 at 9:46 PM, Jack Gallagher notifications@github.com wrote:

Currently, functions like match_term return substitutions represented as a list of pairs. Why don't all these functions use maps instead of lists?

— You are receiving this because you are subscribed to this thread. Reply to this email directly or view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/336

GallagherCommaJack commented 8 years ago

Probably not - needed to use them when writing match_goal and was curious why they worked that way. Substitution lists coming from that should mostly be short (though if people start writing tactics with it that get run 1000+ times in a loop a more cache friendly structure might make a difference)