generate darts, hello-world tests

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

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

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

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