max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update tests for #2966 to use test_extern (#3092)

Browse source 
#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`.
This commit is contained in:
Scott Morrison 2023-12-22 09:22:47 +11:00 • committed by GitHub
parent 63d00ea3c2
commit bcc49d1c5f
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 23 additions and 73 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

96
tests/lean/run/2966.lean
View file

@ -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