organize generator helper functions in a separate file (#52)

Co-authored-by: oxe-i <[email protected]>

Author: oxe-i

generators/GenerateTestFile.lean

@@ -216,20 +216,17 @@ def addImport (pascalExercise : String) : IO Unit := do
 
 def generateStub (exercise : String) : IO Unit := do
   let pascalExercise := pascalCase exercise
-  let content := s!"import Lean
+  let content :=
+s!"import Lean
 import Std
+import Helper
 
 open Lean
 open Std
+open Helper
 
 namespace {pascalExercise}Generator
 
-instance \{α β} [BEq α] [BEq β] : BEq (Except α β)  where
-  beq
-    | .ok a, .ok b => a == b
-    | .error e1, .error e2 => e1 == e2
-    | _, _ => false
-
 def genIntro (exercise : String) : String := s!\"import LeanTest
 import \{exercise}
 
@@ -238,40 +235,6 @@ open LeanTest
 def \{exercise.decapitalize}Tests : TestSuite :=
   (TestSuite.empty \\\"\{exercise}\\\")\"
 
-def getOk \{α β} (except : Except α β) [Inhabited β] : β := except.toOption |> (·.get!)
-
-def errorToOption (expected : Json) : Option String :=
-  match expected.getObjVal? \"error\" with
-  | .error _ => some s!\"\{expected}\"
-  | .ok _    => none
-
-def toExcept (expected : Json) : Except String String :=
-  match expected.getObjVal? \"error\" with
-  | .error _ => .ok s!\"\{expected}\"
-  | .ok msg  => .error msg.compress
-
-def exceptToString \{α β} [ToString α] [ToString β] (except : Except α β) : String :=
-  match except with
-  | .ok value => s!\"(.ok \{value})\"
-  | .error msg => s!\"(.error \{msg})\"
-
-def insertAllInputs (input : Json) : String :=
-  let map := getOk input.getObj?
-  map.values.map (fun val => s!\"\{val}\") |> (String.intercalate \" \" .)
-
-def intLiteral (n : Int) : String :=
-  if n < 0 then s!\"(\{n})\"
-  else s!\"\{n}\"
-
-def toFloat (value : Json) : Float :=
-  value.getNum? |> (getOk .) |> (·.toFloat)
-
-def toLiteral (string : String) : String :=
-  string.dropWhile (·=='\"') |> (·.dropRightWhile (·=='\"'))
-
-def getFunName (property : Json) : String :=
-  toLiteral property.compress
-
 def genTestCase (exercise : String) (case : TreeMap.Raw String Json) : String :=
   let input := case.get! \"input\"
   let expected := case.get! \"expected\"

generators/Generator/Generator.lean

@@ -22,7 +22,6 @@ namespace Generator
 abbrev introGenerator := String -> String
 abbrev testCaseGenerator := String -> Std.TreeMap.Raw String Lean.Json -> String
 abbrev endBodyGenerator := String -> String
-abbrev extraCasesList := List String
 
 def dispatch : Std.HashMap String (introGenerator × testCaseGenerator × endBodyGenerator) :=
   Std.HashMap.ofList [

generators/Generator/Helper.lean

@@ -0,0 +1,49 @@
+import Std
+import Lean
+
+open Std
+open Lean
+
+namespace Helper
+
+instance {α β} [BEq α] [BEq β] : BEq (Except α β)  where
+  beq
+    | .ok a, .ok b => a == b
+    | .error e1, .error e2 => e1 == e2
+    | _, _ => false
+
+def getOk {α β} (except : Except α β) [Inhabited β] : β := except.toOption |> (·.get!)
+
+def errorToOption (expected : Json) : Option String :=
+  match expected.getObjVal? "error" with
+  | .error _ => some s!"{expected}"
+  | .ok _    => none
+
+def toExcept (expected : Json) : Except String String :=
+  match expected.getObjVal? "error" with
+  | .error _ => .ok s!"{expected}"
+  | .ok msg  => .error msg.compress
+
+def exceptToString {α β} [ToString α] [ToString β] (except : Except α β) : String :=
+  match except with
+  | .ok value => s!"(.ok {value})"
+  | .error msg => s!"(.error {msg})"
+
+def insertAllInputs (input : Json) : String :=
+  let map := getOk input.getObj?
+  map.values.map (fun val => s!"{val}") |> (String.intercalate " " .)
+
+def intLiteral (n : Int) : String :=
+  if n < 0 then s!"({n})"
+  else s!"{n}"
+
+def toFloat (value : Json) : Float :=
+  value.getNum? |> (getOk .) |> (·.toFloat)
+
+def toLiteral (string : String) : String :=
+  string.dropWhile (·=='"') |> (·.dropRightWhile (·=='"'))
+
+def getFunName (property : Json) : String :=
+  toLiteral property.compress
+
+end Helper

generators/lakefile.toml

@@ -6,6 +6,10 @@ defaultTargets = ["generator"]
 name = "Generator"
 srcDir = "Generator"
 
+[[lean_lib]]
+name = "Helper"
+srcDir = "Generator"
+
 [[lean_exe]]
 name = "generator"
 root = "GenerateTestFile"