Add saturation test mentioned in egg's #60 discussion

hegg.cabal

@@ -109,7 +109,7 @@ test-suite hegg-test
     hs-source-dirs:   test
     main-is:          Test.hs
     other-modules:    Invariants, Sym, Lambda, SimpleSym,
-                      T1
+                      T1, T2
 
     other-extensions: OverloadedStrings
     build-depends:    base,

test/T2.hs

@@ -0,0 +1,55 @@
+{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE OverloadedStrings #-}
+module T2 where
+
+-- Tests whether this saturates just like mwillsey claims that it does in egg!
+
+import Prelude hiding (not)
+
+import Test.Tasty.HUnit
+import Data.Deriving
+import Data.Equality.Matching
+import Data.Equality.Analysis
+import Data.Equality.Language
+import Data.Equality.Extraction
+import Data.Equality.Saturation
+
+data Lang a = And a a
+            | Or a a
+            | Not a
+            | ToElim a
+            | Sym Int
+            deriving (Functor, Foldable, Traversable)
+
+deriveEq1 ''Lang
+deriveOrd1 ''Lang
+deriveShow1 ''Lang
+
+instance Analysis Lang where
+  type Domain Lang = ()
+  makeA _ _ = ()
+  joinA = (<>)
+
+instance Language Lang
+
+x, y :: Pattern Lang
+x = "x"
+y = "y"
+not :: Pattern Lang -> Pattern Lang
+not = pat . Not
+
+rules :: [Rewrite Lang]
+rules =
+  [ pat (x `And` y) := not (pat (not x `Or` not y))
+  , pat (x `Or` y) := not (pat (not x `And` not y))
+  , not (not x) := pat (ToElim x)
+  , pat (ToElim x) := x
+  ]
+
+main :: IO ()
+main = do
+  fst (equalitySaturation (Fix $ (Fix $ Not $ Fix $ Sym 0) `And` (Fix $ Not $ Fix $ Sym 1)) rules depthCost) @?= Fix (Not $ Fix $ (Fix $ Sym 0) `Or` (Fix $ Sym 1))
+  pure ()
+

test/Test.hs

@@ -12,6 +12,7 @@ import Lambda
 import SimpleSym
 
 import qualified T1
+import qualified T2
 
 tests :: TestTree
 tests = testGroup "Tests"
@@ -20,6 +21,7 @@ tests = testGroup "Tests"
   , simpleSymTests
   , invariants
   , testCase "T1" (T1.main `catch` (\(e :: SomeException) -> assertFailure (show e)))
+  , testCase "T2" (T2.main `catch` (\(e :: SomeException) -> assertFailure (show e)))
   ]
 
 main :: IO ()