You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
So, currently with the SLG solver, answers are stored by a goal + environment. Thus, when an we have an otherwise identical goal with different environments, we can do duplicate work. I had a couple ideas that could help this.
First, it would be relatively easy to have two tables: one for answers where we didn't need the environment, and one where we did. This is kind of like rustc's "global cache".
Another alternative idea though would be to encode the requirements from the environment as delayed subgoals. (Not exactly sure how this would look like implentation-wise)
In either case, I think we need to be careful where we might have an "environment-agnostic" answer, but then clauses in the environment can cause ambiguity.
The text was updated successfully, but these errors were encountered:
So, currently with the SLG solver, answers are stored by a goal + environment. Thus, when an we have an otherwise identical goal with different environments, we can do duplicate work. I had a couple ideas that could help this.
First, it would be relatively easy to have two tables: one for answers where we didn't need the environment, and one where we did. This is kind of like rustc's "global cache".
Another alternative idea though would be to encode the requirements from the environment as delayed subgoals. (Not exactly sure how this would look like implentation-wise)
In either case, I think we need to be careful where we might have an "environment-agnostic" answer, but then clauses in the environment can cause ambiguity.
The text was updated successfully, but these errors were encountered: