DifferenceOfSquares Knapsack Generator (exercism#128)

Author: keiravillekode

exercises/practice/difference-of-squares/DifferenceOfSquaresTest.lean

@@ -5,23 +5,23 @@ open LeanTest
 
 def differenceOfSquaresTests : TestSuite :=
   (TestSuite.empty "DifferenceOfSquares")
-  |>.addTest "Square the sum of the numbers up to the given number - square of sum 1" (do
+  |>.addTest "Square the sum of the numbers up to the given number -> square of sum 1" (do
       return assertEqual 1 (DifferenceOfSquares.squareOfSum 1))
-  |>.addTest "Square the sum of the numbers up to the given number - square of sum 5" (do
+  |>.addTest "Square the sum of the numbers up to the given number -> square of sum 5" (do
       return assertEqual 225 (DifferenceOfSquares.squareOfSum 5))
-  |>.addTest "Square the sum of the numbers up to the given number - square of sum 100" (do
+  |>.addTest "Square the sum of the numbers up to the given number -> square of sum 100" (do
       return assertEqual 25502500 (DifferenceOfSquares.squareOfSum 100))
-  |>.addTest "Sum the squares of the numbers up to the given number - sum of squares 1" (do
+  |>.addTest "Sum the squares of the numbers up to the given number -> sum of squares 1" (do
       return assertEqual 1 (DifferenceOfSquares.sumOfSquares 1))
-  |>.addTest "Sum the squares of the numbers up to the given number - sum of squares 5" (do
+  |>.addTest "Sum the squares of the numbers up to the given number -> sum of squares 5" (do
       return assertEqual 55 (DifferenceOfSquares.sumOfSquares 5))
-  |>.addTest "Sum the squares of the numbers up to the given number - sum of squares 100" (do
+  |>.addTest "Sum the squares of the numbers up to the given number -> sum of squares 100" (do
       return assertEqual 338350 (DifferenceOfSquares.sumOfSquares 100))
-  |>.addTest "Subtract sum of squares from square of sums - difference of squares 1" (do
+  |>.addTest "Subtract sum of squares from square of sums -> difference of squares 1" (do
       return assertEqual 0 (DifferenceOfSquares.differenceOfSquares 1))
-  |>.addTest "Subtract sum of squares from square of sums - difference of squares 5" (do
+  |>.addTest "Subtract sum of squares from square of sums -> difference of squares 5" (do
       return assertEqual 170 (DifferenceOfSquares.differenceOfSquares 5))
-  |>.addTest "Subtract sum of squares from square of sums - difference of squares 100" (do
+  |>.addTest "Subtract sum of squares from square of sums -> difference of squares 100" (do
       return assertEqual 25164150 (DifferenceOfSquares.differenceOfSquares 100))
 
 def main : IO UInt32 := do

generators/Generator/Generator.lean

@@ -26,6 +26,8 @@ import Generator.HammingGenerator
 import Generator.LineUpGenerator
 import Generator.TwoFerGenerator
 import Generator.YachtGenerator
+import Generator.DifferenceOfSquaresGenerator
+import Generator.KnapsackGenerator
 import Generator.PalindromeProductsGenerator
 import Generator.EliudsEggsGenerator
 import Generator.EtlGenerator
@@ -113,6 +115,8 @@ def dispatch : Std.HashMap String (introGenerator × testCaseGenerator × endBod
     ("LineUp", (LineUpGenerator.genIntro, LineUpGenerator.genTestCase, LineUpGenerator.genEnd)),
     ("TwoFer", (TwoFerGenerator.genIntro, TwoFerGenerator.genTestCase, TwoFerGenerator.genEnd)),
     ("Yacht", (YachtGenerator.genIntro, YachtGenerator.genTestCase, YachtGenerator.genEnd)),
+    ("DifferenceOfSquares", (DifferenceOfSquaresGenerator.genIntro, DifferenceOfSquaresGenerator.genTestCase, DifferenceOfSquaresGenerator.genEnd)),
+    ("Knapsack", (KnapsackGenerator.genIntro, KnapsackGenerator.genTestCase, KnapsackGenerator.genEnd)),
     ("PalindromeProducts", (PalindromeProductsGenerator.genIntro, PalindromeProductsGenerator.genTestCase, PalindromeProductsGenerator.genEnd)),
     ("EliudsEggs", (EliudsEggsGenerator.genIntro, EliudsEggsGenerator.genTestCase, EliudsEggsGenerator.genEnd)),
     ("Etl", (EtlGenerator.genIntro, EtlGenerator.genTestCase, EtlGenerator.genEnd)),

generators/Generator/Generator/DifferenceOfSquaresGenerator.lean

@@ -0,0 +1,37 @@
+import Lean.Data.Json
+import Std
+import Helper
+
+open Lean
+open Std
+open Helper
+
+namespace DifferenceOfSquaresGenerator
+
+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 DifferenceOfSquaresGenerator

generators/Generator/Generator/KnapsackGenerator.lean

@@ -0,0 +1,44 @@
+import Lean.Data.Json
+import Std
+import Helper
+
+open Lean
+open Std
+open Helper
+
+namespace KnapsackGenerator
+
+def genIntro (exercise : String) : String := s!"import LeanTest
+import {exercise}
+
+open LeanTest
+
+def {exercise.decapitalize}Tests : TestSuite :=
+  (TestSuite.empty \"{exercise}\")"
+
+def serializeItem (item : Json) : String :=
+  let weight := item.getObjValD "weight" |>.getInt? |> getOk |> intLiteral
+  let value := item.getObjValD "value" |>.getInt? |> getOk |> intLiteral
+  "{ weight := " ++ weight ++ ", value := " ++ value ++ " }"
+
+def genTestCase (exercise : String) (case : TreeMap.Raw String Json) : String :=
+  let input := case.get! "input"
+  let maximumWeight := input.getObjValD "maximumWeight"
+  let items := serializeList (input.getObjValD "items") serializeItem
+  let expected := case.get! "expected"
+  let description := case.get! "description"
+              |> (·.compress)
+  let funName := getFunName (case.get! "property")
+  let call := s!"({exercise}.{funName} {maximumWeight} #{items})"
+  s!"
+  |>.addTest {description} (do
+      return assertEqual {expected} {call})"
+
+def genEnd (exercise : String) : String :=
+  s!"
+
+def main : IO UInt32 := do
+  runTestSuitesWithExitCode [{exercise.decapitalize}Tests]
+"
+
+end KnapsackGenerator