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.
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.