Hamming LineUp TwoFer Generator

Author: keiravillekode

generators/Generator/Generator.lean

@@ -17,6 +17,9 @@ import Generator.RationalNumbersGenerator
 import Generator.GigasecondGenerator
 import Generator.CamiciaGenerator
 import Generator.ChangeGenerator
+import Generator.HammingGenerator
+import Generator.LineUpGenerator
+import Generator.TwoFerGenerator
 import Generator.YachtGenerator
 import Generator.PalindromeProductsGenerator
 import Generator.EliudsEggsGenerator
@@ -93,6 +96,9 @@ def dispatch : Std.HashMap String (introGenerator × testCaseGenerator × endBod
     ("Gigasecond", (GigasecondGenerator.genIntro, GigasecondGenerator.genTestCase, GigasecondGenerator.genEnd)),
     ("Camicia", (CamiciaGenerator.genIntro, CamiciaGenerator.genTestCase, CamiciaGenerator.genEnd)),
     ("Change", (ChangeGenerator.genIntro, ChangeGenerator.genTestCase, ChangeGenerator.genEnd)),
+    ("Hamming", (HammingGenerator.genIntro, HammingGenerator.genTestCase, HammingGenerator.genEnd)),
+    ("LineUp", (LineUpGenerator.genIntro, LineUpGenerator.genTestCase, LineUpGenerator.genEnd)),
+    ("TwoFer", (TwoFerGenerator.genIntro, TwoFerGenerator.genTestCase, TwoFerGenerator.genEnd)),
     ("Yacht", (YachtGenerator.genIntro, YachtGenerator.genTestCase, YachtGenerator.genEnd)),
     ("PalindromeProducts", (PalindromeProductsGenerator.genIntro, PalindromeProductsGenerator.genTestCase, PalindromeProductsGenerator.genEnd)),
     ("EliudsEggs", (EliudsEggsGenerator.genIntro, EliudsEggsGenerator.genTestCase, EliudsEggsGenerator.genEnd)),

generators/Generator/Generator/HammingGenerator.lean

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

generators/Generator/Generator/LineUpGenerator.lean

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

generators/Generator/Generator/TwoFerGenerator.lean

@@ -0,0 +1,39 @@
+import Lean.Data.Json
+import Std
+import Helper
+
+open Lean
+open Std
+open Helper
+
+namespace TwoFerGenerator
+
+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 := match case.get! "input" |> (·.getObjValD "name") |> (·.getStr?) with
+  | .error _ => none
+  | .ok name    => some s!"\"{name}\""
+  let expected := case.get! "expected"
+  let description := case.get! "description"
+              |> (·.compress)
+  let funName := getFunName (case.get! "property")
+  let call := s!"({exercise}.{funName} {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 TwoFerGenerator