diff --git a/config.json b/config.json index 01866f5..07f848e 100644 --- a/config.json +++ b/config.json @@ -242,6 +242,14 @@ "prerequisites": [], "difficulty": 3 }, + { + "slug": "kindergarten-garden", + "name": "Kindergarten Garden", + "uuid": "bd0410ff-0dfd-48e9-b155-489c55e6702b", + "practices": [], + "prerequisites": [], + "difficulty": 3 + }, { "slug": "line-up", "name": "Line Up", diff --git a/exercises/practice/kindergarten-garden/.docs/instructions.md b/exercises/practice/kindergarten-garden/.docs/instructions.md new file mode 100644 index 0000000..6fe11a5 --- /dev/null +++ b/exercises/practice/kindergarten-garden/.docs/instructions.md @@ -0,0 +1,56 @@ +# Instructions + +Your task is to, given a diagram, determine which plants each child in the kindergarten class is responsible for. + +There are 12 children in the class: + +- Alice, Bob, Charlie, David, Eve, Fred, Ginny, Harriet, Ileana, Joseph, Kincaid, and Larry. + +Four different types of seeds are planted: + +| Plant | Diagram encoding | +| ------ | ---------------- | +| Grass | G | +| Clover | C | +| Radish | R | +| Violet | V | + +Each child gets four cups, two on each row: + +```text +[window][window][window] +........................ # each dot represents a cup +........................ +``` + +Their teacher assigns cups to the children alphabetically by their names, which means that Alice comes first and Larry comes last. + +Here is an example diagram representing Alice's plants: + +```text +[window][window][window] +VR...................... +RG...................... +``` + +In the first row, nearest the windows, she has a violet and a radish. +In the second row she has a radish and some grass. + +Your program will be given the plants from left-to-right starting with the row nearest the windows. +From this, it should be able to determine which plants belong to each student. + +For example, if it's told that the garden looks like so: + +```text +[window][window][window] +VRCGVVRVCGGCCGVRGCVCGCGV +VRCCCGCRRGVCGCRVVCVGCGCV +``` + +Then if asked for Alice's plants, it should provide: + +- Violets, radishes, violets, radishes + +While asking for Bob's plants would yield: + +- Clover, grass, clover, clover diff --git a/exercises/practice/kindergarten-garden/.docs/introduction.md b/exercises/practice/kindergarten-garden/.docs/introduction.md new file mode 100644 index 0000000..5ad97d2 --- /dev/null +++ b/exercises/practice/kindergarten-garden/.docs/introduction.md @@ -0,0 +1,6 @@ +# Introduction + +The kindergarten class is learning about growing plants. +The teacher thought it would be a good idea to give the class seeds to plant and grow in the dirt. +To this end, the children have put little cups along the window sills and planted one type of plant in each cup. +The children got to pick their favorites from four available types of seeds: grass, clover, radishes, and violets. diff --git a/exercises/practice/kindergarten-garden/.meta/Example.lean b/exercises/practice/kindergarten-garden/.meta/Example.lean new file mode 100644 index 0000000..0e2678d --- /dev/null +++ b/exercises/practice/kindergarten-garden/.meta/Example.lean @@ -0,0 +1,26 @@ +namespace KindergartenGarden + +inductive Plant where + | grass | clover | radishes | violets + deriving BEq, Repr + +def lookup (letter : Char) : Plant := + match letter with + | 'C' => .clover + | 'R' => .radishes + | 'V' => .violets + | _ => .grass + +def plants (diagram : String) (student: String) : Vector Plant 4 := + let letters := diagram.toSlice.startPos + let first := 2 * (student.front.val.toNat - 65) + let second := first + 1 + let third := (diagram.length + 1) / 2 + first + let fourth := third + 1 + let firstPlant := first |> letters.nextn |> (·.get!) |> lookup + let secondPlant := second |> letters.nextn |> (·.get!) |> lookup + let thirdPlant := third |> letters.nextn |> (·.get!) |> lookup + let fourthPlant := fourth |> letters.nextn |> (·.get!) |> lookup + { toArray := #[firstPlant, secondPlant, thirdPlant, fourthPlant], size_toArray := by simp } + +end KindergartenGarden diff --git a/exercises/practice/kindergarten-garden/.meta/config.json b/exercises/practice/kindergarten-garden/.meta/config.json new file mode 100644 index 0000000..6ab757e --- /dev/null +++ b/exercises/practice/kindergarten-garden/.meta/config.json @@ -0,0 +1,19 @@ +{ + "authors": [ + "keiravillekode" + ], + "files": { + "solution": [ + "KindergartenGarden.lean" + ], + "test": [ + "KindergartenGardenTest.lean" + ], + "example": [ + ".meta/Example.lean" + ] + }, + "blurb": "Given a diagram, determine which plants each child in the kindergarten class is responsible for.", + "source": "Exercise by the JumpstartLab team for students at The Turing School of Software and Design.", + "source_url": "https://www.turing.edu/" +} diff --git a/exercises/practice/kindergarten-garden/.meta/tests.toml b/exercises/practice/kindergarten-garden/.meta/tests.toml new file mode 100644 index 0000000..0cdd9ad --- /dev/null +++ b/exercises/practice/kindergarten-garden/.meta/tests.toml @@ -0,0 +1,61 @@ +# This is an auto-generated file. +# +# Regenerating this file via `configlet sync` will: +# - Recreate every `description` key/value pair +# - Recreate every `reimplements` key/value pair, where they exist in problem-specifications +# - Remove any `include = true` key/value pair (an omitted `include` key implies inclusion) +# - Preserve any other key/value pair +# +# As user-added comments (using the # character) will be removed when this file +# is regenerated, comments can be added via a `comment` key. + +[1fc316ed-17ab-4fba-88ef-3ae78296b692] +description = "partial garden -> garden with single student" + +[acd19dc1-2200-4317-bc2a-08f021276b40] +description = "partial garden -> different garden with single student" + +[c376fcc8-349c-446c-94b0-903947315757] +description = "partial garden -> garden with two students" + +[2d620f45-9617-4924-9d27-751c80d17db9] +description = "partial garden -> multiple students for the same garden with three students -> second student's garden" + +[57712331-4896-4364-89f8-576421d69c44] +description = "partial garden -> multiple students for the same garden with three students -> third student's garden" + +[149b4290-58e1-40f2-8ae4-8b87c46e765b] +description = "full garden -> for Alice, first student's garden" + +[ba25dbbc-10bd-4a37-b18e-f89ecd098a5e] +description = "full garden -> for Bob, second student's garden" + +[566b621b-f18e-4c5f-873e-be30544b838c] +description = "full garden -> for Charlie" + +[3ad3df57-dd98-46fc-9269-1877abf612aa] +description = "full garden -> for David" + +[0f0a55d1-9710-46ed-a0eb-399ba8c72db2] +description = "full garden -> for Eve" + +[a7e80c90-b140-4ea1-aee3-f4625365c9a4] +description = "full garden -> for Fred" + +[9d94b273-2933-471b-86e8-dba68694c615] +description = "full garden -> for Ginny" + +[f55bc6c2-ade8-4844-87c4-87196f1b7258] +description = "full garden -> for Harriet" + +[759070a3-1bb1-4dd4-be2c-7cce1d7679ae] +description = "full garden -> for Ileana" + +[78578123-2755-4d4a-9c7d-e985b8dda1c6] +description = "full garden -> for Joseph" + +[6bb66df7-f433-41ab-aec2-3ead6e99f65b] +description = "full garden -> for Kincaid, second to last student's garden" + +[d7edec11-6488-418a-94e6-ed509e0fa7eb] +description = "full garden -> for Larry, last student's garden" diff --git a/exercises/practice/kindergarten-garden/KindergartenGarden.lean b/exercises/practice/kindergarten-garden/KindergartenGarden.lean new file mode 100644 index 0000000..b981c28 --- /dev/null +++ b/exercises/practice/kindergarten-garden/KindergartenGarden.lean @@ -0,0 +1,10 @@ +namespace KindergartenGarden + +inductive Plant where + | grass | clover | radishes | violets + deriving BEq, Repr + +def plants (diagram : String) (student: String) : Vector Plant 4 := + sorry --remove this line and implement the function + +end KindergartenGarden diff --git a/exercises/practice/kindergarten-garden/KindergartenGardenTest.lean b/exercises/practice/kindergarten-garden/KindergartenGardenTest.lean new file mode 100644 index 0000000..dd37f21 --- /dev/null +++ b/exercises/practice/kindergarten-garden/KindergartenGardenTest.lean @@ -0,0 +1,44 @@ +import LeanTest +import KindergartenGarden + +open LeanTest + +def kindergartenGardenTests : TestSuite := + (TestSuite.empty "KindergartenGarden") + |>.addTest "partial garden -> garden with single student" (do + return assertEqual ⟨#[KindergartenGarden.Plant.radishes, KindergartenGarden.Plant.clover, KindergartenGarden.Plant.grass, KindergartenGarden.Plant.grass], by decide⟩ (KindergartenGarden.plants "RC\nGG" "Alice")) + |>.addTest "partial garden -> different garden with single student" (do + return assertEqual ⟨#[KindergartenGarden.Plant.violets, KindergartenGarden.Plant.clover, KindergartenGarden.Plant.radishes, KindergartenGarden.Plant.clover], by decide⟩ (KindergartenGarden.plants "VC\nRC" "Alice")) + |>.addTest "partial garden -> garden with two students" (do + return assertEqual ⟨#[KindergartenGarden.Plant.clover, KindergartenGarden.Plant.grass, KindergartenGarden.Plant.radishes, KindergartenGarden.Plant.clover], by decide⟩ (KindergartenGarden.plants "VVCG\nVVRC" "Bob")) + |>.addTest "partial garden -> multiple students for the same garden with three students -> second student's garden" (do + return assertEqual ⟨#[KindergartenGarden.Plant.clover, KindergartenGarden.Plant.clover, KindergartenGarden.Plant.clover, KindergartenGarden.Plant.clover], by decide⟩ (KindergartenGarden.plants "VVCCGG\nVVCCGG" "Bob")) + |>.addTest "partial garden -> multiple students for the same garden with three students -> third student's garden" (do + return assertEqual ⟨#[KindergartenGarden.Plant.grass, KindergartenGarden.Plant.grass, KindergartenGarden.Plant.grass, KindergartenGarden.Plant.grass], by decide⟩ (KindergartenGarden.plants "VVCCGG\nVVCCGG" "Charlie")) + |>.addTest "full garden -> for Alice, first student's garden" (do + return assertEqual ⟨#[KindergartenGarden.Plant.violets, KindergartenGarden.Plant.radishes, KindergartenGarden.Plant.violets, KindergartenGarden.Plant.radishes], by decide⟩ (KindergartenGarden.plants "VRCGVVRVCGGCCGVRGCVCGCGV\nVRCCCGCRRGVCGCRVVCVGCGCV" "Alice")) + |>.addTest "full garden -> for Bob, second student's garden" (do + return assertEqual ⟨#[KindergartenGarden.Plant.clover, KindergartenGarden.Plant.grass, KindergartenGarden.Plant.clover, KindergartenGarden.Plant.clover], by decide⟩ (KindergartenGarden.plants "VRCGVVRVCGGCCGVRGCVCGCGV\nVRCCCGCRRGVCGCRVVCVGCGCV" "Bob")) + |>.addTest "full garden -> for Charlie" (do + return assertEqual ⟨#[KindergartenGarden.Plant.violets, KindergartenGarden.Plant.violets, KindergartenGarden.Plant.clover, KindergartenGarden.Plant.grass], by decide⟩ (KindergartenGarden.plants "VRCGVVRVCGGCCGVRGCVCGCGV\nVRCCCGCRRGVCGCRVVCVGCGCV" "Charlie")) + |>.addTest "full garden -> for David" (do + return assertEqual ⟨#[KindergartenGarden.Plant.radishes, KindergartenGarden.Plant.violets, KindergartenGarden.Plant.clover, KindergartenGarden.Plant.radishes], by decide⟩ (KindergartenGarden.plants "VRCGVVRVCGGCCGVRGCVCGCGV\nVRCCCGCRRGVCGCRVVCVGCGCV" "David")) + |>.addTest "full garden -> for Eve" (do + return assertEqual ⟨#[KindergartenGarden.Plant.clover, KindergartenGarden.Plant.grass, KindergartenGarden.Plant.radishes, KindergartenGarden.Plant.grass], by decide⟩ (KindergartenGarden.plants "VRCGVVRVCGGCCGVRGCVCGCGV\nVRCCCGCRRGVCGCRVVCVGCGCV" "Eve")) + |>.addTest "full garden -> for Fred" (do + return assertEqual ⟨#[KindergartenGarden.Plant.grass, KindergartenGarden.Plant.clover, KindergartenGarden.Plant.violets, KindergartenGarden.Plant.clover], by decide⟩ (KindergartenGarden.plants "VRCGVVRVCGGCCGVRGCVCGCGV\nVRCCCGCRRGVCGCRVVCVGCGCV" "Fred")) + |>.addTest "full garden -> for Ginny" (do + return assertEqual ⟨#[KindergartenGarden.Plant.clover, KindergartenGarden.Plant.grass, KindergartenGarden.Plant.grass, KindergartenGarden.Plant.clover], by decide⟩ (KindergartenGarden.plants "VRCGVVRVCGGCCGVRGCVCGCGV\nVRCCCGCRRGVCGCRVVCVGCGCV" "Ginny")) + |>.addTest "full garden -> for Harriet" (do + return assertEqual ⟨#[KindergartenGarden.Plant.violets, KindergartenGarden.Plant.radishes, KindergartenGarden.Plant.radishes, KindergartenGarden.Plant.violets], by decide⟩ (KindergartenGarden.plants "VRCGVVRVCGGCCGVRGCVCGCGV\nVRCCCGCRRGVCGCRVVCVGCGCV" "Harriet")) + |>.addTest "full garden -> for Ileana" (do + return assertEqual ⟨#[KindergartenGarden.Plant.grass, KindergartenGarden.Plant.clover, KindergartenGarden.Plant.violets, KindergartenGarden.Plant.clover], by decide⟩ (KindergartenGarden.plants "VRCGVVRVCGGCCGVRGCVCGCGV\nVRCCCGCRRGVCGCRVVCVGCGCV" "Ileana")) + |>.addTest "full garden -> for Joseph" (do + return assertEqual ⟨#[KindergartenGarden.Plant.violets, KindergartenGarden.Plant.clover, KindergartenGarden.Plant.violets, KindergartenGarden.Plant.grass], by decide⟩ (KindergartenGarden.plants "VRCGVVRVCGGCCGVRGCVCGCGV\nVRCCCGCRRGVCGCRVVCVGCGCV" "Joseph")) + |>.addTest "full garden -> for Kincaid, second to last student's garden" (do + return assertEqual ⟨#[KindergartenGarden.Plant.grass, KindergartenGarden.Plant.clover, KindergartenGarden.Plant.clover, KindergartenGarden.Plant.grass], by decide⟩ (KindergartenGarden.plants "VRCGVVRVCGGCCGVRGCVCGCGV\nVRCCCGCRRGVCGCRVVCVGCGCV" "Kincaid")) + |>.addTest "full garden -> for Larry, last student's garden" (do + return assertEqual ⟨#[KindergartenGarden.Plant.grass, KindergartenGarden.Plant.violets, KindergartenGarden.Plant.clover, KindergartenGarden.Plant.violets], by decide⟩ (KindergartenGarden.plants "VRCGVVRVCGGCCGVRGCVCGCGV\nVRCCCGCRRGVCGCRVVCVGCGCV" "Larry")) + +def main : IO UInt32 := do + runTestSuitesWithExitCode [kindergartenGardenTests] diff --git a/exercises/practice/kindergarten-garden/lakefile.toml b/exercises/practice/kindergarten-garden/lakefile.toml new file mode 100644 index 0000000..e6d53d0 --- /dev/null +++ b/exercises/practice/kindergarten-garden/lakefile.toml @@ -0,0 +1,15 @@ +name = "kindergarten-garden" +version = "0.1.0" +defaultTargets = ["KindergartenGardenTest"] +testDriver = "KindergartenGardenTest" + +[[lean_lib]] +name = "LeanTest" +srcDir = "vendor/LeanTest" + +[[lean_lib]] +name = "KindergartenGarden" + +[[lean_exe]] +name = "KindergartenGardenTest" +root = "KindergartenGardenTest" diff --git a/exercises/practice/kindergarten-garden/lean-toolchain b/exercises/practice/kindergarten-garden/lean-toolchain new file mode 100644 index 0000000..370b26d --- /dev/null +++ b/exercises/practice/kindergarten-garden/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.25.2 diff --git a/exercises/practice/kindergarten-garden/vendor/LeanTest/LeanTest.lean b/exercises/practice/kindergarten-garden/vendor/LeanTest/LeanTest.lean new file mode 100644 index 0000000..012ba20 --- /dev/null +++ b/exercises/practice/kindergarten-garden/vendor/LeanTest/LeanTest.lean @@ -0,0 +1,4 @@ +-- This module serves as the root of the `LeanTest` library. +-- Import modules here that should be built as part of the library. +import LeanTest.Assertions +import LeanTest.Test diff --git a/exercises/practice/kindergarten-garden/vendor/LeanTest/LeanTest/Assertions.lean b/exercises/practice/kindergarten-garden/vendor/LeanTest/LeanTest/Assertions.lean new file mode 100644 index 0000000..60e4ad8 --- /dev/null +++ b/exercises/practice/kindergarten-garden/vendor/LeanTest/LeanTest/Assertions.lean @@ -0,0 +1,166 @@ +/- +Assertion functions for unit testing. +-/ + +namespace LeanTest + +/-- Result of a test assertion -/ +inductive AssertionResult where + | success : AssertionResult + | failure (message : String) : AssertionResult + deriving Repr, BEq + +namespace AssertionResult + +def isSuccess : AssertionResult → Bool + | success => true + | failure _ => false + +def getMessage : AssertionResult → String + | success => "Assertion passed" + | failure msg => msg + +end AssertionResult + +/-- Assert that a boolean condition is true -/ +def assert (condition : Bool) (message : String := "Assertion failed") : AssertionResult := + if condition then + .success + else + .failure message + +/-- Assert that two values are equal -/ +def assertEqual [BEq α] [Repr α] (expected : α) (actual : α) (message : String := "") : AssertionResult := + if expected == actual then + .success + else + let msg := if message.isEmpty then + s!"Expected: {repr expected}\nActual: {repr actual}" + else + s!"{message}\nExpected: {repr expected}\nActual: {repr actual}" + .failure msg + +/-- Assert that two values are not equal -/ +def assertNotEqual [BEq α] [Repr α] (expected : α) (actual : α) (message : String := "") : AssertionResult := + if expected != actual then + .success + else + let msg := if message.isEmpty then + s!"Expected values to be different, but both were: {repr expected}" + else + s!"{message}\nExpected values to be different, but both were: {repr expected}" + .failure msg + +/-- Refute that a boolean condition is true (assert it's false) -/ +def refute (condition : Bool) (message : String := "Refute failed - condition was true") : AssertionResult := + if !condition then + .success + else + .failure message + +/-- Assert that a value is true -/ +def assertTrue (value : Bool) (message : String := "Expected true but got false") : AssertionResult := + assert value message + +/-- Assert that a value is false -/ +def assertFalse (value : Bool) (message : String := "Expected false but got true") : AssertionResult := + refute value message + +/-- Assert that an Option is some -/ +def assertSome [Repr α] (opt : Option α) (message : String := "Expected Some but got None") : AssertionResult := + match opt with + | some _ => .success + | none => .failure message + +/-- Assert that an Option is none -/ +def assertNone [Repr α] (opt : Option α) (message : String := "") : AssertionResult := + match opt with + | none => .success + | some val => + let msg := if message.isEmpty then + s!"Expected None but got Some: {repr val}" + else + s!"{message}\nExpected None but got Some: {repr val}" + .failure msg + +/-- Assert that a list is empty -/ +def assertEmpty [Repr α] (list : List α) (message : String := "") : AssertionResult := + match list with + | [] => .success + | _ => + let msg := if message.isEmpty then + s!"Expected empty list but got: {repr list}" + else + s!"{message}\nExpected empty list but got: {repr list}" + .failure msg + +/-- Assert that a list contains an element -/ +def assertContains [BEq α] [Repr α] (list : List α) (element : α) (message : String := "") : AssertionResult := + if list.contains element then + .success + else + let msg := if message.isEmpty then + s!"Expected list to contain {repr element}\nList: {repr list}" + else + s!"{message}\nExpected list to contain {repr element}\nList: {repr list}" + .failure msg + +/-- Assert that a value is within a range (inclusive) -/ +def assertInRange [LE α] [DecidableRel (· ≤ · : α → α → Prop)] [Repr α] + (value : α) (min : α) (max : α) (message : String := "") : AssertionResult := + if min ≤ value ∧ value ≤ max then + .success + else + let msg := if message.isEmpty then + s!"Expected {repr value} to be in range [{repr min}, {repr max}]" + else + s!"{message}\nExpected {repr value} to be in range [{repr min}, {repr max}]" + .failure msg + +/-- Assert that an Except value is an error -/ +def assertError [Repr ε] [Repr α] (result : Except ε α) (message : String := "") : AssertionResult := + match result with + | .error _ => .success + | .ok val => + let msg := if message.isEmpty then + s!"Expected error but got Ok: {repr val}" + else + s!"{message}\nExpected error but got Ok: {repr val}" + .failure msg + +/-- Assert that an Except value is ok -/ +def assertOk [Repr ε] [Repr α] (result : Except ε α) (message : String := "") : AssertionResult := + match result with + | .ok _ => .success + | .error err => + let msg := if message.isEmpty then + s!"Expected Ok but got error: {repr err}" + else + s!"{message}\nExpected Ok but got error: {repr err}" + .failure msg + +/-- Assert that an IO action throws an error -/ +def assertThrows (action : IO α) (message : String := "") : IO AssertionResult := do + try + let _ ← action + let msg := if message.isEmpty then + "Expected IO action to throw an error, but it succeeded" + else + s!"{message}\nExpected IO action to throw an error, but it succeeded" + return .failure msg + catch _ => + return .success + +/-- Assert that an IO action succeeds (doesn't throw) -/ +def assertSucceeds (action : IO α) (message : String := "") : IO AssertionResult := do + try + let _ ← action + return .success + catch e => + let msg := if message.isEmpty then + s!"Expected IO action to succeed, but it threw: {e}" + else + s!"{message}\nExpected IO action to succeed, but it threw: {e}" + return .failure msg + +end LeanTest diff --git a/exercises/practice/kindergarten-garden/vendor/LeanTest/LeanTest/Test.lean b/exercises/practice/kindergarten-garden/vendor/LeanTest/LeanTest/Test.lean new file mode 100644 index 0000000..5ddbae5 --- /dev/null +++ b/exercises/practice/kindergarten-garden/vendor/LeanTest/LeanTest/Test.lean @@ -0,0 +1,130 @@ +/- +Test case and test suite management. +-/ + +import LeanTest.Assertions + +namespace LeanTest + +/-- A single test case -/ +structure TestCase where + description : String + test : IO AssertionResult + deriving Inhabited + +/-- Result of running a test -/ +structure TestResult where + description : String + result : AssertionResult + deriving Repr + +/-- A collection of tests (test suite) -/ +structure TestSuite where + name : String + tests : List TestCase + deriving Inhabited + +namespace TestSuite + +/-- Create an empty test suite -/ +def empty (name : String) : TestSuite := + { name := name, tests := [] } + +/-- Add a test to the suite -/ +def addTest (suite : TestSuite) (description : String) (test : IO AssertionResult) : TestSuite := + { suite with tests := suite.tests ++ [{ description := description, test := test }] } + +end TestSuite + +/-- Test statistics -/ +structure TestStats where + total : Nat + passed : Nat + failed : Nat + deriving Repr + +namespace TestStats + +def empty : TestStats := + { total := 0, passed := 0, failed := 0 } + +def addResult (stats : TestStats) (result : AssertionResult) : TestStats := + { total := stats.total + 1 + , passed := if result.isSuccess then stats.passed + 1 else stats.passed + , failed := if result.isSuccess then stats.failed else stats.failed + 1 + } + +end TestStats + +/-- ANSI color codes for terminal output -/ +def greenColor : String := "\x1b[32m" +def redColor : String := "\x1b[31m" +def yellowColor : String := "\x1b[33m" +def resetColor : String := "\x1b[0m" +def boldColor : String := "\x1b[1m" + +/-- Run a single test and print the result -/ +def runTest (testCase : TestCase) : IO TestResult := do + let result ← testCase.test + match result with + | .success => + IO.println s!" {greenColor}✓{resetColor} {testCase.description}" + | .failure msg => + IO.println s!" {redColor}✗{resetColor} {testCase.description}" + IO.println s!" {redColor}{msg}{resetColor}" + return { description := testCase.description, result := result } + +/-- Run all tests in a test suite -/ +def runTestSuite (suite : TestSuite) : IO TestStats := do + IO.println s!"\n{boldColor}{suite.name}{resetColor}" + let mut stats := TestStats.empty + + for testCase in suite.tests do + let result ← runTest testCase + stats := stats.addResult result.result + + return stats + +/-- Print test summary -/ +def printSummary (stats : TestStats) : IO Unit := do + IO.println "" + IO.println s!"{boldColor}Test Summary:{resetColor}" + IO.println s!" Total: {stats.total}" + IO.println s!" {greenColor}Passed: {stats.passed}{resetColor}" + + if stats.failed > 0 then + IO.println s!" {redColor}Failed: {stats.failed}{resetColor}" + IO.println s!"\n{redColor}FAILED{resetColor}" + else + IO.println s!"\n{greenColor}ALL TESTS PASSED{resetColor}" + +/-- Run multiple test suites -/ +def runTestSuites (suites : List TestSuite) : IO Unit := do + let mut totalStats := TestStats.empty + + for suite in suites do + let stats ← runTestSuite suite + totalStats := { + total := totalStats.total + stats.total, + passed := totalStats.passed + stats.passed, + failed := totalStats.failed + stats.failed + } + + printSummary totalStats + +/-- Run multiple test suites and return exit code (0 = all passed, 1 = some failed) -/ +def runTestSuitesWithExitCode (suites : List TestSuite) : IO UInt32 := do + let mut totalStats := TestStats.empty + + for suite in suites do + let stats ← runTestSuite suite + totalStats := { + total := totalStats.total + stats.total, + passed := totalStats.passed + stats.passed, + failed := totalStats.failed + stats.failed + } + + printSummary totalStats + return if totalStats.failed > 0 then 1 else 0 + +end LeanTest diff --git a/generators/Generator/Generator.lean b/generators/Generator/Generator.lean index 63fb676..44e01eb 100644 --- a/generators/Generator/Generator.lean +++ b/generators/Generator/Generator.lean @@ -29,6 +29,7 @@ import Generator.GigasecondGenerator import Generator.CamiciaGenerator import Generator.ChangeGenerator import Generator.HammingGenerator +import Generator.KindergartenGardenGenerator import Generator.LineUpGenerator import Generator.TwoFerGenerator import Generator.YachtGenerator @@ -127,6 +128,7 @@ def dispatch : Std.HashMap String (introGenerator × testCaseGenerator × endBod ("Camicia", (CamiciaGenerator.genIntro, CamiciaGenerator.genTestCase, CamiciaGenerator.genEnd)), ("Change", (ChangeGenerator.genIntro, ChangeGenerator.genTestCase, ChangeGenerator.genEnd)), ("Hamming", (HammingGenerator.genIntro, HammingGenerator.genTestCase, HammingGenerator.genEnd)), + ("KindergartenGarden", (KindergartenGardenGenerator.genIntro, KindergartenGardenGenerator.genTestCase, KindergartenGardenGenerator.genEnd)), ("LineUp", (LineUpGenerator.genIntro, LineUpGenerator.genTestCase, LineUpGenerator.genEnd)), ("TwoFer", (TwoFerGenerator.genIntro, TwoFerGenerator.genTestCase, TwoFerGenerator.genEnd)), ("Yacht", (YachtGenerator.genIntro, YachtGenerator.genTestCase, YachtGenerator.genEnd)), diff --git a/generators/Generator/Generator/KindergartenGardenGenerator.lean b/generators/Generator/Generator/KindergartenGardenGenerator.lean new file mode 100644 index 0000000..e8d9c13 --- /dev/null +++ b/generators/Generator/Generator/KindergartenGardenGenerator.lean @@ -0,0 +1,40 @@ +import Lean.Data.Json +import Std +import Helper + +open Lean +open Std +open Helper + +namespace KindergartenGardenGenerator + +def genIntro (exercise : String) : String := s!"import LeanTest +import {exercise} + +open LeanTest + +def {exercise.decapitalize}Tests : TestSuite := + (TestSuite.empty \"{exercise}\")" + +def genTestCase (exercise : String) (case : TreeMap.Raw String Json) : String := + let input := case.get! "input" + let expected := case.get! "expected" + |>.getArr? + |> getOk + |>.map (λ j => ("KindergartenGarden.Plant." ++ ·) <| toCamel <| toLiteral s!"{j}") + let description := case.get! "description" + |> (·.compress) + let funName := getFunName (case.get! "property") + let call := s!"({exercise}.{funName} {insertAllInputs input})" + s!" + |>.addTest {description} (do + return assertEqual ⟨{expected}, by decide⟩ {call})" + +def genEnd (exercise : String) : String := + s!" + +def main : IO UInt32 := do + runTestSuitesWithExitCode [{exercise.decapitalize}Tests] +" + +end KindergartenGardenGenerator