import Data.List
import Control.Monad

type Subst = [(String, Formula)]
(|->) :: String -> Formula -> Subst
v |-> f = [(v,f)]

data Formula = Var String
             | FTrue  | FFalse
             | FAnd   [Formula]
             | FOr    [Formula]
             | FEquiv [Formula]
             | Formula :=> Formula
             | Formula :<= Formula
             | Formula := Formula
             | Not Formula
              deriving (Eq,Ord)

match :: (MonadPlus m) => Formula -> Formula -> [(Formula,m Subst)]
match (Var p) f = [(f, return (p |-> f))]
match FFalse FFalse = [(FFalse, mzero)]
match FFalse _ = []
match FTrue FTrue =  [(FTrue,mzero)]
match FTrue _ = []
match (Not f) (Not g) = map (prod Not id) $ match f g
match (FAnd fs1) (FAnd fs2) = [ matchList FAnd fs1 l | l <- permutations fs2 ]
match (FOr fs1) (FOr fs2) = [ matchList FOr fs1 l | l <- permutations fs2 ]
match (FEquiv fs1) (FEquiv fs2) = [ matchList FEquiv fs1 l | l <- permutations fs2 ]

matchList :: (MonadPlus m) => ([Formula] -> Formula ) -> [Formula] -> [Formula] -> (Formula,m Subst)
matchList cons fs1 fs2 = prod cons msum $ unzip.concat $ zipWith match fs1 fs2

prod f g (a,b) = (f a, g b)