Add kindergarten-garden

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",

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

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.

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

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/"
+}

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"

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

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]

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"

exercises/practice/kindergarten-garden/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.25.2

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