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

Use GADT to avoid closures #186

Merged
merged 1 commit into from
Feb 25, 2024
Merged

Use GADT to avoid closures #186

merged 1 commit into from
Feb 25, 2024

Conversation

polytypic
Copy link
Contributor

@polytypic polytypic commented Jan 25, 2024

This changes the internal update operation to use a GADT to indicate which kind of operation to perform. This helps to avoid allocations for certain operations. The inline attribute is also removed from the internal update function. This reduces code size significantly. The periodic validation is also restricted to happen only on accesses of locations that have been accessed previously.

@polytypic polytypic changed the title Use gadt to avoid closures Use GADT to avoid closures Jan 25, 2024
@polytypic polytypic force-pushed the use-gadt-to-avoid-closures branch 3 times, most recently from a35efe3 to 4a7d8a6 Compare January 25, 2024 16:35
@polytypic polytypic force-pushed the use-gadt-to-avoid-closures branch 5 times, most recently from d320536 to 0f7a159 Compare February 25, 2024 13:18
@polytypic polytypic marked this pull request as ready for review February 25, 2024 15:47
@polytypic polytypic force-pushed the use-gadt-to-avoid-closures branch 15 times, most recently from 5cfa392 to 008daba Compare February 25, 2024 19:56
@polytypic polytypic merged commit cd85659 into main Feb 25, 2024
4 checks passed
@polytypic polytypic deleted the use-gadt-to-avoid-closures branch February 25, 2024 20:48
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.

1 participant