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

Prune broadcast functions based on their triggers #1175

Open
wants to merge 1 commit into
base: main
Choose a base branch
from

Conversation

Chris-Hawblitzel
Copy link
Collaborator

The old way of pruning broadcast functions was to keep all the broadcasts from a module if the module itself was reachable. This pull request introduces a more precise pruning policy that mostly replaces the old policy. In the new policy, a broadcast function is kept (not pruned) if any of its triggers are reachable. (If none of its triggers are reachable, then there would be no way to trigger the broadcast.)

There are a few exceptional cases that don't fall under this policy: arithmetic triggers, extensional equality triggers, and height triggers. For these, the old module-based policy is used. In the future, we could address these with other policies, such as type-based pruning.

The trigger-based policy relies on broadcast functions having explicit triggers. Therefore, this pull request adds a warning for any broadcast function that does not provide explicit triggers.

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.

None yet

1 participant