feat: LCtxSearch abstraction to search the local context in a single pass #189
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
alexkeizer
force-pushed
the
refactor-state-monads-4
branch
from
c3a952a to
d3cab07
Compare
alexkeizer
force-pushed
the
refactor-state-monads-5
branch
from
9065c01 to
20173f9
Compare
alexkeizer
force-pushed
the
refactor-state-monads-4
branch
from
d3cab07 to
ad949b6
Compare
alexkeizer
force-pushed
the
refactor-state-monads-5
branch
from
6431c4f to
60b484e
Compare
alexkeizer
changed the title
This was referenced Sep 26, 2024
…calContext` to `fromMainContext` to reflect that we now use `withMainContext`
alexkeizer
force-pushed
the
refactor-state-monads-5
branch
from
8beb2b5 to
7e6b84f
Compare
|
This is now rebased and ready for review |
shigoel
approved these changes
Sep 30, 2024
|
@alexkeizer Could you please hit Squash and merge if/when the CI succeeds? |
shigoel
added a commit
that referenced
this pull request
Oct 3, 2024
…mContext` (#200) ### Description: Stacked on #189, we use the more powerful search capabilities to include hypotheses that describe reads from *any* `StateField` into the initial AxEffects. ### Testing: What tests have been run? Did `make all` succeed for your changes? Was conformance testing successful on an Aarch64 machine? Yes ### License: By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license. --------- Co-authored-by: Shilpi Goel <[email protected]>
shigoel
added a commit
that referenced
this pull request
Oct 3, 2024
### Description: Stacked on #200. This uses the `searchLCtx` machinery we built in #189 in `sym_aggregate`'s implementation. For now, this searches for exactly the same kind of expressions as before, but this makes it much easier to expand this set in the next PR. ### Testing: What tests have been run? Did `make all` succeed for your changes? Was conformance testing successful on an Aarch64 machine? yes ### License: By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license. --------- Co-authored-by: Shilpi Goel <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Description:
The main purpose of this definition is to build an abstraction around searching the local context for variables of certain expected types. We currently already do this in multiple places, and building an abstraction around it allows us to deduplicate code, making it more robust, more powerful and more performant (although the performance win is probably negligible, given we don't search the local context that often).
SymContext.fromLocalContext, to now do only two passes over the local context, instead of a separate pass for each variable we look for.fromMainContextto emphasize the fact we search the context of the main (TacticM) goal, not the ambient MetaM local context, andsearchLCtxas well, as an option on search patternsIn future PRs, we'd like to:
AxEffects.fromLocalContextusing this search abstractionexplodeSteptactic, andsym_aggregateTesting:
What tests have been run? Did
make allsucceed for your changes? Wasconformance testing successful on an Aarch64 machine? WIP
License:
By submitting this pull request, I confirm that my contribution is
made under the terms of the Apache 2.0 license.