Skip to content

Extend caching in the space engine beyond local context #23483

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

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

Conversation

jchyb
Copy link
Contributor

@jchyb jchyb commented Jul 7, 2025

Previously isSubspace calls would be cached only as part of individual Space object, so when recursing through their ADT contents, we were not able to reuse the previously computed information. Now the cache is shared across the whole space engine run.

Fixes #23317
The compilation of the problematic test now takes around 11 seconds, where previously a much simpler version (with 7 patterns as opposed to 9, with the complexity rising exponentially here) would take 113.75s (with the more complex versions taking too long to measure).
The issue is entirely caused by the reachability check, where the compiler seemed to visibly hang. I noticed that when checking if Prod(List(QuoteMatching.this.TypeMatch((_)), QuoteMatching.this.TypeMatch((_)), QuoteMatching.this.TypeMatch((_)), QuoteMatching.this.TypeMatch((_)), QuoteMatching.this.TypeMatch((_)), QuoteMatching.this.TypeMatch((_)), QuoteMatching.this.TypeMatch((_)), QuoteMatching.this.TypeMatch((_)), QuoteMatching.this.TypeMatch((_)))) is a subspace of Or(List(QuoteMatching.this.TypeMatch((_)), QuoteMatching.this.TypeMatch((_))) | List(QuoteMatching.this.TypeMatch((_))) | Nil) it would keep repeating comparisons of Prod(List(QuoteMatching.this.TypeMatch((_)))) with Or(List(QuoteMatching.this.TypeMatch((_))) | List(QuoteMatching.this.TypeMatch((_)), empty)) etc., inspiring the improvement here.

Previously isSubspace calls would be cached only as part of individual
Space object, so when recursing through their ADT contents, we were not
able to reuse the previously computed information. Now the cache is
shared across the whole space engine run.
@jchyb jchyb force-pushed the fix-space-cache branch from c1acb7e to 01d8ead Compare July 7, 2025 09:29
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.

Pathological (effectively non-terminating) compilation times of quote-matching multiple types
1 participant