From b2e5bfd68cd1b3512dbe81b9525bb50ba6a6003f Mon Sep 17 00:00:00 2001
From: Eric Willigers <keiravillekode@gmail.com>
Date: Sun, 15 Feb 2026 05:51:46 +1100
Subject: [PATCH] generate darts, hello-world tests

---
 exercises/practice/darts/DartsTest.lean       |  2 +-
 generators/Generator/Generator.lean           |  4 ++
 .../Generator/Generator/DartsGenerator.lean   | 43 +++++++++++++++++++
 .../Generator/HelloWorldGenerator.lean        | 36 ++++++++++++++++
 4 files changed, 84 insertions(+), 1 deletion(-)
 create mode 100644 generators/Generator/Generator/DartsGenerator.lean
 create mode 100644 generators/Generator/Generator/HelloWorldGenerator.lean

diff --git a/exercises/practice/darts/DartsTest.lean b/exercises/practice/darts/DartsTest.lean
index 758b054..4c0979b 100644
--- a/exercises/practice/darts/DartsTest.lean
+++ b/exercises/practice/darts/DartsTest.lean
@@ -26,7 +26,7 @@ def dartsTests : TestSuite :=
   |>.addTest "Just outside the middle circle" (do
       return assertEqual 1 (Darts.score (-3.6) (-3.6)))
   |>.addTest "Just within the outer circle" (do
-      return assertEqual 1 (Darts.score (-7.0) 7.0))
+      return assertEqual 1 (Darts.score (-7) 7))
   |>.addTest "Just outside the outer circle" (do
       return assertEqual 0 (Darts.score 7.1 (-7.1)))
   |>.addTest "Asymmetric position between the inner and middle circles" (do
diff --git a/generators/Generator/Generator.lean b/generators/Generator/Generator.lean
index 31629d8..5a7ae15 100644
--- a/generators/Generator/Generator.lean
+++ b/generators/Generator/Generator.lean
@@ -14,6 +14,8 @@ import Generator.SquareRootGenerator
 import Generator.SumOfMultiplesGenerator
 import Generator.SublistGenerator
 import Generator.AffineCipherGenerator
+import Generator.DartsGenerator
+import Generator.HelloWorldGenerator
 import Generator.MeetupGenerator
 import Generator.NthPrimeGenerator
 import Generator.RelativeDistanceGenerator
@@ -109,6 +111,8 @@ def dispatch : Std.HashMap String (introGenerator × testCaseGenerator × endBod
     ("SumOfMultiples", (SumOfMultiplesGenerator.genIntro, SumOfMultiplesGenerator.genTestCase, SumOfMultiplesGenerator.genEnd)),
     ("Sublist", (SublistGenerator.genIntro, SublistGenerator.genTestCase, SublistGenerator.genEnd)),
     ("AffineCipher", (AffineCipherGenerator.genIntro, AffineCipherGenerator.genTestCase, AffineCipherGenerator.genEnd)),
+    ("Darts", (DartsGenerator.genIntro, DartsGenerator.genTestCase, DartsGenerator.genEnd)),
+    ("HelloWorld", (HelloWorldGenerator.genIntro, HelloWorldGenerator.genTestCase, HelloWorldGenerator.genEnd)),
     ("Meetup", (MeetupGenerator.genIntro, MeetupGenerator.genTestCase, MeetupGenerator.genEnd)),
     ("NthPrime", (NthPrimeGenerator.genIntro, NthPrimeGenerator.genTestCase, NthPrimeGenerator.genEnd)),
     ("RelativeDistance", (RelativeDistanceGenerator.genIntro, RelativeDistanceGenerator.genTestCase, RelativeDistanceGenerator.genEnd)),
diff --git a/generators/Generator/Generator/DartsGenerator.lean b/generators/Generator/Generator/DartsGenerator.lean
new file mode 100644
index 0000000..b57db7c
--- /dev/null
+++ b/generators/Generator/Generator/DartsGenerator.lean
@@ -0,0 +1,43 @@
+import Lean.Data.Json
+import Std
+import Helper
+
+open Lean
+open Std
+open Helper
+
+namespace DartsGenerator
+
+def genIntro (exercise : String) : String := s!"import LeanTest
+import {exercise}
+
+open LeanTest
+
+def {exercise.decapitalize}Tests : TestSuite :=
+  (TestSuite.empty \"{exercise}\")"
+
+def toLiteral (v : Json) : String :=
+  let str := s!"{Json.getNum? v |> getOk}"
+  if str.startsWith "-" then s!"({str})" else str
+
+def genTestCase (exercise : String) (case : TreeMap.Raw String Json) : String :=
+  let input := case.get! "input"
+  let x := input |> (·.getObjValD "x") |> toLiteral
+  let y := input |> (·.getObjValD "y") |> toLiteral
+  let expected := case.get! "expected"
+  let description := case.get! "description"
+              |> (·.compress)
+  let funName := getFunName (case.get! "property")
+  let call := s!"({exercise}.{funName} {x} {y})"
+  s!"
+  |>.addTest {description} (do
+      return assertEqual {expected} {call})"
+
+def genEnd (exercise : String) : String :=
+  s!"
+
+def main : IO UInt32 := do
+  runTestSuitesWithExitCode [{exercise.decapitalize}Tests]
+"
+
+end DartsGenerator
diff --git a/generators/Generator/Generator/HelloWorldGenerator.lean b/generators/Generator/Generator/HelloWorldGenerator.lean
new file mode 100644
index 0000000..224a4a1
--- /dev/null
+++ b/generators/Generator/Generator/HelloWorldGenerator.lean
@@ -0,0 +1,36 @@
+import Lean.Data.Json
+import Std
+import Helper
+
+open Lean
+open Std
+open Helper
+
+namespace HelloWorldGenerator
+
+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 expected := case.get! "expected"
+  let description := case.get! "description"
+              |> (·.compress)
+  let funName := getFunName (case.get! "property")
+  let call := s!"{exercise}.{funName}"
+  s!"
+  |>.addTest {description} (do
+      return assertEqual {expected} {call})"
+
+def genEnd (exercise : String) : String :=
+  s!"
+
+def main : IO UInt32 := do
+  runTestSuitesWithExitCode [{exercise.decapitalize}Tests]
+"
+
+end HelloWorldGenerator