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

Experiment: adding an [nb_occurs] function. #32

Closed
wants to merge 1 commit into from
Closed

Conversation

rlepigre
Copy link
Owner

@rlepigre rlepigre commented Apr 4, 2023

This is one possible way to address #29, but it is not clear this is what we want since it might impact performance. In particular, we introduce an extra pointer indirection since we cannot unbox the anyvar type anymore.

@craff
Copy link
Collaborator

craff commented Apr 5, 2023

If also does count very well in all cases: if you define

let self_app : term box -> term box =
  fun t -> box_apply (fun t -> App(t,t)) t

If will count variable in t only once. It is not clear what the user wants in such a case.

@rlepigre
Copy link
Owner Author

rlepigre commented Apr 5, 2023

That's a good point, I guess this approach can only work if the argument of functions passed to box_apply and friends is always used linearly (which I think is pretty much always the case (?)).

In any case, this PR is really just an experiment, it is really not clear to me whether we want/need this.

@craff
Copy link
Collaborator

craff commented Apr 30, 2024

I can review the PR ... or we drop it ?

@rlepigre
Copy link
Owner Author

We should probably drop it at this point, given the problem you highlighted.

@rlepigre rlepigre closed this Apr 30, 2024
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

Successfully merging this pull request may close these issues.

2 participants