ScrabbleScore SquareRoot SumOfMultiples Generator (#124)

Author: keiravillekode

exercises/practice/sum-of-multiples/SumOfMultiplesTest.lean

@@ -6,37 +6,37 @@ open LeanTest
 def sumOfMultiplesTests : TestSuite :=
   (TestSuite.empty "SumOfMultiples")
   |>.addTest "no multiples within limit" (do
-      return assertEqual 0 (SumOfMultiples.sum [3, 5] 1))
+      return assertEqual 0 (SumOfMultiples.sum [3,5] 1))
   |>.addTest "one factor has multiples within limit" (do
-      return assertEqual 3 (SumOfMultiples.sum [3, 5] 4))
+      return assertEqual 3 (SumOfMultiples.sum [3,5] 4))
   |>.addTest "more than one multiple within limit" (do
       return assertEqual 9 (SumOfMultiples.sum [3] 7))
   |>.addTest "more than one factor with multiples within limit" (do
-      return assertEqual 23 (SumOfMultiples.sum [3, 5] 10))
+      return assertEqual 23 (SumOfMultiples.sum [3,5] 10))
   |>.addTest "each multiple is only counted once" (do
-      return assertEqual 2318 (SumOfMultiples.sum [3, 5] 100))
+      return assertEqual 2318 (SumOfMultiples.sum [3,5] 100))
   |>.addTest "a much larger limit" (do
-      return assertEqual 233168 (SumOfMultiples.sum [3, 5] 1000))
+      return assertEqual 233168 (SumOfMultiples.sum [3,5] 1000))
   |>.addTest "three factors" (do
-      return assertEqual 51 (SumOfMultiples.sum [7, 13, 17] 20))
+      return assertEqual 51 (SumOfMultiples.sum [7,13,17] 20))
   |>.addTest "factors not relatively prime" (do
-      return assertEqual 30 (SumOfMultiples.sum [4, 6] 15))
+      return assertEqual 30 (SumOfMultiples.sum [4,6] 15))
   |>.addTest "some pairs of factors relatively prime and some not" (do
-      return assertEqual 4419 (SumOfMultiples.sum [5, 6, 8] 150))
+      return assertEqual 4419 (SumOfMultiples.sum [5,6,8] 150))
   |>.addTest "one factor is a multiple of another" (do
-      return assertEqual 275 (SumOfMultiples.sum [5, 25] 51))
+      return assertEqual 275 (SumOfMultiples.sum [5,25] 51))
   |>.addTest "much larger factors" (do
-      return assertEqual 2203160 (SumOfMultiples.sum [43, 47] 10000))
+      return assertEqual 2203160 (SumOfMultiples.sum [43,47] 10000))
   |>.addTest "all numbers are multiples of 1" (do
       return assertEqual 4950 (SumOfMultiples.sum [1] 100))
   |>.addTest "no factors means an empty sum" (do
       return assertEqual 0 (SumOfMultiples.sum [] 10000))
   |>.addTest "the only multiple of 0 is 0" (do
       return assertEqual 0 (SumOfMultiples.sum [0] 1))
   |>.addTest "the factor 0 does not affect the sum of multiples of other factors" (do
-      return assertEqual 3 (SumOfMultiples.sum [3, 0] 4))
+      return assertEqual 3 (SumOfMultiples.sum [3,0] 4))
   |>.addTest "solutions using include-exclude must extend to cardinality greater than 3" (do
-      return assertEqual 39614537 (SumOfMultiples.sum [2, 3, 5, 7, 11] 10000))
+      return assertEqual 39614537 (SumOfMultiples.sum [2,3,5,7,11] 10000))
 
 def main : IO UInt32 := do
   runTestSuitesWithExitCode [sumOfMultiplesTests]

generators/Generator/Generator.lean

@@ -7,6 +7,9 @@ import Generator.DominoesGenerator
 import Generator.HighScoresGenerator
 import Generator.IsogramGenerator
 import Generator.PangramGenerator
+import Generator.ScrabbleScoreGenerator
+import Generator.SquareRootGenerator
+import Generator.SumOfMultiplesGenerator
 import Generator.SublistGenerator
 import Generator.RelativeDistanceGenerator
 import Generator.HouseGenerator
@@ -86,6 +89,9 @@ def dispatch : Std.HashMap String (introGenerator × testCaseGenerator × endBod
     ("HighScores", (HighScoresGenerator.genIntro, HighScoresGenerator.genTestCase, HighScoresGenerator.genEnd)),
     ("Isogram", (IsogramGenerator.genIntro, IsogramGenerator.genTestCase, IsogramGenerator.genEnd)),
     ("Pangram", (PangramGenerator.genIntro, PangramGenerator.genTestCase, PangramGenerator.genEnd)),
+    ("ScrabbleScore", (ScrabbleScoreGenerator.genIntro, ScrabbleScoreGenerator.genTestCase, ScrabbleScoreGenerator.genEnd)),
+    ("SquareRoot", (SquareRootGenerator.genIntro, SquareRootGenerator.genTestCase, SquareRootGenerator.genEnd)),
+    ("SumOfMultiples", (SumOfMultiplesGenerator.genIntro, SumOfMultiplesGenerator.genTestCase, SumOfMultiplesGenerator.genEnd)),
     ("Sublist", (SublistGenerator.genIntro, SublistGenerator.genTestCase, SublistGenerator.genEnd)),
     ("RelativeDistance", (RelativeDistanceGenerator.genIntro, RelativeDistanceGenerator.genTestCase, RelativeDistanceGenerator.genEnd)),
     ("House", (HouseGenerator.genIntro, HouseGenerator.genTestCase, HouseGenerator.genEnd)),

generators/Generator/Generator/ScrabbleScoreGenerator.lean

@@ -0,0 +1,37 @@
+import Lean.Data.Json
+import Std
+import Helper
+
+open Lean
+open Std
+open Helper
+
+namespace ScrabbleScoreGenerator
+
+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"
+  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} {call})"
+
+def genEnd (exercise : String) : String :=
+  s!"
+
+def main : IO UInt32 := do
+  runTestSuitesWithExitCode [{exercise.decapitalize}Tests]
+"
+
+end ScrabbleScoreGenerator

generators/Generator/Generator/SquareRootGenerator.lean

@@ -0,0 +1,37 @@
+import Lean.Data.Json
+import Std
+import Helper
+
+open Lean
+open Std
+open Helper
+
+namespace SquareRootGenerator
+
+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"
+  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} {call})"
+
+def genEnd (exercise : String) : String :=
+  s!"
+
+def main : IO UInt32 := do
+  runTestSuitesWithExitCode [{exercise.decapitalize}Tests]
+"
+
+end SquareRootGenerator

generators/Generator/Generator/SumOfMultiplesGenerator.lean

@@ -0,0 +1,37 @@
+import Lean.Data.Json
+import Std
+import Helper
+
+open Lean
+open Std
+open Helper
+
+namespace SumOfMultiplesGenerator
+
+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"
+  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} {call})"
+
+def genEnd (exercise : String) : String :=
+  s!"
+
+def main : IO UInt32 := do
+  runTestSuitesWithExitCode [{exercise.decapitalize}Tests]
+"
+
+end SumOfMultiplesGenerator