Basic indexing #21
Basic indexing #21
Conversation
seanmcl
force-pushed
the
sm/06-tensor
branch
2 times, most recently
from
5a52db1 to
daff58a
Compare
| -- (np.int64(1), array([1])) | ||
| -- | ||
| -- x[0].shape, x[0:1:1].shape | ||
| -- ((), (1,)) |
There was a problem hiding this comment.
Do you mean same "dimension" not "shape"?
I think the shape of x is (6,), which isn't the same as (1,)
TensorLib/Index.lean
Outdated
| loop items (dim :: shape) | ||
| else -- there are fewer items than the shape | ||
| loop (.ellipsis :: items) shape | ||
| | _, _ => .error "impossible" |
There was a problem hiding this comment.
I was confused here for a second, until I noticed the length comparison at the start.
Is this case checking the same thing as the line on 63? (maybe a comment would be helpful)
There was a problem hiding this comment.
Nice comment. I lifted the error case to the top so it's more obvious
| [], shape => .ok (shapeToSliceIters shape, shape)
| _, [] => .error "impossible" -- We checked above that there are at least as many dims as items
| let basic := match basic with | ||
| | none => { iter with done := true } -- All slice iterators are maxxed out in this case. Should we check this? | ||
| | some basic => { iter with basic } | ||
| some (ns, basic) |
There was a problem hiding this comment.
The algorithm here has a lot of finicky details, but it is still pretty easy to read.
Nice job!
TensorLib/Index.lean
Outdated
| iter := iter' | ||
| match <- f ns res with | ||
| | .yield k | ||
| | .done k => res := k |
There was a problem hiding this comment.
May have fixed already, the issue with break or return mentioned in prior reviews.
There was a problem hiding this comment.
Fixed and added similar tests.
| dtype := arr.dtype, | ||
| shape := newShape, | ||
| data | ||
| } |
There was a problem hiding this comment.
Cool, I wish I had read this function first. :)
There was a problem hiding this comment.
Ha. Yes I kind of miss out-of-order definitions for this reason. Doing lots of gritty work so the top level stuff is pretty.
"Basic" indexing means indexing with a constant or slice on all the dimensions. (Advanced indexing is for things like indexing by other arrays).
https://numpy.org/doc/stable/user/basics.indexing.html