Skip to content

Commit a29e182

Browse files
keiravillekodekeiravillekode
authored
Add kindergarten-garden (#152)
1 parent d7960a8 commit a29e182

File tree

15 files changed

+588
-0
lines changed

15 files changed

+588
-0
lines changed

‎config.json‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -242,6 +242,14 @@
242242
"prerequisites": [],
243243
"difficulty": 3
244244
},
245+
{
246+
"slug": "kindergarten-garden",
247+
"name": "Kindergarten Garden",
248+
"uuid": "bd0410ff-0dfd-48e9-b155-489c55e6702b",
249+
"practices": [],
250+
"prerequisites": [],
251+
"difficulty": 3
252+
},
245253
{
246254
"slug": "line-up",
247255
"name": "Line Up",

‎exercises/practice/kindergarten-garden/.docs/instructions.md‎

Lines changed: 56 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,56 @@
1+
# Instructions
2+
3+
Your task is to, given a diagram, determine which plants each child in the kindergarten class is responsible for.
4+
5+
There are 12 children in the class:
6+
7+
- Alice, Bob, Charlie, David, Eve, Fred, Ginny, Harriet, Ileana, Joseph, Kincaid, and Larry.
8+
9+
Four different types of seeds are planted:
10+
11+
| Plant | Diagram encoding |
12+
| ------ | ---------------- |
13+
| Grass | G |
14+
| Clover | C |
15+
| Radish | R |
16+
| Violet | V |
17+
18+
Each child gets four cups, two on each row:
19+
20+
```text
21+
[window][window][window]
22+
........................ # each dot represents a cup
23+
........................
24+
```
25+
26+
Their teacher assigns cups to the children alphabetically by their names, which means that Alice comes first and Larry comes last.
27+
28+
Here is an example diagram representing Alice's plants:
29+
30+
```text
31+
[window][window][window]
32+
VR......................
33+
RG......................
34+
```
35+
36+
In the first row, nearest the windows, she has a violet and a radish.
37+
In the second row she has a radish and some grass.
38+
39+
Your program will be given the plants from left-to-right starting with the row nearest the windows.
40+
From this, it should be able to determine which plants belong to each student.
41+
42+
For example, if it's told that the garden looks like so:
43+
44+
```text
45+
[window][window][window]
46+
VRCGVVRVCGGCCGVRGCVCGCGV
47+
VRCCCGCRRGVCGCRVVCVGCGCV
48+
```
49+
50+
Then if asked for Alice's plants, it should provide:
51+
52+
- Violets, radishes, violets, radishes
53+
54+
While asking for Bob's plants would yield:
55+
56+
- Clover, grass, clover, clover

‎exercises/practice/kindergarten-garden/.docs/introduction.md‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
# Introduction
2+
3+
The kindergarten class is learning about growing plants.
4+
The teacher thought it would be a good idea to give the class seeds to plant and grow in the dirt.
5+
To this end, the children have put little cups along the window sills and planted one type of plant in each cup.
6+
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‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
namespace KindergartenGarden
2+
3+
inductive Plant where
4+
| grass | clover | radishes | violets
5+
deriving BEq, Repr
6+
7+
def lookup (letter : Char) : Plant :=
8+
match letter with
9+
| 'C' => .clover
10+
| 'R' => .radishes
11+
| 'V' => .violets
12+
| _ => .grass
13+
14+
def plants (diagram : String) (student: String) : Vector Plant 4 :=
15+
let letters := diagram.toSlice.startPos
16+
let first := 2 * (student.front.val.toNat - 65)
17+
let second := first + 1
18+
let third := (diagram.length + 1) / 2 + first
19+
let fourth := third + 1
20+
let firstPlant := first |> letters.nextn |> (·.get!) |> lookup
21+
let secondPlant := second |> letters.nextn |> (·.get!) |> lookup
22+
let thirdPlant := third |> letters.nextn |> (·.get!) |> lookup
23+
let fourthPlant := fourth |> letters.nextn |> (·.get!) |> lookup
24+
{ toArray := #[firstPlant, secondPlant, thirdPlant, fourthPlant], size_toArray := by simp }
25+
26+
end KindergartenGarden

‎exercises/practice/kindergarten-garden/.meta/config.json‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
{
2+
"authors": [
3+
"keiravillekode"
4+
],
5+
"files": {
6+
"solution": [
7+
"KindergartenGarden.lean"
8+
],
9+
"test": [
10+
"KindergartenGardenTest.lean"
11+
],
12+
"example": [
13+
".meta/Example.lean"
14+
]
15+
},
16+
"blurb": "Given a diagram, determine which plants each child in the kindergarten class is responsible for.",
17+
"source": "Exercise by the JumpstartLab team for students at The Turing School of Software and Design.",
18+
"source_url": "https://www.turing.edu/"
19+
}

‎exercises/practice/kindergarten-garden/.meta/tests.toml‎

Lines changed: 61 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,61 @@
1+
# This is an auto-generated file.
2+
#
3+
# Regenerating this file via `configlet sync` will:
4+
# - Recreate every `description` key/value pair
5+
# - Recreate every `reimplements` key/value pair, where they exist in problem-specifications
6+
# - Remove any `include = true` key/value pair (an omitted `include` key implies inclusion)
7+
# - Preserve any other key/value pair
8+
#
9+
# As user-added comments (using the # character) will be removed when this file
10+
# is regenerated, comments can be added via a `comment` key.
11+
12+
[1fc316ed-17ab-4fba-88ef-3ae78296b692]
13+
description = "partial garden -> garden with single student"
14+
15+
[acd19dc1-2200-4317-bc2a-08f021276b40]
16+
description = "partial garden -> different garden with single student"
17+
18+
[c376fcc8-349c-446c-94b0-903947315757]
19+
description = "partial garden -> garden with two students"
20+
21+
[2d620f45-9617-4924-9d27-751c80d17db9]
22+
description = "partial garden -> multiple students for the same garden with three students -> second student's garden"
23+
24+
[57712331-4896-4364-89f8-576421d69c44]
25+
description = "partial garden -> multiple students for the same garden with three students -> third student's garden"
26+
27+
[149b4290-58e1-40f2-8ae4-8b87c46e765b]
28+
description = "full garden -> for Alice, first student's garden"
29+
30+
[ba25dbbc-10bd-4a37-b18e-f89ecd098a5e]
31+
description = "full garden -> for Bob, second student's garden"
32+
33+
[566b621b-f18e-4c5f-873e-be30544b838c]
34+
description = "full garden -> for Charlie"
35+
36+
[3ad3df57-dd98-46fc-9269-1877abf612aa]
37+
description = "full garden -> for David"
38+
39+
[0f0a55d1-9710-46ed-a0eb-399ba8c72db2]
40+
description = "full garden -> for Eve"
41+
42+
[a7e80c90-b140-4ea1-aee3-f4625365c9a4]
43+
description = "full garden -> for Fred"
44+
45+
[9d94b273-2933-471b-86e8-dba68694c615]
46+
description = "full garden -> for Ginny"
47+
48+
[f55bc6c2-ade8-4844-87c4-87196f1b7258]
49+
description = "full garden -> for Harriet"
50+
51+
[759070a3-1bb1-4dd4-be2c-7cce1d7679ae]
52+
description = "full garden -> for Ileana"
53+
54+
[78578123-2755-4d4a-9c7d-e985b8dda1c6]
55+
description = "full garden -> for Joseph"
56+
57+
[6bb66df7-f433-41ab-aec2-3ead6e99f65b]
58+
description = "full garden -> for Kincaid, second to last student's garden"
59+
60+
[d7edec11-6488-418a-94e6-ed509e0fa7eb]
61+
description = "full garden -> for Larry, last student's garden"

‎exercises/practice/kindergarten-garden/KindergartenGarden.lean‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
namespace KindergartenGarden
2+
3+
inductive Plant where
4+
| grass | clover | radishes | violets
5+
deriving BEq, Repr
6+
7+
def plants (diagram : String) (student: String) : Vector Plant 4 :=
8+
sorry --remove this line and implement the function
9+
10+
end KindergartenGarden

‎exercises/practice/kindergarten-garden/KindergartenGardenTest.lean‎

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,44 @@
1+
import LeanTest
2+
import KindergartenGarden
3+
4+
open LeanTest
5+
6+
def kindergartenGardenTests : TestSuite :=
7+
(TestSuite.empty "KindergartenGarden")
8+
|>.addTest "partial garden -> garden with single student" (do
9+
return assertEqual ⟨#[KindergartenGarden.Plant.radishes, KindergartenGarden.Plant.clover, KindergartenGarden.Plant.grass, KindergartenGarden.Plant.grass], by decide⟩ (KindergartenGarden.plants "RC\nGG" "Alice"))
10+
|>.addTest "partial garden -> different garden with single student" (do
11+
return assertEqual ⟨#[KindergartenGarden.Plant.violets, KindergartenGarden.Plant.clover, KindergartenGarden.Plant.radishes, KindergartenGarden.Plant.clover], by decide⟩ (KindergartenGarden.plants "VC\nRC" "Alice"))
12+
|>.addTest "partial garden -> garden with two students" (do
13+
return assertEqual ⟨#[KindergartenGarden.Plant.clover, KindergartenGarden.Plant.grass, KindergartenGarden.Plant.radishes, KindergartenGarden.Plant.clover], by decide⟩ (KindergartenGarden.plants "VVCG\nVVRC" "Bob"))
14+
|>.addTest "partial garden -> multiple students for the same garden with three students -> second student's garden" (do
15+
return assertEqual ⟨#[KindergartenGarden.Plant.clover, KindergartenGarden.Plant.clover, KindergartenGarden.Plant.clover, KindergartenGarden.Plant.clover], by decide⟩ (KindergartenGarden.plants "VVCCGG\nVVCCGG" "Bob"))
16+
|>.addTest "partial garden -> multiple students for the same garden with three students -> third student's garden" (do
17+
return assertEqual ⟨#[KindergartenGarden.Plant.grass, KindergartenGarden.Plant.grass, KindergartenGarden.Plant.grass, KindergartenGarden.Plant.grass], by decide⟩ (KindergartenGarden.plants "VVCCGG\nVVCCGG" "Charlie"))
18+
|>.addTest "full garden -> for Alice, first student's garden" (do
19+
return assertEqual ⟨#[KindergartenGarden.Plant.violets, KindergartenGarden.Plant.radishes, KindergartenGarden.Plant.violets, KindergartenGarden.Plant.radishes], by decide⟩ (KindergartenGarden.plants "VRCGVVRVCGGCCGVRGCVCGCGV\nVRCCCGCRRGVCGCRVVCVGCGCV" "Alice"))
20+
|>.addTest "full garden -> for Bob, second student's garden" (do
21+
return assertEqual ⟨#[KindergartenGarden.Plant.clover, KindergartenGarden.Plant.grass, KindergartenGarden.Plant.clover, KindergartenGarden.Plant.clover], by decide⟩ (KindergartenGarden.plants "VRCGVVRVCGGCCGVRGCVCGCGV\nVRCCCGCRRGVCGCRVVCVGCGCV" "Bob"))
22+
|>.addTest "full garden -> for Charlie" (do
23+
return assertEqual ⟨#[KindergartenGarden.Plant.violets, KindergartenGarden.Plant.violets, KindergartenGarden.Plant.clover, KindergartenGarden.Plant.grass], by decide⟩ (KindergartenGarden.plants "VRCGVVRVCGGCCGVRGCVCGCGV\nVRCCCGCRRGVCGCRVVCVGCGCV" "Charlie"))
24+
|>.addTest "full garden -> for David" (do
25+
return assertEqual ⟨#[KindergartenGarden.Plant.radishes, KindergartenGarden.Plant.violets, KindergartenGarden.Plant.clover, KindergartenGarden.Plant.radishes], by decide⟩ (KindergartenGarden.plants "VRCGVVRVCGGCCGVRGCVCGCGV\nVRCCCGCRRGVCGCRVVCVGCGCV" "David"))
26+
|>.addTest "full garden -> for Eve" (do
27+
return assertEqual ⟨#[KindergartenGarden.Plant.clover, KindergartenGarden.Plant.grass, KindergartenGarden.Plant.radishes, KindergartenGarden.Plant.grass], by decide⟩ (KindergartenGarden.plants "VRCGVVRVCGGCCGVRGCVCGCGV\nVRCCCGCRRGVCGCRVVCVGCGCV" "Eve"))
28+
|>.addTest "full garden -> for Fred" (do
29+
return assertEqual ⟨#[KindergartenGarden.Plant.grass, KindergartenGarden.Plant.clover, KindergartenGarden.Plant.violets, KindergartenGarden.Plant.clover], by decide⟩ (KindergartenGarden.plants "VRCGVVRVCGGCCGVRGCVCGCGV\nVRCCCGCRRGVCGCRVVCVGCGCV" "Fred"))
30+
|>.addTest "full garden -> for Ginny" (do
31+
return assertEqual ⟨#[KindergartenGarden.Plant.clover, KindergartenGarden.Plant.grass, KindergartenGarden.Plant.grass, KindergartenGarden.Plant.clover], by decide⟩ (KindergartenGarden.plants "VRCGVVRVCGGCCGVRGCVCGCGV\nVRCCCGCRRGVCGCRVVCVGCGCV" "Ginny"))
32+
|>.addTest "full garden -> for Harriet" (do
33+
return assertEqual ⟨#[KindergartenGarden.Plant.violets, KindergartenGarden.Plant.radishes, KindergartenGarden.Plant.radishes, KindergartenGarden.Plant.violets], by decide⟩ (KindergartenGarden.plants "VRCGVVRVCGGCCGVRGCVCGCGV\nVRCCCGCRRGVCGCRVVCVGCGCV" "Harriet"))
34+
|>.addTest "full garden -> for Ileana" (do
35+
return assertEqual ⟨#[KindergartenGarden.Plant.grass, KindergartenGarden.Plant.clover, KindergartenGarden.Plant.violets, KindergartenGarden.Plant.clover], by decide⟩ (KindergartenGarden.plants "VRCGVVRVCGGCCGVRGCVCGCGV\nVRCCCGCRRGVCGCRVVCVGCGCV" "Ileana"))
36+
|>.addTest "full garden -> for Joseph" (do
37+
return assertEqual ⟨#[KindergartenGarden.Plant.violets, KindergartenGarden.Plant.clover, KindergartenGarden.Plant.violets, KindergartenGarden.Plant.grass], by decide⟩ (KindergartenGarden.plants "VRCGVVRVCGGCCGVRGCVCGCGV\nVRCCCGCRRGVCGCRVVCVGCGCV" "Joseph"))
38+
|>.addTest "full garden -> for Kincaid, second to last student's garden" (do
39+
return assertEqual ⟨#[KindergartenGarden.Plant.grass, KindergartenGarden.Plant.clover, KindergartenGarden.Plant.clover, KindergartenGarden.Plant.grass], by decide⟩ (KindergartenGarden.plants "VRCGVVRVCGGCCGVRGCVCGCGV\nVRCCCGCRRGVCGCRVVCVGCGCV" "Kincaid"))
40+
|>.addTest "full garden -> for Larry, last student's garden" (do
41+
return assertEqual ⟨#[KindergartenGarden.Plant.grass, KindergartenGarden.Plant.violets, KindergartenGarden.Plant.clover, KindergartenGarden.Plant.violets], by decide⟩ (KindergartenGarden.plants "VRCGVVRVCGGCCGVRGCVCGCGV\nVRCCCGCRRGVCGCRVVCVGCGCV" "Larry"))
42+
43+
def main : IO UInt32 := do
44+
runTestSuitesWithExitCode [kindergartenGardenTests]

‎exercises/practice/kindergarten-garden/lakefile.toml‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
name = "kindergarten-garden"
2+
version = "0.1.0"
3+
defaultTargets = ["KindergartenGardenTest"]
4+
testDriver = "KindergartenGardenTest"
5+
6+
[[lean_lib]]
7+
name = "LeanTest"
8+
srcDir = "vendor/LeanTest"
9+
10+
[[lean_lib]]
11+
name = "KindergartenGarden"
12+
13+
[[lean_exe]]
14+
name = "KindergartenGardenTest"
15+
root = "KindergartenGardenTest"

‎exercises/practice/kindergarten-garden/lean-toolchain‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
leanprover/lean4:v4.25.2

0 commit comments

Comments
 (0)