LPCIC / elpi

Embeddable Lambda Prolog Interpreter
GNU Lesser General Public License v2.1
283 stars 35 forks source link

Indexing via discrimination tree #205

Closed FissoreD closed 10 months ago

gares commented 10 months ago

Looks much better than this morning. Do the tests pass if we always use the DT index?

FissoreD commented 10 months ago

Most tests pass, but not all yet. I should look deeper to spot the bug. There are some slow down in performance especially for tests like crypt. Even if I think this particular test is not a good use case for indexing with trie, at least in the current implementation where we do not limit the height/depth of the path representing the goal, I suppose lot of time is spent during the creation of the path corresponding to the goal. There are 5 timeout:

TIMEOUT  lyp (type checker for λΥP)                elpi
TIMEOUT  map (defined list) (stdlib map reference)   elpi
TIMEOUT  map (rbtree) (stdlib map)                   elpi
TIMEOUT  mu (standard Prolog benchmark)              elpi
TIMEOUT  set (stdlib set)                            elpi

And three failures:

KO       eta_as (eta expansion of as clause)         elpi
KO       trace-browser-chr (trace generation)        elpi
KO       uvar_keyword (uvar kwd status at the meta level) elpi
gares commented 10 months ago

Indeed, bounding the index to the given depth seems necessary

gares commented 10 months ago

The failures are corner cases, we can look into them together. Bounding the depth of the trie seems more important

gares commented 10 months ago

many changes are nitpicks to reduce the diff