{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications #-}
module T3 where

-- Some e-graph unit tests

import Prelude hiding (not)

-- import Test.Tasty.HUnit
import Data.Equality.Graph
import Data.Equality.Utils
import qualified Data.Equality.Graph.Monad as EGM

data Lang a = And a a
            | Or a a
            | Not a
            | ToElim a
            | Sym Int
            deriving (Functor, Foldable, Traversable, Eq, Ord, Show)

main :: IO ()
main = do
  let _ = EGM.egraph @Lang @() $ do
        id1 <- EGM.represent (Fix (Sym 1))
        id2 <- EGM.represent (Fix (Not (Fix (Not (Fix (Sym 1))))))
        id3 <- EGM.represent (Fix (Sym 2))
        a1  <- EGM.add (Node (And id3 id1))
        a2  <- EGM.add (Node (And id3 id2))
        _ <- EGM.merge a1 a2
        EGM.rebuild -- even rebuilding this fails...
        return (id1,id2)

  -- The children should now be in the same e-class?
  --
  -- Turns out, they don't. So this test should actually be the other way
  -- around (we do not learn s1 ~= s2 from merging a1 and a2)
  --
  -- A counter example:
  -- Consider `f` that returns its second argument (f _ x = x):
  -- so f(a,c) = f(b,c), but a != b
  --
  -- find s1 eg @=? find s2 eg

  return ()