Advanced indexing #25
Merged
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
govereau
approved these changes
Jan 8, 2025
TensorLib/Common.lean
Outdated
| else .error "index out of bounds" | ||
| else if ind < -dim then .error "index out of bounds" | ||
| else .ok (dim + ind).toNat | ||
| (shape.val.zip index).traverse (fun (dim, ind) => conv dim ind) |
There was a problem hiding this comment.
I think this is why you have batteries, for traverse. Why is this not doable with mapM?
There was a problem hiding this comment.
Ah, mapM is better. Changed throughout the codebase. I usually just reach for traverse since it works in more cases, but here all we have are monads so we are good either way.
(Still use Batteries.Data.List for toChunks in one place, but that's it. We could implement this ourselves if we want to ever drop the Batteries/Aesop dependency).
We implement a common version of advanced indexing, where all arguments are (broadcastable to) int arrays.
seanmcl
force-pushed
the
sm/11-advanced-indexing
branch
from
08860fd to
0faad65
Compare
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.
We implement a common version of advanced indexing, where all arguments are (broadcastable to) int arrays.