08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
97 lines
2.7 KiB
Text
97 lines
2.7 KiB
Text
import Lean.Util.Diff
|
||
|
||
open Lean.Diff
|
||
|
||
/-!
|
||
# Tests for diff
|
||
|
||
Tests for various parts of the diffing system
|
||
-/
|
||
|
||
|
||
/-!
|
||
## Prefix and Suffix Matching
|
||
|
||
These tests check that the prefix and suffix matching operations on subarrays used by diff perform
|
||
as expected.
|
||
-/
|
||
|
||
def Ex.abc' := #['a', 'b', 'c']
|
||
def Ex.abc := abc'.toSubarray
|
||
|
||
def Ex.abcde : Subarray Char := #['a','b','c','d','e'].toSubarray
|
||
def Ex.bcde : Subarray Char := #['b','c','d','e'].toSubarray
|
||
|
||
/-- info: (#['a', 'b', 'c'], #[].toSubarray, #['d', 'e'].toSubarray) -/
|
||
#guard_msgs in
|
||
#eval matchPrefix Ex.abc Ex.abcde
|
||
|
||
/-- info: (#['a', 'b', 'c'], #['d', 'e'].toSubarray, #[].toSubarray) -/
|
||
#guard_msgs in
|
||
#eval matchPrefix Ex.abcde Ex.abc
|
||
|
||
/-- info: (#[], #['a', 'b', 'c'].toSubarray, #['b', 'c', 'd', 'e'].toSubarray) -/
|
||
#guard_msgs in
|
||
#eval matchPrefix Ex.abc Ex.bcde
|
||
|
||
/-- info: (#[], #["A"].toSubarray, #["B"].toSubarray) -/
|
||
#guard_msgs in
|
||
#eval matchPrefix #["A"].toSubarray #["B"].toSubarray
|
||
|
||
/-- info: (#["D", "E", "F"], #["G"].toSubarray, #[].toSubarray) -/
|
||
#guard_msgs in
|
||
#eval matchPrefix #["D", "E", "F", "G"].toSubarray #["D", "E", "F"].toSubarray
|
||
|
||
/-- info: (#["A", "A"], #["B"].toSubarray, #["X"].toSubarray) -/
|
||
#guard_msgs in
|
||
#eval matchPrefix #["A", "A", "B"].toSubarray #["A", "A", "X"].toSubarray
|
||
|
||
|
||
def Ex.xyzabc : Subarray Char := #['x', 'y', 'z', 'a', 'b', 'c'].toSubarray
|
||
def Ex.xyzab : Subarray Char := #['x', 'y', 'z', 'a', 'b'].toSubarray
|
||
|
||
/-- info: (#[].toSubarray, #['x', 'y', 'z'].toSubarray, #['a', 'b', 'c']) -/
|
||
#guard_msgs in
|
||
#eval matchSuffix Ex.abc Ex.xyzabc
|
||
|
||
/-- info: (#['a', 'b', 'c'].toSubarray, #['x', 'y', 'z', 'a', 'b'].toSubarray, #[]) -/
|
||
#guard_msgs in
|
||
#eval matchSuffix Ex.abc Ex.xyzab
|
||
|
||
/-- info: (#['a'].toSubarray, #[].toSubarray, #['b']) -/
|
||
#guard_msgs in
|
||
#eval matchSuffix #['a', 'b'].toSubarray #['b'].toSubarray
|
||
|
||
/-!
|
||
## Least Common Subsequence
|
||
|
||
These tests find least common subsequences.
|
||
-/
|
||
|
||
/-- info: #[] -/
|
||
#guard_msgs in
|
||
#eval lcs (α := Nat) (#[].toSubarray) (#[].toSubarray)
|
||
|
||
/-- info: #[] -/
|
||
#guard_msgs in
|
||
#eval lcs (#[1].toSubarray) (#[].toSubarray)
|
||
|
||
/-- info: #[1] -/
|
||
#guard_msgs in
|
||
#eval lcs (#[1].toSubarray) (#[1].toSubarray)
|
||
|
||
/-- info: #[1, 3] -/
|
||
#guard_msgs in
|
||
#eval lcs (#[1,3].toSubarray) (#[1,2,3].toSubarray)
|
||
|
||
/-- info: #["A", "A"] -/
|
||
#guard_msgs in
|
||
#eval lcs ("A,A,B".split (·==',') |>.toStringArray).toSubarray ("A,A,X".split (·==',') |>.toStringArray).toSubarray
|
||
|
||
/-- info: #["A", "D", "E", "F"] -/
|
||
#guard_msgs in
|
||
#eval lcs ("A,C,D,E,F,G".split (·==',') |>.toStringArray).toSubarray ("A,Y,Z,D,E,F".split (·==',') |>.toStringArray).toSubarray
|
||
|
||
/-- info: #["A", "A", "D", "E", "F"] -/
|
||
#guard_msgs in
|
||
#eval lcs ("A,A,B,C,D,E,F,G".split (·==',') |>.toStringArray).toSubarray ("A,A,X,Y,Z,D,E,F".split (·==',') |>.toStringArray).toSubarray
|