ghc prover remove standalone type class

Author: EYH0602

src/tfbench/ghc.py

@@ -54,8 +54,6 @@ def ghc_prove_equiv(code: str) -> Result[None, str]:
 
 $new_types
 
-$new_type_classes
-
 type TRUTH $truth_vars = $truth_signature
 type ANSWER $answer_vars = $answer_signature
 
@@ -102,7 +100,6 @@ def get_prover(
     answer = reorder_constraints(answer)
     return PROVER.substitute(
         new_types="\n".join(types_defs),
-        new_type_classes="",  # todo: support new type classes
         truth_vars=_get_var_str(ground_truth),
         truth_signature=_get_body_str(ground_truth),
         answer_vars=_get_var_str(answer),

tests/test_ghc_pure.py

@@ -1,7 +1,7 @@
 from returns.result import Result, Success, Failure
 from funcy import lmap
 from tfbench.ghc import ghc_prove_equiv, get_prover, reorder_constraints
-from tfbench.type_def import def_new_type, def_new_type_class
+from tfbench.type_def import def_new_type, def_new_type_constructor
 
 
 def _equiv(
@@ -10,11 +10,7 @@ def _equiv(
     new_types: list[str] | None = None,
     should_pass: bool = True,
 ):
-    equiv = (
-        get_prover(truth, answer, lmap(def_new_type, new_types))
-        .alt(str)
-        .bind(ghc_prove_equiv)
-    )
+    equiv = get_prover(truth, answer, new_types or []).alt(str).bind(ghc_prove_equiv)
     match equiv:
         case Success(_):
             assert should_pass
@@ -34,30 +30,38 @@ def test_mono():
     """test GHC type equivalence prover for monomorphic types after rewriting"""
     # check with type after rewriting,
     # i.e. T1, ... T_n
-    _equiv("f:: T1-> T1", "g ::T1 -> T1", new_types=["T1"])
+    _equiv("f:: T1-> T1", "g ::T1 -> T1", new_types=[def_new_type("T1")])
     _not_equiv(
         "f:: T1-> T1",
         "g ::T2 -> T2",
-        new_types=["T1", "T2"],
+        new_types=lmap(def_new_type, ["T1", "T2"]),
     )
 
     _equiv(
         "f:: (T1, T2) -> T1",
         "g ::(T1, T2) -> T1",
-        new_types=["T1", "T2"],
+        new_types=lmap(def_new_type, ["T1", "T2"]),
     )
     _equiv(
         "f:: (Int, T2) -> Int",
         "g ::(Int, T2) -> Int",
-        new_types=["T2"],
+        new_types=lmap(def_new_type, ["T2"]),
     )
     _not_equiv(
         "f:: (Int, T2) -> Int",
         "g ::(Int, T2) -> T2",
-        new_types=["T2"],
+        new_types=lmap(def_new_type, ["T2"]),
     )
 
 
 def test_typeclass_in_body():
     f = "f :: T1 -> T2 T3"
-    _equiv(f, f)
+    _equiv(
+        f,
+        f,
+        new_types=[
+            def_new_type("T1"),
+            def_new_type("T3"),
+            def_new_type_constructor("T2", ["a"]),
+        ],
+    )