-
Notifications
You must be signed in to change notification settings - Fork 406
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Browse files
Browse the repository at this point in the history
#2966 was the `@[extern]` bug that prompted development of the `test_extern` command, but then we merged the fix to #2966 without updating the tests to use `test_extern`.
- Loading branch information
Showing
1 changed file
with
23 additions
and
73 deletions.
There are no files selected for viewing
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,81 +1,31 @@ | ||
| import Lean | ||
| import Lean.Util.TestExtern | ||
|
|
||
| def testCopySlice (src : Array UInt8) (srcOff : Nat) (dest : Array UInt8) (destOff len : Nat) : Bool := | ||
| (ByteArray.copySlice ⟨src⟩ srcOff ⟨dest⟩ destOff len |>.toList) == | ||
| (ByteArray.copySlice ⟨src⟩ srcOff ⟨dest⟩ destOff len |>.toList) | ||
|
|
||
| -- We verify that the `@[extern]` implementation of `ByteArray.copySlice` matches the formal definition, | ||
| -- by equating two copies using `==`, unfolding the definition of one, and then calling `native_decide` | ||
| macro "testCopySliceTactic" : tactic => | ||
| `(tactic| | ||
| (dsimp [testCopySlice] | ||
| conv => | ||
| congr | ||
| congr | ||
| dsimp [ByteArray.copySlice] | ||
| native_decide)) | ||
| deriving instance DecidableEq for ByteArray | ||
|
|
||
| -- These used to fail, as reported in #2966 | ||
| test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 1 ⟨#[4, 5, 6, 7, 8, 9, 10, 11, 12, 13]⟩ 0 6 | ||
|
|
||
| example : testCopySlice #[1,2,3] 1 #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] 0 6 := by | ||
| testCopySliceTactic | ||
|
|
||
| example : testCopySlice #[1,2,3] 1 #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] 0 20 := by | ||
| testCopySliceTactic | ||
|
|
||
| example : testCopySlice #[1,2,3] 1 #[4, 5, 6] 0 6 := by | ||
| testCopySliceTactic | ||
|
|
||
| example : testCopySlice #[1,2,3] 1 #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] 1 6 := by | ||
| testCopySliceTactic | ||
|
|
||
| example : testCopySlice #[1,2,3] 1 #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] 1 20 := by | ||
| testCopySliceTactic | ||
|
|
||
| example : testCopySlice #[1,2,3] 0 #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] 0 6 := by | ||
| testCopySliceTactic | ||
|
|
||
| example : testCopySlice #[1,2,3] 0 #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] 0 20 := by | ||
| testCopySliceTactic | ||
|
|
||
| example : testCopySlice #[1,2,3] 0 #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] 1 6 := by | ||
| testCopySliceTactic | ||
|
|
||
| example : testCopySlice #[1,2,3] 0 #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] 1 20 := by | ||
| testCopySliceTactic | ||
| test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 1 ⟨#[4, 5, 6, 7, 8, 9, 10, 11, 12, 13]⟩ 0 6 | ||
| test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 1 ⟨#[4, 5, 6, 7, 8, 9, 10, 11, 12, 13]⟩ 0 20 | ||
|
|
||
| test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 1 ⟨#[4, 5, 6]⟩ 0 6 | ||
| test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 1 ⟨#[4, 5, 6, 7, 8, 9, 10, 11, 12, 13]⟩ 1 6 | ||
| test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 1 ⟨#[4, 5, 6, 7, 8, 9, 10, 11, 12, 13]⟩ 1 20 | ||
| test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 0 ⟨#[4, 5, 6, 7, 8, 9, 10, 11, 12, 13]⟩ 0 6 | ||
| test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 0 ⟨#[4, 5, 6, 7, 8, 9, 10, 11, 12, 13]⟩ 0 20 | ||
| test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 0 ⟨#[4, 5, 6, 7, 8, 9, 10, 11, 12, 13]⟩ 1 6 | ||
| test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 0 ⟨#[4, 5, 6, 7, 8, 9, 10, 11, 12, 13]⟩ 1 20 | ||
|
|
||
| -- These worked prior to #2966; extra text cases can't hurt! | ||
|
|
||
| example : testCopySlice #[1,2,3] 1 #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] 0 2 := by | ||
| testCopySliceTactic | ||
|
|
||
| example : testCopySlice #[1,2,3] 1 #[4, 5, 6] 0 2 := by | ||
| testCopySliceTactic | ||
|
|
||
| example : testCopySlice #[1,2,3] 1 #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] 1 2 := by | ||
| testCopySliceTactic | ||
|
|
||
| example : testCopySlice #[1,2,3] 1 #[4, 5, 6] 1 2 := by | ||
| testCopySliceTactic | ||
|
|
||
| example : testCopySlice #[1,2,3] 1 #[4, 5, 6] 1 6 := by | ||
| testCopySliceTactic | ||
|
|
||
| example : testCopySlice #[1,2,3] 1 #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] 0 2 := by | ||
| testCopySliceTactic | ||
|
|
||
| example : testCopySlice #[1,2,3] 0 #[4, 5, 6] 0 2 := by | ||
| testCopySliceTactic | ||
|
|
||
| example : testCopySlice #[1,2,3] 0 #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] 1 2 := by | ||
| testCopySliceTactic | ||
|
|
||
| example : testCopySlice #[1,2,3] 0 #[4, 5, 6] 1 2 := by | ||
| testCopySliceTactic | ||
|
|
||
| example : testCopySlice #[1,2,3] 0 #[4, 5, 6] 1 6 := by | ||
| testCopySliceTactic | ||
|
|
||
| example : testCopySlice #[1,2,3] 0 #[4, 5, 6] 0 6 := by | ||
| testCopySliceTactic | ||
| test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 1 ⟨#[4, 5, 6, 7, 8, 9, 10, 11, 12, 13]⟩ 0 2 | ||
| test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 1 ⟨#[4, 5, 6]⟩ 0 2 | ||
| test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 1 ⟨#[4, 5, 6, 7, 8, 9, 10, 11, 12, 13]⟩ 1 2 | ||
| test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 1 ⟨#[4, 5, 6]⟩ 1 2 | ||
| test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 1 ⟨#[4, 5, 6]⟩ 1 6 | ||
| test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 1 ⟨#[4, 5, 6, 7, 8, 9, 10, 11, 12, 13]⟩ 0 2 | ||
| test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 0 ⟨#[4, 5, 6]⟩ 0 2 | ||
| test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 0 ⟨#[4, 5, 6, 7, 8, 9, 10, 11, 12, 13]⟩ 1 2 | ||
| test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 0 ⟨#[4, 5, 6]⟩ 1 2 | ||
| test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 0 ⟨#[4, 5, 6]⟩ 1 6 | ||
| test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 0 ⟨#[4, 5, 6]⟩ 0 6 |