Skip to content

adjust generator #102

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
oxe-i merged 1 commit into from
Feb 6, 2026
Merged

adjust generator #102

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
71 changes: 57 additions & 14 deletions exercises/practice/house/HouseTest.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,33 +6,76 @@ open LeanTest
def houseTests : TestSuite :=
(TestSuite.empty "House")
|>.addTest "verse one - the house that jack built" (do
return assertEqual (String.intercalate "\n\n" ["This is the house that Jack built."]) (House.recite ⟨1, by decide⟩ ⟨1, by decide⟩))
return assertEqual (String.intercalate "\n\n" [
"This is the house that Jack built."
]) (House.recite ⟨1, by decide⟩ ⟨1, by decide⟩))
|>.addTest "verse two - the malt that lay" (do
return assertEqual (String.intercalate "\n\n" ["This is the malt that lay in the house that Jack built."]) (House.recite ⟨2, by decide⟩ ⟨2, by decide⟩))
return assertEqual (String.intercalate "\n\n" [
"This is the malt that lay in the house that Jack built."
]) (House.recite ⟨2, by decide⟩ ⟨2, by decide⟩))
|>.addTest "verse three - the rat that ate" (do
return assertEqual (String.intercalate "\n\n" ["This is the rat that ate the malt that lay in the house that Jack built."]) (House.recite ⟨3, by decide⟩ ⟨3, by decide⟩))
return assertEqual (String.intercalate "\n\n" [
"This is the rat that ate the malt that lay in the house that Jack built."
]) (House.recite ⟨3, by decide⟩ ⟨3, by decide⟩))
|>.addTest "verse four - the cat that killed" (do
return assertEqual (String.intercalate "\n\n" ["This is the cat that killed the rat that ate the malt that lay in the house that Jack built."]) (House.recite ⟨4, by decide⟩ ⟨4, by decide⟩))
return assertEqual (String.intercalate "\n\n" [
"This is the cat that killed the rat that ate the malt that lay in the house that Jack built."
]) (House.recite ⟨4, by decide⟩ ⟨4, by decide⟩))
|>.addTest "verse five - the dog that worried" (do
return assertEqual (String.intercalate "\n\n" ["This is the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built."]) (House.recite ⟨5, by decide⟩ ⟨5, by decide⟩))
return assertEqual (String.intercalate "\n\n" [
"This is the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built."
]) (House.recite ⟨5, by decide⟩ ⟨5, by decide⟩))
|>.addTest "verse six - the cow with the crumpled horn" (do
return assertEqual (String.intercalate "\n\n" ["This is the cow with the crumpled horn that tossed the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built."]) (House.recite ⟨6, by decide⟩ ⟨6, by decide⟩))
return assertEqual (String.intercalate "\n\n" [
"This is the cow with the crumpled horn that tossed the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built."
]) (House.recite ⟨6, by decide⟩ ⟨6, by decide⟩))
|>.addTest "verse seven - the maiden all forlorn" (do
return assertEqual (String.intercalate "\n\n" ["This is the maiden all forlorn that milked the cow with the crumpled horn that tossed the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built."]) (House.recite ⟨7, by decide⟩ ⟨7, by decide⟩))
return assertEqual (String.intercalate "\n\n" [
"This is the maiden all forlorn that milked the cow with the crumpled horn that tossed the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built."
]) (House.recite ⟨7, by decide⟩ ⟨7, by decide⟩))
|>.addTest "verse eight - the man all tattered and torn" (do
return assertEqual (String.intercalate "\n\n" ["This is the man all tattered and torn that kissed the maiden all forlorn that milked the cow with the crumpled horn that tossed the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built."]) (House.recite ⟨8, by decide⟩ ⟨8, by decide⟩))
return assertEqual (String.intercalate "\n\n" [
"This is the man all tattered and torn that kissed the maiden all forlorn that milked the cow with the crumpled horn that tossed the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built."
]) (House.recite ⟨8, by decide⟩ ⟨8, by decide⟩))
|>.addTest "verse nine - the priest all shaven and shorn" (do
return assertEqual (String.intercalate "\n\n" ["This is the priest all shaven and shorn that married the man all tattered and torn that kissed the maiden all forlorn that milked the cow with the crumpled horn that tossed the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built."]) (House.recite ⟨9, by decide⟩ ⟨9, by decide⟩))
return assertEqual (String.intercalate "\n\n" [
"This is the priest all shaven and shorn that married the man all tattered and torn that kissed the maiden all forlorn that milked the cow with the crumpled horn that tossed the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built."
]) (House.recite ⟨9, by decide⟩ ⟨9, by decide⟩))
|>.addTest "verse 10 - the rooster that crowed in the morn" (do
return assertEqual (String.intercalate "\n\n" ["This is the rooster that crowed in the morn that woke the priest all shaven and shorn that married the man all tattered and torn that kissed the maiden all forlorn that milked the cow with the crumpled horn that tossed the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built."]) (House.recite ⟨10, by decide⟩ ⟨10, by decide⟩))
return assertEqual (String.intercalate "\n\n" [
"This is the rooster that crowed in the morn that woke the priest all shaven and shorn that married the man all tattered and torn that kissed the maiden all forlorn that milked the cow with the crumpled horn that tossed the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built."
]) (House.recite ⟨10, by decide⟩ ⟨10, by decide⟩))
|>.addTest "verse 11 - the farmer sowing his corn" (do
return assertEqual (String.intercalate "\n\n" ["This is the farmer sowing his corn that kept the rooster that crowed in the morn that woke the priest all shaven and shorn that married the man all tattered and torn that kissed the maiden all forlorn that milked the cow with the crumpled horn that tossed the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built."]) (House.recite ⟨11, by decide⟩ ⟨11, by decide⟩))
return assertEqual (String.intercalate "\n\n" [
"This is the farmer sowing his corn that kept the rooster that crowed in the morn that woke the priest all shaven and shorn that married the man all tattered and torn that kissed the maiden all forlorn that milked the cow with the crumpled horn that tossed the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built."
]) (House.recite ⟨11, by decide⟩ ⟨11, by decide⟩))
|>.addTest "verse 12 - the horse and the hound and the horn" (do
return assertEqual (String.intercalate "\n\n" ["This is the horse and the hound and the horn that belonged to the farmer sowing his corn that kept the rooster that crowed in the morn that woke the priest all shaven and shorn that married the man all tattered and torn that kissed the maiden all forlorn that milked the cow with the crumpled horn that tossed the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built."]) (House.recite ⟨12, by decide⟩ ⟨12, by decide⟩))
return assertEqual (String.intercalate "\n\n" [
"This is the horse and the hound and the horn that belonged to the farmer sowing his corn that kept the rooster that crowed in the morn that woke the priest all shaven and shorn that married the man all tattered and torn that kissed the maiden all forlorn that milked the cow with the crumpled horn that tossed the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built."
]) (House.recite ⟨12, by decide⟩ ⟨12, by decide⟩))
|>.addTest "multiple verses" (do
return assertEqual (String.intercalate "\n\n" ["This is the cat that killed the rat that ate the malt that lay in the house that Jack built.", "This is the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built.", "This is the cow with the crumpled horn that tossed the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built.", "This is the maiden all forlorn that milked the cow with the crumpled horn that tossed the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built.", "This is the man all tattered and torn that kissed the maiden all forlorn that milked the cow with the crumpled horn that tossed the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built."]) (House.recite ⟨4, by decide⟩ ⟨8, by decide⟩))
return assertEqual (String.intercalate "\n\n" [
"This is the cat that killed the rat that ate the malt that lay in the house that Jack built.",
"This is the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built.",
"This is the cow with the crumpled horn that tossed the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built.",
"This is the maiden all forlorn that milked the cow with the crumpled horn that tossed the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built.",
"This is the man all tattered and torn that kissed the maiden all forlorn that milked the cow with the crumpled horn that tossed the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built."
]) (House.recite ⟨4, by decide⟩ ⟨8, by decide⟩))
|>.addTest "full rhyme" (do
return assertEqual (String.intercalate "\n\n" ["This is the house that Jack built.", "This is the malt that lay in the house that Jack built.", "This is the rat that ate the malt that lay in the house that Jack built.", "This is the cat that killed the rat that ate the malt that lay in the house that Jack built.", "This is the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built.", "This is the cow with the crumpled horn that tossed the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built.", "This is the maiden all forlorn that milked the cow with the crumpled horn that tossed the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built.", "This is the man all tattered and torn that kissed the maiden all forlorn that milked the cow with the crumpled horn that tossed the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built.", "This is the priest all shaven and shorn that married the man all tattered and torn that kissed the maiden all forlorn that milked the cow with the crumpled horn that tossed the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built.", "This is the rooster that crowed in the morn that woke the priest all shaven and shorn that married the man all tattered and torn that kissed the maiden all forlorn that milked the cow with the crumpled horn that tossed the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built.", "This is the farmer sowing his corn that kept the rooster that crowed in the morn that woke the priest all shaven and shorn that married the man all tattered and torn that kissed the maiden all forlorn that milked the cow with the crumpled horn that tossed the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built.", "This is the horse and the hound and the horn that belonged to the farmer sowing his corn that kept the rooster that crowed in the morn that woke the priest all shaven and shorn that married the man all tattered and torn that kissed the maiden all forlorn that milked the cow with the crumpled horn that tossed the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built."]) (House.recite ⟨1, by decide⟩ ⟨12, by decide⟩))
return assertEqual (String.intercalate "\n\n" [
"This is the house that Jack built.",
"This is the malt that lay in the house that Jack built.",
"This is the rat that ate the malt that lay in the house that Jack built.",
"This is the cat that killed the rat that ate the malt that lay in the house that Jack built.",
"This is the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built.",
"This is the cow with the crumpled horn that tossed the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built.",
"This is the maiden all forlorn that milked the cow with the crumpled horn that tossed the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built.",
"This is the man all tattered and torn that kissed the maiden all forlorn that milked the cow with the crumpled horn that tossed the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built.",
"This is the priest all shaven and shorn that married the man all tattered and torn that kissed the maiden all forlorn that milked the cow with the crumpled horn that tossed the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built.",
"This is the rooster that crowed in the morn that woke the priest all shaven and shorn that married the man all tattered and torn that kissed the maiden all forlorn that milked the cow with the crumpled horn that tossed the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built.",
"This is the farmer sowing his corn that kept the rooster that crowed in the morn that woke the priest all shaven and shorn that married the man all tattered and torn that kissed the maiden all forlorn that milked the cow with the crumpled horn that tossed the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built.",
"This is the horse and the hound and the horn that belonged to the farmer sowing his corn that kept the rooster that crowed in the morn that woke the priest all shaven and shorn that married the man all tattered and torn that kissed the maiden all forlorn that milked the cow with the crumpled horn that tossed the dog that worried the cat that killed the rat that ate the malt that lay in the house that Jack built."
]) (House.recite ⟨1, by decide⟩ ⟨12, by decide⟩))

def main : IO UInt32 := do
runTestSuitesWithExitCode [houseTests]
Loading
Loading