Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

pool optim, toward only head normal term added to the pool #26

Open
craff opened this issue Nov 21, 2017 · 0 comments
Open

pool optim, toward only head normal term added to the pool #26

craff opened this issue Nov 21, 2017 · 0 comments

Comments

@craff
Copy link
Collaborator

craff commented Nov 21, 2017

insert_t_node should use a stack to avoid creating node for partially applied function.

For instance, adding [add n p] to the pool also adds [add n] which is a lambda, hence trigger a cloture construction.

This cost is dominating "equiv" when computation are really needed, with
probably a factor much greater that 2 (10 ?) to gain.

@craff craff changed the title pool optim pool optim, toward only head normal term added to the pool Nov 22, 2017
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant