clean up simplification tests, now very pretty

test/Main.hs

@@ -1,3 +1,5 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+
 module Main where
 
 import Test.TypeSpec hiding ( And )
@@ -6,25 +8,37 @@ import Rerefined.Predicates
 import Rerefined.Predicate
 import TypeLevelShow.Utils ( type (++) )
 
+-- | Pretty opaque predicate for simplification proofs.
+data Opaque
+instance Predicate Opaque where type PredicateName d Opaque = "p"
+
+-- | Shorthand for the pretty opaque predicate.
+type P = Opaque
+
 main :: IO ()
 main = print spec
 
 spec :: Expect
-    (And Fail    Succeed `SimplifiesTo` Fail
- -/- And Succeed Fail    `SimplifiesTo` Fail
- -/- And Succeed Succeed `SimplifiesTo` Succeed
- -/- And Fail    Fail    `SimplifiesTo` Fail
-
- -/- Or  Succeed Fail    `SimplifiesTo` Succeed
- -/- Or  Fail    Succeed `SimplifiesTo` Succeed
- -/- Or  Succeed Succeed `SimplifiesTo` Succeed
- -/- Or  Fail    Fail    `SimplifiesTo` Fail
+    -- AND identity laws
+    (And Fail    P       `SimplifiesTo` Fail
+ -/- And P       Fail    `SimplifiesTo` Fail
+ -/- And Succeed P       `SimplifiesTo` P
+ -/- And P       Succeed `SimplifiesTo` P
+
+     -- OR identity laws
+ -/- Or  Succeed P       `SimplifiesTo` Succeed
+ -/- Or  P       Succeed `SimplifiesTo` Succeed
+ -/- Or  Fail    P       `SimplifiesTo` P
+ -/- Or  P       Fail    `SimplifiesTo` P
+
+     -- other
  -/- And (CompareLength RelOpLT 3) (CompareLength RelOpGT 3)
         `SimplifiesTo` Fail
     )
 spec = Valid
 
--- | TODO I'd like to write my own message here, but type-spec is complicated.
+-- | TODO I'd like to write my own failure message here, but type-spec is
+--   complicated.
 type SimplifiesTo p p' = It
     (PredicateName 0 p ++ " simplifies to " ++ PredicateName 0 p')
     (TrySimplify p `Is` Just p')