Skip to content

rectangles: generate using serializeList #104

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
keiravillekode merged 1 commit into from
Feb 6, 2026
Merged

rectangles: generate using serializeList #104

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
91 changes: 78 additions & 13 deletions exercises/practice/rectangles/RectanglesTest.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,31 +8,96 @@ def rectanglesTests : TestSuite :=
|>.addTest "no rows" (do
return assertEqual 0 (Rectangles.rectangles #[]))
|>.addTest "no columns" (do
return assertEqual 0 (Rectangles.rectangles #[""]))
return assertEqual 0 (Rectangles.rectangles #[
""
]))
|>.addTest "no rectangles" (do
return assertEqual 0 (Rectangles.rectangles #[" "]))
return assertEqual 0 (Rectangles.rectangles #[
" "
]))
|>.addTest "one rectangle" (do
return assertEqual 1 (Rectangles.rectangles #["+-+","| |","+-+"]))
return assertEqual 1 (Rectangles.rectangles #[
"+-+",
"| |",
"+-+"
]))
|>.addTest "two rectangles without shared parts" (do
return assertEqual 2 (Rectangles.rectangles #[" +-+"," | |","+-+-+","| | ","+-+ "]))
return assertEqual 2 (Rectangles.rectangles #[
" +-+",
" | |",
"+-+-+",
"| | ",
"+-+ "
]))
|>.addTest "five rectangles with shared parts" (do
return assertEqual 5 (Rectangles.rectangles #[" +-+"," | |","+-+-+","| | |","+-+-+"]))
return assertEqual 5 (Rectangles.rectangles #[
" +-+",
" | |",
"+-+-+",
"| | |",
"+-+-+"
]))
|>.addTest "rectangle of height 1 is counted" (do
return assertEqual 1 (Rectangles.rectangles #["+--+","+--+"]))
return assertEqual 1 (Rectangles.rectangles #[
"+--+",
"+--+"
]))
|>.addTest "rectangle of width 1 is counted" (do
return assertEqual 1 (Rectangles.rectangles #["++","||","++"]))
return assertEqual 1 (Rectangles.rectangles #[
"++",
"||",
"++"
]))
|>.addTest "1x1 square is counted" (do
return assertEqual 1 (Rectangles.rectangles #["++","++"]))
return assertEqual 1 (Rectangles.rectangles #[
"++",
"++"
]))
|>.addTest "only complete rectangles are counted" (do
return assertEqual 1 (Rectangles.rectangles #[" +-+"," |","+-+-+","| | -","+-+-+"]))
return assertEqual 1 (Rectangles.rectangles #[
" +-+",
" |",
"+-+-+",
"| | -",
"+-+-+"
]))
|>.addTest "rectangles can be of different sizes" (do
return assertEqual 3 (Rectangles.rectangles #["+------+----+","| | |","+---+--+ |","| | |","+---+-------+"]))
return assertEqual 3 (Rectangles.rectangles #[
"+------+----+",
"| | |",
"+---+--+ |",
"| | |",
"+---+-------+"
]))
|>.addTest "corner is required for a rectangle to be complete" (do
return assertEqual 2 (Rectangles.rectangles #["+------+----+","| | |","+------+ |","| | |","+---+-------+"]))
return assertEqual 2 (Rectangles.rectangles #[
"+------+----+",
"| | |",
"+------+ |",
"| | |",
"+---+-------+"
]))
|>.addTest "large input with many rectangles" (do
return assertEqual 60 (Rectangles.rectangles #["+---+--+----+","| +--+----+","+---+--+ |","| +--+----+","+---+--+--+-+","+---+--+--+-+","+------+ | |"," +-+"]))
return assertEqual 60 (Rectangles.rectangles #[
"+---+--+----+",
"| +--+----+",
"+---+--+ |",
"| +--+----+",
"+---+--+--+-+",
"+---+--+--+-+",
"+------+ | |",
" +-+"
]))
|>.addTest "rectangles must have four sides" (do
return assertEqual 5 (Rectangles.rectangles #["+-+ +-+","| | | |","+-+-+-+"," | | ","+-+-+-+","| | | |","+-+ +-+"]))
return assertEqual 5 (Rectangles.rectangles #[
"+-+ +-+",
"| | | |",
"+-+-+-+",
" | | ",
"+-+-+-+",
"| | | |",
"+-+ +-+"
]))

def main : IO UInt32 := do
runTestSuitesWithExitCode [rectanglesTests]
5 changes: 3 additions & 2 deletions generators/Generator/Generator/RectanglesGenerator.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,12 +17,13 @@ def {exercise.decapitalize}Tests : TestSuite :=
(TestSuite.empty \"{exercise}\")"

def genTestCase (exercise : String) (case : TreeMap.Raw String Json) : String :=
let input := case.get! "input"
let strings := case.get! "input"
|> (·.getObjValD "strings")
let expected := case.get! "expected"
let description := case.get! "description"
|> (·.compress)
let funName := getFunName (case.get! "property")
let call := s!"({exercise}.{funName} #{insertAllInputs input})"
let call := s!"({exercise}.{funName} #{serializeList strings})"
s!"
|>.addTest {description} (do
return assertEqual {expected} {call})"
Expand Down
Loading