Add Common.lean #15
Add Common.lean #15
Conversation
seanmcl
force-pushed
the
sm/01-common
branch
2 times, most recently
from
0e17abc to
e365e9d
Compare
TensorLib/Common.lean
Outdated
| def natDivCeil (num denom : Nat) : Nat := | ||
| let div := num / denom | ||
| let mod := Nat.mod num denom | ||
| if mod != 0 then div + 1 else div |
There was a problem hiding this comment.
Is this better (num + denom - 1) / denom ? (one division, no if)
There was a problem hiding this comment.
Yes. Tried to prove in Lean and Dafny that they're the same. Proof automation fails, and I gave up after not finding many lemmas via Loogle. Some dafny folks pointed out it's actually hard in Dafny, requiring triggers. Was able to prove for any fixed either numerator or denominator that it's equivalent, but not for both being free.
| --! The number of elements in a tensor. All that's needed is the shape for this calculation. | ||
| -- TODO: cache this? Not sure how this works in Lean. Do we need to make Shape a struct and | ||
| -- put it in the record? | ||
|
|
There was a problem hiding this comment.
Maybe you can use computed fields?
https://leanprover-community.github.io/con-nf/doc/Lean/Elab/ComputedFields.html
There was a problem hiding this comment.
Made it a structure, which gives this flexibility later. I was uncomfortable having such a prominent concept being an abbrev anyway.
TensorLib/Common.lean
Outdated
| so this is just the default case. | ||
| -/ | ||
| def unitStrides (s : Shape) (dataOrder : DataOrder) : Strides := match dataOrder with | ||
| | DataOrder.Fortran => [] -- Unimplemented |
There was a problem hiding this comment.
Should we just not support Fortran order and give an error when loading the file?
There was a problem hiding this comment.
Dropped DataOrder after some discussion. The Npy.lean file will have instructions for turning a fortran-order .npy file to C-order so we can manage it.
TensorLib/Common.lean
Outdated
| let (_, idx) := strides.foldl foldFn (n, []) | ||
| idx.reverse | ||
|
|
||
| -- One-based strides. Note there is a Mathlib conversion from `List Nat` to `List Int` here |
There was a problem hiding this comment.
I don't understand this comment?
There was a problem hiding this comment.
Vestigial. Removed, thanks.
TensorLib/Common.lean
Outdated
| #guard dimIndexToOffset [3, 1] [1, 1] == 4 | ||
|
|
||
| -- In general you should use DimsIter instead of this, which is equivalent | ||
| -- to `DimIter.toList` but I left it here because it is obviously terminating. |
There was a problem hiding this comment.
DimsIter.toList (not DimIter)
| match <- f dims res with | ||
| | .yield k | ||
| | .done k => res := k | ||
| return res |
There was a problem hiding this comment.
Why does the done case not exit the loop?
What happens if you use break or return inside of one of these for loops?
There was a problem hiding this comment.
Oof, nice find. I just didn't grok the signature. I only used it on well-behaved iterators like lists without break or return. Fixed and added tests.
| let x4 := x.get (Fin.mk _ H4) | ||
| let x5 := x.get (Fin.mk _ H5) | ||
| let x6 := x.get (Fin.mk _ H6) | ||
| let x7 := x.get (Fin.mk _ H7) |
There was a problem hiding this comment.
Just curious, how does the Fin get converted to the inputs for get?
Seems like you need the components of the Fin as separate arguments to get.
There was a problem hiding this comment.
For ByteArray, the argument is a Fin.
@[extern "lean_byte_array_fget"]
def get : (a : @& ByteArray) → (@& Fin a.size) → UInt8
There was a problem hiding this comment.
Ah, I think it is just a version thing. Int 4.15 it is:
@[extern "lean_byte_array_fget"]
def get : (a : @& ByteArray) → (i : @& Nat) → (h : i < a.size := by get_elem_tactic) → UInt8
There was a problem hiding this comment.
Ah nice, that is better. Will update when I can update to 4.15 without Aesop crashing. If this seems like it will take time to be fixed, I can go through and copy/paste the aesop tactic scripts. Maybe should do that anyway.
`Common` is a module with a grabbag of functionality required by later files.
Commonis a module with a grabbag of functionality required by later files.