module Congruence_Closure where

import Data.List

{- Implement the "..." below and check that at least all PROPERTY equations hold. -}

{--- Ground term datatype: a function symbol applied to sub-terms. This time no variables! ---}

data Term = App String [Term]
  deriving (Read, Eq)

instance Show Term where
  show (App f xs) = if xs == [] then f else f ++ "(" ++ intercalate "," (map show xs) ++ ")"

subterms :: Term -> [Term]
subterms t@(App c ts) = t:concatMap subterms ts

type Equation = (Term, Term)

type Signature = [(String, Int)]

{--

We suggest two ways to implement congruence closure
(of course, you only need to implement one way):

A) As presented in "Term Rewriting and All That" pp 62:
    iterate over the list of equations by adding all reflexive, symmetric, transitive and congruence closures

B) Compute the equivalence classes of equivalent terms, you are allowed to change the type of closure to

     closure :: Signature -> [Equation] -> [[Term]]
     
   Start with the equivalent terms from the equation list, and implement merge for transitivity, and
   congruence closure on equivalence classes.

A) is simpler, but B) is more fun :-)

--}

closure :: Signature -> [Equation] -> [Equation]
closure sig eqs = ...

sig :: Signature
sig = [("f", 2), ("g", 1), ("a", 0), ("b", 0), ("c", 0)]

f x y = App "f" [x, y]
g x = App "g" [x]
a = App "a" []
b = App "b" []
c = App "c" []

s = App "s" []
t = App "t" []

{-- PROPERTIES --}

{-- PROPERTY prop1 == True --}
prop1 = (s, t) `elem` closure sig [(f a b, a), (s, f (f a b) b), (t, a)]

{-- PROPERTY prop2 == False --}
prop2 = (s, t) `elem` closure sig [(f a b, a), (s, f (f a b) b), (t, b)]